Skip to content

Commit d98b56b

Browse files
SaswatPadhiSaswatPadhi
authored
Merge pull request #5959 from ArenBabikian/contracts-quantifiers-new
Supports quantifiers in function contracts
2 parents 2b5ea24 + edeaf56 commit d98b56b

File tree

27 files changed

+447
-2
lines changed

27 files changed

+447
-2
lines changed

‎regression/contracts/function_check_02/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--check-code-contracts
3+
--enforce-all-contracts
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// 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+
})
9+
// clang-format on
10+
{
11+
return 0;
12+
}
13+
14+
int main()
15+
{
16+
int arr[8];
17+
f1(arr);
18+
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
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.

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// 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+
})
9+
// clang-format on
10+
{
11+
return 0;
12+
}
13+
14+
int main()
15+
{
16+
int len, arr[8];
17+
f1(arr, len);
18+
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
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.
14+
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).

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == i
5+
})
6+
// clang-format on
7+
{
8+
for(int i = 0; i < 10; i++)
9+
{
10+
arr[i] = i;
11+
}
12+
13+
return 0;
14+
}
15+
16+
int main()
17+
{
18+
int arr[10];
19+
f1(arr);
20+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
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.

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] != 0
5+
})
6+
// clang-format on
7+
{
8+
for(int i = 0; i < 10; i++)
9+
{
10+
arr[i] = 0;
11+
}
12+
13+
return 0;
14+
}
15+
16+
int main()
17+
{
18+
int arr[10];
19+
f1(arr);
20+
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
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.
13+
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.

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// 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)
6+
// clang-format on
7+
{
8+
return 0;
9+
}
10+
11+
int main()
12+
{
13+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
14+
f1(arr);
15+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
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.

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

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

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
KNOWNBUG
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
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.
13+
14+
Known Bug:
15+
We expect verification to fail because arr[i] is never equal to 1 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.

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

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

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
The purpose of this test is to ensure that we can safely use __CPROVER_forall
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.

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// clang-format off
2+
int f1(int *arr, int len) __CPROVER_requires(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < len) ==> arr[i] == 0
5+
}) __CPROVER_ensures(__CPROVER_forall {
6+
int i;
7+
(0 <= i && i < len) ==> arr[i] == 0
8+
})
9+
// clang-format on
10+
{
11+
return 0;
12+
}
13+
14+
int main()
15+
{
16+
int len, arr[8];
17+
f1(arr, len);
18+
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
The purpose of this test is to ensure that we can safely use __CPROVER_forall
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.
14+
15+
Known bug:
16+
The current implementation cannot handle a structure such as
17+
__CPROVER_assume(__CPROVER_forall(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).

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == 0
5+
})
6+
// clang-format on
7+
{
8+
for(int i = 0; i < 10; i++)
9+
{
10+
arr[i] = 0;
11+
}
12+
13+
return 0;
14+
}
15+
16+
int main()
17+
{
18+
int arr[10];
19+
f1(arr);
20+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
The purpose of this test is to ensure that we can safely use __CPROVER_forall
10+
in __CPROVER_ensures clauses. By using the --enforce-all-contracts
11+
flag, goto-instrument will transform the __CPROVER_ensures clauses into an
12+
assertion and the verification remains sound when using __CPROVER_forall.

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == i
5+
})
6+
// clang-format on
7+
{
8+
for(int i = 0; i < 10; i++)
9+
{
10+
if(i == 0)
11+
arr[i] = -1;
12+
else
13+
arr[i] = i;
14+
}
15+
16+
return 0;
17+
}
18+
19+
int main()
20+
{
21+
int arr[10];
22+
f1(arr);
23+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
The purpose of this test is to ensure that we can safely use __CPROVER_forall
10+
in __CPROVER_ensures clauses. By using the --enforce-all-contracts
11+
flag, goto-instrument will transform the __CPROVER_ensures clauses into an
12+
assertion and the verification remains sound when using __CPROVER_forall.

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

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

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
The purpose of this test is to ensure that we can safely use __CPROVER_forall
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_forall.

0 commit comments

Comments
 (0)