Add option to print statistics about the VS domain

Author: hannes-steffenhagen-diffblue

src/analyses/ai.cpp

@@ -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,20 +756,30 @@ 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(config.print_progress && diff >= config.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 = {};
@@ -779,6 +789,8 @@ ai_configt ai_configt::from_options(const optionst &options)
     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;
 }
 

src/analyses/ai.h

@@ -144,6 +144,8 @@ 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;
 
@@ -347,7 +349,7 @@ class ai_baset
 
   mutable std::chrono::system_clock::time_point last_progress_output;
 
-  void print_progress_interval() const;
+  void print_progress_interval(const namespacet &ns) const;
 
   const ai_configt config;
   // overload to add a factory
@@ -444,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
@@ -545,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; }

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

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -266,16 +266,18 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(options.get_bool_option("general-analysis") || reachability_task)
   {
     options.set_option("vs-progress", cmdline.isset("vs-progress"));
+    options.set_option(
+      "vs-progress-memory-usage", cmdline.isset("vs-progress-memory-usage"));
     const char *vs_progress_interval = "vs-progress-interval";
 
     if(cmdline.isset(vs_progress_interval))
     {
-      std::string v(cmdline.get_value(vs_progress_interval));
+      std::string interval_value = cmdline.get_value(vs_progress_interval);
 
       try
       {
         // check if valid float
-        std::stof(v);
+        std::stof(interval_value);
       }
       catch(std::out_of_range)
       {
@@ -286,7 +288,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
         throw "argument to --vs-progress-interval is invalid";
       }
 
-      options.set_option(vs_progress_interval, v);
+      options.set_option(vs_progress_interval, interval_value);
     }
 
     // Abstract interpreter choice
@@ -1018,6 +1020,7 @@ void goto_analyzer_parse_optionst::help()
     " --variable-sensitivity       a highly configurable non-relational domain\n" // NOLINT(*)
     " --vs-progress                print variable sensitivity progress data\n"
     " --vs-progress-interval       minimum interval (in s) between progress reports\n" // NOLINT(*)
+    " --vs-progress-memory-usage   display variable sensitivity memory usage along progress\n" // NOLINT(*)
     "\n"
     "Output options:\n"
     " --text file_name             output results in plain text to given file\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -163,7 +163,10 @@ class optionst;
   "(interval-values)" \
   "(vs-progress)" \
   "(vs-progress-interval):" \
+  "(vs-progress-memory-usage)" \
   "(periodic-task)" \
+  "(vs-progress-interval):" \
+  "(vs-progress-interval):" \
 // clang-format on
 
 class goto_analyzer_parse_optionst: