Merge pull request #5640 from jezhiggins/immutable-abstract-objectt

abstract_objectt interface

Author: martin-cs

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -68,7 +68,7 @@ abstract_object_pointert abstract_objectt::abstract_object_merge(
     return this->abstract_object_merge_internal(other);
 
   internal_abstract_object_pointert merged = mutable_clone();
-  merged->make_top();
+  merged->set_top();
   merged->bottom = false;
   return merged->abstract_object_merge_internal(other);
 }
@@ -147,9 +147,9 @@ abstract_object_pointert abstract_objectt::read(
 abstract_object_pointert abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
+  const std::stack<exprt> &stack,
   const exprt &specifier,
-  const abstract_object_pointert value,
+  const abstract_object_pointert &value,
   bool merging_write) const
 {
   return environment.abstract_object_factory(type(), ns, true);

src/analyses/variable-sensitivity/abstract_object.h

@@ -121,7 +121,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   /// Get the real type of the variable this abstract object is representing.
   ///
   /// \return The program type this abstract object represents
-  const typet &type() const;
+  virtual const typet &type() const;
 
   /// Find out if the abstract object is top
   ///
@@ -213,9 +213,9 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   virtual abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
+    const std::stack<exprt> &stack,
     const exprt &specifier,
-    const abstract_object_pointert value,
+    const abstract_object_pointert &value,
     bool merging_write) const;
 
   /// Print the value of the abstract object
@@ -244,11 +244,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   static void
   dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
 
