diff --git a/doc/architectural/memory-primitives.md b/doc/architectural/memory-primitives.md index 7ce7dbcf3d8..2b9f5d86db8 100644 --- a/doc/architectural/memory-primitives.md +++ b/doc/architectural/memory-primitives.md @@ -169,26 +169,33 @@ 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 -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 @@ -204,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. diff --git a/regression/cbmc/pointer-primitive-check-01/main.c b/regression/cbmc/pointer-primitive-check-01/main.c index 4aa5419b48f..53dc948516d 100644 --- a/regression/cbmc/pointer-primitive-check-01/main.c +++ b/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); } diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index c1130edfcff..ffb5ce81dc7 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/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 -- diff --git a/regression/cbmc/pointer-primitive-check-04/main.c b/regression/cbmc/pointer-primitive-check-04/main.c deleted file mode 100644 index 8031c6e830e..00000000000 --- a/regression/cbmc/pointer-primitive-check-04/main.c +++ /dev/null @@ -1,6 +0,0 @@ - -void main() -{ - char *p; - __CPROVER_assume(__CPROVER_r_ok(p, 1)); -} diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc deleted file mode 100644 index 3c9f2d5f074..00000000000 --- a/regression/cbmc/pointer-primitive-check-04/test.desc +++ /dev/null @@ -1,14 +0,0 @@ -CORE -main.c ---pointer-primitive-check -^EXIT=10$ -^SIGNAL=0$ -\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(p, .*1\): FAILURE -\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(p, .*1\): SUCCESS -\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(p, .*1\): SUCCESS -\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(p, .*1\): FAILURE --- -^warning: ignoring --- -Verifies that the check fails for a primitive in an assume that uses an -uninitialized pointer diff --git a/regression/cbmc/r_w_ok1/main.c b/regression/cbmc/r_w_ok1/main.c index 0a24178df9c..06c5bb850a0 100644 --- a/regression/cbmc/r_w_ok1/main.c +++ b/regression/cbmc/r_w_ok1/main.c @@ -7,6 +7,8 @@ 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)); @@ -14,6 +16,8 @@ int main() 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); @@ -21,6 +25,6 @@ int main() 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 } diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index 6a461a6a137..96345e622e8 100644 --- a/regression/cbmc/r_w_ok1/test.desc +++ b/regression/cbmc/r_w_ok1/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$ diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index b65855454d4..6dc27aad94b 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -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 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); }