Use the write_stack in the constant_pointer_abstract_object

Author: thk123

regression/goto-analyzer/sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c

@@ -8,20 +8,21 @@ int main(int argc, char *argv[])
   int *p=a;
   __CPROVER_assert(p==&a[0], "p==&a[0]");
 
+  // Read through pointer
   __CPROVER_assert(*p==1, "*p==1");
 
+  // Read through offset pointer
   __CPROVER_assert(p[1]==2, "p[1]==2");
   __CPROVER_assert(1[p]==2, "1[p]==2");
 
   __CPROVER_assert(*(p+1)==2, "*(p+1)==2");
   __CPROVER_assert(*(1+p)==2, "*(1+p)==2");
 
-  __CPROVER_assert(*(p-1)==1, "*(p-1)==1");
-
   // Test pointer arithmetic
   int *q=&a[1];
   __CPROVER_assert(q==p+1, "q==p+1");
   __CPROVER_assert(*q==2, "*q==2");
+  __CPROVER_assert(*(q-1)==1, "*(q-1)==1");
 
   // Test pointer diffs
   ptrdiff_t x=1;

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc

@@ -13,14 +13,14 @@ sensitivity_test_constants_array_of_constants_pointer.c
 ^\[main.assertion.8\] .* \*b\[1\]==13: Failure \(if reachable\)$
 ^\[main.assertion.9\] .* \*\(b\+1\)==&b1: Success$
 ^\[main.assertion.10\] .* \*\(b\+1\)==&b3: Failure \(if reachable\)$
-^\[main.assertion.11\] .* \*\(1\+b\)==&b1: Unknown$
-^\[main.assertion.12\] .* \*\(1\+b\)==&b3: Unknown$
+^\[main.assertion.11\] .* \*\(1\+b\)==&b1: Success$
+^\[main.assertion.12\] .* \*\(1\+b\)==&b3: Failure \(if reachable\)$
 ^\[main.assertion.13\] .* 1\[b\]==&b1: Success$
 ^\[main.assertion.14\] .* 1\[b\]==&b3: Failure \(if reachable\)$
 ^\[main.assertion.15\] .* \*\*\(b\+1\)==11: Success$
 ^\[main.assertion.16\] .* \*\*\(b\+1\)==13: Failure \(if reachable\)$
-^\[main.assertion.17\] .* \*\*\(1\+b\)==11: Unknown$
-^\[main.assertion.18\] .* \*\*\(1\+b\)==13: Unknown$
+^\[main.assertion.17\] .* \*\*\(1\+b\)==11: Success$
+^\[main.assertion.18\] .* \*\*\(1\+b\)==13: Failure \(if reachable\)$
 ^\[main.assertion.19\] .* \*1\[b\]==11: Success$
 ^\[main.assertion.20\] .* \*1\[b\]==13: Failure \(if reachable\)$
 ^\[main.assertion.21\] .* c\[0\]==&c0: Unknown$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc

@@ -5,18 +5,18 @@ sensitivity_test_constants_pointer_to_constants_array.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* p==&a\[0\]: Success$
 ^\[main.assertion.2\] .* \*p==1: Success$
-^\[main\.assertion\.3\] .* p\[1\]==2: Unknown$
-^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
-^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
-^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main\.assertion\.8\] .* q==p\+1: Unknown$
-^\[main\.assertion\.9\] .* \*q==2: Unknown$
+^\[main\.assertion\.3\] .* p\[1\]==2: Success$
+^\[main\.assertion\.4\] .* 1\[p\]==2: Success$
+^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Success$
+^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Success$
+^\[main\.assertion\.7\] .* q==p\+1: Success$
+^\[main\.assertion\.8\] .* \*q==2: Success$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Success$
 ^\[main\.assertion\.10\] .* q-p==x: Unknown$
-^\[main\.assertion\.11\] .* a\[1\]==4: Unknown$
-^\[main\.assertion\.12\] .* a\[1\]==5: Unknown$
-^\[main\.assertion\.13\] .* a\[1\]==6: Unknown$
-^\[main\.assertion\.14\] .* a\[1\]==7: Unknown$
+^\[main\.assertion\.11\] .* a\[1\]==4: Success$
+^\[main\.assertion\.12\] .* a\[1\]==5: Success$
+^\[main\.assertion\.13\] .* a\[1\]==6: Success$
+^\[main\.assertion\.14\] .* a\[1\]==7: Success$
 ^\[main\.assertion\.15\] .* \*r==2: Unknown$
 ^\[main\.assertion\.16\] .* \*r==1: Unknown$
 ^\[main\.assertion\.17\] .* \*s==0: Unknown$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc

