Changed the pointer abstract object to store an expression

Before there was a problem where if we stored an abstract object that
get modified, as this would cause a copy, the pointer would point at the
old value. To resolve, just store an expression representing what it is
pointing to. This can then be re-evaluated by the enviroment to find its
current possible values.

Author: thk123

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -93,7 +93,7 @@ abstract_object_pointert abstract_environmentt::eval(
           std::dynamic_pointer_cast<pointer_abstract_objectt>(
             eval(dereference.pointer(), ns));
 
-        return pointer_abstract_object->read_dereference(*this);
+        return pointer_abstract_object->read_dereference(*this, ns);
       }
     },
     {
@@ -139,6 +139,7 @@ Function: abstract_environmentt::assign
   Inputs:
    expr - the expression to assign to
    value - the value to assign to the expression
+   ns - the namespace
 
  Outputs: ?
 
@@ -147,7 +148,7 @@ Function: abstract_environmentt::assign
 \*******************************************************************/
 
 bool abstract_environmentt::assign(
-  const exprt &expr, const abstract_object_pointert value)
+  const exprt &expr, const abstract_object_pointert value, const namespacet &ns)
 {
   assert(value);
 
@@ -188,7 +189,7 @@ bool abstract_environmentt::assign(
     {
       symbol_object=map[symbol_expr];
     }
-    final_value=write(symbol_object, value, stactions, false);
+    final_value=write(symbol_object, value, stactions, ns, false);
   }
   else
   {
@@ -218,6 +219,7 @@ Function: abstract_object_pointert abstract_environmentt::write
    rhs - the value we are trying to write to the left hand side
    remaining_stack - what is left of the stack before the rhs can replace or be
                      merged with the rhs
+   ns - the namespace
    merge_write - Are re replacing the left hand side with the right hand side
                  (e.g. we know for a fact that we are overwriting this object)
                  or could the write in fact not take place and therefore we
@@ -231,10 +233,12 @@ Function: abstract_object_pointert abstract_environmentt::write
           abstract_pointer and abstract_array until the stack is empty
 
 \*******************************************************************/
+
 abstract_object_pointert abstract_environmentt::write(
   abstract_object_pointert lhs,
   abstract_object_pointert rhs,
   std::stack<exprt> remaining_stack,
+  const namespacet &ns,
   bool merge_write)
 {
   assert(!remaining_stack.empty());
@@ -307,7 +311,7 @@ abstract_object_pointert abstract_environmentt::write(
 
         sharing_ptrt<pointer_abstract_objectt> modified_pointer=
           pointer_abstract_object->write_dereference(
-            *this, stack, rhs_object, merge_write);
+            *this, ns, stack, rhs_object, merge_write);
 
         return modified_pointer;
       }

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -22,13 +22,18 @@ class abstract_environmentt
   // These three are really the heart of the method
   virtual abstract_object_pointert eval(
     const exprt &expr, const namespacet &ns) const;
-  virtual bool assign(const exprt &expr, const abstract_object_pointert value);
+  virtual bool assign(
+    const exprt &expr,
+    const abstract_object_pointert value,
+    const namespacet &ns);
   virtual bool assume(const exprt &expr, const namespacet &ns);
 
-  virtual abstract_object_pointert write(abstract_object_pointert lhs,
-   abstract_object_pointert rhs,
-   std::stack<exprt> remaining_stack,
-   bool merge_write);
+  virtual abstract_object_pointert write(
+    abstract_object_pointert lhs,
+    abstract_object_pointert rhs,
+    std::stack<exprt> remaining_stack,
+    const namespacet &ns,
+    bool merge_write);
 
   virtual abstract_object_pointert abstract_object_factory(
     const typet type, bool top=true, bool bottom=false) const;

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -10,6 +10,7 @@
 #include <analyses/variable-sensitivity/abstract_enviroment.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
+#include <analyses/ai.h>
 #include "constant_pointer_abstract_object.h"
 
 /*******************************************************************\
@@ -30,7 +31,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     pointer_abstract_objectt(t)
 {
   assert(t.id()==ID_pointer);
-  value=enviroment.abstract_object_factory(t.subtype(), true, false);
+  value=nil_exprt();
 }
 
 /*******************************************************************\
@@ -54,7 +55,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     pointer_abstract_objectt(t, tp, bttm)
 {
   assert(t.id()==ID_pointer);
-  value=enviroment.abstract_object_factory(t.subtype(), top, bottom);
+  value=nil_exprt();
 }
 
 /*******************************************************************\
@@ -100,8 +101,8 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   // can create a pointer
   if(e.id()==ID_address_of)
   {
-    address_of_exprt address_expr(to_address_of_expr(e));
-    value=enviroment.eval(address_expr.object(), ns);
+    //address_of_exprt address_expr(to_address_of_expr(e));
+    value=e;
     top=false;
   }
   else
@@ -111,19 +112,19 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
       constant_exprt constant_expr(to_constant_expr(e));
       if(constant_expr.get_value()==ID_NULL)
       {
-        value=nullptr;
+        value=e;
         top=false;
       }
       else
       {
         // TODO(tkiley): These should probably be logged.
         // unknown type
-        value=enviroment.abstract_object_factory(type.subtype(), true, false);
+        value=nil_exprt();
       }
     }
     else
     {
-      value=enviroment.abstract_object_factory(type.subtype(), true, false);
+      value=nil_exprt();
     }
   }
 }
@@ -163,7 +164,7 @@ bool constant_pointer_abstract_objectt::merge_state(
     else
     {
       top=true;
-      value=nullptr;
+      value=nil_exprt();
       assert(!bottom);
       return !op1->top;
     }
@@ -195,16 +196,9 @@ exprt constant_pointer_abstract_objectt::to_constant() const
   }
   else
   {
-    if(value==nullptr)
-    {
-      return null_pointer_exprt(to_pointer_type(type));
-    }
-    else
-    {
-      const exprt &value_expr=value->to_constant();
-      address_of_exprt address_expr(value_expr);
-      return address_expr;
-    }
+    // TODO(tkiley): I think we would like to eval this before using it
+    // in the to_constant.
+    return value;
   }
 }
 
@@ -233,14 +227,25 @@ void constant_pointer_abstract_objectt::output(
   }
   else
   {
-    if(value==nullptr)
+    if(value.id()==ID_constant && value.get(ID_value)==ID_NULL)
     {
       out << "NULL";
     }
     else
     {
       out << "ptr ->(";
-      value->output(out, ai, ns);
+      if(value.id()==ID_address_of)
+      {
+        const address_of_exprt &address_expr(to_address_of_expr(value));
+        if(address_expr.object().id()==ID_symbol)
+        {
+          const symbol_exprt &symbol_pointed_to(
+            to_symbol_expr(address_expr.object()));
+
+          out << symbol_pointed_to.get_identifier();
+        }
+      }
+
       out << ")";
     }
   }
@@ -252,6 +257,7 @@ Function: constant_pointer_abstract_objectt::read_dereference
 
   Inputs:
    env - the environment
+   ns - the namespace
 
  Outputs: An abstract object representing the value this pointer is pointing
           to
@@ -263,18 +269,30 @@ Function: constant_pointer_abstract_objectt::read_dereference
 \*******************************************************************/
 
 abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
-  const abstract_environmentt &env) const
+  const abstract_environmentt &env, const namespacet &ns) const
 {
-  if(top || bottom || value==nullptr)
+  if(top || bottom || value.id()==ID_nil)
   {
     // Return top if dereferencing a null pointer or we are top
-    bool is_value_top = top || value==nullptr;
+    bool is_value_top = top || value.id()==ID_nil;
     return env.abstract_object_factory(
       type.subtype(), is_value_top, !is_value_top);
   }
   else
   {
-    return value;
+    if(value.id()==ID_address_of)
+    {
+      return env.eval(value.op0(), ns);
+    }
+    else if(value.id()==ID_constant)
+    {
+      // Reading a null pointer, return top
+      return env.abstract_object_factory(type.subtype(), true, false);
+    }
+    else
+    {
+      return env.abstract_object_factory(type.subtype(), true, false);
+    }
   }
 }
 
