__CPROVER_r/w_ok does not require null or a valid pointer

The definition of __CPROVER_r/w_ok (in goto_check.cpp) does include the case
of an invalid pointer, and thus, there is no need to check that the pointer
given to these predicates is valid.

Author: kroening

doc/architectural/memory-primitives.md

@@ -177,19 +177,25 @@ given number of bytes:
 - `_Bool __CPROVER_w_ok(const void *p, size_t size)`
 - `_Bool __CPROVER_rw_ok(const void *p, size_t size)`
 
-At present, both primitives are equivalent as all memory in CBMC is considered
-both readable and writeable. If `p` is the null pointer, the primitives return
-false. If `p` is valid, the primitives return true if the memory segment
-starting at the pointer has at least the given size, and false otherwise. If `p`
-is neither null nor valid, the semantics is unspecified. It is valid to apply
-the primitive to pointers that point to within a memory object. For example:
+At present, all three primitives are equivalent as all memory in CBMC is
+considered both readable and writeable.  If `p` points to a valid object the
+primitives return true if the memory segment starting at the pointer has at
+least the given size, and false otherwise.  Specificially, when `size` is
+zero, and `p` points to the byte one beyond the end of the object, the
+predicate returns true.
+
+If `p` is either null or does not point to a valid object, the predicate
+returns false.
+
+It is valid to apply the primitive to pointers that have a nonzero offset.
+For example:
 
 ```C
 char *p = malloc(10);
-assert(__CPROVER_r_ok(p, 10)); // valid
-p += 5;
-assert(__CPROVER_r_ok(p, 3));  // valid
-assert(__CPROVER_r_ok(p, 10)); // fails
+assert(__CPROVER_r_ok(p, 10)); // passes
+assert(__CPROVER_r_ok(p + 5, 3));  // passes
+assert(__CPROVER_r_ok(p + 5, 10)); // fails
+assert(__CPROVER_r_ok(p + 10, 0)); // passes
 ```
 
 # Detecting potential misuses of memory primitives
@@ -205,8 +211,6 @@ primitives are either null or valid:
 - `__CPROVER_same_object`
 - `__CPROVER_OBJECT_SIZE`
 - `__CPROVER_DYNAMIC_OBJECT`
-- `__CPROVER_r_ok`
-- `__CPROVER_w_ok`
 
 While the first three primitives have well-defined semantics even on invalid
 pointers, using them on invalid pointers is usually unintended in user programs.

regression/cbmc/pointer-primitive-check-01/main.c

@@ -18,11 +18,5 @@ void main()
   __CPROVER_OBJECT_SIZE(p4);
 
   char *p5;
-  __CPROVER_r_ok(p5, 1);
-
-  char *p6;
-  __CPROVER_w_ok(p6, 1);
-
-  char *p7;
-  __CPROVER_DYNAMIC_OBJECT(p7);
+  __CPROVER_DYNAMIC_OBJECT(p5);
 }

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

@@ -19,18 +19,10 @@ main.c
 \[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
 \[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
 \[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
-\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
-\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
-\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
-\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
-\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
-\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
-\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
+\[main.pointer_primitives.17\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p5\): FAILURE
+\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p5\): SUCCESS
+\[main.pointer_primitives.19\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p5\): SUCCESS
+\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p5\): FAILURE
 --
 ^warning: ignoring
 --

regression/cbmc/pointer-primitive-check-04/main.c

@@ -7,20 +7,24 @@ int main()
 
   assert(!__CPROVER_r_ok(p, sizeof(int)));
   assert(!__CPROVER_w_ok(p, sizeof(int)));
+  assert(!__CPROVER_r_ok(p, 0));
+  assert(!__CPROVER_w_ok(p, 0));
 
   p = malloc(sizeof(int));
 
   assert(__CPROVER_r_ok(p, 1));
   assert(__CPROVER_w_ok(p, 1));
   assert(__CPROVER_r_ok(p, sizeof(int)));
   assert(__CPROVER_w_ok(p, sizeof(int)));
+  assert(__CPROVER_r_ok(p + 1, 0));
+  assert(__CPROVER_w_ok(p + 1, 0));
 
   size_t n;
   char *arbitrary_size = malloc(n);
 
   assert(__CPROVER_r_ok(arbitrary_size, n));
   assert(__CPROVER_w_ok(arbitrary_size, n));
 
-  assert(__CPROVER_r_ok(arbitrary_size, n + 1));
-  assert(__CPROVER_w_ok(arbitrary_size, n + 1));
+  assert(__CPROVER_r_ok(arbitrary_size, n + 1)); // expected to fail
+  assert(__CPROVER_w_ok(arbitrary_size, n + 1)); // expected to fail
 }

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

@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 12 failed
+^\*\* 2 of 16 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/r_w_ok1/main.c

@@ -201,12 +201,12 @@ class goto_checkt
   /// \param guard: the condition under which the operation happens
   void pointer_primitive_check(const exprt &expr, const guardt &guard);
 
-  /// Returns true if the given expression is a pointer primitive such as
-  /// __CPROVER_r_ok()
+  /// Returns true if the given expression is a pointer primitive
+  /// that requires a pointer primitive check
   ///
   /// \param expr expression
   /// \return true if the given expression is a pointer primitive
-  bool is_pointer_primitive(const exprt &expr);
+  bool requires_pointer_primitive_check(const exprt &);
 
   optionalt<goto_checkt::conditiont>
   get_pointer_is_null_condition(const exprt &address, const exprt &size);
@@ -1282,10 +1282,7 @@ void goto_checkt::pointer_primitive_check(
   if(expr.source_location().is_built_in())
     return;
 
-  const exprt pointer =
-    (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
-      ? to_r_or_w_ok_expr(expr).pointer()
-      : to_unary_expr(expr).op();
+  const exprt pointer = to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
 
@@ -1317,15 +1314,13 @@ void goto_checkt::pointer_primitive_check(
   }
 }
 
-bool goto_checkt::is_pointer_primitive(const exprt &expr)
+bool goto_checkt::requires_pointer_primitive_check(const exprt &expr)
 {
   // we don't need to include the __CPROVER_same_object primitive here as it
   // is replaced by lower level primitives in the special function handling
   // during typechecking (see c_typecheck_expr.cpp)
   return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
-         expr.id() == ID_object_size || expr.id() == ID_r_ok ||
-         expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
-         expr.id() == ID_is_dynamic_object;
+         expr.id() == ID_object_size || expr.id() == ID_is_dynamic_object;
 }
 
 goto_checkt::conditionst goto_checkt::get_pointer_dereferenceable_conditions(
@@ -1795,7 +1790,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_validity_check(to_dereference_expr(expr), expr, guard);
   }
-  else if(is_pointer_primitive(expr))
+  else if(requires_pointer_primitive_check(expr))
   {
     pointer_primitive_check(expr, guard);
   }