Merge pull request #7229 from tautschnig/bugfixes/7064-pointer-primitive-check

Pointer-primitive checks should succeed for valid pointers at object bound

Author: tautschnig

regression/cbmc/pointer-predicates/at_bounds1.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+int main()
+{
+  size_t s;
+  char *p = malloc(s);
+  // at __CPROVER_max_malloc_size p + s would overflow; all larger values of s
+  // make malloc return NULL when using --malloc-fail-null
+  if(p != NULL && s != __CPROVER_max_malloc_size)
+  {
+    char *q = p + s;
+    __CPROVER_assert(__CPROVER_r_ok(q, 0), "should be valid");
+    __CPROVER_assert(!__CPROVER_r_ok(q + 1, 0), "should fail");
+  }
+}

regression/cbmc/pointer-predicates/at_bounds1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+at_bounds1.c
+--pointer-primitive-check --malloc-fail-null
+^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verifies that the check succeeds when pointing to one-beyond-object-bounds.

regression/cbmc/pointer-primitive-check-03/test.desc

@@ -22,7 +22,8 @@ void main()
   // offset out of bounds
   char *p5 = malloc(10);
   p5 += 10;
-  __CPROVER_r_ok(p5, 1);
+  _Bool result = __CPROVER_r_ok(p5, 1);
+  __CPROVER_assert(!result, "should be false");
 
   // dead
   char *p6;

regression/cbmc/pointer-primitive-check-03/main.c renamed to regression/cbmc/r_w_ok10/main.c

@@ -0,0 +1,19 @@
+CORE
+main.c
+--pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main.pointer_primitives.\d+\] line 7 pointer invalid in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 7 pointer outside object bounds in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 11 pointer invalid in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 15 pointer outside object bounds in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 34 dead object in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 40 deallocated dynamic object in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\*\* 8 of \d+ failed
+--
+^warning: ignoring
+--
+Verifies that the pointer primitives check fails for the various forms of
+invalid pointers

regression/cbmc/r_w_ok10/test.desc

@@ -1454,15 +1454,8 @@ void goto_check_ct::pointer_primitive_check(
       return;
   }
 
-  const auto size_of_expr_opt =
-    size_of_expr(to_pointer_type(pointer.type()).base_type(), ns);
-
-  const exprt size = !size_of_expr_opt.has_value()
-                       ? from_integer(1, size_type())
-                       : size_of_expr_opt.value();
-
-  const conditionst &conditions =
-    get_pointer_points_to_valid_memory_conditions(pointer, size);
+  const conditionst &conditions = get_pointer_points_to_valid_memory_conditions(
+    pointer, from_integer(0, size_type()));
   for(const auto &c : conditions)
   {
     add_guarded_property(