Pass widen_mode down into abstract_object::merge

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_aggregate_object.h

@@ -125,7 +125,8 @@ class abstract_aggregate_objectt : public abstract_objectt,
   static bool merge_shared_maps(
     const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map1,
     const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map2,
-    sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map)
+    sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map,
+    const wident &widen_mode)
   {
     bool modified = false;
 
@@ -135,7 +136,8 @@ class abstract_aggregate_objectt : public abstract_objectt,
 
     for(auto &item : delta_view)
     {
-      auto v_new = abstract_objectt::merge(item.m, item.get_other_map_value());
+      auto v_new =
+        abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode);
       if(v_new.modified)
       {
         modified = true;

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -335,33 +335,27 @@ bool abstract_environmentt::merge(
 {
   // for each entry in the incoming environment we need to either add it
   // if it is new, or merge with the existing key if it is not present
-
   if(bottom)
   {
     *this = env;
     return !env.bottom;
   }
-  else if(env.bottom)
-  {
+
+  if(env.bottom)
     return false;
-  }
-  else
-  {
-    // For each element in the intersection of map and env.map merge
-    // If the result of the merge is top, remove from the map
-    bool modified = false;
-    decltype(env.map)::delta_viewt delta_view;
-    env.map.get_delta_view(map, delta_view);
-    for(const auto &entry : delta_view)
-    {
-      auto merge_result =
-        abstract_objectt::merge(entry.get_other_map_value(), entry.m);
-      modified |= merge_result.modified;
-      map.replace(entry.k, merge_result.object);
-    }
 
-    return modified;
+  // For each element in the intersection of map and env.map merge
+  // If the result of the merge is top, remove from the map
+  bool modified = false;
+  for(const auto &entry : env.map.get_delta_view(map))
+  {
+    auto merge_result =
+      abstract_objectt::merge(entry.get_other_map_value(), entry.m, widen_mode);
+    modified |= merge_result.modified;
+    map.replace(entry.k, merge_result.object);
   }
+
+  return modified;
 }
 
 void abstract_environmentt::havoc(const std::string &havoc_string)

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -55,8 +55,9 @@ const typet &abstract_objectt::type() const
   return t;
 }
 
-abstract_object_pointert
-abstract_objectt::merge(const abstract_object_pointert &other) const
+abstract_object_pointert abstract_objectt::merge(
+  const abstract_object_pointert &other,
+  const wident &widen_mode) const
 {
   return abstract_object_merge(other);
 }
@@ -191,11 +192,12 @@ void abstract_objectt::output(
 
 abstract_objectt::merge_result abstract_objectt::merge(
   const abstract_object_pointert &op1,
-  const abstract_object_pointert &op2)
+  const abstract_object_pointert &op2,
+  const wident &widen_mode)
 {
   abstract_object_pointert result = op1->should_use_base_merge(op2)
                                       ? op1->abstract_object_merge(op2)
-                                      : op1->merge(op2);
+                                      : op1->merge(op2, widen_mode);
   // If no modifications, we will return the original pointer
   return {result, result != op1};
 }

src/analyses/variable-sensitivity/abstract_object.h

@@ -43,6 +43,7 @@ class typet;
 class constant_exprt;
 class abstract_environmentt;
 class namespacet;
+enum class wident;
 
 #define CLONE                                                                  \
   internal_abstract_object_pointert mutable_clone() const override             \
@@ -261,7 +262,8 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   };
   static merge_result merge(
     const abstract_object_pointert &op1,
-    const abstract_object_pointert &op2);
+    const abstract_object_pointert &op2,
+    const wident &widen_mode);
 
   /// Interface method for the meet operation. Decides whether to use the base
   /// implementation or if a more precise abstraction is attainable.
@@ -430,10 +432,11 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   /// the object would be unchanged, then would return itself.
   ///
   /// \param other: The object to merge with this
+  /// \param widen_mode: Indicates if this is a widening merge
   ///
   /// \return Returns the result of the merge.
   virtual abstract_object_pointert
-  merge(const abstract_object_pointert &other) const;
+  merge(const abstract_object_pointert &other, const wident &widen_mode) const;
 
   /// Helper function for base meet. Two cases: return itself (if trivially
   /// contained in other); return BOTTOM otherwise.

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -111,19 +111,21 @@ void constant_abstract_valuet::output(
   }
 }
 
