Skip to content

Commit e9b20d8

Browse files
author
Remi Delmas
committed
CONTRACTS: optimize is_fresh separation checks, add ptr predicate uniqueness checks
- Replaces a bool array indexed by object ID by a nondet demonic variable to track the set of fresh objects and implement separation checks. - Ensures requires or ensures clause assume/assert at most one predicate per pointer by tracking locations where these pointers are stored and adding separation checks on them as well. This is necessary to catch occurences like `__CPROVER_is_fresh(p, size) && __CPROVER_is_fresh(p, size)` in assume contexts. - Adds a new type `__CPROVER_contracts_ptr_pred_ctx_t` in `cprover_contracts.c` to store all contextual information needed to evaluate all pointer predicates. - 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 3d79560 commit e9b20d8

File tree

40 files changed

+766
-185
lines changed

40 files changed

+766
-185
lines changed

Diff for: ‎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
}

Diff for: ‎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
--

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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_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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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.

Diff for: ‎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+
}

Diff for: ‎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)