Merge pull request #4592 from JohnDumbell/jd/enhancement/symex_step_debug

Add symex debugging print-out

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -113,6 +113,7 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
+  options.set_option("show-goto-symex-steps", false);
 
   // Other default
   options.set_option("arrays-uf", "auto");
@@ -415,6 +416,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   // code.
   if(cmdline.isset("java-threading"))
     options.set_option("allow-pointer-unsoundness", true);
+
+  if(cmdline.isset("show-goto-symex-steps"))
+    options.set_option("show-goto-symex-steps", true);
 }
 
 /// invoke main modules

src/cbmc/cbmc_parse_options.cpp

@@ -118,6 +118,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
+  options.set_option("show-goto-symex-steps", false);
 
   // Other default
   options.set_option("arrays-uf", "auto");
@@ -442,6 +443,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("validate-goto-model", true);
   }
 
+  if(cmdline.isset("show-goto-symex-steps"))
+    options.set_option("show-goto-symex-steps", true);
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 

src/goto-checker/bmc_util.h

@@ -175,6 +175,7 @@ void run_property_decider(
   "(program-only)" \
   "(show-loops)" \
   "(show-vcc)" \
+  "(show-goto-symex-steps)" \
   "(slice-formula)" \
   "(unwinding-assertions)" \
   "(no-unwinding-assertions)" \
@@ -192,6 +193,8 @@ void run_property_decider(
 #define HELP_BMC \
   " --paths [strategy]           explore paths one at a time\n" \
   " --show-symex-strategies      list strategies for use with --paths\n" \
+  " --show-goto-symex-steps      show which steps symex travels, includes " \
+  "                              diagnostic information\n" \
   " --program-only               only show program expression\n" \
   " --show-loops                 show the loops in the program\n" \
   " --depth nr                   limit search depth\n" \

src/goto-symex/goto_symex.h

@@ -64,6 +64,10 @@ struct symex_configt final
   /// executed in the goto_symex_statet (in the assignment method).
   bool run_validation_checks;
 
+  /// \brief Prints out the path that symex is actively taking during execution,
+  /// includes diagnostic information about call stack and guard size.
+  bool show_symex_steps;
+
   /// \brief Construct a symex_configt using options specified in an
   /// \ref optionst
   explicit symex_configt(const optionst &options);
@@ -224,6 +228,13 @@ class goto_symext
   virtual void
   symex_step(const get_goto_functiont &get_goto_function, statet &state);
 
+  /// Prints the route of symex as it walks through the code. Used for
+  /// debugging.
+  void print_symex_step(statet &state);
+
+  messaget::mstreamt &
+  print_callstack_entry(const symex_targett::sourcet &target);
+
 public:
 
   /// language_mode: ID_java, ID_C or another language identifier

src/goto-symex/symex_main.cpp

@@ -26,6 +26,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/string2int.h>
 #include <util/symbol_table.h>
 
+#include <util/format.h>
+#include <util/format_expr.h>
+#include <util/format_type.h>
+#include <util/std_types.h>
+
 symex_configt::symex_configt(const optionst &options)
   : max_depth(options.get_unsigned_int_option("depth")),
     doing_path_exploration(options.is_set("paths")),
@@ -38,7 +43,8 @@ symex_configt::symex_configt(const optionst &options)
     unwinding_assertions(options.get_bool_option("unwinding-assertions")),
     partial_loops(options.get_bool_option("partial-loops")),
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
-    run_validation_checks(options.get_bool_option("validate-ssa-equation"))
+    run_validation_checks(options.get_bool_option("validate-ssa-equation")),
+    show_symex_steps(options.get_bool_option("show-goto-symex-steps"))
 {
 }
 
@@ -409,17 +415,103 @@ goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
   };
 }
 
