Add a message_handler parameter to ai_baset in preparation for logging

The legacy ait interface is preserved by creating a local
null_message_handlert and then passing this as a reference to the parent
constructor.  This is not ideal but does preserve behaviour.

Author: martin

src/analyses/ai.h

@@ -51,6 +51,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/deprecate.h>
 #include <util/json.h>
 #include <util/make_unique.h>
+#include <util/message.h>
 #include <util/xml.h>
 
 #include <goto-programs/goto_model.h>
@@ -127,10 +128,12 @@ class ai_baset
   ai_baset(
     std::unique_ptr<ai_history_factory_baset> &&hf,
     std::unique_ptr<ai_domain_factory_baset> &&df,
-    std::unique_ptr<ai_storage_baset> &&st)
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
     : history_factory(std::move(hf)),
       domain_factory(std::move(df)),
-      storage(std::move(st))
+      storage(std::move(st)),
+      message_handler(mh)
   {
   }
 
@@ -515,6 +518,9 @@ class ai_baset
   {
     return storage->get_state(p, *domain_factory);
   }
+
+  // Logging
+  message_handlert &message_handler;
 };
 
 // Perform interprocedural analysis by simply recursing in the interpreter
@@ -525,8 +531,9 @@ class ai_recursive_interproceduralt : public ai_baset
   ai_recursive_interproceduralt(
     std::unique_ptr<ai_history_factory_baset> &&hf,
     std::unique_ptr<ai_domain_factory_baset> &&df,
-    std::unique_ptr<ai_storage_baset> &&st)
-    : ai_baset(std::move(hf), std::move(df), std::move(st))
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
+    : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
   {
   }
 
@@ -562,7 +569,8 @@ class ait : public ai_recursive_interproceduralt
         util_make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
         util_make_unique<ai_domain_factory_default_constructort<domainT>>(),
-        util_make_unique<location_sensitive_storaget>())
+        util_make_unique<location_sensitive_storaget>(),
+        no_logging)
   {
   }
 
@@ -571,7 +579,8 @@ class ait : public ai_recursive_interproceduralt
         util_make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
         std::move(df),
-        util_make_unique<location_sensitive_storaget>())
+        util_make_unique<location_sensitive_storaget>(),
+        no_logging)
   {
   }
 
@@ -613,6 +622,9 @@ class ait : public ai_recursive_interproceduralt
   /// This function exists to enforce that `domainT` is derived from
   /// \ref ai_domain_baset
   void dummy(const domainT &s) { const statet &x=s; (void)x; }
+
+  // To keep the old constructor interface we disable logging
+  null_message_handlert no_logging;
 };
 
 /// Base class for concurrency-aware abstract interpretation. See

src/analyses/variable-sensitivity/three_way_merge_abstract_interpreter.h

@@ -30,8 +30,13 @@ class ai_three_way_merget : public ai_recursive_interproceduralt
   ai_three_way_merget(
     std::unique_ptr<ai_history_factory_baset> &&hf,
     std::unique_ptr<ai_domain_factory_baset> &&df,
-    std::unique_ptr<ai_storage_baset> &&st)
-    : ai_recursive_interproceduralt(std::move(hf), std::move(df), std::move(st))
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
+    : ai_recursive_interproceduralt(
+        std::move(hf),
+        std::move(df),
+        std::move(st),
+        mh)
   {
   }
 

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

@@ -641,14 +641,16 @@ variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht(
   const goto_functionst &goto_functions,
   const namespacet &_ns,
   variable_sensitivity_object_factory_ptrt object_factory,
-  const vsd_configt &configuration)
+  const vsd_configt &configuration,
+  message_handlert &message_handler)
   : ai_three_way_merget(
       util_make_unique<ai_history_factory_default_constructort<ahistoricalt>>(),
       util_make_unique<variable_sensitivity_dependence_domain_factoryt>(
         *this,
         object_factory,
         configuration),
-      util_make_unique<location_sensitive_storaget>()),
+      util_make_unique<location_sensitive_storaget>(),
+      message_handler),
     goto_functions(goto_functions),
     ns(_ns)
 {

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h

@@ -244,7 +244,8 @@ class variable_sensitivity_dependence_grapht : public ai_three_way_merget,
     const goto_functionst &goto_functions,
     const namespacet &_ns,
     variable_sensitivity_object_factory_ptrt object_factory,
-    const vsd_configt &_configuration);
+    const vsd_configt &_configuration,
+    message_handlert &message_handler);
 
   void
   initialize(const irep_idt &function_id, const goto_programt &goto_program)

src/goto-analyzer/build_analyzer.cpp

@@ -22,14 +22,16 @@ Author: Martin Brain, [email protected]
 
 #include <goto-programs/goto_model.h>
 
+#include <util/message.h>
 #include <util/options.h>
 
 /// Ideally this should be a pure function of options.
 /// However at the moment some domains require the goto_model or parts of it
 std::unique_ptr<ai_baset> build_analyzer(
   const optionst &options,
   const goto_modelt &goto_model,
-  const namespacet &ns)
+  const namespacet &ns,
+  message_handlert &mh)
 {
   auto vsd_config = vsd_configt::from_options(options);
   auto vs_object_factory =
@@ -99,15 +101,15 @@ std::unique_ptr<ai_baset> build_analyzer(
       if(options.get_bool_option("recursive-interprocedural"))
       {
         return util_make_unique<ai_recursive_interproceduralt>(
-          std::move(hf), std::move(df), std::move(st));
+          std::move(hf), std::move(df), std::move(st), mh);
       }
       else if(options.get_bool_option("three-way-merge"))
       {
         // Only works with VSD
         if(options.get_bool_option("vsd"))
         {
           return util_make_unique<ai_three_way_merget>(
-            std::move(hf), std::move(df), std::move(st));
+            std::move(hf), std::move(df), std::move(st), mh);
         }
       }
     }
@@ -127,7 +129,7 @@ std::unique_ptr<ai_baset> build_analyzer(
     else if(options.get_bool_option("dependence-graph-vs"))
     {
       return util_make_unique<variable_sensitivity_dependence_grapht>(
-        goto_model.goto_functions, ns, vs_object_factory, vsd_config);
+        goto_model.goto_functions, ns, vs_object_factory, vsd_config, mh);
     }
     else if(options.get_bool_option("vsd"))
     {

src/goto-analyzer/build_analyzer.h

@@ -15,6 +15,7 @@ class ai_baset;
 class goto_modelt;
 class namespacet;
 class optionst;
+class message_handlert;
 
 /// Build an abstract interpreter configured by the options.
 /// This may require options for:
@@ -29,6 +30,7 @@ class optionst;
 std::unique_ptr<ai_baset> build_analyzer(
   const optionst &options,
   const goto_modelt &goto_model,
-  const namespacet &ns);
+  const namespacet &ns,
+  message_handlert &mh);
 
 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -568,7 +568,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     try
     {
-      analyzer = build_analyzer(options, goto_model, ns);
+      analyzer = build_analyzer(options, goto_model, ns, ui_message_handler);
     }
     catch(const invalid_command_line_argument_exceptiont &e)
     {