Remove dynamic_cast from hardness collection code paths

Use a `shared_ptr` to retain co-ownership of the hardness collector in
`solver_factoryt::solvert` and adjust the `symex_target_equationt` API
to `consume a solver_hardnesst`.

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -147,15 +147,16 @@ void output_graphml(
   }
 }
 
-void convert_symex_target_equation(
+static void convert_symex_target_equation(
   symex_target_equationt &equation,
   decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
   msg.status() << "converting SSA" << messaget::eom;
 
-  equation.convert(decision_procedure);
+  equation.convert(decision_procedure, hardness_collector);
 }
 
 std::unique_ptr<memory_model_baset>
@@ -370,7 +371,10 @@ std::chrono::duration<double> prepare_property_decider(
     << messaget::eom;
 
   convert_symex_target_equation(
-    equation, property_decider.get_decision_procedure(), ui_message_handler);
+    equation,
+    property_decider.get_decision_procedure(),
+    property_decider.get_hardness_collector(),
+    ui_message_handler);
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();

src/goto-checker/bmc_util.h

@@ -25,19 +25,13 @@ class decision_proceduret;
 class goto_symex_property_decidert;
 class goto_tracet;
 class memory_model_baset;
-class message_handlert;
 class namespacet;
 class optionst;
 class symex_bmct;
 class symex_target_equationt;
 struct trace_optionst;
 class ui_message_handlert;
 
-void convert_symex_target_equation(
-  symex_target_equationt &equation,
-  decision_proceduret &decision_procedure,
-  message_handlert &message_handler);
-
 /// Returns a function that checks whether an SSA step is an assertion
 /// with \p property_id. Usually used for `build_goto_trace`.
 ssa_step_predicatet

src/goto-checker/goto_symex_property_decider.cpp

@@ -100,13 +100,14 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   exprt goal_disjunction = disjunction(disjuncts);
   decision_procedure.set_to_true(goal_disjunction);
 
-  with_solver_hardness(decision_procedure, [](solver_hardnesst &hardness) {
+  if(auto hardness = solver->hardness_collector())
+  {
     // SSA expr and involved steps have already been collected
     // in symex_target_equationt::convert_assertions
     exprt ssa_expr_unused;
     std::vector<goto_programt::const_targett> involved_steps_unused;
-    hardness.register_assertion_ssas(ssa_expr_unused, involved_steps_unused);
-  });
+    hardness->register_assertion_ssas(ssa_expr_unused, involved_steps_unused);
+  };
 }
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
@@ -125,6 +126,11 @@ boolbvt &goto_symex_property_decidert::get_boolbv_decision_procedure() const
   return solver->boolbv_decision_procedure();
 }
 
+solver_hardnesst *goto_symex_property_decidert::get_hardness_collector() const
+{
+  return solver->hardness_collector();
+}
+
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
 {
   return equation;

src/goto-checker/goto_symex_property_decider.h

@@ -50,6 +50,10 @@ class goto_symex_property_decidert
   /// Returns the solver instance
   boolbvt &get_boolbv_decision_procedure() const;
 
+  /// Returns a pointer to the hardness collector or `nullptr` when hardness
+  /// collection is not set up.
+  solver_hardnesst *get_hardness_collector() const;
+
   /// Return the equation associated with this instance
   symex_target_equationt &get_equation() const;
 

src/goto-checker/multi_path_symex_checker.cpp

@@ -169,8 +169,9 @@ void multi_path_symex_checkert::report()
 {
   if(options.is_set("write-solver-stats-to"))
   {
-    with_solver_hardness(
-      property_decider.get_decision_procedure(),
-      [](solver_hardnesst &hardness) { hardness.produce_report(); });
+    if(auto hardness = property_decider.get_hardness_collector())
+    {
+      hardness->produce_report();
+    }
   }
 }

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -108,15 +108,18 @@ operator()(propertiest &properties)
 
         log.status() << "converting SSA" << messaget::eom;
         equation.convert_without_assertions(
-          property_decider.get_decision_procedure());
+          property_decider.get_decision_procedure(),
+          property_decider.get_hardness_collector());
 
         property_decider.update_properties_goals_from_symex_target_equation(
           properties);
 
         // We convert the assertions in a new context.
         property_decider.get_decision_procedure().push();
         equation.convert_assertions(
-          property_decider.get_decision_procedure(), false);
+          property_decider.get_decision_procedure(),
+          property_decider.get_hardness_collector(),
+          false);
         property_decider.convert_goals();
 
         current_equation_converted = true;

