Skip to content

Commit 08060b4

Browse files
Long PhamLong Pham
Long Pham
authored and
Long Pham
committed
Implemented parsing and type checking for loop variants
1 parent abd4412 commit 08060b4

File tree

8 files changed

+56
-7
lines changed

8 files changed

+56
-7
lines changed

‎src/ansi-c/c_typecheck_base.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,13 @@ class c_typecheck_baset:
120120
implicit_typecast(expr, bool_typet());
121121
}
122122

123+
/* This function is necessary for the implementation of loop variants.
124+
We want to cast loop variants to integers. */
125+
virtual void implicit_typecast_int(exprt &expr)
126+
{
127+
implicit_typecast(expr, int_typet());
128+
}
129+
123130
// code
124131
virtual void start_typecheck_code();
125132
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: 25 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ extern char *yyansi_ctext;
2828

2929
#include <util/mathematical_expr.h>
3030

31+
#include <iostream>
32+
3133
#ifdef _MSC_VER
3234
// possible loss of data
3335
#pragma warning(disable:4242)
@@ -203,6 +205,7 @@ extern char *yyansi_ctext;
203205
%token TOK_CPROVER_FINALLY "__CPROVER_finally"
204206
%token TOK_CPROVER_ID "__CPROVER_ID"
205207
%token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant"
208+
%token TOK_CPROVER_LOOP_VARIANT "__CPROVER_loop_variant"
206209
%token TOK_CPROVER_REQUIRES "__CPROVER_requires"
207210
%token TOK_CPROVER_ENSURES "__CPROVER_ensures"
208211
%token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
@@ -497,6 +500,13 @@ loop_invariant_opt:
497500
{ $$=$3; }
498501
;
499502

503+
loop_variant_opt:
504+
/* nothing */
505+
{ init($$); parser_stack($$).make_nil(); }
506+
| TOK_CPROVER_LOOP_VARIANT '(' ACSL_binding_expression ')'
507+
{ $$=$3; std::cout<<"Loop variant has been parsed.\n"; }
508+
;
509+
500510
statement_expression: '(' compound_statement ')'
501511
{
502512
$$=$1;
@@ -2418,24 +2428,31 @@ declaration_or_expression_statement:
24182428

24192429
iteration_statement:
24202430
TOK_WHILE '(' comma_expression_opt ')'
2421-
loop_invariant_opt statement
2431+
loop_invariant_opt loop_variant_opt
2432+
statement
24222433
{
24232434
$$=$1;
24242435
statement($$, ID_while);
2425-
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($6)));
2436+
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));
24262437

24272438
if(parser_stack($5).is_not_nil())
24282439
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5));
2440+
2441+
if(parser_stack($6).is_not_nil())
2442+
parser_stack($$).add(ID_C_spec_loop_variant).swap(parser_stack($6));
24292443
}
24302444
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
2431-
loop_invariant_opt ';'
2445+
loop_invariant_opt loop_variant_opt ';'
24322446
{
24332447
$$=$1;
24342448
statement($$, ID_dowhile);
24352449
parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
24362450

24372451
if(parser_stack($7).is_not_nil())
24382452
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($7));
2453+
2454+
if(parser_stack($8).is_not_nil())
2455+
parser_stack($$).add(ID_C_spec_loop_variant).swap(parser_stack($8));
24392456
}
24402457
| TOK_FOR
24412458
{
@@ -2449,7 +2466,7 @@ iteration_statement:
24492466
'(' declaration_or_expression_statement
24502467
comma_expression_opt ';'
24512468
comma_expression_opt ')'
2452-
loop_invariant_opt
2469+
loop_invariant_opt loop_variant_opt
24532470
statement
24542471
{
24552472
$$=$1;
@@ -2458,11 +2475,14 @@ iteration_statement:
24582475
mto($$, $4);
24592476
mto($$, $5);
24602477
mto($$, $7);
2461-
mto($$, $10);
2478+
mto($$, $11);
24622479

24632480
if(parser_stack($9).is_not_nil())
24642481
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($9));
24652482

2483+
if(parser_stack($10).is_not_nil())
2484+
parser_stack($$).add(ID_C_spec_loop_variant).swap(parser_stack($10));
2485+
24662486
if(PARSER.for_has_scope)
24672487
PARSER.pop_scope(); // remove the C99 for-scope
24682488
}

‎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}"loop_variant" { 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)

‎src/util/std_types.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,17 @@ class bool_typet:public typet
4040
}
4141
};
4242

43+
/// The int type.
44+
/// This is necessary for the type checking of loop variants, which should have
45+
/// some kind of integer type.
46+
class int_typet:public typet
47+
{
48+
public:
49+
int_typet():typet(ID_integer)
50+
{
51+
}
52+
};
53+
4354
/// The empty type
4455
class empty_typet:public typet
4556
{

0 commit comments

Comments
 (0)