Merge pull request #1915 from karkhaz/kk-abstract-paths-worklist

Path exploration goodies

Author: tautschnig

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.
@@ -595,17 +598,24 @@ void bmct::setup_unwind()
 /// \param callback_after_symex: optional callback to be run after symex.
 ///   See class member `bmct::driver_callback_after_symex` for details.
 int bmct::do_language_agnostic_bmc(
+  const path_strategy_choosert &path_strategy_chooser,
   const optionst &opts,
   abstract_goto_modelt &model,
   const ui_message_handlert::uit &ui,
   messaget &message,
   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;
-  goto_symext::branch_worklistt worklist;
+  std::unique_ptr<path_storaget> worklist;
+  std::string strategy = opts.get_option("exploration-strategy");
+  INVARIANT(
+    path_strategy_chooser.is_valid_strategy(strategy),
+    "Front-end passed us invalid path strategy '" + strategy + "'");
+  worklist = path_strategy_chooser.get(strategy);
   try
   {
     {
@@ -614,21 +624,23 @@ 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);
+      tmp_result = bmc.run(model);
+      if(tmp_result != safety_checkert::resultt::PAUSED)
+        final_result = tmp_result;
     }
     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
-    // 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
@@ -641,31 +653,34 @@ 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()
-                       << " 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;
       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();
+      tmp_result = pe.run(model);
+      if(tmp_result != safety_checkert::resultt::PAUSED)
+        final_result &= tmp_result;
+      worklist->pop();
     }
   }
   catch(const char *error_msg)
@@ -684,14 +699,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;
 }
@@ -701,7 +720,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, kroening@kroening.com
 #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)
@@ -115,6 +117,7 @@ class bmct:public safety_checkert
   }
 
   static int do_language_agnostic_bmc(
+    const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,
     abstract_goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
@@ -128,7 +131,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 +140,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 +169,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 +260,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)
   {
@@ -292,15 +295,17 @@ class path_explorert : public bmct
   "(no-unwinding-assertions)"                                                  \
   "(no-pretty-names)"                                                          \
   "(partial-loops)"                                                            \
-  "(paths)"                                                                    \
+  "(paths):"                                                                   \
+  "(show-symex-strategies)"                                                    \
   "(depth):"                                                                   \
   "(unwind):"                                                                  \
   "(unwindset):"                                                               \
   "(graphml-witness):"                                                         \
   "(unwindset):"
 
 #define HELP_BMC                                                               \
-  " --paths                      explore paths one at a time\n"                \
+  " --paths [strategy]           explore paths one at a time\n"                \
+  " --show-symex-strategies      list strategies for use with --paths\n"       \
   " --program-only               only show program expression\n"               \
   " --show-loops                 show the loops in the program\n"              \
   " --depth nr                   limit search depth\n"                         \

src/cbmc/cbmc_parse_options.cpp

@@ -68,7 +68,8 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "CBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -79,7 +80,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
   xml_interfacet(cmdline),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "CBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -146,8 +148,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
-  if(cmdline.isset("paths"))
-    options.set_option("paths", true);
+  if(cmdline.isset("show-symex-strategies"))
+  {
+    std::cout << path_strategy_chooser.show_strategies();
+    exit(CPROVER_EXIT_SUCCESS);
+  }
+
+  path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
 
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
@@ -531,7 +538,11 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
   return bmct::do_language_agnostic_bmc(
-    options, goto_model, ui_message_handler.get_ui(), *this);
+    path_strategy_chooser,
+    options,
+    goto_model,
+    ui_message_handler.get_ui(),
+    *this);
 }
 
 bool cbmc_parse_optionst::set_properties()

src/cbmc/cbmc_parse_options.h

@@ -110,6 +110,7 @@ class cbmc_parse_optionst:
 protected:
   goto_modelt goto_model;
   ui_message_handlert ui_message_handler;
+  const path_strategy_choosert path_strategy_chooser;
 
   void eval_verbosity();
   void register_languages();

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, kroening@kroening.com
 #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/doxyfile

@@ -281,7 +281,7 @@ OPTIMIZE_OUTPUT_VHDL   = NO
 # Note that for custom extensions you also need to set FILE_PATTERNS otherwise
 # the files are not read by doxygen.
 
-EXTENSION_MAPPING      =
+EXTENSION_MAPPING      = h=c++
 
 # If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments
 # according to the Markdown format, which allows for more readable

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;