Skip to content

Commit 31fe7de

Browse files
author
Long Pham
committed
Multidimensional decreases clauses
1 parent 03213c1 commit 31fe7de

File tree

20 files changed

+342
-85
lines changed

20 files changed

+342
-85
lines changed

‎regression/contracts/variant_missing_invariant_warning/test.desc

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,7 @@
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.$
6-
^\[main.1\].*Check loop invariant before entry: SUCCESS$
7-
^\[main.2\].*Check that loop invariant is preserved: SUCCESS$
85
^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$
96
^EXIT=0$
107
^SIGNAL=0$

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

‎regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c

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

‎regression/contracts/variant_multidimensional_not_decreasing_fail1/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+
^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test fails because the given multidimensional decreases clause does not
10+
monotonically decrease. A mistake is in the second component of the
11+
decreases clause: j. It should instead be N - j.

‎regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c

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

‎regression/contracts/variant_multidimensional_not_decreasing_fail2/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+
^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test fails because the given multidimensional decreases clause does not
10+
monotonically decrease. A mistake is in the first component of the
11+
decreases clause: i. It should instead be N - i.

‎regression/contracts/variant_multidimensional_two_index_variables/main.c

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

‎regression/contracts/variant_multidimensional_two_index_variables/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test succeeds. It tests whether a multidimensional decreases clause works
10+
properly.

‎regression/contracts/variant_not_decreasing_fail/test.desc

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

‎regression/contracts/variant_parsing_tuple_fail/main.c renamed to ‎regression/contracts/variant_parsing_multiple_clauses_fail/main.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ int main()
55
while(i != N)
66
// clang-format off
77
__CPROVER_loop_invariant(0 <= i && i <= N)
8-
__CPROVER_decreases(N - i, 42)
8+
__CPROVER_decreases(N - i)
9+
__CPROVER_decreases(42)
910
// clang-format on
1011
{
1112
i++;

‎regression/contracts/variant_parsing_multiple_clauses_fail/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+
activate-multi-line-match
5+
^main.c.*error: syntax error before '__CPROVER_decreases'\n.*__CPROVER_decreases\(42\)$
6+
^PARSING ERROR$
7+
^EXIT=(1|64)$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test fails because we have multiple decreases clauses. CBMC only admits
12+
one decreases clause for each loop. If one wants to write a multidimensional
13+
decreases clause, it should be placed inside a single __CPROVER_decreases(...),
14+
where each component of the multidimensional decreases clause is separated by a
15+
comma. Hence, in this test, the correct syntax is
16+
__CPROVER_decreases(N - i, 42).

‎regression/contracts/variant_parsing_tuple_fail/test.desc

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

‎regression/contracts/variant_weak_invariant_fail/test.desc

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

‎regression/contracts/variant_while_true_pass/test.desc

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,7 @@
11
CORE
22
main.c
33
--apply-loop-contracts
4-
^main.c function main$
5-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
6-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
74
^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
8-
^.*0 of 3 failed \(1 iterations\)$
9-
^VERIFICATION SUCCESSFUL$
105
^EXIT=0$
116
^SIGNAL=0$
127
--

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -828,9 +828,11 @@ void c_typecheck_baset::typecheck_spec_decreases(codet &code)
828828
{
829829
if(code.find(ID_C_spec_decreases).is_not_nil())
830830
{
831-
exprt &variant = static_cast<exprt &>(code.add(ID_C_spec_decreases));
832-
833-
typecheck_expr(variant);
834-
implicit_typecast_arithmetic(variant);
831+
for(auto &decreases_clause_component :
832+
(static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
833+
{
834+
typecheck_expr(decreases_clause_component);
835+
implicit_typecast_arithmetic(decreases_clause_component);
836+
}
835837
}
836838
}

‎src/ansi-c/parser.y

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -509,10 +509,17 @@ cprover_contract_loop_invariant_list_opt:
509509
| cprover_contract_loop_invariant_list
510510
;
511511

512+
ACSL_binding_expression_list:
513+
ACSL_binding_expression
514+
{ init($$); mto($$, $1); }
515+
| ACSL_binding_expression_list ',' ACSL_binding_expression
516+
{ $$=$1; mto($$, $3); }
517+
;
518+
512519
cprover_contract_decreases_opt:
513520
/* nothing */
514521
{ init($$); parser_stack($$).make_nil(); }
515-
| TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
522+
| TOK_CPROVER_DECREASES '(' ACSL_binding_expression_list ')'
516523
{ $$=$3; }
517524
;
518525

@@ -2449,8 +2456,8 @@ iteration_statement:
24492456
if(!parser_stack($6).operands().empty())
24502457
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
24512458

2452-
if(parser_stack($7).is_not_nil())
2453-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7));
2459+
if(!parser_stack($7).operands().empty())
2460+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
24542461
}
24552462
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
24562463
cprover_contract_assigns_opt
@@ -2464,8 +2471,8 @@ iteration_statement:
24642471
if(!parser_stack($8).operands().empty())
24652472
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
24662473

2467-
if(parser_stack($9).is_not_nil())
2468-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9));
2474+
if(!parser_stack($9).operands().empty())
2475+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands());
24692476
}
24702477
| TOK_FOR
24712478
{
@@ -2495,8 +2502,8 @@ iteration_statement:
24952502
if(!parser_stack($10).operands().empty())
24962503
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
24972504

2498-
if(parser_stack($11).is_not_nil())
2499-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11));
2505+
if(!parser_stack($11).operands().empty())
2506+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($11).operands());
25002507

25012508
if(PARSER.for_has_scope)
25022509
PARSER.pop_scope(); // remove the C99 for-scope

0 commit comments

Comments
 (0)