Skip to content

Commit df7696e

Browse files
martin-csAalok Thakkar
martin-cs
authored and
Aalok Thakkar
committed
Parser support for assigns contracts on loops
1. Renamed cprover_contract_assigns_opt to cprover_contract_assigns. 2. Created cprover_contract_assigns_opt which has a unit production and cprover_contract_assigns. 3. Renamed cprover_decreases_opt to cprover_contract_decreases_opt. 4. Renamed loop_invariant to cprover_loop_invariant. 5. Renamed loop_invariant_list to cprover_loop_invariant_list. 6. Renamed loop_invariant_list_opt to cprover_loop_invariant_list_opt. 7. Added cprover_contract_assigns_opt to iteration statement. This adds parser support for assigns contracts on loops.
1 parent b35228a commit df7696e

File tree

9 files changed

+133
-28
lines changed

9 files changed

+133
-28
lines changed

‎regression/contracts/invar_assigns_alias_analysis/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
#define SIZE 8
5+
6+
struct blob { char *data; };
7+
8+
void main()
9+
{
10+
struct blob *b = malloc(sizeof(struct blob));
11+
b->data = malloc(SIZE);
12+
13+
b->data[5] = 0;
14+
for (unsigned i = 0; i < SIZE; i++)
15+
__CPROVER_assigns(b->data)
16+
__CPROVER_loop_invariant(i <= SIZE)
17+
{
18+
b->data[i] = 1;
19+
}
20+
21+
assert(b->data[5] == 0);
22+
}

‎regression/contracts/invar_assigns_alias_analysis/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
KNOWNBUG
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main.assertion.1\] .* assertion b->data[5] == 0: FAILURE$
9+
^VERIFICATION FAILED$
10+
--
11+
--
12+
This test shows a known bug in the current implementation
13+
for assigns clause. Fixing this is a part of future work.

‎regression/contracts/invar_assigns_opt/main.c

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int r1, s1 = 1;
6+
__CPROVER_assume(r1 >= 0);
7+
while(r1 > 0)
8+
// clang-format off
9+
__CPROVER_loop_invariant(r1 >= 0 && s1 == 1)
10+
__CPROVER_decreases(r1)
11+
// clang-format on
12+
{
13+
s1 = 1;
14+
r1--;
15+
}
16+
assert(r1 == 0);
17+
assert(s1 == 1);
18+
19+
int r2, s2 = 1;
20+
__CPROVER_assume(r2 >= 0);
21+
while(r2 > 0)
22+
// clang-format off
23+
__CPROVER_assigns(r2, s2)
24+
__CPROVER_loop_invariant(r2 >= 0 && s2 == 1)
25+
__CPROVER_decreases(r2)
26+
// clang-format on
27+
{
28+
s2 = 1;
29+
r2--;
30+
}
31+
assert(r2 == 0);
32+
assert(s2 == 1);
33+
34+
return 0;
35+
36+
}

‎regression/contracts/invar_assigns_opt/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$
9+
^\[main.assertion.2\] .* assertion s1 == 1: SUCCESS$
10+
^\[main.3\] .* Check loop invariant before entry: SUCCESS$
11+
^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
12+
^\[main.assertion.3\] .* assertion r2 == 0: SUCCESS$
13+
^\[main.assertion.4\] .* assertion s2 == 1: SUCCESS$
14+
^VERIFICATION SUCCESSFUL$
15+
--
16+
--
17+
This test checks that adding assigns clause is optional
18+
and that if a proof does not require it, then adding an
19+
appropriate assigns clause does not lead to any
20+
unexpected behavior.

‎regression/contracts/invar_check_multiple_loops/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,4 +27,4 @@ int main()
2727
assert(x == y + 2 * n);
2828

2929
return 0;
30-
}
30+
}

‎regression/contracts/invar_check_nested_loops/main.c

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

1717
while(a > 0)
1818
// clang-format off
19+
__CPROVER_assigns(s, a)
1920
__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
2021
__CPROVER_decreases(a)
2122
// clang-format on

‎regression/contracts/invar_dynamic_struct_member/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ void main()
99
t->x = 0;
1010

1111
unsigned n;
12-
for(unsigned i = 0; i < n; ++i)
12+
for(unsigned i = 0; i < n; ++i)
1313
__CPROVER_loop_invariant(i <= n)
1414
{
1515
switch(i % 4)

‎regression/contracts/invar_loop_constant_pass/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,4 @@ main.c
1010
^VERIFICATION SUCCESSFUL$
1111
--
1212
This test checks that the invariant is correctly used to satisfy
13-
all assertions that follow a loop.
13+
all assertions that follow a loop.

‎src/ansi-c/parser.y

Lines changed: 38 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -491,25 +491,26 @@ quantifier_expression:
491491
}
492492
;
493493

