Add new goto-instrument option print-global-state-size

Author: tautschnig

Diff for: CHANGELOG

@@ -6,6 +6,7 @@
   of --undefined-function-is-assume-false
 * The --fixedbv command-line option has been removed
   (it was marked deprecated in January 2017)
+* GOTO-INSTRUMENT: New option --print-global-state-size
 
 
 5.8

Diff for: regression/goto-instrument/print_global_state_size1/main.c

@@ -0,0 +1,9 @@
+#include <stdint.h>
+
+uint32_t some_global_var;
+int8_t other_global_var;
+
+int main(int argc, char *argv[])
+{
+  return 0;
+}

Diff for: regression/goto-instrument/print_global_state_size1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--print-global-state-size
+^EXIT=0$
+^SIGNAL=0$
+^Total size of global objects: 40 bits$
+--
+^warning: ignoring

Diff for: src/goto-instrument/count_eloc.cpp

@@ -16,12 +16,15 @@ Date: December 2012
 #include <iostream>
 #include <unordered_set>
 
-#include <util/prefix.h>
 #include <util/file_util.h>
+#include <util/pointer_offset_size.h>
+#include <util/prefix.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/goto_model.h>
 
+#include <linking/static_lifetime_init.h>
+
 typedef std::unordered_set<irep_idt> linest;
 typedef std::unordered_map<irep_idt, linest> filest;
 typedef std::unordered_map<irep_idt, filest> working_dirst;
@@ -142,3 +145,56 @@ void print_path_lengths(const goto_modelt &goto_model)
       ++n_reachable;
   std::cout << "Reachable instructions: " << n_reachable << "\n";
 }
+
+void print_global_state_size(const goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  // if we have a linked object, only account for those that are used
+  // (slice-global-inits may have been used to avoid unnecessary initialization)
+  goto_functionst::function_mapt::const_iterator f_it =
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION);
+  const bool has_initialize =
+    f_it != goto_model.goto_functions.function_map.end();
+  std::unordered_set<irep_idt> initialized;
+
+  if(has_initialize)
+  {
+    for(const auto &ins : f_it->second.body.instructions)
+    {
+      if(ins.is_assign())
+      {
+        const code_assignt &code_assign = to_code_assign(ins.code);
+        object_descriptor_exprt ode;
+        ode.build(code_assign.lhs(), ns);
+
+        if(ode.root_object().id() == ID_symbol)
+        {
+          const symbol_exprt &symbol_expr = to_symbol_expr(ode.root_object());
+          initialized.insert(symbol_expr.get_identifier());
+        }
+      }
+    }
+  }
+
+  mp_integer total_size = 0;
+
+  for(const auto &symbol_entry : goto_model.symbol_table.symbols)
+  {
+    const symbolt &symbol = symbol_entry.second;
+    if(
+      symbol.is_type || symbol.is_macro || symbol.type.id() == ID_code ||
+      symbol.type.get_bool(ID_C_constant) ||
+      has_prefix(id2string(symbol.name), CPROVER_PREFIX) ||
+      (has_initialize && initialized.find(symbol.name) == initialized.end()))
+    {
+      continue;
+    }
+
+    const mp_integer bits = pointer_offset_bits(symbol.type, ns);
+    if(bits > 0)
+      total_size += bits;
+  }
+
+  std::cout << "Total size of global objects: " << total_size << " bits\n";
+}

Diff for: src/goto-instrument/count_eloc.h

@@ -19,16 +19,20 @@ class goto_modelt;
 void count_eloc(const goto_modelt &);
 void list_eloc(const goto_modelt &);
 void print_path_lengths(const goto_modelt &);
+void print_global_state_size(const goto_modelt &);
 
 #define OPT_GOTO_PROGRAM_STATS                                                 \
   "(count-eloc)"                                                               \
   "(list-eloc)"                                                                \
+  "(print-global-state-size)"                                                  \
   "(print-path-lengths)"
 
 #define HELP_GOTO_PROGRAM_STATS                                                \
   " --count-eloc                 count effective lines of code\n"              \
   " --list-eloc                  list full path names of lines "               \
   "containing code\n"                                                          \
+  " --print-global-state-size    count the total number of bits of global "    \
+  "objects\n"                                                                  \
   " --print-path-lengths         print statistics about control-flow graph "   \
   "paths\n"
 

Diff for: src/goto-instrument/goto_instrument_parse_options.cpp

@@ -483,6 +483,12 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
+    if(cmdline.isset("print-global-state-size"))
+    {
+      print_global_state_size(goto_model);
+      return CPROVER_EXIT_SUCCESS;
+    }
+
     if(cmdline.isset("list-symbols"))
     {
       show_symbol_table_brief(goto_model, get_ui());