DRAFT: Control Flow Retrace feature

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

regression/book-examples/simple-goto/C00.desc

@@ -0,0 +1,6 @@
+CORE
+simple_goto.c
+--function foo --retrace 00
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/book-examples/simple-goto/C01.desc

@@ -0,0 +1,6 @@
+CORE
+simple_goto.c
+--function foo --retrace 01
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/book-examples/simple-goto/C10.desc

@@ -0,0 +1,6 @@
+CORE
+simple_goto.c
+--function foo --retrace 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/book-examples/simple-goto/simple_goto.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdbool.h>
+
+void foo(bool arg1, bool arg2)
+{
+  bool v1 = false;
+  bool v2 = false;
+  if(arg1)
+    goto l1;
+  v1 = true;
+l1:
+  if(arg2)
+    goto l2;
+  v2 = true;
+l2:
+  assert(v1);
+  assert(v2);
+}

src/cbmc/cbmc_parse_options.cpp

@@ -168,6 +168,21 @@
     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 @@
   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,194 @@
   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;
+    should_pause_symex = true;
+  }
+  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;
+    should_pause_symex = true;
+  }
+
+  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")),
@@ -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")}
@@ -641,7 +641,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);