Skip to content

Commit d4757e2

Browse files
tautschnigtautschnig
authored
Merge pull request #8562 from remi-delmas-3000/contracts-allow-is-fresh-to-fail
CONTRACTS: allow pointer predicates to fail in `assume` contexts
2 parents 97c8624 + e965339 commit d4757e2

File tree

52 files changed

+1266
-62
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+1266
-62
lines changed

Diff for: ‎doc/man/cbmc.1

+7
Original file line numberDiff line numberDiff line change
@@ -334,6 +334,13 @@ set malloc failure mode to return null
334334
\fB\-\-string\-abstraction\fR
335335
track C string lengths and zero\-termination
336336
.TP
337+
\fB\-\-dfcc\-debug\-lib\fR
338+
enable debug assertions in the cprover contracts library
339+
.TP
340+
\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
341+
use simplified invalid pointer model in the cprover contracts library
342+
(faster, unsound)
343+
.TP
337344
\fB\-\-reachability\-slice\fR
338345
remove instructions that cannot appear on a trace
339346
from entry point to a property

Diff for: ‎doc/man/goto-analyzer.1

+7
Original file line numberDiff line numberDiff line change
@@ -585,6 +585,13 @@ set malloc failure mode to return null
585585
.TP
586586
\fB\-\-string\-abstraction\fR
587587
track C string lengths and zero\-termination
588+
.TP
589+
\fB\-\-dfcc\-debug\-lib\fR
590+
enable debug assertions in the cprover contracts library
591+
.TP
592+
\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
593+
use simplified invalid pointer model in the cprover contracts library
594+
(faster, unsound)
588595
.SS "Standard Checks"
589596
From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
590597
apply some checks to the program by default (called the "standard checks"), with the

Diff for: ‎doc/man/goto-instrument.1

+7
Original file line numberDiff line numberDiff line change
@@ -706,6 +706,13 @@ do not allow malloc calls to fail by default
706706
\fB\-\-string\-abstraction\fR
707707
track C string lengths and zero\-termination
708708
.TP
709+
\fB\-\-dfcc\-debug\-lib\fR
710+
enable debug assertions in the cprover contracts library
711+
.TP
712+
\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
713+
use simplified invalid pointer model in the cprover contracts library
714+
(faster, unsound)
715+
.TP
709716
\fB\-\-model\-argc\-argv\fR \fIn\fR
710717
Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
711718
set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

