abstract_environmentt::to_predicate

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -419,6 +419,29 @@ void abstract_environmentt::output(
   out << "}\n";
 }
 
+exprt abstract_environmentt::to_predicate() const
+{
+  if(is_bottom())
+    return false_exprt();
+  if(is_top())
+    return true_exprt();
+
+  auto predicates = std::vector<exprt> { };
+  for(const auto &entry : map.get_view())
+  {
+    auto sym = entry.first;
+    auto val = entry.second;
+
+    auto pred = val->to_predicate(symbol_exprt(sym, val->type()));
+
+    predicates.push_back(pred);
+  }
+
+  if(predicates.size() == 1)
+    return predicates.front();
+  return and_exprt(predicates);
+}
+
 bool abstract_environmentt::verify() const
 {
   decltype(map)::viewt view;

src/analyses/variable-sensitivity/abstract_environment.h

@@ -224,6 +224,12 @@ class abstract_environmentt
   void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
     const;
 
+  /// Gives a boolean condition that is true for all values represented by the
+  /// environment.
+  ///
+  /// \return An exprt describing the environment
+  exprt to_predicate() const;
+
   /// Check the structural invariants are maintained.
   /// In this case this is checking there aren't any null pointer mapped values
   bool verify() const;

unit/Makefile

@@ -14,6 +14,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
+       analyses/variable-sensitivity/abstract_environment/to_predicate.cpp \
        analyses/variable-sensitivity/abstract_object/merge.cpp \
        analyses/variable-sensitivity/abstract_object/index_range.cpp \
        analyses/variable-sensitivity/constant_abstract_value/meet.cpp \

unit/analyses/variable-sensitivity/abstract_environment/module_dependencies.txt

@@ -0,0 +1,3 @@
+analyses
+testing-utils
+util

unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp

@@ -0,0 +1,73 @@
+/*******************************************************************\
+
+ Module: Tests for abstract_environmentt::to_predicate
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
+#include <testing-utils/use_catch.h>
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
+
+SCENARIO(
+  "abstract_environment to predicate",
+  "[core][analyses][variable-sensitivity][abstract_environment][to_predicate]")
+{
+  auto config = vsd_configt::constant_domain();
+  config.context_tracking.data_dependency_context = false;
+  config.context_tracking.last_write_context = false;
+  auto object_factory =
+    variable_sensitivity_object_factoryt::configured_with(config);
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  GIVEN("an abstract environment")
+  {
+    WHEN("it is TOP")
+    {
+      auto env = abstract_environmentt{object_factory};
+      env.make_top();
+      THEN_PREDICATE(env, "TRUE");
+    }
+    WHEN("it is BOTTOM")
+    {
+      auto env = abstract_environmentt{object_factory};
+      env.make_bottom();
+      THEN_PREDICATE(env, "FALSE");
+    }
+    WHEN("contains x = 2")
+    {
+      auto env = abstract_environmentt{object_factory};
+      env.make_top();
+
+      auto type = signedbv_typet(32);
+      auto val2 = make_constant(from_integer(2, type), env, ns);
+      auto x_name = symbol_exprt(dstringt("x"), type);
+
+      env.assign(x_name, val2, ns);
+
+      THEN_PREDICATE(env, "x == 2");
+    }
+    WHEN("contains x = 2, y = 3")
+    {
+      auto env = abstract_environmentt{object_factory};
+      env.make_top();
+
+      auto type = signedbv_typet(32);
+      auto val2 = make_constant(from_integer(2, type), env, ns);
+      auto x_name = symbol_exprt(dstringt("x"), type);
+
+      auto val3 = make_constant(from_integer(3, type), env, ns);
+      auto y_name = symbol_exprt(dstringt("y"), type);
+
+      env.assign(x_name, val2, ns);
+      env.assign(y_name, val3, ns);
+
+      THEN_PREDICATE(env, "y == 3 && x == 2");
+    }
+  }
+}

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

@@ -538,3 +538,13 @@ void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out)
     REQUIRE(repr == out);
   }
 }
+
+void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out)
+{
+  auto pred = env.to_predicate();
+  THEN("predicate is " + out)
+  {
+    auto repr = expr_to_str(pred);
+    REQUIRE(repr == out);
+  }
+}

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h

@@ -255,5 +255,6 @@ std::string exprs_to_str(const std::vector<exprt> &values);
 void THEN_PREDICATE(
   const abstract_object_pointert &obj,
   const std::string &out);
+void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out);
 
 #endif