Merge pull request #8100 from tautschnig/cleanup/dereference-messaget

Remove default messaget value from goto_program_dereferencet

Author: tautschnig

doc/architectural/goto-program-transformations.md

@@ -310,6 +310,7 @@ line options. The reachability slicer is enabled by the `--reachability-slice`
 command line option. The implementation of this pass is called via the \ref
 reachability_slicer(goto_modelt &, message_handlert &) function. The full slicer
 is enabled by the `--full-slice` command line option. The implementation of this
-pass is called via the \ref full_slicer(goto_modelt &) function.
+pass is called via the \ref full_slicer(goto_modelt &, message_handlert &)
+function.
 
 <em>Predecessor pass is \ref properties-transform .</em>

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -276,7 +276,7 @@ ai_baset *janalyzer_parse_optionst::build_analyzer(
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      domain = new dependence_grapht(ns);
+      domain = new dependence_grapht(ns, ui_message_handler);
     }
     else if(options.get_bool_option("intervals"))
     {

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -897,9 +897,10 @@ bool jbmc_parse_optionst::process_goto_functions(
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
-      property_slicer(goto_model, cmdline.get_values("property"));
+      property_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
     else
-      full_slicer(goto_model);
+      full_slicer(goto_model, ui_message_handler);
   }
 
   // remove any skips introduced

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -144,7 +144,11 @@ int jdiff_parse_optionst::doit()
         : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
                                             : impact_modet::BOTH);
     change_impact(
-      goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
+      goto_model1,
+      goto_model2,
+      impact_mode,
+      cmdline.isset("compact-output"),
+      ui_message_handler);
 
     return CPROVER_EXIT_SUCCESS;
   }

src/analyses/dependence_graph.cpp