src/goto-checker/solver_factory.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include <goto-symex/solver_hardness.h>
 #include <solvers/flattening/bv_dimacs.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/solver_resource_limits.h>
@@ -71,6 +70,16 @@ solver_factoryt::solvert::solvert(
 {
 }
 
+solver_factoryt::solvert::solvert(
+  std::unique_ptr<boolbvt> p1,
+  std::unique_ptr<propt> p2,
+  std::shared_ptr<solver_hardnesst> p3)
+  : hardness_ptr(std::move(p3)),
+    prop_ptr(std::move(p2)),
+    decision_procedure_is_boolbvt_ptr(std::move(p1))
+{
+}
+
 stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const
 {
   PRECONDITION(
@@ -88,6 +97,11 @@ boolbvt &solver_factoryt::solvert::boolbv_decision_procedure() const
   return *decision_procedure_is_boolbvt_ptr;
 }
 
+solver_hardnesst *solver_factoryt::solvert::hardness_collector() const
+{
+  return hardness_ptr.get();
+}
+
 void solver_factoryt::set_decision_procedure_time_limit(
   solver_resource_limitst &decision_procedure)
 {
@@ -168,8 +182,9 @@ static void emit_solver_warning(
 template <typename SatcheckT>
 static typename std::enable_if<
   !std::is_base_of<hardness_collectort, SatcheckT>::value,
-  std::unique_ptr<SatcheckT>>::type
-make_satcheck_prop(message_handlert &message_handler, const optionst &options)
+  std::pair<std::unique_ptr<SatcheckT>, std::shared_ptr<solver_hardnesst>>>::
+  type
+  make_satcheck_prop(message_handlert &message_handler, const optionst &options)
 {
   auto satcheck = std::make_unique<SatcheckT>(message_handler);
   if(options.is_set("write-solver-stats-to"))
@@ -179,27 +194,29 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
       << "Configured solver does not support --write-solver-stats-to. "
       << "Solver stats will not be written." << messaget::eom;
   }
-  return satcheck;
+  return {std::move(satcheck), nullptr};
 }
 
 template <typename SatcheckT>
 static typename std::enable_if<
   std::is_base_of<hardness_collectort, SatcheckT>::value,
-  std::unique_ptr<SatcheckT>>::type
-make_satcheck_prop(message_handlert &message_handler, const optionst &options)
+  std::pair<std::unique_ptr<SatcheckT>, std::shared_ptr<solver_hardnesst>>>::
+  type
+  make_satcheck_prop(message_handlert &message_handler, const optionst &options)
 {
   auto satcheck = std::make_unique<SatcheckT>(message_handler);
-  if(options.is_set("write-solver-stats-to"))
-  {
-    std::unique_ptr<solver_hardnesst> solver_hardness =
-      std::make_unique<solver_hardnesst>();
-    solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
-    satcheck->solver_hardness = std::move(solver_hardness);
-  }
-  return satcheck;
+  if(!options.is_set("write-solver-stats-to"))
+    return {std::move(satcheck), nullptr};
+
+  std::shared_ptr<solver_hardnesst> solver_hardness =
+    std::make_shared<solver_hardnesst>();
+  solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
+  satcheck->solver_hardness = solver_hardness;
+
+  return {std::move(satcheck), std::move(solver_hardness)};
 }
 
-static std::unique_ptr<propt>
+static std::pair<std::unique_ptr<propt>, std::shared_ptr<solver_hardnesst>>
 get_sat_solver(message_handlert &message_handler, const optionst &options)
 {
   const bool no_simplifier = options.get_bool_option("beautify") ||
@@ -326,12 +343,15 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 {
-  auto sat_solver = get_sat_solver(message_handler, options);
+  auto sat_solver_and_hardness_opt = get_sat_solver(message_handler, options);
 
   bool get_array_constraints =
     options.get_bool_option("show-array-constraints");
   auto bv_pointers = std::make_unique<bv_pointerst>(
-    ns, *sat_solver, message_handler, get_array_constraints);
+    ns,
+    *sat_solver_and_hardness_opt.first,
+    message_handler,
+    get_array_constraints);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
@@ -341,7 +361,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
   set_decision_procedure_time_limit(*bv_pointers);
 
   std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
-  return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
+  return std::make_unique<solvert>(
+    std::move(boolbv),
+    std::move(sat_solver_and_hardness_opt.first),
+    std::move(sat_solver_and_hardness_opt.second));
 }
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
@@ -376,11 +399,11 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
 {
-  std::unique_ptr<propt> prop = get_sat_solver(message_handler, options);
+  auto prop_and_hardness_opt = get_sat_solver(message_handler, options);
 
   bv_refinementt::infot info;
   info.ns = &ns;
-  info.prop = prop.get();
+  info.prop = prop_and_hardness_opt.first.get();
   info.output_xml = output_xml_in_refinement;
 
   // we allow setting some parameters
@@ -396,7 +419,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
     std::make_unique<bv_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
-    std::move(decision_procedure), std::move(prop));
+    std::move(decision_procedure),
+    std::move(prop_and_hardness_opt.first),
+    std::move(prop_and_hardness_opt.second));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
@@ -407,8 +432,8 @@ solver_factoryt::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns = &ns;
-  auto prop = get_sat_solver(message_handler, options);
-  info.prop = prop.get();
+  auto prop_and_hardness_opt = get_sat_solver(message_handler, options);
+  info.prop = prop_and_hardness_opt.first.get();
   info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;
   if(options.get_bool_option("max-node-refinement"))
@@ -422,7 +447,9 @@ solver_factoryt::get_string_refinement()
     std::make_unique<string_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
-    std::move(decision_procedure), std::move(prop));
+    std::move(decision_procedure),
+    std::move(prop_and_hardness_opt.first),
+    std::move(prop_and_hardness_opt.second));
 }
 
 std::unique_ptr<std::ofstream> open_outfile_and_check(

src/goto-checker/solver_factory.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 
+#include <goto-symex/solver_hardness.h>
 #include <solvers/flattening/boolbv.h>
 #include <solvers/smt2/smt2_dec.h>
 
@@ -46,11 +47,17 @@ class solver_factoryt final
       std::unique_ptr<stack_decision_proceduret> p1,
       std::unique_ptr<std::ofstream> p2);
     solvert(std::unique_ptr<boolbvt> p1, std::unique_ptr<propt> p2);
