More tests to confirm value-sets of intervals behaviour

Author: jezhiggins

unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp

@@ -451,6 +451,155 @@ SCENARIO(
       }
     }
   }
+  GIVEN("adding a value-set of intervals and constants with a constant")
+  {
+    auto interval12 = constant_interval_exprt(val1, val2);
+    auto interval23 = constant_interval_exprt(val2, val3);
+    auto interval34 = constant_interval_exprt(val3, val4);
+    auto interval45 = constant_interval_exprt(val4, val5);
+
+    WHEN("{ [1,2] } + 2")
+    {
+      auto op1 = make_value_set(interval12, environment, ns);
+      auto op2 = make_constant(val2, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [3,4] }")
+      {
+        EXPECT(result, {interval34});
+      }
+    }
+    WHEN("{ [1,2], 3 } + 2")
+    {
+      auto op1 = make_value_set({interval12, val3}, environment, ns);
+      auto op2 = make_constant(val2, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [3,4], 5 }")
+      {
+        EXPECT(result, {interval34, val5});
+      }
+    }
+    WHEN("{ [1,2], [2,3] } + 2")
+    {
+      auto op1 = make_value_set({interval12, interval23}, environment, ns);
+      auto op2 = make_constant(val2, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [3,4], [4,5] }")
+      {
+        EXPECT(result, {interval34, interval45});
+      }
+    }
+  }
+  GIVEN("adding a value-set of intervals and constants with an interval")
+  {
+    auto interval12 = constant_interval_exprt(val1, val2);
+    auto interval23 = constant_interval_exprt(val2, val3);
+    auto interval34 = constant_interval_exprt(val3, val4);
+    auto interval45 = constant_interval_exprt(val4, val5);
+    auto interval24 = constant_interval_exprt(val2, val4);
+    auto interval35 = constant_interval_exprt(val3, val5);
+
+    WHEN("{ [1,2] } + [1,2]")
+    {
+      auto op1 = make_value_set(interval12, environment, ns);
+      auto op2 = make_interval(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4] }")
+      {
+        EXPECT(result, {interval24});
+      }
+    }
+    WHEN("{ [1,2], 1 } + [1,2]")
+    {
+      auto op1 = make_value_set({interval12, val1}, environment, ns);
+      auto op2 = make_interval(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4], [2,3] }")
+      {
+        EXPECT(result, {interval24, interval23});
+      }
+    }
+    WHEN("{ [1,2], [2,3] } + [1,2]")
+    {
+      auto op1 = make_value_set({interval12, interval23}, environment, ns);
+      auto op2 = make_interval(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4], [3,5] }")
+      {
+        EXPECT(result, {interval24, interval35});
+      }
+    }
+  }
+  GIVEN("adding a value-set of intervals and constants with a value-set")
+  {
+    auto interval12 = constant_interval_exprt(val1, val2);
+    auto interval23 = constant_interval_exprt(val2, val3);
+    auto interval34 = constant_interval_exprt(val3, val4);
+    auto interval45 = constant_interval_exprt(val4, val5);
+    auto interval24 = constant_interval_exprt(val2, val4);
+    auto interval35 = constant_interval_exprt(val3, val5);
+
+    WHEN("{ [1,2] } + { 1, 2 }")
+    {
+      auto op1 = make_value_set(interval12, environment, ns);
+      auto op2 = make_value_set({val1, val2}, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,3], [3,4] }")
+      {
+        EXPECT(result, {interval23, interval34});
+      }
+    }
+    WHEN("{ [1,2] } + { [1,2] }")
+    {
+      auto op1 = make_value_set(interval12, environment, ns);
+      auto op2 = make_value_set(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4] }")
+      {
+        EXPECT(result, {interval24});
+      }
+    }
+    WHEN("{ [1,2], 1 } + { [1,2] }")
+    {
+      auto op1 = make_value_set({interval12, val1}, environment, ns);
+      auto op2 = make_value_set(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4], [2,3] }")
+      {
+        EXPECT(result, {interval24, interval23});
+      }
+    }
+    WHEN("{ [1,2], [2,3] } + { [1,2] }")
+    {
+      auto op1 = make_value_set({interval12, interval23}, environment, ns);
+      auto op2 = make_interval(interval12, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4], [3,5] }")
+      {
+        EXPECT(result, {interval24, interval35});
+      }
+    }
+    WHEN("{ [1,2], 1 } + { [1,2], 1 }")
+    {
+      auto op1 = make_value_set({interval12, val1}, environment, ns);
+      auto op2 = make_value_set({interval12, val1}, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= { [2,4], [2,3], [2,3], 2 }")
+      { // duplicate interval ok as first pass. Will be eliminated in due course.
+        EXPECT(result, {interval24, interval23, interval23, val2});
+      }
+    }
+  }
   GIVEN("multiple operands")
   {
     WHEN("{ 1, 2, 3 } + 1 + 1")

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

@@ -13,12 +13,6 @@
 #include <util/mathematical_types.h>
 #include <util/string_utils.h>
 
-std::shared_ptr<value_set_abstract_objectt>
-make_value_set(exprt val, abstract_environmentt &env, namespacet &ns)
-{
-  return std::make_shared<value_set_abstract_objectt>(val, env, ns);
-}
-
 std::shared_ptr<const constant_abstract_valuet>
 make_constant(exprt val, abstract_environmentt &env, namespacet &ns)
 {
@@ -38,29 +32,51 @@ std::shared_ptr<const constant_abstract_valuet> make_bottom_constant()
 }
 
 std::shared_ptr<const interval_abstract_valuet> make_interval(
-  exprt vall,
-  exprt valh,
+  const exprt &vall,
+  const exprt &valh,
   abstract_environmentt &env,
   namespacet &ns)
 {
   auto interval = constant_interval_exprt(vall, valh);
-  return std::make_shared<interval_abstract_valuet>(interval, env, ns);
+  return make_interval(interval, env, ns);
+}
+
+std::shared_ptr<const interval_abstract_valuet> make_interval(
+  const constant_interval_exprt &val,
+  abstract_environmentt &env,
+  namespacet &ns)
+{
+  return std::make_shared<interval_abstract_valuet>(val, env, ns);
 }
 
 std::shared_ptr<const interval_abstract_valuet> make_top_interval()
 {
   return std::make_shared<interval_abstract_valuet>(
     signedbv_typet(32), true, false);
 }
+
+std::shared_ptr<value_set_abstract_objectt>
+make_value_set(exprt val, abstract_environmentt &env, namespacet &ns)
+{
+  auto vals = std::vector<exprt>{val};
+  return make_value_set(vals, env, ns);
+}
+
 std::shared_ptr<value_set_abstract_objectt> make_value_set(
   const std::vector<exprt> &vals,
   abstract_environmentt &env,
   namespacet &ns)
 {
   auto initial_values = abstract_object_sett{};
   for(auto v : vals)
-    initial_values.insert(make_constant(v, env, ns));
-  auto vs = make_value_set(vals[0], env, ns);
+  {
+    if(v.id() == ID_constant_interval)
+      initial_values.insert(
+        std::make_shared<interval_abstract_valuet>(v, env, ns));
+    else
+      initial_values.insert(make_constant(v, env, ns));
+  }
+  auto vs = std::make_shared<value_set_abstract_objectt>(vals[0], env, ns);
   vs->set_values(initial_values);
   return vs;
 }

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h

@@ -17,8 +17,12 @@ std::shared_ptr<const constant_abstract_valuet> make_top_constant();
 std::shared_ptr<const constant_abstract_valuet> make_bottom_constant();
 
 std::shared_ptr<const interval_abstract_valuet> make_interval(
-  exprt vall,
-  exprt valh,
+  const exprt &vall,
+  const exprt &valh,
+  abstract_environmentt &env,
+  namespacet &ns);
+std::shared_ptr<const interval_abstract_valuet> make_interval(
+  const constant_interval_exprt &val,
   abstract_environmentt &env,
   namespacet &ns);
 std::shared_ptr<const interval_abstract_valuet> make_top_interval();