Symex resource monitoring: per-function step counts, memory, callgrind output, and live progress display

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

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.

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

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.

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.

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,18 @@ 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("show-symex-progress"))
+    options.set_option("show-symex-progress", true);
+
   if(cmdline.isset("validate-ssa-equation"))
   {
     options.set_option("validate-ssa-equation", true);
@@ -508,8 +516,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 +577,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 +588,9 @@ int cbmc_parse_optionst::doit()
       return CPROVER_EXIT_INCORRECT_TASK;
     }
 
-    std::unique_ptr<languaget> language=
-      get_language_from_filename(filename);
+    std::unique_ptr<languaget> 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 +614,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 +1031,10 @@ 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--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"

src/cbmc/cbmc_parse_options.h

@@ -62,6 +62,8 @@ class optionst;
   "(export-symex-ready-goto):" \
   OPT_COVER \
   "(symex-coverage-report):" \
+  "(symex-callgrind):" \
+  "(show-symex-progress)" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(arrays-uf-always)(arrays-uf-never)" \

src/goto-checker/bmc_util.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include "bmc_util.h"
 
 #include <util/json_stream.h>
+#include <util/memory_info.h>
 #include <util/ui_message.h>
 
 #include <goto-programs/graphml_witness.h>
@@ -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<double>(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)
   {

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 <fstream>
+
 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.

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "multi_path_symex_only_checker.h"
 
+#include <util/console.h>
+#include <util/memory_info.h>
 #include <util/ui_message.h>
 
 #include <goto-symex/shadow_memory.h>
@@ -19,6 +21,9 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "bmc_util.h"
 
+#include <algorithm>
+#include <fstream>
+
 multi_path_symex_only_checkert::multi_path_symex_only_checkert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
@@ -41,8 +46,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();
 
@@ -52,6 +57,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;
+      }
+    }
+  }
+
   if(options.get_bool_option("show-vcc"))
   {
     show_vcc(options, ui_message_handler, equation);
@@ -80,15 +100,65 @@ 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<double> symex_runtime =
     std::chrono::duration<double>(symex_stop - symex_start);
   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<std::pair<irep_idt, std::size_t>> 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;
+
+    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)
+    {
+      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);
 }