494-
loop_invariant:
494+
495+
cprover_loop_invariant:
495496
TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
496497
{ $$=$3; }
497498
;
498499

499-
loop_invariant_list:
500-
loop_invariant
500+
cprover_loop_invariant_list:
501+
cprover_loop_invariant
501502
{ init($$); mto($$, $1); }
502-
| loop_invariant_list loop_invariant
503+
| cprover_loop_invariant_list cprover_loop_invariant
503504
{ $$=$1; mto($$, $2); }
504505
;
505506

506-
loop_invariant_list_opt:
507+
cprover_loop_invariant_list_opt:
507508
/* nothing */
508509
{ init($$); parser_stack($$).make_nil(); }
509-
| loop_invariant_list
510+
| cprover_loop_invariant_list
510511
;
511512

512-
cprover_decreases_opt:
513+
cprover_contract_decreases_opt:
513514
/* nothing */
514515
{ init($$); parser_stack($$).make_nil(); }
515516
| TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
@@ -2437,31 +2438,35 @@ declaration_or_expression_statement:
24372438

24382439
iteration_statement:
24392440
TOK_WHILE '(' comma_expression_opt ')'
2440-
loop_invariant_list_opt cprover_decreases_opt
2441+
cprover_contract_assigns_opt
2442+
cprover_loop_invariant_list_opt
2443+
cprover_contract_decreases_opt
24412444
statement
24422445
{
24432446
$$=$1;
24442447
statement($$, ID_while);
2445-
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));
2448+
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
24462449

24472450
if(!parser_stack($5).operands().empty())
2448-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($5).operands());
2451+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
24492452

2450-
if(parser_stack($6).is_not_nil())
2451-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
2453+
if(parser_stack($7).is_not_nil())
2454+
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
24522455
}
24532456
| TOK_DO statement TOK_WHILE '(' comma_expression ')'
2454-
loop_invariant_list_opt cprover_decreases_opt ';'
2457+
cprover_contract_assigns_opt
2458+
cprover_loop_invariant_list_opt
2459+
cprover_contract_decreases_opt ';'
24552460
{
24562461
$$=$1;
24572462
statement($$, ID_dowhile);
24582463
parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
24592464

2460-
if(!parser_stack($7).operands().empty())
2461-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
2465+
if(!parser_stack($8).operands().empty())
2466+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
24622467

2463-
if(parser_stack($8).is_not_nil())
2464-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
2468+
if(parser_stack($9).is_not_nil())
2469+
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9));
24652470
}
24662471
| TOK_FOR
24672472
{
@@ -2475,7 +2480,9 @@ iteration_statement:
24752480
'(' declaration_or_expression_statement
24762481
comma_expression_opt ';'
24772482
comma_expression_opt ')'
2478-
loop_invariant_list_opt cprover_decreases_opt
2483+
cprover_contract_assigns_opt
2484+
cprover_loop_invariant_list_opt
2485+
cprover_contract_decreases_opt
24792486
statement
24802487
{
24812488
$$=$1;
@@ -2484,13 +2491,13 @@ iteration_statement:
24842491
mto($$, $4);
24852492
mto($$, $5);
24862493
mto($$, $7);
2487-
mto($$, $11);
2494+
mto($$, $12);
24882495

2489-
if(!parser_stack($9).operands().empty())
2490-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($9).operands());
2496+
if(!parser_stack($10).operands().empty())
2497+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
24912498

2492-
if(parser_stack($10).is_not_nil())
2493-
parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));
2499+
if(parser_stack($11).is_not_nil())
2500+
parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($11));
24942501

24952502
if(PARSER.for_has_scope)
24962503
PARSER.pop_scope(); // remove the C99 for-scope
@@ -3272,10 +3279,10 @@ cprover_function_contract:
32723279
set($$, ID_C_spec_requires);
32733280
mto($$, $3);
32743281
}
3275-
| cprover_contract_assigns_opt
3282+
| cprover_contract_assigns
32763283
;
32773284

3278-
cprover_contract_assigns_opt:
3285+
cprover_contract_assigns:
32793286
TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
32803287
{
32813288
$$=$1;
@@ -3291,6 +3298,12 @@ cprover_contract_assigns_opt:
32913298
}
32923299
;
32933300

3301+
cprover_contract_assigns_opt:
3302+
/* nothing */
3303+
{ init($$); parser_stack($$).make_nil(); }
3304+
| cprover_contract_assigns
3305+
;
3306+
32943307
cprover_function_contract_sequence:
32953308
cprover_function_contract
32963309
| cprover_function_contract_sequence cprover_function_contract

0 commit comments

Comments
 (0)