VSD - correct widening merge to handle extreme values

src/analyses/Makefile

@@ -52,6 +52,7 @@ SRC = ai.cpp \
       variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
       variable-sensitivity/variable_sensitivity_domain.cpp \
       variable-sensitivity/variable_sensitivity_object_factory.cpp \
+      variable-sensitivity/widened_range.cpp \
       variable-sensitivity/write_location_context.cpp \
       variable-sensitivity/write_stack.cpp \
       variable-sensitivity/write_stack_entry.cpp \

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -17,6 +17,7 @@
 #include "abstract_environment.h"
 #include "abstract_object_statistics.h"
 #include "interval_abstract_value.h"
+#include "widened_range.h"
 
 static index_range_implementation_ptrt make_interval_index_range(
   const constant_interval_exprt &interval,
@@ -350,27 +351,11 @@ abstract_object_pointert widening_merge(
   const constant_interval_exprt &lhs,
   const constant_interval_exprt &rhs)
 {
-  auto lower_bound =
-    constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
-  auto upper_bound =
-    constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
-  auto range = plus_exprt(
-    minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
-
-  auto dummy_symbol_table = symbol_tablet{};
-  auto dummy_namespace = namespacet{dummy_symbol_table};
-
-  // should extend lower bound?
-  if(rhs.get_lower() < lhs.get_lower())
-    lower_bound =
-      simplify_expr(minus_exprt(lower_bound, range), dummy_namespace);
-  // should extend upper bound?
-  if(lhs.get_upper() < rhs.get_upper())
-    upper_bound =
-      simplify_expr(plus_exprt(upper_bound, range), dummy_namespace);
+  auto widened = widened_ranget(lhs, rhs);
 
   // new interval ...
-  auto new_interval = constant_interval_exprt(lower_bound, upper_bound);
+  auto new_interval = constant_interval_exprt(
+    widened.widened_lower_bound, widened.widened_upper_bound);
   return interval_abstract_valuet::make_interval(new_interval);
 }
 

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -14,6 +14,7 @@
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/interval_abstract_value.h>
 #include <analyses/variable-sensitivity/value_set_abstract_object.h>
+#include <analyses/variable-sensitivity/widened_range.h>
 
 #include <util/arith_tools.h>
 #include <util/make_unique.h>
@@ -414,6 +415,7 @@ static abstract_object_sett compact_values(const abstract_object_sett &values)
 }
 
 static exprt eval_expr(const exprt &e);
+static bool is_eq(const exprt &lhs, const exprt &rhs);
 static bool is_le(const exprt &lhs, const exprt &rhs);
 static abstract_object_sett collapse_values_in_intervals(
   const abstract_object_sett &values,
@@ -446,6 +448,8 @@ void collapse_overlapping_intervals(
     intervals.begin(),
     intervals.end(),
     [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
+      if(is_eq(lhs.get_lower(), rhs.get_lower()))
+        return is_le(lhs.get_upper(), rhs.get_upper());
       return is_le(lhs.get_lower(), rhs.get_lower());
     });
 
@@ -556,10 +560,14 @@ static exprt eval_expr(const exprt &e)
   return simplify_expr(e, ns);
 }
 
+static bool is_eq(const exprt &lhs, const exprt &rhs)
+{
+  return constant_interval_exprt::equal(lhs, rhs);
+}
+
 static bool is_le(const exprt &lhs, const exprt &rhs)
 {
-  auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs);
-  return eval_expr(is_le_expr).is_true();
+  return constant_interval_exprt::less_than_or_equal(lhs, rhs);
 }
 
 static abstract_object_sett widen_value_set(
@@ -572,41 +580,34 @@ static abstract_object_sett widen_value_set(
 
   auto widened_ends = std::vector<constant_interval_exprt>{};
 
-  auto lower_bound =
-    constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
-  auto upper_bound =
-    constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
-  auto range = plus_exprt(
-    minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
-
-  auto symbol_table = symbol_tablet{};
-  auto ns = namespacet{symbol_table};
+  auto range = widened_ranget(lhs, rhs);
 
   // should extend lower bound?
-  if(rhs.get_lower() < lhs.get_lower())
+  if(range.is_lower_widened)
   {
-    auto widened_lower_bound = constant_interval_exprt(
-      simplify_expr(minus_exprt(lower_bound, range), ns), lower_bound);
-    widened_ends.push_back(widened_lower_bound);
+    auto extended_lower_bound =
+      constant_interval_exprt(range.widened_lower_bound, range.lower_bound);
+
+    widened_ends.push_back(extended_lower_bound);
     for(auto &obj : values)
     {
       auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
       auto as_expr = value->to_interval();
-      if(is_le(as_expr.get_lower(), lower_bound))
+      if(is_le(as_expr.get_lower(), range.lower_bound))
         widened_ends.push_back(as_expr);
     }
   }
   // should extend upper bound?
-  if(lhs.get_upper() < rhs.get_upper())
+  if(range.is_upper_widened)
   {
-    auto widened_upper_bound = constant_interval_exprt(
-      upper_bound, simplify_expr(plus_exprt(upper_bound, range), ns));
-    widened_ends.push_back(widened_upper_bound);
+    auto extended_upper_bound =
+      constant_interval_exprt(range.upper_bound, range.widened_upper_bound);
+    widened_ends.push_back(extended_upper_bound);
     for(auto &obj : values)
     {
       auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
       auto as_expr = value->to_interval();
-      if(is_le(upper_bound, as_expr.get_upper()))
+      if(is_le(range.upper_bound, as_expr.get_upper()))
         widened_ends.push_back(as_expr);
     }
   }

src/analyses/variable-sensitivity/widened_range.cpp

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+ Module: helper for extending intervals during widening merges
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include "widened_range.h"
+#include <util/simplify_expr.h>
+
+static bool has_underflowed(const exprt &value)
+{
+  return constant_interval_exprt::greater_than(
+    value, from_integer(0, value.type()));
+}
+static bool has_overflowed(const exprt &value, const exprt &initial_value)
+{
+  return constant_interval_exprt::less_than(value, initial_value);
+}
+
+exprt widened_ranget::widen_lower_bound() const
+{
+  if(!is_lower_widened)
+    return lower_bound;
+
+  auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range_), 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 widened_ranget::widen_upper_bound() const
+{
+  if(!is_upper_widened)
+    return upper_bound;
+
+  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, upper_bound))
+    return max_exprt(upper_bound.type());
+
+  return new_upper_bound;
+}

src/analyses/variable-sensitivity/widened_range.h

@@ -0,0 +1,58 @@
+/*******************************************************************\
+
+ Module: helper for extending intervals during widening merges
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
+#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
+
+#include <util/arith_tools.h>
+#include <util/interval.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+class widened_ranget
+{
+public:
+  widened_ranget(
+    const constant_interval_exprt &lhs,
+    const constant_interval_exprt &rhs)
+    : is_lower_widened(
+        constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())),
+      is_upper_widened(
+        constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())),
+      lower_bound(
+        constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())),
+      upper_bound(
+        constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())),
+      ns_(symbol_tablet{}),
+      range_(plus_exprt(
+        minus_exprt(upper_bound, lower_bound),
+        from_integer(1, lhs.type()))),
+      widened_lower_bound(widen_lower_bound()),
+      widened_upper_bound(widen_upper_bound())
+  {
+  }
+
+  const bool is_lower_widened;
+  const bool is_upper_widened;
+  const exprt lower_bound;
+  const exprt upper_bound;
+
+private:
+  namespacet ns_;
+  exprt range_;
+
+public:
+  const exprt widened_lower_bound;
+  const exprt widened_upper_bound;
+
+private:
+  exprt widen_lower_bound() const;
+  exprt widen_upper_bound() const;
+};
+
+#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H