Enable mixed value-set and interval expression evaluation

rewrite_expression has, incorrectly, expected every term in the
rewritten expression to be a constant. When there are intervals in play,
this is clearly not the case.

When we encounter an interval, don't attempt to coerce it to a constant
expression, simply use the existing operand.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -556,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>{};

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

@@ -287,6 +287,46 @@ SCENARIO(
       }
     }
   }
+  GIVEN("adding an interval and a value-set of constants")
+  {
+    WHEN("[2,2] + { 1 }")
+    {
+      auto op1 = make_interval(val2, val2, environment, ns);
+      auto op2 = make_value_set(val1, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[3,3]}")
+      {
+        EXPECT(result, {constant_interval_exprt(val3, val3)});
+      }
+    }
+    WHEN("[2,4] + { 1 }")
+    {
+      auto op1 = make_interval(val2, val4, environment, ns);
+      auto op2 = make_value_set(val1, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[3,5]}")
+      {
+        EXPECT(result, {constant_interval_exprt(val3, val5)});
+      }
+    }
+    WHEN("[1,2] + { 1, 2, 3 }")
+    {
+      auto op1 = make_interval(val1, val2, environment, ns);
+      auto op2 = make_value_set({val1, val2, val3}, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[2,3], [3,4], [4,5]}")
+      {
+        EXPECT(
+          result,
+          {constant_interval_exprt(val2, val3),
+           constant_interval_exprt(val3, val4),
+           constant_interval_exprt(val4, val5)});
+      }
+    }
+  }
 
   GIVEN("adding two value_sets")
   {
@@ -371,6 +411,46 @@ SCENARIO(
       }
     }
   }
+  GIVEN("adding a value-set of constants and an interval")
+  {
+    WHEN("{ 1 } + [2,2]")
+    {
+      auto op1 = make_value_set(val1, environment, ns);
+      auto op2 = make_interval(val2, val2, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[3,3]}")
+      {
+        EXPECT(result, {constant_interval_exprt(val3, val3)});
+      }
+    }
+    WHEN("{ 1 } + [2,4]")
+    {
+      auto op1 = make_value_set(val1, environment, ns);
+      auto op2 = make_interval(val2, val4, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[3,5]}")
+      {
+        EXPECT(result, {constant_interval_exprt(val3, val5)});
+      }
+    }
+    WHEN("{ 1, 2, 3 } + [1,2]")
+    {
+      auto op1 = make_value_set({val1, val2, val3}, environment, ns);
+      auto op2 = make_interval(val1, val2, environment, ns);
+      auto result = add_as_value_set(op1, op2, environment, ns);
+
+      THEN("= {[2,3], [3,4], [4,5]}")
+      {
+        EXPECT(
+          result,
+          {constant_interval_exprt(val2, val3),
+           constant_interval_exprt(val3, val4),
+           constant_interval_exprt(val4, val5)});
+      }
+    }
+  }
   GIVEN("multiple operands")
   {
     WHEN("{ 1, 2, 3 } + 1 + 1")

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

@@ -93,13 +93,22 @@ bool set_contains(const abstract_object_sett &set, const exprt &val)
   auto i = std::find_if(
     set.begin(), set.end(), [&val](const abstract_object_pointert &lhs) {
       auto l = lhs->to_constant();
+      auto interval =
+        std::dynamic_pointer_cast<const interval_abstract_valuet>(lhs);
+      if(interval)
+        l = interval->to_interval();
       return l == val;
     });
   return i != set.end();
 }
 
-std::string expr_to_str(const exprt &expr)
+static std::string interval_to_str(const constant_interval_exprt &expr);
+
+static std::string expr_to_str(const exprt &expr)
 {
+  if(expr.id() == ID_constant_interval)
+    return interval_to_str(to_constant_interval_expr(expr));
+
   auto st = symbol_tablet{};
   auto ns = namespacet{st};
   auto expr_str = std::string{};
@@ -110,6 +119,13 @@ std::string expr_to_str(const exprt &expr)
   return expr_str;
 }
 
+static std::string interval_to_str(const constant_interval_exprt &expr)
+{
+  auto lower = expr_to_str(expr.get_lower());
+  auto upper = expr_to_str(expr.get_upper());
+  return "[" + lower + "," + upper + "]";
+}
+
 template <class Container, typename UnaryOp>
 std::string container_to_str(const Container &con, UnaryOp unaryOp)
 {
@@ -125,7 +141,9 @@ std::string container_to_str(const Container &con, UnaryOp unaryOp)
 std::string set_to_str(const abstract_object_sett &set)
 {
   return container_to_str(set, [](const abstract_object_pointert &lhs) {
-    return expr_to_str(lhs->to_constant());
+    auto i = std::dynamic_pointer_cast<const interval_abstract_valuet>(lhs);
+    return i ? interval_to_str(i->to_interval())
+             : expr_to_str(lhs->to_constant());
   });
 }