Skip to content

Commit 0e93b07

Browse files
author
Remi Delmas
committed
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
1 parent d4757e2 commit 0e93b07

File tree

40 files changed

+763
-168
lines changed

40 files changed

+763
-168
lines changed

‎regression/contracts-dfcc/test_aliasing_ensure/main.c

+7-27
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,15 @@
1-
#include <assert.h>
2-
#include <stdbool.h>
3-
#include <stdlib.h>
4-
5-
int z;
6-
7-
// clang-format off
8-
int foo(int *x, int *y)
9-
__CPROVER_assigns(z, *x)
10-
__CPROVER_requires(
11-
__CPROVER_is_fresh(x, sizeof(int)) &&
12-
*x > 0 &&
13-
*x < 4)
14-
__CPROVER_ensures(
15-
__CPROVER_is_fresh(y, sizeof(int)) &&
16-
!__CPROVER_is_fresh(x, sizeof(int)) &&
17-
x != NULL &&
18-
x != y &&
19-
__CPROVER_return_value == *x + 5)
1+
int *foo()
2+
// clang-format off
3+
__CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)))
204
// clang-format on
215
{
22-
*x = *x + 4;
23-
y = malloc(sizeof(*y));
24-
*y = *x;
25-
z = *y;
26-
return (*x + 5);
6+
int *ret = malloc(sizeof(int));
7+
__CPROVER_assume(ret);
8+
return ret;
279
}
2810

2911
int main()
3012
{
31-
int n = 4;
32-
n = foo(&n, &n);
33-
assert(!(n < 4));
13+
foo();
3414
return 0;
3515
}

‎regression/contracts-dfcc/test_aliasing_ensure/test.desc

-4
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
7-
\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
8-
\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS
9-
\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS
10-
\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS
117
^VERIFICATION SUCCESSFUL$
128
--
139
--

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_pointer_equals(y, x) && __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_pointer_equals(y, x) || __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_equals(y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) ||
7+
__CPROVER_pointer_equals(y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Tests that more than one predicate can be assumed on a same target as long at
10+
they don't hold at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_fail/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.6] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming more than one pointer predicate on the same target pointer triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) ||
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming more than one pointer predicate on the same target pointer triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) || __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_is_fresh(y, sizeof(int)) &&
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1 || *x == 0)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_is_fresh(y, sizeof(int)) ||
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1 || *x == 0)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

0 commit comments

Comments
 (0)