Skip to content

Commit 92402a9

Browse files
Long PhamLong Pham
Long Pham
authored and
Long Pham
committed
Implemented parsing and type checking for loop variants
1 parent 2e3ba57 commit 92402a9

File tree

21 files changed

+113
-7
lines changed

21 files changed

+113
-7
lines changed

‎regression/contracts/invar_check_break_pass/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ int main()
77

88
while(r > 0)
99
__CPROVER_loop_invariant(r >= 0)
10+
__CPROVER_decreases(r)
1011
{
1112
--r;
1213
if(r <= 1)

‎regression/contracts/invar_check_continue/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ int main()
77

88
while(r > 0)
99
__CPROVER_loop_invariant(r >= 0)
10+
__CPROVER_decreases(r)
1011
{
1112
--r;
1213
if(r < 5)

‎regression/contracts/invar_check_multiple_loops/main.c

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

88
for(r = 0; r < n; ++r)
99
__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
10+
__CPROVER_decreases(n - r)
1011
{
1112
x++;
1213
}
1314
while(r > 0)
1415
__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
16+
__CPROVER_decreases(r)
1517
{
1618
y--;
1719
r--;

‎regression/contracts/invar_check_nested_loops/main.c

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

88
for(int i = 0; i < n; ++i)
99
__CPROVER_loop_invariant(i <= n && s == i)
10+
__CPROVER_decreases(n - i)
1011
{
1112
int a, b;
1213
__CPROVER_assume(b >= 0 && a == b);
1314

1415
while(a > 0)
1516
__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
17+
__CPROVER_decreases(a)
1618
{
1719
s++;
1820
a--;

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ void main()
99
unsigned i;
1010
while(i > 0)
1111
__CPROVER_loop_invariant(*data == 42)
12+
__CPROVER_decreases(i)
1213
{
1314
*data = 42;
1415
i--;

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ void main()
1111
unsigned i;
1212
while(i > 0)
1313
__CPROVER_loop_invariant(*data == 42)
14+
__CPROVER_decreases(i)
1415
{
1516
*data = 42;
1617
i--;

‎regression/contracts/invar_check_sufficiency/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ int main()
77

88
while(r > 0)
99
__CPROVER_loop_invariant(r >= 0)
10+
__CPROVER_decreases(r)
1011
{
1112
--r;
1213
}

‎regression/contracts/invar_loop_constant_no_modify/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ int main()
77
__CPROVER_assume(r >= 0);
88
while(r > 0)
99
__CPROVER_loop_invariant(r >= 0)
10+
__CPROVER_decreases(r)
1011
{
1112
r--;
1213
}

‎regression/contracts/invar_loop_constant_pass/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ int main()
66
__CPROVER_assume(r >= 0);
77
while(r > 0)
88
__CPROVER_loop_invariant(r >= 0 && s == 1)
9+
__CPROVER_decreases(r)
910
{
1011
s = 1;
1112
r--;

‎regression/contracts/invariant_side_effects/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ int main()
88
*a = 0;
99
while(*a < N)
1010
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
11+
__CPROVER_decreases(N - *a)
1112
{
1213
++(*a);
1314
}

‎regression/contracts/variant_parsing_fail/main.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int N = 10;
5+
while (i != N)
6+
__CPROVER_loop_invariant(1 == 1)
7+
__CPROVER__decreases(N - i)
8+
{
9+
i++;
10+
}
11+
12+
return 0;
13+
}

‎regression/contracts/variant_parsing_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+
^main.c: In function 'main':$
5+
^main.c:8:1: error: syntax error before '{'$
6+
^.*{$
7+
^PARSING ERROR$
8+
^EXIT=1$
9+
^SIGNAL=0$
10+
--
11+
--
12+
This test fails because it has two understores (instead of just one)
13+
between CPROVER and loop. This is a parsing error.

‎regression/contracts/variant_typechecking_fail/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
2+
int main()
3+
{
4+
int i = 0;
5+
int N = 10;
6+
while (i != N)
7+
__CPROVER_loop_invariant(1 == 1)
8+
__CPROVER_decreases("This is a string")
9+
{
10+
i++;
11+
}
12+
13+
return 0;
14+
}

‎regression/contracts/variant_typechecking_fail/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+
--enforce-all-contracts
4+
^main.c: In function 'main':$
5+
^main.c:8:1: error: in expression '"This is a string"':$
6+
^conversion from 'char \[17l\]' to 'integer': implicit conversion not permitted
7+
^.*__CPROVER_decreases\("This is a string"\)
8+
^CONVERSION ERROR$
9+
^EXIT=1$
10+
^SIGNAL=0$
11+
--
12+
--
13+
This test fails because a loop variant is a string, and it cannot be
14+
cast to an integer. Hence, type checing of the loop variant fails.

‎src/ansi-c/c_typecheck_base.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/std_code.h>
1717
#include <util/symbol_table.h>
1818
#include <util/typecheck.h>
19+
#include <util/mathematical_types.h>
1920

2021
#include "designator.h"
2122

@@ -120,6 +121,16 @@ class c_typecheck_baset:
120121
implicit_typecast(expr, bool_typet());
121122
}
122123

124+
// This function is necessary for the implementation of loop variants.
125+
// We want to cast loop variants to integers. The class integer_typet from
126+
// mathmatical_types.h represents an unbounded integer type. Ideally,
127+
// we want to use a bounded integer type (as opposed to an unbounded integer
128+
// type) for loop variants.
129+
virtual void implicit_typecast_int(exprt &expr)
130+
{
131+
implicit_typecast(expr, integer_typet());
132+
}
133+
123134
// code
124135
virtual void start_typecheck_code();
125136
virtual void typecheck_code(codet &code);

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -485,6 +485,7 @@ void c_typecheck_baset::typecheck_for(codet &code)
485485
}
486486

487487
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
488+
typecheck_spec_expr(code, ID_C_spec_loop_variant);
488489
}
489490

490491
void c_typecheck_baset::typecheck_label(code_labelt &code)
@@ -773,6 +774,7 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
773774
continue_is_allowed=old_continue_is_allowed;
774775

775776
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
777+
typecheck_spec_expr(code, ID_C_spec_loop_variant);
776778
}
777779

778780
void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
@@ -806,6 +808,7 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
806808
continue_is_allowed=old_continue_is_allowed;
807809

808810
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
811+
typecheck_spec_expr(code, ID_C_spec_loop_variant);
809812
}
810813

811814
void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
@@ -815,6 +818,11 @@ void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
815818
exprt &constraint = static_cast<exprt &>(code.add(spec));
816819

817820
typecheck_expr(constraint);
818-
implicit_typecast_bool(constraint);
821+
if (spec == ID_C_spec_loop_invariant) {
822+
implicit_typecast_bool(constraint);
823+
}
824+
else if (spec == ID_C_spec_loop_variant) {
825+
implicit_typecast_int(constraint);
826+
}
819827
}
820828
}

‎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_LOOP_VARIANT "__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+
loop_variant_opt:
502+
/* nothing */
503+
{ init($$); parser_stack($$).make_nil(); }
504+
| TOK_CPROVER_LOOP_VARIANT '(' 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 loop_variant_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_loop_variant).swap(parser_stack($6));
24292441
}
24302442
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
2431-
loop_invariant_opt ';'
2443+
loop_invariant_opt loop_variant_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_loop_variant).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 loop_variant_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_loop_variant).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_LOOP_VARIANT; }
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/goto-instrument/loop_utils.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,7 @@ void get_modifies_lhs(
116116
const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
117117
for(const auto &mod : local_may_alias.get(t, ptr.pointer))
118118
{
119+
if(mod.id() == ID_unknown) continue;
119120
if(ptr.offset.is_nil())
120121
modifies.insert(dereference_exprt{mod});
121122
else

‎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_loop_variant, #spec_loop_variant)
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)