widening interval_abstract_value lower_bound can be minimum

If new lower bound is already at minimum, or underflows, then
explicitly set to min_exprt(type)

Author: jezhiggins

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -346,7 +346,14 @@ void interval_abstract_valuet::output(
   }
 }
 
-exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns);
+exprt extend_lower_bound(
+  const exprt &lower_bound,
+  const exprt &range,
+  const namespacet &ns);
+exprt extend_upper_bound(
+  const exprt &upper_bound,
+  const exprt &range,
+  const namespacet &ns);
 
 abstract_object_pointert widening_merge(
   const constant_interval_exprt &lhs,
@@ -361,37 +368,61 @@ abstract_object_pointert widening_merge(
   auto dummy_namespace = namespacet{dummy_symbol_table};
 
   auto range = plus_exprt(
-      minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
+    minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
 
   // should extend lower bound?
-  if(rhs.get_lower() < lhs.get_lower()) lower_bound =
-    simplify_expr(minus_exprt(lower_bound, range), dummy_namespace);
+  if(constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower()))
+    lower_bound = extend_lower_bound(lower_bound, range, dummy_namespace);
   // should extend upper bound?
-  if(lhs.get_upper() < rhs.get_upper())
+  if(constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper()))
     upper_bound = extend_upper_bound(upper_bound, range, dummy_namespace);
 
   // new interval ...
   auto new_interval = constant_interval_exprt(lower_bound, upper_bound);
   return interval_abstract_valuet::make_interval(new_interval);
 }
 
-bool has_overflowed(const exprt& value)
+bool has_underflowed(const exprt &value)
 {
-  return constant_interval_exprt::less_than(value, from_integer(0, value.type()));
+  return constant_interval_exprt::greater_than(
+    value, from_integer(0, value.type()));
 }
+bool has_overflowed(const exprt &value)
+{
+  return constant_interval_exprt::less_than(
+    value, from_integer(0, value.type()));
+}
+
+exprt extend_lower_bound(
+  const exprt &lower_bound,
+  const exprt &range,
+  const namespacet &ns)
+{
+  auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range), ns);
 
-exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns)
+  if(
+    constant_interval_exprt::contains_extreme(new_lower_bound) ||
+    has_underflowed(new_lower_bound))
+    return min_exprt(lower_bound.type());
+
+  return new_lower_bound;
+}
+
+exprt extend_upper_bound(
+  const exprt &upper_bound,
+  const exprt &range,
+  const namespacet &ns)
 {
   auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range), ns);
 
-  if (constant_interval_exprt::contains_extreme(new_upper_bound) ||
-     has_overflowed(new_upper_bound))
+  if(
+    constant_interval_exprt::contains_extreme(new_upper_bound) ||
+    has_overflowed(new_upper_bound))
     return max_exprt(upper_bound.type());
 
   return new_upper_bound;
 }
 
-
 abstract_object_pointert interval_abstract_valuet::merge_with_value(
   const abstract_value_pointert &other,
   const widen_modet &widen_mode) const

unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp

@@ -13,8 +13,9 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
 
-static merge_result<const interval_abstract_valuet>
-widening_merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
+static merge_result<const interval_abstract_valuet> widening_merge(
+  const abstract_object_pointert &op1,
+  const abstract_object_pointert &op2)
 {
   auto result = abstract_objectt::merge(op1, op2, widen_modet::could_widen);
 
@@ -319,7 +320,7 @@ SCENARIO(
     }
     WHEN("merging [0, 1] with [1, very_large]")
     {
-      auto veryLarge = from_integer(2<<29, type);
+      auto veryLarge = from_integer(2 << 29, type);
       auto op1 = make_interval(val0, val1, environment, ns);
       auto op2 = make_interval(val1, veryLarge, environment, ns);
 
@@ -330,5 +331,113 @@ SCENARIO(
         EXPECT_MODIFIED(merged, val0, valMax);
       }
     }
+
+    WHEN("merging [1, 10] with [MIN, 1]")
+    {
+      auto op1 = make_interval(val1, val10, environment, ns);
+      auto op2 = make_interval(valMin, val1, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is [MIN, 10]")
+      {
+        EXPECT_MODIFIED(merged, valMin, val10);
+      }
+    }
+    WHEN("merging [0, 1] with [-very_large, 1]")
+    {
+      auto veryLargeMinus = from_integer(-(2 << 29), type);
+      auto op1 = make_interval(val0, val1, environment, ns);
+      auto op2 = make_interval(veryLargeMinus, val1, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is [MIN, 1]")
+      {
+        EXPECT_MODIFIED(merged, valMin, val1);
+      }
+    }
+
+    WHEN("merging [1, MAX] with [MIN, 1]")
+    {
+      auto op1 = make_interval(val1, valMax, environment, ns);
+      auto op2 = make_interval(valMin, val1, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is TOP - ie [MIN, MAX]")
+      {
+        EXPECT_MODIFIED_TOP(merged);
+      }
+    }
+    WHEN("merging [MIN, 1] with [1, MAX]")
+    {
+      auto op1 = make_interval(valMin, val1, environment, ns);
+      auto op2 = make_interval(val1, valMax, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is TOP - ie [MIN, MAX]")
+      {
+        EXPECT_MODIFIED_TOP(merged);
+      }
+    }
+    WHEN("merging [0, very_large] with [-very_large, 0]")
+    {
+      auto veryLarge = from_integer(2 << 29, type);
+      auto veryLargeMinus = from_integer(-(2 << 29), type);
+      auto op1 = make_interval(val0, veryLarge, environment, ns);
+      auto op2 = make_interval(veryLargeMinus, val0, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is [MIN, very_large]")
+      {
+        EXPECT_MODIFIED(merged, valMin, veryLarge);
+      }
+    }
+    WHEN("merging [-very_large, 0] with [0, very_large]")
+    {
+      auto veryLarge = from_integer(2 << 29, type);
+      auto veryLargeMinus = from_integer(-(2 << 29), type);
+      auto op1 = make_interval(veryLargeMinus, val0, environment, ns);
+      auto op2 = make_interval(val0, veryLarge, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is [-very_large, MAX]")
+      {
+        EXPECT_MODIFIED(merged, veryLargeMinus, valMax);
+      }
+    }
+
+    WHEN("merging [-very_large, very_large] with [0, 1]")
+    {
+      auto veryLarge = from_integer(2 << 29, type);
+      auto veryLargeMinus = from_integer(-(2 << 29), type);
+      auto op1 = make_interval(veryLargeMinus, veryLarge, environment, ns);
+      auto op2 = make_interval(val0, val1, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is [-very_large, very_large]")
+      {
+        EXPECT_UNMODIFIED(merged, veryLargeMinus, veryLarge);
+      }
+    }
+    WHEN("merging [0, 1] with [-very_large, very_large]")
+    {
+      auto veryLarge = from_integer(2 << 29, type);
+      auto veryLargeMinus = from_integer(-(2 << 29), type);
+      auto op1 = make_interval(val0, val1, environment, ns);
+      auto op2 = make_interval(veryLargeMinus, veryLarge, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("result is TOP, ie [MIN, MAX]")
+      {
+        EXPECT_MODIFIED_TOP(merged);
+      }
+    }
   }
 }