+    solvert(
+      std::unique_ptr<boolbvt> p1,
+      std::unique_ptr<propt> p2,
+      std::shared_ptr<solver_hardnesst> p3);
 
     stack_decision_proceduret &decision_procedure() const;
     boolbvt &boolbv_decision_procedure() const;
+    solver_hardnesst *hardness_collector() const;
 
   private:
+    std::shared_ptr<solver_hardnesst> hardness_ptr;
     // the objects are deleted in the opposite order they appear below
     std::unique_ptr<std::ofstream> ofstream_ptr;
     std::unique_ptr<propt> prop_ptr;

src/goto-instrument/accelerate/scratch_program.cpp

@@ -63,7 +63,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
     return false;
   }
 
-  equation.convert(*checker);
+  equation.convert(*checker, nullptr);
 
 #ifdef DEBUG
   std::cout << "Finished symex, invoking decision procedure.\n";

src/goto-symex/solver_hardness.h

@@ -158,26 +158,4 @@ struct hash<solver_hardnesst::hardness_ssa_keyt>
 };
 } // namespace std
 
-static inline void with_solver_hardness(
-  decision_proceduret &maybe_hardness_collector,
-  std::function<void(solver_hardnesst &hardness)> handler)
-{
-  // FIXME I am wondering if there is a way to do this that is a bit less
-  // dynamically typed.
-  if(
-    auto prop_conv_solver =
-      dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
-  {
-    if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
-    {
-      if(hardness_collector->solver_hardness)
-      {
-        auto &solver_hardness = static_cast<solver_hardnesst &>(
-          *(hardness_collector->solver_hardness));
-        handler(solver_hardness);
-      }
-    }
-  }
-}
-
 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H