Merge pull request #5887 from jezhiggins/vsd-value-sets-and-intervals

VSD - Further cross-representation expression evaluation

Author: martin-cs

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -135,8 +135,9 @@ bool any_of_type(const std::vector<abstract_object_pointert> &operands)
            operands.begin(),
            operands.end(),
            [](const abstract_object_pointert &p) {
-             return std::dynamic_pointer_cast<const representation_type>(p) !=
-                    nullptr;
+             return (!p->is_top()) &&
+                    (std::dynamic_pointer_cast<const representation_type>(p) !=
+                     nullptr);
            }) != operands.end();
 }
 
@@ -555,13 +556,25 @@ class value_set_evaluator
   rewrite_expression(const std::vector<abstract_object_pointert> &ops) const
   {
     auto operands_expr = exprt::operandst{};
-    for(auto v : ops)
-      operands_expr.push_back(v->to_constant());
+    for(size_t i = 0; i != expression.operands().size(); ++i)
+    {
+      const auto &v = ops[i];
+      if(is_constant_value(v))
+        operands_expr.push_back(v->to_constant());
+      else
+        operands_expr.push_back(expression.operands()[i]);
+    }
     auto rewritten_expr =
       exprt(expression.id(), expression.type(), std::move(operands_expr));
     return rewritten_expr;
   }
 
+  static bool is_constant_value(const abstract_object_pointert &v)
+  {
+    return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
+           nullptr;
+  }
+
   std::vector<value_ranget> operands_as_ranges() const
   {
     auto unwrapped = std::vector<value_ranget>{};

src/analyses/variable-sensitivity/abstract_value_object.h

@@ -287,10 +287,8 @@ class abstract_value_objectt : public abstract_objectt,
   virtual index_range_implementation_ptrt
   index_range_implementation(const namespacet &ns) const = 0;
 
-  virtual value_range_implementation_ptrt value_range_implementation() const
-  {
-    return util_make_unique<empty_value_ranget>();
-  }
+  virtual value_range_implementation_ptrt
+  value_range_implementation() const = 0;
 };
 
 #endif

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -427,6 +427,12 @@ interval_abstract_valuet::index_range_implementation(const namespacet &ns) const
   return make_interval_index_range(interval, ns);
 }
 
+value_range_implementation_ptrt
+interval_abstract_valuet::value_range_implementation() const
+{
+  return make_single_value_range(shared_from_this());
+}
+
 void interval_abstract_valuet::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -38,6 +38,8 @@ class interval_abstract_valuet : public abstract_value_objectt
   index_range_implementation_ptrt
   index_range_implementation(const namespacet &ns) const override;
 
+  value_range_implementation_ptrt value_range_implementation() const override;
+
   exprt to_constant() const override;
   const constant_interval_exprt &to_interval() const
   {

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -11,18 +11,17 @@
 
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
 #include <analyses/variable-sensitivity/context_abstract_object.h>
-#include <analyses/variable-sensitivity/interval_abstract_value.h>
 #include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
 #include <analyses/variable-sensitivity/value_set_abstract_object.h>
 #include <util/make_unique.h>
 
 static index_range_implementation_ptrt
-make_value_set_index_range(const abstract_object_sett &vals);
+make_value_set_index_range(const std::set<exprt> &vals);
 
 class value_set_index_ranget : public index_range_implementationt
 {
 public:
-  explicit value_set_index_ranget(const abstract_object_sett &vals)
+  explicit value_set_index_ranget(const std::set<exprt> &vals)
     : values(vals), cur(), next(values.begin())
   {
     PRECONDITION(!values.empty());
@@ -37,7 +36,7 @@ class value_set_index_ranget : public index_range_implementationt
     if(next == values.end())
       return false;
 
-    cur = (*next)->to_constant();
+    cur = *next;
     ++next;
     return true;
   }
@@ -47,13 +46,13 @@ class value_set_index_ranget : public index_range_implementationt
   }
 
 private:
-  const abstract_object_sett &values;
+  std::set<exprt> values;
   exprt cur;
-  abstract_object_sett::const_iterator next;
+  std::set<exprt>::const_iterator next;
 };
 
 static index_range_implementation_ptrt
-make_value_set_index_range(const abstract_object_sett &vals)
+make_value_set_index_range(const std::set<exprt> &vals)
 {
   return util_make_unique<value_set_index_ranget>(vals);
 }
