Skip to content

Commit d84e62d

Browse files
qinhepingqinheping
committed
Add goto-level loop-contract annotation
This commit allows us to parse and annotate loop contracts from JSON files to GOTO models. We first parse the JSON file to get the configuration. Function configurations consist of function id (regex) and a list of loop-contract configurations. Loop-contract configurations consist of: Loop number of the loop we are annotating to. Loop invariants as strings. (optional) Loop assigns as strings. (optional) Loop decreases as strings. (optional) A symbol map that map symbol names in the loop contracts strings to their name in the symbol table of the goto model. Loop contracts mangling consists of four steps. Construct a fake function with a fake loop that contains the loop contracts for parsing the contracts. Parse the fake function and extract the contracts as exprt. Substitute symbols in the extracted exprt with the symbols in the symbol table of the goto model according to the symbol map provided by the user. Typecheck all contract exprt. Annotate all contract exprt to the corresponding loop.
1 parent da48fba commit d84e62d

29 files changed

+958
-119
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=10$
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.

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

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

‎regression/contracts-dfcc/loop_contracts_file_fail/test_matching_no_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_no_function.json --dfcc main --apply-loop-contracts
4+
^function .* matches no function
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test checks that loop contracts wrangler correctly error out
10+
when there is no matched function.

‎regression/contracts-dfcc/loop_contracts_file_fail/test_matching_no_function.json

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

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

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
inline int memcmp(const void *s1, const void *s2, unsigned n)
2+
{
3+
int res = 0;
4+
const unsigned char *sc1 = s1, *sc2 = s2;
5+
for(; n != 0; n--)
6+
// clang-format off
7+
__CPROVER_loop_invariant(n <= __CPROVER_loop_entry(n))
8+
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
9+
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
10+
__CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n))
11+
__CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n))
12+
__CPROVER_loop_invariant(res == 0)
13+
__CPROVER_loop_invariant(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
14+
&& sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)
15+
// clang-format on
16+
{
17+
res = (*sc1++) - (*sc2++);
18+
long d1 = sc1 - (const unsigned char *)s1;
19+
long d2 = sc2 - (const unsigned char *)s2;
20+
if(res != 0)
21+
return res;
22+
}
23+
return res;
24+
}
25+
26+
int main()
27+
{
28+
unsigned SIZE;
29+
__CPROVER_assume(1 < SIZE && SIZE < 65536);
30+
unsigned char *a = malloc(SIZE);
31+
unsigned char *b = malloc(SIZE);
32+
memcpy(b, a, SIZE);
33+
assert(memcmp(a, b, SIZE) == 0);
34+
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE gcc-only
2+
main.c
3+
--dfcc main --apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
This test checks that loop contracts work correctly on memcmp.

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"functions": [
3+
{
4+
"memcmp": [
5+
{
6+
"loop_id": "0",
7+
"invariants": "(n <= __CPROVER_loop_entry(n))&&(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))&&
8+
(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))&&
9+
(sc1 <= s1 + __CPROVER_loop_entry(n))&&
10+
(sc2 <= s2 + __CPROVER_loop_entry(n))&&
11+
(res == 0)&&
12+
(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
13+
&& sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)",
14+
"symbol_map": "n,memcmp::n; sc1,memcmp::1::sc1; sc2,memcmp::1::sc2; res,memcmp::1::res; s1, memcmp::s1; s2, memcmp::s2"
15+
}
16+
]
17+
}
18+
]
19+
}

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE gcc-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+
--
9+
This test checks that loop contracts work correctly on memcmp.
10+
Using loop contracts from the contracts file.

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

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

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE dfcc-only
2+
main.c
3+
--loop-contracts-file test.json --dfcc main --apply-loop-contracts
4+
^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$
5+
^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
6+
^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
7+
^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
8+
^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
9+
^\[main.assigns.\d+\] line \d+ Check that x is assignable: SUCCESS$
10+
^VERIFICATION SUCCESSFUL$
11+
^EXIT=0$
12+
^SIGNAL=0$
13+
--
14+
--
15+
This test checks that decreases clause is properly initialized
16+
when the loop head and loop invariant compilation emit several goto instructions.
17+
Using loop contracts from the contracts file.

‎src/ansi-c/c_typecheck_base.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,7 @@ class c_typecheck_baset:
6565

6666
virtual void typecheck()=0;
6767
virtual void typecheck_expr(exprt &expr);
68+
virtual void typecheck_spec_assigns(exprt::operandst &targets);
6869

6970
protected:
7071
symbol_table_baset &symbol_table;
@@ -160,7 +161,6 @@ class c_typecheck_baset:
160161
/// is found in expr.
161162
virtual void check_was_freed(const exprt &expr, std::string &clause_type);
162163

163-
virtual void typecheck_spec_assigns(exprt::operandst &targets);
164164
virtual void typecheck_spec_frees(exprt::operandst &targets);
165165
virtual void typecheck_conditional_targets(
166166
exprt::operandst &targets,

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ SRC = accelerate/accelerate.cpp \
1717
branch.cpp \
1818
call_sequences.cpp \
1919
contracts/contracts.cpp \
20+
contracts/contracts_wrangler.cpp \
2021
contracts/dynamic-frames/dfcc_utils.cpp \
2122
contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
2223
contracts/dynamic-frames/dfcc_contract_mode.cpp \

‎src/goto-instrument/contracts/contracts.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,11 @@ Date: February 2016
4040
" --loop-contracts-no-unwind\n" \
4141
" do not unwind transformed loops\n"
4242

43+
#define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
44+
#define HELP_LOOP_CONTRACTS_FILE \
45+
" --loop-contracts-file <file>\n" \
46+
" parse and annotate loop contracts from files\n"
47+
4348
#define FLAG_REPLACE_CALL "replace-call-with-contract"
4449
#define HELP_REPLACE_CALL \
4550
" --replace-call-with-contract <function>[/contract]\n" \

0 commit comments

Comments
 (0)