diff --git a/regression/contracts/invar_assigns_alias_analysis/main.c b/regression/contracts/invar_assigns_alias_analysis/main.c new file mode 100644 index 00000000000..d2a81998022 --- /dev/null +++ b/regression/contracts/invar_assigns_alias_analysis/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + + b->data[5] = 0; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(b->data) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/invar_assigns_alias_analysis/test.desc b/regression/contracts/invar_assigns_alias_analysis/test.desc new file mode 100644 index 00000000000..961be46b17c --- /dev/null +++ b/regression/contracts/invar_assigns_alias_analysis/test.desc @@ -0,0 +1,14 @@ +KNOWNBUG +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion b->data[5] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test shows the need for assigns clauses. Currently we only +parse the assigns clause for loops, but there is no implementation +to actually enforce them. In the future, we will add this feature. diff --git a/regression/contracts/invar_assigns_empty/main.c b/regression/contracts/invar_assigns_empty/main.c new file mode 100644 index 00000000000..ba05010b0a0 --- /dev/null +++ b/regression/contracts/invar_assigns_empty/main.c @@ -0,0 +1,15 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_assigns() __CPROVER_loop_invariant(r >= 0) + { + r--; + } + assert(r == 0); + + return 0; +} diff --git a/regression/contracts/invar_assigns_empty/test.desc b/regression/contracts/invar_assigns_empty/test.desc new file mode 100644 index 00000000000..19eddb6eb55 --- /dev/null +++ b/regression/contracts/invar_assigns_empty/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that empty assigns clause is supported +in loop contracts. diff --git a/regression/contracts/invar_assigns_opt/main.c b/regression/contracts/invar_assigns_opt/main.c new file mode 100644 index 00000000000..b3f5ca1769b --- /dev/null +++ b/regression/contracts/invar_assigns_opt/main.c @@ -0,0 +1,26 @@ +#include + +int main() +{ + int r1, s1 = 1; + __CPROVER_assume(r1 >= 0); + while(r1 > 0) + __CPROVER_loop_invariant(r1 >= 0 && s1 == 1) __CPROVER_decreases(r1) + { + s1 = 1; + r1--; + } + assert(r1 == 0); + + int r2, s2 = 1; + __CPROVER_assume(r2 >= 0); + while(r2 > 0) + __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1) + __CPROVER_decreases(r2) + { + s2 = 1; + r2--; + } + assert(r2 == 0); + return 0; +} diff --git a/regression/contracts/invar_assigns_opt/test.desc b/regression/contracts/invar_assigns_opt/test.desc new file mode 100644 index 00000000000..e5e6d920973 --- /dev/null +++ b/regression/contracts/invar_assigns_opt/test.desc @@ -0,0 +1,20 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$ +^\[main.4\] .* Check loop invariant before entry: SUCCESS$ +^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.2\] .* assertion r2 == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that adding assigns clause is optional +and that if a proof does not require it, then adding an +appropriate assigns clause does not lead to any +unexpected behavior. diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 304bf0b329e..ab444152907 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -491,25 +491,25 @@ quantifier_expression: } ; -loop_invariant: +cprover_contract_loop_invariant: TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')' { $$=$3; } ; -loop_invariant_list: - loop_invariant +cprover_contract_loop_invariant_list: + cprover_contract_loop_invariant { init($$); mto($$, $1); } - | loop_invariant_list loop_invariant + | cprover_contract_loop_invariant_list cprover_contract_loop_invariant { $$=$1; mto($$, $2); } ; -loop_invariant_list_opt: +cprover_contract_loop_invariant_list_opt: /* nothing */ { init($$); parser_stack($$).make_nil(); } - | loop_invariant_list + | cprover_contract_loop_invariant_list ; -cprover_decreases_opt: +cprover_contract_decreases_opt: /* nothing */ { init($$); parser_stack($$).make_nil(); } | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')' @@ -2437,31 +2437,35 @@ declaration_or_expression_statement: iteration_statement: TOK_WHILE '(' comma_expression_opt ')' - loop_invariant_list_opt cprover_decreases_opt + cprover_contract_assigns_opt + cprover_contract_loop_invariant_list_opt + cprover_contract_decreases_opt statement { $$=$1; statement($$, ID_while); - parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7))); + parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8))); - if(!parser_stack($5).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($5).operands()); + if(!parser_stack($6).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands()); - if(parser_stack($6).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6)); + if(parser_stack($7).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7)); } | TOK_DO statement TOK_WHILE '(' comma_expression ')' - loop_invariant_list_opt cprover_decreases_opt ';' + cprover_contract_assigns_opt + cprover_contract_loop_invariant_list_opt + cprover_contract_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).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands()); + if(!parser_stack($8).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands()); - if(parser_stack($8).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8)); + if(parser_stack($9).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9)); } | TOK_FOR { @@ -2475,7 +2479,9 @@ iteration_statement: '(' declaration_or_expression_statement comma_expression_opt ';' comma_expression_opt ')' - loop_invariant_list_opt cprover_decreases_opt + cprover_contract_assigns_opt + cprover_contract_loop_invariant_list_opt + cprover_contract_decreases_opt statement { $$=$1; @@ -2484,13 +2490,13 @@ iteration_statement: mto($$, $4); mto($$, $5); mto($$, $7); - mto($$, $11); + mto($$, $12); - if(!parser_stack($9).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($9).operands()); + if(!parser_stack($10).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands()); - if(parser_stack($10).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10)); + if(parser_stack($11).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11)); if(PARSER.for_has_scope) PARSER.pop_scope(); // remove the C99 for-scope @@ -3272,10 +3278,10 @@ cprover_function_contract: set($$, ID_C_spec_requires); mto($$, $3); } - | cprover_contract_assigns_opt + | cprover_contract_assigns ; -cprover_contract_assigns_opt: +cprover_contract_assigns: TOK_CPROVER_ASSIGNS '(' argument_expression_list ')' { $$=$1; @@ -3291,6 +3297,12 @@ cprover_contract_assigns_opt: } ; +cprover_contract_assigns_opt: + /* nothing */ + { init($$); parser_stack($$).make_nil(); } + | cprover_contract_assigns + ; + cprover_function_contract_sequence: cprover_function_contract | cprover_function_contract_sequence cprover_function_contract