Reorganised pointer representation hierarchy

Introduce new base class, abstract_pointer_objectt. It should be,
but is not yet, an abstract (in C++ terms) class as it's not
intended to be directly instantiable.

pointer_abstract_object now renamed two_value_pointer_abstract_objectt.

constant_pointer_abstract_objectt and two_value_pointer_abstract_objectt
are now peers.

Deleted the unused value_set_pointer_abstract_objectt in anticipation of
reintroducing a more functional value-set pointer representation
shortly.

Author: jezhiggins

scripts/expected_doxygen_warnings.txt

@@ -97,6 +97,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (122), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (244), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/Makefile

@@ -33,29 +33,27 @@ SRC = ai.cpp \
       static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
-      variable-sensitivity/abstract_object.cpp \
       variable-sensitivity/abstract_environment.cpp \
+      variable-sensitivity/abstract_object.cpp \
+      variable-sensitivity/abstract_pointer_object.cpp \
       variable-sensitivity/abstract_value_object.cpp \
       variable-sensitivity/constant_abstract_value.cpp \
       variable-sensitivity/constant_pointer_abstract_object.cpp \
       variable-sensitivity/context_abstract_object.cpp \
-      variable-sensitivity/write_location_context.cpp \
-      variable-sensitivity/pointer_abstract_object.cpp \
-      variable-sensitivity/variable_sensitivity_domain.cpp \
-      variable-sensitivity/variable_sensitivity_object_factory.cpp \
-      variable-sensitivity/full_struct_abstract_object.cpp \
-      variable-sensitivity/full_array_abstract_object.cpp \
-      variable-sensitivity/write_stack.cpp \
-      variable-sensitivity/write_stack_entry.cpp \
       variable-sensitivity/data_dependency_context.cpp \
-      variable-sensitivity/value_set_abstract_object.cpp \
-      variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
+      variable-sensitivity/full_array_abstract_object.cpp \
+      variable-sensitivity/full_struct_abstract_object.cpp \
       variable-sensitivity/interval_abstract_value.cpp \
+      variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_value.cpp \
-      variable-sensitivity/value_set_pointer_abstract_object.cpp \
-      variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/variable_sensitivity_configuration.cpp \
+      variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
+      variable-sensitivity/variable_sensitivity_domain.cpp \
+      variable-sensitivity/variable_sensitivity_object_factory.cpp \
+      variable-sensitivity/write_location_context.cpp \
+      variable-sensitivity/write_stack.cpp \
+      variable-sensitivity/write_stack_entry.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -11,8 +11,8 @@
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/abstract_object_statistics.h>
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
-#include <analyses/variable-sensitivity/pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
+#include <analyses/variable-sensitivity/two_value_pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/two_value_struct_abstract_object.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <util/pointer_expr.h>

src/analyses/variable-sensitivity/pointer_abstract_object.cpp renamed to src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -2,23 +2,20 @@
 
  Module: analyses variable-sensitivity
 
- Author: Thomas Kiley, [email protected]
+ Author: Jez Higgins, [email protected]
 
 \*******************************************************************/
-#include <util/std_expr.h>
-#include <util/std_types.h>
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/abstract_pointer_object.h>
 
-#include "pointer_abstract_object.h"
-
-pointer_abstract_objectt::pointer_abstract_objectt(const typet &t)
+abstract_pointer_objectt::abstract_pointer_objectt(const typet &t)
   : abstract_objectt(t)
 {
   PRECONDITION(t.id() == ID_pointer);
 }
 
