diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c new file mode 100644 index 00000000000..479d5b4e916 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c @@ -0,0 +1,16 @@ +void foo(int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) + __CPROVER_requires(__CPROVER_pointer_equals(y, x) || 1) + __CPROVER_assigns(*y) +// clang-format on +{ + *y = 0; +} + +void main() +{ + int *x; + int *y; + foo(x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc new file mode 100644 index 00000000000..50338575985 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_equals` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_equals` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c new file mode 100644 index 00000000000..52dd0486677 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c @@ -0,0 +1,34 @@ +#include +void foo(int *a, int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int))) + __CPROVER_requires( + (__CPROVER_pointer_equals(x,a) && y == NULL) || + (x == NULL && __CPROVER_pointer_equals(y,a)) + ) + __CPROVER_assigns(y == NULL: *x) + __CPROVER_assigns(x == NULL: *y) +// clang-format on +{ + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(a, x)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(a, y)); + *y = 0; + } +} + +void main() +{ + int *a; + int *x; + int *y; + foo(a, x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc new file mode 100644 index 00000000000..bd71dc7d63a --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$ +^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts. +The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null, +or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`. +The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows +that both cases of the disjunction expressed in the requires clause are reachable. diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c new file mode 100644 index 00000000000..27b35453c39 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c @@ -0,0 +1,28 @@ + +typedef struct +{ + int *a; + int *x; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int))) + __CPROVER_ensures( + __CPROVER_pointer_equals( + __CPROVER_return_value.x, + __CPROVER_return_value.a) || 1) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *x = ret.x; + *x = 0; //expected to fail +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc new file mode 100644 index 00000000000..03832485dc2 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_equals` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_equals` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c new file mode 100644 index 00000000000..fb853f061f7 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c @@ -0,0 +1,49 @@ +#include +typedef struct +{ + int *a; + int *x; + int *y; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int))) + __CPROVER_ensures(( + __CPROVER_pointer_equals( + __CPROVER_return_value.x, + __CPROVER_return_value.a) && + __CPROVER_return_value.y == NULL + ) || ( + __CPROVER_return_value.x == NULL && + __CPROVER_pointer_equals( + __CPROVER_return_value.y, + __CPROVER_return_value.a))) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *a = ret.a; + int *x = ret.x; + int *y = ret.y; + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(x, a)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(y, a)); + *y = 0; + } +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc new file mode 100644 index 00000000000..1c5c5f7bc57 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.assertion.\d+\] line 33 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$ +^\[bar.assertion.\d+\] line 39 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts. +The postcondition of `foo` describes a disjunction of cases: either `x` equals `a` and `y` is null, +or `x` is null and `y` equals `a`. The function `bar` branches on `y == NULL`. +The test succeeds if the two `assert(0)` are falsifiable, which which shows that +both cases of the disjunction expressed in the ensures clause of `foo` are reachable. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 35bc45cb257..dea0fdc1b1d 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2591,7 +2591,19 @@ exprt c_typecheck_baset::do_special_functions( const irep_idt &identifier=to_symbol_expr(f_op).get_identifier(); - if(identifier == CPROVER_PREFIX "is_fresh") + if(identifier == CPROVER_PREFIX "pointer_equals") + { + if(expr.arguments().size() != 2) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "pointer_equals expects two operands; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } + else if(identifier == CPROVER_PREFIX "is_fresh") { if(expr.arguments().size() != 2) { diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index f0ae5e74004..d2d96df9d97 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -44,6 +44,7 @@ void __CPROVER_fence(const char *kind, ...); // contract-related functions __CPROVER_bool __CPROVER_is_freeable(const void *mem); __CPROVER_bool __CPROVER_was_freed(const void *mem); +__CPROVER_bool __CPROVER_pointer_equals(void *p, void *q); __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); __CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void)); // same as pointer_in_range with experimental support in contracts diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index e662bbbd599..5a64466659e 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1162,6 +1162,62 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr) #endif } +/// \brief Implementation of the `pointer_equals` front-end predicate. +/// +/// \param ptr1 First argument of the `pointer_equals` predicate +/// \param ptr2 Second argument of the `pointer_equals` predicate +/// \param write_set Write set which conveys the invocation context +/// (requires/ensures clause, assert/assume context); +/// +/// \details The behaviour is as follows: +/// When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`, +/// the predicate nondeterministically invalidates `*ptr1` and returns `false`, +/// or checks that `ptr2` is either NULL or valid, and assigns `*ptr1` to `ptr2`. +/// When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, +/// the predicate checks that both `*ptr1` and `ptr2` are either NULL or valid, +/// and returns the value of (*ptr1 == ptr2). +__CPROVER_bool __CPROVER_contracts_pointer_equals( + void **ptr1, + void *ptr2, + __CPROVER_contracts_write_set_ptr_t write_set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + (write_set != 0) & ((write_set->assume_requires_ctx == 1) | + (write_set->assert_requires_ctx == 1) | + (write_set->assume_ensures_ctx == 1) | + (write_set->assert_ensures_ctx == 1)), + "__CPROVER_is_fresh is used only in requires or ensures clauses"); +#ifdef __CPROVER_DFCC_DEBUG_LIB + __CPROVER_assert( + __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)), + "set readable"); +#endif + if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) + { + if(__VERIFIER_nondet___CPROVER_bool()) + { + __CPROVER_contracts_make_invalid_pointer(ptr1); + return 0; + } + __CPROVER_assert( + (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0), + "pointer_equals is only called with valid pointers"); + *ptr1 = ptr2; + return 1; + } + else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */ + { + void *derefd = *ptr1; + __CPROVER_assert( + (derefd == 0) || __CPROVER_r_ok(derefd, 0), + "pointer_equals is only called with valid pointers"); + __CPROVER_assert( + (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0), + "pointer_equals is only called with valid pointers"); + return derefd == ptr2; + } +} /// \brief Implementation of the `is_fresh` front-end predicate. /// diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index dfacdd636ee..b33c52692f0 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -29,6 +29,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_instrument_loop.cpp \ contracts/dynamic-frames/dfcc_library.cpp \ contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \ + contracts/dynamic-frames/dfcc_pointer_equals.cpp \ contracts/dynamic-frames/dfcc_is_fresh.cpp \ contracts/dynamic-frames/dfcc_pointer_in_range.cpp \ contracts/dynamic-frames/dfcc_is_freeable.cpp \ diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index b1b5230962e..039c622067f 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -29,6 +29,7 @@ Each of these translation passes is implemented in a specific class: @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh @ref dfcc_pointer_in_ranget | Implements @ref contracts-dev-spec-pointer-in-range + @ref dfcc_pointer_equalst | Implements @ref contracts-dev-spec-pointer-equals @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md index 22c64d14402..072fc75af0f 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md @@ -174,6 +174,9 @@ Calls to `__CPROVER_obeys_contract` are rewritten as described in Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in @subpage contracts-dev-spec-pointer-in-range +Calls to `__CPROVER_pointer_equals` are rewritten as described in +@subpage contracts-dev-spec-pointer-equals + For all other function or function pointer calls, we proceed as follows. If the function call has an LHS (i.e. its result is assigned to a return value diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md index 56f23746c0b..2f689dabd98 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md @@ -8,6 +8,9 @@ The C extensions for contract specification provide three pointer-related memory predicates: ```c +// Holds iff ptr1 and ptr2 are both either null or valid and are equal. +__CPROVER_bool __CPROVER_pointer_equals(void *ptr1, void* ptr2); + // Holds iff ptr is pointing to an object distinct to all objects pointed to by // other __CPROVER_is_fresh occurrences in the contract's pre and post conditions __CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size); diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md new file mode 100644 index 00000000000..c5a03bbe7b1 --- /dev/null +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md @@ -0,0 +1,25 @@ +# Rewriting Calls to the __CPROVER_pointer_equals Predicate {#contracts-dev-spec-pointer-equals} + +Back to top @ref contracts-dev-spec + +@tableofcontents + +In goto programs encoding pre or post conditions (generated from the contract +clauses) and in all user-defined functions, we simply replace calls to +`__CPROVER_pointer_equals` with calls to the library implementation. + +```c +__CPROVER_contracts_pointer_equals( + void **ptr1, + void *ptr2, + __CPROVER_contracts_write_set_ptr_t write_set); +``` + +This function implements the `__CPROVER_pointer_equals` behaviour in all +possible contexts (contract checking vs replacement, requires vs ensures clause +context, as described by the flags carried by the write set parameter). + +--- + Prev | Next +:-----|:------ + @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md index c8f06d4a174..5c97a1a893a 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md @@ -23,4 +23,4 @@ context, as described by the flags carried by the write set parameter). --- Prev | Next :-----|:------ - @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file + @ref contracts-dev | @ref contracts-dev-spec-pointer-equals \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index 2f966f83582..e2c526bd840 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -9,6 +9,49 @@ let users describe the shape of the memory accessed through pointers in _requires clauses_ and _ensures clauses_. Attempting to call these predicates outside of a requires or ensures clause context will result in a verification error. + +## The __CPROVER_pointer_equals predicate +### Syntax + +```c +bool __CPROVER_pointer_equals(void *p, void *q); +``` +This predicate can only be used in ensures and requires clauses and checks for +pointer validity and equality. + +#### Parameters + +`__CPROVER_pointer_equals` takes two pointers as arguments. + +#### Return Value + +It returns a `bool` value: +- `true` iff pointers are both null or valid and are equal, +- `false` otherwise. + +### Semantics + +#### Enforcement + +When checking a contract using `--enforce-contract foo`: +- used in a _requires_ clause, the predicate will check that `ptr2` is always + either null or valid, and it will make `ptr1` equal to `ptr2`. + This results in a state resulting in a state where both pointers are either + null or valid and equal; +- used in an _ensures_ clause it will check that memory both pointers are always + either null or valid and equal. + +#### Replacement + +When checking a contract using `--replace-call-with-contract foo`, we get the +dual behaviour: +- used in a _requires_ clause it will check that memory both pointers are always + either null or valid and equal, +- used in an _ensures_ clause, the predicate will check that `ptr2` is always + either null or valid, and it will make `ptr1` equal to `ptr2`. + This results in a state resulting in a state where both pointers are either + null or valid and equal. + ## The __CPROVER_is_fresh predicate ### Syntax diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index ea0417d3371..4b7302cd2c2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -37,6 +37,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_is_fresh.h" #include "dfcc_library.h" #include "dfcc_obeys_contract.h" +#include "dfcc_pointer_equals.h" #include "dfcc_pointer_in_range.h" #include "dfcc_spec_functions.h" #include "dfcc_utils.h" @@ -525,6 +526,11 @@ void dfcc_instrumentt::instrument_instructions( dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts) { + // rewrite pointer_equals calls + dfcc_pointer_equalst pointer_equals(library, message_handler); + pointer_equals.rewrite_calls( + goto_program, first_instruction, last_instruction, cfg_info); + // rewrite pointer_in_range calls dfcc_pointer_in_ranget pointer_in_range(library, message_handler); pointer_in_range.rewrite_calls( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp index 1da53f0245f..2c945eb8acd 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp @@ -53,6 +53,7 @@ init_function_symbols(std::unordered_set &function_symbols) "contracts_obj_set_create_indexed_by_object_id"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove"); + function_symbols.insert(CPROVER_PREFIX "contracts_pointer_equals"); function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc"); function_symbols.insert(CPROVER_PREFIX "contracts_was_freed"); function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated"); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 242b330b4d3..efa62681c5f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -125,6 +125,7 @@ const std::map create_dfcc_fun_to_name() {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"}, {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"}, {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"}, + {dfcc_funt::POINTER_EQUALS, CONTRACTS_PREFIX "pointer_equals"}, {dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"}, {dfcc_funt::POINTER_IN_RANGE_DFCC, CONTRACTS_PREFIX "pointer_in_range_dfcc"}, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index aa49b9fe536..68e243200b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -126,6 +126,8 @@ enum class dfcc_funt LINK_ALLOCATED, /// \see __CPROVER_contracts_link_deallocated LINK_DEALLOCATED, + /// \see __CPROVER_contracts_pointer_equals + POINTER_EQUALS, /// \see __CPROVER_contracts_is_fresh IS_FRESH, /// \see __CPROVER_contracts_pointer_in_range_dfcc diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index ef8300f1182..52034128cd6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -7,6 +7,10 @@ Date: August 2022 \*******************************************************************/ +// TODO when scanning the goto functions to detect pointer predicates, +// replace pointer equality p == q with __CPROVER_pointer_equals(p,q) +// in all user-defined memory predicates. + #include "dfcc_lift_memory_predicates.h" #include @@ -44,7 +48,8 @@ bool dfcc_lift_memory_predicatest::is_lifted_function( /// True iff function_id is a core memory predicate static bool is_core_memory_predicate(const irep_idt &function_id) { - return (function_id == CPROVER_PREFIX "is_fresh") || + return (function_id == CPROVER_PREFIX "pointer_equals") || + (function_id == CPROVER_PREFIX "is_fresh") || (function_id == CPROVER_PREFIX "pointer_in_range_dfcc") || (function_id == CPROVER_PREFIX "obeys_contract"); } @@ -231,7 +236,15 @@ void dfcc_lift_memory_predicatest::collect_parameters_to_lift( { const irep_idt &callee_id = to_symbol_expr(it.call_function()).get_identifier(); - if(callee_id == CPROVER_PREFIX "is_fresh") + if(callee_id == CPROVER_PREFIX "pointer_equals") + { + auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } + else if(callee_id == CPROVER_PREFIX "is_fresh") { auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); if(opt_rank.has_value()) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp new file mode 100644 index 00000000000..a5fbfea3fa7 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp @@ -0,0 +1,145 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: Jan 2025 + +\*******************************************************************/ + +#include "dfcc_pointer_equals.h" + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "dfcc_cfg_info.h" +#include "dfcc_library.h" + +dfcc_pointer_equalst::dfcc_pointer_equalst( + dfcc_libraryt &library, + message_handlert &message_handler) + : library(library), message_handler(message_handler), log(message_handler) +{ +} + +void dfcc_pointer_equalst::rewrite_calls( + goto_programt &program, + dfcc_cfg_infot cfg_info) +{ + rewrite_calls( + program, + program.instructions.begin(), + program.instructions.end(), + cfg_info); +} + +void dfcc_pointer_equalst::rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + dfcc_cfg_infot cfg_info) +{ + auto &target = first_instruction; + while(target != last_instruction) + { + if(target->is_function_call()) + { + const auto &function = target->call_function(); + + if(function.id() == ID_symbol) + { + const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + + if(fun_name == CPROVER_PREFIX "pointer_equals") + { + // add address on first operand + target->call_arguments()[0] = + address_of_exprt(target->call_arguments()[0]); + + // fix the function name. + to_symbol_expr(target->call_function()) + .set_identifier( + library.dfcc_fun_symbol[dfcc_funt::POINTER_EQUALS].name); + + // pass the write_set + target->call_arguments().push_back(cfg_info.get_write_set(target)); + } + } + } + target++; + } +} + +class pointer_equality_visitort : public expr_visitort +{ +private: + std::vector equality_exprs_to_transform; + +public: + void visit_expr(exprt &expr) + { + if(expr.id() == ID_equal) + { + const equal_exprt &equal_expr = to_equal_expr(expr); + + // Check if both operands are pointers + if( + equal_expr.lhs().type().id() == ID_pointer && + equal_expr.rhs().type().id() == ID_pointer) + { + equality_exprs_to_transform.push_back(&expr); + } + } + } + + // Apply the transformations after visiting + void transform() + { + const code_typet pointer_equals_type( + {code_typet::parametert(pointer_type(void_type())), + code_typet::parametert(pointer_type(void_type()))}, + bool_typet()); + + symbol_exprt pointer_equals("ID_pointer_equals", pointer_equals_type); + + for(exprt *expr_ptr : equality_exprs_to_transform) + { + const equal_exprt &equal_expr = to_equal_expr(*expr_ptr); + + // Create the function call to __CPROVER_pointer_equals + // Add the original equality operands as arguments + side_effect_expr_function_callt result( + pointer_equals, + {equal_expr.lhs(), equal_expr.rhs()}, + bool_typet(), + equal_expr.source_location()); + + result.arguments().push_back(equal_expr.lhs()); + result.arguments().push_back(equal_expr.rhs()); + + // Set the type of the function call + result.type() = bool_typet(); + + // Replace the original expression + *expr_ptr = result; + } + } +}; + +// Usage function +void rewrite_equal_exprt_to_pointer_equals(exprt &expr) +{ + pointer_equality_visitort visitor; + + // First collect all equality expressions + expr.visit(visitor); + + // Then transform them + visitor.transform(); +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h new file mode 100644 index 00000000000..350d87d03c7 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h @@ -0,0 +1,65 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: Jan 2025 + +\*******************************************************************/ + +/// \file +/// Instruments occurrences of pointer_equals predicates in programs +/// encoding requires and ensures clauses of contracts. + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H + +#include + +#include + +class goto_modelt; +class message_handlert; +class dfcc_libraryt; +class dfcc_cfg_infot; +class exprt; + +/// Rewrites `equal_exprt` over pointers into calls +/// to the front-end function `__CPROVER_pointer_equals`, +/// at the expression level. Meant to be Applied before GOTO conversion +/// of function contract clauses, followed by `rewrite_calls`. +void rewrite_equal_exprt_to_pointer_equals(exprt &expr); + +/// Rewrites calls to pointer_equals predicates into calls +/// to the library implementation. +class dfcc_pointer_equalst +{ +public: + /// \param library The contracts instrumentation library + /// \param message_handler Used for messages + dfcc_pointer_equalst( + dfcc_libraryt &library, + message_handlert &message_handler); + + /// Rewrites calls to pointer_equals predicates into calls + /// to the library implementation in the given program, passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info); + + /// Rewrites calls to pointer_equals predicates into calls + /// to the library implementation in the given program between + /// first_instruction (included) and last_instruction (excluded), passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + dfcc_cfg_infot cfg_info); + +protected: + dfcc_libraryt &library; + message_handlert &message_handler; + messaget log; +}; + +#endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 45d83370521..a625383f182 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -27,6 +27,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_lift_memory_predicates.h" +#include "dfcc_pointer_equals.h" #include "dfcc_utils.h" /// Generate the contract write set @@ -563,6 +564,8 @@ void dfcc_wrapper_programt::encode_requires_clauses() "Check requires clause of contract " + id2string(contract_symbol.name) + " for function " + id2string(wrapper_id)); } + // // rewrite pointer equalities before goto conversion + // TODO rewrite_equal_exprt_to_pointer_equals(requires_lmbd); codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl); converter.goto_convert(requires_statement, requires_program, language_mode); } @@ -614,7 +617,8 @@ void dfcc_wrapper_programt::encode_ensures_clauses() "Check ensures clause of contract " + id2string(contract_symbol.name) + " for function " + id2string(wrapper_id)); } - + // // rewrite pointer equalities before goto conversion + // TODO rewrite_equal_exprt_to_pointer_equals(ensures); codet ensures_statement(statement_type, {std::move(ensures)}, sl); converter.goto_convert(ensures_statement, ensures_program, language_mode); }