From c0c7808d6c1a4e0549bb84c3ff74d92d340cb464 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 22 Jan 2025 12:05:02 -0500 Subject: [PATCH] CONTRACTS: demonic encoding for is_fresh separation set, uniqueness of pointer requires/ensures To reduce array theory usage, use a nondet demonic variable to track the set of fresh objects and implement separation checks for is fresh (replaces a bool array indexed by object ID). In the same way, track the set of locations storing pointers that are targets of pointer predicates, and add assertions to prove that at most one pointer predicate is established per pointer. This detects and avoids situations where a badly written requires or ensures clause would require conflicting predicates to hold for a same pointer in a requires or ensures clause. Adds a new type `__CPROVER_contracts_ptr_pred_ctx_t` and utility functions in `cprover_contracts.c` to store these new pointer predicate context information used to support pointer predicate evaluation. Propagate changes to `dfcc_libraryt` and `dfcc_wrapper_programt`. Add new tests for pointer assumption uniqueness checks Fix failing tests that used is_fresh under negation in ensures Update dev doc fix failing tests --- .../test_aliasing_ensure/main.c | 34 +-- .../test_aliasing_ensure/test.desc | 4 - .../main.c | 20 ++ .../test.desc | 11 + .../main.c | 20 ++ .../test.desc | 10 + .../main.c | 22 ++ .../test.desc | 11 + .../main.c | 22 ++ .../test.desc | 10 + .../main.c | 22 ++ .../test.desc | 10 + .../main.c | 22 ++ .../test.desc | 10 + .../main.c | 20 ++ .../test.desc | 10 + .../main.c | 20 ++ .../test.desc | 10 + .../main.c | 22 ++ .../test.desc | 11 + .../main.c | 22 ++ .../test.desc | 10 + .../main.c | 17 ++ .../test.desc | 11 + .../main.c | 17 ++ .../test.desc | 14 + .../main.c | 21 ++ .../test.desc | 10 + .../main.c | 32 +++ .../test.desc | 10 + .../main.c | 22 ++ .../test.desc | 11 + .../test_scalar_memory_enforce/main.c | 1 - src/ansi-c/library/cprover_contracts.c | 249 ++++++++++++------ .../contracts-dev-spec-dfcc-runtime.md | 4 +- .../dynamic-frames/dfcc_is_cprover_symbol.cpp | 4 +- .../contracts/dynamic-frames/dfcc_library.cpp | 36 ++- .../contracts/dynamic-frames/dfcc_library.h | 34 ++- .../dynamic-frames/dfcc_wrapper_program.cpp | 56 ++-- .../dynamic-frames/dfcc_wrapper_program.h | 29 +- 40 files changed, 763 insertions(+), 168 deletions(-) create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc diff --git a/regression/contracts-dfcc/test_aliasing_ensure/main.c b/regression/contracts-dfcc/test_aliasing_ensure/main.c index 9b66c5589cd..d59bfe7deb1 100644 --- a/regression/contracts-dfcc/test_aliasing_ensure/main.c +++ b/regression/contracts-dfcc/test_aliasing_ensure/main.c @@ -1,35 +1,15 @@ -#include -#include -#include - -int z; - -// clang-format off -int foo(int *x, int *y) - __CPROVER_assigns(z, *x) - __CPROVER_requires( - __CPROVER_is_fresh(x, sizeof(int)) && - *x > 0 && - *x < 4) - __CPROVER_ensures( - __CPROVER_is_fresh(y, sizeof(int)) && - !__CPROVER_is_fresh(x, sizeof(int)) && - x != NULL && - x != y && - __CPROVER_return_value == *x + 5) +int *foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int))) // clang-format on { - *x = *x + 4; - y = malloc(sizeof(*y)); - *y = *x; - z = *y; - return (*x + 5); + int *ret = malloc(sizeof(int)); + __CPROVER_assume(ret); + return ret; } int main() { - int n = 4; - n = foo(&n, &n); - assert(!(n < 4)); + foo(); return 0; } diff --git a/regression/contracts-dfcc/test_aliasing_ensure/test.desc b/regression/contracts-dfcc/test_aliasing_ensure/test.desc index 11f828e0e09..f4672b8a3ee 100644 --- a/regression/contracts-dfcc/test_aliasing_ensure/test.desc +++ b/regression/contracts-dfcc/test_aliasing_ensure/test.desc @@ -4,10 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ -\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS -\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS -\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c new file mode 100644 index 00000000000..3e0f9019148 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c @@ -0,0 +1,20 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires(__CPROVER_pointer_equals(y, x) && __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc new file mode 100644 index 00000000000..a9518be3f8e --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming the more than one pointer predicate on the same target pointer +at the same time triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c new file mode 100644 index 00000000000..d59373da733 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c @@ -0,0 +1,20 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires(__CPROVER_pointer_equals(y, x) || __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1 || *x == 0) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc new file mode 100644 index 00000000000..fc07efa0e6c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that a same pointer can be the target of multiple pointer predicates as +long as they do not apply at the same time. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c new file mode 100644 index 00000000000..1baed0c514f --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_pointer_in_range_dfcc(x, y, x) && + __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc new file mode 100644 index 00000000000..45f29f51e98 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming the more than one pointer predicate on the same target pointer +at the same time triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c new file mode 100644 index 00000000000..7ff64a79922 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_pointer_in_range_dfcc(x, y, x) || + __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc new file mode 100644 index 00000000000..ce6d882dbfa --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that more than one predicate can be assumed on a same target as long at +they don't hold at the same time. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c new file mode 100644 index 00000000000..1a4cb7173c7 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_pointer_in_range_dfcc(x, y, x) && + __CPROVER_pointer_in_range_dfcc(x, y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc new file mode 100644 index 00000000000..516be7ab02e --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.6] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming more than one pointer predicate on the same target pointer triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c new file mode 100644 index 00000000000..c51b17dd142 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_pointer_in_range_dfcc(x, y, x) || + __CPROVER_pointer_in_range_dfcc(x, y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc new file mode 100644 index 00000000000..fc07efa0e6c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that a same pointer can be the target of multiple pointer predicates as +long as they do not apply at the same time. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c new file mode 100644 index 00000000000..9ccae900abe --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c @@ -0,0 +1,20 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) && __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1 || *x == 0) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc new file mode 100644 index 00000000000..0f5932dd18d --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming more than one pointer predicate on the same target pointer triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c new file mode 100644 index 00000000000..2a8f24a3e55 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c @@ -0,0 +1,20 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) || __CPROVER_pointer_equals(y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1 || *x == 0) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc new file mode 100644 index 00000000000..fc07efa0e6c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that a same pointer can be the target of multiple pointer predicates as +long as they do not apply at the same time. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c new file mode 100644 index 00000000000..066174498c7 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_is_fresh(y, sizeof(int)) && + __CPROVER_pointer_in_range_dfcc(x, y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1 || *x == 0) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc new file mode 100644 index 00000000000..1c685d2a1fb --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming the more than one pointer predicate on the same target pointer +at the same time triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c new file mode 100644 index 00000000000..780bcd8e768 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_is_fresh(y, sizeof(int)) || + __CPROVER_pointer_in_range_dfcc(x, y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1 || *x == 0) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc new file mode 100644 index 00000000000..fc07efa0e6c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that a same pointer can be the target of multiple pointer predicates as +long as they do not apply at the same time. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c new file mode 100644 index 00000000000..cc39fa82856 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c @@ -0,0 +1,17 @@ +void foo(int *x) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_assigns(*x) +__CPROVER_ensures(*x == 0) +// clang-format on +{ + *x = 0; +} + +int main() +{ + int *x; + foo(x); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc new file mode 100644 index 00000000000..64699f20363 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming the more than one pointer predicate on the same target pointer +at the same time triggers a failure. diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c new file mode 100644 index 00000000000..e338a05dd25 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c @@ -0,0 +1,17 @@ +void foo(int *x) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) || __CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_assigns(*x) +__CPROVER_ensures(*x == 0) +// clang-format on +{ + *x = 0; +} + +int main() +{ + int *x; + foo(x); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc new file mode 100644 index 00000000000..703a129c1b0 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc @@ -0,0 +1,14 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that a same pointer can be the target of multiple pointer predicates as +long as they do not apply at the same time. +- `x` is fresh and inialized to 0 +- `y` is equal to `x`if select is true, or fresh otherwise +- foo assigns y to 1 +- x is equal to 1 if select is true, 0 otherwise diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c new file mode 100644 index 00000000000..db9611a59f2 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/main.c @@ -0,0 +1,21 @@ +void foo(int *x, int *y, int **z) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(z, sizeof(int*))) +__CPROVER_requires(__CPROVER_pointer_equals(*z, x)) +__CPROVER_assigns(*z) +__CPROVER_ensures(__CPROVER_pointer_equals(*z, y)) +// clang-format on +{ + *z = y; +} + +int main() +{ + int *x; + int *y; + int **z; + foo(x, y, z); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc new file mode 100644 index 00000000000..12ffdbea606 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_enforce_reset_before_requires_equals_equals_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that assuming different predicates on a same pointer is possible across pre and post conditions. +Initially *z equals x, after the call *z equals y. diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c new file mode 100644 index 00000000000..d878f006513 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/main.c @@ -0,0 +1,32 @@ +void foo(int *x, int *y, int **z) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(z, sizeof(int*))) +__CPROVER_requires(__CPROVER_pointer_equals(*z, x)) +__CPROVER_assigns(*z) +__CPROVER_ensures(__CPROVER_pointer_equals(*z, y)) +// clang-format on +{ + *z = y; +} + +void bar() + // clang-format off +__CPROVER_requires(1) +__CPROVER_assigns() +__CPROVER_ensures(1) +// clang-format on +{ + int x; + int y; + int *z = &x; + foo(&x, &y, &z); + assert(z == &y); +} + +int main() +{ + bar(); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc new file mode 100644 index 00000000000..0d7313a649c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_replace_reset_before_requires_equals_equals_pass/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract bar --replace-call-with-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that assuming different predicates on a same pointer is possible across pre and post conditions. +Initially *z equals x, after the call *z equals y. diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c new file mode 100644 index 00000000000..1a4cb7173c7 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c @@ -0,0 +1,22 @@ +void foo(int *x, int *y) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(*x == 0) +__CPROVER_requires( + __CPROVER_pointer_in_range_dfcc(x, y, x) && + __CPROVER_pointer_in_range_dfcc(x, y, x)) +__CPROVER_assigns(*y) +__CPROVER_ensures(*y == 1) +__CPROVER_ensures(*x == 1) +// clang-format on +{ + *y = 1; +} + +int main() +{ + int *x; + int *y; + foo(x, y); + return 0; +} diff --git a/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc new file mode 100644 index 00000000000..1c685d2a1fb --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Tests that assuming the more than one pointer predicate on the same target pointer +at the same time triggers a failure. diff --git a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c index b22c93fe00f..ff6bbd8a739 100644 --- a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c +++ b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c @@ -21,7 +21,6 @@ int foo(int *x) ptr_ok(x)) __CPROVER_ensures( !ptr_ok(x) && - !__CPROVER_is_fresh(x, sizeof(int)) && return_ok(__CPROVER_return_value, x)) // clang-format on { diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 5a64466659e..afa583a110a 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -64,9 +64,28 @@ typedef struct void **elems; } __CPROVER_contracts_obj_set_t; -/// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t. +/// \brief Type of pointers to \ref __CPROVER_contracts_obj_set_t. typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; +/// \brief Stores context information supporting the evaluation of pointer +/// predicates in both assume and assert contexts for all predicates: +/// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract. +typedef struct +{ + /// \brief Nondet variable ranging over the set of objects allocated + /// by __CPROVER_contracts_is_fresh. Used to check separation constraints + /// in __CPROVER_contracts_is_fresh. + void *fresh_ptr; + /// \brief Nondet variable ranging over the set of locations storing + /// pointers on which predicates were assumed/asserted. Used to ensure + /// that at most one predicate is assumed per pointer. + void **ptr_pred; +} __CPROVER_contracts_ptr_pred_ctx_t; + +/// \brief Type of pointers to \ref __CPROVER_contracts_ptr_pred_ctx_t. +typedef __CPROVER_contracts_ptr_pred_ctx_t + *__CPROVER_contracts_ptr_pred_ctx_ptr_t; + /// \brief Runtime representation of a write set. typedef struct { @@ -84,7 +103,7 @@ typedef struct __CPROVER_contracts_obj_set_t deallocated; /// \brief Pointer to object set supporting the is_fresh predicate checks /// (indexed mode) - __CPROVER_contracts_obj_set_ptr_t linked_is_fresh; + __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx; /// \brief Object set recording the is_fresh allocations in post conditions __CPROVER_contracts_obj_set_ptr_t linked_allocated; /// \brief Object set recording the deallocations (used by was_freed) @@ -393,6 +412,27 @@ __CPROVER_HIDE:; return set->elems[object_id] == ptr; } +/// \brief Resets the nondet tracker for pointer predicates in \p set. +/// Invoked right between requires and ensures clauses to allow ensures clauses +/// to establish a different pointer predicates on the same pointers. +void __CPROVER_contracts_ptr_pred_ctx_init( + __CPROVER_contracts_ptr_pred_ctx_ptr_t set) +{ +__CPROVER_HIDE:; + set->fresh_ptr = (void *)0; + set->ptr_pred = (void **)0; +} + +/// \brief Resets the nondet tracker for pointer predicates in \p set. +/// Invoked right between requires and ensures clauses to allow ensures clauses +/// to establish a different pointer predicates on the same pointers. +void __CPROVER_contracts_ptr_pred_ctx_reset( + __CPROVER_contracts_ptr_pred_ctx_ptr_t set) +{ +__CPROVER_HIDE:; + set->ptr_pred = (void **)0; +} + /// \brief Initialises a \ref __CPROVER_contracts_write_set_t object. /// \param[inout] set Pointer to the object to initialise /// \param[in] contract_assigns_size Max size of the assigns clause @@ -434,7 +474,7 @@ __CPROVER_HIDE:; &(set->contract_frees_append), contract_frees_size); __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated)); __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated)); - set->linked_is_fresh = 0; + set->linked_ptr_pred_ctx = 0; set->linked_allocated = 0; set->linked_deallocated = 0; set->assume_requires_ctx = assume_requires_ctx; @@ -473,8 +513,8 @@ __CPROVER_HIDE:; __CPROVER_deallocate(set->contract_frees_append.elems); __CPROVER_deallocate(set->allocated.elems); __CPROVER_deallocate(set->deallocated.elems); - // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems - // since they are owned by someone else. + // do not free set->linked_ptr_pred_ctx->elems or + // set->deallocated_linked->elems since they are owned by someone else. } /// \brief Inserts a snapshot of the range starting at \p ptr of size \p size @@ -1060,23 +1100,23 @@ __CPROVER_HIDE:; } /// \brief Links \p is_fresh_set to -/// \p write_set->linked_is_fresh so that the is_fresh predicates +/// \p write_set->linked_ptr_pred_ctx so that the is_fresh predicates /// can be evaluated in requires and ensures clauses. -void __CPROVER_contracts_link_is_fresh( +void __CPROVER_contracts_link_ptr_pred_ctx( __CPROVER_contracts_write_set_ptr_t write_set, - __CPROVER_contracts_obj_set_ptr_t is_fresh_set) + __CPROVER_contracts_ptr_pred_ctx_ptr_t ptr_pred_ctx) { __CPROVER_HIDE:; #ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(write_set != 0, "write_set not NULL"); #endif - if((is_fresh_set != 0)) + if((ptr_pred_ctx != 0)) { - write_set->linked_is_fresh = is_fresh_set; + write_set->linked_ptr_pred_ctx = ptr_pred_ctx; } else { - write_set->linked_is_fresh = 0; + write_set->linked_ptr_pred_ctx = 0; } } @@ -1202,7 +1242,15 @@ __CPROVER_HIDE:; } __CPROVER_assert( (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0), - "pointer_equals is only called with valid pointers"); + "__CPROVER_pointer_equals is only called with valid pointers"); + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != ptr1, + "__CPROVER_pointer_equals does not conflict with other pointer " + "predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? ptr1 + : write_set->linked_ptr_pred_ctx->ptr_pred; *ptr1 = ptr2; return 1; } @@ -1211,11 +1259,23 @@ __CPROVER_HIDE:; void *derefd = *ptr1; __CPROVER_assert( (derefd == 0) || __CPROVER_r_ok(derefd, 0), - "pointer_equals is only called with valid pointers"); + "__CPROVER_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; + "__CPROVER_pointer_equals is only called with valid pointers"); + if(derefd != ptr2) + { + return 0; + } + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != ptr1, + "__CPROVER_pointer_equals does not conflict with other pointer " + "predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? ptr1 + : write_set->linked_ptr_pred_ctx->ptr_pred; + return 1; } } @@ -1229,16 +1289,14 @@ __CPROVER_HIDE:; /// \param write_set Write set in which seen/allocated objects are recorded; /// /// \details The behaviour is as follows: -/// - When \p set->assume_requires_ctx is `true`, the predicate allocates a new -/// object, records the object in \p set->linked_is_fresh, updates \p *elem to -/// point to the fresh object and returns `true`; -/// - When \p set->assume_ensures_ctx is `true`, the predicate allocates a new -/// object, records the object in \p set->linked_allocated, updates \p *elem -/// to point to the fresh object and returns `true`; +/// - When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`, +/// returns false if another pointer predicate is already assumed for the target +/// pointer, otherwise, allocates a fresh object for `*elem` and records +/// *elem and elem in the pointer predicate context struct. /// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, -/// the predicate first computes wether \p *elem is in \p set->linked_is_fresh -/// and returns false if it is. Otherwise it records the object in -/// \p set->linked_is_fresh and returns the value of r_ok(*elem, size). +/// returns false if another pointer predicate is already assumed for the target +/// pointer, otherwise, checks validity and separation separation of *elem +/// and records *elem and elem in the pointer predicate context struct. __CPROVER_bool __CPROVER_contracts_is_fresh( void **elem, __CPROVER_size_t size, @@ -1256,7 +1314,7 @@ __CPROVER_HIDE:; __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)), "set readable"); __CPROVER_assert( - write_set->linked_is_fresh, "set->linked_is_fresh is not NULL"); + write_set->linked_ptr_pred_ctx, "set->linked_ptr_pred_ctx is not NULL"); #endif if(write_set->assume_requires_ctx) { @@ -1294,9 +1352,19 @@ __CPROVER_HIDE:; __CPROVER_contracts_make_invalid_pointer(elem); return 0; } - void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != elem, + "__CPROVER_is_fresh does not conflict with other pointer predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? elem + : write_set->linked_ptr_pred_ctx->ptr_pred; + write_set->linked_ptr_pred_ctx->fresh_ptr = + __VERIFIER_nondet___CPROVER_bool() + ? ptr + : write_set->linked_ptr_pred_ctx->fresh_ptr; // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); @@ -1308,18 +1376,6 @@ __CPROVER_HIDE:; // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; -#ifdef __CPROVER_DFCC_DEBUG_LIB - // manually inlined below - __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr); -#else - __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); - write_set->linked_is_fresh->nof_elems = - (write_set->linked_is_fresh->elems[object_id] != 0) - ? write_set->linked_is_fresh->nof_elems - : write_set->linked_is_fresh->nof_elems + 1; - write_set->linked_is_fresh->elems[object_id] = ptr; - write_set->linked_is_fresh->is_empty = 0; -#endif return 1; } else if(write_set->assume_ensures_ctx) @@ -1357,6 +1413,17 @@ __CPROVER_HIDE:; void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != elem, + "__CPROVER_is_fresh does not conflict with other pointer predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? elem + : write_set->linked_ptr_pred_ctx->ptr_pred; + write_set->linked_ptr_pred_ctx->fresh_ptr = + __VERIFIER_nondet___CPROVER_bool() + ? ptr + : write_set->linked_ptr_pred_ctx->fresh_ptr; // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); @@ -1369,17 +1436,6 @@ __CPROVER_HIDE:; __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; -#ifdef __CPROVER_DFCC_DEBUG_LIB - __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr); -#else - __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); - write_set->linked_allocated->nof_elems = - (write_set->linked_allocated->elems[object_id] != 0) - ? write_set->linked_allocated->nof_elems - : write_set->linked_allocated->nof_elems + 1; - write_set->linked_allocated->elems[object_id] = ptr; - write_set->linked_allocated->is_empty = 0; -#endif return 1; } else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx) @@ -1390,34 +1446,26 @@ __CPROVER_HIDE:; (write_set->assume_ensures_ctx == 0), "only one context flag at a time"); #endif - __CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh; void *ptr = *elem; - // null pointers or already seen pointers are not fresh -#ifdef __CPROVER_DFCC_DEBUG_LIB - // manually inlined below - if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr))) - return 0; -#else - if(ptr == 0) - return 0; - - __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); - - if(seen->elems[object_id] != 0) - return 0; -#endif - -#ifdef __CPROVER_DFCC_DEBUG_LIB - // manually inlined below - __CPROVER_contracts_obj_set_add(seen, ptr); -#else - seen->nof_elems = - (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1; - seen->elems[object_id] = ptr; - seen->is_empty = 0; -#endif - // check size - return __CPROVER_r_ok(ptr, size); + if( + ptr != (void *)0 && + !__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) && + __CPROVER_r_ok(ptr, size)) + { + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != elem, + "__CPROVER_is_fresh does not conflict with other pointer predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? elem + : write_set->linked_ptr_pred_ctx->ptr_pred; + write_set->linked_ptr_pred_ctx->fresh_ptr = + __VERIFIER_nondet___CPROVER_bool() + ? ptr + : write_set->linked_ptr_pred_ctx->fresh_ptr; + return 1; + } + return 0; } else { @@ -1484,13 +1532,37 @@ __CPROVER_HIDE:; __CPROVER_size_t max_offset = ub_offset - lb_offset; __CPROVER_assume(offset <= max_offset); *ptr = (char *)lb + offset; + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != ptr, + "__CPROVER_pointer_in_range_dfcc does not conflict with other pointer " + "predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? ptr + : write_set->linked_ptr_pred_ctx->ptr_pred; return 1; } else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */ { __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr); - return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset && - offset <= ub_offset; + if( + __CPROVER_same_object(lb, *ptr) && lb_offset <= offset && + offset <= ub_offset) + { + __CPROVER_assert( + write_set->linked_ptr_pred_ctx->ptr_pred != ptr, + "__CPROVER_pointer_in_range_dfcc does not conflict with other " + "predicate"); + write_set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() + ? ptr + : write_set->linked_ptr_pred_ctx->ptr_pred; + return 1; + } + else + { + return 0; + } } } @@ -1661,6 +1733,14 @@ __CPROVER_HIDE:; if(__VERIFIER_nondet___CPROVER_bool()) return 0; + __CPROVER_assert( + set->linked_ptr_pred_ctx->ptr_pred != (void **)function_pointer, + "__CPROVER_obeys_contract does not conflict with other pointer " + "predicate"); + set->linked_ptr_pred_ctx->ptr_pred = __VERIFIER_nondet___CPROVER_bool() + ? (void **)function_pointer + : set->linked_ptr_pred_ctx->ptr_pred; + // must hold, assign the function pointer to the contract function *function_pointer = contract; return 1; @@ -1668,7 +1748,18 @@ __CPROVER_HIDE:; else { // in assumption contexts, the pointer gets checked for equality - return *function_pointer == contract; + if(*function_pointer == contract) + { + __CPROVER_assert( + set->linked_ptr_pred_ctx->ptr_pred != (void **)function_pointer, + "__CPROVER_obeys_contract does not conflict with other pointer " + "predicate"); + set->linked_ptr_pred_ctx->ptr_pred = + __VERIFIER_nondet___CPROVER_bool() ? (void **)function_pointer + : set->linked_ptr_pred_ctx->ptr_pred; + return 1; + } + return 0; } } #endif // __CPROVER_contracts_library_defined diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md index f1456324578..6b0b4f225c5 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md @@ -112,8 +112,8 @@ typedef struct __CPROVER_contracts_write_set_t // Set of objects deallocated by the function under analysis (indexed mode) __CPROVER_contracts_obj_set_t deallocated; - // Object set supporting the is_fresh predicate checks (indexed mode) - __CPROVER_contracts_obj_set_ptr_t linked_is_fresh; + // Object set supporting the pointer predicate checks + __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx; // Object set recording the is_fresh allocations in post conditions // (replacement mode only) 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 2c945eb8acd..9ec810a2bda 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 @@ -30,6 +30,8 @@ init_function_symbols(std::unordered_set &function_symbols) function_symbols.insert(CPROVER_PREFIX "assert"); function_symbols.insert(CPROVER_PREFIX "assignable"); function_symbols.insert(CPROVER_PREFIX "assume"); + function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_init"); + function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_reset"); function_symbols.insert(CPROVER_PREFIX "contracts_car_create"); function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains"); function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create"); @@ -42,7 +44,7 @@ init_function_symbols(std::unordered_set &function_symbols) function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh"); function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated"); function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated"); - function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh"); + function_symbols.insert(CPROVER_PREFIX "contracts_link_ptr_pred_ctx"); function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append"); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index efa62681c5f..f9a5f51c2fe 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -52,6 +52,8 @@ const std::map create_dfcc_type_to_name() {dfcc_typet::CAR, CONTRACTS_PREFIX "car_t"}, {dfcc_typet::CAR_SET, CONTRACTS_PREFIX "car_set_t"}, {dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"}, + {dfcc_typet::PTR_PRED_CTX, CONTRACTS_PREFIX "ptr_pred_ctx_t"}, + {dfcc_typet::PTR_PRED_CTX_PTR, CONTRACTS_PREFIX "ptr_pred_ctx_ptr_t"}, {dfcc_typet::OBJ_SET, CONTRACTS_PREFIX "obj_set_t"}, {dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"}, {dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"}, @@ -122,9 +124,11 @@ const std::map create_dfcc_fun_to_name() CONTRACTS_PREFIX "write_set_havoc_object_whole"}, {dfcc_funt::WRITE_SET_HAVOC_SLICE, CONTRACTS_PREFIX "write_set_havoc_slice"}, - {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"}, + {dfcc_funt::LINK_PTR_PRED_CTX, CONTRACTS_PREFIX "link_ptr_pred_ctx"}, {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"}, {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"}, + {dfcc_funt::PTR_PRED_CTX_INIT, CONTRACTS_PREFIX "ptr_pred_ctx_init"}, + {dfcc_funt::PTR_PRED_CTX_RESET, CONTRACTS_PREFIX "ptr_pred_ctx_reset"}, {dfcc_funt::POINTER_EQUALS, CONTRACTS_PREFIX "pointer_equals"}, {dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"}, {dfcc_funt::POINTER_IN_RANGE_DFCC, @@ -810,14 +814,14 @@ const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call( return call; } -const code_function_callt dfcc_libraryt::link_is_fresh_call( +const code_function_callt dfcc_libraryt::link_ptr_pred_ctx_call( const exprt &write_set_ptr, - const exprt &is_fresh_obj_set_ptr, + const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location) { code_function_callt call( - dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(), - {write_set_ptr, is_fresh_obj_set_ptr}); + dfcc_fun_symbol[dfcc_funt::LINK_PTR_PRED_CTX].symbol_expr(), + {write_set_ptr, ptr_pred_ctx_ptr}); call.add_source_location() = source_location; return call; } @@ -882,3 +886,25 @@ const code_function_callt dfcc_libraryt::obj_set_release_call( call.add_source_location() = source_location; return call; } + +const code_function_callt dfcc_libraryt::ptr_pred_ctx_init_call( + const exprt &ptr_pred_ctx_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(), + {ptr_pred_ctx_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::ptr_pred_ctx_reset_call( + const exprt &ptr_pred_ctx_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(), + {ptr_pred_ctx_ptr}); + call.add_source_location() = source_location; + return call; +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index 68e243200b7..d119fc1926b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -31,6 +31,10 @@ enum class dfcc_typet CAR_SET, /// type of pointers to sets of CAR CAR_SET_PTR, + /// type of context info for pointer predicates evaluation + PTR_PRED_CTX, + /// type of pointers to context info for pointer predicates evaluation + PTR_PRED_CTX_PTR, /// type of sets of object identifiers OBJ_SET, /// type of pointers to sets of object identifiers @@ -62,6 +66,10 @@ enum class dfcc_funt OBJ_SET_CREATE_APPEND, /// \see __CPROVER_contracts_obj_set_release OBJ_SET_RELEASE, + /// \see __CPROVER_contracts_ptr_pred_ctx_init + PTR_PRED_CTX_INIT, + /// \see __CPROVER_contracts_ptr_pred_ctx_reset + PTR_PRED_CTX_RESET, /// \see __CPROVER_contracts_obj_set_add OBJ_SET_ADD, /// \see __CPROVER_contracts_obj_set_append @@ -120,8 +128,8 @@ enum class dfcc_funt WRITE_SET_HAVOC_OBJECT_WHOLE, /// \see __CPROVER_contracts_write_set_havoc_slice WRITE_SET_HAVOC_SLICE, - /// \see __CPROVER_contracts_link_is_fresh - LINK_IS_FRESH, + /// \see __CPROVER_contracts_link_ptr_pred_ctx + LINK_PTR_PRED_CTX, /// \see __CPROVER_contracts_link_allocated LINK_ALLOCATED, /// \see __CPROVER_contracts_link_deallocated @@ -155,9 +163,7 @@ class typet; class dfcc_libraryt { public: - dfcc_libraryt( - goto_modelt &goto_model, - message_handlert &lmessage_handler); + dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler); protected: /// True iff the contracts library symbols are loaded @@ -413,10 +419,10 @@ class dfcc_libraryt const source_locationt &source_location); /// \brief Builds call to - /// \ref __CPROVER_contracts_link_is_fresh - const code_function_callt link_is_fresh_call( + /// \ref __CPROVER_contracts_link_ptr_pred_ctx + const code_function_callt link_ptr_pred_ctx_call( const exprt &write_set_ptr, - const exprt &is_fresh_obj_set_ptr, + const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location); /// \brief Builds call to @@ -451,6 +457,18 @@ class dfcc_libraryt const code_function_callt obj_set_release_call( const exprt &obj_set_ptr, const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_ptr_pred_ctx_init + const code_function_callt ptr_pred_ctx_init_call( + const exprt &ptr_pred_ctx_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_ptr_pred_ctx_init + const code_function_callt ptr_pred_ctx_reset_call( + const exprt &ptr_pred_ctx_ptr, + const source_locationt &source_location); }; #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 a625383f182..b1b1e0a43b3 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -115,30 +115,30 @@ static symbol_exprt create_addr_of_ensures_write_set( } /// Generate object set used to support is_fresh predicates -static symbol_exprt create_is_fresh_set( +static symbol_exprt create_ptr_pred_ctx( symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { return dfcc_utilst::create_symbol( symbol_table, - library.dfcc_type[dfcc_typet::OBJ_SET], + library.dfcc_type[dfcc_typet::PTR_PRED_CTX], wrapper_symbol.name, - "__is_fresh_set", + "__ptr_pred_ctx", wrapper_symbol.location); } /// Generate object set pointer used to support is_fresh predicates -static symbol_exprt create_addr_of_is_fresh_set( +static symbol_exprt create_addr_of_ptr_pred_ctx( symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { return dfcc_utilst::create_symbol( symbol_table, - library.dfcc_type[dfcc_typet::OBJ_SET_PTR], + library.dfcc_type[dfcc_typet::PTR_PRED_CTX_PTR], wrapper_symbol.name, - "__address_of_is_fresh_set", + "__address_of_ptr_pred_ctx", wrapper_symbol.location); } @@ -186,9 +186,9 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( goto_model.symbol_table, library, wrapper_symbol)), - is_fresh_set( - create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)), - addr_of_is_fresh_set(create_addr_of_is_fresh_set( + ptr_pred_ctx( + create_ptr_pred_ctx(goto_model.symbol_table, library, wrapper_symbol)), + addr_of_ptr_pred_ctx(create_addr_of_ptr_pred_ctx( goto_model.symbol_table, library, wrapper_symbol)), @@ -226,7 +226,7 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( // encode all contract clauses encode_requires_write_set(); encode_ensures_write_set(); - encode_is_fresh_set(); + encode_ptr_pred_ctx(); encode_requires_clauses(); encode_contract_write_set(); encode_function_call(); @@ -246,7 +246,7 @@ void dfcc_wrapper_programt::add_to_dest(goto_programt &dest) { // add code to dest in the right order dest.destructive_append(preamble); - dest.destructive_append(link_is_fresh); + dest.destructive_append(link_ptr_pred_ctx); dest.destructive_append(preconditions); dest.destructive_append(history); dest.destructive_append(write_set_checks); @@ -500,39 +500,39 @@ void dfcc_wrapper_programt::encode_contract_write_set() goto_programt::make_dead(addr_of_contract_write_set, wrapper_sl)); } -void dfcc_wrapper_programt::encode_is_fresh_set() +void dfcc_wrapper_programt::encode_ptr_pred_ctx() { - preamble.add(goto_programt::make_decl(is_fresh_set, wrapper_sl)); + preamble.add(goto_programt::make_decl(ptr_pred_ctx, wrapper_sl)); - preamble.add(goto_programt::make_decl(addr_of_is_fresh_set, wrapper_sl)); + preamble.add(goto_programt::make_decl(addr_of_ptr_pred_ctx, wrapper_sl)); preamble.add(goto_programt::make_assignment( - addr_of_is_fresh_set, address_of_exprt(is_fresh_set), wrapper_sl)); + addr_of_ptr_pred_ctx, address_of_exprt(ptr_pred_ctx), wrapper_sl)); - // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble + // CALL ptr_pred_ctx_init(ptr_pred_ctx) in preamble preamble.add(goto_programt::make_function_call( - library.obj_set_create_indexed_by_object_id_call( - addr_of_is_fresh_set, wrapper_sl), + library.ptr_pred_ctx_init_call(addr_of_ptr_pred_ctx, wrapper_sl), wrapper_sl)); // link to requires write set - link_is_fresh.add(goto_programt::make_function_call( - library.link_is_fresh_call( - addr_of_requires_write_set, addr_of_is_fresh_set, wrapper_sl), + link_ptr_pred_ctx.add(goto_programt::make_function_call( + library.link_ptr_pred_ctx_call( + addr_of_requires_write_set, addr_of_ptr_pred_ctx, wrapper_sl), wrapper_sl)); // link to ensures write set - link_is_fresh.add(goto_programt::make_function_call( - library.link_is_fresh_call( - addr_of_ensures_write_set, addr_of_is_fresh_set, wrapper_sl), + link_ptr_pred_ctx.add(goto_programt::make_function_call( + library.link_ptr_pred_ctx_call( + addr_of_ensures_write_set, addr_of_ptr_pred_ctx, wrapper_sl), wrapper_sl)); - // release call in postamble - postamble.add(goto_programt::make_function_call( - library.obj_set_release_call(addr_of_is_fresh_set, wrapper_sl), + // reset tracking of target pointers to allow ensures clause to + // post different predicates. + link_deallocated_contract.add(goto_programt::make_function_call( + library.ptr_pred_ctx_reset_call(addr_of_ptr_pred_ctx, wrapper_sl), wrapper_sl)); // DEAD instructions in postamble - postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl)); + postamble.add(goto_programt::make_dead(ptr_pred_ctx, wrapper_sl)); } void dfcc_wrapper_programt::encode_requires_clauses() diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index 224bdf8f795..cd6910507d0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -41,14 +41,15 @@ class conditional_target_group_exprt; /// \details The body of the wrapper is divided into a number of sections /// represented as separate goto_programs: /// - \ref preamble -/// - create is_fresh_set, requires_write_set, ensures_write_set, +/// - create ptr_pred_ctx, requires_write_set, ensures_write_set, /// contract_write_set variables -/// - \ref link_is_fresh -/// - link the is_fresh_set to requires_write_set and ensures_write_set +/// - \ref link_ptr_pred_ctx +/// - link the ptr_pred_ctx to requires_write_set and ensures_write_set /// - in REPLACE mode, link the caller_write_set to the contract_write_set /// so that deallocations and allocations are reflected in the caller /// - \ref preconditions -/// - evaluate preconditions, checking side effects against requires_write_set +/// - evaluate preconditions, while checking the absence of side effects +/// against the empty requires_write_set /// - \ref history /// - declare and snapshot history variables /// - \ref write_set_checks @@ -82,7 +83,8 @@ class conditional_target_group_exprt; /// CALL link_allocated(ensures_write_set, caller_write_set); /// ``` /// - \ref postconditions -/// - evaluate preconditions, checking side effects against ensures_write_set +/// - reset pointer predicate context object, evaluate preconditions while +/// checking absence of side effects against the empty ensures_write_set /// - \ref postamble /// - release all object sets and write set variables /// @@ -159,10 +161,10 @@ class dfcc_wrapper_programt const symbol_exprt addr_of_ensures_write_set; /// Symbol for the object set used to evaluate is_fresh predicates. - const symbol_exprt is_fresh_set; + const symbol_exprt ptr_pred_ctx; /// Symbol for the pointer to the is_fresh object set. - const symbol_exprt addr_of_is_fresh_set; + const symbol_exprt addr_of_ptr_pred_ctx; /// Set of required or ensured contracts for function pointers discovered /// when processing the contract of interest. @@ -187,7 +189,7 @@ class dfcc_wrapper_programt // in the declaration order below. goto_programt preamble; - goto_programt link_is_fresh; + goto_programt link_ptr_pred_ctx; goto_programt preconditions; goto_programt history; goto_programt write_set_checks; @@ -224,11 +226,12 @@ class dfcc_wrapper_programt /// - Adds release function call in \ref postamble void encode_contract_write_set(); - /// Encodes the object set used to evaluate is fresh predicates, - /// - Adds declaration of object set and pointer to set to \ref preamble - /// - Adds initialisation function call in \ref preamble - /// - Adds release function call in \ref postamble - void encode_is_fresh_set(); + /// Encodes the pointer predicates evaluation context object. + /// - Adds declaration of context object and pointer to \ref preamble + /// - Adds init function call in \ref preamble + /// - Adds reset function call in \ref link_deallocated_contract + /// - Adds dead instruction in \ref postamble + void encode_ptr_pred_ctx(); /// Encodes preconditions, instruments them to check for side effects void encode_requires_clauses();