Merge pull request #5610 from jezhiggins/variable-sensitivity-object-factory-rework

Variable sensitivity object factory rework

Author: martin-cs

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -337,7 +337,7 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  return variable_sensitivity_object_factoryt::instance().get_abstract_object(
+  return object_factory->get_abstract_object(
     type, top, bottom, e, environment, ns);
 }
 
@@ -527,7 +527,3 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const
   }
   return statistics;
 }
-
-abstract_environmentt::abstract_environmentt() : bottom(true)
-{
-}

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -28,11 +28,23 @@
 #include <util/sharing_map.h>
 #include <util/std_expr.h>
 
+class variable_sensitivity_object_factoryt;
+using variable_sensitivity_object_factory_ptrt =
+  std::shared_ptr<variable_sensitivity_object_factoryt>;
+
 class abstract_environmentt
 {
 public:
   using map_keyt = irep_idt;
-  abstract_environmentt();
+
+  abstract_environmentt() = delete;
+
+  abstract_environmentt(
+    variable_sensitivity_object_factory_ptrt _object_factory)
+    : bottom(true), object_factory(_object_factory)
+  {
+  }
+
   /// These three are really the heart of the method
 
   /// Evaluate the value of an expression relative to the current domain
@@ -248,6 +260,8 @@ class abstract_environmentt
     const exprt &e,
     const abstract_environmentt &environment,
     const namespacet &ns) const;
+
+  variable_sensitivity_object_factory_ptrt object_factory;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

@@ -613,31 +613,37 @@ class variable_sensitivity_dependence_domain_factoryt
 {
 public:
   explicit variable_sensitivity_dependence_domain_factoryt(
-    variable_sensitivity_dependence_grapht &_dg)
-    : dg(_dg)
+    variable_sensitivity_dependence_grapht &_dg,
+    variable_sensitivity_object_factory_ptrt _object_factory)
+    : dg(_dg), object_factory(_object_factory)
   {
   }
 
   std::unique_ptr<statet> make(locationt l) const override
   {
     auto node_id = dg.add_node();
     dg.nodes[node_id].PC = l;
-    auto p = util_make_unique<variable_sensitivity_dependence_domaint>(node_id);
+    auto p = util_make_unique<variable_sensitivity_dependence_domaint>(
+      node_id, object_factory);
     CHECK_RETURN(p->is_bottom());
 
     return std::unique_ptr<statet>(p.release());
   }
 
 private:
   variable_sensitivity_dependence_grapht &dg;
+  variable_sensitivity_object_factory_ptrt object_factory;
 };
 
 variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht(
   const goto_functionst &goto_functions,
-  const namespacet &_ns)
+  const namespacet &_ns,
+  variable_sensitivity_object_factory_ptrt _object_factory)
   : ai_three_way_merget(
       util_make_unique<ai_history_factory_default_constructort<ahistoricalt>>(),
-      util_make_unique<variable_sensitivity_dependence_domain_factoryt>(*this),
+      util_make_unique<variable_sensitivity_dependence_domain_factoryt>(
+        *this,
+        _object_factory),
       util_make_unique<location_sensitive_storaget>()),
     goto_functions(goto_functions),
     ns(_ns)

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h

@@ -74,8 +74,13 @@ class variable_sensitivity_dependence_domaint
 public:
   typedef grapht<vs_dep_nodet>::node_indext node_indext;
 
-  explicit variable_sensitivity_dependence_domaint(node_indext id)
-    : node_id(id), has_values(false), has_changed(false)
+  explicit variable_sensitivity_dependence_domaint(
+    node_indext id,
+    variable_sensitivity_object_factory_ptrt object_factory)
+    : variable_sensitivity_domaint(object_factory),
+      node_id(id),
+      has_values(false),
+      has_changed(false)
   {
   }
 
@@ -237,7 +242,8 @@ class variable_sensitivity_dependence_grapht : public ai_three_way_merget,
 
   explicit variable_sensitivity_dependence_grapht(
     const goto_functionst &goto_functions,
-    const namespacet &_ns);
+    const namespacet &_ns,
+    variable_sensitivity_object_factory_ptrt object_factory);
 
   void
   initialize(const irep_idt &function_id, const goto_programt &goto_program)

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -74,6 +74,12 @@
 class variable_sensitivity_domaint : public ai_domain_baset
 {
 public:
+  explicit variable_sensitivity_domaint(
+    variable_sensitivity_object_factory_ptrt _object_factory)
+    : abstract_state(_object_factory)
+  {
+  }
+
   /// Compute the abstract transformer for a single instruction
   ///
   /// \param function_from: the name of the function containing from
@@ -212,6 +218,27 @@ class variable_sensitivity_domaint : public ai_domain_baset
 #endif
 };
 
