A decision_proceduret isn't a messaget

Some derived classes may want to generate output, but then it's safe for them to
be messaget's.

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -54,8 +54,6 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 {
   status() << "Passing problem to " << solver.decision_procedure_text() << eom;
 
-  solver.set_message_handler(get_message_handler());
-
   auto solver_start=std::chrono::steady_clock::now();
 
   convert_symex_target_equation(

src/cbmc/bmc.cpp

@@ -45,8 +45,6 @@ decision_proceduret::resultt bmct::run_decision_procedure()
   status() << "Passing problem to "
            << prop_conv.decision_procedure_text() << eom;
 
-  prop_conv.set_message_handler(get_message_handler());
-
   auto solver_start = std::chrono::steady_clock::now();
 
   convert_symex_target_equation(equation, prop_conv, get_message_handler());
@@ -192,8 +190,6 @@ safety_checkert::resultt bmct::run(
 
 safety_checkert::resultt bmct::decide(const goto_functionst &goto_functions)
 {
-  prop_conv.set_message_handler(get_message_handler());
-
   if(options.get_bool_option("stop-on-fail"))
     return stop_on_fail();
   else

src/cbmc/bmc.h

@@ -75,7 +75,7 @@ class bmct:public safety_checkert
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table, symex_symbol_table),
-      equation(),
+      equation(_message_handler),
       path_storage(_path_storage),
       symex(
         _message_handler,

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -26,6 +26,7 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
   : incremental_goto_checkert(options, ui_message_handler),
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
+    equation(ui_message_handler),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),

src/goto-checker/single_path_symex_checker.cpp

@@ -49,7 +49,7 @@ operator()(propertiest &properties)
     symex_initialized = true;
 
     // Put initial state into the work list
-    symex_target_equationt equation;
+    symex_target_equationt equation(ui_message_handler);
     symex_bmct symex(
       ui_message_handler,
       goto_model.get_symbol_table(),

src/goto-checker/single_path_symex_only_checker.cpp

@@ -39,7 +39,7 @@ operator()(propertiest &properties)
 
   {
     // Put initial state into the work list
-    symex_target_equationt equation;
+    symex_target_equationt equation(ui_message_handler);
     symex_bmct symex(
       ui_message_handler,
       goto_model.get_symbol_table(),

src/goto-checker/solver_factory.cpp

@@ -268,6 +268,8 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_dec->use_FPA_theory = true;
 
+    smt2_dec->set_message_handler(message_handler);
+
     set_prop_conv_time_limit(*smt2_dec);
     return util_make_unique<solvert>(std::move(smt2_dec));
   }
@@ -284,8 +286,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory = true;
 
-    smt2_conv->set_message_handler(message_handler);
-
     set_prop_conv_time_limit(*smt2_conv);
     return util_make_unique<solvert>(std::move(smt2_conv));
   }
@@ -314,8 +314,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory = true;
 
-    smt2_conv->set_message_handler(message_handler);
-
     set_prop_conv_time_limit(*smt2_conv);
     return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }

src/goto-instrument/accelerate/scratch_program.h

@@ -41,7 +41,7 @@ class scratch_programt:public goto_programt
       symbol_table(_symbol_table),
       symex_symbol_table(),
       ns(symbol_table, symex_symbol_table),
-      equation(),
+      equation(mh),
       path_storage(),
       options(get_default_options()),
       symex(mh, symbol_table, equation, options, path_storage),

src/goto-symex/symex_target_equation.cpp

@@ -359,12 +359,10 @@ void symex_target_equationt::convert_assignments(
   {
     if(step.is_assignment() && !step.ignore && !step.converted)
     {
-      decision_procedure.conditional_output(
-        decision_procedure.debug(),
-        [&step](messaget::mstreamt &mstream) {
-          step.output(mstream);
-          mstream << messaget::eom;
-        });
+      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
+        step.output(mstream);
+        mstream << messaget::eom;
+      });
 
       decision_procedure.set_to_true(step.cond_expr);
       step.converted = true;
@@ -404,12 +402,10 @@ void symex_target_equationt::convert_guards(
       step.guard_literal=const_literal(false);
     else
     {
-      prop_conv.conditional_output(
-        prop_conv.debug(),
-        [&step](messaget::mstreamt &mstream) {
-          step.output(mstream);
-          mstream << messaget::eom;
-        });
+      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
+        step.output(mstream);
+        mstream << messaget::eom;
+      });
 
       try
       {
@@ -436,9 +432,8 @@ void symex_target_equationt::convert_assumptions(
         step.cond_literal=const_literal(true);
       else
       {
-        prop_conv.conditional_output(
-          prop_conv.debug(),
-          [&step](messaget::mstreamt &mstream) {
+        log.conditional_output(
+          log.debug(), [&step](messaget::mstreamt &mstream) {
             step.output(mstream);
             mstream << messaget::eom;
           });
@@ -469,9 +464,8 @@ void symex_target_equationt::convert_goto_instructions(
         step.cond_literal=const_literal(true);
       else
       {
-        prop_conv.conditional_output(
-          prop_conv.debug(),
-          [&step](messaget::mstreamt &mstream) {
+        log.conditional_output(
+          log.debug(), [&step](messaget::mstreamt &mstream) {
             step.output(mstream);
             mstream << messaget::eom;
           });
@@ -498,11 +492,10 @@ void symex_target_equationt::convert_constraints(
   {
     if(step.is_constraint() && !step.ignore && !step.converted)
     {
-      decision_procedure.conditional_output(
-        decision_procedure.debug(), [&step](messaget::mstreamt &mstream) {
-          step.output(mstream);
-          mstream << messaget::eom;
-        });
+      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
+        step.output(mstream);
+        mstream << messaget::eom;
+      });
 
       try
       {
@@ -568,12 +561,10 @@ void symex_target_equationt::convert_assertions(
     {
       step.converted = true;
 
-      prop_conv.conditional_output(
-        prop_conv.debug(),
-        [&step](messaget::mstreamt &mstream) {
-          step.output(mstream);
-          mstream << messaget::eom;
-        });
+      log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
+        step.output(mstream);
+        mstream << messaget::eom;
+      });
 
       implies_exprt implication(
         assumption,

src/goto-symex/symex_target_equation.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 #include <util/merge_irep.h>
+#include <util/message.h>
 #include <util/narrow.h>
 
 #include <goto-programs/goto_program.h>
@@ -37,6 +38,11 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
+  explicit symex_target_equationt(message_handlert &message_handler)
+    : log(message_handler)
+  {
+  }
+
   virtual ~symex_target_equationt() = default;
 
   /// \copydoc symex_targett::shared_read()
@@ -408,6 +414,8 @@ class symex_target_equationt:public symex_targett
   }
 
 protected:
+  messaget log;
+
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
   void merge_ireps(SSA_stept &SSA_step);

src/solvers/prop/prop_conv.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/decision_procedure.h>
 #include <util/expr.h>
+#include <util/message.h>
 #include <util/std_expr.h>
 
 #include "literal.h"
@@ -67,7 +68,7 @@ class prop_convt:public decision_proceduret
 
 /*! \brief TO_BE_DOCUMENTED
 */
-class prop_conv_solvert:public prop_convt
+class prop_conv_solvert : public prop_convt, public messaget
 {
 public:
   explicit prop_conv_solvert(propt &_prop) : prop(_prop)

src/solvers/smt2/smt2_dec.h

@@ -22,7 +22,9 @@ class smt2_stringstreamt
 
 /*! \brief Decision procedure interface for various SMT 2.x solvers
 */
-class smt2_dect:protected smt2_stringstreamt, public smt2_convt
+class smt2_dect : protected smt2_stringstreamt,
+                  public smt2_convt,
+                  public messaget
 {
 public:
   smt2_dect(

src/util/decision_procedure.h

@@ -12,11 +12,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_DECISION_PROCEDURE_H
 #define CPROVER_UTIL_DECISION_PROCEDURE_H
 
-#include "message.h"
+#include <iosfwd>
+#include <string>
 
 class exprt;
 
-class decision_proceduret:public messaget
+class decision_proceduret
 {
 public:
   virtual ~decision_proceduret();

unit/goto-symex/ssa_equation.cpp

@@ -6,6 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
@@ -27,7 +28,7 @@ SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
 
     goto_programt goto_program;
     goto_program.add_instruction(END_FUNCTION);
-    symex_target_equationt equation;
+    symex_target_equationt equation(null_message_handler);
     symex_targett::sourcet at_end_function(fun_name, goto_program);
     equation.SSA_steps.emplace_back(
       at_end_function, goto_trace_stept::typet::FUNCTION_RETURN);