value_set index_range should flatten contained values into one range

A constant of, say, 5 has a index_range of 5. A value_set of { 5, 6,
9 } therefore has an index_range of 5,6,9.

An interval of [1, 3] has an index_range of 1,2,3. A value_set
containing that interval should have the same index_range.

A value_set of multiple constants and intervals should have an
index_range which is the union of its contents index_range.

Author: jezhiggins

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/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});
+    }
+  }
 }

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

@@ -104,6 +104,13 @@ as_value_set(const abstract_object_pointert &aop)
   return std::dynamic_pointer_cast<const value_set_abstract_objectt>(aop);
 }
 
+bool set_contains(const std::vector<exprt> &set, const exprt &val)
+{
+  auto i = std::find_if(
+    set.begin(), set.end(), [&val](const exprt &lhs) { return lhs == val; });
+  return i != set.end();
+}
+
 bool set_contains(const abstract_object_sett &set, const exprt &val)
 {
   auto i = std::find_if(
@@ -210,14 +217,31 @@ void EXPECT(
   REQUIRE_FALSE(result->is_bottom());
 
   auto values = result->get_values();
+  auto value_string = set_to_str(values);
+  auto expected_string = exprs_to_str(expected_values);
+
+  INFO("Expect " + value_string + " to match " + expected_string);
   REQUIRE(values.size() == expected_values.size());
 
-  auto value_string = set_to_str(values);
+  for(auto &ev : expected_values)
+  {
+    INFO("Expect " + value_string + " to match " + expected_string);
+    REQUIRE(set_contains(values, ev));
+  }
+}
+
+void EXPECT(
+  const std::vector<exprt> &values,
+  const std::vector<exprt> &expected_values)
+{
+  auto value_string = exprs_to_str(values);
   auto expected_string = exprs_to_str(expected_values);
+  INFO("Expect " + value_string + " to match " + expected_string);
+  REQUIRE(values.size() == expected_values.size());
 
   for(auto &ev : expected_values)
   {
-    INFO("Expect " + value_string + " to include " + expected_string);
+    INFO("Expect " + value_string + " to match " + expected_string);
     REQUIRE(set_contains(values, ev));
   }
 }

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h

@@ -61,6 +61,10 @@ void EXPECT(
   std::shared_ptr<const value_set_abstract_objectt> &result,
   const std::vector<exprt> &expected_values);
 
+void EXPECT(
+  const std::vector<exprt> &values,
+  const std::vector<exprt> &expected_values);
+
 void EXPECT_TOP(std::shared_ptr<const abstract_objectt> result);
 
 void EXPECT_TOP(std::shared_ptr<const value_set_abstract_objectt> &result);