Symex paths saved onto abstract data structure

This commit introduces a new data type, path_queuet, representing saved
symbolic execution paths, used instead of the std::list. This allows us
to implement custom logic for saving and removing paths, rather than
simply pushing to the back and popping the front.

This commit introduces a concrete instantiation of path_queuet, called
path_fifot, with the same functionality as the old std::list. This is in
preparation for further instantiations that implement more sophisticated
logic for deciding which path should be resumed next.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -605,7 +605,8 @@ int bmct::do_language_agnostic_bmc(
   const symbol_tablet &symbol_table = model.get_symbol_table();
   message_handlert &mh = message.get_message_handler();
   safety_checkert::resultt result;
-  goto_symext::branch_worklistt worklist;
+  std::unique_ptr<path_storaget> worklist =
+    path_storaget::make(path_storaget::disciplinet::FIFO);
   try
   {
     {
@@ -614,17 +615,17 @@ int bmct::do_language_agnostic_bmc(
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex);
+      bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
       bmc.set_ui(ui);
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
       result = bmc.run(model);
     }
     INVARIANT(
-      opts.get_bool_option("paths") || worklist.empty(),
+      opts.get_bool_option("paths") || worklist->empty(),
       "the worklist should be empty after doing full-program "
       "model checking, but the worklist contains " +
-        std::to_string(worklist.size()) + " unexplored branches.");
+        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
@@ -641,31 +642,31 @@ int bmct::do_language_agnostic_bmc(
     // difference between the implementations of perform_symbolic_exection()
     // in bmct and path_explorert, for more information.
 
-    while(!worklist.empty())
+    while(!worklist->empty())
     {
       message.status() << "___________________________\n"
-                       << "Starting new path (" << worklist.size()
+                       << "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;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      goto_symext::branch_pointt &resume = worklist.front();
+      path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
         opts,
         symbol_table,
         mh,
         pc,
         resume.equation,
         resume.state,
-        worklist,
+        *worklist,
         callback_after_symex);
       if(driver_configure_bmc)
         driver_configure_bmc(pe, symbol_table);
       result &= pe.run(model);
-      worklist.pop_front();
+      worklist->pop();
     }
   }
   catch(const char *error_msg)
@@ -701,7 +702,7 @@ void bmct::perform_symbolic_execution(
 {
   symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
   INVARIANT(
-    options.get_bool_option("paths") || branch_worklist.empty(),
+    options.get_bool_option("paths") || path_storage.empty(),
     "Branch points were saved even though we should have been "
     "executing the entire program and merging paths");
 }

src/cbmc/bmc.h

@@ -23,6 +23,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_trace.h>
 
 #include <goto-symex/symex_target_equation.h>
+#include <goto-symex/path_storage.h>
+
 #include <goto-programs/goto_model.h>
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
@@ -49,32 +51,32 @@ class bmct:public safety_checkert
   ///   constructor is `false` (unset), an instance of this class will
   ///   symbolically execute the entire program, performing path merging
   ///   to build a formula corresponding to all executions of the program
-  ///   up to the unwinding limit. In this case, the `branch_worklist`
+  ///   up to the unwinding limit. In this case, the `path_storage`
   ///   member shall not be touched; this is enforced by the assertion in
   ///   this class' implementation of bmct::perform_symbolic_execution().
   ///
   /// - If the `--paths` flag is `true`, this `bmct` object will explore a
   ///   single path through the codebase without doing any path merging.
   ///   If some paths were not taken, the state at those branch points
-  ///   will be appended to `branch_worklist`. After the single path that
+  ///   will be appended to `path_storage`. After the single path that
   ///   this `bmct` object executed has been model-checked, you can resume
   ///   exploring further paths by popping an element from
-  ///   `branch_worklist` and using it to construct a path_explorert
+  ///   `path_storage` and using it to construct a path_explorert
   ///   object.
   bmct(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
-    goto_symext::branch_worklistt &_branch_worklist,
+    path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table, symex_symbol_table),
       equation(),
-      branch_worklist(_branch_worklist),
-      symex(_message_handler, outer_symbol_table, equation, branch_worklist),
+      path_storage(_path_storage),
+      symex(_message_handler, outer_symbol_table, equation, path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)
@@ -128,7 +130,7 @@ class bmct:public safety_checkert
   ///
   /// This constructor exists as a delegate for the path_explorert class.
   /// It differs from \ref bmct's public constructor in that it actually
-  /// does something with the branch_worklistt argument, and also takes a
+  /// does something with the path_storaget argument, and also takes a
   /// symex_target_equationt. See the documentation for path_explorert for
   /// details.
   bmct(
@@ -137,15 +139,15 @@ class bmct:public safety_checkert
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &_equation,
-    goto_symext::branch_worklistt &_branch_worklist,
+    path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       equation(_equation),
-      branch_worklist(_branch_worklist),
-      symex(_message_handler, outer_symbol_table, equation, branch_worklist),
+      path_storage(_path_storage),
+      symex(_message_handler, outer_symbol_table, equation, path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)
@@ -166,7 +168,7 @@ class bmct:public safety_checkert
   symbol_tablet symex_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
-  goto_symext::branch_worklistt &branch_worklist;
+  path_storaget &path_storage;
   symex_bmct symex;
   prop_convt &prop_conv;
   std::unique_ptr<memory_model_baset> memory_model;
@@ -257,15 +259,15 @@ class path_explorert : public bmct
     prop_convt &_prop_conv,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
-    goto_symext::branch_worklistt &branch_worklist,
+    path_storaget &path_storage,
     std::function<bool(void)> callback_after_symex)
     : bmct(
         _options,
         outer_symbol_table,
         _message_handler,
         _prop_conv,
         saved_equation,
-        branch_worklist,
+        path_storage,
         callback_after_symex),
       saved_state(saved_state)
   {

src/cbmc/symex_bmc.cpp

@@ -22,8 +22,8 @@ symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
-  goto_symext::branch_worklistt &branch_worklist)
-  : goto_symext(mh, outer_symbol_table, _target, branch_worklist),
+  path_storaget &path_storage)
+  : goto_symext(mh, outer_symbol_table, _target, path_storage),
     record_coverage(false),
     max_unwind(0),
     max_unwind_is_set(false),

src/cbmc/symex_bmc.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/threeval.h>
 
+#include <goto-symex/path_storage.h>
 #include <goto-symex/goto_symex.h>
 
 #include "symex_coverage.h"
@@ -26,7 +27,7 @@ class symex_bmct: public goto_symext
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
-    goto_symext::branch_worklistt &branch_worklist);
+    path_storaget &path_storage);
 
   // To show progress
   source_locationt last_source_location;

