Merge pull request #1641 from karkhaz/kk-big-6-6

Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking

Author: tautschnig

.gitignore

@@ -101,6 +101,7 @@ src/goto-cc/goto-cc.exe
 src/goto-cc/goto-cl.exe
 src/goto-instrument/goto-instrument
 src/goto-instrument/goto-instrument.exe
+src/jbmc/jbmc
 src/musketeer/musketeer
 src/musketeer/musketeer.exe
 src/symex/symex

scripts/cpplint.py

@@ -3625,8 +3625,8 @@ def CheckOperatorSpacing(filename, clean_lines, linenum, error):
 #          'Remove spaces around %s' % match.group(0))
 
 # check any inherited classes don't have a space between the type and the :
-  if Search(r'(struct|class)\s[\w_]*\s+:', line):
-    error(filename, linenum, 'readability/identifier_spacing', 4, 'There shouldn\'t be a space between class identifier and :')
+  if Search(r'(struct|class)\s[\w_]*:', line):
+    error(filename, linenum, 'readability/identifier_spacing', 4, 'There should be a space between class identifier and :')
 
   #check type definitions end with t
   # Look for class declarations and check the final character is a t

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

@@ -12,20 +12,24 @@ Author: Daniel Kroening, [email protected]
 #include "bmc.h"
 
 #include <chrono>
+#include <exception>
 #include <fstream>
 #include <iostream>
 #include <memory>
 
+#include <util/exit_codes.h>
 #include <util/string2int.h>
 #include <util/source_location.h>
 #include <util/string_utils.h>
+#include <util/memory_info.h>
 #include <util/message.h>
 #include <util/json.h>
 #include <util/cprover_prefix.h>
 
 #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>
@@ -37,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/memory_model_tso.h>
 #include <goto-symex/memory_model_pso.h>
 
+#include "cbmc_solvers.h"
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 
@@ -359,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())
@@ -595,3 +599,118 @@ void bmct::setup_unwind()
   if(options.get_option("unwind")!="")
     symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
 }
+
+int bmct::do_language_agnostic_bmc(
+  const optionst &opts,
+  const goto_modelt &goto_model,
+  const ui_message_handlert::uit &ui,
+  messaget &message,
+  std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
+{
+  message_handlert &mh = message.get_message_handler();
+  safety_checkert::resultt result;
+  goto_symext::branch_worklistt worklist;
+  try
+  {
+    {
+      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)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(const std::string &error_msg)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(...)
+  {
+    message.error() << "unable to get solver" << message.eom;
+    throw std::current_exception();
+  }
+
+  switch(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;
+  }
+  UNREACHABLE;
+}
+
+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");
+}
+
+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);
+}