Feature to --retrace a single control flow path

Adds a feature to retrace and verify a single control flow path. The path
can be given using `--retrace` as a string of 0s and 1s. From a very brief
evaluation test, it seems to be faster than bounded loop unwinding. Only
that it might be challenging to find a path to retrace. The 0s and 1s in
the input retrace string follow the goto decisions in cbmc's internal goto
program representation. During symbolic execution, files and line numbers
for each decision are logged to the console, so the interactive use should
be intuitive.

Co-authored-by: Yosephine Setiawan <[email protected]>

Author: lks9

doc/man/cbmc.1

@@ -366,6 +366,9 @@ explore paths one at a time
 \fB\-\-show\-symex\-strategies\fR
 list strategies for use with \fB\-\-paths\fR
 .TP
+\fB\-\-retrace\fR [trace]
+follow a single control flow path, given by a trace string of 0s and 1s
+.TP
 \fB\-\-show\-goto\-symex\-steps\fR
 show which steps symex travels, includes
 diagnostic information

doc/man/jbmc.1

@@ -281,6 +281,9 @@ explore paths one at a time
 \fB\-\-show\-symex\-strategies\fR
 list strategies for use with \fB\-\-paths\fR
 .TP
+\fB\-\-retrace\fR [trace]
+follow a single control flow path, given by a trace string of 0s and 1s
+.TP
 \fB\-\-show\-goto\-symex\-steps\fR
 show which steps symex travels, includes
 diagnostic information

src/cbmc/cbmc_parse_options.cpp

