Move common merge & meet member functions down to abstract_value_object

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -177,6 +177,29 @@ abstract_object_pointert abstract_value_objectt::expression_transform(
   return environment.add_object_context(result);
 }
 
+abstract_object_pointert abstract_value_objectt::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, widen_mode);
+
+  return abstract_objectt::merge(other, widen_mode);
+}
+
+abstract_object_pointert
+abstract_value_objectt::meet(const abstract_object_pointert &other) const
+{
+  auto cast_other =
+    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
+  if(cast_other)
+    return meet_with_value(cast_other);
+
+  return abstract_objectt::meet(other);
+}
+
 // evaluation helpers
 template <class representation_type>
 abstract_object_pointert make_top(const typet &type)

src/analyses/variable-sensitivity/abstract_value_object.h

@@ -287,6 +287,29 @@ class abstract_value_objectt : public abstract_objectt,
     const namespacet &ns) const final;
 
 protected:
+  using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;
+
+  /// Attempts to do a value/value merge if both are constants,
+  /// 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 wident &widen_mode) const final;
+
+  abstract_object_pointert
+  meet(const abstract_object_pointert &other) const final;
+
+  virtual abstract_object_pointert merge_with_value(
+    const abstract_value_pointert &other,
+    const wident &widen_mode) const = 0;
+
+  virtual abstract_object_pointert
+  meet_with_value(const abstract_value_pointert &other) const = 0;
+
   virtual index_range_implementation_ptrt
   index_range_implementation(const namespacet &ns) const = 0;
 

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -111,18 +111,6 @@ void constant_abstract_valuet::output(
   }
 }
 
-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, widen_mode);
-
-  return abstract_objectt::merge(other, widen_mode);
-}
-
 abstract_object_pointert constant_abstract_valuet::merge_with_value(
   const abstract_value_pointert &other,
   const wident &widen_mode) const
@@ -137,17 +125,6 @@ abstract_object_pointert constant_abstract_valuet::merge_with_value(
   return abstract_objectt::merge(other, widen_mode);
 }
 
-abstract_object_pointert
-constant_abstract_valuet::meet(const abstract_object_pointert &other) const
-{
-  auto cast_other =
-    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
-  if(cast_other)
-    return meet_with_value(cast_other);
-
-  return abstract_objectt::meet(other);
-}
-
 abstract_object_pointert constant_abstract_valuet::meet_with_value(
   const abstract_value_pointert &other) const
 {

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -64,20 +64,6 @@ class constant_abstract_valuet : public abstract_value_objectt
 protected:
   CLONE
 
-  /// Attempts to do a constant/constant merge if both are constants,
-  /// 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 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
@@ -88,10 +74,12 @@ class constant_abstract_valuet : public abstract_value_objectt
   ///         case it returns this.
   abstract_object_pointert merge_with_value(
     const abstract_value_pointert &other,
-    const wident &widen_mode) const;
+    const wident &widen_mode) const override;
+
   abstract_object_pointert
-  meet_with_value(const abstract_value_pointert &other) const;
+  meet_with_value(const abstract_value_pointert &other) const override;
 
+private:
   exprt value;
 };
 

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -344,18 +344,6 @@ void interval_abstract_valuet::output(
   }
 }
 
-abstract_object_pointert interval_abstract_valuet::merge(
-  const abstract_object_pointert &other,
-  const wident &widen_mode) const
-{
-  abstract_value_pointert cast_other =
-    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
-  if(cast_other)
-    return merge_with_value(cast_other, widen_mode);
-
-  return abstract_objectt::merge(other, widen_mode);
-}
-
 /// 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
@@ -386,17 +374,6 @@ abstract_object_pointert interval_abstract_valuet::merge_with_value(
       interval.get_upper(), other_interval.get_upper())));
 }
 
-abstract_object_pointert
-interval_abstract_valuet::meet(const abstract_object_pointert &other) const
-{
-  auto cast_other =
-    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
-  if(cast_other)
-    return meet_with_value(cast_other);
-
-  return abstract_objectt::meet(other);
-}
-
 /// 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,

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -62,22 +62,15 @@ class interval_abstract_valuet : public abstract_value_objectt
 
 protected:
   CLONE
-  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:
-  using interval_abstract_value_pointert =
-    sharing_ptrt<interval_abstract_valuet>;
 
   abstract_object_pointert merge_with_value(
     const abstract_value_pointert &other,
-    const wident &widen_mode) const;
+    const wident &widen_mode) const override;
+
   abstract_object_pointert
-  meet_with_value(const abstract_value_pointert &other) const;
+  meet_with_value(const abstract_value_pointert &other) const override;
 
+private:
   constant_interval_exprt interval;
 };
 

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -286,29 +286,6 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values(
   return result;
 }
 
-abstract_object_pointert value_set_abstract_objectt::merge(
-  const abstract_object_pointert &other,
-  const wident &widen_mode) const
-{
-  auto other_value =
-    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
-  if(other_value)
-    return merge_with_value(other_value, widen_mode);
-
-  return abstract_objectt::merge(other, widen_mode);
-}
-
-abstract_object_pointert
-value_set_abstract_objectt::meet(const abstract_object_pointert &other) const
-{
-  auto cast_other =
-    std::dynamic_pointer_cast<const abstract_value_objectt>(other);
-  if(cast_other)
-    return meet_with_value(cast_other);
-
-  return abstract_objectt::meet(other);
-}
-
 void value_set_abstract_objectt::set_top_internal()
 {
   values.clear();

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -71,12 +71,12 @@ class value_set_abstract_objectt : public abstract_value_objectt,
 protected:
   CLONE
 
-  /// \copydoc abstract_object::merge
-  abstract_object_pointert merge(
-    const abstract_object_pointert &other,
+  abstract_object_pointert merge_with_value(
+    const abstract_value_pointert &other,
     const wident &widen_mode) const override;
+
   abstract_object_pointert
-  meet(const abstract_object_pointert &other) const override;
+  meet_with_value(const abstract_value_pointert &other) const override;
 
 private:
   /// Update the set of stored values to \p new_values. Build a new abstract
@@ -97,12 +97,6 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   abstract_object_pointert
   resolve_values(const abstract_object_sett &new_values) 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;
-
   // data
   abstract_object_sett values;