Skip to content

Commit 8a50d78

Browse files
Aren BabikianArenBabikian
Aren Babikian
authored and
ArenBabikian
committed
Add support for quantifiers in function contracts
This adds basic support for quantifiers in funtion contracts. Current support only handles cases where a function contract contains a single, non-nested quantified formula.
1 parent 2459a7a commit 8a50d78

File tree

27 files changed

+441
-2
lines changed

27 files changed

+441
-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: 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 a negative context. By using the --enforce-all-contracts flag, this test
11+
assumes the statement in __CPROVER_requires, then asserts the same statement
12+
(in __CPROVER_ensures), 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: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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. By using the --enforce-all-contracts flag, this test
11+
assumes the statement in __CPROVER_requires, then asserts the same statement
12+
(in __CPROVER_ensures), thus, verification should be successful.
13+
14+
Known bug:
15+
The current implementation cannot handle a structure such as
16+
__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is
17+
not explicitly bounded to a predefined range (i.e. if at least
18+
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 safety 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 safety 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 safety 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 safety 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: 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 a negative context. By using the --enforce-all-contracts flag, this test
11+
assumes the statement in __CPROVER_requires, then asserts the same statement
12+
(in __CPROVER_ensures), 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: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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. By using the --enforce-all-contracts flag, this test
11+
assumes the statement in __CPROVER_requires, then asserts the same statement
12+
(in __CPROVER_ensures), thus, verification should be successful.
13+
14+
Known bug:
15+
The current implementation cannot handle a structure such as
16+
__CPROVER_assume(__CPROVER_forall(int i; pred(i))), where i is
17+
not explicitly bounded to a predefined range (i.e. if at least
18+
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 safety 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 safety 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 safety 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)