@@ -146,7 +145,15 @@ value_set_abstract_objectt::index_range_implementation(
   if(values.empty())
     return make_indeterminate_index_range();
 
-  return make_value_set_index_range(values);
+  std::set<exprt> flattened;
+  for(const auto &o : values)
+  {
+    const auto &v = std::dynamic_pointer_cast<const abstract_value_objectt>(o);
+    for(auto e : v->index_range(ns))
+      flattened.insert(e);
+  }
+
+  return make_value_set_index_range(flattened);
 }
 
 value_range_implementation_ptrt

unit/Makefile

@@ -16,16 +16,15 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        analyses/variable-sensitivity/abstract_object/merge.cpp \
        analyses/variable-sensitivity/abstract_object/index_range.cpp \
-       analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp \
        analyses/variable-sensitivity/constant_abstract_value/merge.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
        analyses/variable-sensitivity/eval.cpp \
        analyses/variable-sensitivity/eval-member-access.cpp \
        analyses/variable-sensitivity/interval_abstract_value/meet.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \
        analyses/variable-sensitivity/last_written_location.cpp \
+       analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \
        analyses/variable-sensitivity/value_set/abstract_value.cpp \
-       analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp \
        analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \
        analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \
        ansi-c/max_malloc_size.cpp \

unit/analyses/variable-sensitivity/abstract_object/index_range.cpp

@@ -1,17 +1,16 @@
+#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h"
 #include <analyses/variable-sensitivity/abstract_environment.h>
-#include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
 #include <analyses/variable-sensitivity/value_set_abstract_object.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <testing-utils/use_catch.h>
 #include <util/arith_tools.h>
