refactoring bmc.cpp

bmct::run is now split into:
    bmct::setup
    bmct::get_memory_model
    bmct::slice
    bmct::execute
    bmct::show

This change is necessary for incremental checking

Author: polgreen

src/cbmc/bmc.cpp

@@ -305,11 +305,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 +320,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 +340,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 +356,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 +413,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 +436,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 +498,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;
 
@@ -108,6 +111,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);