Path exploration pushes both successors onto queue

When doing path exploration and encountering a conditional goto
instruction, both successors of the goto (the next instruction, and the
target) are pushed onto the path exploration workqueue. This allows the
symbolic execution caller to have complete control over which path to
execute next.

Prior to this commit, symex would push one successor onto the workqueue
and continue executing the path of the other successor until the path
was terminated. This commit introduces the possibility that symbolic
execution pauses without reaching the end of a path, and needs to be
resumed by the caller. Thus, new safety checker results are introduced
(SUSPENDED and UNKNOWN); the former signals to the caller of symex that
symex has not reached the end of a branch, and therefore no safety check
has been performed.

The (currently only) path exploration strategy still pops paths in the
order that they were pushed. This behaviour means that the paths that it
pops will always alternate between the next instruction of a goto, and
the target of that same goto. The test suite is updated to reflect this
strategy.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -342,6 +342,9 @@ safety_checkert::resultt bmct::execute(
     const goto_functionst &goto_functions =
       goto_model.get_goto_functions();
 
+    if(symex.should_pause_symex)
+      return safety_checkert::resultt::PAUSED;
+
     // This provides the driver program the opportunity to do things like a
     // symbol-table or goto-functions dump instead of actually running the
     // checker, like show-vcc except driver-program specific.
@@ -602,9 +605,10 @@ int bmct::do_language_agnostic_bmc(
   std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
   std::function<bool(void)> callback_after_symex)
 {
+  safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
+  safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
   const symbol_tablet &symbol_table = model.get_symbol_table();
   message_handlert &mh = message.get_message_handler();
-  safety_checkert::resultt result;
   std::unique_ptr<path_storaget> worklist =
     path_storaget::make(path_storaget::disciplinet::FIFO);
   try
@@ -619,7 +623,9 @@ int bmct::do_language_agnostic_bmc(
       bmc.set_ui(ui);
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
-      result = bmc.run(model);
+      tmp_result = bmc.run(model);
+      if(tmp_result != safety_checkert::resultt::PAUSED)
+        final_result = tmp_result;
     }
     INVARIANT(
       opts.get_bool_option("paths") || worklist->empty(),
@@ -628,8 +634,8 @@ int bmct::do_language_agnostic_bmc(
         std::to_string(worklist->size()) + " unexplored branches.");
 
     // When model checking, the bmc.run() above will already have explored
-    // the entire program, and result contains the verification result. The
-    // worklist (containing paths that have not yet been explored) is thus
+    // the entire program, and final_result contains the verification result.
+    // The worklist (containing paths that have not yet been explored) is thus
     // empty, and we don't enter this loop.
     //
     // When doing path exploration, there will be some saved paths left to
@@ -644,10 +650,11 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      message.status() << "___________________________\n"
-                       << "Starting new path (" << worklist->size()
-                       << " to go)\n"
-                       << message.eom;
+      if(tmp_result != safety_checkert::resultt::PAUSED)
+        message.status() << "___________________________\n"
+                         << "Starting new path (" << worklist->size()
+                         << " to go)\n"
+                         << message.eom;
       cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
       solvers.set_ui(ui);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
@@ -665,7 +672,9 @@ int bmct::do_language_agnostic_bmc(
         callback_after_symex);
       if(driver_configure_bmc)
         driver_configure_bmc(pe, symbol_table);
-      result &= pe.run(model);
+      tmp_result = pe.run(model);
+      if(tmp_result != safety_checkert::resultt::PAUSED)
+        final_result &= tmp_result;
       worklist->pop();
     }
   }
@@ -685,14 +694,18 @@ int bmct::do_language_agnostic_bmc(
     throw std::current_exception();
   }
 
-  switch(result)
+  switch(final_result)
   {
   case safety_checkert::resultt::SAFE:
     return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
     return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
     return CPROVER_EXIT_INTERNAL_ERROR;
+  case safety_checkert::resultt::UNKNOWN:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  case safety_checkert::resultt::PAUSED:
+    UNREACHABLE;
   }
   UNREACHABLE;
 }

src/goto-programs/safety_checker.h

@@ -30,7 +30,23 @@ class safety_checkert:public messaget
     const namespacet &_ns,
     message_handlert &_message_handler);
 
-  enum class resultt { SAFE, UNSAFE, ERROR };
+  enum class resultt
+  {
+    /// No safety properties were violated
+    SAFE,
+    /// Some safety properties were violated
+    UNSAFE,
+    /// Safety is unknown due to an error during safety checking
+    ERROR,
+    /// Symbolic execution has been suspended due to encountering a GOTO while
+    /// doing path exploration; the symex state has been saved, and symex should
+    /// be resumed by the caller.
+    PAUSED,
+    /// We haven't yet assigned a safety check result to this object. A value of
+    /// UNKNOWN can be used to initialize a resultt object, and that object may
+    /// then safely be used with the |= and &= operators.
+    UNKNOWN
+  };
 
   // check whether all assertions in goto_functions are safe
   // if UNSAFE, then a trace is returned
