Skip to content

Commit 99ccbcd

Browse files
SaswatPadhiSaswatPadhi
authored
Merge pull request #6183 from LongPham7/Long_internship
Parsing and type-checking loop variants (aka ranking functions)
2 parents 3c62abb + 72f9431 commit 99ccbcd

File tree

21 files changed

+146
-17
lines changed

21 files changed

+146
-17
lines changed

‎regression/contracts/invar_check_break_pass/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
if(r <= 1)

‎regression/contracts/invar_check_continue/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
if(r < 5)

‎regression/contracts/invar_check_large/main.c

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@ int main()
2222
int l = 0;
2323
int r = 1;
2424
while(h > l)
25+
// clang-format off
2526
__CPROVER_loop_invariant(
2627
// Turn off `clang-format` because it breaks the `==>` operator.
27-
/* clang-format off */
2828
h >= l &&
2929
0 <= l && l < 5 &&
3030
0 <= h && h < 5 &&
@@ -44,8 +44,9 @@ int main()
4444
(2 > h ==> arr2 >= pivot) &&
4545
(3 > h ==> arr3 >= pivot) &&
4646
(4 > h ==> arr4 >= pivot)
47-
/* clang-format on */
4847
)
48+
__CPROVER_decreases(h - l)
49+
// clang-format on
4950
{
5051
if(*(arr[h]) <= pivot && *(arr[l]) >= pivot)
5152
{

‎regression/contracts/invar_check_multiple_loops/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,18 @@ int main()
66
__CPROVER_assume(n > 0 && x == y);
77

88
for(r = 0; r < n; ++r)
9+
// clang-format off
910
__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
11+
__CPROVER_decreases(n - r)
12+
// clang-format on
1013
{
1114
x++;
1215
}
1316
while(r > 0)
17+
// clang-format off
1418
__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
19+
__CPROVER_decreases(r)
20+
// clang-format on
1521
{
1622
y--;
1723
r--;

‎regression/contracts/invar_check_nested_loops/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,19 @@ int main()
66
__CPROVER_assume(n >= 0);
77

88
for(int i = 0; i < n; ++i)
9+
// clang-format off
910
__CPROVER_loop_invariant(i <= n && s == i)
11+
__CPROVER_decreases(n - i)
12+
// clang-format on
1013
{
1114
int a, b;
1215
__CPROVER_assume(b >= 0 && a == b);
1316

1417
while(a > 0)
18+
// clang-format off
1519
__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
20+
__CPROVER_decreases(a)
21+
// clang-format on
1622
{
1723
s++;
1824
a--;

‎regression/contracts/invar_check_pointer_modifies-01/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,10 @@ void main()
88

99
unsigned i;
1010
while(i > 0)
11+
// clang-format off
1112
__CPROVER_loop_invariant(*data == 42)
13+
__CPROVER_decreases(i)
14+
// clang-format on
1215
{
1316
*data = 42;
1417
i--;

‎regression/contracts/invar_check_pointer_modifies-02/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,10 @@ void main()
1010

1111
unsigned i;
1212
while(i > 0)
13+
// clang-format off
1314
__CPROVER_loop_invariant(*data == 42)
15+
__CPROVER_decreases(i)
16+
// clang-format on
1417
{
1518
*data = 42;
1619
i--;

‎regression/contracts/invar_check_sufficiency/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
}

‎regression/contracts/invar_loop_constant_no_modify/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
int s = 1;
77
__CPROVER_assume(r >= 0);
88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
r--;
1215
}

‎regression/contracts/invar_loop_constant_pass/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,10 @@ int main()
55
int r, s = 1;
66
__CPROVER_assume(r >= 0);
77
while(r > 0)
8+
// clang-format off
89
__CPROVER_loop_invariant(r >= 0 && s == 1)
10+
__CPROVER_decreases(r)
11+
// clang-format on
912
{
1013
s = 1;
1114
r--;

‎regression/contracts/invariant_side_effects/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@ int main()
77

88
*a = 0;
99
while(*a < N)
10+
// clang-format off
1011
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
12+
__CPROVER_decreases(N - *a)
13+
// clang-format on
1114
{
1215
++(*a);
1316
}

‎regression/contracts/variant_parsing_statement_fail/main.c

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

‎regression/contracts/variant_parsing_statement_fail/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+
activate-multi-line-match
5+
^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$
6+
^PARSING ERROR$
7+
^EXIT=(1|64)$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test fails because the loop variant is a statement (more precisely,
12+
an assignment) rather than an expression (more precisely, an ACSL binding
13+
expression).

‎regression/contracts/variant_parsing_tuple_fail/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int N = 10;
5+
while(i != N)
6+
// clang-format off
7+
__CPROVER_loop_invariant(0 <= i && i <= N)
8+
__CPROVER_decreases(N - i, 42)
9+
// clang-format on
10+
{
11+
i++;
12+
}
13+
14+
return 0;
15+
}

‎regression/contracts/variant_parsing_tuple_fail/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+
activate-multi-line-match
5+
^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$
6+
^PARSING ERROR$
7+
^EXIT=(1|64)$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test fails because the loop variant has two arguments instead of just one.
12+
Currently, we only support loop variants of single arguments - we do not
13+
support loop variants of tuples (yet).

‎src/ansi-c/c_typecheck_base.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,8 @@ class c_typecheck_baset:
144144
virtual void typecheck_while(code_whilet &code);
145145
virtual void typecheck_dowhile(code_dowhilet &code);
146146
virtual void typecheck_start_thread(codet &code);
147-
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
147+
virtual void typecheck_spec_loop_invariant(codet &code);
148+
virtual void typecheck_spec_decreases(codet &code);
148149

149150
bool break_is_allowed;
150151
bool continue_is_allowed;

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,8 @@ void c_typecheck_baset::typecheck_for(codet &code)
484484
typecheck_code(code); // recursive call
485485
}
486486

487-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
487+
typecheck_spec_loop_invariant(code);
488+
typecheck_spec_decreases(code);
488489
}
489490

490491
void c_typecheck_baset::typecheck_label(code_labelt &code)
@@ -772,7 +773,8 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
772773
break_is_allowed=old_break_is_allowed;
773774
continue_is_allowed=old_continue_is_allowed;
774775

775-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
776+
typecheck_spec_loop_invariant(code);
777+
typecheck_spec_decreases(code);
776778
}
777779

778780
void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
@@ -805,16 +807,28 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
805807
break_is_allowed=old_break_is_allowed;
806808
continue_is_allowed=old_continue_is_allowed;
807809

808-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
810+
typecheck_spec_loop_invariant(code);
811+
typecheck_spec_decreases(code);
809812
}
810813

811-
void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
814+
void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
812815
{
813-
if(code.find(spec).is_not_nil())
816+
if(code.find(ID_C_spec_loop_invariant).is_not_nil())
814817
{
815-
exprt &constraint = static_cast<exprt &>(code.add(spec));
818+
exprt &invariant = static_cast<exprt &>(code.add(ID_C_spec_loop_invariant));
816819

817-
typecheck_expr(constraint);
818-
implicit_typecast_bool(constraint);
820+
typecheck_expr(invariant);
821+
implicit_typecast_bool(invariant);
822+
}
823+
}
824+
825+
void c_typecheck_baset::typecheck_spec_decreases(codet &code)
826+
{
827+
if(code.find(ID_C_spec_decreases).is_not_nil())
828+
{
829+
exprt &variant = static_cast<exprt &>(code.add(ID_C_spec_decreases));
830+
831+
typecheck_expr(variant);
832+
implicit_typecast_arithmetic(variant);
819833
}
820834
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)
5151
return;
5252
}
5353

