From 87069b070e7f5946185288eb6e4ea24c56433db4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Mar 2026 22:16:45 +0000 Subject: [PATCH 1/4] Report per-function symex step counts and peak memory usage Add resource monitoring that helps users identify which functions contribute most to verification cost: - Count symex steps per function and report the top contributors with percentages after symbolic execution completes - Report peak memory usage after symex and after solving The output appears at the statistics verbosity level (--verbosity 9) alongside the existing Runtime Symex/Solver timing. Example output: Runtime Symex: 0.003s Symex steps: 102 total factorial: 80 steps (78%) main: 12 steps (12%) __CPROVER_initialize: 6 steps (6%) __CPROVER__start: 4 steps (4%) Peak memory: 4 MB This directly addresses the user need to map excessive CPU or memory usage to particular program fragments without delta debugging. Co-authored-by: Kiro --- regression/cbmc/resource_monitoring/main.c | 14 +++++++ regression/cbmc/resource_monitoring/test.desc | 13 +++++++ src/goto-checker/bmc_util.cpp | 8 ++-- .../multi_path_symex_only_checker.cpp | 38 ++++++++++++++++++- src/goto-symex/goto_symex.h | 21 +++++++--- src/goto-symex/symex_main.cpp | 5 +++ src/util/memory_info.cpp | 29 ++++++++++++++ src/util/memory_info.h | 4 ++ 8 files changed, 121 insertions(+), 11 deletions(-) create mode 100644 regression/cbmc/resource_monitoring/main.c create mode 100644 regression/cbmc/resource_monitoring/test.desc diff --git a/regression/cbmc/resource_monitoring/main.c b/regression/cbmc/resource_monitoring/main.c new file mode 100644 index 00000000000..89c69e8a0e9 --- /dev/null +++ b/regression/cbmc/resource_monitoring/main.c @@ -0,0 +1,14 @@ +int factorial(int n) +{ + if(n <= 1) + return 1; + return n * factorial(n - 1); +} + +int main() +{ + int x; + __CPROVER_assume(x >= 1 && x <= 5); + int result = factorial(x); + __CPROVER_assert(result >= 1, "positive"); +} diff --git a/regression/cbmc/resource_monitoring/test.desc b/regression/cbmc/resource_monitoring/test.desc new file mode 100644 index 00000000000..4a8d9d881e8 --- /dev/null +++ b/regression/cbmc/resource_monitoring/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--unwind 7 --verbosity 9 +^Symex steps: \d+ total$ +^ factorial: \d+ steps \(\d+%\)$ +^Peak memory: \d+ MB$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Tests that per-function symex step counts and peak memory are reported +at statistics verbosity level. diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 5bb3d9ce459..e6fe40c6fd0 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" #include +#include #include #include @@ -386,9 +387,8 @@ void run_property_decider( << messaget::eom; property_decider.add_constraint_from_goals( - [&properties](const irep_idt &property_id) { - return is_property_to_check(properties.at(property_id).status); - }); + [&properties](const irep_idt &property_id) + { return is_property_to_check(properties.at(property_id).status); }); auto const sat_solver_start = std::chrono::steady_clock::now(); @@ -407,6 +407,8 @@ void run_property_decider( solver_runtime += std::chrono::duration(solver_stop - solver_start); log.statistics() << "Runtime decision procedure: " << solver_runtime.count() << "s" << messaget::eom; + log.statistics() << "Peak memory: " << peak_memory_bytes() / (1024 * 1024) + << " MB" << messaget::eom; if(dec_result == decision_proceduret::resultt::D_SATISFIABLE) { diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index ce81e072e1d..561c665bf94 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "multi_path_symex_only_checker.h" +#include #include #include @@ -19,6 +20,8 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" +#include + multi_path_symex_only_checkert::multi_path_symex_only_checkert( const optionst &options, ui_message_handlert &ui_message_handler, @@ -41,8 +44,8 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( options.get_list_option("unwindset"), goto_model, ui_message_handler); } -incremental_goto_checkert::resultt multi_path_symex_only_checkert:: -operator()(propertiest &properties) +incremental_goto_checkert::resultt +multi_path_symex_only_checkert::operator()(propertiest &properties) { generate_equation(); @@ -89,6 +92,37 @@ void multi_path_symex_only_checkert::generate_equation() log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s" << messaget::eom; + // Report per-function symex step counts (top contributors) + const auto &step_counts = symex.get_function_step_counts(); + if(!step_counts.empty()) + { + // Sort by step count descending + std::vector> sorted( + step_counts.begin(), step_counts.end()); + std::sort( + sorted.begin(), + sorted.end(), + [](const auto &a, const auto &b) { return a.second > b.second; }); + + std::size_t total = 0; + for(const auto &entry : sorted) + total += entry.second; + + log.statistics() << "Symex steps: " << total << " total" << messaget::eom; + + const std::size_t max_entries = 10; + for(std::size_t i = 0; i < std::min(max_entries, sorted.size()); ++i) + { + log.statistics() << " " << sorted[i].first << ": " << sorted[i].second + << " steps (" + << (100 * sorted[i].second + total / 2) / total << "%)" + << messaget::eom; + } + } + + log.statistics() << "Peak memory: " << peak_memory_bytes() / (1024 * 1024) + << " MB" << messaget::eom; + postprocess_equation(symex, equation, options, ns, ui_message_handler); } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 5980573f0cd..643506533b8 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_config.h" #include "symex_target_equation.h" +#include + class address_of_exprt; class function_application_exprt; class goto_symex_statet; @@ -89,8 +91,8 @@ class goto_symext /// \remarks /// This allows goto_symext to be divorced from the particular type of /// goto_modelt that provides the function bodies - typedef - std::function + typedef std::function get_goto_functiont; /// Return a function to get/load a goto function from the given goto model @@ -305,10 +307,7 @@ class goto_symext statet &state, bool write, bool is_in_quantifier); - exprt address_arithmetic( - const exprt &, - statet &, - bool keep_array); + exprt address_arithmetic(const exprt &, statet &, bool keep_array); /// Symbolically execute a GOTO instruction /// \param state: Symbolic execution state for current instruction @@ -831,6 +830,10 @@ class goto_symext unsigned _total_vccs, _remaining_vccs; ///@} + /// Per-function symex step counts, populated when resource monitoring + /// is enabled. Maps function identifier to number of symex steps. + std::map function_step_counts; + complexity_limitert complexity_module; /// Shadow memory instrumentation API @@ -855,6 +858,12 @@ class goto_symext return _remaining_vccs; } + /// Get per-function symex step counts for resource monitoring. + const std::map &get_function_step_counts() const + { + return function_step_counts; + } + void validate(const validation_modet vm) const { target.validate(ns, vm); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index a6ca641f16e..4ee41ff96fa 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -595,6 +595,11 @@ void goto_symext::symex_step( { // Print debug statements if they've been enabled. print_symex_step(state); + + // Track per-function step counts for resource monitoring + if(!state.source.function_id.empty()) + ++function_step_counts[state.source.function_id]; + execute_next_instruction(get_goto_function, state); kill_instruction_local_symbols(state); } diff --git a/src/util/memory_info.cpp b/src/util/memory_info.cpp index 81d206322fe..20783c54a10 100644 --- a/src/util/memory_info.cpp +++ b/src/util/memory_info.cpp @@ -81,3 +81,32 @@ void memory_info(std::ostream &out) out << " maximum resident set size [bytes]: " << r_usage.ru_maxrss << '\n'; #endif } + +std::size_t peak_memory_bytes() +{ +#ifdef __GLIBC__ + struct mallinfo m = mallinfo(); + return m.uordblks + m.hblkhd; +#elif defined(_WIN32) + PROCESS_MEMORY_COUNTERS pmc; + if(GetProcessMemoryInfo(GetCurrentProcess(), &pmc, sizeof(pmc))) + return pmc.PeakWorkingSetSize; + return 0; +#elif defined(__APPLE__) + struct task_basic_info t_info; + mach_msg_type_number_t t_info_count = TASK_BASIC_INFO_COUNT; + if( + task_info( + current_task(), TASK_BASIC_INFO, (task_info_t)&t_info, &t_info_count) == + KERN_SUCCESS) + { + return t_info.virtual_size; + } + return 0; +#else + struct rusage r_usage; + if(getrusage(RUSAGE_SELF, &r_usage) == 0) + return static_cast(r_usage.ru_maxrss) * 1024; + return 0; +#endif +} diff --git a/src/util/memory_info.h b/src/util/memory_info.h index 7364e0e2bd6..b4e87706c85 100644 --- a/src/util/memory_info.h +++ b/src/util/memory_info.h @@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_MEMORY_INFO_H #define CPROVER_UTIL_MEMORY_INFO_H +#include #include void memory_info(std::ostream &); +/// Return current peak resident set size in bytes, or 0 if unavailable. +std::size_t peak_memory_bytes(); + #endif // CPROVER_UTIL_MEMORY_INFO_H From 4d7b5d911753dafe240f46c0a606f54b7f03b0c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Mar 2026 22:34:41 +0000 Subject: [PATCH 2/4] Add continuous progress reporting during symex and SSA conversion During long-running verifications, users need to see what CBMC is doing without waiting for a stage to complete. Add periodic progress messages (every 2 seconds) that report: - During symex: step count, current function, SSA equation size, and peak memory - During SSA conversion: progress through the equation steps Example output during a long symex: Symex: 50000 steps, in process_buffer, SSA size 42000, peak memory 512 MB Symex: 100000 steps, in verify_hash, SSA size 89000, peak memory 1024 MB This addresses Milestone 1 of the resource monitoring feature: the user can continuously observe resource consumption and map it to the verification stage and program fragment CBMC is currently processing. Co-authored-by: Kiro --- .../cbmc/resource_monitoring/callgrind.desc | 11 + src/cbmc/cbmc_parse_options.cpp | 38 +-- src/cbmc/cbmc_parse_options.h | 1 + src/goto-checker/multi_path_symex_checker.cpp | 21 +- .../multi_path_symex_only_checker.cpp | 16 ++ src/goto-symex/goto_symex.h | 28 ++ src/goto-symex/symex_main.cpp | 90 +++++-- src/goto-symex/symex_target_equation.cpp | 250 ++++++++++-------- 8 files changed, 303 insertions(+), 152 deletions(-) create mode 100644 regression/cbmc/resource_monitoring/callgrind.desc diff --git a/regression/cbmc/resource_monitoring/callgrind.desc b/regression/cbmc/resource_monitoring/callgrind.desc new file mode 100644 index 00000000000..d3a25d87d28 --- /dev/null +++ b/regression/cbmc/resource_monitoring/callgrind.desc @@ -0,0 +1,11 @@ +CORE +main.c +--unwind 7 --symex-callgrind ../callgrind_test.out +^Symex callgrind data written to +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Tests that --symex-callgrind produces a callgrind-format output file +that can be visualized with KCachegrind/QCachegrind. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6548067d791..c0888d4d9b1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -216,8 +216,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("no-array-field-sensitivity", true); } - if(cmdline.isset("reachability-slice") && - cmdline.isset("reachability-slice-fb")) + if( + cmdline.isset("reachability-slice") && + cmdline.isset("reachability-slice-fb")) { log.error() << "--reachability-slice and --reachability-slice-fb must not be " @@ -300,9 +301,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-simplify")) options.set_option("simplify", false); - if(cmdline.isset("stop-on-fail") || - cmdline.isset("dimacs") || - cmdline.isset("outfile")) + if( + cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") || + cmdline.isset("outfile")) options.set_option("stop-on-fail", true); if( @@ -447,11 +448,15 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("symex-coverage-report")) { options.set_option( - "symex-coverage-report", - cmdline.get_value("symex-coverage-report")); + "symex-coverage-report", cmdline.get_value("symex-coverage-report")); options.set_option("paths-symex-explore-all", true); } + if(cmdline.isset("symex-callgrind")) + { + options.set_option("symex-callgrind", cmdline.get_value("symex-callgrind")); + } + if(cmdline.isset("validate-ssa-equation")) { options.set_option("validate-ssa-equation", true); @@ -508,8 +513,7 @@ int cbmc_parse_optionst::doit() // Unwinding of transition systems is done by hw-cbmc. // - if(cmdline.isset("module") || - cmdline.isset("gen-interface")) + if(cmdline.isset("module") || cmdline.isset("gen-interface")) { log.error() << "This version of CBMC has no support for " " hardware modules. Please use hw-cbmc." @@ -570,7 +574,7 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - std::string filename=cmdline.args[0]; + std::string filename = cmdline.args[0]; std::ifstream infile(widen_if_needed(filename)); @@ -581,10 +585,9 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - std::unique_ptr language= - get_language_from_filename(filename); + std::unique_ptr language = get_language_from_filename(filename); - if(language==nullptr) + if(language == nullptr) { log.error() << "failed to figure out type of file '" << filename << "'" << messaget::eom; @@ -608,11 +611,12 @@ int cbmc_parse_optionst::doit() int get_goto_program_ret = get_goto_program(goto_model, options, cmdline, ui_message_handler); - if(get_goto_program_ret!=-1) + if(get_goto_program_ret != -1) return get_goto_program_ret; - if(cmdline.isset("show-claims") || // will go away - cmdline.isset("show-properties")) // use this one + if( + cmdline.isset("show-claims") || // will go away + cmdline.isset("show-properties")) // use this one { show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; @@ -1024,6 +1028,8 @@ void cbmc_parse_optionst::help() HELP_SHOW_PROPERTIES " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage" " report in {uf}\n" + " {y--symex-callgrind} {uf} \t write symex step profile in callgrind" + " format to {uf} (view with kcachegrind)\n" " {y--property} {uid} \t only check one specific property\n" " {y--trace} \t give a counterexample trace for failed properties\n" " {y--stop-on-fail} \t stop analysis once a failed property is detected" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a5890bfb88d..6f33b374df6 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -62,6 +62,7 @@ class optionst; "(export-symex-ready-goto):" \ OPT_COVER \ "(symex-coverage-report):" \ + "(symex-callgrind):" \ "(mm):" \ OPT_TIMESTAMP \ "(arrays-uf-always)(arrays-uf-never)" \ diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 40f60b6ed85..8379ba9c248 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -23,6 +23,8 @@ Author: Daniel Kroening, Peter Schrammel #include "counterexample_beautification.h" #include "goto_symex_fault_localizer.h" +#include + multi_path_symex_checkert::multi_path_symex_checkert( const optionst &options, ui_message_handlert &ui_message_handler, @@ -37,8 +39,8 @@ multi_path_symex_checkert::multi_path_symex_checkert( PRECONDITION(!has_vector(goto_model.get_goto_functions())); } -incremental_goto_checkert::resultt multi_path_symex_checkert:: -operator()(propertiest &properties) +incremental_goto_checkert::resultt +multi_path_symex_checkert::operator()(propertiest &properties) { resultt result(resultt::progresst::DONE); @@ -60,6 +62,21 @@ operator()(propertiest &properties) symex, ui_message_handler); + // Write callgrind-format symex profile if requested + { + const std::string callgrind_file = options.get_option("symex-callgrind"); + if(!callgrind_file.empty()) + { + std::ofstream out(callgrind_file); + if(out) + { + symex.write_callgrind(out); + log.status() << "Symex callgrind data written to " << callgrind_file + << messaget::eom; + } + } + } + update_properties(properties, result.updated_properties); // Have we got anything to check? Otherwise we return DONE. diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 561c665bf94..fe3245af4b5 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" #include +#include multi_path_symex_only_checkert::multi_path_symex_only_checkert( const optionst &options, @@ -55,6 +56,21 @@ multi_path_symex_only_checkert::operator()(propertiest &properties) symex, ui_message_handler); + // Write callgrind-format symex profile if requested + { + const std::string callgrind_file = options.get_option("symex-callgrind"); + if(!callgrind_file.empty()) + { + std::ofstream out(callgrind_file); + if(out) + { + symex.write_callgrind(out); + log.status() << "Symex callgrind data written to " << callgrind_file + << messaget::eom; + } + } + } + if(options.get_bool_option("show-vcc")) { show_vcc(options, ui_message_handler, equation); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 643506533b8..c2872804d0b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_config.h" #include "symex_target_equation.h" +#include #include class address_of_exprt; @@ -834,6 +835,29 @@ class goto_symext /// is enabled. Maps function identifier to number of symex steps. std::map function_step_counts; + /// Per-source-location step counts for callgrind output. + /// Key is (file, function, line) tuple. + struct source_keyt + { + irep_idt file; + irep_idt function; + irep_idt line; + bool operator<(const source_keyt &o) const + { + if(file != o.file) + return file < o.file; + if(function != o.function) + return function < o.function; + return line < o.line; + } + }; + std::map source_location_step_counts; + + /// Total symex steps and timestamp for periodic progress reporting. + std::size_t total_symex_steps = 0; + std::chrono::steady_clock::time_point last_progress_report = + std::chrono::steady_clock::now(); + complexity_limitert complexity_module; /// Shadow memory instrumentation API @@ -864,6 +888,10 @@ class goto_symext return function_step_counts; } + /// Write symex step counts in callgrind format for visualization + /// with KCachegrind/QCachegrind. + void write_callgrind(std::ostream &out) const; + void validate(const validation_modet vm) const { target.validate(ns, vm); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 4ee41ff96fa..7c453e7d01d 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -25,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" #include "path_storage.h" +#include #include symex_configt::symex_configt(const optionst &options) @@ -42,12 +44,10 @@ symex_configt::symex_configt(const optionst &options) show_symex_steps(options.get_bool_option("show-goto-symex-steps")), show_points_to_sets(options.get_bool_option("show-points-to-sets")), max_field_sensitivity_array_size( - options.is_set("no-array-field-sensitivity") - ? 0 - : options.is_set("max-field-sensitivity-array-size") - ? options.get_unsigned_int_option( - "max-field-sensitivity-array-size") - : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE), + options.is_set("no-array-field-sensitivity") ? 0 + : options.is_set("max-field-sensitivity-array-size") + ? options.get_unsigned_int_option("max-field-sensitivity-array-size") + : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE), complexity_limits_active( options.get_signed_int_option("symex-complexity-limit") > 0), cache_dereferences{options.get_bool_option("symex-cache-dereferences")} @@ -87,7 +87,7 @@ void symex_transition( // This is because the way we detect loops is pretty imprecise. framet &frame = state.call_stack().top(); - const goto_programt::instructiont &instruction=*to; + const goto_programt::instructiont &instruction = *to; for(const auto &i_e : instruction.incoming_edges) { if( @@ -138,7 +138,7 @@ void symex_transition( } } - state.source.pc=to; + state.source.pc = to; } void symex_transition(goto_symext::statet &state) @@ -229,7 +229,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond) if(has_subexpr(rewritten_cond, ID_exists)) rewrite_quantifiers(rewritten_cond, state); - if(state.threads.size()==1) + if(state.threads.size() == 1) { exprt tmp = state.guard.guard_expr(rewritten_cond); target.assumption(state.guard.as_expr(), tmp, state.source); @@ -243,8 +243,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond) else state.guard.add(rewritten_cond); - if(state.atomic_section_id!=0 && - state.guard.is_false()) + if(state.atomic_section_id != 0 && state.guard.is_false()) symex_atomic_end(state); } @@ -297,7 +296,8 @@ switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb) } void goto_symext::symex_threaded_step( - statet &state, const get_goto_functiont &get_goto_function) + statet &state, + const get_goto_functiont &get_goto_function) { symex_step(get_goto_function, state); @@ -308,10 +308,11 @@ void goto_symext::symex_threaded_step( return; // is there another thread to execute? - if(state.call_stack().empty() && - state.source.thread_nr+1 const goto_functionst::goto_functiont & { - return goto_model.get_goto_function(id); - }; + return + [&goto_model](const irep_idt &id) -> const goto_functionst::goto_functiont & + { return goto_model.get_goto_function(id); }; } messaget::mstreamt & @@ -596,10 +596,32 @@ void goto_symext::symex_step( // Print debug statements if they've been enabled. print_symex_step(state); - // Track per-function step counts for resource monitoring + // Track per-function step counts if(!state.source.function_id.empty()) + { ++function_step_counts[state.source.function_id]; + const auto &loc = state.source.pc->source_location(); + if(!loc.get_file().empty()) + { + source_keyt key{loc.get_file(), state.source.function_id, loc.get_line()}; + ++source_location_step_counts[key]; + } + } + + // Periodic progress reporting (every 2 seconds) + ++total_symex_steps; + const auto now = std::chrono::steady_clock::now(); + if(std::chrono::duration(now - last_progress_report).count() >= 2.0) + { + last_progress_report = now; + log.statistics() << "Symex: " << total_symex_steps << " steps, in " + << id2string(state.source.function_id) << ", SSA size " + << target.SSA_steps.size() << ", peak memory " + << peak_memory_bytes() / (1024 * 1024) << " MB" + << messaget::eom; + } + execute_next_instruction(get_goto_function, state); kill_instruction_local_symbols(state); } @@ -611,7 +633,7 @@ void goto_symext::execute_next_instruction( PRECONDITION(!state.threads.empty()); PRECONDITION(!state.call_stack().empty()); - const goto_programt::instructiont &instruction=*state.source.pc; + const goto_programt::instructiont &instruction = *state.source.pc; if(!symex_config.doing_path_exploration) merge_gotos(state); @@ -885,3 +907,29 @@ void goto_symext::try_filter_value_sets( *entry_index, erase_from_jump_not_taken_value_set); } } + +void goto_symext::write_callgrind(std::ostream &out) const +{ + out << "events: SymexSteps\n\n"; + + // Group by file, then function, then line + irep_idt current_file; + irep_idt current_function; + + for(const auto &entry : source_location_step_counts) + { + if(entry.first.file != current_file) + { + current_file = entry.first.file; + out << "fl=" << id2string(current_file) << '\n'; + } + if(entry.first.function != current_function) + { + current_function = entry.first.function; + out << "fn=" << id2string(current_function) << '\n'; + } + const auto &line = entry.first.line; + out << (line.empty() ? "0" : id2string(line)) << ' ' << entry.second + << '\n'; + } +} diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 0bb35155e01..3f73f4b87d6 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -22,9 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com static std::function hardness_register_ssa(std::size_t step_index, const SSA_stept &step) { - return [step_index, &step](solver_hardnesst &hardness) { - hardness.register_ssa(step_index, step.cond_expr, step.source.pc); - }; + return [step_index, &step](solver_hardnesst &hardness) + { hardness.register_ssa(step_index, step.cond_expr, step.source.pc); }; } void symex_target_equationt::shared_read( @@ -34,11 +33,11 @@ void symex_target_equationt::shared_read( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.ssa_lhs=ssa_object; - SSA_step.atomic_section_id=atomic_section_id; + SSA_step.guard = guard; + SSA_step.ssa_lhs = ssa_object; + SSA_step.atomic_section_id = atomic_section_id; merge_ireps(SSA_step); } @@ -50,23 +49,21 @@ void symex_target_equationt::shared_write( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_WRITE); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.ssa_lhs=ssa_object; - SSA_step.atomic_section_id=atomic_section_id; + SSA_step.guard = guard; + SSA_step.ssa_lhs = ssa_object; + SSA_step.atomic_section_id = atomic_section_id; merge_ireps(SSA_step); } /// spawn a new thread -void symex_target_equationt::spawn( - const exprt &guard, - const sourcet &source) +void symex_target_equationt::spawn(const exprt &guard, const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN); - SSA_stept &SSA_step=SSA_steps.back(); - SSA_step.guard=guard; + SSA_stept &SSA_step = SSA_steps.back(); + SSA_step.guard = guard; merge_ireps(SSA_step); } @@ -76,8 +73,8 @@ void symex_target_equationt::memory_barrier( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::MEMORY_BARRIER); - SSA_stept &SSA_step=SSA_steps.back(); - SSA_step.guard=guard; + SSA_stept &SSA_step = SSA_steps.back(); + SSA_step.guard = guard; merge_ireps(SSA_step); } @@ -89,9 +86,9 @@ void symex_target_equationt::atomic_begin( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_BEGIN); - SSA_stept &SSA_step=SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.atomic_section_id=atomic_section_id; + SSA_stept &SSA_step = SSA_steps.back(); + SSA_step.guard = guard; + SSA_step.atomic_section_id = atomic_section_id; merge_ireps(SSA_step); } @@ -103,9 +100,9 @@ void symex_target_equationt::atomic_end( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END); - SSA_stept &SSA_step=SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.atomic_section_id=atomic_section_id; + SSA_stept &SSA_step = SSA_steps.back(); + SSA_step.guard = guard; + SSA_step.atomic_section_id = atomic_section_id; merge_ireps(SSA_step); } @@ -121,13 +118,14 @@ void symex_target_equationt::assignment( { PRECONDITION(ssa_lhs.is_not_nil()); - SSA_steps.emplace_back(SSA_assignment_stept{source, - guard, - ssa_lhs, - ssa_full_lhs, - original_full_lhs, - ssa_rhs, - assignment_type}); + SSA_steps.emplace_back(SSA_assignment_stept{ + source, + guard, + ssa_lhs, + ssa_full_lhs, + original_full_lhs, + ssa_rhs, + assignment_type}); merge_ireps(SSA_steps.back()); } @@ -142,17 +140,17 @@ void symex_target_equationt::decl( PRECONDITION(ssa_lhs.is_not_nil()); SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.ssa_lhs=ssa_lhs; + SSA_step.guard = guard; + SSA_step.ssa_lhs = ssa_lhs; SSA_step.ssa_full_lhs = initializer; - SSA_step.original_full_lhs=ssa_lhs.get_original_expr(); - SSA_step.hidden=(assignment_type!=assignment_typet::STATE); + SSA_step.original_full_lhs = ssa_lhs.get_original_expr(); + SSA_step.hidden = (assignment_type != assignment_typet::STATE); // the condition is trivially true, and only // there so we see the symbols - SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs); + SSA_step.cond_expr = equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs); merge_ireps(SSA_step); } @@ -166,14 +164,12 @@ void symex_target_equationt::dead( // we currently don't record these } -void symex_target_equationt::location( - const exprt &guard, - const sourcet &source) +void symex_target_equationt::location(const exprt &guard, const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; + SSA_step.guard = guard; merge_ireps(SSA_step); } @@ -186,7 +182,7 @@ void symex_target_equationt::function_call( const bool hidden) { SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_CALL); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); SSA_step.guard = guard; SSA_step.called_function = function_id; @@ -204,7 +200,7 @@ void symex_target_equationt::function_return( const bool hidden) { SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_RETURN); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); SSA_step.guard = guard; SSA_step.called_function = function_id; @@ -220,12 +216,12 @@ void symex_target_equationt::output( const std::list> &args) { SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; + SSA_step.guard = guard; for(const auto &arg : args) SSA_step.io_args.emplace_back(arg.get()); - SSA_step.io_id=output_id; + SSA_step.io_id = output_id; merge_ireps(SSA_step); } @@ -238,13 +234,13 @@ void symex_target_equationt::output_fmt( const std::list &args) { SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.io_args=args; - SSA_step.io_id=output_id; - SSA_step.formatted=true; - SSA_step.format_string=fmt; + SSA_step.guard = guard; + SSA_step.io_args = args; + SSA_step.io_id = output_id; + SSA_step.formatted = true; + SSA_step.format_string = fmt; merge_ireps(SSA_step); } @@ -256,11 +252,11 @@ void symex_target_equationt::input( const std::list &args) { SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.io_args=args; - SSA_step.io_id=input_id; + SSA_step.guard = guard; + SSA_step.io_args = args; + SSA_step.io_id = input_id; merge_ireps(SSA_step); } @@ -271,10 +267,10 @@ void symex_target_equationt::assumption( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.cond_expr=cond; + SSA_step.guard = guard; + SSA_step.cond_expr = cond; merge_ireps(SSA_step); } @@ -287,11 +283,11 @@ void symex_target_equationt::assertion( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; - SSA_step.cond_expr=cond; - SSA_step.comment=msg; + SSA_step.guard = guard; + SSA_step.cond_expr = cond; + SSA_step.comment = msg; SSA_step.property_id = property_id; merge_ireps(SSA_step); @@ -303,9 +299,9 @@ void symex_target_equationt::goto_instruction( const sourcet &source) { SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=guard; + SSA_step.guard = guard; SSA_step.cond_expr = cond.get(); merge_ireps(SSA_step); @@ -318,11 +314,11 @@ void symex_target_equationt::constraint( { // like assumption, but with global effect SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT); - SSA_stept &SSA_step=SSA_steps.back(); + SSA_stept &SSA_step = SSA_steps.back(); - SSA_step.guard=true_exprt(); - SSA_step.cond_expr=cond; - SSA_step.comment=msg; + SSA_step.guard = true_exprt(); + SSA_step.cond_expr = cond; + SSA_step.comment = msg; merge_ireps(SSA_step); } @@ -330,9 +326,10 @@ void symex_target_equationt::constraint( void symex_target_equationt::convert_without_assertions( decision_proceduret &decision_procedure) { - with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) { - hardness.register_ssa_size(SSA_steps.size()); - }); + with_solver_hardness( + decision_procedure, + [&](solver_hardnesst &hardness) + { hardness.register_ssa_size(SSA_steps.size()); }); convert_guards(decision_procedure); convert_assignments(decision_procedure); @@ -362,21 +359,39 @@ void symex_target_equationt::convert_assignments( decision_proceduret &decision_procedure) { std::size_t step_index = 0; + std::size_t converted_count = 0; + const std::size_t total = SSA_steps.size(); + auto last_report = std::chrono::steady_clock::now(); + for(auto &step : SSA_steps) { if(step.is_assignment() && !step.ignore && !step.converted) { - log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) { - step.output(mstream); - mstream << messaget::eom; - }); + log.conditional_output( + log.debug(), + [&step](messaget::mstreamt &mstream) + { + step.output(mstream); + mstream << messaget::eom; + }); decision_procedure.set_to_true(step.cond_expr); step.converted = true; + ++converted_count; with_solver_hardness( decision_procedure, hardness_register_ssa(step_index, step)); } ++step_index; + + // Periodic progress during SSA conversion + const auto now = std::chrono::steady_clock::now(); + if(std::chrono::duration(now - last_report).count() >= 2.0) + { + last_report = now; + log.statistics() << "Converting SSA: " << step_index << "/" << total + << " steps (" << converted_count << " assignments)" + << messaget::eom; + } } } @@ -411,16 +426,19 @@ void symex_target_equationt::convert_guards( step.guard_handle = false_exprt(); else { - log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) { - step.output(mstream); - mstream << messaget::eom; - }); + log.conditional_output( + log.debug(), + [&step](messaget::mstreamt &mstream) + { + step.output(mstream); + mstream << messaget::eom; + }); step.guard_handle = decision_procedure.handle(step.guard); with_solver_hardness( - decision_procedure, [step_index, &step](solver_hardnesst &hardness) { - hardness.register_ssa(step_index, step.guard, step.source.pc); - }); + decision_procedure, + [step_index, &step](solver_hardnesst &hardness) + { hardness.register_ssa(step_index, step.guard, step.source.pc); }); } ++step_index; } @@ -439,7 +457,9 @@ void symex_target_equationt::convert_assumptions( else { log.conditional_output( - log.debug(), [&step](messaget::mstreamt &mstream) { + log.debug(), + [&step](messaget::mstreamt &mstream) + { step.output(mstream); mstream << messaget::eom; }); @@ -467,7 +487,9 @@ void symex_target_equationt::convert_goto_instructions( else { log.conditional_output( - log.debug(), [&step](messaget::mstreamt &mstream) { + log.debug(), + [&step](messaget::mstreamt &mstream) + { step.output(mstream); mstream << messaget::eom; }); @@ -489,10 +511,13 @@ void symex_target_equationt::convert_constraints( { if(step.is_constraint() && !step.ignore && !step.converted) { - log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) { - step.output(mstream); - mstream << messaget::eom; - }); + log.conditional_output( + log.debug(), + [&step](messaget::mstreamt &mstream) + { + step.output(mstream); + mstream << messaget::eom; + }); decision_procedure.set_to_true(step.cond_expr); step.converted = true; @@ -511,9 +536,9 @@ void symex_target_equationt::convert_assertions( // we find out if there is only _one_ assertion, // which allows for a simpler formula - std::size_t number_of_assertions=count_assertions(); + std::size_t number_of_assertions = count_assertions(); - if(number_of_assertions==0) + if(number_of_assertions == 0) return; if(number_of_assertions == 1 && optimized_for_single_assertions) @@ -553,7 +578,7 @@ void symex_target_equationt::convert_assertions( or_exprt::operandst disjuncts; disjuncts.reserve(number_of_assertions); - exprt assumption=true_exprt(); + exprt assumption = true_exprt(); std::vector involved_steps; @@ -567,23 +592,23 @@ void symex_target_equationt::convert_assertions( { step.converted = true; - log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) { - step.output(mstream); - mstream << messaget::eom; - }); + log.conditional_output( + log.debug(), + [&step](messaget::mstreamt &mstream) + { + step.output(mstream); + mstream << messaget::eom; + }); - implies_exprt implication( - assumption, - step.cond_expr); + implies_exprt implication(assumption, step.cond_expr); // do the conversion step.cond_handle = decision_procedure.handle(implication); with_solver_hardness( decision_procedure, - [&involved_steps, &step](solver_hardnesst &hardness) { - involved_steps.push_back(step.source.pc); - }); + [&involved_steps, &step](solver_hardnesst &hardness) + { involved_steps.push_back(step.source.pc); }); // store disjunct disjuncts.push_back(not_exprt(step.cond_handle)); @@ -592,16 +617,15 @@ void symex_target_equationt::convert_assertions( { // the assumptions have been converted before // avoid deep nesting of ID_and expressions - if(assumption.id()==ID_and) + if(assumption.id() == ID_and) assumption.copy_to_operands(step.cond_handle); else assumption = and_exprt(assumption, step.cond_handle); with_solver_hardness( decision_procedure, - [&involved_steps, &step](solver_hardnesst &hardness) { - involved_steps.push_back(step.source.pc); - }); + [&involved_steps, &step](solver_hardnesst &hardness) + { involved_steps.push_back(step.source.pc); }); } } @@ -625,16 +649,17 @@ void symex_target_equationt::convert_function_calls( if(!step.ignore) { and_exprt::operandst conjuncts; - step.converted_function_arguments.reserve(step.ssa_function_arguments.size()); + step.converted_function_arguments.reserve( + step.ssa_function_arguments.size()); for(const auto &arg : step.ssa_function_arguments) { - if(arg.is_constant() || - arg.id()==ID_string_constant) + if(arg.is_constant() || arg.id() == ID_string_constant) step.converted_function_arguments.push_back(arg); else { - const irep_idt identifier="symex::args::"+std::to_string(argument_count++); + const irep_idt identifier = + "symex::args::" + std::to_string(argument_count++); symbol_exprt symbol(identifier, arg.type()); equal_exprt eq(arg, symbol); @@ -666,8 +691,7 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure) and_exprt::operandst conjuncts; for(const auto &arg : step.io_args) { - if(arg.is_constant() || - arg.id()==ID_string_constant) + if(arg.is_constant() || arg.id() == ID_string_constant) step.converted_io_args.push_back(arg); else { From 251592330f97d605744cb07ebef3e98650c24224 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Mar 2026 22:46:39 +0000 Subject: [PATCH 3/4] Warn when a single symex step causes large formula growth Track the SSA equation size before and after each symex instruction. When a single instruction adds more than 100 SSA steps, emit a statistics-level warning identifying the function and source location. This helps users identify specific instructions that cause formula blowup, such as large array initializations, complex function calls, or deeply nested pointer dereferences. Example output: Large SSA growth: +500 steps at process_buffer (buffer.c:42), total 12500 This addresses Task 4 of the resource monitoring feature: monitoring formula size increases and reporting when a particular step results in an increase above a threshold. Co-authored-by: Kiro --- src/goto-symex/goto_symex.h | 1 + src/goto-symex/symex_main.cpp | 17 +++++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index c2872804d0b..9685611ec3d 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -855,6 +855,7 @@ class goto_symext /// Total symex steps and timestamp for periodic progress reporting. std::size_t total_symex_steps = 0; + std::size_t last_equation_size = 0; std::chrono::steady_clock::time_point last_progress_report = std::chrono::steady_clock::now(); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 7c453e7d01d..3a45f1e2219 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -623,6 +623,23 @@ void goto_symext::symex_step( } execute_next_instruction(get_goto_function, state); + + // Track formula growth — warn when a single instruction adds many SSA steps + { + const std::size_t new_size = target.SSA_steps.size(); + const std::size_t growth = new_size - last_equation_size; + if(growth > 100) + { + const auto &loc = state.source.pc->source_location(); + log.statistics() << "Large SSA growth: +" << growth << " steps at " + << id2string(state.source.function_id); + if(!loc.get_file().empty()) + log.statistics() << " (" << id2string(loc.get_file()) << ":" + << id2string(loc.get_line()) << ")"; + log.statistics() << ", total " << new_size << messaget::eom; + } + last_equation_size = new_size; + } kill_instruction_local_symbols(state); } From 7bc26ff644306a2702ab83e656f419e64992c0d6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Mar 2026 23:02:40 +0000 Subject: [PATCH 4/4] Add --show-symex-progress for live call stack and loop display Add an interactive terminal display that shows the current call stack and loop nesting during symbolic execution. Enabled with the --show-symex-progress flag, it redraws the terminal every 2 seconds to show: - A header with total steps, SSA equation size, and memory usage - The full call stack with indentation showing nesting depth - The current function highlighted in orange - Active loop unwindings with iteration counts shown in cyan Example display (redrawn in place on a terminal): Symex: 50000 steps, SSA 42000, 512 MB __CPROVER__start main process_buffer [process_buffer.0 iter 15] verify_hash [verify_hash.0 iter 3] When output is not a terminal (CI, pipes), the interactive display is disabled and the existing one-line periodic progress is used. At the end of symex, max call depth and loop nesting are reported (testable in CI via --verbosity 9). Also clears the interactive display before printing final statistics, and adds man page entries for --show-symex-progress and --symex-callgrind. Co-authored-by: Kiro --- doc/man/cbmc.1 | 18 +++++ .../cbmc/resource_monitoring/progress.desc | 12 +++ src/cbmc/cbmc_parse_options.cpp | 5 ++ src/cbmc/cbmc_parse_options.h | 1 + .../multi_path_symex_only_checker.cpp | 20 +++++ src/goto-symex/goto_symex.h | 13 +++ src/goto-symex/symex_main.cpp | 80 +++++++++++++++++-- 7 files changed, 144 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc/resource_monitoring/progress.desc diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 0e454caf4c1..4f587608d65 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -620,6 +620,24 @@ verbosity level \fB\-\-timestamp\fR [\fBmonotonic\fR|\fBwall\fR] Print microsecond\-precision timestamps. \fBmonotonic\fR: stamps increase monotonically. \fBwall\fR: ISO\-8601 wall clock timestamps. +.TP +\fB\-\-symex\-callgrind\fR \fIfile\fR +Write per\-source\-location symbolic execution step counts in callgrind +format to \fIfile\fR. The output can be visualized with +.BR kcachegrind (1) +or +.BR qcachegrind (1) +to identify expensive code paths. +.TP +\fB\-\-show\-symex\-progress\fR +Show a live display of the call stack and loop nesting during symbolic +execution. When output is a terminal, the display is redrawn in place +every 2 seconds showing the current call stack with indentation, the +active function highlighted, and loop iteration counts. When output is +not a terminal, a one\-line progress summary is printed periodically +instead. At the end of symbolic execution, the maximum call depth and +loop nesting observed are reported. Per\-function step counts and peak +memory usage are always reported at verbosity level 9 (statistics). .SH ENVIRONMENT All tools honor the TMPDIR environment variable when generating temporary files and directories. Furthermore note that diff --git a/regression/cbmc/resource_monitoring/progress.desc b/regression/cbmc/resource_monitoring/progress.desc new file mode 100644 index 00000000000..50c3ac99093 --- /dev/null +++ b/regression/cbmc/resource_monitoring/progress.desc @@ -0,0 +1,12 @@ +CORE +main.c +--unwind 7 --show-symex-progress --verbosity 9 +^Max call depth: [1-9]\d*, max active loops: \d+$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Tests that --show-symex-progress reports max call depth and loop nesting. +The interactive terminal display is not tested here (requires a real +terminal), but the summary statistics are always emitted. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c0888d4d9b1..cc8ca161ba1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -457,6 +457,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("symex-callgrind", cmdline.get_value("symex-callgrind")); } + if(cmdline.isset("show-symex-progress")) + options.set_option("show-symex-progress", true); + if(cmdline.isset("validate-ssa-equation")) { options.set_option("validate-ssa-equation", true); @@ -1030,6 +1033,8 @@ void cbmc_parse_optionst::help() " report in {uf}\n" " {y--symex-callgrind} {uf} \t write symex step profile in callgrind" " format to {uf} (view with kcachegrind)\n" + " {y--show-symex-progress} \t show live call stack and loop nesting during" + " symbolic execution (terminal only)\n" " {y--property} {uid} \t only check one specific property\n" " {y--trace} \t give a counterexample trace for failed properties\n" " {y--stop-on-fail} \t stop analysis once a failed property is detected" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 6f33b374df6..8a07f765ee8 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -63,6 +63,7 @@ class optionst; OPT_COVER \ "(symex-coverage-report):" \ "(symex-callgrind):" \ + "(show-symex-progress)" \ "(mm):" \ OPT_TIMESTAMP \ "(arrays-uf-always)(arrays-uf-never)" \ diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index fe3245af4b5..ca2d6499d9f 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "multi_path_symex_only_checker.h" +#include #include #include @@ -99,9 +100,21 @@ void multi_path_symex_only_checkert::generate_equation() const auto symex_start = std::chrono::steady_clock::now(); + symex.interactive_display_enabled = + options.get_bool_option("show-symex-progress"); + symex_symbol_table = symex.symex_from_entry_point_of( goto_symext::get_goto_function(goto_model), fields); + // Clear interactive display before printing final stats + if(symex.interactive_display_enabled && consolet::is_terminal()) + { + auto &out = consolet::out(); + for(std::size_t i = 0; i < symex.interactive_display_lines; ++i) + out << consolet::cursorup << consolet::cleareol; + symex.interactive_display_lines = 0; + } + const auto symex_stop = std::chrono::steady_clock::now(); std::chrono::duration symex_runtime = std::chrono::duration(symex_stop - symex_start); @@ -126,6 +139,13 @@ void multi_path_symex_only_checkert::generate_equation() log.statistics() << "Symex steps: " << total << " total" << messaget::eom; + if(symex.interactive_display_enabled) + { + log.statistics() << "Max call depth: " << symex.max_call_depth_seen + << ", max active loops: " << symex.max_active_loops_seen + << messaget::eom; + } + const std::size_t max_entries = 10; for(std::size_t i = 0; i < std::min(max_entries, sorted.size()); ++i) { diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 9685611ec3d..fe23e631356 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -859,6 +859,19 @@ class goto_symext std::chrono::steady_clock::time_point last_progress_report = std::chrono::steady_clock::now(); +public: + /// When true, show live call stack and loop nesting on the terminal. + /// Enabled by --show-symex-progress. + bool interactive_display_enabled = false; + + /// Maximum call stack depth and loop nesting observed during symex. + std::size_t max_call_depth_seen = 0; + std::size_t max_active_loops_seen = 0; + + /// Number of lines drawn by the last interactive display, for redrawing. + std::size_t interactive_display_lines = 0; + +protected: complexity_limitert complexity_module; /// Shadow memory instrumentation API diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 3a45f1e2219..015d1724310 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution +#include #include #include #include @@ -611,15 +612,84 @@ void goto_symext::symex_step( // Periodic progress reporting (every 2 seconds) ++total_symex_steps; + + // Track max call depth and loop nesting + if(interactive_display_enabled) + { + const auto depth = state.call_stack().size(); + if(depth > max_call_depth_seen) + max_call_depth_seen = depth; + + std::size_t active_loops = 0; + for(const auto &frame : state.call_stack()) + for(const auto &loop : frame.loop_iterations) + if(loop.second.count > 0) + ++active_loops; + if(active_loops > max_active_loops_seen) + max_active_loops_seen = active_loops; + } + const auto now = std::chrono::steady_clock::now(); if(std::chrono::duration(now - last_progress_report).count() >= 2.0) { last_progress_report = now; - log.statistics() << "Symex: " << total_symex_steps << " steps, in " - << id2string(state.source.function_id) << ", SSA size " - << target.SSA_steps.size() << ", peak memory " - << peak_memory_bytes() / (1024 * 1024) << " MB" - << messaget::eom; + + if(interactive_display_enabled && consolet::is_terminal()) + { + // Erase previous display + auto &out = consolet::out(); + for(std::size_t i = 0; i < interactive_display_lines; ++i) + out << consolet::cursorup << consolet::cleareol; + + std::size_t lines = 0; + + // Header line + out << consolet::bold << "Symex: " << consolet::reset << total_symex_steps + << " steps, SSA " << target.SSA_steps.size() << ", " + << peak_memory_bytes() / (1024 * 1024) << " MB\n"; + ++lines; + + // Call stack + const auto &stack = state.call_stack(); + for(std::size_t i = 0; i < stack.size(); ++i) + { + const auto &frame = stack[i]; + const auto &fn = frame.function_identifier; + if(fn.empty()) + continue; + + out << std::string(2 * i, ' '); + if(i + 1 == stack.size()) + out << consolet::orange; + out << id2string(fn); + + // Show active loops in this frame + for(const auto &loop : frame.loop_iterations) + { + if(loop.second.count > 0) + { + out << consolet::cyan << " [" << id2string(loop.first) << " iter " + << loop.second.count << "]" << consolet::reset; + } + } + + if(i + 1 == stack.size()) + out << consolet::reset; + out << '\n'; + ++lines; + } + + interactive_display_lines = lines; + out << std::flush; + } + else + { + log.statistics() << "Symex: " << total_symex_steps << " steps, in " + << id2string(state.source.function_id) << ", SSA size " + << target.SSA_steps.size() << ", peak memory " + << peak_memory_bytes() / (1024 * 1024) << " MB" + << messaget::eom; + } } execute_next_instruction(get_goto_function, state);