Skip to content

Commit 7f5300e

Browse files
author
Remi Delmas
committed
CONTRACTS: new method to detect static locals for contract instrumentation
The previous method relied on building a call graph and could not be used on functions that had already been through an inlining pass. This new method uses source_locations and manages scoping by tracking the min and max source_locations for functions that are encountered when traversing instructions. Then, when collecting statics from the symbol table, we only keep the ones that are found in the traversed functions and whose source_location is within the seen intervals. The method makes the sound pessimistic choice to widen the tracked intervals and collect variables whenever the encountered source_locations are undefined or only partially defined. When replace-call-with-contract is used, extra pragmas are used to track static locals and make sure they are propagated to the write set of the function in which the call is replaced.
1 parent 79c1637 commit 7f5300e

File tree

13 files changed

+716
-91
lines changed

13 files changed

+716
-91
lines changed

‎regression/contracts/assigns_enforce_19/main.c‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@ static int c = 0;
66
int f() __CPROVER_assigns()
77
{
88
static int a = 0;
9+
static int aa = 0;
910
a++;
11+
aa++;
1012
return a;
1113
}
1214

‎regression/contracts/assigns_enforce_19/test.desc‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,21 @@
11
CORE
22
main.c
33
--enforce-contract f --enforce-contract g
4-
^\[f.assigns.\d+\] line 9 Check that a is assignable: SUCCESS$
5-
^\[g.assigns.\d+\] line 14 Check that b is valid: SUCCESS$
6-
^\[g.assigns.\d+\] line 16 Check that b is assignable: SUCCESS$
7-
^\[g.assigns.\d+\] line 17 Check that c is assignable: FAILURE$
8-
^\[g.assigns.\d+\] line 18 Check that \*points_to_b is assignable: SUCCESS$
9-
^\[g.assigns.\d+\] line 19 Check that \*points_to_c is assignable: FAILURE$
4+
^\[f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$
5+
^\[f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$
6+
^\[g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$
7+
^\[g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
8+
^\[g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
9+
^\[g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
10+
^\[g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
1011
^VERIFICATION FAILED$
1112
^EXIT=10$
1213
^SIGNAL=0$
1314
--
1415
--
1516
Checks whether contract enforcement works with (local and global) static variables.
1617
Local static variables should be part of the local write set.
18+
Shows that we detect using the source location even when there is space
19+
before the declaration and the actual start of the program.
1720
Global static variables should be included in the global write set,
1821
otherwise any assignment to it is invalid.

‎regression/contracts/assigns_enforce_detect_replaced_local_statics/main.c‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
#include <stdlib.h>
4+
5+
int baz() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
6+
{
7+
static int __local_static = 0;
8+
__local_static = 0;
9+
10+
return __local_static;
11+
}
12+
13+
int bar() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
14+
{
15+
static int __local_static_arr[2];
16+
__local_static_arr[0] = 0;
17+
__local_static_arr[1] = 0;
18+
19+
baz();
20+
return __local_static_arr[0] | __local_static_arr[1];
21+
}
22+
23+
void foo() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
24+
{
25+
bar();
26+
}
27+
28+
int main()
29+
{
30+
foo();
31+
__CPROVER_assert(baz() == 0, "expecting FAILURE");
32+
__CPROVER_assert(bar() == 0, "expecting FAILURE");
33+
}

‎regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
CORE
2+
main.c
3+
--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --pointer-check
4+
^\[foo.assigns.\d+\] line \d+ Check that __local_static \(assigned by the contract of bar\) is assignable: SUCCESS$
5+
^\[foo.assigns.\d+\] line \d+ Check that __local_static_arr \(assigned by the contract of bar\) is assignable: SUCCESS$
6+
^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$
7+
^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$
8+
^VERIFICATION FAILED$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
--
13+
This test checks that locally declared static variables are correctly detected
14+
and tracked when function contract replacement is used.
15+
Here, baz declares a local static variable,
16+
bar calls baz, and we replace the call to baz in bar.
17+
bar also declares a local static array variable.
18+
the call to bar is replaced by its contract in foo.
19+
We see that in foo, two assignments to these local statics are checked,
20+
showing that the replacement of bar in foo is modeled as nondet assignments.
21+
We also see that these assignments are succesfully checked against the empty
22+
assigns clause of foo, which shows that they are automatically propagated to
23+
the assigns clause of foo as expected.

‎regression/contracts/loop_assigns_scoped_local_statics/main.c‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
#include <assert.h>
2+
3+
int j;
4+
5+
int before_loop()
6+
{
7+
static int __static_local;
8+
__static_local = 0;
9+
return __static_local;
10+
}
11+
12+
int after_loop()
13+
{
14+
static int __static_local;
15+
__static_local = 0;
16+
return __static_local;
17+
}
18+
19+
int lowerbound()
20+
{
21+
static int __static_local;
22+
__static_local = 0;
23+
return 0;
24+
}
25+
26+
int upperbound()
27+
{
28+
static int __static_local;
29+
__static_local = 0;
30+
return 10;
31+
}
32+
33+
void incr(int *i)
34+
{
35+
static int __static_local;
36+
__static_local = 0;
37+
(*i)++;
38+
}
39+
40+
int body_1(int i)
41+
{
42+
static int __static_local;
43+
__static_local = 0;
44+
j = i;
45+
return __static_local;
46+
}
47+
48+
int body_2(int *i)
49+
{
50+
static int __static_local;
51+
__static_local = 0;
52+
(*i)++;
53+
(*i)--;
54+
return __static_local;
55+
}
56+
57+
int body_3(int *i)
58+
{
59+
static int __static_local;
60+
__static_local = 0;
61+
(*i)++;
62+
if(*i == 4)
63+
return 1;
64+
65+
(*i)--;
66+
return 0;
67+
}
68+
69+
int main()
70+
{
71+
assert(before_loop() == 0);
72+
73+
for(int i = lowerbound(); i < upperbound(); incr(&i))
74+
// clang-format off
75+
__CPROVER_assigns(i, j)
76+
__CPROVER_loop_invariant(0 <= i && i <= 10)
77+
__CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
78+
// clang-format on
79+
{
80+
body_1(i);
81+
82+
if(body_3(&i))
83+
return 1;
84+
85+
body_2(&i);
86+
}
87+
88+
assert(j == 9);
89+
assert(before_loop() == 0);
90+
assert(after_loop() == 0);
91+
}

‎regression/contracts/loop_assigns_scoped_local_statics/test.desc‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
7+
^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
8+
^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
9+
^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
10+
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
11+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
12+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
13+
^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
14+
^\[body_1.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
15+
^\[body_2.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
16+
^\[body_3.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
17+
^\[incr.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
18+
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
19+
^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
20+
^\[upperbound.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
21+
^VERIFICATION SUCCESSFUL$
22+
--
23+
--
24+
This test checks assigns clause checking presence of locally declared static
25+
variables.
26+
We observe that the local static variables declared within the loop's
27+
scope are correctly gathered and added to the write set,
28+
and are havoced (body_1 and body_2 do not return 0 anymore after the loop).

‎regression/contracts/loop_assigns_scoped_local_statics_propagate/main.c‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
4+
int j;
5+
6+
int before_loop()
7+
{
8+
static int __static_local;
9+
__static_local = 0;
10+
return __static_local;
11+
}
12+
13+
int after_loop()
14+
{
15+
static int __static_local;
16+
__static_local = 0;
17+
return __static_local;
18+
}
19+
20+
int bar(int i) __CPROVER_requires(true) __CPROVER_ensures(j == i)
21+
__CPROVER_assigns(j)
22+
{
23+
static int __static_local;
24+
__static_local = 0;
25+
j = i;
26+
return __static_local;
27+
}
28+
29+
int main()
30+
{
31+
assert(before_loop() == 0);
32+
33+
for(int i = 0; i < 10; i++)
34+
// clang-format off
35+
__CPROVER_assigns(i, j)
36+
__CPROVER_loop_invariant(0 <= i && i <= 10)
37+
__CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
38+
// clang-format on
39+
{
40+
bar(i);
41+
}
42+
43+
assert(j == 9);
44+
assert(before_loop() == 0);
45+
assert(after_loop() == 0);
46+
}

‎regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
CORE
2+
main.c
3+
--replace-call-with-contract bar --apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assigns.\d+\] line \d+ Check that j \(assigned by the contract of bar\) is assignable: SUCCESS$
7+
^\[main.assigns.\d+\] line \d+ Check that __static_local \(assigned by the contract of bar\) is assignable: SUCCESS$
8+
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
9+
^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
10+
^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
11+
^\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$
12+
^\[main.assigns.\d+\] line \d+ Check that i is valid: SUCCESS$
13+
^\[main.assigns.\d+\] line \d+ Check that j is valid: SUCCESS$
14+
^\[main.assertion.\d+\] line \d+ assertion j == 9: SUCCESS$
15+
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
16+
^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
17+
^VERIFICATION SUCCESSFUL$
18+
--
19+
--
20+
This test checks assigns clause checking presence of locally declared static
21+
variables and loops.
22+
We observe that the local static variables declared within the loop's
23+
scope are correctly gathered and added to the write set,
24+
and are havoced (body_1 and body_2 do not return 0 anymore after the loop).

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

Lines changed: 15 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -257,11 +257,8 @@ void code_contractst::check_apply_loop_contracts(
257257
// assigns clause snapshots
258258
goto_programt snapshot_instructions;
259259

260-
instrument_spec_assigns.track_static_locals(snapshot_instructions);
261-
262-
// ^^^ FIXME ^^^ we should only allow assignments to static locals
263-
// declared in functions that are called in the loop body, not from the whole
264-
// function...
260+
instrument_spec_assigns.track_static_locals_between(
261+
loop_head, loop_end, snapshot_instructions);
265262

266263
// set of targets to havoc
267264
assignst to_havoc;
@@ -799,25 +796,22 @@ bool code_contractst::apply_function_contract(
799796
targets.add_to_operands(std::move(target));
800797
common_replace(targets);
801798

802-
// Create a sequence of non-deterministic assignments...
799+
// Create a sequence of non-deterministic assignments ...
800+
801+
// ... for the assigns clause targets and static locals
803802
goto_programt havoc_instructions;
804803

805-
// ...for assigns clause targets
806-
if(!assigns_clause.empty())
807-
{
808-
// Havoc all targets in the assigns clause
809-
// TODO: handle local statics possibly touched by this function
810-
havoc_assigns_clause_targetst havocker(
811-
target_function,
812-
targets.operands(),
813-
goto_functions,
814-
location,
815-
symbol_table,
816-
log.get_message_handler());
817-
havocker.get_instructions(havoc_instructions);
818-
}
804+
havoc_assigns_clause_targetst havocker(
805+
target_function,
806+
targets.operands(),
807+
goto_functions,
808+
location,
809+
symbol_table,
810+
log.get_message_handler());
811+
812+
havocker.get_instructions(havoc_instructions);
819813

820-
// ...for the return value
814+
// ... for the return value
821815
if(call_ret_opt.has_value())
822816
{
823817
auto &call_ret = call_ret_opt.value();

0 commit comments

Comments
 (0)