@@ -47,11 +63,22 @@ class safety_checkert:public messaget
 };
 
 /// \brief The worst of two results
+///
+/// A result of PAUSED means that the safety check has not yet completed,
+/// thus it makes no sense to compare it to the result of a completed safety
+/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an
+/// argument to this function.
 inline safety_checkert::resultt &
 operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
 {
+  PRECONDITION(
+    a != safety_checkert::resultt::PAUSED &&
+    b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
+  case safety_checkert::resultt::UNKNOWN:
+    a = b;
+    return a;
   case safety_checkert::resultt::ERROR:
     return a;
   case safety_checkert::resultt::SAFE:
@@ -60,16 +87,29 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
   case safety_checkert::resultt::UNSAFE:
     a = b == safety_checkert::resultt::ERROR ? b : a;
     return a;
+  case safety_checkert::resultt::PAUSED:
+    UNREACHABLE;
   }
   UNREACHABLE;
 }
 
 /// \brief The best of two results
+///
+/// A result of PAUSED means that the safety check has not yet completed,
+/// thus it makes no sense to compare it to the result of a completed safety
+/// check. Therefore do not pass safety_checkert::resultt:PAUSED as an
+/// argument to this function.
 inline safety_checkert::resultt &
 operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
 {
+  PRECONDITION(
+    a != safety_checkert::resultt::PAUSED &&
+    b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
+  case safety_checkert::resultt::UNKNOWN:
+    a = b;
+    return a;
   case safety_checkert::resultt::SAFE:
     return a;
   case safety_checkert::resultt::ERROR:
@@ -78,6 +118,8 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
   case safety_checkert::resultt::UNSAFE:
     a = b == safety_checkert::resultt::SAFE ? b : a;
     return a;
+  case safety_checkert::resultt::PAUSED:
+    UNREACHABLE;
   }
   UNREACHABLE;
 }

src/goto-symex/goto_symex.h

@@ -53,7 +53,8 @@ class goto_symext
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
     path_storaget &path_storage)
-    : total_vccs(0),
+    : should_pause_symex(false),
+      total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
       language_mode(),
@@ -159,6 +160,15 @@ class goto_symext
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
+  /// \brief Have states been pushed onto the workqueue?
+  ///
+  /// If this flag is set at the end of a symbolic execution run, it means that
+  /// symex has been paused because we encountered a GOTO instruction while
+  /// doing path exploration, and thus pushed the successor states of the GOTO
+  /// onto path_storage. The symbolic execution caller should now choose which
+  /// successor state to continue executing, and resume symex from that state.
+  bool should_pause_symex;
+
 protected:
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.

src/goto-symex/goto_symex_state.h

@@ -372,7 +372,13 @@ class goto_symex_statet final
   incremental_dirtyt dirty;
 
   goto_programt::const_targett saved_target;
-  bool has_saved_target;
+
+  /// \brief This state is saved, with the PC pointing to the target of a GOTO
+  bool has_saved_jump_target;
+
+  /// \brief This state is saved, with the PC pointing to the next instruction
+  /// of a GOTO
+  bool has_saved_next_instruction;
   bool saved_target_is_backwards;
 
 private:

src/goto-symex/path_storage.cpp

@@ -19,17 +19,20 @@ path_storaget::make(path_storaget::disciplinet discipline)
   UNREACHABLE;
 }
 
-path_storaget::patht &path_fifot::peek()
+path_storaget::patht &path_fifot::private_peek()
 {
   return paths.front();
 }
 
-void path_fifot::push(const path_storaget::patht &bp)
+void path_fifot::push(
+  const path_storaget::patht &next_instruction,
+  const path_storaget::patht &jump_target)
 {
-  paths.push_back(bp);
+  paths.push_back(next_instruction);
+  paths.push_back(jump_target);
 }
 
-void path_fifot::pop()
+void path_fifot::private_pop()
 {
   paths.pop_front();
 }

src/goto-symex/path_storage.h

@@ -48,13 +48,29 @@ class path_storaget
   virtual ~path_storaget() = default;
 
   /// \brief Reference to the next path to resume
