Skip to content

Commit 49a75bf

Browse files
SaswatPadhiSaswatPadhi
committed
instrument loops per given assigns clauses
1 parent e0da7e7 commit 49a75bf

File tree

23 files changed

+403
-101
lines changed

23 files changed

+403
-101
lines changed

‎regression/contracts/assigns_enforce_arrays_05/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract assigns_ptr --enforce-contract assigns_range
3+
--enforce-contract assigns_range
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎regression/contracts/invar_assigns_alias_analysis/test.desc

Lines changed: 0 additions & 14 deletions
This file was deleted.

‎regression/contracts/invar_assigns_empty/main.c

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,8 @@
22

33
int main()
44
{
5-
int r;
6-
__CPROVER_assume(r >= 0);
7-
while(r > 0)
8-
__CPROVER_assigns() __CPROVER_loop_invariant(r >= 0)
5+
while(1 == 1)
6+
__CPROVER_assigns() __CPROVER_loop_invariant(1 == 1)
97
{
10-
r--;
118
}
12-
assert(r == 0);
13-
14-
return 0;
159
}

‎regression/contracts/invar_assigns_empty/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ main.c
55
^SIGNAL=0$
66
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
77
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
98
^VERIFICATION SUCCESSFUL$
109
--
1110
--

‎regression/contracts/invar_assigns_opt/test.desc

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,16 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
9-
^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$
10-
^\[main.4\] .* Check loop invariant before entry: SUCCESS$
11-
^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
12-
^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
13-
^\[main.assertion.2\] .* assertion r2 == 0: SUCCESS$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
9+
^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
10+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
11+
^\[main.\d+\] .* Check that s2 is assignable: SUCCESS$
12+
^\[main.\d+\] .* Check that r2 is assignable: SUCCESS$
13+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
14+
^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
15+
^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
1416
^VERIFICATION SUCCESSFUL$
1517
--
1618
--

‎regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,4 +18,9 @@ to pass -- we should not mistakenly havoc the allocations, just their values.
1818
However, the `data[1][2][3] == 0` assertion is expected to fail since `data`
1919
is havoced.
2020

21-
Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
21+
Blocked on #6326:
22+
The assigns clause in this case would have an entire 3D space,
23+
and some of it must be re-established, to the original objects
24+
but with different values at certain locations, by the loop invariant.
25+
However, currently we cannot restrict same_object for pointers
26+
within loop invariants.

‎regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,10 @@ void main()
1717
data[4][5][6] = 0;
1818

1919
for(unsigned i = 0; i < SIZE; i++)
20+
// clang-format off
21+
__CPROVER_assigns(i, data[4][5][6])
2022
__CPROVER_loop_invariant(i <= SIZE)
23+
// clang-format on
2124
{
2225
data[4][5][6] = 1;
2326
}

‎regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.\d+\] .* Check that i is assignable: SUCCESS$
8+
^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$
9+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
10+
^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
11+
^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
1012
^VERIFICATION FAILED$
1113
--
1214
--
@@ -17,5 +19,3 @@ The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]`
1719
is havoced and the invariant does not reestablish its value.
1820
However, the `data[1][2][3] == 0` assertion is expected to pass -- we should
1921
not havoc the entire `data` array, if only a constant index if being modified.
20-
21-
Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.

‎regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,9 @@ We _could_ do a more precise analysis in future where we only havoc
1919
`data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be
2020
modified in the given loop.
2121

22-
Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
22+
Blocked on #6326:
23+
The assigns clause in this case would have an entire 2D grid,
24+
and some of it must be re-established, to the original objects
25+
but with different values at certain locations, by the loop invariant.
26+
However, currently we cannot restrict same_object for pointers
27+
within loop invariants.

‎regression/contracts/loop_assigns-01/main.c

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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+
struct blob *b = malloc(sizeof(struct blob));
14+
b->data = malloc(SIZE);
15+
16+
b->data[5] = 0;
17+
for(unsigned i = 0; i < SIZE; i++)
18+
// clang-format off
19+
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data))
20+
__CPROVER_loop_invariant(i <= SIZE)
21+
// clang-format on
22+
{
23+
b->data[i] = 1;
24+
}
25+
26+
assert(b->data[5] == 0);
27+
}

‎regression/contracts/loop_assigns-01/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.\d+\] .* Check that i is assignable: SUCCESS$
8+
^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
9+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
10+
^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
11+
^VERIFICATION FAILED$
12+
--
13+
--
14+
This test (taken from #6021) shows the need for assigns clauses on loops.
15+
The alias analysis in this case returns `unknown`,
16+
and so we must manually annotate an assigns clause on the loop.

‎regression/contracts/loop_assigns-02/main.c

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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+
struct blob *b = malloc(sizeof(struct blob));
14+
b->data = malloc(SIZE);
15+
16+
b->data[5] = 0;
17+
for(unsigned i = 0; i < SIZE; i++)
18+
// clang-format off
19+
__CPROVER_assigns(i, b->data[i])
20+
__CPROVER_loop_invariant(i <= SIZE)
21+
// clang-format on
22+
{
23+
b->data[i] = 1;
24+
}
25+
26+
assert(b->data[5] == 0);
27+
}

