Merge pull request #1625 from karkhaz/kk-symext-is-messaget

Make goto_symext a subtype of messaget

Author: tautschnig

src/cbmc/bmc.cpp

@@ -340,7 +340,6 @@ void bmct::get_memory_model()
 void bmct::setup()
 {
   get_memory_model();
-  symex.set_message_handler(get_message_handler());
   symex.options=options;
 
   {

src/cbmc/bmc.h

@@ -38,14 +38,14 @@ class bmct:public safety_checkert
     const optionst &_options,
     const symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    prop_convt &_prop_conv):
-    safety_checkert(ns, _message_handler),
-    options(_options),
-    ns(_symbol_table, new_symbol_table),
-    equation(ns),
-    symex(ns, new_symbol_table, equation),
-    prop_conv(_prop_conv),
-    ui(ui_message_handlert::uit::PLAIN)
+    prop_convt &_prop_conv)
+    : safety_checkert(ns, _message_handler),
+      options(_options),
+      ns(_symbol_table, new_symbol_table),
+      equation(ns),
+      symex(_message_handler, ns, new_symbol_table, equation),
+      prop_conv(_prop_conv),
+      ui(ui_message_handlert::uit::PLAIN)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=

src/cbmc/symex_bmc.cpp

@@ -17,14 +17,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 
 symex_bmct::symex_bmct(
+  message_handlert &mh,
   const namespacet &_ns,
   symbol_tablet &_new_symbol_table,
-  symex_targett &_target):
-  goto_symext(_ns, _new_symbol_table, _target),
-  record_coverage(false),
-  max_unwind(0),
-  max_unwind_is_set(false),
-  symex_coverage(_ns)
+  symex_targett &_target)
+  : goto_symext(mh, _ns, _new_symbol_table, _target),
+    record_coverage(false),
+    max_unwind(0),
+    max_unwind_is_set(false),
+    symex_coverage(_ns)
 {
 }
 
