From 1405144aab8d0ea951df89d81e59a4c554b7b3a8 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 16 Jan 2025 17:19:06 -0500 Subject: [PATCH] Add new pointer_equals predicate Havoc to invalid for function contracts --- .../main.c | 16 ++ .../test.desc | 20 +++ .../main.c | 34 ++++ .../test.desc | 32 ++++ .../main.c | 28 ++++ .../test.desc | 17 ++ .../main.c | 49 ++++++ .../test.desc | 32 ++++ src/ansi-c/c_typecheck_expr.cpp | 14 +- src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/library/cprover_contracts.c | 142 ++++++++++++----- src/goto-instrument/Makefile | 1 + .../doc/developer/contracts-dev-arch.md | 1 + .../contracts-dev-spec-dfcc-instrument.md | 3 + ...ts-dev-spec-memory-predicates-rewriting.md | 3 + .../contracts-dev-spec-pointer-equals.md | 25 +++ .../contracts-dev-spec-pointer-in-range.md | 4 +- .../doc/user/contracts-memory-predicates.md | 43 ++++++ .../dynamic-frames/dfcc_instrument.cpp | 6 + .../dynamic-frames/dfcc_instrument_loop.cpp | 1 + .../dynamic-frames/dfcc_is_cprover_symbol.cpp | 1 + .../contracts/dynamic-frames/dfcc_library.cpp | 2 + .../contracts/dynamic-frames/dfcc_library.h | 4 + .../dfcc_lift_memory_predicates.cpp | 13 +- .../dynamic-frames/dfcc_pointer_equals.cpp | 145 ++++++++++++++++++ .../dynamic-frames/dfcc_pointer_equals.h | 65 ++++++++ .../dynamic-frames/dfcc_spec_functions.cpp | 50 ++++-- .../dynamic-frames/dfcc_spec_functions.h | 29 +++- .../dynamic-frames/dfcc_wrapper_program.cpp | 6 +- 29 files changed, 726 insertions(+), 61 deletions(-) create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc create mode 100644 src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h 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..ee7887f294b --- /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: FAILURE$ +^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$ +^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer NULL in \*y: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer invalid in \*y: UNKNOWN$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: deallocated dynamic object in \*y: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: dead object in \*y: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*y: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 8 dereference failure: invalid integer address in \*y: UNKNOWN$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions, +the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to +false the target pointer of the predicate remains undefined. 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..97ba8f9024d --- /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 16 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that \*x is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: dead object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line 22 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[foo.assertion.\d+\] line 23 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$ +^\[foo.assigns.\d+\] line 24 Check that \*y is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_in_range_dfcc` under disjunctions in assume contexts. +The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null, +or `x` is null and `y` is in range of `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..ae39751e332 --- /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 24 dereference failure: pointer NULL in \*x: FAILURE$ +^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: UNKNOWN$ +^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: FAILURE$ +^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: FAILURE$ +^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: FAILURE$ +^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: UNKNOWN$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions, +the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to +false the target pointer remains undefined. 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..d0f29a67b8a --- /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 35 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line 36 assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line 37 Check that \*x is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: dead object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[bar.assertion.\d+\] line 41 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line 42 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[bar.assertion.\d+\] line 43 assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line 44 Check that \*y is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: dead object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_in_range` under disjunctions in assume contexts. +The postcondition of `foo` describes a disjunction of cases: either `x` is in range of `a` and `y` is null, +or `x` is null and `y` is in range of `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 e1a2466f1e4..7892f869c3f 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1136,9 +1136,82 @@ void *__CPROVER_contracts_malloc( __CPROVER_size_t, __CPROVER_contracts_write_set_ptr_t); +/// \brief Makes the given pointer invalid. +/// +/// Used to craft invalid pointers when pointer predicates return false +/// in "assume" mode. +void __CPROVER_contracts_make_invalid_pointer(void **ptr) +{ +#ifndef DFCC_SIMPLE_INVALID + *ptr = (void *)__VERIFIER_nondet_size(); +#else + void *dummy = __CPROVER_allocate(0, 0); + __CPROVER_deallocated = + __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated; + *ptr = __VERIFIER_nondet___CPROVER_bool() ? dummy : (void *)0; +#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 DFCC_DEBUG + __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. /// -/// The behaviour depends on the boolean flags carried by \p set +/// The behaviour depends on the boolean flags carried by \p write_set /// which reflect the invocation context: checking vs. replacing a contract, /// in a requires or an ensures clause context. /// \param elem First argument of the `is_fresh` predicate @@ -1204,23 +1277,14 @@ __CPROVER_HIDE:; "__CPROVER_is_fresh max allocation size exceeded"); __CPROVER_assume(size <= __CPROVER_max_malloc_size); } + + // SOUNDNESS: allow predicate to fail if(__VERIFIER_nondet___CPROVER_bool()) { - // in the failure case, make pointer null or pointing to a unique - // dummy deallocated object of size 0. - if(__VERIFIER_nondet___CPROVER_bool()) - { - *elem = (void *)0; - } - else - { - void *dummy = __CPROVER_allocate(0, 0); - __CPROVER_deallocated = - __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated; - *elem = dummy; - } + __CPROVER_contracts_make_invalid_pointer(elem); return 0; } + void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; @@ -1274,23 +1338,14 @@ __CPROVER_HIDE:; "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size"); __CPROVER_assume(size <= __CPROVER_max_malloc_size); } + + // SOUNDNESS: allow predicate to fail if(__VERIFIER_nondet___CPROVER_bool()) { - // in the failure case, make pointer null or pointing to a unique - // dummy deallocated object of size 0. - if(__VERIFIER_nondet___CPROVER_bool()) - { - *elem = (void *)0; - } - else - { - void *dummy = __CPROVER_allocate(0, 0); - __CPROVER_deallocated = - __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated; - *elem = dummy; - } + __CPROVER_contracts_make_invalid_pointer(elem); return 0; } + void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; @@ -1343,7 +1398,7 @@ __CPROVER_HIDE:; if(seen->elems[object_id] != 0) return 0; #endif - // record fresh object in the object set + // record fresh object in the object set #ifdef DFCC_DEBUG // manually inlined below __CPROVER_contracts_obj_set_add(seen, ptr); @@ -1365,6 +1420,23 @@ __CPROVER_HIDE:; } } +/// \brief Implementation of the `pointer_in_range_dfcc` front-end predicate. +/// +/// The behaviour depends on the boolean flags carried by \p write_set +/// which reflect the invocation context: checking vs. replacing a contract, +/// in a requires or an ensures clause context. +/// \param lb Lower bound pointer +/// \param ptr Target pointer of the predicate +/// \param ub Upper bound pointer +/// \param write_set Write set in which seen/allocated objects are recorded; +/// +/// \details The behaviour is as follows: +/// - When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`, +/// the predicate checks that \p lb and \p ub are valid, into the same object, +/// ordered, and checks that \p ptr is between \p lb and \p ub. +/// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, +/// the predicate checks that \p lb and \p ub are valid, into the same object, +/// ordered, and assigns \p ptr to some nondet offset between \p lb and \p ub. __CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc( void *lb, void **ptr, @@ -1392,19 +1464,7 @@ __CPROVER_HIDE:; { if(__VERIFIER_nondet___CPROVER_bool()) { - // in the failure case, make pointer null or pointing to a unique - // dummy deallocated object of size 0. - if(__VERIFIER_nondet___CPROVER_bool()) - { - *ptr = (void *)0; - } - else - { - void *dummy = __CPROVER_allocate(0, 0); - __CPROVER_deallocated = - __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated; - *ptr = dummy; - } + __CPROVER_contracts_make_invalid_pointer(ptr); return 0; } 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..c7b33c52491 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_euqalst | 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..7f7507ae68a 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 @@ -9,7 +9,7 @@ clauses) and in all user-defined functions, we simply replace calls to `__CPROVER_pointer_in_range_dfcc` with calls to the library implementation. ```c -__CPROVER_pointer_in_range_dfcc( +__CPROVER_contracts_pointer_in_range_dfcc( void *lb, void **ptr, void *ub, @@ -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_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 7f6acd75e7f..08d7a497a1c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -121,6 +121,7 @@ void dfcc_instrument_loopt::operator()( function_id, write_set_populate_instrs, loop.addr_of_write_set_var, + dfcc_ptr_havoc_modet::NONDET, havoc_instrs, nof_targets); spec_functions.to_spec_assigns_instructions( 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..71bd2121cc7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -125,6 +125,8 @@ 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::MAKE_INVALID_POINTER, CONTRACTS_PREFIX "make_invalid_pointer"}, + {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..3d0668e4f9e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -126,6 +126,10 @@ enum class dfcc_funt LINK_ALLOCATED, /// \see __CPROVER_contracts_link_deallocated LINK_DEALLOCATED, + /// \see __CPROVER_contracts_make_invalid_pointer + MAKE_INVALID_POINTER, + /// \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..1eec3a7a27c 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 @@ -44,7 +44,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 +232,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..063bddb9022 --- /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_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 1772647fc94..265a99ad924 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -103,6 +103,7 @@ void dfcc_spec_functionst::generate_havoc_function( havoc_function_id, original_program, write_set_symbol.symbol_expr(), + dfcc_ptr_havoc_modet::INVALID, havoc_program, nof_targets); @@ -144,6 +145,7 @@ void dfcc_spec_functionst::generate_havoc_instructions( const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, + dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets) { @@ -191,8 +193,9 @@ void dfcc_spec_functionst::generate_havoc_instructions( // DECL __havoc_target; // CALL __havoc_target = havoc_hook(set, next_idx); // IF !__havoc_target GOTO label; - // ASSIGN *__havoc_target = nondet(target_type); - // label: DEAD __havoc_target; + // .... add code for scalar or pointer targets ... + // label: + // DEAD __havoc_target; // ``` // declare a local var to store targets havoced via nondet assignment auto &target_type = get_target_type(ins_it->call_arguments().at(0)); @@ -213,13 +216,42 @@ void dfcc_spec_functionst::generate_havoc_instructions( havoc_program.add(goto_programt::make_incomplete_goto( dfcc_utilst::make_null_check_expr(target_expr), location)); - // create nondet assignment to the target - side_effect_expr_nondett nondet(target_type, location); - havoc_program.add(goto_programt::make_assignment( - dereference_exprt{typecast_exprt::conditional_cast( - target_expr, pointer_type(target_type))}, - nondet, - location)); + if( + ptr_havoc_mode == dfcc_ptr_havoc_modet::INVALID && + target_type.id() == ID_pointer) + { + // ``` + // DECL *__invalid_ptr; + // ASSIGN *__havoc_target = __invalid_ptr; + // DEAD __invalid_ptr; + // ``` + const auto invalid_ptr_expr = dfcc_utilst::create_symbol( + goto_model.symbol_table, + target_type, + function_id, + "__invalid_ptr", + location); + + havoc_program.add(goto_programt::make_assignment( + dereference_exprt{typecast_exprt::conditional_cast( + target_expr, pointer_type(target_type))}, + invalid_ptr_expr, + location)); + havoc_program.add( + goto_programt::make_dead(invalid_ptr_expr, location)); + } + else + { + // ``` + // ASSIGN *__havoc_target = nondet(target_type); + // ``` + side_effect_expr_nondett nondet(target_type, location); + havoc_program.add(goto_programt::make_assignment( + dereference_exprt{typecast_exprt::conditional_cast( + target_expr, pointer_type(target_type))}, + nondet, + location)); + } auto label = havoc_program.add(goto_programt::make_dead(target_expr, location)); goto_instruction->complete_goto(label); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index e75f025f800..45a92c21ac5 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -32,6 +32,19 @@ class message_handlert; class symbolt; class conditional_target_group_exprt; +/// \brief Represents the different ways to havoc pointers. +/// +/// Remark: +/// - Function contracts use invalid +/// - Loop contracts use nondet +enum class dfcc_ptr_havoc_modet +{ + /// havocs the pointer to an invalid pointer + INVALID, + /// havocs the pointer to an nondet pointer + NONDET +}; + /// This class rewrites GOTO functions that use the built-ins: /// - `__CPROVER_assignable`, /// - `__CPROVER_object_whole`, @@ -48,6 +61,9 @@ class dfcc_spec_functionst message_handlert &message_handler, dfcc_libraryt &library); + /// Generates the havoc function for a function contract. + /// Pointer-typed targets are turned into invalid pointers by the havoc. + /// /// From a function: /// /// ``` @@ -62,10 +78,12 @@ class dfcc_spec_functionst /// /// Which havocs the targets specified by `function_id`, passed /// - /// \param function_id function to generate instructions from - /// \param havoc_function_id write set variable to havoc - /// \param nof_targets maximum number of targets to havoc - /// + /// \param[in] function_id function to generate instructions from + /// \param[in] havoc_function_id write set variable to havoc + /// \param[in] make_havoced_pointers_invalid if true, havoc turns pointers + /// into invalid pointers. Otherwise, makes them nondeterministic, i.e. + /// range over all addresses known by symex so far. + /// \param[out] nof_targets maximum number of targets to havoc void generate_havoc_function( const irep_idt &function_id, const irep_idt &havoc_function_id, @@ -89,13 +107,14 @@ class dfcc_spec_functionst /// \param[in] function_id function id to use for prefixing fresh variables /// \param[in] original_program program from which to derive the havoc program /// \param[in] write_set_to_havoc write set symbol to havoc + /// \param[in] ptr_havoc_mode havocing mode for pointers /// \param[out] havoc_program destination program for havoc instructions /// \param[out] nof_targets max number of havoc targets discovered - /// void generate_havoc_instructions( const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, + dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets); 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..c4003d36f49 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 + // 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 + // 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); }