@@ -284,6 +302,7 @@ Function: constant_pointer_abstract_objectt::write_dereference
 
   Inputs:
    environment - the environment
+   ns - the namespace
    stack - the remaining stack
    new_value - the value to write to the dereferenced pointer
    merging_write - is it a merging write (i.e. we aren't certain
@@ -305,14 +324,15 @@ Function: constant_pointer_abstract_objectt::write_dereference
 sharing_ptrt<pointer_abstract_objectt>
   constant_pointer_abstract_objectt::write_dereference(
     abstract_environmentt &environment,
+    const namespacet &ns,
     const std::stack<exprt> stack,
     const abstract_object_pointert new_value,
     bool merging_write)
 {
   if(top || bottom)
   {
     return pointer_abstract_objectt::write_dereference(
-      environment, stack, new_value, merging_write);
+      environment, ns, stack, new_value, merging_write);
   }
   else
   {
@@ -324,19 +344,21 @@ sharing_ptrt<pointer_abstract_objectt>
 
       if(merging_write)
       {
+        abstract_object_pointert pointed_value=environment.eval(value, ns);
         bool modifications;
-        copy->value=value->merge(new_value, modifications);
+        pointed_value->merge(new_value, modifications);
       }
       else
       {
-        copy->value=new_value;
+        environment.assign(value, new_value, ns);
       }
       return copy;
     }
     else
     {
+      abstract_object_pointert pointed_value=environment.eval(value, ns);
       return std::dynamic_pointer_cast<constant_pointer_abstract_objectt>(
-        environment.write(value, new_value, stack, merging_write));
+        environment.write(pointed_value, new_value, stack, ns, merging_write));
     }
   }
 }

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -43,16 +43,17 @@ class constant_pointer_abstract_objectt:public pointer_abstract_objectt
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns);
 
   abstract_object_pointert read_dereference(
-    const abstract_environmentt &env) const;
+    const abstract_environmentt &env, const namespacet &ns) const;
 
   sharing_ptrt<pointer_abstract_objectt> write_dereference(
     abstract_environmentt &environment,
+    const namespacet &ns,
     const std::stack<exprt> stack,
     const abstract_object_pointert value,
     bool merging_write);
 
 private:
