prop_conv_solvert is not a messaget

Gets a log member instead.

Author: peterschrammel

jbmc/src/jbmc/bmc.cpp

@@ -204,8 +204,11 @@ safety_checkert::resultt bmct::stop_on_fail()
     if(options.get_bool_option("trace"))
     {
       if(options.get_bool_option("beautify"))
-        counterexample_beautificationt()(
+      {
+        // NOLINTNEXTLINE(whitespace/braces)
+        counterexample_beautificationt{ui_message_handler}(
           dynamic_cast<boolbvt &>(prop_conv), equation);
+      }
 
       build_error_trace(
         error_trace, ns, equation, prop_conv, ui_message_handler);

src/goto-checker/counterexample_beautification.cpp

@@ -19,6 +19,12 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/literal_expr.h>
 #include <solvers/prop/minimize.h>
 
+counterexample_beautificationt::counterexample_beautificationt(
+  message_handlert &message_handler)
+  : log(message_handler)
+{
+}
+
 void counterexample_beautificationt::get_minimization_list(
   prop_convt &prop_conv,
   const symex_target_equationt &equation,
@@ -92,7 +98,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
   boolbv.set_to(literal_exprt(failed->cond_literal), false);
 
   {
-    boolbv.status() << "Beautifying counterexample (guards)" << messaget::eom;
+    log.status() << "Beautifying counterexample (guards)" << messaget::eom;
 
     // compute weights for guards
     typedef std::map<literalt, unsigned> guard_countt;
@@ -117,8 +123,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
     }
 
     // give to propositional minimizer
-    prop_minimizet prop_minimize(boolbv);
-    prop_minimize.set_message_handler(boolbv.get_message_handler());
+    prop_minimizet prop_minimize{boolbv, log.get_message_handler()};
 
     for(const auto &g : guard_count)
       prop_minimize.objective(g.first, g.second);
@@ -128,16 +133,15 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
   }
 
   {
-    boolbv.status() << "Beautifying counterexample (values)" << messaget::eom;
+    log.status() << "Beautifying counterexample (values)" << messaget::eom;
 
     // get symbols we care about
     minimization_listt minimization_list;
 
     get_minimization_list(boolbv, equation, minimization_list);
 
     // minimize
-    bv_minimizet bv_minimize(boolbv);
-    bv_minimize.set_message_handler(boolbv.get_message_handler());
+    bv_minimizet bv_minimize(boolbv, log.get_message_handler());
     bv_minimize(minimization_list);
   }
 }

src/goto-checker/counterexample_beautification.h

@@ -21,9 +21,8 @@ Author: Daniel Kroening, [email protected]
 class counterexample_beautificationt
 {
 public:
-  virtual ~counterexample_beautificationt()
-  {
-  }
+  explicit counterexample_beautificationt(message_handlert &message_handler);
+  virtual ~counterexample_beautificationt() = default;
 
   void operator()(boolbvt &boolbv, const symex_target_equationt &equation);
 
@@ -41,6 +40,8 @@ class counterexample_beautificationt
 
   // the failed property
   symex_target_equationt::SSA_stepst::const_iterator failed;
+
+  messaget log;
 };
 
 #endif // CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H

src/goto-checker/multi_path_symex_checker.cpp

@@ -104,7 +104,8 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const
 {
   if(options.get_bool_option("beautify"))
   {
-    counterexample_beautificationt()(
+    // NOLINTNEXTLINE(whitespace/braces)
+    counterexample_beautificationt{ui_message_handler}(
       dynamic_cast<boolbvt &>(property_decider.get_solver()), equation);
   }
 

src/goto-checker/single_path_symex_checker.cpp

@@ -133,7 +133,8 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const
 {
   if(options.get_bool_option("beautify"))
   {
-    counterexample_beautificationt()(
+    // NOLINTNEXTLINE(whitespace/braces)
+    counterexample_beautificationt{ui_message_handler}(
       dynamic_cast<boolbvt &>(property_decider->get_solver()),
       property_decider->get_equation());
   }

src/goto-checker/solver_factory.cpp

@@ -157,8 +157,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
     solver->set_prop(util_make_unique<satcheckt>(message_handler));
   }
 
-  auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
-  bv_pointers->set_message_handler(message_handler);
+  auto bv_pointers =
+    util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
@@ -180,8 +180,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
 
   std::string filename = options.get_option("outfile");
 
-  auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
-  bv_dimacs->set_message_handler(message_handler);
+  auto bv_dimacs =
+    util_make_unique<bv_dimacst>(ns, *prop, message_handler, filename);
   return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
 }
 
@@ -209,9 +209,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
 
   info.refine_arrays = options.get_bool_option("refine-arrays");
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
+  info.message_handler = &message_handler;
 
   auto prop_conv = util_make_unique<bv_refinementt>(info);
-  prop_conv->set_message_handler(message_handler);
   set_prop_conv_time_limit(*prop_conv);
   return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
 }
@@ -233,9 +233,9 @@ solver_factoryt::get_string_refinement()
       options.get_unsigned_int_option("max-node-refinement");
   info.refine_arrays = options.get_bool_option("refine-arrays");
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
+  info.message_handler = &message_handler;
 
   auto prop_conv = util_make_unique<string_refinementt>(info);
-  prop_conv->set_message_handler(message_handler);
   set_prop_conv_time_limit(*prop_conv);
   return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
 }

src/goto-instrument/accelerate/scratch_program.h

@@ -49,7 +49,7 @@ class scratch_programt:public goto_programt
       options(get_default_options()),
       symex(mh, symbol_table, equation, options, path_storage, guard_manager),
       satcheck(util_make_unique<satcheckt>(mh)),
-      satchecker(ns, *satcheck),
+      satchecker(ns, *satcheck, mh),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
       checker(&z3) // checker(&satchecker)
   {

src/solvers/flattening/arrays.cpp

@@ -22,8 +22,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
-arrayst::arrayst(const namespacet &_ns, propt &_prop)
-  : equalityt(_prop), ns(_ns)
+arrayst::arrayst(
+  const namespacet &_ns,
+  propt &_prop,
+  message_handlert &message_handler)
+  : equalityt(_prop, message_handler), ns(_ns)
 {
   lazy_arrays = false;        // will be set to true when --refine is used
   incremental_cache = false;  // for incremental solving
@@ -48,7 +51,7 @@ literalt arrayst::record_array_equality(
   // check types
   if(op0.type() != op1.type())
   {
-    error() << equality.pretty() << messaget::eom;
+    log.error() << equality.pretty() << messaget::eom;
     DATA_INVARIANT(
       false,
       "record_array_equality got equality without matching types");
@@ -116,7 +119,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(array_type != with_expr.old().type())
     {
-      error() << a.pretty() << messaget::eom;
+      log.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
@@ -137,7 +140,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(array_type != update_expr.old().type())
     {
-      error() << a.pretty() << messaget::eom;
+      log.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "collect_arrays got 'update' without matching types");
@@ -159,14 +162,14 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(array_type != if_expr.true_case().type())
     {
-      error() << a.pretty() << messaget::eom;
+      log.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(array_type != if_expr.false_case().type())
     {
-      error() << a.pretty() << messaget::eom;
+      log.error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
@@ -520,7 +523,7 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      error() << expr.pretty() << messaget::eom;
+      log.error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "with-expression operand should match array element type");
@@ -596,7 +599,7 @@ void arrayst::add_array_constraints_update(
 
     if(index_expr.type()!=value.type())
     {
-      prop.message.error() << expr.pretty() << messaget::eom;
+      prop.message.log.error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "update operand should match array element type");

src/solvers/flattening/arrays.h

@@ -29,7 +29,10 @@ class update_exprt;
 class arrayst:public equalityt
 {
 public:
-  arrayst(const namespacet &_ns, propt &_prop);
+  arrayst(
+    const namespacet &_ns,
+    propt &_prop,
+    message_handlert &message_handler);
 
   void post_process() override
   {

src/solvers/flattening/boolbv.h

@@ -32,8 +32,11 @@ class member_exprt;
 class boolbvt:public arrayst
 {
 public:
-  boolbvt(const namespacet &_ns, propt &_prop)
-    : arrayst(_ns, _prop),
+  boolbvt(
+    const namespacet &_ns,
+    propt &_prop,
+    message_handlert &message_handler)
+    : arrayst(_ns, _prop, message_handler),
       unbounded_array(unbounded_arrayt::U_NONE),
       boolbv_width(_ns),
       bv_utils(_prop),

src/solvers/flattening/boolbv_constant.cpp

@@ -33,8 +33,9 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
       if(tmp.size()!=op_width)
       {
-        error().source_location=expr.find_source_location();
-        error() << "convert_constant: unexpected operand width" << eom;
+        log.error().source_location = expr.find_source_location();
+        log.error() << "convert_constant: unexpected operand width"
+                    << messaget::eom;
         throw 0;
       }
 
@@ -101,9 +102,9 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
     if(binary.size()*2!=width)
     {
-      error().source_location=expr.find_source_location();
-      error() << "wrong value length in constant: "
-              << expr.pretty() << eom;
+      log.error().source_location = expr.find_source_location();
+      log.error() << "wrong value length in constant: " << expr.pretty()
+                  << messaget::eom;
       throw 0;
     }
 
@@ -135,9 +136,9 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
         break;
 
       default:
-        error().source_location=expr.find_source_location();
-        error() << "unknown character in Verilog constant:"
-                << expr.pretty() << eom;
+        log.error().source_location = expr.find_source_location();
+        log.error() << "unknown character in Verilog constant:" << expr.pretty()
+                    << messaget::eom;
         throw 0;
       }
     }