Merge pull request #5979 from jezhiggins/vsd-widening

Vsd - merge values

Author: martin-cs

src/analyses/variable-sensitivity/abstract_object.h

@@ -456,6 +456,10 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
     top = false;
     this->set_not_top_internal();
   }
+  void set_not_bottom()
+  {
+    bottom = false;
+  }
 };
 
 struct abstract_hashert

src/analyses/variable-sensitivity/abstract_object_set.cpp

@@ -37,18 +37,24 @@ 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());
 
-  exprt lower_expr = first()->to_constant();
-  exprt upper_expr = first()->to_constant();
+  const auto &initial =
+    std::dynamic_pointer_cast<const abstract_value_objectt>(first());
+
+  exprt lower_expr = initial->to_interval().get_lower();
+  exprt upper_expr = initial->to_interval().get_upper();
   for(const auto &value : values)
   {
-    const auto &value_expr = value->to_constant();
-    lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
-    upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
+    const auto &v =
+      std::dynamic_pointer_cast<const abstract_value_objectt>(value);
+    const auto &value_expr = v->to_interval();
+    lower_expr =
+      constant_interval_exprt::get_min(lower_expr, value_expr.get_lower());
+    upper_expr =
+      constant_interval_exprt::get_max(upper_expr, value_expr.get_upper());
   }
-  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.
@@ -291,4 +294,6 @@ class abstract_value_objectt : public abstract_objectt,
   value_range_implementation() const = 0;
 };
 
-#endif
+using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;
+
+#endif

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -42,6 +42,11 @@ constant_abstract_valuet::constant_abstract_valuet(const typet &t)
 {
 }
 
+constant_abstract_valuet::constant_abstract_valuet(const exprt &e)
+  : abstract_value_objectt(e.type(), false, false), value(e)
+{
+}
+
 constant_abstract_valuet::constant_abstract_valuet(
   const typet &t,
   bool tp,
@@ -86,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,
@@ -104,38 +114,25 @@ void constant_abstract_valuet::output(
 abstract_object_pointert
 constant_abstract_valuet::merge(abstract_object_pointert other) const
 {
-  constant_abstract_value_pointert cast_other =
-    std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
+  auto cast_other =
+    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
   if(cast_other)
-  {
     return merge_constant_constant(cast_other);
-  }
-  else
-  {
-    // TODO(tkiley): How do we set the result to be toppish? Does it matter?
-    return abstract_objectt::merge(other);
-  }
+
+  return abstract_objectt::merge(other);
 }
 
 abstract_object_pointert constant_abstract_valuet::merge_constant_constant(
-  const constant_abstract_value_pointert &other) const
+  const abstract_value_pointert &other) const
 {
-  if(is_bottom())
-  {
-    return std::make_shared<constant_abstract_valuet>(*other);
-  }
-  else
-  {
-    // Can we actually merge these value
-    if(value == other->value)
-    {
-      return shared_from_this();
-    }
-    else
-    {
-      return abstract_objectt::merge(other);
-    }
-  }
+  auto other_expr = other->to_constant();
+  if(is_bottom() && other_expr.is_constant())
+    return std::make_shared<constant_abstract_valuet>(other_expr);
+
+  if(value == other_expr) // Can we actually merge these value
+    return shared_from_this();
+
+  return abstract_objectt::merge(other);
 }
 
 void constant_abstract_valuet::get_statistics(

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -19,12 +19,9 @@
 
 class constant_abstract_valuet : public abstract_value_objectt
 {
-private:
-  typedef sharing_ptrt<constant_abstract_valuet>
-    constant_abstract_value_pointert;
-
 public:
   explicit constant_abstract_valuet(const typet &t);
+  explicit constant_abstract_valuet(const exprt &t);
   constant_abstract_valuet(const typet &t, bool tp, bool bttm);
   constant_abstract_valuet(
     const exprt &e,
@@ -39,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,
@@ -75,15 +73,15 @@ class constant_abstract_valuet : public abstract_value_objectt
   abstract_object_pointert merge(abstract_object_pointert other) const override;
 
 private:
-  /// Merges another constant abstract value into this one
+  /// Merges another abstract value into this one
   ///
   /// \param other: the abstract object to merge with
   ///
   /// \return Returns a new abstract object that is the result of the merge
   ///         unless the merge is the same as this abstract object, in which
   ///         case it returns this.
   abstract_object_pointert
-  merge_constant_constant(const constant_abstract_value_pointert &other) const;
+  merge_constant_constant(const abstract_value_pointert &other) const;
 
   exprt value;
 };

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -282,6 +282,19 @@ exprt interval_abstract_valuet::to_constant() const
 #endif
 }
 
+size_t interval_abstract_valuet::internal_hash() const
+{
+  return std::hash<std::string>{}(interval.pretty());
+}
+
+bool interval_abstract_valuet::internal_equality(
+  const abstract_object_pointert &other) const
+{
+  auto cast_other =
+    std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
+  return cast_other && interval == cast_other->interval;
+}
+
 void interval_abstract_valuet::output(
   std::ostream &out,
   const ai_baset &ai,
@@ -329,8 +342,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 +355,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,11 +41,14 @@ 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;
   }
 
+  size_t internal_hash() const override;
+  bool internal_equality(const abstract_object_pointert &other) const override;
+
   void output(
     std::ostream &out,
     const class ai_baset &ai,
@@ -68,7 +71,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,25 @@ value_set_abstract_objectt::value_range_implementation() const
   return make_value_set_value_range(values);
 }
 
+exprt value_set_abstract_objectt::to_constant() const
+{
+  verify();
+
+  if(values.size() == 1)
+    return values.first()->to_constant();
+
+  auto interval = to_interval();
+  if(interval.is_single_value_interval())
+    return interval.get_lower();
+
+  return 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 +219,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)
   //{
@@ -215,19 +236,19 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values(
 abstract_object_pointert
 value_set_abstract_objectt::merge(abstract_object_pointert other) const
 {
+  auto union_values = !is_bottom() ? values : abstract_object_sett{};
+
   auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
   if(other_value_set)
   {
-    auto union_values = values;
     union_values.insert(other_value_set->get_values());
     return resolve_values(union_values);
   }
 
   auto other_value =
-    std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
+    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
   if(other_value)
   {
-    auto union_values = values;
     union_values.insert(other_value);
     return resolve_values(union_values);
   }
@@ -254,6 +275,7 @@ void value_set_abstract_objectt::set_values(
     set_not_top();
     values = other_values;
   }
+  set_not_bottom();
   verify();
 }