New goto-instrument option: --print-global-state-size

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

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;
+}

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

src/goto-instrument/count_eloc.cpp

@@ -16,10 +16,14 @@ 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;
@@ -141,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";
+}

src/goto-instrument/count_eloc.h

@@ -14,10 +14,26 @@ Date: December 2012
 #ifndef CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H
 #define CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H
 
-#include <goto-programs/goto_model.h>
+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"
 
 #endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -91,7 +91,6 @@ Author: Daniel Kroening, [email protected]
 #include "wmm/weak_memory.h"
 #include "call_sequences.h"
 #include "accelerate/accelerate.h"
-#include "count_eloc.h"
 #include "horn_encoding.h"
 #include "thread_instrumentation.h"
 #include "skip_loops.h"
@@ -484,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());
@@ -1454,15 +1459,14 @@ void goto_instrument_parse_optionst::help()
     " --dump-cpp                   generate C++ source\n"
     " --dot                        generate CFG graph in DOT format\n"
     " --interpreter                do concrete execution\n"
-    " --count-eloc                 count effective lines of code\n"
-    " --list-eloc                  list full path names of lines containing code\n" // NOLINT(*)
     "\n"
     "Diagnosis:\n"
     " --show-loops                 show the loops in the program\n"
     HELP_SHOW_PROPERTIES
     " --show-symbol-table          show loaded symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    HELP_GOTO_PROGRAM_STATS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --print-internal-representation\n" // NOLINTNEXTLINE(*)
     "                              show verbose internal representation of the program\n"
@@ -1471,8 +1475,6 @@ void goto_instrument_parse_optionst::help()
     " --show-natural-loops         show natural loop heads\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --list-calls-args            list all function calls with their arguments\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --print-path-lengths         print statistics about control-flow graph paths\n"
     " --call-graph                 show graph of function calls\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --reachable-call-graph       show graph of function calls potentially reachable from main function\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -27,6 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/generate_function_bodies.h>
 
+#include "count_eloc.h"
+
 // clang-format off
 #define GOTO_INSTRUMENT_OPTIONS \
   "(all)" \
@@ -81,17 +83,18 @@ Author: Daniel Kroening, [email protected]
   "(accelerate)(constant-propagator)" \
   "(k-induction):(step-case)(base-case)" \
   "(show-call-sequences)(check-call-sequence)" \
-  "(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \
+  "(interpreter)(show-reaching-definitions)" \
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
-  "(show-threaded)(list-calls-args)(print-path-lengths)" \
+  "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
   OPT_FLUSH \
   "(splice-call):" \
   OPT_REMOVE_CALLS_NO_BODY \
-  OPT_REPLACE_FUNCTION_BODY
+  OPT_REPLACE_FUNCTION_BODY \
+  OPT_GOTO_PROGRAM_STATS
 
 // clang-format on