Factor out perform_symex into bmc_util

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -292,3 +292,54 @@ void output_coverage_report(
                 << "'" << messaget::eom;
   }
 }
+
+static void postprocess_equation(
+  symex_bmct &symex,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler)
+{
+
+  // add a partial ordering, if required
+  // We won't be able to decide any properties by adding this,
+  // but we'd like to see the entire SSA.
+  if(equation.has_threads())
+  {
+    std::unique_ptr<memory_model_baset> memory_model =
+      get_memory_model(options, ns);
+    memory_model->set_message_handler(ui_message_handler);
+    (*memory_model)(equation);
+  }
+
+  messaget log(ui_message_handler);
+  log.statistics() << "size of program expression: "
+                   << equation.SSA_steps.size() << " steps" << messaget::eom;
+
+  slice(symex, equation, ns, options, ui_message_handler);
+
+  if(options.get_bool_option("validate-ssa-equation"))
+  {
+    symex.validate(validation_modet::INVARIANT);
+  }
+}
+
+void perform_symex(
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex,
+  symbol_tablet &symex_symbol_table,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler)
+{
+  auto get_goto_function =
+    [&goto_model](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
+  // perform symbolic execution
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+
+  postprocess_equation(symex, equation, options, ns, ui_message_handler);
+}

src/goto-checker/bmc_util.h

@@ -69,6 +69,16 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+/// Perform symbolic execution from the entry point
+void perform_symex(
+  abstract_goto_modelt &,
+  symex_bmct &,
+  symbol_tablet &,
+  symex_target_equationt &,
+  const optionst &,
+  const namespacet &,
+  ui_message_handlert &);
+
 void output_coverage_report(
   const std::string &cov_out,
   const abstract_goto_modelt &goto_model,

src/goto-checker/multi_path_symex_checker.cpp

@@ -39,7 +39,14 @@ operator()(propertiest &properties)
 
   if(!symex_has_run)
   {
-    perform_symex();
+    perform_symex(
+      goto_model,
+      symex,
+      symex_symbol_table,
+      equation,
+      options,
+      ns,
+      ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -39,7 +39,14 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::
 operator()(propertiest &properties)
 {
-  perform_symex();
+  perform_symex(
+    goto_model,
+    symex,
+    symex_symbol_table,
+    equation,
+    options,
+    ns,
+    ui_message_handler);
 
   output_coverage_report(
     options.get_option("symex-coverage-report"),
@@ -67,35 +74,3 @@ operator()(propertiest &properties)
     properties, result.updated_properties);
   return result;
 }
-
-void multi_path_symex_only_checkert::perform_symex()
-{
-  auto get_goto_function =
-    [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  // perform symbolic execution
-  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
-
-  // add a partial ordering, if required
-  // We won't be able to decide any properties by adding this,
-  // but we'd like to see the entire SSA.
-  if(equation.has_threads())
-  {
-    std::unique_ptr<memory_model_baset> memory_model =
-      get_memory_model(options, ns);
-    memory_model->set_message_handler(ui_message_handler);
-    (*memory_model)(equation);
-  }
-
-  log.statistics() << "size of program expression: "
-                   << equation.SSA_steps.size() << " steps" << messaget::eom;
-
-  slice(symex, equation, ns, options, ui_message_handler);
-
-  if(options.get_bool_option("validate-ssa-equation"))
-  {
-    symex.validate(validation_modet::INVARIANT);
-  }
-}

src/goto-checker/multi_path_symex_only_checker.h

@@ -33,8 +33,6 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symex_target_equationt equation;
   path_fifot path_storage; // should go away
   symex_bmct symex;
-
-  void perform_symex();
 };
 
 #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H