@@ -37,10 +38,9 @@ void symex_bmct::symex_step(
 
   if(!source_location.is_nil() && last_source_location!=source_location)
   {
-    debug() << "BMC at file " << source_location.get_file()
-            << " line " << source_location.get_line()
-            << " function " << source_location.get_function()
-            << eom;
+    log.debug() << "BMC at file " << source_location.get_file() << " line "
+                << source_location.get_line() << " function "
+                << source_location.get_function() << log.eom;
 
     last_source_location=source_location;
   }
@@ -52,15 +52,15 @@ void symex_bmct::symex_step(
      state.source.pc->is_assume() &&
      simplify_expr(state.source.pc->guard, ns).is_false())
   {
-    statistics() << "aborting path on assume(false) at "
-                 << state.source.pc->source_location
-                 << " thread " << state.source.thread_nr;
+    log.statistics() << "aborting path on assume(false) at "
+                     << state.source.pc->source_location << " thread "
+                     << state.source.thread_nr;
 
     const irep_idt &c=state.source.pc->source_location.get_comment();
     if(!c.empty())
-      statistics() << ": " << c;
+      log.statistics() << ": " << c;
 
-    statistics() << eom;
+    log.statistics() << log.eom;
   }
 
   goto_symext::symex_step(goto_functions, state);
@@ -94,7 +94,7 @@ void symex_bmct::merge_goto(
 
   goto_symext::merge_goto(goto_state, state);
 
-  assert(prev_pc->is_goto());
+  PRECONDITION(prev_pc->is_goto());
   if(record_coverage &&
      // could the branch possibly be taken?
      !prev_guard.is_false() &&
@@ -132,15 +132,14 @@ bool symex_bmct::get_unwind(
 
   bool abort=unwind>=this_loop_limit;
 
-  statistics() << (abort?"Not unwinding":"Unwinding")
-               << " loop " << id << " iteration "
-               << unwind;
+  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
+                   << " iteration " << unwind;
 
   if(this_loop_limit!=std::numeric_limits<unsigned>::max())
-    statistics() << " (" << this_loop_limit << " max)";
+    log.statistics() << " (" << this_loop_limit << " max)";
 
-  statistics() << " " << source.pc->source_location
-               << " thread " << source.thread_nr << eom;
+  log.statistics() << " " << source.pc->source_location << " thread "
+                   << source.thread_nr << log.eom;
 
   return abort;
 }
@@ -176,15 +175,13 @@ bool symex_bmct::get_unwind_recursion(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    statistics() << (abort?"Not unwinding":"Unwinding")
-                 << " recursion "
-                 << symbol.display_name()
-                 << " iteration " << unwind;
+    log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
+                     << symbol.display_name() << " iteration " << unwind;
 
     if(this_loop_limit!=std::numeric_limits<unsigned>::max())
-      statistics() << " (" << this_loop_limit << " max)";
+      log.statistics() << " (" << this_loop_limit << " max)";
 
-    statistics() << eom;
+    log.statistics() << log.eom;
   }
 
   return abort;
@@ -194,7 +191,7 @@ void symex_bmct::no_body(const irep_idt &identifier)
 {
   if(body_warnings.insert(identifier).second)
   {
-    warning() <<
-      "**** WARNING: no body for function " << identifier << eom;
+    log.warning() << "**** WARNING: no body for function " << identifier
+                  << log.eom;
   }
 }

src/cbmc/symex_bmc.h

@@ -18,12 +18,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_coverage.h"
 
-class symex_bmct:
-  public goto_symext,
-  public messaget
+class symex_bmct: public goto_symext
 {
 public:
   symex_bmct(
+    message_handlert &mh,
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     symex_targett &_target);

src/goto-instrument/accelerate/accelerate.cpp

@@ -109,14 +109,14 @@ int acceleratet::accelerate_loop(goto_programt::targett &loop_header)
   program.update();
 
 #if 1
-  enumerating_loop_accelerationt
-    acceleration(
-      symbol_table,
-      goto_functions,
-      program,
-      loop,
-      loop_header,
-      accelerate_limit);
+  enumerating_loop_accelerationt acceleration(
+    message_handler,
+    symbol_table,
+    goto_functions,
+    program,
+    loop,
+    loop_header,
+    accelerate_limit);
 #else
   disjunctive_polynomial_accelerationt
     acceleration(symbol_table, goto_functions, program, loop, loop_header);
@@ -333,7 +333,7 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator)
 
     if(jt==dirty_vars_map.end())
     {
-      scratch_programt scratch(symbol_table);
+      scratch_programt scratch(symbol_table, message_handler);
       symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
       dirty_var=new_sym.symbol_expr();
       dirty_vars_map[*it]=dirty_var;
@@ -512,7 +512,7 @@ void acceleratet::insert_automaton(trace_automatont &automaton)
   // machine.
   for(const auto &sym : automaton.alphabet)
   {
-    scratch_programt state_machine(symbol_table);
+    scratch_programt state_machine(symbol_table, message_handler);
     trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
 
     build_state_machine(p.first, p.second, accept_states, state, next_state,
@@ -648,15 +648,16 @@ int acceleratet::accelerate_loops()
   return num_accelerated;
 }
 
-
 void accelerate_functions(
   goto_modelt &goto_model,
+  message_handlert &message_handler,
   bool use_z3)
 {
   Forall_goto_functions(it, goto_model.goto_functions)
   {
     std::cout << "Accelerating function " << it->first << '\n';
-    acceleratet accelerate(it->second.body, goto_model, use_z3);
+    acceleratet accelerate(
+      it->second.body, goto_model, message_handler, use_z3);
 
     int num_accelerated=accelerate.accelerate_loops();
 

src/goto-instrument/accelerate/accelerate.h

@@ -14,6 +14,7 @@ Author: Matt Lewis
 
 #include <util/namespace.h>
 #include <util/expr.h>
+#include <util/message.h>
 
 #include <analyses/natural_loops.h>
 
@@ -28,15 +29,18 @@ Author: Matt Lewis
 
 class acceleratet
 {
- public:
-  acceleratet(goto_programt &_program,
-              goto_modelt &_goto_model,
-              bool _use_z3):
+public:
+  acceleratet(
+    goto_programt &_program,
+    goto_modelt &_goto_model,
+    message_handlert &message_handler,
+    bool _use_z3)
+    : message_handler(message_handler),
       program(_program),
       goto_functions(_goto_model.goto_functions),
       symbol_table(_goto_model.symbol_table),
       ns(_goto_model.symbol_table),
-      utils(symbol_table, goto_functions),
+      utils(symbol_table, message_handler, goto_functions),
       use_z3(_use_z3)
   {
     natural_loops(program);
@@ -51,46 +55,54 @@ class acceleratet
 
   static const int accelerate_limit = -1;
 
- protected:
-  void find_paths(goto_programt::targett &loop_header,
-                  pathst &loop_paths,
-                  pathst &exit_paths,
-                  goto_programt::targett &back_jump);
+protected:
+  message_handlert &message_handler;
 
-  void extend_path(goto_programt::targett &t,
-                   goto_programt::targett &loop_header,
-                   natural_loops_mutablet::natural_loopt &loop,
-                   patht &prefix,
-                   pathst &loop_paths,
-                   pathst &exit_paths,
-                   goto_programt::targett &back_jump);
+  void find_paths(
+    goto_programt::targett &loop_header,
+    pathst &loop_paths,
+    pathst &exit_paths,
+    goto_programt::targett &back_jump);
+
+  void extend_path(
+    goto_programt::targett &t,
+    goto_programt::targett &loop_header,
+    natural_loops_mutablet::natural_loopt &loop,
+    patht &prefix,
+    pathst &loop_paths,
+    pathst &exit_paths,
+    goto_programt::targett &back_jump);
 
   goto_programt::targett find_back_jump(goto_programt::targett loop_header);
 
-  void insert_looping_path(goto_programt::targett &loop_header,
-                           goto_programt::targett &back_jump,
-                           goto_programt &looping_path,
-                           patht &inserted_path);
-  void insert_accelerator(goto_programt::targett &loop_header,
-                          goto_programt::targett &back_jump,
-                          path_acceleratort &accelerator,
-                          subsumed_patht &subsumed);
+  void insert_looping_path(
+    goto_programt::targett &loop_header,
+    goto_programt::targett &back_jump,
+    goto_programt &looping_path,
+    patht &inserted_path);
+  void insert_accelerator(
+    goto_programt::targett &loop_header,
+    goto_programt::targett &back_jump,
+    path_acceleratort &accelerator,
+    subsumed_patht &subsumed);
 
   void set_dirty_vars(path_acceleratort &accelerator);
   void add_dirty_checks();
   bool is_underapproximate(path_acceleratort &accelerator);
 
-  void make_overflow_loc(goto_programt::targett loop_header,
-                         goto_programt::targett &loop_end,
-                         goto_programt::targett &overflow_loc);
+  void make_overflow_loc(
+    goto_programt::targett loop_header,
+    goto_programt::targett &loop_end,
+    goto_programt::targett &overflow_loc);
 
   void insert_automaton(trace_automatont &automaton);
-  void build_state_machine(trace_automatont::sym_mapt::iterator p,
-                           trace_automatont::sym_mapt::iterator end,
-                           state_sett &accept_states,
-                           symbol_exprt state,
-                           symbol_exprt next_state,
-                           scratch_programt &state_machine);
+  void build_state_machine(
+    trace_automatont::sym_mapt::iterator p,
+    trace_automatont::sym_mapt::iterator end,
+    state_sett &accept_states,
+    symbol_exprt state,
+    symbol_exprt next_state,
+    scratch_programt &state_machine);
 
   symbolt make_symbol(std::string name, typet type);
   void decl(symbol_exprt &sym, goto_programt::targett t);
@@ -117,6 +129,7 @@ class acceleratet
 
 void accelerate_functions(
   goto_modelt &,
+  message_handlert &message_handler,
   bool use_z3);
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -128,7 +128,7 @@ bool acceleration_utilst::check_inductive(
   // assert (target1==polynomial1);
   // assert (target2==polynomial2);
   // ...
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   std::vector<exprt> polynomials_hold;
   substitutiont substitution;
 
@@ -386,7 +386,7 @@ bool acceleration_utilst::do_assumptions(
   // assert(!precondition);
 
   exprt condition=precondition(path);
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   substitutiont substitution;
   stash_polynomials(program, polynomials, substitution, path);