Add abstract_value_objectt::to_interval()

Analogous to to_constant, it returns a constant_interval_exprt that
expresses the range of the value. For constants the interval is across
whatever the constant is, for intervals it is their interval(!) and for
value_sets it is the interval between the smallest and largest values in
the set.

Used to intervals to merge with any other value type.

This commit includes unit tests for interval_abstract_objectt::merge.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_object_set.cpp

@@ -37,7 +37,7 @@ void abstract_object_sett::output(
   join_strings(out, output_values.begin(), output_values.end(), ", ");
 }
 
-abstract_object_pointert abstract_object_sett::to_interval()
+constant_interval_exprt abstract_object_sett::to_interval() const
 {
   PRECONDITION(!values.empty());
 
@@ -49,6 +49,5 @@ abstract_object_pointert abstract_object_sett::to_interval()
     lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
     upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
   }
-  return std::make_shared<interval_abstract_valuet>(
-    constant_interval_exprt(lower_expr, upper_expr));
+  return constant_interval_exprt(lower_expr, upper_expr);
 }

src/analyses/variable-sensitivity/abstract_object_set.h

@@ -80,10 +80,9 @@ class abstract_object_sett
   void
   output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
 
-  /// Cast the set of values \p other_values to an interval.
-  /// \param other_values: the value-set to be abstracted into an interval
-  /// \return the interval-abstract-object containing \p other_values
-  abstract_object_pointert to_interval();
+  /// Calculate the set of values as an interval.
+  /// \return the constant_interval_exprt bounding the values
+  constant_interval_exprt to_interval() const;
 
 private:
   value_sett values;

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -631,11 +631,17 @@ class value_set_evaluator
     auto unwrapped_values = unwrap_and_extract_values(new_values);
 
     if(unwrapped_values.size() > value_set_abstract_objectt::max_value_set_size)
-      return unwrapped_values.to_interval();
+      return make_interval(unwrapped_values);
 
     return make_value_set(unwrapped_values);
   }
 
+  static abstract_object_pointert
+  make_interval(const abstract_object_sett &values)
+  {
+    return std::make_shared<interval_abstract_valuet>(values.to_interval());
+  }
+
   static abstract_object_pointert
   make_value_set(const abstract_object_sett &values)
   {

src/analyses/variable-sensitivity/abstract_value_object.h

@@ -13,6 +13,7 @@
 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
 
 #include <analyses/variable-sensitivity/abstract_object.h>
+#include <util/interval.h>
 
 class abstract_value_tag
 {
@@ -265,6 +266,8 @@ class abstract_value_objectt : public abstract_objectt,
     return value_ranget(value_range_implementation());
   }
 
+  virtual constant_interval_exprt to_interval() const = 0;
+
   /// Interface for transforms
   ///
   /// \param expr: the expression to evaluate and find the result of it.
@@ -293,4 +296,4 @@ class abstract_value_objectt : public abstract_objectt,
 
 using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;
 
-#endif
+#endif

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -91,6 +91,11 @@ exprt constant_abstract_valuet::to_constant() const
   }
 }
 
+constant_interval_exprt constant_abstract_valuet::to_interval() const
+{
+  return constant_interval_exprt(value, value);
+}
+
 void constant_abstract_valuet::output(
   std::ostream &out,
   const ai_baset &ai,

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -36,6 +36,7 @@ class constant_abstract_valuet : public abstract_value_objectt
   value_range_implementation_ptrt value_range_implementation() const override;
 
   exprt to_constant() const override;
+  constant_interval_exprt to_interval() const override;
 
   void output(
     std::ostream &out,

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -329,8 +329,8 @@ void interval_abstract_valuet::output(
 abstract_object_pointert
 interval_abstract_valuet::merge(abstract_object_pointert other) const
 {
-  interval_abstract_value_pointert cast_other =
-    std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
+  abstract_value_pointert cast_other =
+    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
   if(cast_other)
   {
     return merge_intervals(cast_other);
@@ -342,31 +342,31 @@ interval_abstract_valuet::merge(abstract_object_pointert other) const
 }
 
 /// Merge another interval abstract object with this one
-/// \param other The interval abstract object to merge with
+/// \param other The abstract value object to merge with
 /// \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 interval_abstract_valuet::merge_intervals(
-  interval_abstract_value_pointert other) const
+abstract_object_pointert
+interval_abstract_valuet::merge_intervals(abstract_value_pointert &other) const
 {
-  if(is_bottom() || other->interval.contains(interval))
-  {
-    return other;
-  }
-  else if(other->is_bottom() || interval.contains(other->interval))
-  {
+  if(other->is_bottom())
     return shared_from_this();
-  }
-  else
-  {
-    return std::make_shared<interval_abstract_valuet>(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())));
-  }
+
+  auto other_interval = other->to_interval();
+
+  if(is_bottom())
+    return std::make_shared<interval_abstract_valuet>(other_interval);
+
+  if(interval.contains(other_interval))
+    return shared_from_this();
+
+  return std::make_shared<interval_abstract_valuet>(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())));
 }
 
 abstract_object_pointert

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -41,7 +41,7 @@ class interval_abstract_valuet : public abstract_value_objectt
   value_range_implementation_ptrt value_range_implementation() const override;
 
   exprt to_constant() const override;
-  const constant_interval_exprt &to_interval() const
+  constant_interval_exprt to_interval() const override
   {
     return interval;
   }
@@ -68,7 +68,7 @@ class interval_abstract_valuet : public abstract_value_objectt
     sharing_ptrt<interval_abstract_valuet>;
 
   abstract_object_pointert
-  merge_intervals(interval_abstract_value_pointert other) const;
+  merge_intervals(abstract_value_pointert &other) const;
   abstract_object_pointert
   meet_intervals(interval_abstract_value_pointert other) const;
 

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -9,6 +9,7 @@
 /// \file
 /// Value Set Abstract Object
 
+#include "interval_abstract_value.h"
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
@@ -162,6 +163,18 @@ value_set_abstract_objectt::value_range_implementation() const
   return make_value_set_value_range(values);
 }
 
+exprt value_set_abstract_objectt::to_constant() const
+{
+  verify();
+  return values.size() == 1 ? (*values.begin())->to_constant()
+                            : abstract_objectt::to_constant();
+}
+
+constant_interval_exprt value_set_abstract_objectt::to_interval() const
+{
+  return values.to_interval();
+}
+
 abstract_object_pointert value_set_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
@@ -199,7 +212,8 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values(
 
   if(unwrapped_values.size() > max_value_set_size)
   {
-    return unwrapped_values.to_interval();
+    return std::make_shared<interval_abstract_valuet>(
+      unwrapped_values.to_interval());
   }
   //if(unwrapped_values.size() == 1)
   //{

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -36,12 +36,8 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   value_range_implementation_ptrt value_range_implementation() const override;
 
   /// \copydoc abstract_objectt::to_constant
-  exprt to_constant() const override
-  {
-    verify();
-    return values.size() == 1 ? (*values.begin())->to_constant()
-                              : abstract_objectt::to_constant();
-  }
+  exprt to_constant() const override;
+  constant_interval_exprt to_interval() const override;
 
   /// Getter for the set of stored abstract objects.
   /// \return the values represented by this abstract object