[path explore 5/7] Support path-based exploratio2

This commit introduces the --paths flag to CBMC, which makes CBMC
model-check each individual path of the program rather than merging
paths and model-checking the entire program.

The overall strategy involves allowing the "state" of symbolic
execution---i.e., a pair of goto_symex_statet and symex_target_equationt
---to be saved during an execution, and for an execution to be resumed
from a saved pair. By saving the state at every branch point and
disabling path merging, symbolic execution only runs along one path but
populates a worklist of saved states that should be executed later. At
the top level, CBMC or JBMC loops while the worklist of saved states is
non-empty, creating a new bmct object to resume executing each saved
path.

This commit includes the following supporting changes:

- goto_symex_statet now owns a symbol table, separate from the one
  supporting the goto_program, which is used for dynamically created
  objects during symbolic execution. goto_symex was previously using a
  symbol table that was passed to it by reference for this purpose, but
  that symbol table is needed when resuming symbolic execution from a
  saved point and so ought properly to be part of the symbolic execution
  state.

- goto_symex_statet now has a pointer to a symex_target_equationt, which
  can be updated with an equation from a previously-saved symbolic
  execution run. While equations are also conceptually part of the state
  of symbolic execution, they are heavily used after symbolic execution
  has completed (and the symex state has been deallocated) and so the
  equation is not owned by the state. An explicit copy constructor has
  been added to goto_symex_statet that initializes the equation member,
  so that symbolic execution can proceed either with an empty equation
  or with an equation that was earlier saved.

- goto_symex_statet no longer has a pointer to a dirtyt, as this was
  hindering it from being copied.

Author: karkhaz

src/analyses/dirty.cpp

@@ -69,6 +69,7 @@ void dirtyt::find_dirty_address_of(const exprt &expr)
 
 void dirtyt::output(std::ostream &out) const
 {
+  die_if_uninitialized();
   for(const auto &d : dirty)
     out << d << '\n';
 }

src/analyses/dirty.h

@@ -17,49 +17,80 @@ Date: March 2013
 #include <unordered_set>
 
 #include <util/std_expr.h>