src/goto-instrument/accelerate/scratch_program.h

@@ -23,6 +23,7 @@ Author: Matt Lewis
 #include <goto-programs/goto_functions.h>
 
 #include <goto-symex/goto_symex.h>
+#include <goto-symex/path_storage.h>
 #include <goto-symex/symex_target_equation.h>
 
 #include <solvers/smt2/smt2_dec.h>
@@ -41,8 +42,8 @@ class scratch_programt:public goto_programt
       symex_symbol_table(),
       ns(symbol_table, symex_symbol_table),
       equation(),
-      branch_worklist(),
-      symex(mh, symbol_table, equation, branch_worklist),
+      path_storage(),
+      symex(mh, symbol_table, equation, path_storage),
       satcheck(util_make_unique<satcheckt>()),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
@@ -78,7 +79,7 @@ class scratch_programt:public goto_programt
   symbol_tablet symex_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
-  goto_symext::branch_worklistt branch_worklist;
+  path_fifot path_storage;
   goto_symext symex;
 
   std::unique_ptr<propt> satcheck;

src/goto-symex/Makefile

@@ -8,6 +8,7 @@ SRC = adjust_float_expressions.cpp \
       memory_model_sc.cpp \
       memory_model_tso.cpp \
       partial_order_concurrency.cpp \
+      path_storage.cpp \
       postcondition.cpp \
       precondition.cpp \
       rewrite_union.cpp \

src/goto-symex/goto_symex.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_functions.h>
 
 #include "goto_symex_state.h"
+#include "path_storage.h"
 #include "symex_target_equation.h"
 
 class byte_extract_exprt;
@@ -47,30 +48,11 @@ class goto_symext
 public:
   typedef goto_symex_statet statet;
 
-  /// \brief Information saved at a conditional goto to resume execution
-  struct branch_pointt
-  {
-    symex_target_equationt equation;
-    statet state;
-
-    explicit branch_pointt(const symex_target_equationt &e, const statet &s)
-      : equation(e), state(s, &equation)
-    {
-    }
-
-    explicit branch_pointt(const branch_pointt &other)
-      : equation(other.equation), state(other.state, &equation)
-    {
-    }
-  };
-
-  typedef std::list<branch_pointt> branch_worklistt;
-
   goto_symext(
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
-    branch_worklistt &branch_worklist)
+    path_storaget &path_storage)
     : total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
@@ -81,7 +63,7 @@ class goto_symext
       atomic_section_counter(0),
       log(mh),
       guard_identifier("goto_symex::\\guard"),
-      branch_worklist(branch_worklist)
+      path_storage(path_storage)
   {
     options.set_option("simplify", true);
     options.set_option("assertions", true);
@@ -462,7 +444,7 @@ class goto_symext
   void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
 
-  branch_worklistt &branch_worklist;
+  path_storaget &path_storage;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/path_storage.cpp

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: Path Storage
+
+Author: Kareem Khazem <[email protected]>
+
+\*******************************************************************/
+
+#include "path_storage.h"
+
+std::unique_ptr<path_storaget>
+path_storaget::make(path_storaget::disciplinet discipline)
+{
+  switch(discipline)
+  {
+  case path_storaget::disciplinet::FIFO:
+    return std::unique_ptr<path_fifot>(new path_fifot());
+  }
+  UNREACHABLE;
+}
+
+path_storaget::patht &path_fifot::peek()
+{
+  return paths.front();
+}
+
+void path_fifot::push(const path_storaget::patht &bp)
+{
+  paths.push_back(bp);
+}
+
+void path_fifot::pop()
+{
+  paths.pop_front();
+}
+
+std::size_t path_fifot::size() const
+{
+  return paths.size();
+}