Eliminate static variable_sensitivity_object_factoryt

jezhiggins · jezhiggins · commit dd66f939e59f · 2020-11-19T09:59:12.000Z
Pass variable_sensitivity_object_factoryt_ptr to abstract_environmenti
constructor, which uses it to create the domain objects.
Update unit tests now static variable_sensitivity_object_factoryt is gone
Remove redundant forward declaration
diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/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)
-{
-}
diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.h b/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
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h
@@ -71,15 +71,12 @@
 #include <analyses/ai.h>
 #include <analyses/variable-sensitivity/abstract_enviroment.h>
 
-class variable_sensitivity_object_factoryt;
-using variable_sensitivity_object_factory_ptrt =
-std::shared_ptr<variable_sensitivity_object_factoryt>;
-
 class variable_sensitivity_domaint : public ai_domain_baset
 {
 public:
   explicit variable_sensitivity_domaint(
-    variable_sensitivity_object_factory_ptrt _object_factory) {
+    variable_sensitivity_object_factory_ptrt _object_factory)
+  : abstract_state(_object_factory) {
   }
 
   /// Compute the abstract transformer for a single instruction
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h
@@ -125,16 +125,16 @@ struct vsd_configt
 class variable_sensitivity_object_factoryt
 {
 public:
+  static std::shared_ptr<variable_sensitivity_object_factoryt> 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) {
   }
 
-  static variable_sensitivity_object_factoryt &instance()
-  {
-    return s_instance;
-  }
-
   /// Get the appropriate abstract object for the variable under
   /// consideration.
   ///
@@ -167,6 +167,7 @@ class variable_sensitivity_object_factoryt
   variable_sensitivity_object_factoryt() : initialized(false)
   {
   }
+
   static variable_sensitivity_object_factoryt s_instance;
   enum ABSTRACT_OBJECT_TYPET
   {
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -771,16 +771,16 @@ 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;
-    }
+    //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");
diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/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);
diff --git a/unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp b/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;
diff --git a/unit/analyses/variable-sensitivity/eval.cpp b/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,
diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/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;
diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp
@@ -11,6 +11,7 @@
 #include <analyses/variable-sensitivity/abstract_enviroment.h>
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/interval_abstract_value.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 
 SCENARIO(
   "meet_interval_abstract_value",
@@ -42,7 +43,10 @@ SCENARIO(
     const auto x_ge_max = binary_relation_exprt(varx, ID_ge, max_value);
     const auto x_gt_max = binary_relation_exprt(varx, ID_gt, max_value);
 
-    abstract_environmentt enviroment;
+    auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+      vsd_configt::intervals());
+
+    abstract_environmentt enviroment { object_factory };
     enviroment.make_top();
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
diff --git a/unit/analyses/variable-sensitivity/last_written_location.cpp b/unit/analyses/variable-sensitivity/last_written_location.cpp
@@ -34,6 +34,9 @@ SCENARIO(
   "symbols",
   "[core][analyses][variable-sensitivity][last-written-location]")
 {
+  auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+    vsd_configt::constant_domain());
+
   GIVEN("Two identifiers that contain integer values")
   {
     const irep_idt identifier = "hello";
@@ -54,12 +57,9 @@ SCENARIO(
     symbol_table.add(second_sym);
     namespacet ns(symbol_table);
 
-    variable_sensitivity_object_factoryt::instance().set_options(
-      vsd_configt::constant_domain());
-
     WHEN("The identifiers get inserted into two environments")
     {
-      abstract_environmentt env;
+      abstract_environmentt env(object_factory);
 
       auto first_eval_rhs = env.eval(rhs_val, ns);
       auto first_eval_res = env.eval(first_val, ns);
@@ -71,7 +71,7 @@ SCENARIO(
       env.assign(first_val, first_eval_rhs, ns);
       env.assign(second_val, second_eval_rhs, ns);
 
-      abstract_environmentt second_env;
+      abstract_environmentt second_env(object_factory);
       second_env.assign(first_val, first_eval_rhs, ns);
       second_env.assign(second_val, second_eval_rhs, ns);
 
@@ -107,7 +107,7 @@ SCENARIO(
       "The identifiers get inserted into two environments, but one of "
       "them has a different value in one of the environments")
     {
-      abstract_environmentt env;
+      abstract_environmentt env(object_factory);
 
       auto first_eval_rhs = env.eval(rhs_val, ns);
       auto first_eval_res = env.eval(first_val, ns);
@@ -121,7 +121,7 @@ SCENARIO(
 
       auto rhs_val_3 = from_integer(20, integer_typet());
 
-      abstract_environmentt second_env;
+      abstract_environmentt second_env(object_factory);
       auto new_rhs_val = second_env.eval(rhs_val_3, ns);
       second_env.assign(first_val, first_eval_rhs, ns);
       second_env.assign(second_val, new_rhs_val, ns);
diff --git a/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp b/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp
@@ -67,6 +67,16 @@ class ContainsAllOf
 };
 } // namespace
 
+std::unique_ptr<variable_sensitivity_domain_factoryt> domain_factory()
+{
+  auto vs_object_factory =
+    std::make_shared<variable_sensitivity_object_factoryt>(vsd_configt {});
+
+  return
+    util_make_unique<variable_sensitivity_domain_factoryt>(vs_object_factory);
+}
+
+
 TEST_CASE(
   "A value set abstract object created from type is top",
   VALUE_SET_TEST_TAGS)
@@ -257,9 +267,11 @@ TEST_CASE(
   auto const value_set =
     value_set_abstract_valuet{type, value_set_abstract_valuet::valuest{}};
 
+  const ait<variable_sensitivity_domaint> ai { domain_factory() };
+
   std::stringstream ss;
   value_set.output(
-    ss, ait<variable_sensitivity_domaint>{}, namespacet{symbol_tablet{}});
+    ss, ai, namespacet{symbol_tablet{}});
   REQUIRE(ss.str() == "BOTTOM");
 }
 
@@ -271,9 +283,11 @@ TEST_CASE(
   auto const value = from_integer(10, type);
   auto const value_set = value_set_abstract_valuet{type, {value}};
 
+  const ait<variable_sensitivity_domaint> ai { domain_factory() };
+
   std::stringstream ss;
   value_set.output(
-    ss, ait<variable_sensitivity_domaint>{}, namespacet{symbol_tablet{}});
+    ss, ai, namespacet{symbol_tablet{}});
   REQUIRE(ss.str() == "{ 10 }");
 }
 
@@ -289,9 +303,11 @@ TEST_CASE(
   auto const value_set =
     value_set_abstract_valuet{type, {value1, value2, value3}};
 
+  const ait<variable_sensitivity_domaint> ai { domain_factory() };
+
   std::stringstream ss;
   value_set.output(
-    ss, ait<variable_sensitivity_domaint>{}, namespacet{symbol_tablet{}});
+    ss, ai, namespacet{symbol_tablet{}});
   REQUIRE(ss.str() == "{ 10 12 14 }");
 }
 
@@ -310,9 +326,11 @@ TEST_CASE(
   auto const value_set = value_set_abstract_valuet{type, values};
   REQUIRE(value_set.is_top());
 
+  const ait<variable_sensitivity_domaint> ai { domain_factory() };
+
   std::stringstream ss;
   value_set.output(
-    ss, ait<variable_sensitivity_domaint>{}, namespacet{symbol_tablet{}});
+    ss, ai, namespacet{symbol_tablet{}});
   REQUIRE(ss.str() == "TOP");
 }
 
@@ -368,8 +386,8 @@ static abstract_environmentt get_value_set_abstract_environment()
   config.advanced_sensitivities.new_value_set = true;
   config.context_tracking.data_dependency_context = false;
   config.context_tracking.last_write_context = false;
-  variable_sensitivity_object_factoryt::instance().set_options(config);
-  auto environment = abstract_environmentt{};
+  auto object_factory = variable_sensitivity_object_factoryt::configured_with(config);
+  auto environment = abstract_environmentt { object_factory };
   environment.make_top();
   return environment;
 }

