Remove abstract_objectt::read member function

Now we've moved some work into expression_transform, we don't need a
read member on the base class.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -136,14 +136,6 @@ abstract_object_pointert abstract_objectt::expression_transform(
   return environment.abstract_object_factory(copy.type(), copy, ns);
 }
 
-abstract_object_pointert abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return shared_from_this();
-}
-
 abstract_object_pointert abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/abstract_object.h

@@ -177,23 +177,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   /// that allows an object to be built from a value.
   virtual exprt to_constant() const;
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  virtual abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -43,21 +43,13 @@ abstract_object_pointert array_abstract_objectt::expression_transform(
 {
   if(expr.id() == ID_index)
   {
-    return read(environment, expr, ns);
+    return read_index(environment, to_index_expr(expr), ns);
   }
 
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
 
-abstract_object_pointert array_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return this->read_index(env, to_index_expr(specifier), ns);
-}
-
 abstract_object_pointert array_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -63,23 +63,6 @@ class array_abstract_objectt : public abstract_objectt
     const abstract_environmentt &environment,
     const namespacet &ns) const override;
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -30,28 +30,6 @@ void context_abstract_objectt::set_not_top_internal()
     set_child(child_abstract_object->clear_top());
 }
 
-/**
- * A helper function to evaluate an abstract object contained
- * within a container object. More precise abstractions may override this
- * to return more precise results.
- *
- * \param env the abstract environment
- * \param specifier a modifier expression, such as an array index or field
- * specifier used to indicate access to a specific component
- * \param ns the current namespace
- *
- * \return the abstract_objectt representing the value of the read component.
- * For the dependency context, the operation is simply delegated to the
- * child object
- */
-abstract_object_pointert context_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return child_abstract_object->read(env, specifier, ns);
-}
-
 /**
  * A helper function to evaluate writing to a component of an
  * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/context_abstract_object.h

@@ -107,11 +107,6 @@ class context_abstract_objectt : public abstract_objectt
   void set_top_internal() override;
   void set_not_top_internal() override;
 
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,

src/analyses/variable-sensitivity/pointer_abstract_object.cpp

@@ -44,21 +44,13 @@ abstract_object_pointert pointer_abstract_objectt::expression_transform(
 {
   if(expr.id() == ID_dereference)
   {
-    return read(environment, expr, ns);
+    return read_dereference(environment, ns);
   }
 
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
 
-abstract_object_pointert pointer_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return read_dereference(env, ns);
-}
-
 abstract_object_pointert pointer_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/pointer_abstract_object.h

@@ -64,23 +64,6 @@ class pointer_abstract_objectt : public abstract_objectt
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/struct_abstract_object.cpp

@@ -45,21 +45,13 @@ abstract_object_pointert struct_abstract_objectt::expression_transform(
 {
   if(expr.id() == ID_member)
   {
-    return read(environment, expr, ns);
+    return read_component(environment, to_member_expr(expr), ns);
   }
 
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
 
-abstract_object_pointert struct_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return this->read_component(env, to_member_expr(specifier), ns);
-}
-
 abstract_object_pointert struct_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/struct_abstract_object.h

@@ -63,23 +63,6 @@ class struct_abstract_objectt : public abstract_objectt
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/union_abstract_object.cpp

@@ -36,14 +36,6 @@ union_abstract_objectt::union_abstract_objectt(
   PRECONDITION(ns.follow(expr.type()).id() == ID_union);
 }
 
-abstract_object_pointert union_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  return read_component(env, to_member_expr(specifier), ns);
-}
-
 abstract_object_pointert union_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/union_abstract_object.h

@@ -42,23 +42,6 @@ class union_abstract_objectt : public abstract_objectt
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /**
-   * A helper function to evaluate an abstract object contained
-   * within a container object. More precise abstractions may override this
-   * to return more precise results.
-   *
-   * \param env the abstract environment
-   * \param specifier a modifier expression, such as an array index or field
-   * specifier used to indicate access to a specific component
-   * \param ns the current namespace
-   *
-   * \return the abstract_objectt representing the value of the read component.
-   */
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -111,18 +111,6 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform(
   return resolve_new_values(resulting_objects);
 }
 
-abstract_object_pointert value_set_abstract_objectt::read(
-  const abstract_environmentt &env,
-  const exprt &specifier,
-  const namespacet &ns) const
-{
-  abstract_object_sett new_values;
-  for(const auto &st_value : values)
-    new_values.insert(st_value->read(env, specifier, ns));
-
-  return resolve_new_values(new_values);
-}
-
 abstract_object_pointert value_set_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -89,14 +89,6 @@ class value_set_abstract_objectt : public abstract_valuet
   /// either converted to interval or marked as `top`.
   static const size_t max_value_set_size = 10;
 
-  /// \copydoc abstract_objectt::read
-  ///
-  /// Delegate reading to stored values.
-  abstract_object_pointert read(
-    const abstract_environmentt &env,
-    const exprt &specifier,
-    const namespacet &ns) const override;
-
   /// \copydoc abstract_objectt::write
   ///
   /// Delegate writing to stored values.

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

@@ -61,7 +61,8 @@ class array_utilt
     constant_array_abstract_object_pointert array_object,
     const index_exprt &index) const
   {
-    return array_object->read(enviroment, index, ns)->to_constant();
+    return array_object->expression_transform(index, {}, enviroment, ns)
+      ->to_constant();
   }
 
 private:

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

@@ -42,7 +42,8 @@ class struct_utilt
     full_struct_abstract_objectt::constant_struct_pointert struct_object,
     const member_exprt &component) const
   {
-    return struct_object->read(enviroment, component, ns)->to_constant();
+    return struct_object->expression_transform(component, {}, enviroment, ns)
+      ->to_constant();
   }
 
   // At the moment the full_struct_abstract_object does not support