+class variable_sensitivity_domain_factoryt
+  : public ai_domain_factoryt<variable_sensitivity_domaint>
+{
+public:
+  explicit variable_sensitivity_domain_factoryt(
+    variable_sensitivity_object_factory_ptrt _object_factory)
+    : object_factory(_object_factory)
+  {
+  }
+
+  std::unique_ptr<statet> make(locationt l) const override
+  {
+    auto d = util_make_unique<variable_sensitivity_domaint>(object_factory);
+    CHECK_RETURN(d->is_bottom());
+    return std::unique_ptr<statet>(d.release());
+  }
+
+private:
+  variable_sensitivity_object_factory_ptrt object_factory;
+};
+
 #ifdef ENABLE_STATS
 template <>
 struct get_domain_statisticst<variable_sensitivity_domaint>

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

@@ -10,9 +10,6 @@
 #include "util/namespace.h"
 #include "value_set_abstract_value.h"
 
-variable_sensitivity_object_factoryt
-  variable_sensitivity_object_factoryt::s_instance;
-
 variable_sensitivity_object_factoryt::ABSTRACT_OBJECT_TYPET
 variable_sensitivity_object_factoryt::get_abstract_object_type(const typet type)
 {
@@ -143,10 +140,3 @@ variable_sensitivity_object_factoryt::get_abstract_object(
       followed_type, top, bottom, e, environment, ns);
   }
 }
-
-void variable_sensitivity_object_factoryt::set_options(
-  const vsd_configt &options)
-{
-  this->configuration = options;
-  initialized = true;
-}

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h

@@ -122,12 +122,22 @@ struct vsd_configt
   }
 };
 
