From d8c5a9854a03481fbf3b2421dde075ffc6a77ad8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 15:23:49 +0100 Subject: [PATCH 1/2] Cleanup options handling of count-eloc, list-eloc, print-path-lengths --- src/goto-instrument/count_eloc.cpp | 1 + src/goto-instrument/count_eloc.h | 14 +++++++++++++- .../goto_instrument_parse_options.cpp | 6 +----- .../goto_instrument_parse_options.h | 9 ++++++--- 4 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index e6162a79b19..252562ba037 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -20,6 +20,7 @@ Date: December 2012 #include #include +#include typedef std::unordered_set linest; typedef std::unordered_map filest; diff --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index 9a140eec52b..da86c359aeb 100644 --- a/src/goto-instrument/count_eloc.h +++ b/src/goto-instrument/count_eloc.h @@ -14,10 +14,22 @@ Date: December 2012 #ifndef CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H #define CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H -#include +class goto_modelt; void count_eloc(const goto_modelt &); void list_eloc(const goto_modelt &); void print_path_lengths(const goto_modelt &); +#define OPT_GOTO_PROGRAM_STATS \ + "(count-eloc)" \ + "(list-eloc)" \ + "(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-path-lengths print statistics about control-flow graph " \ + "paths\n" + #endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index fdb1fc664f6..80afdf2d6cd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -91,7 +91,6 @@ Author: Daniel Kroening, kroening@kroening.com #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" @@ -1454,8 +1453,6 @@ 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" @@ -1463,6 +1460,7 @@ void goto_instrument_parse_optionst::help() " --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 +1469,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" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 60fbe8bd485..779574b364c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -27,6 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "count_eloc.h" + // clang-format off #define GOTO_INSTRUMENT_OPTIONS \ "(all)" \ @@ -81,17 +83,18 @@ Author: Daniel Kroening, kroening@kroening.com "(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 From d46a55c3e36116bbdcfbaa64ed804e82ad2cf0b9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 15:25:14 +0100 Subject: [PATCH 2/2] Add new goto-instrument option print-global-state-size --- CHANGELOG | 1 + .../print_global_state_size1/main.c | 9 +++ .../print_global_state_size1/test.desc | 8 +++ src/goto-instrument/count_eloc.cpp | 58 ++++++++++++++++++- src/goto-instrument/count_eloc.h | 4 ++ .../goto_instrument_parse_options.cpp | 6 ++ 6 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 regression/goto-instrument/print_global_state_size1/main.c create mode 100644 regression/goto-instrument/print_global_state_size1/test.desc diff --git a/CHANGELOG b/CHANGELOG index 2022bb01308..06fd741315a 100644 --- a/CHANGELOG +++ b/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 --git a/regression/goto-instrument/print_global_state_size1/main.c b/regression/goto-instrument/print_global_state_size1/main.c new file mode 100644 index 00000000000..68f16e02519 --- /dev/null +++ b/regression/goto-instrument/print_global_state_size1/main.c @@ -0,0 +1,9 @@ +#include + +uint32_t some_global_var; +int8_t other_global_var; + +int main(int argc, char *argv[]) +{ + return 0; +} diff --git a/regression/goto-instrument/print_global_state_size1/test.desc b/regression/goto-instrument/print_global_state_size1/test.desc new file mode 100644 index 00000000000..1dad42d154a --- /dev/null +++ b/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 --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 252562ba037..56552f9ce19 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -16,12 +16,15 @@ Date: December 2012 #include #include -#include #include +#include +#include #include #include +#include + typedef std::unordered_set linest; typedef std::unordered_map filest; typedef std::unordered_map 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 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 --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index da86c359aeb..eb719d08a55 100644 --- a/src/goto-instrument/count_eloc.h +++ b/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 --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 80afdf2d6cd..efe68017124 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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());