Skip to content

Commit 56e0b20

Browse files
SaswatPadhiSaswatPadhi
committed
Cleanup regression tests for quantified contracts
1 parent 78a08ce commit 56e0b20

File tree

38 files changed

+436
-219
lines changed

38 files changed

+436
-219
lines changed

‎regression/contracts/quantifiers-exists-both-01/main.c

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
// clang-format off
2-
int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
3-
int i;
4-
(0 <= i && i < 8) ==> arr[i] == 0
5-
}) __CPROVER_ensures(__CPROVER_exists {
6-
int i;
7-
(0 <= i && i < 8) ==> arr[i] == 0
8-
})
2+
int f1(int *arr)
3+
__CPROVER_requires(__CPROVER_exists {
4+
int i;
5+
(0 <= i && i < 8) && arr[i] == 0
6+
})
7+
__CPROVER_ensures(__CPROVER_exists {
8+
int i;
9+
(0 <= i && i < 8) && arr[i] == 0
10+
})
911
// clang-format on
1012
{
1113
return 0;

‎regression/contracts/quantifiers-exists-both-01/test.desc

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,14 @@ main.c
33
--enforce-all-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[1\] assertion: SUCCESS$
67
^VERIFICATION SUCCESSFUL$
78
--
9+
^warning: ignoring
810
--
9-
The purpose of this test is to ensure that we can safely use __CPROVER_exists
10-
in a negative context (which is currently not always the case). By using the
11-
--enforce-all-contracts flag, this test assumes the statement in
12-
__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
13-
thus, verification should be successful.
11+
The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
12+
positive and negative contexts (ENSURES and REQUIRES clauses).
13+
14+
With the SAT backend existential quantifiers in a positive context,
15+
e.g., the ENSURES clause being enforced in this case,
16+
are supported only if the quantifier is bound to a constant range.

‎regression/contracts/quantifiers-exists-both-02/main.c

Lines changed: 32 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,42 @@
1+
#include <stdlib.h>
2+
3+
#define MAX_LEN 8
4+
15
// clang-format off
2-
int f1(int *arr, int *len) __CPROVER_requires(__CPROVER_exists {
3-
int i;
4-
(0 <= i && i < len) ==> arr[i] == 0
5-
}) __CPROVER_ensures(__CPROVER_exists {
6-
int i;
7-
(0 <= i && i < len) ==> arr[i] == 0
8-
})
6+
int f1(int *arr, int len)
7+
__CPROVER_requires(
8+
len > 0 ==> __CPROVER_exists {
9+
int i;
10+
// constant bounds for explicit unrolling with SAT backend
11+
(0 <= i && i < MAX_LEN) && (
12+
// actual symbolic bound for `i`
13+
i < len && arr[i] == 0
14+
)
15+
}
16+
)
17+
__CPROVER_ensures(
18+
len > 0 ==> __CPROVER_exists {
19+
int i;
20+
// constant bounds for explicit unrolling with SAT backend
21+
(0 <= i && i < MAX_LEN) && (
22+
// actual symbolic bound for `i`
23+
i < len && arr[i] == 0
24+
)
25+
}
26+
)
927
// clang-format on
1028
{
1129
return 0;
1230
}
1331

1432
int main()
1533
{
16-
int len, arr[8];
34+
int len;
35+
__CPROVER_assume(0 <= len && len <= MAX_LEN);
36+
37+
int *arr = malloc(len);
38+
if(len > 0)
39+
arr[0] = 0;
40+
1741
f1(arr, len);
1842
}

‎regression/contracts/quantifiers-exists-both-02/test.desc

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,16 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--enforce-all-contracts
3+
--replace-all-calls-with-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[1\] assertion: SUCCESS$
67
^VERIFICATION SUCCESSFUL$
78
--
9+
^warning: ignoring
810
--
9-
The purpose of this test is to ensure that we can safely use __CPROVER_exists
10-
in a negative context (which is currently not always the case). By using the
11-
--enforce-all-contracts flag, this test assumes the statement in
12-
__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
13-
thus, verification should be successful.
11+
The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
12+
positive and negative contexts (ENSURES and REQUIRES clauses).
1413

15-
Known bug:
16-
The current implementation cannot handle a structure such as
17-
__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is
18-
not explicitly bounded to a predefined range (i.e. if at least
19-
one of its bound is only declared and not defined).
14+
With the SAT backend existential quantifiers in a positive context,
15+
e.g., the REQUIRES clause being replaced in this case,
16+
are supported only if the quantifier is bound to a constant range.

‎regression/contracts/quantifiers-exists-ensures-01/main.c

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ int f1(int *arr)
33
__CPROVER_assigns(*arr)
44
__CPROVER_ensures(__CPROVER_exists {
55
int i;
6-
(0 <= i && i < 10) ==> arr[i] == i
6+
(0 <= i && i < 10) && arr[i] == i
77
})
88
// clang-format on
99
{
@@ -15,8 +15,26 @@ int f1(int *arr)
1515
return 0;
1616
}
1717

18+
// clang-format off
19+
int f2(int *arr)
20+
__CPROVER_assigns(*arr)
21+
__CPROVER_ensures(__CPROVER_exists {
22+
int i;
23+
(0 <= i && i < 10) && arr[i] != 0
24+
})
25+
// clang-format on
26+
{
27+
for(int i = 0; i < 10; i++)
28+
{
29+
arr[i] = 0;
30+
}
31+
32+
return 0;
33+
}
34+
1835
int main()
1936
{
2037
int arr[10];
38+
f2(arr);
2139
f1(arr);
2240
}

‎regression/contracts/quantifiers-exists-ensures-01/test.desc

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
11
CORE
22
main.c
33
--enforce-all-contracts
4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
77
--
8+
^warning: ignoring
89
--
910
The purpose of this test is to ensure that we can safely use __CPROVER_exists
10-
in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag,
11-
goto-instrument will transform the __CPROVER_ensures clauses into an
12-
assertion and the verification remains sound when using __CPROVER_exists.
11+
within positive contexts (enforced ENSURES clauses).
12+
13+
With the SAT backend existential quantifiers in a positive context,
14+
e.g., the ENSURES clause being enforced in this case,
15+
are supported only if the quantifier is bound to a constant range.

‎regression/contracts/quantifiers-exists-ensures-02/main.c

Lines changed: 32 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,41 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
#include <stdlib.h>
4+
5+
#define MAX_LEN 128
6+
17
// clang-format off
2-
int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
3-
int i;
4-
(0 <= i && i < 10) ==> arr[i] != 0
5-
})
8+
int f1(int *arr, int len)
9+
__CPROVER_ensures(
10+
len > 0 ==> __CPROVER_exists {
11+
int i;
12+
// test replacement with symbolic bound
13+
(0 <= i && i < len) && arr[i] == 0
14+
}
15+
)
616
// clang-format on
717
{
8-
for(int i = 0; i < 10; i++)
9-
{
10-
arr[i] = 0;
11-
}
12-
18+
// we are only checking for contract replacement
1319
return 0;
1420
}
1521

