Widen merged intervals when widen_modet is could_widen

Extends upper and/or lower bound by the width of the interval.

Does not widen in lhs value would be unchanged in non-widening merge -
ie only widens if interval is extended by the merge.

Author: jezhiggins

regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc

@@ -4,5 +4,4 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^main::1::1::i .* \[5, 5\] @ \[6\]
-^main::1::p .* \[2, 20\] @ \[5\]
 --

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -254,6 +254,13 @@ interval_abstract_valuet::interval_abstract_valuet(
 {
 }
 
+interval_abstract_valuet::interval_abstract_valuet(
+  const exprt &lower,
+  const exprt &upper)
+  : interval_abstract_valuet(constant_interval_exprt(lower, upper))
+{
+}
+
 interval_abstract_valuet::interval_abstract_valuet(
   const exprt &e,
   const abstract_environmentt &environment,
@@ -344,14 +351,34 @@ void interval_abstract_valuet::output(
   }
 }
 
-/// Merge another interval abstract object with this one
-/// \param other The abstract value object to merge with
-/// \param widen_mode: Indicates if this is a widening merge
-/// \return This if the other interval is subsumed by this,
-///          other if this is subsumed by other.
-///          Otherwise, a new interval abstract object
-///          with the smallest interval that subsumes both
-///          this and other
+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);
+
+  // new interval ...
+  auto new_interval = constant_interval_exprt(lower_bound, upper_bound);
+  return make_interval(new_interval);
+}
+
 abstract_object_pointert interval_abstract_valuet::merge_with_value(
   const abstract_value_pointert &other,
   const widen_modet &widen_mode) const
@@ -367,19 +394,17 @@ abstract_object_pointert interval_abstract_valuet::merge_with_value(
   if(interval.contains(other_interval))
     return shared_from_this();
 
-  return make_interval(constant_interval_exprt(
-    constant_interval_exprt::get_min(
-      interval.get_lower(), other_interval.get_lower()),
-    constant_interval_exprt::get_max(
-      interval.get_upper(), other_interval.get_upper())));
+  if(widen_mode == widen_modet::could_widen)
+    return widening_merge(interval, other_interval);
+
+  auto lower_bound = constant_interval_exprt::get_min(
+    interval.get_lower(), other_interval.get_lower());
+  auto upper_bound = constant_interval_exprt::get_max(
+    interval.get_upper(), other_interval.get_upper());
+
+  return make_interval(lower_bound, upper_bound);
 }
 
-/// Meet another interval abstract object with this one
-/// \param other The interval abstract object to meet with
-/// \return This if the other interval subsumes this,
-///          other if this subsumes other.
-///          Otherwise, a new interval abstract object
-///          with the intersection interval (of this and other)
 abstract_object_pointert interval_abstract_valuet::meet_with_value(
   const abstract_value_pointert &other) const
 {

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -27,6 +27,7 @@ class interval_abstract_valuet : public abstract_value_objectt
   interval_abstract_valuet(const typet &t, bool tp, bool bttm);
 
   explicit interval_abstract_valuet(const constant_interval_exprt &e);
+  interval_abstract_valuet(const exprt &lower, const exprt &upper);
 
   interval_abstract_valuet(
     const exprt &e,
@@ -63,10 +64,24 @@ class interval_abstract_valuet : public abstract_value_objectt
 protected:
   CLONE
 
+  /// Merge another interval abstract object with this one
+  /// \param other The abstract value object to merge with
+  /// \param widen_mode: Indicates if this is a widening merge
+  /// \return This if the other interval is subsumed by this,
+  ///          other if this is subsumed by other.
+  ///          Otherwise, a new interval abstract object
+  ///          with the smallest interval that subsumes both
+  ///          this and other
   abstract_object_pointert merge_with_value(
     const abstract_value_pointert &other,
     const widen_modet &widen_mode) const override;
 
+  /// Meet another interval abstract object with this one
+  /// \param other The interval abstract object to meet with
+  /// \return This if the other interval subsumes this,
+  ///          other if this subsumes other.
+  ///          Otherwise, a new interval abstract object
+  ///          with the intersection interval (of this and other)
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 

unit/Makefile

@@ -23,6 +23,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/eval-member-access.cpp \
        analyses/variable-sensitivity/interval_abstract_value/meet.cpp \
        analyses/variable-sensitivity/interval_abstract_value/merge.cpp \
+       analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \
        analyses/variable-sensitivity/last_written_location.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \

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

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
- Module: Unit tests for intervalabstract_valuet::merge
+ Module: Unit tests for interval_abstract_valuet::merge
 
  Author: Jez Higgins.