+messaget::mstreamt &
+goto_symext::print_callstack_entry(const symex_targett::sourcet &source)
+{
+  log.status() << source.function_id
+               << " location number: " << source.pc->location_number;
+
+  return log.status();
+}
+
+void goto_symext::print_symex_step(statet &state)
+{
+  // If we're showing the route, begin outputting debug info, and don't print
+  // instructions we don't run.
+
+  // We also skip dead instructions as they don't add much to step-based
+  // debugging and if there's no code block at this point.
+  if(
+    !symex_config.show_symex_steps || state.guard.is_false() ||
+    state.source.pc->type == DEAD ||
+    (state.source.pc->code.is_nil() && state.source.pc->type != END_FUNCTION))
+  {
+    return;
+  }
+
+  if(state.source.pc->code.is_not_nil())
+  {
+    auto guard_expression = state.guard.as_expr();
+    std::size_t size = 0;
+    for(auto it = guard_expression.depth_begin();
+        it != guard_expression.depth_end();
+        ++it)
+    {
+      size++;
+    }
+
+    log.status() << "[Guard size: " << size << "] "
+                 << format(state.source.pc->code);
+
+    if(
+      state.source.pc->source_location.is_not_nil() &&
+      !state.source.pc->source_location.get_java_bytecode_index().empty())
+    {
+      log.status()
+        << " bytecode index: "
+        << state.source.pc->source_location.get_java_bytecode_index();
+    }
+
+    log.status() << messaget::eom;
+  }
+
+  // Print the method we're returning too.
+  const auto &call_stack = state.threads[state.source.thread_nr].call_stack;
+  if(state.source.pc->type == END_FUNCTION)
+  {
+    log.status() << messaget::eom;
+
+    if(!call_stack.empty())
+    {
+      log.status() << "Returning to: ";
+      print_callstack_entry(call_stack.back().calling_location)
+        << messaget::eom;
+    }
+
+    log.status() << messaget::eom;
+  }
+
+  // On a function call print the entire call stack.
+  if(state.source.pc->type == FUNCTION_CALL)
+  {
+    log.status() << messaget::eom;
+
+    if(!call_stack.empty())
+    {
+      log.status() << "Call stack:" << messaget::eom;
+
+      for(auto &frame : call_stack)
+      {
+        print_callstack_entry(frame.calling_location) << messaget::eom;
+      }
+
+      print_callstack_entry(state.source) << messaget::eom;
+
+      // Add the method we're about to enter with no location number.
+      log.status() << format(
+                        to_code_function_call(state.source.pc->code).function())
+                   << messaget::eom << messaget::eom;
+    }
+  }
+}
+
 /// do just one step
 void goto_symext::symex_step(
   const get_goto_functiont &get_goto_function,
   statet &state)
 {
-  #if 0
-  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
-  std::cout << "Location: " << state.source.pc->source_location << '\n';
-  std::cout << "Guard: " << format(state.guard.as_expr()) << '\n';
-  std::cout << "Code: " << format(state.source.pc->code) << '\n';
-  #endif
+  // Print debug statements if they've been enabled.
+  print_symex_step(state);
 
   PRECONDITION(!state.threads.empty());
   PRECONDITION(!state.call_stack().empty());

src/util/format_expr.cpp

@@ -324,6 +324,31 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
         os << ' ' << format(s);
       return os << " }";
     }
+    else if(statement == ID_dead)
+    {
+      return os << "dead " << format(to_code_dead(code).symbol()) << ";";
+    }
+    else if(statement == ID_decl)
+    {
+      const auto &declaration_symb = to_code_decl(code).symbol();
+      return os << "decl " << format(declaration_symb.type()) << " "
+                << format(declaration_symb) << ";";
+    }
+    else if(statement == ID_function_call)
+    {
+      const auto &func_call = to_code_function_call(code);
+      os << to_symbol_expr(func_call.function()).get_identifier() << "(";
+
+      // Join all our arguments together.
+      join_strings(
+        os,
+        func_call.arguments().begin(),
+        func_call.arguments().end(),
+        ", ",
+        [](const exprt &expr) { return format(expr); });
+
+      return os << ");";
+    }
     else
       return fallback_format_rec(os, expr);
   }