-abstract_object_pointert
-constant_abstract_valuet::merge(const abstract_object_pointert &other) const
+abstract_object_pointert constant_abstract_valuet::merge(
+  const abstract_object_pointert &other,
+  const wident &widen_mode) const
 {
   auto cast_other =
     std::dynamic_pointer_cast<const abstract_value_objectt>(other);
   if(cast_other)
-    return merge_with_value(cast_other);
+    return merge_with_value(cast_other, widen_mode);
 
-  return abstract_objectt::merge(other);
+  return abstract_objectt::merge(other, widen_mode);
 }
 
 abstract_object_pointert constant_abstract_valuet::merge_with_value(
-  const abstract_value_pointert &other) const
+  const abstract_value_pointert &other,
+  const wident &widen_mode) const
 {
   auto other_expr = other->to_constant();
   if(is_bottom() && other_expr.is_constant())
@@ -132,7 +134,7 @@ abstract_object_pointert constant_abstract_valuet::merge_with_value(
   if(value == other_expr) // Can we actually merge these value
     return shared_from_this();
 
-  return abstract_objectt::merge(other);
+  return abstract_objectt::merge(other, widen_mode);
 }
 
 abstract_object_pointert

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -68,23 +68,27 @@ class constant_abstract_valuet : public abstract_value_objectt
   /// otherwise falls back to the parent merge
   ///
   /// \param other: the abstract object to merge with
+  /// \param widen_mode: Indicates if this is a widening merge
   ///
   /// \return Returns the result of the merge
-  abstract_object_pointert
-  merge(const abstract_object_pointert &other) const override;
+  abstract_object_pointert merge(
+    const abstract_object_pointert &other,
+    const wident &widen_mode) const override;
   abstract_object_pointert
   meet(const abstract_object_pointert &other) const override;
 
 private:
   /// Merges another abstract value into this one
   ///
   /// \param other: the abstract object to merge with
+  /// \param widen_mode: Indicates if this is a widening merge
   ///
   /// \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_with_value(const abstract_value_pointert &other) const;
+  abstract_object_pointert merge_with_value(
+    const abstract_value_pointert &other,
+    const wident &widen_mode) const;
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const;
 

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -57,43 +57,32 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
 }
 
 abstract_object_pointert constant_pointer_abstract_objectt::merge(
-  const abstract_object_pointert &other) const
+  const abstract_object_pointert &other,
+  const wident &widen_mode) const
 {
   auto cast_other =
     std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
   if(cast_other)
-  {
-    return merge_constant_pointers(cast_other);
-  }
-  else
-  {
-    // TODO(tkiley): How do we set the result to be toppish?
-    return abstract_pointer_objectt::merge(other);
-  }
+    return merge_constant_pointers(cast_other, widen_mode);
+
+  return abstract_pointer_objectt::merge(other, widen_mode);
 }
 
 abstract_object_pointert
 constant_pointer_abstract_objectt::merge_constant_pointers(
-  const constant_pointer_abstract_pointert &other) const
+  const constant_pointer_abstract_pointert &other,
+  const wident &widen_mode) const
 {
   if(is_bottom())
-  {
     return std::make_shared<constant_pointer_abstract_objectt>(*other);
-  }
-  else
-  {
-    bool matching_pointer =
-      value_stack.to_expression() == other->value_stack.to_expression();
 
-    if(matching_pointer)
-    {
-      return shared_from_this();
-    }
-    else
-    {
-      return abstract_pointer_objectt::merge(other);
-    }
-  }
+  bool matching_pointers =
+    value_stack.to_expression() == other->value_stack.to_expression();
+
+  if(matching_pointers)
+    return shared_from_this();
+
+  return abstract_pointer_objectt::merge(other, widen_mode);
 }
 
 exprt constant_pointer_abstract_objectt::to_constant() const
@@ -196,7 +185,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
       {
         abstract_object_pointert pointed_value = environment.eval(value, ns);
         abstract_object_pointert merged_value =
-          abstract_objectt::merge(pointed_value, new_value).object;
+          abstract_objectt::merge(pointed_value, new_value, wident::no).object;
         environment.assign(value, merged_value, ns);
       }
       else

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -119,10 +119,12 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
   /// constant pointer merge
   ///
   /// \param op1: the pointer being merged
+  /// \param widen_mode: Indicates if this is a widening merge
   ///
   /// \return Returns the result of the merge.
-  abstract_object_pointert
-  merge(const abstract_object_pointert &op1) const override;
+  abstract_object_pointert merge(
+    const abstract_object_pointert &op1,
+    const wident &widen_mode) const override;
 
   CLONE
 
@@ -131,12 +133,14 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
   /// value, we merge, otherwise we set to top.
   ///
   /// \param other: the pointer being merged
+  /// \param widen_mode: Indicates if this is a widening merge
   ///
   /// \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_pointers(
-    const constant_pointer_abstract_pointert &other) const;
+    const constant_pointer_abstract_pointert &other,
+    const wident &widen_mode) const;
 
   write_stackt value_stack;
 };

src/analyses/variable-sensitivity/data_dependency_context.cpp

@@ -230,12 +230,14 @@ abstract_object_pointert data_dependency_contextt::update_location_context(
  * object with a given abstract_object
  *
  * \param other the abstract object to merge with
+ * \param widen_mode: Indicates if this is a widening merge
  *
  * \return the result of the merge, or 'this' if the merge would not change
  * the current abstract object
  */
-abstract_object_pointert
-data_dependency_contextt::merge(const abstract_object_pointert &other) const
+abstract_object_pointert data_dependency_contextt::merge(
+  const abstract_object_pointert &other,
+  const wident &widen_mode) const
 {
   auto cast_other =
     std::dynamic_pointer_cast<const data_dependency_contextt>(other);
@@ -244,7 +246,7 @@ data_dependency_contextt::merge(const abstract_object_pointert &other) const
   {
     const auto merged_parent =
       std::dynamic_pointer_cast<const data_dependency_contextt>(
-        this->write_location_contextt::merge(other));
+        this->write_location_contextt::merge(other, widen_mode));
 
     const auto updated_parent =
       std::dynamic_pointer_cast<const data_dependency_contextt>(
@@ -275,7 +277,7 @@ data_dependency_contextt::merge(const abstract_object_pointert &other) const
       return shared_from_this();
   }
 
-  return abstract_objectt::merge(other);
+  return abstract_objectt::merge(other, widen_mode);
 }
 
 /**

src/analyses/variable-sensitivity/data_dependency_context.h

@@ -70,8 +70,9 @@ class data_dependency_contextt : public write_location_contextt
 protected:
   CLONE
 
-  abstract_object_pointert
-  merge(const abstract_object_pointert &other) const override;
+  abstract_object_pointert merge(
+    const abstract_object_pointert &other,
+    const wident &widen_mode) const override;
 
   abstract_object_pointert abstract_object_merge_internal(
     const abstract_object_pointert &other) const override;