Diff for: ‎regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only smt-backend broken-cprover-smt-backend
1+
FUTURE dfcc-only smt-backend broken-cprover-smt-backend
22
main.c
33
--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
44
^EXIT=0$
@@ -7,6 +7,12 @@ main.c
77
--
88
^warning: ignoring
99
--
10+
11+
Marked as FUTURE because:
12+
- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`,
13+
but the CI uses older versions;
14+
- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI.
15+
1016
Tests support for quantifiers in loop contracts with the SMT backend.
1117
When quantified loop invariants are used, they are inserted three times
1218
in the transformed program (base case assertion, step case assumption,

Diff for: ‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c

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

Diff for: ‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: (FAILURE|UNKNOWN)$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (FAILURE|UNKNOWN)
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (FAILURE|UNKNOWN)$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (FAILURE|UNKNOWN)
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (FAILURE|UNKNOWN)
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (FAILURE|UNKNOWN)
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (FAILURE|UNKNOWN)$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
19+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
20+
and no object gets allocated, and pointers remain invalid.

Diff for: ‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <stdlib.h>
2+
void foo(int *x, int *y)
3+
// clang-format off
4+
__CPROVER_requires(
5+
(__CPROVER_is_fresh(x, sizeof(*x)) && y == NULL) ||
6+
(x == NULL && __CPROVER_is_fresh(y, sizeof(*y)))
7+
)
8+
__CPROVER_assigns(y == NULL: *x)
9+
__CPROVER_assigns(x == NULL: *y)
10+
// clang-format on
11+
{
12+
if(y == NULL)
13+
{
14+
assert(0);
15+
*x = 0;
16+
}
17+
else
18+
{
19+
assert(0);
20+
assert(x == NULL);
21+
*y = 0;
22+
}
23+
}
24+
25+
void main()
26+
{
27+
int *x;
28+
int *y;
29+
foo(x, y);
30+
}

Diff for: ‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
5+
^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
6+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
13+
^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
15+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
21+
^EXIT=10$
22+
^SIGNAL=0$
23+
^VERIFICATION FAILED$
24+
--
25+
--
26+
Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
27+
The precondition of `foo` describes a disjunction of cases, either `x` is fresh and `y` is null,
28+
or `x` is null and `y` is fresh. The function `foo` branches on `y == NULL`.
29+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
30+
that both cases of the disjunction expressed in the requires clause are reachable.

Diff for: ‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int *foo()
2+
// clang-format off
3+
__CPROVER_ensures(
4+
__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)) || 1);
5+
// clang-format on
6+
7+
void bar()
8+
{
9+
int *x = foo();
10+
*x = 0; //expected to fail
11+
}
12+
void main()
13+
{
14+
bar();
15+
}

Diff for: ‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
5+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
6+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
7+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
8+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
9+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
16+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
17+
and no object gets allocated, and pointers remain invalid.

Diff for: ‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#include <stdlib.h>
2+
typedef struct
3+
{
4+
int *x;
5+
int *y;
6+
} ret_t;
7+
8+
ret_t foo()
9+
// clang-format off
10+
__CPROVER_ensures((
11+
__CPROVER_is_fresh(__CPROVER_return_value.x, sizeof(int)) &&
12+
__CPROVER_return_value.y == NULL
13+
) || (
14+
__CPROVER_return_value.x == NULL &&
15+
__CPROVER_is_fresh(__CPROVER_return_value.y, sizeof(int))
16+
))
17+
// clang-format on
18+
;
19+
20+
void bar()
21+
{
22+
ret_t ret = foo();
23+
int *x = ret.x;
24+
int *y = ret.y;
25+
if(y == NULL)
26+
{
27+
assert(0);
28+
*x = 0;
29+
}
30+
else
31+
{
32+
assert(0);
33+
assert(x == NULL);
34+
*y = 0;
35+
}
36+
}
37+
38+
void main()
39+
{
40+
bar();
41+
}

Diff for: ‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
5+
^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
6+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
13+
^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
15+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
21+
^EXIT=10$
22+
^SIGNAL=0$
23+
^VERIFICATION FAILED$
24+
--
25+
--
26+
Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
27+
The postcondition of `foo` describes a disjunction of cases: either `x` is fresh and `y` is null,
28+
or `x` is null and `y` is fresh. The function `bar` branches on `y == NULL`.
29+
The test succeeds if the two `assert(0)` are falsifiable, which which shows that
30+
both cases of the disjunction expressed in the ensures clause of `foo` are reachable.

Diff for: ‎regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c

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

Diff for: ‎regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
19+
the program accepts models where `__CPROVER_pointer_equals` evaluates to
20+
false and the target pointer remains invalid.

Diff for: ‎regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdlib.h>
2+
void foo(int *a, int *x, int *y)
3+
// clang-format off
4+
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int)))
5+
__CPROVER_requires(
6+
(__CPROVER_pointer_equals(x,a) && y == NULL) ||
7+
(x == NULL && __CPROVER_pointer_equals(y,a))
8+
)
9+
__CPROVER_assigns(y == NULL: *x)
10+
__CPROVER_assigns(x == NULL: *y)
11+
// clang-format on
12+
{
13+
if(y == NULL)
14+
{
15+
assert(0);
16+
assert(__CPROVER_same_object(a, x));
17+
*x = 0;
18+
}
19+
else
20+
{
21+
assert(0);
22+
assert(x == NULL);
23+
assert(__CPROVER_same_object(a, y));
24+
*y = 0;
25+
}
26+
}
27+
28+
void main()
29+
{
30+
int *a;
31+
int *x;
32+
int *y;
33+
foo(a, x, y);
34+
}

Diff for: ‎regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
5+
^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
14+
^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
16+
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
21+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
23+
^EXIT=10$
24+
^SIGNAL=0$
25+
^VERIFICATION FAILED$
26+
--
27+
--
28+
Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
29+
The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null,
30+
or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`.
31+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
32+
that both cases of the disjunction expressed in the requires clause are reachable.

0 commit comments

Comments
 (0)