Skip to content

Parsing and type-checking loop variants (aka ranking functions) #6183

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 23, 2021
Merged

Parsing and type-checking loop variants (aka ranking functions) #6183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions regression/contracts/invar_check_break_pass/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@ int main()
__CPROVER_assume(r >= 0);

while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0)
__CPROVER_decreases(r)
// clang-format on
{
--r;
if(r <= 1)
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_check_continue/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@ int main()
__CPROVER_assume(r >= 0);

while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0)
__CPROVER_decreases(r)
// clang-format on
{
--r;
if(r < 5)
Expand Down
5 changes: 3 additions & 2 deletions regression/contracts/invar_check_large/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@ int main()
int l = 0;
int r = 1;
while(h > l)
// clang-format off
__CPROVER_loop_invariant(
// Turn off `clang-format` because it breaks the `==>` operator.
/* clang-format off */
h >= l &&
0 <= l && l < 5 &&
0 <= h && h < 5 &&
Expand All @@ -44,8 +44,9 @@ int main()
(2 > h ==> arr2 >= pivot) &&
(3 > h ==> arr3 >= pivot) &&
(4 > h ==> arr4 >= pivot)
/* clang-format on */
)
__CPROVER_decreases(h - l)
// clang-format on
{
if(*(arr[h]) <= pivot && *(arr[l]) >= pivot)
{
Expand Down
6 changes: 6 additions & 0 deletions regression/contracts/invar_check_multiple_loops/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,18 @@ int main()
__CPROVER_assume(n > 0 && x == y);

for(r = 0; r < n; ++r)
// clang-format off
__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
__CPROVER_decreases(n - r)
// clang-format on
{
x++;
}
while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
__CPROVER_decreases(r)
// clang-format on
{
y--;
r--;
Expand Down
6 changes: 6 additions & 0 deletions regression/contracts/invar_check_nested_loops/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,19 @@ int main()
__CPROVER_assume(n >= 0);

for(int i = 0; i < n; ++i)
// clang-format off
__CPROVER_loop_invariant(i <= n && s == i)
__CPROVER_decreases(n - i)
// clang-format on
{
int a, b;
__CPROVER_assume(b >= 0 && a == b);

while(a > 0)
// clang-format off
__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
__CPROVER_decreases(a)
// clang-format on
{
s++;
a--;
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_check_pointer_modifies-01/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ void main()

unsigned i;
while(i > 0)
// clang-format off
__CPROVER_loop_invariant(*data == 42)
__CPROVER_decreases(i)
// clang-format on
{
*data = 42;
i--;
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_check_pointer_modifies-02/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ void main()

unsigned i;
while(i > 0)
// clang-format off
__CPROVER_loop_invariant(*data == 42)
__CPROVER_decreases(i)
// clang-format on
{
*data = 42;
i--;
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_check_sufficiency/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@ int main()
__CPROVER_assume(r >= 0);

while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0)
__CPROVER_decreases(r)
// clang-format on
{
--r;
}
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_loop_constant_no_modify/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@ int main()
int s = 1;
__CPROVER_assume(r >= 0);
while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0)
__CPROVER_decreases(r)
// clang-format on
{
r--;
}
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invar_loop_constant_pass/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,10 @@ int main()
int r, s = 1;
__CPROVER_assume(r >= 0);
while(r > 0)
// clang-format off
__CPROVER_loop_invariant(r >= 0 && s == 1)
__CPROVER_decreases(r)
// clang-format on
{
s = 1;
r--;
Expand Down
3 changes: 3 additions & 0 deletions regression/contracts/invariant_side_effects/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,10 @@ int main()

*a = 0;
while(*a < N)
// clang-format off
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
__CPROVER_decreases(N - *a)
// clang-format on
{
++(*a);
}
Expand Down
16 changes: 16 additions & 0 deletions regression/contracts/variant_parsing_statement_fail/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@

int main()
{
int i = 0;
int N = 10;
while(i != N)
// clang-format off
__CPROVER_loop_invariant(0 <= i && i <= N)
__CPROVER_decreases(int x = 0)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to have a __CPROVER_decreases without a loop invariant?

Copy link
Author

@LongPham7 LongPham7 Jun 23, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it is possible. The default loop invariant is true. The code for that is already in my local repository, and I will file a second PR soon.

// clang-format on
{
i++;
}

return 0;
}
13 changes: 13 additions & 0 deletions regression/contracts/variant_parsing_statement_fail/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
CORE
main.c
--enforce-all-contracts
activate-multi-line-match
^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$
^PARSING ERROR$
^EXIT=(1|64)$
^SIGNAL=0$
--
--
This test fails because the loop variant is a statement (more precisely,
an assignment) rather than an expression (more precisely, an ACSL binding
expression).
15 changes: 15 additions & 0 deletions regression/contracts/variant_parsing_tuple_fail/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
int main()
{
int i = 0;
int N = 10;
while(i != N)
// clang-format off
__CPROVER_loop_invariant(0 <= i && i <= N)
__CPROVER_decreases(N - i, 42)
// clang-format on
{
i++;
}

return 0;
}
13 changes: 13 additions & 0 deletions regression/contracts/variant_parsing_tuple_fail/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
CORE
main.c
--enforce-all-contracts
activate-multi-line-match
^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$
^PARSING ERROR$
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice to see some negative tests!

^EXIT=(1|64)$
^SIGNAL=0$
--
--
This test fails because the loop variant has two arguments instead of just one.
Currently, we only support loop variants of single arguments - we do not
support loop variants of tuples (yet).
3 changes: 2 additions & 1 deletion src/ansi-c/c_typecheck_base.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,8 @@ class c_typecheck_baset:
virtual void typecheck_while(code_whilet &code);
virtual void typecheck_dowhile(code_dowhilet &code);
virtual void typecheck_start_thread(codet &code);
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
virtual void typecheck_spec_loop_invariant(codet &code);
virtual void typecheck_spec_decreases(codet &code);

bool break_is_allowed;
bool continue_is_allowed;
Expand Down
30 changes: 22 additions & 8 deletions src/ansi-c/c_typecheck_code.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -484,7 +484,8 @@ void c_typecheck_baset::typecheck_for(codet &code)
typecheck_code(code); // recursive call
}

typecheck_spec_expr(code, ID_C_spec_loop_invariant);
typecheck_spec_loop_invariant(code);
typecheck_spec_decreases(code);
}

void c_typecheck_baset::typecheck_label(code_labelt &code)
Expand Down Expand Up @@ -772,7 +773,8 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
break_is_allowed=old_break_is_allowed;
continue_is_allowed=old_continue_is_allowed;

typecheck_spec_expr(code, ID_C_spec_loop_invariant);
typecheck_spec_loop_invariant(code);
typecheck_spec_decreases(code);
}

void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
Expand Down Expand Up @@ -805,16 +807,28 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
break_is_allowed=old_break_is_allowed;
continue_is_allowed=old_continue_is_allowed;

typecheck_spec_expr(code, ID_C_spec_loop_invariant);
typecheck_spec_loop_invariant(code);
typecheck_spec_decreases(code);
}

void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
{
if(code.find(spec).is_not_nil())
if(code.find(ID_C_spec_loop_invariant).is_not_nil())
{
exprt &constraint = static_cast<exprt &>(code.add(spec));
exprt &invariant = static_cast<exprt &>(code.add(ID_C_spec_loop_invariant));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there anything else we could check at this point? For instance, the number of operands? @SaswatPadhi

 // this comes with 1 operand, which is a Boolean statement
  if(code.operands().size()!=1)
  {
    error().source_location = code.source_location();
    error() << "decreases expected to have 1 operand" << eom;
    throw 0;
  }

Copy link
Contributor

@SaswatPadhi SaswatPadhi Jun 23, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a good idea, but that's already taken care of by the parsing rule, so we don't need to add it to the type checker.

For instance, take a look at regression/contracts/variant_parsing_tuple_fail regression test added in this PR.

Also note that in future this restriction would be relaxed to allow multi-dimensional ranking functions. I'm not sure if we'll make __CPROVER_decreases variadic, or allow some other syntax for tuples.


typecheck_expr(constraint);
implicit_typecast_bool(constraint);
typecheck_expr(invariant);
implicit_typecast_bool(invariant);
}
}

void c_typecheck_baset::typecheck_spec_decreases(codet &code)
{
if(code.find(ID_C_spec_decreases).is_not_nil())
{
exprt &variant = static_cast<exprt &>(code.add(ID_C_spec_decreases));

typecheck_expr(variant);
implicit_typecast_arithmetic(variant);
}
}
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)
return;
}

// fist do sub-nodes
// first do sub-nodes
typecheck_expr_operands(expr);

// now do case-split
Expand Down
28 changes: 23 additions & 5 deletions src/ansi-c/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,7 @@ extern char *yyansi_ctext;
%token TOK_CPROVER_FINALLY "__CPROVER_finally"
%token TOK_CPROVER_ID "__CPROVER_ID"
%token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant"
%token TOK_CPROVER_DECREASES "__CPROVER_decreases"
%token TOK_CPROVER_REQUIRES "__CPROVER_requires"
%token TOK_CPROVER_ENSURES "__CPROVER_ensures"
%token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
Expand Down Expand Up @@ -497,6 +498,13 @@ loop_invariant_opt:
{ $$=$3; }
;

cprover_decreases_opt:
/* nothing */
{ init($$); parser_stack($$).make_nil(); }
| TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
{ $$=$3; }
;

statement_expression: '(' compound_statement ')'
{
$$=$1;
Expand Down Expand Up @@ -2418,24 +2426,31 @@ declaration_or_expression_statement:

iteration_statement:
TOK_WHILE '(' comma_expression_opt ')'
loop_invariant_opt statement
loop_invariant_opt cprover_decreases_opt
statement
{
$$=$1;
statement($$, ID_while);
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($6)));
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));

