Move ai configuration to separate config object

This lets us reuse the logic of getting the ait
configuration from command line options.

Also, this includes a small simplification
of the printing logic

Author: hannes-steffenhagen-diffblue

src/analyses/ai.cpp

@@ -369,7 +369,7 @@ bool ai_baset::visit(
       const code_function_callt &code=
         to_code_function_call(l->code);
 
-      if(periodic_task)
+      if(config.periodic_task)
       {
         goto_functionst::function_mapt::const_iterator f_it =
           goto_functions.function_map.find(goto_functionst::entry_point());
@@ -763,12 +763,40 @@ void ai_baset::print_progress_interval() const
   system_clock::time_point now = system_clock::now();
   auto diff = now - last_progress_output;
 
-  if(diff >= min_progress_interval)
+  if(config.print_progress && diff >= config.progress_interval)
   {
     print_progress();
     last_progress_output = now;
   }
 }
 
-ai_baset::null_streamt ai_baset::null_stream;
-std::ostream ai_baset::null_output_stream(&ai_baset::null_stream);
+ai_configt ai_configt::from_options(const optionst &options)
+{
+  ai_configt result = {};
+  result.print_progress = options.get_bool_option("vs-progress");
+  if(options.is_set("vs-progress-interval"))
+  {
+    result.progress_interval = ai_configt::secondst(
+      std::stof(options.get_option("vs-progress-interval")));
+  }
+  return result;
+}
+
+ai_configt &ai_configt::with_print_progress(bool print_progress)
+{
+  this->print_progress = print_progress;
+  return *this;
+}
+
+ai_configt &
+ai_configt::with_progress_interval(ai_configt::secondst progress_interval)
+{
+  this->progress_interval = progress_interval;
+  return *this;
+}
+
+ai_configt &ai_configt::with_periodic_task(bool periodic_task)
+{
+  this->periodic_task = periodic_task;
+  return *this;
+}

src/analyses/ai.h

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/make_unique.h>
 
 #include <goto-programs/goto_model.h>
+#include <util/options.h>
 
 // forward reference
 class ai_baset;
@@ -139,6 +140,19 @@ class ai_domain_baset
 
 };
 
+struct ai_configt
+{
+  using secondst = std::chrono::duration<float>;
+  bool print_progress = false;
+  secondst progress_interval = secondst(0.0f);
+  bool periodic_task = false;
+
+  ai_configt &with_print_progress(bool print_progress);
+  ai_configt &with_progress_interval(secondst progress_interval);
+  ai_configt &with_periodic_task(bool periodic_task);
+  static ai_configt from_options(const optionst &);
+};
+
 // don't use me -- I am just a base class
 // use ait instead
 class ai_baset
@@ -147,14 +161,9 @@ class ai_baset
   typedef ai_domain_baset statet;
   typedef goto_programt::const_targett locationt;
 
-  ai_baset(
-    const bool print_progress,
-    const float min_progress_interval,
-    const bool periodic_task) :
-      progress_output_stream(print_progress ? std::cout : null_output_stream),
-      min_progress_interval(min_progress_interval),
-      periodic_task(periodic_task)
+  ai_baset(ai_configt config) : config(config)
   {
+    last_progress_output = std::chrono::system_clock::now();
   }
 
   virtual ~ai_baset()
@@ -298,20 +307,12 @@ class ai_baset
     return output_xml(ns, goto_function.body, "");
   }
 
-private:
-  class null_streamt : public std::streambuf {};
-
-  static null_streamt null_stream;
-  static std::ostream null_output_stream;
-
-  std::ostream &progress_output_stream;
-
 protected:
   // we do not use the existing error(), progress(), etc. streams as we want to
   // be able to print progress output just for the ai framework
   std::ostream &progress() const
   {
-    return progress_output_stream;
+    return std::clog;
   }
 
   // we collect progress data irrespective of whether printing progress data is
@@ -344,15 +345,11 @@ class ai_baset
 
   void print_progress() const;
 
-  const std::chrono::duration<float> min_progress_interval;
-
-  // default-constructed time points have the epoch as value
   mutable std::chrono::system_clock::time_point last_progress_output;
 
   void print_progress_interval() const;
 