@@ -9,9 +9,9 @@ sensitivity_test_constants_pointer_to_two_value_array.c
 ^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
 ^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
 ^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main.assertion.8\] .* q==p\+1: Unknown$
-^\[main.assertion.9\] .* \*q==2: Unknown$
+^\[main.assertion\.7\] .* q==p\+1: Success$
+^\[main.assertion\.8\] .* \*q==2: Unknown$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Unknown$
 ^\[main.assertion.10\] .* q-p==x: Unknown$
 ^\[main.assertion.11\] .* a\[1\]==4: Unknown$
 ^\[main.assertion.12\] .* a\[1\]==5: Unknown$

regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/test.desc

@@ -9,9 +9,9 @@ sensitivity_test_two_value_pointer_to_two_value_array.c
 ^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
 ^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
 ^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main\.assertion\.8\] .* q==p\+1: Unknown$
-^\[main\.assertion\.9\] .* \*q==2: Unknown$
+^\[main\.assertion\.7\] .* q==p\+1: Unknown$
+^\[main\.assertion\.8\] .* \*q==2: Unknown$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Unknown$
 ^\[main\.assertion\.10\] .* q-p==x: Unknown$
 ^\[main\.assertion\.11\] .* a\[1\]==4: Unknown$
 ^\[main\.assertion\.12\] .* a\[1\]==5: Unknown$

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -32,7 +32,6 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     pointer_abstract_objectt(t)
 {
   assert(t.id()==ID_pointer);
-  value=nil_exprt();
 }
 
 /*******************************************************************\
@@ -56,7 +55,6 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     pointer_abstract_objectt(t, tp, bttm)
 {
   assert(t.id()==ID_pointer);
-  value=nil_exprt();
 }
 
 /*******************************************************************\
@@ -74,7 +72,7 @@ Function: constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const constant_pointer_abstract_objectt &old):
-    pointer_abstract_objectt(old), value(old.value)
+    pointer_abstract_objectt(old), value_stack(old.value_stack)
 {}
 
 /*******************************************************************\
@@ -94,26 +92,11 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const exprt &e,
   const abstract_environmentt &environment,
   const namespacet &ns):
-    pointer_abstract_objectt(e, environment, ns)
+    pointer_abstract_objectt(e, environment, ns),
+    value_stack(e, environment, ns)
 {
   assert(e.type().id()==ID_pointer);
-  value=nil_exprt();
-
-  if(e.id()==ID_address_of)
-  {
-    value=e;
-    top=false;
-  }
-  else if(e.id()==ID_constant)
-  {
-    constant_exprt constant_expr(to_constant_expr(e));
-    if(constant_expr.get_value()==ID_NULL)
-    {
-      value=e;
-      top=false;
-    }
-  }
-  // Else unknown expression type - possibly we should handle more
+  top=value_stack.is_top_value();
 }
 
 /*******************************************************************\
@@ -174,8 +157,10 @@ abstract_object_pointert
   }
   else
   {
-    // Can we actually merge these value
-    if(value==other->value)
+    bool matching_pointer=
+      value_stack.to_expression()==other->value_stack.to_expression();
+
+    if(matching_pointer)
     {
       return shared_from_this();
     }
@@ -213,7 +198,7 @@ exprt constant_pointer_abstract_objectt::to_constant() const
   {
     // TODO(tkiley): I think we would like to eval this before using it
     // in the to_constant.
-    return value;
+    return value_stack.to_expression();
   }
 }
 
@@ -236,33 +221,27 @@ Function: constant_pointer_abstract_objectt::output
 void constant_pointer_abstract_objectt::output(
   std::ostream &out, const ai_baset &ai, const namespacet &ns) const
 {
-  if(is_top() || is_bottom())
+  if(is_top() || is_bottom() || value_stack.is_top_value())
   {
     pointer_abstract_objectt::output(out, ai, ns);
   }
   else
   {
-    if(value.id()==ID_constant && value.get(ID_value)==ID_NULL)
-    {
-      out << "NULL";
-    }
-    else
+    out << "ptr ->(";
+    const exprt &value=value_stack.to_expression();
+    if(value.id()==ID_address_of)
     {
-      out << "ptr ->(";
-      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 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();
-        }
-      }
+        const symbol_exprt &symbol_pointed_to(
+          to_symbol_expr(address_expr.object()));
 
-      out << ")";
+        out << symbol_pointed_to.get_identifier();
+      }
     }
+
+    out << ")";
   }
 }
 
@@ -286,28 +265,16 @@ Function: constant_pointer_abstract_objectt::read_dereference
 abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
   const abstract_environmentt &env, const namespacet &ns) const
 {
-  if(is_top() || is_bottom() || value.id()==ID_nil)
+  if(is_top() || is_bottom() || value_stack.is_top_value())
   {
     // Return top if dereferencing a null pointer or we are top
-    bool is_value_top = is_top() || value.id()==ID_nil;
+    bool is_value_top = is_top() || value_stack.is_top_value();
     return env.abstract_object_factory(
       type().subtype(), ns, is_value_top, !is_value_top);
   }
   else
   {
-    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(), ns, true, false);
-    }
-    else
-    {
-      return env.abstract_object_factory(type().subtype(), ns, true, false);
-    }
+    return env.eval(value_stack.to_expression().op0(), ns);
   }
 }
 
@@ -344,22 +311,13 @@ sharing_ptrt<pointer_abstract_objectt>
     const abstract_object_pointert new_value,
     bool merging_write) const
 {
-  if(is_top() || is_bottom())
+  if(is_top() || is_bottom() || value_stack.is_top_value())
   {
     return pointer_abstract_objectt::write_dereference(
       environment, ns, stack, new_value, merging_write);
   }
   else
   {
-    // If not an address, we don't know what we are pointing to
-    if(value.id()!=ID_address_of)
-    {
-      return pointer_abstract_objectt::write_dereference(
-        environment, ns, stack, new_value, merging_write);
-    }
-
-    const address_of_exprt &address_expr=to_address_of_expr(value);
-
     sharing_ptrt<constant_pointer_abstract_objectt> copy=
       sharing_ptrt<constant_pointer_abstract_objectt>(
         new constant_pointer_abstract_objectt(*this));
@@ -369,26 +327,30 @@ sharing_ptrt<pointer_abstract_objectt>
       // We should not be changing the type of an abstract object
       assert(new_value->type()==type().subtype());
 
-
+      // Get an expression that we can assign to
+      exprt value=value_stack.to_expression().op0();
       if(merging_write)
       {
         abstract_object_pointert pointed_value=
-          environment.eval(address_expr.object(), ns);
+          environment.eval(value, ns);
         bool modifications;
         abstract_object_pointert merged_value=
           abstract_objectt::merge(pointed_value, new_value, modifications);
-        environment.assign(address_expr.object(), merged_value, ns);
+        environment.assign(value, merged_value, ns);
       }
       else
       {
-        environment.assign(address_expr.object(), new_value, ns);
+        environment.assign(value, new_value, ns);
       }
     }
     else
     {
+      exprt value=value_stack.to_expression().op0();
       abstract_object_pointert pointed_value=
-        environment.eval(address_expr.object(), ns);
-      environment.write(pointed_value, new_value, stack, ns, merging_write);
+        environment.eval(value, ns);
+      abstract_object_pointert modified_value=
+        environment.write(pointed_value, new_value, stack, ns, merging_write);
+        environment.assign(value, modified_value, ns);
 
       // but the pointer itself does not change!
     }

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -11,6 +11,7 @@
 #include <iosfwd>
 
 #include <analyses/variable-sensitivity/pointer_abstract_object.h>
+#include <analyses/variable-sensitivity/write_stack.h>
 
 class constant_pointer_abstract_objectt:public pointer_abstract_objectt
 {
@@ -57,7 +58,7 @@ class constant_pointer_abstract_objectt:public pointer_abstract_objectt
   abstract_object_pointert merge_constant_pointers(
     const constant_pointer_abstract_pointert other) const;
 
-  exprt value;
+  write_stackt value_stack;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H // NOLINT(*)