1622
int main()
1723
{
18-
int arr[10];
19-
f1(arr);
24+
int len;
25+
__CPROVER_assume(0 <= len && len <= MAX_LEN);
26+
27+
int *arr = malloc(len * sizeof(int));
28+
29+
f1(arr, len);
30+
31+
bool found_zero = false;
32+
for(int i = 0; i <= MAX_LEN; i++)
33+
{
34+
if(i < len)
35+
found_zero |= (arr[i] == 0);
36+
}
37+
38+
// clang-format off
39+
assert(len > 0 ==> found_zero);
40+
// clang-format on
2041
}

‎regression/contracts/quantifiers-exists-ensures-02/test.desc

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,14 @@
11
CORE
22
main.c
3-
--enforce-all-contracts
4-
^EXIT=10$
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
55
^SIGNAL=0$
6-
^VERIFICATION FAILED$
6+
^\[main.assertion.1\] line .* assertion len > 0 ==> found_zero: SUCCESS$
7+
^VERIFICATION SUCCESSFUL$
78
--
9+
^warning: ignoring
810
--
911
The purpose of this test is to ensure that we can safely use __CPROVER_exists
10-
in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag,
11-
goto-instrument will transform the __CPROVER_ensures clauses into an
12-
assertion and the verification remains sound when using __CPROVER_exists.
12+
within negative contexts (replaced ENSURES clauses).
1313

14-
Known Bug:
15-
We expect verification to fail because arr[i] is always equal to 0 for
16-
[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
17-
range for i. However, in the current implementation of quantifier handling,
18-
the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
19-
instead, as part of a logic formula, which causes verification to succeed.
14+
This is fully supported (without requiring full unrolling) with the SAT backend.

‎regression/contracts/quantifiers-exists-requires-01/main.c

Lines changed: 31 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,39 @@
1+
#include <stdbool.h>
2+
#include <stdlib.h>
3+
4+
#define MAX_LEN 64
5+
16
// clang-format off
2-
int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
3-
int i;
4-
(0 <= i && i < 10) ==> arr[i] == 4
5-
}) __CPROVER_ensures(__CPROVER_return_value == 0)
7+
bool f1(int *arr, int len)
8+
__CPROVER_requires(
9+
len > 0 ==> __CPROVER_exists {
10+
int i;
11+
// test enforcement with symbolic bound
12+
(0 <= i && i < len) && arr[i] == 4
13+
}
14+
)
15+
__CPROVER_ensures(
16+
__CPROVER_return_value == true
17+
)
618
// clang-format on
719
{
8-
return 0;
20+
bool found_four = false;
21+
for(int i = 0; i <= MAX_LEN; i++)
22+
{
23+
if(i < len)
24+
found_four |= (arr[i] == 4);
25+
}
26+
27+
// clang-format off
28+
return (len > 0 ==> found_four);
29+
// clang-format on
930
}
1031

1132
int main()
1233
{
13-
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
14-
f1(arr);
34+
int len;
35+
__CPROVER_assume(0 <= len && len <= MAX_LEN);
36+
37+
int *arr = malloc(len * sizeof(int));
38+
f1(arr, len);
1539
}

‎regression/contracts/quantifiers-exists-requires-01/test.desc

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
11
CORE
22
main.c
3-
--replace-all-calls-with-contracts
3+
--enforce-all-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[1\] assertion: SUCCESS$
67
^VERIFICATION SUCCESSFUL$
78
--
9+
^warning: ignoring
810
--
911
The purpose of this test is to ensure that we can safely use __CPROVER_exists
10-
in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
11-
flag, goto-instrument will transform the __CPROVER_requires clauses into an
12-
assertion and the verification remains sound when using __CPROVER_exists.
12+
within both negative contexts (enforced REQUIRES clauses).
13+
14+
This is fully supported (without requiring full unrolling) with the SAT backend.

0 commit comments

Comments
 (0)