Merge pull request #5586 from tautschnig/messaget-partial_order_concurrency

partial_order_concurrencyt isn't a messaget

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -330,8 +330,7 @@ void postprocess_equation(
   {
     std::unique_ptr<memory_model_baset> memory_model =
       get_memory_model(options, ns);
-    memory_model->set_message_handler(ui_message_handler);
-    (*memory_model)(equation);
+    (*memory_model)(equation, ui_message_handler);
   }
 
   messaget log(ui_message_handler);

src/goto-symex/memory_model.h

@@ -20,7 +20,7 @@ class memory_model_baset : public partial_order_concurrencyt
   explicit memory_model_baset(const namespacet &_ns);
   virtual ~memory_model_baset();
 
-  virtual void operator()(symex_target_equationt &) = 0;
+  virtual void operator()(symex_target_equationt &, message_handlert &) = 0;
 
 protected:
   /// In-thread program order

src/goto-symex/memory_model_pso.cpp

@@ -11,11 +11,13 @@ Author: Michael Tautschnig, [email protected]
 
 #include "memory_model_pso.h"
 
-void memory_model_psot::operator()(symex_target_equationt &equation)
+void memory_model_psot::
+operator()(symex_target_equationt &equation, message_handlert &message_handler)
 {
-  statistics() << "Adding PSO constraints" << eom;
+  messaget log{message_handler};
+  log.statistics() << "Adding PSO constraints" << messaget::eom;
 
-  build_event_lists(equation);
+  build_event_lists(equation, message_handler);
   build_clock_type();
 
   read_from(equation);

src/goto-symex/memory_model_pso.h

@@ -22,7 +22,7 @@ class memory_model_psot:public memory_model_tsot
   {
   }
 
-  virtual void operator()(symex_target_equationt &equation);
+  virtual void operator()(symex_target_equationt &equation, message_handlert &);
 
 protected:
   virtual bool program_order_is_relaxed(

src/goto-symex/memory_model_sc.cpp

@@ -13,11 +13,13 @@ Author: Michael Tautschnig, [email protected]
 
 #include <util/std_expr.h>
 
-void memory_model_sct::operator()(symex_target_equationt &equation)
+void memory_model_sct::
+operator()(symex_target_equationt &equation, message_handlert &message_handler)
 {
-  statistics() << "Adding SC constraints" << eom;
+  messaget log{message_handler};
+  log.statistics() << "Adding SC constraints" << messaget::eom;
 
-  build_event_lists(equation);
+  build_event_lists(equation, message_handler);
   build_clock_type();
 
   read_from(equation);

src/goto-symex/memory_model_sc.h

@@ -22,7 +22,7 @@ class memory_model_sct:public memory_model_baset
   {
   }
 
-  virtual void operator()(symex_target_equationt &equation);
+  virtual void operator()(symex_target_equationt &equation, message_handlert &);
 
 protected:
   virtual exprt before(event_it e1, event_it e2);

src/goto-symex/memory_model_tso.cpp

@@ -14,11 +14,13 @@ Author: Michael Tautschnig, [email protected]
 #include <util/std_expr.h>
 #include <util/simplify_expr.h>
 
-void memory_model_tsot::operator()(symex_target_equationt &equation)
+void memory_model_tsot::
+operator()(symex_target_equationt &equation, message_handlert &message_handler)
 {
-  statistics() << "Adding TSO constraints" << eom;
+  messaget log{message_handler};
+  log.statistics() << "Adding TSO constraints" << messaget::eom;
 
-  build_event_lists(equation);
+  build_event_lists(equation, message_handler);
   build_clock_type();
 
   read_from(equation);

src/goto-symex/memory_model_tso.h

@@ -22,7 +22,7 @@ class memory_model_tsot:public memory_model_sct
   {
   }
 
-  virtual void operator()(symex_target_equationt &equation);
+  virtual void operator()(symex_target_equationt &equation, message_handlert &);
 
 protected:
   virtual exprt before(event_it e1, event_it e2);

src/goto-symex/partial_order_concurrency.cpp

@@ -73,7 +73,8 @@ void partial_order_concurrencyt::add_init_writes(
 }
 
 void partial_order_concurrencyt::build_event_lists(
-  symex_target_equationt &equation)
+  symex_target_equationt &equation,
+  message_handlert &message_handler)
 {
   add_init_writes(equation);
 
@@ -107,6 +108,7 @@ void partial_order_concurrencyt::build_event_lists(
     }
   }
 
+  messaget log{message_handler};
   for(address_mapt::const_iterator
       a_it=address_map.begin();
       a_it!=address_map.end();
@@ -116,9 +118,8 @@ void partial_order_concurrencyt::build_event_lists(
     if(a_rec.reads.empty())
       continue;
 
-    statistics() << "Shared " << a_it->first << ": "
-                 << a_rec.reads.size() << "R/"
-                 << a_rec.writes.size() << "W" << eom;
+    log.statistics() << "Shared " << a_it->first << ": " << a_rec.reads.size()
+                     << "R/" << a_rec.writes.size() << "W" << messaget::eom;
   }
 }
 

src/goto-symex/partial_order_concurrency.h

@@ -12,14 +12,12 @@ Author: Michael Tautschnig, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
 #define CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
 
-#include <util/message.h>
-
 #include "symex_target_equation.h"
 
 /// Base class for implementing memory models via additional constraints for
 /// SSA equations. Provides methods for encoding ordering of shared read/write
 /// events.
-class partial_order_concurrencyt:public messaget
+class partial_order_concurrencyt
 {
 public:
   explicit partial_order_concurrencyt(const namespacet &_ns);
@@ -67,7 +65,10 @@ class partial_order_concurrencyt:public messaget
   /// 2) the _numbering_ map (with per-thread unique number of every event)
   /// \param equation: the target equation (containing the events to be
   ///   processed)
-  void build_event_lists(symex_target_equationt &);
+  /// \param message_handler: message handler to output statistics
+  void build_event_lists(
+    symex_target_equationt &equation,
+    message_handlert &message_handler);
 
   /// For each shared read event and for each shared write event that appears
   /// after spawn or has false _guard_ prepend a shared write SSA step with