Merge pull request diffblue#227 from hannes-steffenhagen-diffblue/feature-domain_summary-flag-rebase-rebase

Feature domain summary flag

Author: chrisr-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());
@@ -515,15 +515,15 @@ bool ai_baset::do_function_call(
       progress_data.max_stack_depth
         = std::max(progress_data.max_stack_depth, progress_data.stack.size());
 
-      print_progress_interval();
+      print_progress_interval(ns);
 
       fixedpoint(goto_function.body, goto_functions, ns);
 
       progress_data.functions_returned.insert(id);
       progress_data.num_functions_returned++;
       progress_data.stack.pop_front();
 
-      print_progress_interval();
+      print_progress_interval(ns);
     }
   }
 
@@ -756,19 +756,59 @@ void ai_baset::print_progress() const
   progress() << std::flush;
 }
 
-void ai_baset::print_progress_interval() const
+void ai_baset::print_progress_interval(const namespacet &ns) const
 {
   using namespace std::chrono;
 
   system_clock::time_point now = system_clock::now();
   auto diff = now - last_progress_output;
-
-  if(diff >= min_progress_interval)
+  if(diff >= config.progress_interval)
   {
-    print_progress();
     last_progress_output = now;
+    if(config.print_progress)
+    {
+      print_progress();
+    }
+    if(config.print_memory_usage)
+    {
+      print_memory_usage(ns);
+    }
+  }
+}
+
+void ai_baset::print_memory_usage(const namespacet &ns) const
+{
+}
+
+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")));
   }
+  result.print_memory_usage =
+    options.get_bool_option("vs-progress-memory-usage");
+  return result;
+}
+
+ai_configt &ai_configt::with_print_progress(bool print_progress)
+{
+  this->print_progress = print_progress;
+  return *this;
 }
 
-ai_baset::null_streamt ai_baset::null_stream;
-std::ostream ai_baset::null_output_stream(&ai_baset::null_stream);
+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,21 @@ class ai_domain_baset
 
 };
 
+struct ai_configt
+{
+  using secondst = std::chrono::duration<float>;
+  bool print_progress = false;
+  bool print_memory_usage = 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 +163,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 +309,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 +347,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;
+  void print_progress_interval(const namespacet &ns) const;
 
+  const ai_configt config;
   // overload to add a factory
   virtual void initialize(const goto_programt &);
   virtual void initialize(const goto_functionst::goto_functiont &);
@@ -447,6 +446,19 @@ class ai_baset
   virtual statet &get_state(locationt l)=0;
   virtual const statet &find_state(locationt l) const=0;
   virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
+
+  virtual void print_memory_usage(const namespacet &ns) const;
+};
+
+template <typename domainT>
+struct get_domain_statisticst
+{
+  void add_entry(const domainT &domain, const namespacet &ns)
+  {
+  }
+  void print(std::ostream &out) const
+  {
+  }
 };
 
 // domainT is expected to be derived from ai_domain_baseT
@@ -455,11 +467,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{})
   {
   }
 
@@ -548,6 +560,16 @@ class ait:public ai_baset
     sequential_fixedpoint(goto_functions, ns);
   }
 
+  void print_memory_usage(const namespacet &ns) const override
+  {
+    get_domain_statisticst<domainT> statistics;
+    for(auto const &state_entry : state_map)
+    {
+      statistics.add_entry(state_entry.second, ns);
+    }
+    statistics.print(progress());
+  }
+
 private:
   // to enforce that domainT is derived from ai_domain_baset
   void dummy(const domainT &s) { const statet &x=s; (void)x; }
@@ -570,11 +592,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/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -592,3 +592,8 @@ void variable_sensitivity_domaint::apply_domain(
     abstract_state.assign(symbol, value, ns);
   }
 }
+abstract_object_statisticst
+variable_sensitivity_domaint::gather_statistics(const namespacet &ns) const
+{
+  return abstract_state.gather_statistics(ns);
+}

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -137,6 +137,49 @@ class variable_sensitivity_domaint:public ai_domain_baset
     const namespacet &ns);
 
   abstract_environmentt abstract_state;
+
+public:
+  abstract_object_statisticst gather_statistics(const namespacet &ns) const;
+};
+
+template <>
+struct get_domain_statisticst<variable_sensitivity_domaint>
+{
+  abstract_object_statisticst total_statistics = {};
+  void
+  add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
+  {
+    auto statistics = domain.gather_statistics(ns);
+    total_statistics.number_of_interval_abstract_objects +=
+      statistics.number_of_interval_abstract_objects;
+    total_statistics.number_of_globals += statistics.number_of_globals;
+    total_statistics.number_of_single_value_intervals +=
+      statistics.number_of_single_value_intervals;
+    total_statistics.number_of_constants += statistics.number_of_constants;
+    total_statistics.number_of_pointers += statistics.number_of_constants;
+    total_statistics.number_of_arrays += statistics.number_of_arrays;
+    total_statistics.number_of_structs += statistics.number_of_arrays;
+    total_statistics.objects_memory_usage += statistics.objects_memory_usage;
+  }
+
+  void print(std::ostream &out) const
+  {
+    out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
+        << "  Memory Usage: "
+        << total_statistics.objects_memory_usage.to_string() << '\n'
+        << "  Number of structs: " << total_statistics.number_of_structs << '\n'
+        << "  Number of arrays: " << total_statistics.number_of_arrays << '\n'
+        << "  Number of pointers: " << total_statistics.number_of_pointers
+        << '\n'
+        << "  Number of constants: " << total_statistics.number_of_constants
+        << '\n'
+        << "  Number of intervals: "
+        << total_statistics.number_of_interval_abstract_objects << '\n'
+        << "  Number of single value intervals: "
+        << total_statistics.number_of_single_value_intervals << '\n'
+        << "  Number of globals: " << total_statistics.number_of_globals << '\n'
+        << "<< End Variable Sensitivity Domain Statistics >>\n";
+  }
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H