-#include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
 SCENARIO(
   "index_range for constant_abstract_values"
-  "[core][analyses][variable-sensitivity][constant_abstract_value][index-"
+  "[core][analyses][variable-sensitivity][constant_abstract_value][index_"
   "range]")
 {
   auto type = signedbv_typet(32);
@@ -26,8 +25,7 @@ SCENARIO(
   {
     auto int_value = 99;
     auto value_expr = from_integer(int_value, type);
-    auto value =
-      std::make_shared<constant_abstract_valuet>(value_expr, env, ns);
+    auto value = make_constant(value_expr, env, ns);
 
     auto range = value->index_range(ns);
 
@@ -59,7 +57,7 @@ SCENARIO(
 
   GIVEN("a top constant's range is has a single nil expression")
   {
-    auto value = std::make_shared<constant_abstract_valuet>(type);
+    auto value = make_top_constant();
 
     auto range = value->index_range(ns);
 
@@ -78,7 +76,7 @@ SCENARIO(
 
 SCENARIO(
   "index_range for interval_abstract_values"
-  "[core][analyses][variable-sensitivity][interval_abstract_value][index-"
+  "[core][analyses][variable-sensitivity][interval_abstract_value][index_"
   "range]")
 {
   auto object_factory = variable_sensitivity_object_factoryt::configured_with(
@@ -91,7 +89,7 @@ SCENARIO(
 
   GIVEN("a top intervals's range is empty")
   {
-    auto value = std::make_shared<interval_abstract_valuet>(type, true, false);
+    auto value = make_top_interval();
 
     auto range = value->index_range(ns);
 
@@ -105,8 +103,7 @@ SCENARIO(
   {
     auto int_value = 99;
     auto value_expr = from_integer(int_value, type);
-    auto value =
-      std::make_shared<interval_abstract_valuet>(value_expr, env, ns);
+    auto value = make_interval(value_expr, value_expr, env, ns);
 
     auto range = value->index_range(ns);
 
@@ -127,12 +124,9 @@ SCENARIO(
   GIVEN("a [99,100] interval's index_range has two elements")
   {
     auto int_value = 99;
-    auto value_expr = from_integer(int_value, type);
-    auto value = std::make_shared<interval_abstract_valuet>(
-      constant_interval_exprt(
-        from_integer(int_value, type), from_integer(int_value + 1, type), type),
-      env,
-      ns);
+    auto lower = from_integer(int_value, type);
+    auto upper = from_integer(int_value + 1, type);
+    auto value = make_interval(lower, upper, env, ns);
 
     auto range = value->index_range(ns);
 
@@ -159,12 +153,9 @@ SCENARIO(
   GIVEN("a [99,102] interval's index_range has four elements")
   {
     auto int_value = 99;
-    auto value_expr = from_integer(int_value, type);
-    auto value = std::make_shared<interval_abstract_valuet>(
-      constant_interval_exprt(
-        from_integer(int_value, type), from_integer(int_value + 3, type), type),
-      env,
-      ns);
+    auto lower = from_integer(int_value, type);
+    auto upper = from_integer(int_value + 3, type);
+    auto value = make_interval(lower, upper, env, ns);
 
     auto range = value->index_range(ns);
 
@@ -186,7 +177,7 @@ SCENARIO(
 
 SCENARIO(
   "index_range for value_set_abstract_values"
-  "[core][analyses][variable-sensitivity][value_set_abstract_value][index-"
+  "[core][analyses][variable-sensitivity][value_set_abstract_value][index_"
   "range]")
 {
   auto object_factory = variable_sensitivity_object_factoryt::configured_with(
@@ -197,10 +188,9 @@ SCENARIO(
   namespacet ns(symbol_table);
   auto type = signedbv_typet(32);
 
-  GIVEN("a value_set is empty")
+  GIVEN("a TOP value_set is empty")
   {
-    auto value =
-      std::make_shared<value_set_abstract_objectt>(type, true, false);
+    auto value = make_top_value_set();
     auto range = value->index_range(ns);
 
     THEN("range should have a nil expr")
@@ -214,4 +204,91 @@ SCENARIO(
       REQUIRE(i == range.end());
     }
   }
+  GIVEN("a value_set { 99, 100, 101, 102 } index_range has four elements")
+  {
+    auto int_value = 99;
+    auto _99 = from_integer(int_value, type);
+    auto _100 = from_integer(100, type);
+    auto _101 = from_integer(101, type);
+    auto _102 = from_integer(102, type);
+    auto value = make_value_set({_99, _100, _101, _102}, env, ns);
+
+    auto range = value->index_range(ns);
+
+    THEN("range has four values")
+    {
+      auto values = std::vector<exprt>();
+      for(const auto &e : range)
+        values.push_back(to_constant_expr(e));
+
+      REQUIRE(values.size() == 4);
+      EXPECT(values, {_99, _100, _101, _102});
+    }
+  }
+  GIVEN("a value_set { [99, 102] } index_range has four elements")
+  {
+    auto int_value = 99;
+    auto _99 = from_integer(int_value, type);
+    auto _100 = from_integer(100, type);
+    auto _101 = from_integer(101, type);
+    auto _102 = from_integer(102, type);
+    auto _99_102 = constant_interval_exprt(_99, _102);
+    auto value = make_value_set({_99_102}, env, ns);
+
+    auto range = value->index_range(ns);
+
+    THEN("range has four values")
+    {
+      auto values = std::vector<exprt>();
+      for(const auto &e : range)
+        values.push_back(to_constant_expr(e));
+
+      REQUIRE(values.size() == 4);
+      EXPECT(values, {_99, _100, _101, _102});
+    }
+  }
+  GIVEN("a value_set { 99, 100, [101, 102] } index_range has four elements")
+  {
+    auto int_value = 99;
+    auto _99 = from_integer(int_value, type);
+    auto _100 = from_integer(100, type);
+    auto _101 = from_integer(101, type);
+    auto _102 = from_integer(102, type);
+    auto _101_102 = constant_interval_exprt(_101, _102);
+    auto value = make_value_set({_99, _101_102, _100}, env, ns);
+
+    auto range = value->index_range(ns);
+
+    THEN("range has four values")
+    {
+      auto values = std::vector<exprt>();
+      for(const auto &e : range)
+        values.push_back(to_constant_expr(e));
+
+      REQUIRE(values.size() == 4);
+      EXPECT(values, {_99, _100, _101, _102});
+    }
+  }
+  GIVEN("a value_set { [99, 102], 100, 101 } index_range has four elements")
+  {
+    auto int_value = 99;
+    auto _99 = from_integer(int_value, type);
+    auto _100 = from_integer(100, type);
+    auto _101 = from_integer(101, type);
+    auto _102 = from_integer(102, type);
+    auto _99_102 = constant_interval_exprt(_99, _102);
+    auto value = make_value_set({_99_102, _100, _101}, env, ns);
+
+    auto range = value->index_range(ns);
+
+    THEN("range has four values")
+    {
+      auto values = std::vector<exprt>();
+      for(const auto &e : range)
+        values.push_back(to_constant_expr(e));
+
+      REQUIRE(values.size() == 4);
+      EXPECT(values, {_99, _100, _101, _102});
+    }
+  }
 }