Skip to content

Commit 5592d7e

Browse files
feliperodrifeliperodri
authored
Merge pull request #6236 from LongPham7/Long_internship
Multidimensional decreases clauses
2 parents 7e291a5 + 36f661e commit 5592d7e

File tree

18 files changed

+346
-77
lines changed

18 files changed

+346
-77
lines changed

‎regression/contracts/variant_missing_invariant_warning/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
CORE
22
main.c
33
--apply-loop-contracts
4-
activate-multi-line-match
54
^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.$
65
^\[main.1\].*Check loop invariant before entry: SUCCESS$
76
^\[main.2\].*Check that loop invariant is preserved: SUCCESS$
87
^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$
8+
^VERIFICATION SUCCESSFUL$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

‎regression/contracts/variant_multidimensional_ackermann/main.c

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
#include <stdio.h>
2+
3+
int ackermann(int m, int n);
4+
5+
int main()
6+
{
7+
int m = 3;
8+
int n = 5;
9+
int result = ackermann(m, n);
10+
11+
printf("Result of the Ackermann function: %d\n", result);
12+
return 0;
13+
}
14+
15+
int ackermann(int m, int n)
16+
// clang-format off
17+
__CPROVER_requires(0 <= m && 0 <= n)
18+
__CPROVER_ensures(__CPROVER_return_value >= 0)
19+
// clang-format on
20+
{
21+
while(m > 0)
22+
// clang-format off
23+
__CPROVER_loop_invariant(0 <= m && 0 <= n)
24+
__CPROVER_decreases(m, n)
25+
// clang-format on
26+
{
27+
if(n == 0)
28+
{
29+
m--;
30+
n = 1;
31+
}
32+
else
33+
{
34+
n = ackermann(m, n - 1);
35+
m--;
36+
}
37+
}
38+
39+
return n + 1;
40+
}

‎regression/contracts/variant_multidimensional_ackermann/test.desc

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts --replace-all-calls-with-contracts
4+
^\[precondition.1\] .* Check requires clause: SUCCESS$
5+
^\[precondition.2\] .* Check requires clause: SUCCESS$
6+
^\[ackermann.1\] .* Check loop invariant before entry: SUCCESS$
7+
^\[ackermann.2\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[ackermann.3\] .* Check decreases clause on loop iteration: SUCCESS$
9+
^VERIFICATION SUCCESSFUL$
10+
^EXIT=0$
11+
^SIGNAL=0$
12+
--
13+
--
14+
It tests whether we can prove (only partially) the termination of the Ackermann
15+
function using a multidimensional decreases clause.
16+
17+
Note that this particular implementation of the Ackermann function contains
18+
both a while-loop and recursion. Therefore, to fully prove the termination of
19+
the Ackermann function, we must prove both
20+
(i) the termination of the while-loop and
21+
(ii) the termination of the recursion.
22+
Because CBMC does not support termination proofs of recursions (yet), we cannot
23+
prove the latter, but the former. Hence, the termination proof in the code is
24+
only "partial."
25+
26+
Furthermore, the Ackermann function has a function contract that the result
27+
is always non-negative. This post-condition is necessary for establishing
28+
the loop invariant. However, in this test, we do not enforce the function
29+
contract. Instead, we assume that the function contract is correct and use it
30+
(i.e. replace a recursive call of the Ackermann function with its contract).
31+
32+
We cannot verify/enforce the function contract of the Ackermann function, since
33+
CBMC does not support function contracts for recursively defined functions.
34+
As of now, CBMC only supports function contracts for non-recursive functions.

‎regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int j = 0;
5+
int N = 10;
6+
while(i < N)
7+
// clang-format off
8+
__CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
9+
__CPROVER_decreases(N - i, j)
10+
// clang-format on
11+
{
12+
if(j < N)
13+
{
14+
j++;
15+
}
16+
else
17+
{
18+
i++;
19+
j = 0;
20+
}
21+
}
22+
}

‎regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
5+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
6+
^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
7+
^VERIFICATION FAILED$
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
--
12+
This test fails because the given multidimensional decreases clause does not
13+
monotonically decrease. A mistake is in the second component of the
14+
decreases clause: j. It should instead be N - j.

‎regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int j = 0;
5+
int N = 10;
6+
while(i < N)
7+
// clang-format off
8+
__CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
9+
__CPROVER_decreases(i, N - j)
10+
// clang-format on
11+
{
12+
if(j < N)
13+
{
14+
j++;
15+
}
16+
else
17+
{
18+
i++;
19+
j = 0;
20+
}
21+
}
22+
}

‎regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
5+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
6+
^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
7+
^VERIFICATION FAILED$
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
--
12+
This test fails because the given multidimensional decreases clause does not
13+
monotonically decrease. A mistake is in the first component of the
14+
decreases clause: i. It should instead be N - i.

‎regression/contracts/variant_multidimensional_two_index_variables/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int j = 0;
5+
int N = 10;
6+
while(i < N)
7+
// clang-format off
8+
__CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N)
9+
__CPROVER_decreases(N - i, N - j)
10+
// clang-format on
11+
{
12+
if(j < N)
13+
{
14+
j++;
15+
}
16+
else
17+
{
18+
i++;
19+
j = 0;
20+
}
21+
}
22+
}

‎regression/contracts/variant_multidimensional_two_index_variables/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+
--apply-loop-contracts
4+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
5+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
6+
^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
7+
^VERIFICATION SUCCESSFUL$
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
--
12+
It tests whether a multidimensional decreases clause works properly.

‎regression/contracts/variant_not_decreasing_fail/test.desc

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--apply-loop-contracts
4-
^main.c function main$
54
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
65
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
76
^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
8-
^.* 1 of 3 failed \(2 iterations\)$
97
^VERIFICATION FAILED$
108
^EXIT=10$
119
^SIGNAL=0$

0 commit comments

Comments
 (0)