-  abstract_object_pointert value;
+  exprt value;
 
 
 };

src/analyses/variable-sensitivity/pointer_abstract_object.cpp

@@ -98,6 +98,7 @@ Function: pointer_abstract_objectt::read_dereference
 
   Inputs:
    env - the environment
+   ns - the namespace
 
  Outputs: An abstract object representing the value being pointed to
 
@@ -107,7 +108,7 @@ Function: pointer_abstract_objectt::read_dereference
 \*******************************************************************/
 
 abstract_object_pointert pointer_abstract_objectt::read_dereference(
-  const abstract_environmentt &env) const
+  const abstract_environmentt &env, const namespacet &ns) const
 {
   pointer_typet pointer_type(to_pointer_type(type));
   const typet &pointed_to_type=pointer_type.subtype();
@@ -121,6 +122,7 @@ Function: pointer_abstract_objectt::write_dereference
 
   Inputs:
    environment - the abstract environment
+   ns - the namespace
    stack - the remaining stack of expressions on the LHS to evaluate
    value - the value we are trying to assign to what the pointer is
            pointing to
@@ -141,6 +143,7 @@ Function: pointer_abstract_objectt::write_dereference
 sharing_ptrt<pointer_abstract_objectt>
   pointer_abstract_objectt::write_dereference(
     abstract_environmentt &environment,
+    const namespacet &ns,
     const std::stack<exprt> stack,
     const abstract_object_pointert value,
     bool merging_write)

src/analyses/variable-sensitivity/pointer_abstract_object.h

@@ -30,10 +30,11 @@ class pointer_abstract_objectt:public abstract_objectt
 
   // pointer interface
   virtual abstract_object_pointert read_dereference(
-    const abstract_environmentt &env) const;
+    const abstract_environmentt &env, const namespacet &ns) const;
 
   virtual sharing_ptrt<pointer_abstract_objectt> write_dereference(
     abstract_environmentt &environment,
+    const namespacet &ns,
     const std::stack<exprt> stack,
     const abstract_object_pointert value,
     bool merging_write);

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -54,7 +54,8 @@ void variable_sensitivity_domaint::transform(
     abstract_object_pointert top_object=
       abstract_state.abstract_object_factory(
         to_code_dead(instruction.code).symbol().type(), true);
-    abstract_state.assign(to_code_dead(instruction.code).symbol(), top_object);
+    abstract_state.assign(
+      to_code_dead(instruction.code).symbol(), top_object, ns);
     }
     break;
 
@@ -64,7 +65,7 @@ void variable_sensitivity_domaint::transform(
 
       // TODO : check return values
       abstract_object_pointert r = abstract_state.eval(inst.rhs(), ns);
-      abstract_state.assign(inst.lhs(), r);
+      abstract_state.assign(inst.lhs(), r, ns);
     }
     break;