-pointer_abstract_objectt::pointer_abstract_objectt(
+abstract_pointer_objectt::abstract_pointer_objectt(
   const typet &type,
   bool top,
   bool bottom)
@@ -27,7 +24,7 @@ pointer_abstract_objectt::pointer_abstract_objectt(
   PRECONDITION(type.id() == ID_pointer);
 }
 
-pointer_abstract_objectt::pointer_abstract_objectt(
+abstract_pointer_objectt::abstract_pointer_objectt(
   const exprt &e,
   const abstract_environmentt &environment,
   const namespacet &ns)
@@ -36,22 +33,20 @@ pointer_abstract_objectt::pointer_abstract_objectt(
   PRECONDITION(e.type().id() == ID_pointer);
 }
 
-abstract_object_pointert pointer_abstract_objectt::expression_transform(
+abstract_object_pointert abstract_pointer_objectt::expression_transform(
   const exprt &expr,
   const std::vector<abstract_object_pointert> &operands,
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
   if(expr.id() == ID_dereference)
-  {
     return read_dereference(environment, ns);
-  }
 
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
 
-abstract_object_pointert pointer_abstract_objectt::write(
+abstract_object_pointert abstract_pointer_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
   const std::stack<exprt> &stack,
@@ -62,7 +57,7 @@ abstract_object_pointert pointer_abstract_objectt::write(
   return write_dereference(environment, ns, stack, value, merging_write);
 }
 
-abstract_object_pointert pointer_abstract_objectt::read_dereference(
+abstract_object_pointert abstract_pointer_objectt::read_dereference(
   const abstract_environmentt &env,
   const namespacet &ns) const
 {
@@ -72,27 +67,23 @@ abstract_object_pointert pointer_abstract_objectt::read_dereference(
   return env.abstract_object_factory(pointed_to_type, ns, true, false);
 }
 
-#include <iostream>
-
-abstract_object_pointert pointer_abstract_objectt::write_dereference(
-  abstract_environmentt &environment,
+abstract_object_pointert abstract_pointer_objectt::write_dereference(
+  abstract_environmentt &env,
   const namespacet &ns,
   const std::stack<exprt> &stack,
   const abstract_object_pointert &value,
   bool merging_write) const
 {
   if(is_top() || is_bottom())
   {
-    environment.havoc("Writing to a 2value pointer");
+    env.havoc("Writing to a 2value pointer");
     return shared_from_this();
   }
-  else
-  {
-    return std::make_shared<pointer_abstract_objectt>(type(), true, false);
-  }
+
+  return std::make_shared<abstract_pointer_objectt>(type(), true, false);
 }
 
-void pointer_abstract_objectt::get_statistics(
+void abstract_pointer_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,
   const abstract_environmentt &env,

src/analyses/variable-sensitivity/pointer_abstract_object.h renamed to src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -2,84 +2,52 @@
 
  Module: analyses variable-sensitivity
 
- Author: Thomas Kiley, [email protected]
+ Author: Jez Higgins, [email protected]
 
 \*******************************************************************/
 
 /// \file
 /// The base of all pointer abstractions
-#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H
-#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H
-
-#include <stack>
+#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
+#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
 
 #include <analyses/variable-sensitivity/abstract_object.h>
 
-class typet;
-class constant_exprt;
-class abstract_environmentt;
+class abstract_pointer_tag
+{
+};
 
-class pointer_abstract_objectt : public abstract_objectt
+class abstract_pointer_objectt : public abstract_objectt,
+                                 public abstract_pointer_tag
 {
 public:
   /// \param type: the type the abstract_object is representing
-  explicit pointer_abstract_objectt(const typet &type);
+  explicit abstract_pointer_objectt(const typet &type);
 
   /// Start the abstract object at either top or bottom or neither
   /// Asserts if both top and bottom are true
   ///
   /// \param type: the type the abstract_object is representing
   /// \param top: is the abstract_object starting as top
   /// \param bottom: is the abstract_object starting as bottom
-  pointer_abstract_objectt(const typet &type, bool top, bool bottom);
-
-  /// Interface for transforms
-  ///
-  /// \param expr: the expression to evaluate and find the result of it.
-  ///              This will be the symbol referred to be op0()
-  /// \param operands: an abstract_object (pointer) that represent
-  ///                  the possible values of each operand
-  /// \param environment: the abstract environment in which the
-  ///                     expression is being evaluated
-  /// \param ns: the current variable namespace
-  ///
-  /// \return Returns the abstract_object representing the result of
-  ///         this expression to the maximum precision available.
-  ///
-  /// To try and resolve different expressions with the maximum level
-  /// of precision available.
-  abstract_object_pointert expression_transform(
-    const exprt &expr,
-    const std::vector<abstract_object_pointert> &operands,
-    const abstract_environmentt &environment,
-    const namespacet &ns) const override;
+  abstract_pointer_objectt(const typet &type, bool top, bool bottom);
 
   /// \param expr: the expression to use as the starting pointer for
   ///              an abstract object
   /// \param environment: the environment in which the pointer is being
   ///                     created
   /// \param ns: the current namespace
-  explicit pointer_abstract_objectt(
+  explicit abstract_pointer_objectt(
     const exprt &expr,
     const abstract_environmentt &environment,
     const namespacet &ns);
 
-  /**
-   * A helper function to evaluate writing to a component of an
-   * abstract object. More precise abstractions may override this to
-   * update what they are storing for a specific component.
-   *
-   * \param environment the abstract environment
-   * \param ns the current namespace
-   * \param stack the remaining stack of expressions on the LHS to evaluate
-   * \param specifier the expression uses to access a specific component
-   * \param value the value we are trying to write to the component
-   * \param merging_write if true, this and all future writes will be merged
-   * with the current value
-   *
-   * \return the abstract_objectt representing the result of writing
-   * to a specific component.
-   */
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override;
+
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,
@@ -95,9 +63,7 @@ class pointer_abstract_objectt : public abstract_objectt
     const namespacet &ns) const override;
 
 protected:
-  CLONE
-
-  /// A helper function to read elements from an array. More precise
+  /// Evaluate reading the pointer's value. More precise
   /// abstractions may override this to provide more precise results.
   ///
   /// \param env: the environment
@@ -108,8 +74,8 @@ class pointer_abstract_objectt : public abstract_objectt
     const abstract_environmentt &env,
     const namespacet &ns) const;
 
-  /// A helper function to evaluate writing to a pointers value. More
-  /// precise abstractions may override this provide more precise results.
+  /// Evaluate writing to a pointer's value. More precise abstractions
+  /// may override this provide more precise results.
   ///
   /// \param environment: the abstract environment
   /// \param ns: the namespace
@@ -132,4 +98,4 @@ class pointer_abstract_objectt : public abstract_objectt
     bool merging_write) const;
 };
 
-#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H
+#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -18,7 +18,7 @@
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const typet &type)
-  : pointer_abstract_objectt(type)
+  : abstract_pointer_objectt(type)
 {
   PRECONDITION(type.id() == ID_pointer);
 }
@@ -27,22 +27,22 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const typet &type,
   bool top,
   bool bottom)
-  : pointer_abstract_objectt(type, top, bottom)
+  : abstract_pointer_objectt(type, top, bottom)
 {
   PRECONDITION(type.id() == ID_pointer);
 }
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const constant_pointer_abstract_objectt &old)
-  : pointer_abstract_objectt(old), value_stack(old.value_stack)
+  : abstract_pointer_objectt(old), value_stack(old.value_stack)
 {
 }
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const exprt &expr,
   const abstract_environmentt &environment,
   const namespacet &ns)
-  : pointer_abstract_objectt(expr, environment, ns),
+  : abstract_pointer_objectt(expr, environment, ns),
     value_stack(expr, environment, ns)
 {
   PRECONDITION(expr.type().id() == ID_pointer);
@@ -68,13 +68,13 @@ constant_pointer_abstract_objectt::merge(abstract_object_pointert other) const
   else
   {
     // TODO(tkiley): How do we set the result to be toppish?
-    return pointer_abstract_objectt::merge(other);
+    return abstract_pointer_objectt::merge(other);
   }
 }
 
 abstract_object_pointert
 constant_pointer_abstract_objectt::merge_constant_pointers(
-  const constant_pointer_abstract_pointert other) const
+  const constant_pointer_abstract_pointert &other) const
 {
   if(is_bottom())
   {
@@ -91,7 +91,7 @@ constant_pointer_abstract_objectt::merge_constant_pointers(
     }
     else
     {
-      return pointer_abstract_objectt::merge(other);
+      return abstract_pointer_objectt::merge(other);
     }
   }
 }
@@ -100,7 +100,7 @@ exprt constant_pointer_abstract_objectt::to_constant() const
 {
   if(is_top() || is_bottom())
   {
-    return pointer_abstract_objectt::to_constant();
+    return abstract_pointer_objectt::to_constant();
   }
   else
   {
@@ -117,7 +117,7 @@ void constant_pointer_abstract_objectt::output(
 {
   if(is_top() || is_bottom() || value_stack.is_top_value())
   {
-    pointer_abstract_objectt::output(out, ai, ns);
+    abstract_pointer_objectt::output(out, ai, ns);
   }
   else
   {
@@ -180,7 +180,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
 {
   if(is_top() || is_bottom() || value_stack.is_top_value())
   {
-    return pointer_abstract_objectt::write_dereference(
+    return abstract_pointer_objectt::write_dereference(
       environment, ns, stack, new_value, merging_write);
   }
   else
@@ -225,7 +225,7 @@ void constant_pointer_abstract_objectt::get_statistics(
   const abstract_environmentt &env,
   const namespacet &ns) const
 {
-  pointer_abstract_objectt::get_statistics(statistics, visited, env, ns);
+  abstract_pointer_objectt::get_statistics(statistics, visited, env, ns);
   // don't bother following nullptr
   if(!is_top() && !is_bottom() && !value_stack.is_top_value())
   {