@@ -164,7 +164,7 @@ void dep_graph_domaint::data_dependencies(
   // TODO use (future) reaching-definitions-dereferencing rw_set
   value_setst &value_sets=
     dep_graph.reaching_definitions().get_value_sets();
-  rw_range_set_value_sett rw_set(ns, value_sets);
+  rw_range_set_value_sett rw_set(ns, value_sets, message_handler);
   goto_rw(function_to, to, rw_set);
 
   for(const auto &read_object_entry : rw_set.get_r_set())
@@ -341,28 +341,35 @@ jsont dep_graph_domaint::output_json(
 class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
 {
 public:
-  explicit dep_graph_domain_factoryt(dependence_grapht &_dg) : dg(_dg)
+  dep_graph_domain_factoryt(
+    dependence_grapht &_dg,
+    message_handlert &message_handler)
+    : dg(_dg), message_handler(message_handler)
   {
   }
 
   std::unique_ptr<statet> make(locationt l) const override
   {
     auto node_id = dg.add_node();
     dg.nodes[node_id].PC = l;
-    auto p = std::make_unique<dep_graph_domaint>(node_id);
+    auto p = std::make_unique<dep_graph_domaint>(node_id, message_handler);
     CHECK_RETURN(p->is_bottom());
 
     return std::unique_ptr<statet>(p.release());
   }
 
 private:
   dependence_grapht &dg;
+  message_handlert &message_handler;
 };
 
-dependence_grapht::dependence_grapht(const namespacet &_ns)
-  : ait<dep_graph_domaint>(std::make_unique<dep_graph_domain_factoryt>(*this)),
+dependence_grapht::dependence_grapht(
+  const namespacet &_ns,
+  message_handlert &message_handler)
+  : ait<dep_graph_domaint>(
+      std::make_unique<dep_graph_domain_factoryt>(*this, message_handler)),
     ns(_ns),
-    rd(ns)
+    rd(ns, message_handler)
 {
 }
 

src/analyses/dependence_graph.h

@@ -68,8 +68,11 @@ class dep_graph_domaint:public ai_domain_baset
 public:
   typedef grapht<dep_nodet>::node_indext node_indext;
 
-  explicit dep_graph_domaint(node_indext id)
-    : has_values(false), node_id(id), has_changed(false)
+  dep_graph_domaint(node_indext id, message_handlert &message_handler)
+    : has_values(false),
+      node_id(id),
+      has_changed(false),
+      message_handler(message_handler)
   {
   }
 
@@ -189,6 +192,8 @@ class dep_graph_domaint:public ai_domain_baset
   // location has a data dependency on
   depst data_deps;
 
+  message_handlert &message_handler;
+
   friend const depst &
     dependence_graph_test_get_control_deps(const dep_graph_domaint &);
   friend const depst &
@@ -220,7 +225,7 @@ class dependence_grapht:
 
   typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
 
-  explicit dependence_grapht(const namespacet &_ns);
+  dependence_grapht(const namespacet &_ns, message_handlert &);
 
   void initialize(const goto_functionst &goto_functions)
   {

src/analyses/goto_rw.cpp

@@ -682,7 +682,7 @@ void rw_range_set_value_sett::get_objects_dereference(
     size);
 
   exprt object=deref;
-  dereference(function, target, object, ns, value_sets);
+  dereference(function, target, object, ns, value_sets, message_handler);
 
   auto type_bits = pointer_offset_bits(object.type(), ns);
 

src/analyses/goto_rw.h

@@ -21,7 +21,7 @@ Date: April 2010
 #include <goto-programs/goto_program.h>
 
 class goto_functionst;
-
+class message_handlert;
 class rw_range_sett;
 
 void goto_rw(
@@ -212,8 +212,8 @@ class rw_range_sett
 
   virtual ~rw_range_sett();
 
-  explicit rw_range_sett(const namespacet &_ns):
-    ns(_ns)
+  rw_range_sett(const namespacet &_ns, message_handlert &message_handler)
+    : ns(_ns), message_handler(message_handler)
   {
   }
 
@@ -263,6 +263,7 @@ class rw_range_sett
 
 protected:
   const namespacet &ns;
+  message_handlert &message_handler;
 
   objectst r_range_set, w_range_set;
 
@@ -370,9 +371,9 @@ class rw_range_set_value_sett:public rw_range_sett
 public:
   rw_range_set_value_sett(
     const namespacet &_ns,
-    value_setst &_value_sets):
-    rw_range_sett(_ns),
-    value_sets(_value_sets)
+    value_setst &_value_sets,
+    message_handlert &message_handler)
+    : rw_range_sett(_ns, message_handler), value_sets(_value_sets)
   {
   }
 
@@ -463,8 +464,9 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
   rw_guarded_range_set_value_sett(
     const namespacet &_ns,
     value_setst &_value_sets,
-    guard_managert &guard_manager)
-    : rw_range_set_value_sett(_ns, _value_sets),
+    guard_managert &guard_manager,
+    message_handlert &message_handler)
+    : rw_range_set_value_sett(_ns, _value_sets, message_handler),
       guard_manager(guard_manager),
       guard(true_exprt(), guard_manager)
   {

src/analyses/reaching_definitions.cpp

@@ -32,27 +32,30 @@ class rd_range_domain_factoryt : public ai_domain_factoryt<rd_range_domaint>
 {
 public:
   rd_range_domain_factoryt(
-    sparse_bitvector_analysist<reaching_definitiont> *_bv_container)
-    : bv_container(_bv_container)
+    sparse_bitvector_analysist<reaching_definitiont> *_bv_container,
+    message_handlert &message_handler)
+    : bv_container(_bv_container), message_handler(message_handler)
   {
     PRECONDITION(bv_container != nullptr);
   }
 
   std::unique_ptr<statet> make(locationt) const override
   {
-    auto p = std::make_unique<rd_range_domaint>(bv_container);
+    auto p = std::make_unique<rd_range_domaint>(bv_container, message_handler);
     CHECK_RETURN(p->is_bottom());
     return std::unique_ptr<statet>(p.release());
   }
 
 private:
   sparse_bitvector_analysist<reaching_definitiont> *const bv_container;
+  message_handlert &message_handler;
 };
 
 reaching_definitions_analysist::reaching_definitions_analysist(
-  const namespacet &_ns)
+  const namespacet &_ns,
+  message_handlert &message_handler)
   : concurrency_aware_ait<rd_range_domaint>(
-      std::make_unique<rd_range_domain_factoryt>(this)),
+      std::make_unique<rd_range_domain_factoryt>(this, message_handler)),
     ns(_ns)
 {
 }
@@ -306,7 +309,7 @@ void rd_range_domaint::transform_assign(
   locationt to,
   reaching_definitions_analysist &rd)
 {
-  rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
+  rw_range_set_value_sett rw_set(ns, rd.get_value_sets(), message_handler);
   goto_rw(function_to, to, rw_set);
   const bool is_must_alias=rw_set.get_w_set().size()==1;
 

src/analyses/reaching_definitions.h

@@ -159,8 +159,12 @@ class rd_range_domaint:public ai_domain_baset
 {
 public:
   rd_range_domaint(
-    sparse_bitvector_analysist<reaching_definitiont> *_bv_container)
-    : ai_domain_baset(), has_values(false), bv_container(_bv_container)
+    sparse_bitvector_analysist<reaching_definitiont> *_bv_container,
+    message_handlert &message_handler)
+    : ai_domain_baset(),
+      has_values(false),
+      bv_container(_bv_container),
+      message_handler(message_handler)
   {
     PRECONDITION(bv_container != nullptr);
   }
@@ -346,6 +350,8 @@ class rd_range_domaint:public ai_domain_baset
   bool merge_inner(
     values_innert &dest,
     const values_innert &other);
+
+  message_handlert &message_handler;
 };
 
 class reaching_definitions_analysist:
@@ -354,7 +360,7 @@ class reaching_definitions_analysist:
 {
 public:
   // constructor
-  explicit reaching_definitions_analysist(const namespacet &_ns);
+  reaching_definitions_analysist(const namespacet &_ns, message_handlert &);
 
   virtual ~reaching_definitions_analysist();
 

src/cbmc/cbmc_parse_options.cpp

@@ -940,9 +940,12 @@ bool cbmc_parse_optionst::process_goto_program(
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(options.is_set("property"))
-      property_slicer(goto_model, options.get_list_option("property"));
+      property_slicer(
+        goto_model,
+        options.get_list_option("property"),
+        log.get_message_handler());
     else
-      full_slicer(goto_model);
+      full_slicer(goto_model, log.get_message_handler());
   }
 
   // remove any skips introduced since coverage instrumentation

src/goto-analyzer/build_analyzer.cpp

@@ -123,7 +123,7 @@ std::unique_ptr<ai_baset> build_analyzer(
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      return std::make_unique<dependence_grapht>(ns);
+      return std::make_unique<dependence_grapht>(ns, mh);
     }
     else if(options.get_bool_option("dependence-graph-vs"))
     {

src/goto-diff/change_impact.cpp

@@ -207,7 +207,8 @@ class change_impactt
     const goto_modelt &model_old,
     const goto_modelt &model_new,
     impact_modet impact_mode,
-    bool compact_output);
+    bool compact_output,
+    message_handlert &message_handler);
 
   void operator()();
 
@@ -289,19 +290,20 @@ class change_impactt
 };
 
 change_impactt::change_impactt(
-    const goto_modelt &model_old,
-    const goto_modelt &model_new,
-    impact_modet _impact_mode,
-    bool _compact_output):
-  impact_mode(_impact_mode),
-  compact_output(_compact_output),
-  old_goto_functions(model_old.goto_functions),
-  ns_old(model_old.symbol_table),
-  new_goto_functions(model_new.goto_functions),
-  ns_new(model_new.symbol_table),
-  unified_diff(model_old, model_new),
-  old_dep_graph(ns_old),
-  new_dep_graph(ns_new)
+  const goto_modelt &model_old,
+  const goto_modelt &model_new,
+  impact_modet _impact_mode,
+  bool _compact_output,
+  message_handlert &message_handler)
+  : impact_mode(_impact_mode),
+    compact_output(_compact_output),
+    old_goto_functions(model_old.goto_functions),
+    ns_old(model_old.symbol_table),
+    new_goto_functions(model_new.goto_functions),
+    ns_new(model_new.symbol_table),
+    unified_diff(model_old, model_new),
+    old_dep_graph(ns_old, message_handler),
+    new_dep_graph(ns_new, message_handler)
 {
   // syntactic difference?
   if(!unified_diff())
@@ -757,8 +759,10 @@ void change_impact(
   const goto_modelt &model_old,
   const goto_modelt &model_new,
   impact_modet impact_mode,
-  bool compact_output)
+  bool compact_output,
+  message_handlert &message_handler)
 {
-  change_impactt c(model_old, model_new, impact_mode, compact_output);
+  change_impactt c(
+    model_old, model_new, impact_mode, compact_output, message_handler);
   c();
 }

src/goto-diff/change_impact.h

@@ -15,12 +15,14 @@ Date: April 2016
 #define CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
 
 class goto_modelt;
+class message_handlert;
 enum class impact_modet { FORWARD, BACKWARD, BOTH };
 
 void change_impact(
   const goto_modelt &model_old,
   const goto_modelt &model_new,
   impact_modet impact_mode,
-  bool compact_output);
+  bool compact_output,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_DIFF_CHANGE_IMPACT_H

src/goto-diff/goto_diff_parse_options.cpp

@@ -147,7 +147,8 @@ int goto_diff_parse_optionst::doit()
       goto_model1,
       goto_model2,
       impact_mode,
-      cmdline.isset("compact-output"));
+      cmdline.isset("compact-output"),
+      ui_message_handler);
 
     return CPROVER_EXIT_SUCCESS;
   }