if(parser_stack($5).is_not_nil())
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5));

if(parser_stack($6).is_not_nil())
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
}
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
loop_invariant_opt ';'
loop_invariant_opt cprover_decreases_opt ';'
{
$$=$1;
statement($$, ID_dowhile);
parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));

if(parser_stack($7).is_not_nil())
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($7));

if(parser_stack($8).is_not_nil())
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
}
| TOK_FOR
{
Expand All @@ -2449,7 +2464,7 @@ iteration_statement:
'(' declaration_or_expression_statement
comma_expression_opt ';'
comma_expression_opt ')'
loop_invariant_opt
loop_invariant_opt cprover_decreases_opt
statement
{
$$=$1;
Expand All @@ -2458,11 +2473,14 @@ iteration_statement:
mto($$, $4);
mto($$, $5);
mto($$, $7);
mto($$, $10);
mto($$, $11);

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

if(parser_stack($10).is_not_nil())
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));

if(PARSER.for_has_scope)
PARSER.pop_scope(); // remove the C99 for-scope
}
Expand Down
1 change: 1 addition & 0 deletions src/ansi-c/scanner.l
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1281,6 +1281,7 @@ __decltype { if(PARSER.cpp98 &&
{CPROVER_PREFIX}"finally" { loc(); return TOK_CPROVER_FINALLY; }
{CPROVER_PREFIX}"ID" { loc(); return TOK_CPROVER_ID; }
{CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; }
{CPROVER_PREFIX}"decreases" { loc(); return TOK_CPROVER_DECREASES; }
{CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; }
{CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; }
{CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; }
Expand Down
1 change: 1 addition & 0 deletions src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -572,6 +572,7 @@ IREP_ID_ONE(is_weak)
IREP_ID_ONE(used)
IREP_ID_ONE(is_used)
IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
IREP_ID_TWO(C_spec_decreases, #spec_decreases)
IREP_ID_TWO(C_spec_requires, #spec_requires)
IREP_ID_TWO(C_spec_ensures, #spec_ensures)
IREP_ID_TWO(C_spec_assigns, #spec_assigns)
Expand Down