Merge pull request #5346 from danpoe/fixes/address-check

Treat uninitialized pointers like unknown pointers in address_check()

Author: danpoe

regression/cbmc/pointer-check-01/test.c

@@ -0,0 +1,9 @@
+void main()
+{
+  char *p;
+
+  if(p == 0)
+  {
+    *p;
+  }
+}

regression/cbmc/pointer-check-01/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that pointer check for *p fails when its value is constrained to 0

regression/cbmc/pointer-check-02/test.c

@@ -0,0 +1,11 @@
+void main()
+{
+  char *p;
+
+  {
+    int i;
+    __CPROVER_assume(p == &i);
+  }
+
+  *p;
+}

regression/cbmc/pointer-check-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that pointer check for *p fails when its value is constrained to point to
+an out-of-scope local variable

regression/cbmc/pointer-extra-checks/test.desc

@@ -8,7 +8,13 @@ main.c
 ^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: SUCCESS$
 ^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: SUCCESS$
 ^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
-^\[main.pointer_dereference.6\] .* dereference failure: pointer uninitialized in \*s: FAILURE$
+^\[main.pointer_dereference.6\] .* dereference failure: pointer invalid in \*s: FAILURE$
+^\[main.pointer_dereference.7\] .* dereference failure: pointer NULL in \*s: FAILURE$
+^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
+^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
+^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$
+^\[main.pointer_dereference.11\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
+^\[main.pointer_dereference.12\] .* dereference failure: invalid integer address in \*s: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
@@ -28,12 +34,6 @@ main.c
 ^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer uninitialized in \*r:
 ^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*r:
 ^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*r:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer NULL in \*s:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*s:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: deallocated dynamic object in \*s:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*s:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside dynamic object bounds in \*s:
-^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*s:
 --
 This test ensures that local_bitvector_analysis is correctly labelling obvious
 cases of pointers and that --pointer-check is not generating excess assertions.

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -3,8 +3,8 @@ test.c
 --harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
 ^EXIT=0$
 ^SIGNAL=0$
-\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
-\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS

src/analyses/goto_check.cpp

@@ -1282,30 +1282,24 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     const exprt in_bounds_of_some_explicit_allocation =
       disjunction(alloc_disjuncts);
 
-    if(flags.is_unknown() || flags.is_null())
-    {
-      conditions.push_back(conditiont(
-        or_exprt(
-          in_bounds_of_some_explicit_allocation,
-          not_exprt(null_pointer(address))),
-        "pointer NULL"));
-    }
+    const bool unknown = flags.is_unknown() || flags.is_uninitialized();
 
-    if(flags.is_unknown())
+    if(unknown)
     {
       conditions.push_back(conditiont{
         not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
     }
 
-    if(flags.is_uninitialized())
+    if(unknown || flags.is_null())
     {
-      conditions.push_back(
-        conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
-                            not_exprt{is_invalid_pointer_exprt{address}}},
-                   "pointer uninitialized"});
+      conditions.push_back(conditiont(
+        or_exprt(
+          in_bounds_of_some_explicit_allocation,
+          not_exprt(null_pointer(address))),
+        "pointer NULL"));
     }
 
-    if(flags.is_unknown() || flags.is_dynamic_heap())
+    if(unknown || flags.is_dynamic_heap())
     {
       conditions.push_back(conditiont(
         or_exprt(
@@ -1314,7 +1308,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         "deallocated dynamic object"));
     }
 
-    if(flags.is_unknown() || flags.is_dynamic_local())
+    if(unknown || flags.is_dynamic_local())
     {
       conditions.push_back(conditiont(
         or_exprt(
@@ -1323,7 +1317,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         "dead object"));
     }
 
-    if(flags.is_unknown() || flags.is_dynamic_heap())
+    if(unknown || flags.is_dynamic_heap())
     {
       const or_exprt object_bounds_violation(
         object_lower_bound(address, nil_exprt()),
@@ -1337,9 +1331,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         "pointer outside dynamic object bounds"));
     }
 
-    if(
-      flags.is_unknown() || flags.is_dynamic_local() ||
-      flags.is_static_lifetime())
+    if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
     {
       const or_exprt object_bounds_violation(
         object_lower_bound(address, nil_exprt()),
@@ -1354,7 +1346,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         "pointer outside object bounds"));
     }
 
-    if(flags.is_unknown() || flags.is_integer_address())
+    if(unknown || flags.is_integer_address())
     {
       conditions.push_back(conditiont(
         implies_exprt(