‎regression/contracts/loop_assigns-02/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.\d+\] .* Check that i is assignable: SUCCESS$
8+
^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
9+
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
10+
^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
11+
^VERIFICATION FAILED$
12+
--
13+
--
14+
This test (taken from #6021) shows the need for assigns clauses on loops.
15+
The alias analysis in this case returns `unknown`,
16+
and so we must manually annotate an assigns clause on the loop.
17+
18+
Note that the annotated assigns clause in this case is an underapproximation,
19+
per the current semantics of the assigns clause -- it must model ALL memory
20+
being assigned to by the loop, not just a single symbolic iteration.

‎regression/contracts/loop_assigns-03/main.c

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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+
struct blob *b = malloc(sizeof(struct blob));
14+
b->data = malloc(SIZE);
15+
16+
b->data[5] = 0;
17+
for(unsigned i = 0; i < SIZE; i++)
18+
// clang-format off
19+
__CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->data))
20+
__CPROVER_loop_invariant(i <= SIZE)
21+
// clang-format on
22+
{
23+
b->data[i] = 1;
24+
}
25+
26+
assert(b->data[5] == 0);
27+
}

‎regression/contracts/loop_assigns-03/test.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.\d+\] .* Check that i is assignable: FAILURE$
8+
^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
9+
^VERIFICATION FAILED$
10+
--
11+
--
12+
This test (taken from #6021) shows the need for assigns clauses on loops.
13+
The alias analysis in this case returns `unknown`,
14+
and so we must manually annotate an assigns clause on the loop.
15+
16+
Note that the annotated assigns clause in this case is an underapproximation,
17+
because `i` is also assigned in the loop and should be marked as assignable.

‎regression/contracts/loop_assigns-04/main.c

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
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+
int y;
14+
struct blob *b = malloc(sizeof(struct blob));
15+
b->data = malloc(SIZE);
16+
17+
b->data[5] = 0;
18+
for(unsigned i = 0; i < SIZE; i++)
19+
// clang-format off
20+
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data))
21+
__CPROVER_loop_invariant(i <= SIZE)
22+
// clang-format on
23+
{
24+
b->data[i] = 1;
25+
26+
int x;
27+
for(unsigned j = 0; j < i; j++)
28+
// clang-format off
29+
// y is not assignable by outer loop, so this should be flagged
30+
__CPROVER_assigns(j, y, x, b->data[i])
31+
__CPROVER_loop_invariant(j <= i)
32+
// clang-format on
33+
{
34+
x = b->data[j] * b->data[j];
35+
b->data[i] += x;
36+
y += j;
37+
}
38+
}
39+
40+
assert(b->data[5] == 0);
41+
}

‎regression/contracts/loop_assigns-04/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.\d+\] .* Check that i is assignable: SUCCESS$
7+
^\[main.\d+\] .* Check that j is assignable: SUCCESS$
8+
^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
9+
^\[main.\d+\] .* Check that y is assignable: FAILURE$
10+
^VERIFICATION FAILED$
11+
--
12+
--
13+
This test (taken from #6021) shows the need for assigns clauses on loops.
14+
The alias analysis in this case returns `unknown`,
15+
and so we must manually annotate an assigns clause on the loop.
16+
17+
Note that the annotated assigns clause in this case is an underapproximation,
18+
because `i` is also assigned in the loop and should be marked as assignable.

‎regression/contracts/invar_assigns_alias_analysis/main.c renamed to ‎regression/contracts/loop_assigns-fail/main.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ void main()
1616
b->data[5] = 0;
1717
for(unsigned i = 0; i < SIZE; i++)
1818
// clang-format off
19-
__CPROVER_assigns(b->data)
2019
__CPROVER_loop_invariant(i <= SIZE)
2120
// clang-format on
2221
{

‎regression/contracts/loop_assigns-fail/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
activate-multi-line-match
5+
Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN!
6+
^EXIT=6$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This test (taken from #6021) shows the need for assigns clauses on loops.
11+
The alias analysis in this case returns `unknown`.

‎regression/contracts/variant_missing_invariant_warning/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
CORE
22
main.c
33
--apply-loop-contracts
4-
^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$
4+
activate-multi-line-match
5+
^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$
56
^\[main.1\].*Check loop invariant before entry: SUCCESS$
67
^\[main.2\].*Check that loop invariant is preserved: SUCCESS$
78
^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$

0 commit comments

Comments
 (0)