+class variable_sensitivity_object_factoryt;
+using variable_sensitivity_object_factory_ptrt =
+  std::shared_ptr<variable_sensitivity_object_factoryt>;
+
 class variable_sensitivity_object_factoryt
 {
 public:
-  static variable_sensitivity_object_factoryt &instance()
+  static variable_sensitivity_object_factory_ptrt
+  configured_with(const vsd_configt &options)
+  {
+    return std::make_shared<variable_sensitivity_object_factoryt>(options);
+  }
+
+  explicit variable_sensitivity_object_factoryt(const vsd_configt &options)
+    : configuration(options), initialized(true)
   {
-    return s_instance;
   }
 
   /// Get the appropriate abstract object for the variable under
@@ -152,17 +162,11 @@ class variable_sensitivity_object_factoryt
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /// Called once to record the appropriate variables from the command line
-  /// options so that they can be accessed easily when they are needed.
-  ///
-  /// \param options: the command line options
-  void set_options(const vsd_configt &options);
-
 private:
   variable_sensitivity_object_factoryt() : initialized(false)
   {
   }
-  static variable_sensitivity_object_factoryt s_instance;
+
   enum ABSTRACT_OBJECT_TYPET
   {
     TWO_VALUE,

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -446,6 +446,10 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
   const optionst &options,
   const namespacet &ns)
 {
+  auto vsd_config = vsd_configt::from_options(options);
+  auto vs_object_factory =
+    variable_sensitivity_object_factoryt::configured_with(vsd_config);
+
   // These support all of the option categories
   if(
     options.get_bool_option("recursive-interprocedural") ||
@@ -485,8 +489,8 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
     }
     else if(options.get_bool_option("vsd"))
     {
-      df = util_make_unique<
-        ai_domain_factory_default_constructort<variable_sensitivity_domaint>>();
+      df = util_make_unique<variable_sensitivity_domain_factoryt>(
+        vs_object_factory);
     }
     // non-null is not fully supported, despite the historical options
     // dependency-graph is quite heavily tied to the legacy-ait infrastructure
@@ -537,11 +541,13 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
     else if(options.get_bool_option("dependence-graph-vs"))
     {
       return new variable_sensitivity_dependence_grapht(
-        goto_model.goto_functions, ns);
+        goto_model.goto_functions, ns, vs_object_factory);
     }
     else if(options.get_bool_option("vsd"))
     {
-      return new ait<variable_sensitivity_domaint>();
+      auto df = util_make_unique<variable_sensitivity_domain_factoryt>(
+        vs_object_factory);
+      return new ait<variable_sensitivity_domaint>(std::move(df));
     }
     else if(options.get_bool_option("intervals"))
     {
@@ -629,7 +635,6 @@ int goto_analyzer_parse_optionst::doit()
   return perform_analysis(options);
 }
 
-
 /// Depending on the command line mode, run one of the analysis tasks
 int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 {
@@ -758,18 +763,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(options.get_bool_option("general-analysis"))
   {
-    // TODO : replace with the domain factory infrastructure
-    try
-    {
-      variable_sensitivity_object_factoryt::instance().set_options(
-        vsd_configt::from_options(options));
-    }
-    catch(const invalid_command_line_argument_exceptiont &e)
-    {
-      log.error() << e.what() << messaget::eom;
-      return CPROVER_EXIT_USAGE_ERROR;
-    }
-
     // Output file factory
     const std::string outfile=options.get_option("outfile");
 
@@ -790,7 +783,17 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     // Build analyzer
     log.status() << "Selecting abstract domain" << messaget::eom;
     namespacet ns(goto_model.symbol_table);  // Must live as long as the domain.
-    std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
+    std::unique_ptr<ai_baset> analyzer;
+
+    try
+    {
+      analyzer.reset(build_analyzer(options, ns));
+    }
+    catch(const invalid_command_line_argument_exceptiont &e)
+    {
+      log.error() << e.what() << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
 
     if(analyzer == nullptr)
     {
@@ -862,7 +865,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_VERIFICATION_SAFE;
   }
 
-
   // Final defensive error case
   log.error() << "no analysis option given -- consider reading --help"
               << messaget::eom;

unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp

@@ -9,6 +9,7 @@
 #include <analyses/variable-sensitivity/abstract_enviroment.h>
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <testing-utils/use_catch.h>
 #include <typeinfo>
 #include <util/arith_tools.h>
@@ -27,7 +28,9 @@ SCENARIO(
     const exprt val1 = from_integer(1, integer_typet());
     const exprt val2 = from_integer(2, integer_typet());
 
-    abstract_environmentt enviroment;
+    auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+      vsd_configt::constant_domain());
+    abstract_environmentt enviroment{object_factory};
     enviroment.make_top();
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);

unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp

@@ -101,14 +101,13 @@ SCENARIO(
     const index_exprt i2 =
       index_exprt(nil_exprt(), from_integer(2, integer_typet()));
 
-    abstract_environmentt enviroment;
+    auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+      vsd_configt::constant_domain());
+    abstract_environmentt enviroment(object_factory);
     enviroment.make_top();
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
 
-    variable_sensitivity_object_factoryt::instance().set_options(
-      vsd_configt::constant_domain());
-
     array_utilt util(enviroment, ns);
 
     abstract_object_pointert result;

unit/analyses/variable-sensitivity/eval.cpp

@@ -21,9 +21,9 @@ SCENARIO(
 {
   GIVEN("An environment with intervals domain")
   {
-    variable_sensitivity_object_factoryt::instance().set_options(
+    auto object_factory = variable_sensitivity_object_factoryt::configured_with(
       vsd_configt::intervals());
-    abstract_environmentt environment;
+    abstract_environmentt environment(object_factory);
     environment.make_top(); // Domains are bottom on construction
 
     symbol_tablet symbol_table;
@@ -68,7 +68,7 @@ SCENARIO(
         // b1 = 0
         environment.assign(
           b1.symbol_expr(),
-          variable_sensitivity_object_factoryt::instance().get_abstract_object(
+          object_factory->get_abstract_object(
             number_type,
             false,
             false,

unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp

@@ -128,14 +128,13 @@ SCENARIO(
     const member_exprt b(nil_exprt(), "b", integer_typet());
     const member_exprt c(nil_exprt(), "c", integer_typet());
 
-    abstract_environmentt enviroment;
+    auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+      vsd_configt::constant_domain());
+    abstract_environmentt enviroment(object_factory);
     enviroment.make_top();
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
 
-    variable_sensitivity_object_factoryt::instance().set_options(
-      vsd_configt::constant_domain());
-
     struct_utilt util(enviroment, ns);
 
     abstract_object_pointert result;