Skip to content

Commit ba0c1bb

Browse files
qinhepingqinheping
authored
Merge pull request #7788 from qinheping/features/goto-level-loop-contracts
CONTRACTS: Add goto-level loop-contract annotation
2 parents 4b95215 + b543536 commit ba0c1bb

29 files changed

+834
-3
lines changed

‎doc/man/goto-instrument.1

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1010,6 +1010,9 @@ check and use loop contracts when provided
10101010
\fB\-loop\-contracts\-no\-unwind\fR
10111011
do not unwind transformed loops
10121012
.TP
1013+
\fB\-loop\-contracts\-file\fR \fIfile\fR
1014+
annotate loop contracts from the file to the goto program
1015+
.TP
10131016
\fB\-\-replace\-call\-with\-contract\fR \fIfun\fR
10141017
replace calls to \fIfun\fR with \fIfun\fR's contract
10151018
.TP

‎regression/contracts-dfcc/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,12 @@ endif()
1414

1515

1616
add_test_pl_tests(
17-
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true"
17+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true" ${gcc_only}
1818
)
1919

2020
add_test_pl_profile(
2121
"contracts-non-dfcc"
22-
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} false"
22+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} false" ${gcc_only}
2323
"-C;-X;dfcc-only;-s;non-dfcc"
2424
"CORE"
2525
)

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.json

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"functions": [
3+
{
4+
"foo": [
5+
{
6+
"loop_id": "0",
7+
"assigns": "i",
8+
"invariants": "0 <= i && i <= 10",
9+
"decreases": "i",
10+
"symbol_map": "i,foo::1::1::i"
11+
}
12+
]
13+
}
14+
]
15+
}

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test_contracts_file.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--loop-contracts-file test.json --dfcc main --apply-loop-contracts
4+
^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: FAILURE$
6+
^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
^VERIFICATION FAILED$
10+
--
11+
--
12+
This test checks that program variables with special name prefixes
13+
__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking.
14+
Using loop contracts from the contracts file.

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.json

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
{
2+
"functions": [
3+
{
4+
"foo": [
5+
{
6+
"loop_id": "0",
7+
"assigns": "i,nondet_var, __VERIFIER_var, __CPROVER_var",
8+
"invariants": "0 <= i && i <= 10",
9+
"decreases": "i",
10+
"symbol_map": "i,foo::1::1::i;
11+
nondet_var,foo::1::nondet_var;
12+
__VERIFIER_var, foo::1::__VERIFIER_var;
13+
__CPROVER_var,foo::1::__CPROVER_var"
14+
}
15+
]
16+
}
17+
]
18+
}

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test_contracts_file.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--loop-contracts-file test.json --dfcc main --apply-loop-contracts
4+
^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: SUCCESS$
5+
^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: SUCCESS$
6+
^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: SUCCESS$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
^VERIFICATION SUCCESSFUL$
10+
--
11+
--
12+
This test checks that when program variables names have special prefixes
13+
__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them
14+
assignable.
15+
Using loop contracts from the contracts file.

‎regression/contracts-dfcc/history-index/test.json

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
"functions": [
3+
{
4+
"main": [
5+
{
6+
"loop_id": "0",
7+
"invariants": "x[0] == __CPROVER_loop_entry(x[0])",
8+
"symbol_map": "x,main::1::x"
9+
}
10+
]
11+
}
12+
]
13+
}

‎regression/contracts-dfcc/history-index/test_contracts_file.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--loop-contracts-file test.json --dfcc main --apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^Tracking history of index expressions is not supported yet\.
9+
--
10+
This test checks that `ID_index` expressions are allowed within history variables.
11+
Using loop contracts from the contracts file.

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

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
#define SIZE 8
5+
6+
struct blob
7+
{
8+
char *data;
9+
};
10+
11+
void main()
12+
{
13+
foo();
14+
}
15+
16+
void foo()
17+
{
18+
struct blob *b = malloc(sizeof(struct blob));
19+
b->data = malloc(SIZE);
20+
21+
b->data[5] = 0;
22+
for(unsigned i = 0; i < SIZE; i++)
23+
// clang-format off
24+
// clang-format on
25+
{
26+
b->data[i] = 1;
27+
}
28+
}
29+
30+
void foo1()
31+
{
32+
struct blob *b = malloc(sizeof(struct blob));
33+
b->data = malloc(SIZE);
34+
35+
b->data[5] = 0;
36+
for(unsigned i = 0; i < SIZE; i++)
37+
// clang-format off
38+
// clang-format on
39+
{
40+
b->data[i] = 1;
41+
}
42+
}

‎regression/contracts-dfcc/loop_contracts_file_fail/test_matching_more_than_one_function.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--loop-contracts-file test_matching_more_than_one_function.json --dfcc main --apply-loop-contracts
4+
^function regex .* matches more than one function
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test checks that loop contracts wrangler correctly error out
10+
when there is more than one matched function.

0 commit comments

Comments
 (0)