Skip to content

Commit 3410558

Browse files
remi-delmas-3000remi-delmas-3000
authored
Merge pull request #6679 from remi-delmas-3000/contract-detect-local-statics
CONTRACTS: new method to detect static locals for contract instrumentation
2 parents d971ad8 + 7f5300e commit 3410558

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)