Original file line number	Diff line number	Diff line change
`@@ -337,7 +337,7 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(`
`337`	`337`	`const abstract_environmentt &environment,`
`338`	`338`	`const namespacet &ns) const`
`339`	`339`	`{`
`340`		`- return variable_sensitivity_object_factoryt::instance().get_abstract_object(`
	`340`	`+ return object_factory->get_abstract_object(`
`341`	`341`	`type, top, bottom, e, environment, ns);`
`342`	`342`	`}`
`343`	`343`
`@@ -527,7 +527,3 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const`
`527`	`527`	`}`
`528`	`528`	`return statistics;`
`529`	`529`	`}`
`530`		`-`
`531`		`-abstract_environmentt::abstract_environmentt() : bottom(true)`
`532`		`-{`
`533`		`-}`
Original file line number	Diff line number	Diff line change
`@@ -125,16 +125,16 @@ struct vsd_configt`
`125`	`125`	`class variable_sensitivity_object_factoryt`
`126`	`126`	`{`
`127`	`127`	`public:`
	`128`	`+ static std::shared_ptr<variable_sensitivity_object_factoryt> configured_with(`
	`129`	`+ const vsd_configt &options) {`
	`130`	`+ return std::make_shared<variable_sensitivity_object_factoryt>(options);`
	`131`	`+ }`
	`132`	`+`
`128`	`133`	`explicit variable_sensitivity_object_factoryt(const vsd_configt &options)`
`129`	`134`	`: configuration(options),`
`130`	`135`	`initialized(true) {`
`131`	`136`	`}`
`132`	`137`
`133`		`- static variable_sensitivity_object_factoryt &instance()`
`134`		`- {`
`135`		`- return s_instance;`
`136`		`- }`
`137`		`-`
`138`	`138`	`/// Get the appropriate abstract object for the variable under`
`139`	`139`	`/// consideration.`
`140`	`140`	`///`
`@@ -167,6 +167,7 @@ class variable_sensitivity_object_factoryt`
`167`	`167`	`variable_sensitivity_object_factoryt() : initialized(false)`
`168`	`168`	`{`
`169`	`169`	`}`
	`170`	`+`
`170`	`171`	`static variable_sensitivity_object_factoryt s_instance;`
`171`	`172`	`enum ABSTRACT_OBJECT_TYPET`
`172`	`173`	`{`