__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

@@ -169,25 +169,28 @@ to pointers that point to within a memory object.
 
 ## Checking if a memory segment has at least a given size
 
-The following two primitives can be used to check whether there is a memory
-segment starting at the given pointer and extending for at least the given
-number of bytes:
+The following three primitives can be used to check whether there is a
+memory segment starting at the given pointer and extending for at least the
+given number of bytes:
 
 - `_Bool __CPROVER_r_ok(const void *p, size_t size)`
 - `_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
+At present, all three 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:
+is neither null nor valid, 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
+assert(__CPROVER_r_ok(p, 10)); // passes
 p += 5;
-assert(__CPROVER_r_ok(p, 3));  // valid
+assert(__CPROVER_r_ok(p, 3));  // passes
 assert(__CPROVER_r_ok(p, 10)); // fails
 ```
 
@@ -204,8 +207,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

@@ -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 &expr);
 
   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);
   }