54-
// fist do sub-nodes
54+
// first do sub-nodes
5555
typecheck_expr_operands(expr);
5656

5757
// now do case-split

‎src/ansi-c/parser.y

Lines changed: 23 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,7 @@ extern char *yyansi_ctext;
203203
%token TOK_CPROVER_FINALLY "__CPROVER_finally"
204204
%token TOK_CPROVER_ID "__CPROVER_ID"
205205
%token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant"
206+
%token TOK_CPROVER_DECREASES "__CPROVER_decreases"
206207
%token TOK_CPROVER_REQUIRES "__CPROVER_requires"
207208
%token TOK_CPROVER_ENSURES "__CPROVER_ensures"
208209
%token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
@@ -497,6 +498,13 @@ loop_invariant_opt:
497498
{ $$=$3; }
498499
;
499500

501+
cprover_decreases_opt:
502+
/* nothing */
503+
{ init($$); parser_stack($$).make_nil(); }
504+
| TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
505+
{ $$=$3; }
506+
;
507+
500508
statement_expression: '(' compound_statement ')'
501509
{
502510
$$=$1;
@@ -2418,24 +2426,31 @@ declaration_or_expression_statement:
24182426

24192427
iteration_statement:
24202428
TOK_WHILE '(' comma_expression_opt ')'
2421-
loop_invariant_opt statement
2429+
loop_invariant_opt cprover_decreases_opt
2430+
statement
24222431
{
24232432
$$=$1;
24242433
statement($$, ID_while);
2425-
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($6)));
2434+
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));
24262435

