Merge pull request #1614 from polgreen/cegis_cbmc

Cegis cbmc

Author: kroening

src/cbmc/bmc.cpp

@@ -45,6 +45,17 @@ void bmct::do_unwind_module()
   // this is a hook for hw-cbmc
 }
 
+/// Hook used by CEGIS to selectively freeze variables
+/// in the SAT solver after the SSA formula is added to the solver.
+/// Freezing variables is necessary to make use of incremental
+/// solving with MiniSat SimpSolver.
+/// Potentially a useful hook for other applications using
+/// incremental solving.
+void bmct::freeze_program_variables()
+{
+  // this is a hook for cegis
+}
+
 void bmct::error_trace()
 {
   status() << "Building error trace" << eom;
@@ -131,6 +142,8 @@ void bmct::do_conversion()
     forall_expr_list(it, bmc_constraints)
       prop_conv.set_to_true(*it);
   }
+  // hook for cegis to freeze synthesis program vars
+  freeze_program_variables();
 }
 
 decision_proceduret::resultt
@@ -305,11 +318,10 @@ void bmct::show_program()
   }
 }
 
-safety_checkert::resultt bmct::run(
-  const goto_functionst &goto_functions)
+
+void bmct::get_memory_model()
 {
   const std::string mm=options.get_option("mm");
-  std::unique_ptr<memory_model_baset> memory_model;
 
   if(mm.empty() || mm=="sc")
     memory_model=util_make_unique<memory_model_sct>(ns);
@@ -321,9 +333,13 @@ safety_checkert::resultt bmct::run(
   {
     error() << "Invalid memory model " << mm
             << " -- use one of sc, tso, pso" << eom;
-    return safety_checkert::resultt::ERROR;
+    throw "invalid memory model";
   }
+}
 
+void bmct::setup()
+{
+  get_memory_model();
   symex.set_message_handler(get_message_handler());
   symex.options=options;
 
@@ -337,11 +353,13 @@ safety_checkert::resultt bmct::run(
 
   symex.last_source_location.make_nil();
 
-  try
-  {
-    // get unwinding info
     setup_unwind();
+}
 
+safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
+{
+  try
+  {
     // perform symbolic execution
     symex(goto_functions);
 
@@ -351,77 +369,12 @@ safety_checkert::resultt bmct::run(
       memory_model->set_message_handler(get_message_handler());
       (*memory_model)(equation);
     }
-  }
-
-  catch(const std::string &error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
-
-    return safety_checkert::resultt::ERROR;
-  }
-
-  catch(const char *error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
-
-    return safety_checkert::resultt::ERROR;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return safety_checkert::resultt::ERROR;
-  }
 
   statistics() << "size of program expression: "
                << equation.SSA_steps.size()
                << " steps" << eom;
 
-  try
-  {
-    if(options.get_option("slice-by-trace")!="")
-    {
-      symex_slice_by_tracet symex_slice_by_trace(ns);
-
-      symex_slice_by_trace.slice_by_trace
-        (options.get_option("slice-by-trace"), equation);
-    }
-
-    if(equation.has_threads())
-    {
-      // we should build a thread-aware SSA slicer
-      statistics() << "no slicing due to threads" << eom;
-    }
-    else
-    {
-      if(options.get_bool_option("slice-formula"))
-      {
-        slice(equation);
-        statistics() << "slicing removed "
-                     << equation.count_ignored_SSA_steps()
-                     << " assignments" << eom;
-      }
-      else
-      {
-        if(options.get_list_option("cover").empty())
-        {
-          simple_slice(equation);
-          statistics() << "simple slicing removed "
-                       << equation.count_ignored_SSA_steps()
-                       << " assignments" << eom;
-        }
-      }
-    }
-
-    {
-      statistics() << "Generated " << symex.total_vccs
-                   << " VCC(s), " << symex.remaining_vccs
-                   << " remaining after simplification" << eom;
-    }
+    slice();
 
     // coverage report
     std::string cov_out=options.get_option("symex-coverage-report");
@@ -473,13 +426,19 @@ safety_checkert::resultt bmct::run(
 
   catch(const std::string &error_str)
   {
-    error() << error_str << eom;
+    messaget message(get_message_handler());
+    message.error().source_location=symex.last_source_location;
+    message.error() << error_str << messaget::eom;
+
     return safety_checkert::resultt::ERROR;
   }
 
   catch(const char *error_str)
   {
-    error() << error_str << eom;
+    messaget message(get_message_handler());
+    message.error().source_location=symex.last_source_location;
+    message.error() << error_str << messaget::eom;
+
     return safety_checkert::resultt::ERROR;
   }
 
@@ -490,6 +449,56 @@ safety_checkert::resultt bmct::run(
   }
 }
 
+void bmct::slice()
+{
+  if(options.get_option("slice-by-trace")!="")
+  {
+    symex_slice_by_tracet symex_slice_by_trace(ns);
+
+    symex_slice_by_trace.slice_by_trace
+    (options.get_option("slice-by-trace"),
+        equation);
+  }
+  // any properties to check at all?
+  if(equation.has_threads())
+  {
+    // we should build a thread-aware SSA slicer
+    statistics() << "no slicing due to threads" << eom;
+  }
+  else
+  {
+    if(options.get_bool_option("slice-formula"))
+    {
+      ::slice(equation);
+      statistics() << "slicing removed "
+                   << equation.count_ignored_SSA_steps()
+                   << " assignments"<<eom;
+    }
+    else
+    {
+      if(options.get_list_option("cover").empty())
+      {
+        simple_slice(equation);
+        statistics() << "simple slicing removed "
+                     << equation.count_ignored_SSA_steps()
+                     << " assignments"<<eom;
+      }
+    }
+  }
+  statistics() << "Generated "
+               << symex.total_vccs<<" VCC(s), "
+               << symex.remaining_vccs
+               << " remaining after simplification" << eom;
+}
+
+safety_checkert::resultt bmct::run(
+  const goto_functionst &goto_functions)
+{
+  setup();
+
+  return execute(goto_functions);
+}
+
 safety_checkert::resultt bmct::decide(
   const goto_functionst &goto_functions,
   prop_convt &prop_conv)
@@ -502,6 +511,19 @@ safety_checkert::resultt bmct::decide(
     return all_properties(goto_functions, prop_conv);
 }
 
+void bmct::show(const goto_functionst &goto_functions)
+{
+  if(options.get_bool_option("show-vcc"))
+  {
+    show_vcc();
+  }
+
+  if(options.get_bool_option("program-only"))
+  {
+    show_program();
+  }
+}
+
 safety_checkert::resultt bmct::stop_on_fail(
   const goto_functionst &goto_functions,
   prop_convt &prop_conv)

src/cbmc/bmc.h

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
+#include <goto-symex/memory_model.h>
 
 #include "symex_bmc.h"
 
@@ -52,6 +53,8 @@ class bmct:public safety_checkert
   }
 
   virtual resultt run(const goto_functionst &goto_functions);
+  void setup();
+  safety_checkert::resultt execute(const goto_functionst &);
   virtual ~bmct() { }
 
   // additional stuff
@@ -73,7 +76,7 @@ class bmct:public safety_checkert
   symex_target_equationt equation;
   symex_bmct symex;
   prop_convt &prop_conv;
-
+  std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
   ui_message_handlert::uit ui;
 
@@ -89,6 +92,8 @@ class bmct:public safety_checkert
   virtual void do_unwind_module();
   void do_conversion();
 
+  virtual void freeze_program_variables();
+
   virtual void show_vcc();
   virtual void show_vcc_plain(std::ostream &out);
   virtual void show_vcc_json(std::ostream &out);
@@ -108,6 +113,10 @@ class bmct:public safety_checkert
     resultt result,
     const goto_functionst &goto_functions);
 
+  void get_memory_model();
+  void slice();
+  void show(const goto_functionst &);
+
   bool cover(
     const goto_functionst &goto_functions,
     const optionst::value_listt &criteria);

src/goto-symex/goto_symex.h

@@ -80,6 +80,40 @@ class goto_symext
     const goto_functionst &goto_functions,
     const goto_programt &goto_program);
 
+  /// Symexes from the first instruction and the given state, terminating as
+  /// soon as the last instruction is reached.  This is useful to explicitly
+  /// symex certain ranges of a program, e.g. in an incremental decision
+  /// procedure.
+  /// \param state Symex state to start with.
+  /// \param goto_functions GOTO model to symex.
+  /// \param first Entry point in form of a first instruction.
+  /// \param limit Final instruction, which itself will not be symexed.
+  virtual void operator()(
+    statet &state,
+    const goto_functionst &goto_functions,
+    goto_programt::const_targett first,
+    goto_programt::const_targett limit);
+
+  /// Initialise the symbolic execution and the given state with <code>pc</code>
+  /// as entry point.
+  /// \param state Symex state to initialise.
+  /// \param goto_functions GOTO model to symex.
+  /// \param pc first instruction to symex
+  /// \param limit final instruction, which itself will not
+  /// be symexed.
+  void symex_entry_point(
+    statet &state,
+    const goto_functionst &goto_functions,
+    goto_programt::const_targett pc,
+    goto_programt::const_targett limit);
+
+  /// Invokes symex_step and verifies whether additional threads can be
+  /// executed.
+  /// \param state Current GOTO symex step.
+  /// \param goto_functions GOTO model to symex.
+  void symex_threaded_step(
+    statet &state, const goto_functionst &goto_functions);
+
   /** execute just one step */
   virtual void symex_step(
     const goto_functionst &goto_functions,