-  abstract_object_pointert clone() const
-  {
-    return abstract_object_pointert(mutable_clone());
-  }
-
   /**
    * Determine whether 'this' abstract_object has been modified in comparison
    * to a previous 'before' state.
@@ -323,7 +318,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
       return shared_from_this();
 
     internal_abstract_object_pointert clone = mutable_clone();
-    clone->make_top();
+    clone->set_top();
     return clone;
   }
 
@@ -333,7 +328,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
       return shared_from_this();
 
     internal_abstract_object_pointert clone = mutable_clone();
-    clone->clear_top();
+    clone->set_not_top();
     return clone;
   }
 
@@ -384,10 +379,10 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
 
   // Hooks to allow a sub-class to perform its own operations on
   // setting/clearing top
-  virtual void make_top_internal()
+  virtual void set_top_internal()
   {
   }
-  virtual void clear_top_internal()
+  virtual void set_not_top_internal()
   {
   }
 
@@ -478,15 +473,15 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
     sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map);
 
   // The one exception is merge in descendant classes, which needs this
-  void make_top()
+  void set_top()
   {
     top = true;
-    this->make_top_internal();
+    this->set_top_internal();
   }
-  void clear_top()
+  void set_not_top()
   {
     top = false;
-    this->clear_top_internal();
+    this->set_not_top_internal();
   }
 };
 

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -46,9 +46,9 @@ abstract_object_pointert array_abstract_objectt::read(
 abstract_object_pointert array_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
+  const std::stack<exprt> &stack,
   const exprt &specifier,
-  const abstract_object_pointert value,
+  const abstract_object_pointert &value,
   bool merging_write) const
 {
   return this->write_index(
@@ -68,12 +68,12 @@ abstract_object_pointert array_abstract_objectt::read_index(
   return env.abstract_object_factory(subtype, ns, !is_bottom(), is_bottom());
 }
 
-sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
+abstract_object_pointert array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
+  const std::stack<exprt> &stack,
   const index_exprt &index_expr,
-  const abstract_object_pointert value,
+  const abstract_object_pointert &value,
   bool merging_write) const
 {
   // TODO(tkiley): Should this in fact havoc since we can't verify
@@ -82,12 +82,11 @@ sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
   // havoc and the default should derive from this.
   if(is_top() || is_bottom())
   {
-    return std::dynamic_pointer_cast<const array_abstract_objectt>(clone());
+    return shared_from_this();
   }
   else
   {
-    return sharing_ptrt<array_abstract_objectt>(
-      new array_abstract_objectt(type(), true, false));
+    return std::make_shared<array_abstract_objectt>(type(), true, false);
   }
 }
 

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -78,9 +78,9 @@ class array_abstract_objectt : public abstract_objectt
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
+    const std::stack<exprt> &stack,
     const exprt &specifier,
-    const abstract_object_pointert value,
+    const abstract_object_pointert &value,
     bool merging_write) const override;
 
   void get_statistics(
@@ -117,15 +117,15 @@ class array_abstract_objectt : public abstract_objectt
   /// \param value: the value we are trying to assign to that value in the array
   /// \param merging_write: ?
   ///
-  /// \return The array_abstract_objectt representing the result of writing
+  /// \return The abstract_object_pointert representing the result of writing
   ///          to a specific component. In this case this will always be top
   ///          as we are not tracking the value in the array.
-  virtual sharing_ptrt<array_abstract_objectt> write_index(
+  virtual abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
+    const std::stack<exprt> &stack,
     const index_exprt &index_expr,
-    const abstract_object_pointert value,
+    const abstract_object_pointert &value,
     bool merging_write) const;
 };
 

src/analyses/variable-sensitivity/constant_array_abstract_object.cpp

@@ -43,7 +43,7 @@ constant_array_abstract_objectt::constant_array_abstract_objectt(
       map.insert(mp_integer(index), environment.eval(entry, ns));
       ++index;
     }
-    clear_top();
+    set_not_top();
   }
   DATA_INVARIANT(verify(), "Structural invariants maintained");
 }
@@ -56,7 +56,7 @@ bool constant_array_abstract_objectt::verify() const
          (is_top() || is_bottom()) == map.empty();
 }
 
-void constant_array_abstract_objectt::make_top_internal()
+void constant_array_abstract_objectt::set_top_internal()
 {
   // A structural invariant of constant_array_abstract_objectt is that
   // (is_top() || is_bottom()) => map.empty()
@@ -189,13 +189,12 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
   }
 }
 
-sharing_ptrt<array_abstract_objectt>
-constant_array_abstract_objectt::write_index(
+abstract_object_pointert constant_array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
+  const std::stack<exprt> &stack,
   const index_exprt &index_expr,
-  const abstract_object_pointert value,
+  const abstract_object_pointert &value,
   bool merging_write) const
 {
   if(is_bottom())
@@ -231,7 +230,7 @@ constant_array_abstract_objectt::write_index(
             old_value.value(), value, stack, ns, merging_write));
       }
 
-      result->clear_top();
+      result->set_not_top();
       DATA_INVARIANT(result->verify(), "Structural invariants maintained");
       return result;
     }
@@ -248,7 +247,7 @@ constant_array_abstract_objectt::write_index(
           starting_value.first,
           environment.write(starting_value.second, value, stack, ns, true));
 
-        result->clear_top();
+        result->set_not_top();
       }
 
       DATA_INVARIANT(result->verify(), "Structural invariants maintained");
@@ -303,7 +302,7 @@ constant_array_abstract_objectt::write_index(
         {
           result->map.insert(index_value, value);
         }
-        result->clear_top();
+        result->set_not_top();
         DATA_INVARIANT(result->verify(), "Structural invariants maintained");
         return result;
       }

src/analyses/variable-sensitivity/constant_array_abstract_object.h

@@ -110,14 +110,14 @@ class constant_array_abstract_objectt : public array_abstract_objectt
   /// \param value: the value we are trying to assign to that value in the array
   /// \param merging_write: Should this and all future writes be merged with the
   ///                       current value
-  /// \return The array_abstract_objectt representing the result of writing
+  /// \return The abstract_object_pointert representing the result of writing
   ///         to a specific index.
-  sharing_ptrt<array_abstract_objectt> write_index(
+  abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
+    const std::stack<exprt> &stack,
     const index_exprt &index_expr,
-    const abstract_object_pointert value,
+    const abstract_object_pointert &value,
     bool merging_write) const override;
 
   /// Tries to do an array/array merge if merging with a constant array
@@ -138,7 +138,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
 
   /// \brief Perform any additional structural modifications when setting this
   /// object to TOP
-  void make_top_internal() override;
+  void set_top_internal() override;
 
   /// Evaluates the index and tries to convert it to a constant integer
   ///

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -46,11 +46,11 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   PRECONDITION(expr.type().id() == ID_pointer);
   if(value_stack.is_top_value())
   {
-    make_top();
+    set_top();
   }
   else
   {
-    clear_top();
+    set_not_top();
   }
 }
 
@@ -169,12 +169,11 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
   }
 }
 
-sharing_ptrt<pointer_abstract_objectt>
-constant_pointer_abstract_objectt::write_dereference(
+abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
-  const abstract_object_pointert new_value,
+  const std::stack<exprt> &stack,
+  const abstract_object_pointert &new_value,
   bool merging_write) const
 {
   if(is_top() || is_bottom() || value_stack.is_top_value())

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -99,11 +99,11 @@ class constant_pointer_abstract_objectt : public pointer_abstract_objectt
   ///
   /// \return A modified abstract object representing this pointer after it
   ///         has been written to.
-  sharing_ptrt<pointer_abstract_objectt> write_dereference(
+  abstract_object_pointert write_dereference(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
-    const abstract_object_pointert value,
+    const std::stack<exprt> &stack,
+    const abstract_object_pointert &value,
     bool merging_write) const override;
 
   void get_statistics(

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -18,13 +18,13 @@ void context_abstract_objectt::set_child(const abstract_object_pointert &child)
   child_abstract_object = child;
 }
 
-void context_abstract_objectt::make_top_internal()
+void context_abstract_objectt::set_top_internal()
 {
   if(!child_abstract_object->is_top())
     set_child(child_abstract_object->make_top());
 }
 
-void context_abstract_objectt::clear_top_internal()
+void context_abstract_objectt::set_not_top_internal()
 {
   if(child_abstract_object->is_top())
     set_child(child_abstract_object->clear_top());
@@ -71,9 +71,9 @@ abstract_object_pointert context_abstract_objectt::read(
 abstract_object_pointert context_abstract_objectt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
-  const std::stack<exprt> stack,
+  const std::stack<exprt> &stack,
   const exprt &specifier,
-  const abstract_object_pointert value,
+  const abstract_object_pointert &value,
   bool merging_write) const
 {
   abstract_object_pointert updated_child = child_abstract_object->write(

src/analyses/variable-sensitivity/context_abstract_object.h

@@ -55,7 +55,7 @@ class context_abstract_objectt : public abstract_objectt
   {
   }
 
-  virtual const typet &type() const
+  const typet &type() const override
   {
     return child_abstract_object->type();
   }
@@ -104,8 +104,8 @@ class context_abstract_objectt : public abstract_objectt
 
   // These are internal hooks that allow sub-classes to perform additional
   // actions when an abstract_object is set/unset to TOP
-  void make_top_internal() override;
-  void clear_top_internal() override;
+  void set_top_internal() override;
+  void set_not_top_internal() override;
 
   abstract_object_pointert read(
     const abstract_environmentt &env,
@@ -115,9 +115,9 @@ class context_abstract_objectt : public abstract_objectt
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,
-    const std::stack<exprt> stack,
+    const std::stack<exprt> &stack,
     const exprt &specifier,
-    const abstract_object_pointert value,
+    const abstract_object_pointert &value,
     bool merging_write) const override;
 
   bool has_been_modified(const abstract_object_pointert before) const override;