-  bool periodic_task;
-
+  const ai_configt config;
   // overload to add a factory
   virtual void initialize(const goto_programt &);
   virtual void initialize(const goto_functionst::goto_functiont &);
@@ -455,11 +452,11 @@ class ait:public ai_baset
 {
 public:
   // constructor
-  ait(
-    const bool print_progress = false,
-    const float min_progress_interval = 0,
-    const bool periodic_task = false) :
-      ai_baset(print_progress, min_progress_interval, periodic_task)
+  ait(ai_configt config) : ai_baset(config)
+  {
+  }
+
+  ait() : ai_baset(ai_configt{})
   {
   }
 
@@ -570,11 +567,7 @@ class concurrency_aware_ait:public ait<domainT>
   typedef typename ait<domainT>::statet statet;
 
   // constructor
-  concurrency_aware_ait(
-    const bool print_progress = false,
-    const float min_progress_interval = 0,
-    const bool periodic_task = false):
-      ait<domainT>(print_progress, min_progress_interval, periodic_task)
+  concurrency_aware_ait(const ai_configt &config) : ait<domainT>(config)
   {
   }
 

src/analyses/dependence_graph.h

@@ -229,8 +229,8 @@ class dependence_grapht:
   explicit dependence_grapht(
     const goto_functionst &goto_functions,
     const namespacet &_ns,
-    bool periodic_task = false):
-      ait(false, 0, periodic_task),
+    bool periodic_task = false)
+    : ait(ai_configt{}.with_periodic_task(periodic_task)),
       goto_functions(goto_functions),
       ns(_ns),
       rd(ns, goto_functions, periodic_task)

src/analyses/reaching_definitions.h

@@ -273,16 +273,14 @@ class reaching_definitions_analysist:
   explicit reaching_definitions_analysist(
     const namespacet &_ns,
     const goto_functionst &goto_functions,
-    const bool periodic_task = false):
-      concurrency_aware_ait<rd_range_domaint>(
-        false,
-        0,
-        periodic_task),
-          ns(_ns),
-          goto_functions(goto_functions),
-          value_sets(nullptr),
-          is_threaded(nullptr),
-          is_dirty(nullptr)
+    const bool periodic_task = false)
+    : concurrency_aware_ait<rd_range_domaint>(
+        ai_configt{}.with_periodic_task(periodic_task)),
+      ns(_ns),
+      goto_functions(goto_functions),
+      value_sets(nullptr),
+      is_threaded(nullptr),
+      is_dirty(nullptr)
   {
   }
 

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h

@@ -168,9 +168,8 @@ class variable_sensitivity_dependence_grapht:
   explicit variable_sensitivity_dependence_grapht(
     const goto_functionst &goto_functions,
     const namespacet &_ns,
-    const bool print_progress = false,
-    const float min_progress_interval = 0):
-      ait<variable_sensitivity_dependence_domaint>(print_progress, min_progress_interval),
+    const ai_configt &config = {})
+    : ait<variable_sensitivity_dependence_domaint>(config),
       goto_functions(goto_functions),
       ns(_ns)
   {

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -407,19 +407,13 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
 #endif
     else if(options.get_bool_option("variable-sensitivity"))
     {
-      domain=new ait<variable_sensitivity_domaint>(
-        options.get_bool_option("vs-progress"),
-        options.is_set("vs-progress-interval") ?
-          std::stof(options.get_option("vs-progress-interval")) : 0);
+      domain = new ait<variable_sensitivity_domaint>(
+        ai_configt::from_options(options));
     }
     else if(options.get_bool_option("dependence-graph-vs"))
     {
-      domain=new variable_sensitivity_dependence_grapht(
-        goto_model.goto_functions,
-        ns,
-        options.get_bool_option("vs-progress"),
-        options.is_set("vs-progress-interval") ?
-          std::stof(options.get_option("vs-progress-interval")) : 0);
+      domain = new variable_sensitivity_dependence_grapht(
+        goto_model.goto_functions, ns, ai_configt::from_options(options));
     }
   }
   else if(options.get_bool_option("concurrent"))