-  virtual patht &peek() = 0;
-
-  /// \brief Add a path to resume to the storage
-  virtual void push(const patht &bp) = 0;
+  patht &peek()
+  {
+    PRECONDITION(!empty());
+    return private_peek();
+  }
+
+  /// \brief Add paths to resume to the storage
+  ///
+  /// Symbolic execution is suspended when we reach a conditional goto
+  /// instruction with two successors. Thus, we always add a pair of paths to
+  /// the path storage.
+  ///
+  /// \param next_instruction the instruction following the goto instruction
+  /// \param jump_target the target instruction of the goto instruction
+  virtual void
+  push(const patht &next_instruction, const patht &jump_target) = 0;
 
   /// \brief Remove the next path to resume from the storage
-  virtual void pop() = 0;
+  void pop()
+  {
+    PRECONDITION(!empty());
+    private_pop();
+  }
 
   /// \brief How many paths does this storage contain?
   virtual std::size_t size() const = 0;
@@ -64,19 +80,27 @@ class path_storaget
   {
     return size() == 0;
   };
+
+private:
+  // Derived classes should override these methods, allowing the base class to
+  // enforce preconditions.
+  virtual patht &private_peek() = 0;
+  virtual void private_pop() = 0;
 };
 
 /// \brief FIFO save queue: paths are resumed in the order that they were saved
 class path_fifot : public path_storaget
 {
 public:
-  patht &peek() override;
-  void push(const patht &bp) override;
-  void pop() override;
+  void push(const patht &, const patht &) override;
   std::size_t size() const override;
 
 protected:
   std::list<patht> paths;
+
+private:
+  patht &private_peek() override;
+  void private_pop() override;
 };
 
 #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */

src/goto-symex/symex_goto.cpp

@@ -152,7 +152,7 @@ void goto_symext::symex_goto(statet &state)
   // new_state_pc for later. But if we're executing from a saved state, then
   // new_state_pc should be the state that we saved from earlier, so let's
   // execute that instead.
-  if(state.has_saved_target)
+  if(state.has_saved_jump_target)
   {
     INVARIANT(
       new_state_pc == state.saved_target,
@@ -170,28 +170,45 @@ void goto_symext::symex_goto(statet &state)
     new_state_pc = state_pc;
     state_pc = tmp;
 
-    log.debug() << "Resuming from '" << state_pc->source_location << "'"
-                << log.eom;
+    log.debug() << "Resuming from jump target '" << state_pc->source_location
+                << "'" << log.eom;
+  }
+  else if(state.has_saved_next_instruction)
+  {
+    log.debug() << "Resuming from next instruction '"
+                << state_pc->source_location << "'" << log.eom;
   }
   else if(options.get_bool_option("paths"))
   {
-    // At this point, `state_pc` is the instruction we should execute
-    // immediately, and `new_state_pc` is the instruction that we should execute
-    // later (after we've finished exploring this branch). For path-based
-    // exploration, save `new_state_pc` to the saved state that we will resume
-    // executing from, so that goto_symex::symex_goto() knows that we've already
-    // explored the branch starting from `state_pc` when it is later called at
-    // this branch.
-    path_storaget::patht branch_point(target, state);
-    branch_point.state.saved_target = new_state_pc;
-    branch_point.state.has_saved_target = true;
+    // We should save both the instruction after this goto, and the target of
+    // the goto.
+
+    path_storaget::patht next_instruction(target, state);
+    next_instruction.state.saved_target = state_pc;
+    next_instruction.state.has_saved_next_instruction = true;
+    next_instruction.state.saved_target_is_backwards = !forward;
+
+    path_storaget::patht jump_target(target, state);
+    jump_target.state.saved_target = new_state_pc;
+    jump_target.state.has_saved_jump_target = true;
     // `forward` tells us where the branch we're _currently_ executing is
     // pointing to; this needs to be inverted for the branch that we're saving,
     // so let its truth value for `backwards` be the same as ours for `forward`.
-    branch_point.state.saved_target_is_backwards = forward;
-    path_storage.push(branch_point);
-    log.debug() << "Saving '" << new_state_pc->source_location << "'"
+    jump_target.state.saved_target_is_backwards = forward;
+
+    log.debug() << "Saving next instruction '"
+                << next_instruction.state.saved_target->source_location << "'"
+                << log.eom;
+    log.debug() << "Saving jump target '"
+                << jump_target.state.saved_target->source_location << "'"
                 << log.eom;
+    path_storage.push(next_instruction, jump_target);
+
+    // It is now up to the caller of symex to decide which path to continue
+    // executing. Signal to the caller that states have been pushed (therefore
+    // symex has not yet completed and must be resumed), and bail out.
+    should_pause_symex = true;
+    return;
   }
 
   // put into state-queue
@@ -242,7 +259,7 @@ void goto_symext::symex_goto(statet &state)
       state.rename(guard_expr, ns);
     }
 
-    if(state.has_saved_target)
+    if(state.has_saved_jump_target)
     {
       if(forward)
         state.guard.add(guard_expr);