@@ -168,6 +168,21 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("retrace"))
+  {
+    auto retrace_input = cmdline.get_value("retrace");
+    options.set_option("retrace", retrace_input);
+
+    // check retrace input
+    for(auto &c : retrace_input)
+      if(c != '0' && c != '1')
+      {
+        log.error() << "--retrace input string must only contain 0s and 1s"
+                    << messaget::eom;
+        exit(CPROVER_EXIT_USAGE_ERROR);
+      }
+  }
+
   // We want to warn the user that if we are using standard checks (that enables
   // unwinding-assertions) and we did not disable them manually.
   if(

src/goto-checker/bmc_util.cpp

@@ -186,7 +186,14 @@ void setup_symex(
   if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
     symex.language_mode = init_symbol->mode;
 
-  msg.status() << "Starting Bounded Model Checking" << messaget::eom;
+  if(options.is_set("retrace"))
+  {
+    msg.status() << "Starting Retrace Model Checking" << messaget::eom;
+  }
+  else
+  {
+    msg.status() << "Starting Bounded Model Checking" << messaget::eom;
+  }
 
   symex.last_source_location.make_nil();
 

src/goto-checker/bmc_util.h

@@ -182,6 +182,7 @@ void run_property_decider(
   "(partial-loops)"                                                            \
   "(paths):"                                                                   \
   "(show-symex-strategies)"                                                    \
+  "(retrace):"                                                                 \
   "(depth):"                                                                   \
   "(max-field-sensitivity-array-size):"                                        \
   "(no-array-field-sensitivity)"                                               \
@@ -197,6 +198,8 @@ void run_property_decider(
 #define HELP_BMC                                                               \
   " {y--paths} [strategy] \t explore paths one at a time\n"                    \
   " {y--show-symex-strategies} \t list strategies for use with {y--paths}\n"   \
+  " {y--retrace} [trace] \t follow a single control flow path, given by a "    \
+  "trace string of 0s and 1s\n"                                                \
   " {y--show-goto-symex-steps} \t show which steps symex travels, includes "   \
   "diagnostic information\n"                                                   \
   " {y--show-points-to-sets} \t show points-to sets for pointer dereference. " \

src/goto-symex/goto_symex.h

@@ -318,6 +318,9 @@ class goto_symext
   /// Symbolically execute a GOTO instruction in the context of unreachable code
   /// \param state: Symbolic execution state for current instruction
   void symex_unreachable_goto(statet &state);
+  /// Symbolically execute a GOTO along a control flow retrace input path
+  /// \param state: Symbolic execution state for current instruction
+  void symex_goto_retrace(statet &state);
   /// Symbolically execute a SET_RETURN_VALUE instruction
   /// \param state: Symbolic execution state for current instruction
   /// \param return_value: The value to be returned

src/goto-symex/symex_config.h

@@ -24,6 +24,9 @@ struct symex_configt final
 
   bool doing_path_exploration;
 
+  bool retracing;
+  std::string retrace_input;
+
   bool allow_pointer_unsoundness;
 
   bool constant_propagation;

src/goto-symex/symex_goto.cpp

@@ -260,8 +260,7 @@ void goto_symext::symex_goto(statet &state)
   DATA_INVARIANT(
     instruction.targets.size() == 1, "no support for non-deterministic gotos");
 
-  goto_programt::const_targett goto_target=
-    instruction.get_target();
+  goto_programt::const_targett goto_target = instruction.get_target();
 
   const bool backward = instruction.is_backwards_goto();
 
@@ -614,6 +613,197 @@ void goto_symext::symex_unreachable_goto(statet &state)
   symex_transition(state);
 }
 
+void goto_symext::symex_goto_retrace(statet &state)
+{
+  // get guard, targets as in symex_goto()
+  const goto_programt::instructiont &instruction = *state.source.pc;
+
+  exprt new_guard = clean_expr(instruction.condition(), state, false);
+
+  renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
+  renamed_guard = try_evaluate_pointer_comparisons(
+    std::move(renamed_guard), state.value_set, language_mode, ns);
+  if(symex_config.simplify_opt)
+    renamed_guard.simplify(ns);
+  new_guard = renamed_guard.get();
+
+  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
+
+  DATA_INVARIANT(
+    !instruction.targets.empty(), "goto should have at least one target");
+
+  // we only do deterministic gotos for now
+  DATA_INVARIANT(
+    instruction.targets.size() == 1, "no support for non-deterministic gotos");
+
+  goto_programt::const_targett goto_target = instruction.get_target();
+
+  const bool backward = instruction.is_backwards_goto();
+
+  goto_programt::const_targett next_instruction = state.source.pc;
+  next_instruction++;
+
+  // goto or next depends on input trace from user
+  bool choose_goto;
+  static size_t retrace_index = 0;
+  if(retrace_index < symex_config.retrace_input.size())
+  {
+    choose_goto = symex_config.retrace_input[retrace_index] == '1';
+  }
+  else
+  {
+    choose_goto = false;
+  }
+  retrace_index++;
+
+  // print goto choice
+  log.conditional_output(
+    log.status(),
+    [this, &state, &goto_target, &next_instruction, choose_goto](
+      messaget::mstreamt &mstream)
+    {
+      source_locationt cur = state.source.pc->source_location();
+      source_locationt goto_dest = goto_target->source_location();
+      source_locationt next_dest = next_instruction->source_location();
+      source_locationt t_dest = choose_goto ? goto_dest : next_dest;
+      source_locationt nt_dest = choose_goto ? next_dest : goto_dest;
+
+      auto cur_file = cur.get_file();
+      if(cur_file.empty())
+        cur_file = "<unknown>";
+      auto t_file = t_dest.get_file();
+      if(t_file.empty())
+        t_file = "<unknown>";
+      auto nt_file = nt_dest.get_file();
+      if(nt_file.empty())
+        nt_file = "<unknown>";
+
+      // print nothing when files are the same
+      if(cur_file == t_file)
+        t_file = "";
+      if(cur_file == nt_file)
+        nt_file = "";
+
+      auto cur_line = cur.get_line();
+      if(cur_line.empty())
+        cur_line = "?";
+      auto t_line = t_dest.get_line();
+      if(t_line.empty())
+        t_line = "?";
+      auto nt_line = nt_dest.get_line();
+      if(nt_line.empty())
+        nt_line = "?";
+
+      std::string head = symex_config.retrace_input;
+      // add 0s in case input trace was shorter
+      head.resize(retrace_index - 1, '0');
+      std::string decision = choose_goto ? "1" : "0";
+
+      std::string step = choose_goto ? " goto " : " next ";
+
+      std::string padding_1 =
+        cur_line.size() < 3 ? std::string(3 - cur_line.size(), ' ') : "";
+      std::string padding_2 =
+        t_line.size() < 3 ? std::string(3 - t_line.size(), ' ') : "";
+
+      mstream << "Retrace "
+              << head << messaget::bold << decision << messaget::reset
+              << " at " << cur_file << ":" << cur_line << padding_1
+              << step << t_file << ":" << t_line << padding_2
+              << " (not " << nt_file << ":" << nt_line << ")"
+              << messaget::eom;
+    });
+
+  // warn when not following unconditional goto
+  if(new_guard.is_true() && !choose_goto)
+  {
+    log.result() << "Retrace input "
+                 << messaget::red << "inconsistent" << messaget::reset
+                 << ": 0/next although guard is true!"
+                 << log.eom;
+  }
+  else if(new_guard.is_false() && choose_goto)
+  {
+    log.result() << "Retrace input "
+                 << messaget::red << "inconsistent" << messaget::reset
+                 << ": 1/goto although guard is false!"
+                 << log.eom;
+  }
+
+  symex_targett::sourcet original_source = state.source;
+  goto_programt::const_targett new_state_pc;
+
+  if(choose_goto)
+  {
+    // Jump to the jump target if the input is '1'
+    new_state_pc = goto_target;
+    symex_transition(state, new_state_pc, backward);
+  }
+  else
+  {
+    // Jump to the next instruction
+    new_state_pc = state.source.pc;
+    new_state_pc++;
+    symex_transition(state);
+  }
+
+  // produce new guard symbol
+  exprt guard_expr;
+
+  if(
+    new_guard.id() == ID_symbol ||
+    (new_guard.id() == ID_not && to_not_expr(new_guard).op().id() == ID_symbol))
+  {
+    guard_expr = new_guard;
+  }
+  else
+  {
+    symbol_exprt guard_symbol_expr =
+      symbol_exprt(statet::guard_identifier(), bool_typet());
+    exprt new_rhs = boolean_negate(new_guard);
+
+    ssa_exprt new_lhs =
+      state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
+    new_lhs =
+      state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
+
+    guardt guard{true_exprt{}, guard_manager};
+
+    log.conditional_output(
+      log.debug(),
+      [this, &new_lhs](messaget::mstreamt &mstream)
+      {
+        mstream << "Assignment to " << new_lhs.get_identifier()
+                << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0)
+                << " bits]"
+                << messaget::eom;
+      });
+
+    target.assignment(
+      guard.as_expr(),
+      new_lhs,
+      new_lhs,
+      guard_symbol_expr,
+      new_rhs,
+      original_source,
+      symex_targett::assignment_typet::GUARD);
+
+    guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
+  }
+
+  if(choose_goto)
+  {
+    symex_assume_l2(state, guard_expr);
+    state.guard.add(guard_expr);
+  }
+  else
+  {
+    symex_assume_l2(state, boolean_negate(guard_expr));
+    state.guard.add(boolean_negate(guard_expr));
+  }
+  return;
+}
+
 bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
 {
   // dummy implementation

src/goto-symex/symex_main.cpp

@@ -30,6 +30,8 @@ Author: Daniel Kroening, [email protected]
 symex_configt::symex_configt(const optionst &options)
   : max_depth(options.get_unsigned_int_option("depth")),
     doing_path_exploration(options.is_set("paths")),
+    retracing(options.is_set("retrace")),
+    retrace_input(options.get_option("retrace")),
     allow_pointer_unsoundness(
       options.get_bool_option("allow-pointer-unsoundness")),
     constant_propagation(options.get_bool_option("propagation")),
@@ -641,7 +643,9 @@ void goto_symext::execute_next_instruction(
     break;
 
   case GOTO:
-    if(state.reachable)
+    if(symex_config.retracing)
+      symex_goto_retrace(state);
+    else if(state.reachable)
       symex_goto(state);
     else
       symex_unreachable_goto(state);