Merge pull request diffblue#213 from hannes-steffenhagen-diffblue/feature-domain_summary-28

Feature domain summary 28

Author: chrisr-diffblue

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -9,6 +9,7 @@
 #include <stack>
 #include <map>
 #include <ostream>
+#include <algorithm>
 
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
@@ -739,10 +740,21 @@ std::vector<symbol_exprt> abstract_environmentt::modified_symbols(
   return symbols_diff;
 }
 
+static std::size_t count_globals(const namespacet &ns)
+{
+  auto const& symtab = ns.get_symbol_table();
+  auto val = std::count_if(symtab.begin(), symtab.end(),
+                       [](const symbol_table_baset::const_iteratort::value_type& sym) {
+                         return sym.second.is_lvalue && sym.second.is_static_lifetime;
+                       });
+  return val;
+}
+
 abstract_object_statisticst
 abstract_environmentt::gather_statistics(const namespacet &ns) const
 {
   abstract_object_statisticst statistics = {};
+  statistics.number_of_globals = count_globals(ns);
   decltype(map)::viewt view;
   map.get_view(view);
   abstract_object_visitedt visited;

src/analyses/variable-sensitivity/abstract_object_statistics.h

@@ -3,10 +3,18 @@
 
 #include <cstddef>
 
+#include <util/memory_units.h>
 struct abstract_object_statisticst
 {
-  std::size_t number_of_interval_abstract_objects;
-  std::size_t number_of_single_value_intervals;
+  std::size_t number_of_interval_abstract_objects = 0;
+  std::size_t number_of_single_value_intervals = 0;
+  std::size_t number_of_structs = 0;
+  std::size_t number_of_arrays = 0;
+  std::size_t number_of_pointers = 0;
+  std::size_t number_of_constants = 0;
+  std::size_t number_of_globals = 0;
+  /// An underestimation of the memory usage of the abstract objects
+  memory_sizet objects_memory_usage;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_STATISTICS_H

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -199,3 +199,9 @@ sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
       new array_abstract_objectt(type(), true, false));
   }
 }
+
+void array_abstract_objectt::get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited,
+                                            const abstract_environmentt &env, const namespacet &ns) const {
+  abstract_objectt::get_statistics(statistics, visited, env, ns);
+  ++statistics.number_of_arrays;
+}

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -39,6 +39,9 @@ class array_abstract_objectt:public abstract_objectt
     const abstract_object_pointert value,
     bool merging_write) const override;
 
+  void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited,
+                      const abstract_environmentt &env, const namespacet &ns) const override;
+
 protected:
   CLONE
 

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -231,3 +231,13 @@ abstract_object_pointert constant_abstract_valuet::merge_constant_constant(
     }
   }
 }
+
+void constant_abstract_valuet::get_statistics(abstract_object_statisticst &statistics,
+                                              abstract_object_visitedt &visited,
+                                              const abstract_environmentt &env,
+                                              const namespacet& ns) const
+{
+  abstract_valuet::get_statistics(statistics, visited, env, ns);
+  ++statistics.number_of_constants;
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
+}

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -42,6 +42,11 @@ class constant_abstract_valuet:public abstract_valuet
     const class ai_baset &ai,
     const class namespacet &ns) const override;
 
+  void get_statistics(abstract_object_statisticst &statistics,
+                      abstract_object_visitedt &visited,
+                      const abstract_environmentt &env,
+                      const namespacet& ns) const override;
+
 protected:
   CLONE
   virtual abstract_object_pointert merge(

src/analyses/variable-sensitivity/constant_array_abstract_object.cpp

@@ -549,4 +549,5 @@ void constant_array_abstract_objectt::get_statistics(
       object.second->get_statistics(statistics, visited, env, ns);
     }
   }
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
 }

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -373,4 +373,5 @@ void constant_pointer_abstract_objectt::get_statistics(
   {
     read_dereference(env, ns)->get_statistics(statistics, visited, env, ns);
   }
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
 }

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -180,4 +180,5 @@ void context_abstract_objectt::get_statistics(
   {
     child_abstract_object->get_statistics(statistics, visited, env, ns);
   }
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
 }

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -496,4 +496,5 @@ void full_struct_abstract_objectt::get_statistics(
       object.second->get_statistics(statistics, visited, env, ns);
     }
   }
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
 }