Merge pull request #4362 from peterschrammel/property-decider-utilities

Factor out property decider utilities

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -30,6 +30,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/make_unique.h>
 #include <util/ui_message.h>
 
+#include "goto_symex_property_decider.h"
 #include "symex_bmc.h"
 
 void message_building_error_trace(messaget &log)
@@ -358,3 +359,63 @@ void postprocess_equation(
     symex.validate(validation_modet::INVARIANT);
   }
 }
+
+std::chrono::duration<double> prepare_property_decider(
+  propertiest &properties,
+  symex_target_equationt &equation,
+  goto_symex_property_decidert &property_decider,
+  ui_message_handlert &ui_message_handler)
+{
+  auto solver_start = std::chrono::steady_clock::now();
+
+  messaget log(ui_message_handler);
+  log.status() << "Passing problem to "
+               << property_decider.get_solver().decision_procedure_text()
+               << messaget::eom;
+
+  convert_symex_target_equation(
+    equation, property_decider.get_solver(), ui_message_handler);
+  property_decider.update_properties_goals_from_symex_target_equation(
+    properties);
+  property_decider.convert_goals();
+  property_decider.freeze_goal_variables();
+
+  auto solver_stop = std::chrono::steady_clock::now();
+  return std::chrono::duration<double>(solver_stop - solver_start);
+}
+
+void run_property_decider(
+  incremental_goto_checkert::resultt &result,
+  propertiest &properties,
+  goto_symex_property_decidert &property_decider,
+  ui_message_handlert &ui_message_handler,
+  std::chrono::duration<double> solver_runtime,
+  bool set_pass)
+{
+  auto solver_start = std::chrono::steady_clock::now();
+
+  messaget log(ui_message_handler);
+  log.status() << "Running "
+               << property_decider.get_solver().decision_procedure_text()
+               << messaget::eom;
+
+  property_decider.add_constraint_from_goals(
+    [&properties](const irep_idt &property_id) {
+      return is_property_to_check(properties.at(property_id).status);
+    });
+
+  decision_proceduret::resultt dec_result = property_decider.solve();
+
+  property_decider.update_properties_status_from_goals(
+    properties, result.updated_properties, dec_result, set_pass);
+
+  auto solver_stop = std::chrono::steady_clock::now();
+  solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
+  log.status() << "Runtime decision procedure: " << solver_runtime.count()
+               << "s" << messaget::eom;
+
+  if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
+  {
+    result.progress = incremental_goto_checkert::resultt::progresst::FOUND_FAIL;
+  }
+}

src/goto-checker/bmc_util.h

@@ -12,14 +12,17 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
 #define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
+#include <chrono>
 #include <memory>
 
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/build_goto_trace.h>
 #include <goto-symex/path_storage.h>
 
+#include "incremental_goto_checker.h"
 #include "properties.h"
 
+class goto_symex_property_decidert;
 class goto_tracet;
 class memory_model_baset;
 class message_handlert;
@@ -136,6 +139,39 @@ void update_status_of_unknown_properties(
   propertiest &properties,
   std::unordered_set<irep_idt> &updated_properties);
 
+/// Converts the equation and sets up the property decider,
+/// but does not call solve.
+/// \param [in,out] properties: Sets the status of properties to be checked to
+///   UNKNOWN
+/// \param [in,out] equation: The equation that will be converted
+/// \param [in,out] property_decider: The property decider that we are going to
+///   set up
+/// \param [in,out] ui_message_handler: For logging
+/// \return The runtime for converting the equation
+std::chrono::duration<double> prepare_property_decider(
+  propertiest &properties,
+  symex_target_equationt &equation,
+  goto_symex_property_decidert &property_decider,
+  ui_message_handlert &ui_message_handler);
+
+/// Runs the property decider to solve the equation
+/// \param [in,out] result: For recording the progress and the updated
+///   properties
+/// \param [in,out] properties: The status will be updated
+/// \param [in,out] property_decider: The property decider that will solve the
+///   equation
+/// \param [in,out] ui_message_handler: For logging
+/// \param solver_runtime: The solver runtime will be added and output
+/// \param set_pass: If true then update UNKNOWN properties to PASS
+///   if the solver returns UNSATISFIABLE
+void run_property_decider(
+  incremental_goto_checkert::resultt &result,
+  propertiest &properties,
+  goto_symex_property_decidert &property_decider,
+  ui_message_handlert &ui_message_handler,
+  std::chrono::duration<double> solver_runtime,
+  bool set_pass = true);
+
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \

src/goto-checker/multi_path_symex_checker.cpp

@@ -65,51 +65,18 @@ operator()(propertiest &properties)
     if(!has_properties_to_check(properties))
       return result;
 
-    log.status() << "Passing problem to "
-                 << property_decider.get_solver().decision_procedure_text()
-                 << messaget::eom;
-
-    const auto solver_start = std::chrono::steady_clock::now();
-
-    convert_symex_target_equation(
-      equation, property_decider.get_solver(), ui_message_handler);
-    property_decider.update_properties_goals_from_symex_target_equation(
-      properties);
-    property_decider.convert_goals();
-    property_decider.freeze_goal_variables();
+    solver_runtime += prepare_property_decider(
+      properties, equation, property_decider, ui_message_handler);
 
     if(options.get_bool_option("localize-faults"))
       freeze_guards(equation, property_decider.get_solver());
 
-    const auto solver_stop = std::chrono::steady_clock::now();
-    solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
-
-    log.status() << "Running "
-                 << property_decider.get_solver().decision_procedure_text()
-                 << messaget::eom;
     equation_generated = true;
   }
 
-  const auto solver_start = std::chrono::steady_clock::now();
-
-  property_decider.add_constraint_from_goals(
-    [&properties](const irep_idt &property_id) {
-      return is_property_to_check(properties.at(property_id).status);
-    });
-
-  decision_proceduret::resultt dec_result = property_decider.solve();
-
-  property_decider.update_properties_status_from_goals(
-    properties, result.updated_properties, dec_result);
-
-  const auto solver_stop = std::chrono::steady_clock::now();
-  solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
-  log.status() << "Runtime decision procedure: " << solver_runtime.count()
-               << "s" << messaget::eom;
+  run_property_decider(
+    result, properties, property_decider, ui_message_handler, solver_runtime);
 
-  result.progress = dec_result == decision_proceduret::resultt::D_SATISFIABLE
-                      ? resultt::progresst::FOUND_FAIL
-                      : resultt::progresst::DONE;
   return result;
 }
 

src/goto-checker/single_path_symex_checker.cpp

@@ -33,7 +33,14 @@ operator()(propertiest &properties)
   // There might be more solutions from the previous equation.
   if(property_decider)
   {
-    decide(result, properties);
+    run_property_decider(
+      result,
+      properties,
+      *property_decider,
+      ui_message_handler,
+      std::chrono::duration<double>(0),
+      false);
+
     if(result.progress == resultt::progresst::FOUND_FAIL)
       return result;
   }
@@ -91,8 +98,22 @@ operator()(propertiest &properties)
 
     if(symex.get_remaining_vccs() > 0)
     {
-      prepare(result, properties, resume.equation);
-      decide(result, properties);
+      update_properties_status_from_symex_target_equation(
+        properties, result.updated_properties, resume.equation);
+
+      property_decider = util_make_unique<goto_symex_property_decidert>(
+        options, ui_message_handler, resume.equation, ns);
+
+      const auto solver_runtime = prepare_property_decider(
+        properties, resume.equation, *property_decider, ui_message_handler);
+
+      run_property_decider(
+        result,
+        properties,
+        *property_decider,
+        ui_message_handler,
+        solver_runtime,
+        false);
 
       if(result.progress == resultt::progresst::FOUND_FAIL)
         return result;
@@ -175,58 +196,3 @@ void single_path_symex_checkert::output_proof()
   const path_storaget::patht &resume = worklist->peek();
   output_graphml(resume.equation, ns, options);
 }
-
-void single_path_symex_checkert::prepare(
-  resultt &result,
-  propertiest &properties,
-  symex_target_equationt &equation)
-{
-  update_properties_status_from_symex_target_equation(
-    properties, result.updated_properties, equation);
-
-  property_decider = util_make_unique<goto_symex_property_decidert>(
-    options, ui_message_handler, equation, ns);
-
-  log.status() << "Passing problem to "
-               << property_decider->get_solver().decision_procedure_text()
-               << messaget::eom;
-
-  convert_symex_target_equation(
-    equation, property_decider->get_solver(), ui_message_handler);
-  property_decider->update_properties_goals_from_symex_target_equation(
-    properties);
-  property_decider->convert_goals();
-  property_decider->freeze_goal_variables();
-}
-
-void single_path_symex_checkert::decide(
-  resultt &result,
-  propertiest &properties)
-{
-  auto solver_start = std::chrono::steady_clock::now();
-
-  log.status() << "Running "
-               << property_decider->get_solver().decision_procedure_text()
-               << messaget::eom;
-
-  property_decider->add_constraint_from_goals(
-    [&properties](const irep_idt &property_id) {
-      return is_property_to_check(properties.at(property_id).status);
-    });
-
-  decision_proceduret::resultt dec_result = property_decider->solve();
-
-  property_decider->update_properties_status_from_goals(
-    properties, result.updated_properties, dec_result, false);
-
-  auto solver_stop = std::chrono::steady_clock::now();
-  log.status()
-    << "Runtime decision procedure: "
-    << std::chrono::duration<double>(solver_stop - solver_start).count() << "s"
-    << messaget::eom;
-
-  if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
-  {
-    result.progress = resultt::progresst::FOUND_FAIL;
-  }
-}

src/goto-checker/single_path_symex_checker.h

@@ -47,12 +47,6 @@ class single_path_symex_checkert : public single_path_symex_only_checkert,
 protected:
   bool symex_initialized = false;
   std::unique_ptr<goto_symex_property_decidert> property_decider;
-
-  void prepare(
-    resultt &result,
-    propertiest &properties,
-    symex_target_equationt &equation);
-  void decide(resultt &result, propertiest &properties);
 };
 
 #endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H