24272436
if(parser_stack($5).is_not_nil())
24282437
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5));
2438+
2439+
if(parser_stack($6).is_not_nil())
2440+
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
24292441
}
24302442
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
2431-
loop_invariant_opt ';'
2443+
loop_invariant_opt cprover_decreases_opt ';'
24322444
{
24332445
$$=$1;
24342446
statement($$, ID_dowhile);
24352447
parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
24362448

24372449
if(parser_stack($7).is_not_nil())
24382450
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($7));
2451+
2452+
if(parser_stack($8).is_not_nil())
2453+
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
24392454
}
24402455
| TOK_FOR
24412456
{
@@ -2449,7 +2464,7 @@ iteration_statement:
24492464
'(' declaration_or_expression_statement
24502465
comma_expression_opt ';'
24512466
comma_expression_opt ')'
2452-
loop_invariant_opt
2467+
loop_invariant_opt cprover_decreases_opt
24532468
statement
24542469
{
24552470
$$=$1;
@@ -2458,11 +2473,14 @@ iteration_statement:
24582473
mto($$, $4);
24592474
mto($$, $5);
24602475
mto($$, $7);
2461-
mto($$, $10);
2476+
mto($$, $11);
24622477

24632478
if(parser_stack($9).is_not_nil())
24642479
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($9));
24652480

2481+
if(parser_stack($10).is_not_nil())
2482+
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));
2483+
24662484
if(PARSER.for_has_scope)
24672485
PARSER.pop_scope(); // remove the C99 for-scope
24682486
}

‎src/ansi-c/scanner.l

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1281,6 +1281,7 @@ __decltype { if(PARSER.cpp98 &&
12811281
{CPROVER_PREFIX}"finally" { loc(); return TOK_CPROVER_FINALLY; }
12821282
{CPROVER_PREFIX}"ID" { loc(); return TOK_CPROVER_ID; }
12831283
{CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; }
1284+
{CPROVER_PREFIX}"decreases" { loc(); return TOK_CPROVER_DECREASES; }
12841285
{CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; }
12851286
{CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; }
12861287
{CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; }

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -572,6 +572,7 @@ IREP_ID_ONE(is_weak)
572572
IREP_ID_ONE(used)
573573
IREP_ID_ONE(is_used)
574574
IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
575+
IREP_ID_TWO(C_spec_decreases, #spec_decreases)
575576
IREP_ID_TWO(C_spec_requires, #spec_requires)
576577
IREP_ID_TWO(C_spec_ensures, #spec_ensures)
577578
IREP_ID_TWO(C_spec_assigns, #spec_assigns)

0 commit comments

Comments
 (0)