+#include <util/invariant.h>
 #include <goto-programs/goto_functions.h>
 
 class dirtyt
 {
+private:
+  void die_if_uninitialized() const
+  {
+    INVARIANT(
+      initialized,
+      "Uninitialized dirtyt. This dirtyt was constructed using the default "
+      "constructor and not subsequently initialized using "
+      "dirtyt::build().");
+  }
+
 public:
+  bool initialized;
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   typedef goto_functionst::goto_functiont goto_functiont;
 
-  dirtyt()
+  /// \post dirtyt objects that are created through this constructor are not
+  /// safe to use. If you copied a dirtyt (for example, by adding an object
+  /// that owns a dirtyt to a container and then copying it back out), you will
+  /// need to re-initialize the dirtyt by calling dirtyt::build().
+  dirtyt() : initialized(false)
   {
   }
 
-  explicit dirtyt(const goto_functiont &goto_function)
+  explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
   {
     build(goto_function);
+    initialized = true;
   }
 
-  explicit dirtyt(const goto_functionst &goto_functions)
+  explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
   {
-    forall_goto_functions(it, goto_functions)
-      build(it->second);
+    build(goto_functions);
+    // build(g_funs) responsible for setting initialized to true, since
+    // it is public and can be called independently
   }
 
   void output(std::ostream &out) const;
 
   bool operator()(const irep_idt &id) const
   {
+    die_if_uninitialized();
     return dirty.find(id)!=dirty.end();
   }
 
   bool operator()(const symbol_exprt &expr) const
   {
+    die_if_uninitialized();
     return operator()(expr.get_identifier());
   }
 
   const id_sett &get_dirty_ids() const
   {
+    die_if_uninitialized();
     return dirty;
   }
 
   void add_function(const goto_functiont &goto_function)
   {
     build(goto_function);
+    initialized = true;
+  }
+
+  void build(const goto_functionst &goto_functions)
+  {
+    // dirtyts should not be initialized twice
+    PRECONDITION(!initialized);
+    forall_goto_functions(it, goto_functions)
+      build(it->second);
+    initialized = true;
   }
 
 protected:

src/cbmc/bmc.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/mode.h>
 #include <langapi/language_util.h>
 
+#include <goto-programs/goto_model.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
 #include <goto-programs/graphml_witness.h>
@@ -363,8 +364,7 @@ safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
 {
   try
   {
-    // perform symbolic execution
-    symex.symex_from_entry_point_of(goto_functions);
+    perform_symbolic_execution(goto_functions);
 
     // add a partial ordering, if required
     if(equation.has_threads())
@@ -607,13 +607,69 @@ int bmct::do_language_agnostic_bmc(
   messaget &message,
   std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
 {
-  cbmc_solverst solvers(
-    opts, goto_model.symbol_table, message.get_message_handler());
-  solvers.set_ui(ui);
-  std::unique_ptr<cbmc_solverst::solvert> solver;
+  message_handlert &mh = message.get_message_handler();
+  safety_checkert::resultt result;
+  goto_symext::branch_worklistt worklist;
   try
   {
-    solver = solvers.get_solver();
+    {
+      cbmc_solverst solvers(
+        opts, goto_model.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();
+      bmct bmc(opts, goto_model.symbol_table, mh, pc, worklist);
+      bmc.set_ui(ui);
+      frontend_configure_bmc(bmc, goto_model);
+      result = bmc.run(goto_model.goto_functions);
+    }
+    INVARIANT(
+      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.");
+
+    // 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
+    // empty, and we don't enter this loop.
+    //
+    // When doing path exploration, there will be some saved paths left to
+    // explore in the worklist. We thus need to run the above code again,
+    // once for each saved path in the worklist, to continue symbolically
+    // execute the program. Note that the code in the loop is similar to
+    // the code above except that we construct a path_explorert rather than
+    // a bmct, which allows us to execute from a saved state rather than
+    // from the entry point. See the path_explorert documentation, and the
+    // difference between the implementations of perform_symbolic_exection()
+    // in bmct and path_explorert, for more information.
+
+    while(!worklist.empty())
+    {
+      message.status() << "___________________________\n"
+                       << "Starting new path (" << worklist.size()
+                       << " to go)\n"
+                       << message.eom;
+      cbmc_solverst solvers(
+        opts, goto_model.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_explorert pe(
+        opts,
+        goto_model.symbol_table,
+        mh,
+        pc,
+        resume.equation,
+        resume.state,
+        worklist);
+      frontend_configure_bmc(pe, goto_model);
+      result &= pe.run(goto_model.goto_functions);
+      worklist.pop_front();
+    }
   }
   catch(const char *error_msg)
   {
@@ -631,35 +687,30 @@ int bmct::do_language_agnostic_bmc(
     throw std::current_exception();
   }
 
-  bmct bmc(
-    opts,
-    goto_model.symbol_table,
-    message.get_message_handler(),
-    solver->prop_conv());
-
-  frontend_configure_bmc(bmc, goto_model);
-  bmc.set_ui(ui);
-
-  int result = CPROVER_EXIT_INTERNAL_ERROR;
-
-  // do actual BMC
-  switch(bmc.run(goto_model.goto_functions))
+  switch(result)
   {
   case safety_checkert::resultt::SAFE:
-    result = CPROVER_EXIT_VERIFICATION_SAFE;
-    break;
+    return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
-    result = CPROVER_EXIT_VERIFICATION_UNSAFE;
-    break;
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
-    result = CPROVER_EXIT_INTERNAL_ERROR;
-    break;
+    return CPROVER_EXIT_INTERNAL_ERROR;
   }
+  UNREACHABLE;
+}
 
-  // let's log some more statistics
-  message.debug() << "Memory consumption:" << messaget::endl;
-  memory_info(message.debug());
-  message.debug() << eom;
+void bmct::perform_symbolic_execution(const goto_functionst &goto_functions)
+{
+  symex.symex_from_entry_point_of(goto_functions, symex_symbol_table);
+  INVARIANT(
+    options.get_bool_option("paths") || branch_worklist.empty(),
+    "Branch points were saved even though we should have been "
+    "executing the entire program and merging paths");
+}
 
-  return result;
+void path_explorert::perform_symbolic_execution(
+  const goto_functionst &goto_functions)
+{
+  symex.resume_symex_from_saved_state(
+    goto_functions, saved_state, &equation, symex_symbol_table);
 }