From c2f986fa102992d320992670106813fc0c6d77ce Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 10 Nov 2021 22:51:16 +0000 Subject: [PATCH 1/7] fix a bug with inclusion checking on havoc_object The write set inclusion check on havoc_object(ptr) only checked the inclusion of (ptr+0) in the write set, but performed havocing of the entire object (i.e., ptr+0 until ptr+OBJECT_SIZE(ptr)). The proposed change fixes this behavior and checks the inclusion of the entire object in the write set. --- regression/contracts/assigns_enforce_20/test.desc | 2 +- src/goto-instrument/contracts/contracts.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc index b8da1fa1031..1cca96c1c7f 100644 --- a/regression/contracts/assigns_enforce_20/test.desc +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6b1724a4c4f..a39996775fe 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -942,8 +942,8 @@ void code_contractst::check_frame_conditions( instruction_it->is_other() && instruction_it->get_other().get_statement() == ID_havoc_object) { - const exprt &havoc_argument = dereference_exprt( - to_typecast_expr(instruction_it->get_other().operands().front()).op()); + const auto havoc_argument = + pointer_object(instruction_it->get_other().operands().front()); add_inclusion_check(body, assigns, instruction_it, havoc_argument); } } From b5b8a5a26f94e50c0e3e1dd30f52689e6d727a00 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Mon, 8 Nov 2021 23:52:00 +0000 Subject: [PATCH 2/7] fix recording old variant value at the beginning of loop body The loop variant value is supposed to be recorded just after the loop head (i.e., at the beginning of the loop body). Previously this was done by computing std::next(loop_head). However, complex C loop guards could be compiled to multiple GOTO instructions and it might be necessarey to advance the loop_head multiple times. The proposed change advanced the loop_head instruction pointer until the source_location differs. This approach might still fail if the loop guard was split across multiple lines in the source file. --- .../main.c | 14 ++++++++++++++ .../test.desc | 19 +++++++++++++++++++ src/goto-instrument/contracts/contracts.cpp | 16 +++++++++++++++- 3 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 regression/contracts/variant_multi_instruction_loop_head/main.c create mode 100644 regression/contracts/variant_multi_instruction_loop_head/test.desc diff --git a/regression/contracts/variant_multi_instruction_loop_head/main.c b/regression/contracts/variant_multi_instruction_loop_head/main.c new file mode 100644 index 00000000000..705dd64d99a --- /dev/null +++ b/regression/contracts/variant_multi_instruction_loop_head/main.c @@ -0,0 +1,14 @@ +int main() +{ + int x = 0; + int *y = &x; + + while(*y <= 0 && *y < 10) + // clang-format off + __CPROVER_loop_invariant(1 == 1) + __CPROVER_decreases(10 - x) + // clang-format on + { + x++; + } +} diff --git a/regression/contracts/variant_multi_instruction_loop_head/test.desc b/regression/contracts/variant_multi_instruction_loop_head/test.desc new file mode 100644 index 00000000000..dfcc8fcf847 --- /dev/null +++ b/regression/contracts/variant_multi_instruction_loop_head/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--apply-loop-contracts +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails even without the fix proposed in the commit, so it should be improved. +It is expected to fail because the proposed invariant isn't strong enough to help prove +termination using the specified variant. + +The test highlights a case where a C loop guard is compiled to multiple GOTO instructions. +Therefore the loop_head pointer needs to be advanced multiple times to get to the loop body, +where the initial value of the loop variant (/ ranking function) must be recorded. + +The proposed fix advances the pointer until the source_location differs from the original +loop_head's source_location. However, this might still not work if the loop guard in the +original C code was split across multiple lines in the first place. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index a39996775fe..7a19116cb1e 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -209,7 +209,21 @@ void code_contractst::check_apply_loop_contracts( converter.goto_convert(old_decreases_assignment, havoc_code, mode); } - goto_function.body.destructive_insert(std::next(loop_head), havoc_code); + // Forward the loop_head iterator until the start of the body. + // This is necessary because complex C loop_head conditions could be + // converted to multiple GOTO instructions (e.g. temporaries are introduced). + // FIXME: This simple approach wouldn't work when + // the loop guard in the source file is split across multiple lines. + const auto head_loc = loop_head->source_location(); + while(loop_head->source_location() == head_loc) + loop_head = std::next(loop_head); + + // At this point, we are just past the loop head, + // so at the beginning of the loop body. + auto loop_body = loop_head; + loop_head--; + + goto_function.body.destructive_insert(loop_body, havoc_code); } // Generate: assert(invariant) just after the loop exits From 2499f8a2ba478f613292482dc7b35c8e7aa5729c Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 12 Nov 2021 20:43:25 +0000 Subject: [PATCH 3/7] reject contracts on do/while loops for now Whether the first (unguarded) loop iteration should be executed "before" the base case assertion or not is still under discussion. Loop contracts on do/while loops are rejected until this is resolved. --- .../contracts/loop_contracts_do_while/main.c | 13 +++++++++++++ .../contracts/loop_contracts_do_while/test.desc | 9 +++++++++ src/goto-instrument/contracts/contracts.cpp | 15 ++++++++------- 3 files changed, 30 insertions(+), 7 deletions(-) create mode 100644 regression/contracts/loop_contracts_do_while/main.c create mode 100644 regression/contracts/loop_contracts_do_while/test.desc diff --git a/regression/contracts/loop_contracts_do_while/main.c b/regression/contracts/loop_contracts_do_while/main.c new file mode 100644 index 00000000000..88477df7fc2 --- /dev/null +++ b/regression/contracts/loop_contracts_do_while/main.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int x = 0; + + do + { + x++; + } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10); + + assert(x == 10); +} diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc new file mode 100644 index 00000000000..488a91f377f --- /dev/null +++ b/regression/contracts/loop_contracts_do_while/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on do/while loops. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 7a19116cb1e..ddcbf167705 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -184,9 +184,14 @@ void code_contractst::check_apply_loop_contracts( new_decreases_vars.push_back(new_decreases_var); } - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) + // TODO: Fix loop contract handling for do/while loops. + if(loop_end->is_goto() && !loop_end->get_condition().is_true()) { + log.error() << "Loop contracts are unsupported on do/while loops: " + << loop_head->source_location() << messaget::eom; + throw 0; + + // non-deterministically skip the loop if it is a do-while loop. havoc_code.add(goto_programt::make_goto( loop_end, side_effect_expr_nondett(bool_typet(), loop_head->source_location()))); @@ -276,11 +281,7 @@ void code_contractst::check_apply_loop_contracts( // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume(); - - if(loop_head->is_goto()) - loop_end->set_condition(false_exprt()); - else - loop_end->set_condition(boolean_negate(loop_end->get_condition())); + loop_end->set_condition(boolean_negate(loop_end->get_condition())); } void code_contractst::add_quantified_variable( From e0da7e79c4611ffe0e1802fbcf411f0b47492b2c Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Mon, 8 Nov 2021 04:04:52 +0000 Subject: [PATCH 4/7] parsing, type checking & conversion of loop assigns clauses In this commit we implement the parsing actions, type checking and conversion routines for assigns clauses on loops. The syntax rules along with regressions tests were introduced in an earlier PR: #6196. --- .../assigns_enforce_address_of/test.desc | 2 +- .../assigns_enforce_elvis_4/test.desc | 2 +- .../assigns_enforce_function_calls/test.desc | 2 +- .../assigns_enforce_literal/test.desc | 2 +- .../assigns_enforce_side_effects_1/test.desc | 2 +- .../assigns_enforce_side_effects_2/test.desc | 2 +- .../assigns_enforce_side_effects_3/test.desc | 2 +- .../test.desc | 2 +- src/ansi-c/c_typecheck_base.cpp | 28 +---------- src/ansi-c/c_typecheck_base.h | 3 ++ src/ansi-c/c_typecheck_code.cpp | 50 +++++++++++++++++++ src/ansi-c/parser.y | 9 ++++ src/goto-programs/goto_convert.cpp | 20 +++++--- 13 files changed, 84 insertions(+), 42 deletions(-) diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 4c3cfa2b9b4..9e9033a30f9 100644 --- a/regression/contracts/assigns_enforce_address_of/test.desc +++ b/regression/contracts/assigns_enforce_address_of/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_elvis_4/test.desc b/regression/contracts/assigns_enforce_elvis_4/test.desc index 6504078edc2..b2f68af4a92 100644 --- a/regression/contracts/assigns_enforce_elvis_4/test.desc +++ b/regression/contracts/assigns_enforce_elvis_4/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: void-typed targets not permitted$ +^.*error: void-typed targets not permitted in assigns clause$ -- -- Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected. diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index f2547f2a9fb..a18e73b93cf 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 45e09d5d0da..e5fa1712864 100644 --- a/regression/contracts/assigns_enforce_literal/test.desc +++ b/regression/contracts/assigns_enforce_literal/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc index d6f3c98d246..57965527d2a 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: void-typed targets not permitted$ +^.*error: void-typed targets not permitted in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index 21ba293dd46..c0ee204ba71 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index 21ba293dd46..c0ee204ba71 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc index 2cdc55e7c5f..c77f85d72c7 100644 --- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc +++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -error: illegal target in assigns clause +error: non-lvalue target in assigns clause -- Checks whether type checking reports illegal target in assigns clause. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index c41bd51bbeb..1cad4a50b7b 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -739,33 +739,7 @@ void c_typecheck_baset::typecheck_declaration( CPROVER_PREFIX "loop_entry is not allowed in preconditions."); } - for(auto &target : code_type.assigns()) - { - typecheck_expr(target); - - if(target.type().id() == ID_empty) - { - error().source_location = target.source_location(); - error() << "void-typed targets not permitted" << eom; - throw 0; - } - else if(target.id() == ID_pointer_object) - { - // skip - } - else if(!target.get_bool(ID_C_lvalue)) - { - error().source_location = target.source_location(); - error() << "illegal target in assigns clause" << eom; - throw 0; - } - else if(has_subexpr(target, ID_side_effect)) - { - error().source_location = target.source_location(); - error() << "assigns clause is not side-effect free" << eom; - throw 0; - } - } + typecheck_spec_assigns(code_type.assigns()); if(!as_const(code_type).ensures().empty()) { diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 405940c81fe..1b92f0e633a 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -144,6 +144,9 @@ 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); + + // contracts + virtual void typecheck_spec_assigns(exprt::operandst &targets); virtual void typecheck_spec_loop_invariant(codet &code); virtual void typecheck_spec_decreases(codet &code); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 6fd492371ce..233cf3a1afc 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -493,6 +494,12 @@ void c_typecheck_baset::typecheck_for(codet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } } void c_typecheck_baset::typecheck_label(code_labelt &code) @@ -782,6 +789,12 @@ void c_typecheck_baset::typecheck_while(code_whilet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } } void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) @@ -816,6 +829,43 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } +} + +void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) +{ + for(auto &target : targets) + { + typecheck_expr(target); + + if(target.type().id() == ID_empty) + { + error().source_location = target.source_location(); + error() << "void-typed targets not permitted in assigns clause" << eom; + throw 0; + } + else if(target.id() == ID_pointer_object) + { + // skip + } + else if(!target.get_bool(ID_C_lvalue)) + { + error().source_location = target.source_location(); + error() << "non-lvalue target in assigns clause" << eom; + throw 0; + } + else if(has_subexpr(target, ID_side_effect)) + { + error().source_location = target.source_location(); + error() << "assigns clause is not side-effect free" << eom; + throw 0; + } + } } void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 6d9157f3633..17b2bf89be1 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -2453,6 +2453,9 @@ iteration_statement: statement($$, ID_while); 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_assigns)).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()); @@ -2468,6 +2471,9 @@ iteration_statement: 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_assigns)).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()); @@ -2499,6 +2505,9 @@ iteration_statement: mto($$, $7); mto($$, $12); + if(!parser_stack($9).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_assigns)).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()); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index dbbd5e226dc..d5ccf182cd9 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -863,11 +863,15 @@ void goto_convertt::convert_loop_contracts( goto_programt::targett loop, const irep_idt &mode) { - exprt invariant = - static_cast(code.find(ID_C_spec_loop_invariant)); - exprt decreases_clause = - static_cast(code.find(ID_C_spec_decreases)); + auto assigns = static_cast(code.find(ID_C_spec_assigns)); + if(assigns.is_not_nil()) + { + PRECONDITION(loop->is_goto()); + loop->guard.add(ID_C_spec_assigns).swap(assigns.op()); + } + auto invariant = + static_cast(code.find(ID_C_spec_loop_invariant)); if(!invariant.is_nil()) { if(has_subexpr(invariant, ID_side_effect)) @@ -880,6 +884,8 @@ void goto_convertt::convert_loop_contracts( loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant); } + auto decreases_clause = + static_cast(code.find(ID_C_spec_decreases)); if(!decreases_clause.is_nil()) { if(has_subexpr(decreases_clause, ID_side_effect)) @@ -972,7 +978,7 @@ void goto_convertt::convert_for( goto_programt::targett y = tmp_y.add( goto_programt::make_goto(u, true_exprt(), code.source_location())); - // loop invariant and decreases clause + // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(sideeffects); @@ -1030,7 +1036,7 @@ void goto_convertt::convert_while( goto_programt tmp_x; convert(code.body(), tmp_x, mode); - // loop invariant and decreases clause + // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_branch); @@ -1099,7 +1105,7 @@ void goto_convertt::convert_dowhile( // y: if(c) goto w; y->complete_goto(w); - // loop invariant and decreases clause + // assigns_clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_w); From 49a75bf4286c882a560bafcaec73d84bc703b6ad Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Tue, 9 Nov 2021 04:39:12 +0000 Subject: [PATCH 5/7] instrument loops per given assigns clauses --- .../assigns_enforce_arrays_05/test.desc | 2 +- .../invar_assigns_alias_analysis/test.desc | 14 -- .../contracts/invar_assigns_empty/main.c | 10 +- .../contracts/invar_assigns_empty/test.desc | 1 - .../contracts/invar_assigns_opt/test.desc | 18 +- .../test.desc | 7 +- .../main.c | 3 + .../test.desc | 14 +- .../test.desc | 7 +- regression/contracts/loop_assigns-01/main.c | 27 +++ .../contracts/loop_assigns-01/test.desc | 16 ++ regression/contracts/loop_assigns-02/main.c | 27 +++ .../contracts/loop_assigns-02/test.desc | 20 ++ regression/contracts/loop_assigns-03/main.c | 27 +++ .../contracts/loop_assigns-03/test.desc | 17 ++ regression/contracts/loop_assigns-04/main.c | 41 ++++ .../contracts/loop_assigns-04/test.desc | 18 ++ .../main.c | 1 - .../contracts/loop_assigns-fail/test.desc | 11 + .../test.desc | 3 +- src/goto-instrument/contracts/contracts.cpp | 214 +++++++++++++----- src/goto-instrument/contracts/contracts.h | 2 + src/goto-instrument/loop_utils.cpp | 4 + 23 files changed, 403 insertions(+), 101 deletions(-) delete mode 100644 regression/contracts/invar_assigns_alias_analysis/test.desc create mode 100644 regression/contracts/loop_assigns-01/main.c create mode 100644 regression/contracts/loop_assigns-01/test.desc create mode 100644 regression/contracts/loop_assigns-02/main.c create mode 100644 regression/contracts/loop_assigns-02/test.desc create mode 100644 regression/contracts/loop_assigns-03/main.c create mode 100644 regression/contracts/loop_assigns-03/test.desc create mode 100644 regression/contracts/loop_assigns-04/main.c create mode 100644 regression/contracts/loop_assigns-04/test.desc rename regression/contracts/{invar_assigns_alias_analysis => loop_assigns-fail}/main.c (92%) create mode 100644 regression/contracts/loop_assigns-fail/test.desc diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 4a485acff3f..4fe133f4914 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract assigns_ptr --enforce-contract assigns_range +--enforce-contract assigns_range ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_assigns_alias_analysis/test.desc b/regression/contracts/invar_assigns_alias_analysis/test.desc deleted file mode 100644 index 961be46b17c..00000000000 --- a/regression/contracts/invar_assigns_alias_analysis/test.desc +++ /dev/null @@ -1,14 +0,0 @@ -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 index ba05010b0a0..4a41b2ea796 100644 --- a/regression/contracts/invar_assigns_empty/main.c +++ b/regression/contracts/invar_assigns_empty/main.c @@ -2,14 +2,8 @@ int main() { - int r; - __CPROVER_assume(r >= 0); - while(r > 0) - __CPROVER_assigns() __CPROVER_loop_invariant(r >= 0) + while(1 == 1) + __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1) { - r--; } - assert(r == 0); - - return 0; } diff --git a/regression/contracts/invar_assigns_empty/test.desc b/regression/contracts/invar_assigns_empty/test.desc index 19eddb6eb55..69966423ea5 100644 --- a/regression/contracts/invar_assigns_empty/test.desc +++ b/regression/contracts/invar_assigns_empty/test.desc @@ -5,7 +5,6 @@ main.c ^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$ -- -- diff --git a/regression/contracts/invar_assigns_opt/test.desc b/regression/contracts/invar_assigns_opt/test.desc index e5e6d920973..da69d71761f 100644 --- a/regression/contracts/invar_assigns_opt/test.desc +++ b/regression/contracts/invar_assigns_opt/test.desc @@ -3,14 +3,16 @@ 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$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that s2 is assignable: SUCCESS$ +^\[main.\d+\] .* Check that r2 is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc index 174fa755423..1606615be95 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc @@ -18,4 +18,9 @@ to pass -- we should not mistakenly havoc the allocations, just their values. However, the `data[1][2][3] == 0` assertion is expected to fail since `data` is havoced. -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. +Blocked on #6326: +The assigns clause in this case would have an entire 3D space, +and some of it must be re-established, to the original objects +but with different values at certain locations, by the loop invariant. +However, currently we cannot restrict same_object for pointers +within loop invariants. diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c index 1717ab001d8..02f03ffa58f 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c @@ -17,7 +17,10 @@ void main() data[4][5][6] = 0; for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, data[4][5][6]) __CPROVER_loop_invariant(i <= SIZE) + // clang-format on { data[4][5][6] = 1; } diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc index f57ca4872a7..441b05eea40 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc @@ -1,12 +1,14 @@ -KNOWNBUG +CORE main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ -^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ ^VERIFICATION FAILED$ -- -- @@ -17,5 +19,3 @@ The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]` is havoced and the invariant does not reestablish its value. However, the `data[1][2][3] == 0` assertion is expected to pass -- we should not havoc the entire `data` array, if only a constant index if being modified. - -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc index 0e180ad0d42..ac12b40c298 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc @@ -19,4 +19,9 @@ We _could_ do a more precise analysis in future where we only havoc `data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be modified in the given loop. -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. +Blocked on #6326: +The assigns clause in this case would have an entire 2D grid, +and some of it must be re-established, to the original objects +but with different values at certain locations, by the loop invariant. +However, currently we cannot restrict same_object for pointers +within loop invariants. diff --git a/regression/contracts/loop_assigns-01/main.c b/regression/contracts/loop_assigns-01/main.c new file mode 100644 index 00000000000..896e34dace1 --- /dev/null +++ b/regression/contracts/loop_assigns-01/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(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-01/test.desc b/regression/contracts/loop_assigns-01/test.desc new file mode 100644 index 00000000000..8e242fd5b3d --- /dev/null +++ b/regression/contracts/loop_assigns-01/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. diff --git a/regression/contracts/loop_assigns-02/main.c b/regression/contracts/loop_assigns-02/main.c new file mode 100644 index 00000000000..d4b45140be3 --- /dev/null +++ b/regression/contracts/loop_assigns-02/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(i, b->data[i]) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc new file mode 100644 index 00000000000..e1ecdc4b04b --- /dev/null +++ b/regression/contracts/loop_assigns-02/test.desc @@ -0,0 +1,20 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +per the current semantics of the assigns clause -- it must model ALL memory +being assigned to by the loop, not just a single symbolic iteration. diff --git a/regression/contracts/loop_assigns-03/main.c b/regression/contracts/loop_assigns-03/main.c new file mode 100644 index 00000000000..d3b137376f3 --- /dev/null +++ b/regression/contracts/loop_assigns-03/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(__CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-03/test.desc b/regression/contracts/loop_assigns-03/test.desc new file mode 100644 index 00000000000..632e889b1b4 --- /dev/null +++ b/regression/contracts/loop_assigns-03/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: FAILURE$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +because `i` is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/loop_assigns-04/main.c b/regression/contracts/loop_assigns-04/main.c new file mode 100644 index 00000000000..26ac38f8a93 --- /dev/null +++ b/regression/contracts/loop_assigns-04/main.c @@ -0,0 +1,41 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + int y; + 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(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + + int x; + for(unsigned j = 0; j < i; j++) + // clang-format off + // y is not assignable by outer loop, so this should be flagged + __CPROVER_assigns(j, y, x, b->data[i]) + __CPROVER_loop_invariant(j <= i) + // clang-format on + { + x = b->data[j] * b->data[j]; + b->data[i] += x; + y += j; + } + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc new file mode 100644 index 00000000000..fef5d6e0572 --- /dev/null +++ b/regression/contracts/loop_assigns-04/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that y is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +because `i` is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/invar_assigns_alias_analysis/main.c b/regression/contracts/loop_assigns-fail/main.c similarity index 92% rename from regression/contracts/invar_assigns_alias_analysis/main.c rename to regression/contracts/loop_assigns-fail/main.c index d2a81998022..43f17c4bf7c 100644 --- a/regression/contracts/invar_assigns_alias_analysis/main.c +++ b/regression/contracts/loop_assigns-fail/main.c @@ -16,7 +16,6 @@ void main() 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 { diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc new file mode 100644 index 00000000000..b1f4751987d --- /dev/null +++ b/regression/contracts/loop_assigns-fail/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +activate-multi-line-match +Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN! +^EXIT=6$ +^SIGNAL=0$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`. diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc index be05a219c40..4af9a7823c3 100644 --- a/regression/contracts/variant_missing_invariant_warning/test.desc +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -1,7 +1,8 @@ CORE main.c --apply-loop-contracts -^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$ +activate-multi-line-match +^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$ ^\[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$ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ddcbf167705..e2e310a0fd3 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -30,6 +30,7 @@ Date: February 2016 #include #include #include +#include #include #include #include @@ -41,6 +42,7 @@ Date: February 2016 #include "utils.h" void code_contractst::check_apply_loop_contracts( + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, @@ -57,23 +59,29 @@ void code_contractst::check_apply_loop_contracts( t->location_number > loop_end->location_number) loop_end = t; - // see whether we have an invariant and a decreases clause + // check for assigns, invariant, and decreases clauses + auto assigns = static_cast( + loop_end->get_condition().find(ID_C_spec_assigns)); auto invariant = static_cast( loop_end->get_condition().find(ID_C_spec_loop_invariant)); auto decreases_clause = static_cast( loop_end->get_condition().find(ID_C_spec_decreases)); + assigns_clauset loop_assigns( + assigns.operands(), log, ns, function_name, symbol_table); + if(invariant.is_nil()) { - if(decreases_clause.is_nil()) + if(decreases_clause.is_nil() && assigns.is_nil()) return; else { invariant = true_exprt(); log.warning() << "The loop at " << loop_head->source_location().as_string() - << " does not have a loop invariant, but has a decreases clause. " - << "Hence, a default loop invariant ('true') is being used." + << " does not have an invariant, but has other clauses" + << " specified in its contract.\n" + << "Hence, a default invariant ('true') is being used to prove those." << messaget::eom; } } @@ -97,23 +105,20 @@ void code_contractst::check_apply_loop_contracts( // to // initialize loop_entry variables; // H: assert(invariant); + // snapshot(write_set); // havoc; // assume(invariant); // if(guard) goto E: - // old_decreases_value = decreases_clause(current_environment); - // loop; - // new_decreases_value = decreases_clause(current_environment); + // old_decreases_value = decreases_clause_expr; + // loop with optional write_set inclusion checks; + // new_decreases_value = decreases_clause_expr; // assert(invariant); // assert(new_decreases_value < old_decreases_value); // assume(false); // E: ... - // find out what can get changed in the loop - modifiest modifies; - get_modifies(local_may_alias, loop, modifies); - - // build the havocking code - goto_programt havoc_code; + // an intermediate goto_program to store generated instructions + goto_programt generated_code; // process quantified variables correctly (introduce a fresh temporary) // and return a copy of the invariant @@ -133,11 +138,11 @@ void code_contractst::check_apply_loop_contracts( parameter2history, loop_head->source_location(), mode, - havoc_code, + generated_code, ID_loop_entry); // Create 'loop_entry' history variables - insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code); + insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); // Generate: assert(invariant) just before the loop // We use a block scope to create a temporary assertion, @@ -145,14 +150,46 @@ void code_contractst::check_apply_loop_contracts( { code_assertt assertion{invariant_expr()}; assertion.add_source_location() = loop_head->source_location(); - converter.goto_convert(assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert(assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check loop invariant before entry"); } // havoc the variables that may be modified - havoc_if_validt havoc_gen(modifies, ns); - havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code); + modifiest modifies; + if(assigns.is_nil()) + { + try + { + get_modifies(local_may_alias, loop, modifies); + } + catch(const analysis_exceptiont &exc) + { + log.error() << "Failed to infer variables being modified by the loop at " + << loop_head->source_location() + << ".\nPlease specify an assigns clause.\nReason:" + << messaget::eom; + throw exc; + } + } + else + { + for(const auto &target : assigns.operands()) + modifies.insert(target); + + // create snapshots of the CARs -- must be done before havocing + for(const auto &car : loop_assigns.get_write_set()) + { + auto snapshot_instructions = car.generate_snapshot_instructions(); + insert_before_swap_and_advance( + goto_function.body, loop_head, snapshot_instructions); + }; + } + + havoc_assigns_targetst havoc_gen(modifies, ns); + havoc_gen.append_full_havoc_code( + loop_head->source_location(), generated_code); + insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); // Generate: assume(invariant) just after havocing // We use a block scope to create a temporary assumption, @@ -160,7 +197,7 @@ void code_contractst::check_apply_loop_contracts( { code_assumet assumption{invariant_expr()}; assumption.add_source_location() = loop_head->source_location(); - converter.goto_convert(assumption, havoc_code, mode); + converter.goto_convert(assumption, generated_code, mode); } // Create fresh temporary variables that store the multidimensional @@ -171,7 +208,7 @@ void code_contractst::check_apply_loop_contracts( new_tmp_symbol( clause.type(), loop_head->source_location(), mode, symbol_table) .symbol_expr(); - havoc_code.add(goto_programt::make_decl( + generated_code.add(goto_programt::make_decl( old_decreases_var, loop_head->source_location())); old_decreases_vars.push_back(old_decreases_var); @@ -179,7 +216,7 @@ void code_contractst::check_apply_loop_contracts( new_tmp_symbol( clause.type(), loop_head->source_location(), mode, symbol_table) .symbol_expr(); - havoc_code.add(goto_programt::make_decl( + generated_code.add(goto_programt::make_decl( new_decreases_var, loop_head->source_location())); new_decreases_vars.push_back(new_decreases_var); } @@ -192,17 +229,44 @@ void code_contractst::check_apply_loop_contracts( throw 0; // non-deterministically skip the loop if it is a do-while loop. - havoc_code.add(goto_programt::make_goto( + generated_code.add(goto_programt::make_goto( loop_end, side_effect_expr_nondett(bool_typet(), loop_head->source_location()))); } - // Now havoc at the loop head. + // Assume invariant & decl the variant temporaries (just before loop guard). // Use insert_before_swap to preserve jumps to loop head. - insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code); + insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + + // Forward the loop_head iterator until the start of the body. + // This is necessary because complex C loop_head conditions could be + // converted to multiple GOTO instructions (e.g. temporaries are introduced). + // FIXME: This simple approach wouldn't work when + // the loop guard in the source file is split across multiple lines. + const auto head_loc = loop_head->source_location(); + while(loop_head->source_location() == head_loc) + loop_head++; + + // At this point, we are just past the loop head, + // so at the beginning of the loop body. + auto loop_body = loop_head; + loop_head--; + + // Perform write set instrumentation before adding anything else to loop body. + // Copy the loop_body as we would increment the iterator while instrumenting. + if(assigns.is_not_nil()) + { + auto copy_loop_body = loop_body; + check_frame_conditions( + function_name, + goto_function.body, + copy_loop_body, + loop_end, + loop_assigns); + } // Generate: assignments to store the multidimensional decreases clause's - // value before the loop + // value just before the loop body (but just after the loop guard) if(!decreases_clause.is_nil()) { for(size_t i = 0; i < old_decreases_vars.size(); i++) @@ -211,24 +275,10 @@ void code_contractst::check_apply_loop_contracts( decreases_clause_exprs[i]}; old_decreases_assignment.add_source_location() = loop_head->source_location(); - converter.goto_convert(old_decreases_assignment, havoc_code, mode); + converter.goto_convert(old_decreases_assignment, generated_code, mode); } - // Forward the loop_head iterator until the start of the body. - // This is necessary because complex C loop_head conditions could be - // converted to multiple GOTO instructions (e.g. temporaries are introduced). - // FIXME: This simple approach wouldn't work when - // the loop guard in the source file is split across multiple lines. - const auto head_loc = loop_head->source_location(); - while(loop_head->source_location() == head_loc) - loop_head = std::next(loop_head); - - // At this point, we are just past the loop head, - // so at the beginning of the loop body. - auto loop_body = loop_head; - loop_head--; - - goto_function.body.destructive_insert(loop_body, havoc_code); + goto_function.body.destructive_insert(loop_body, generated_code); } // Generate: assert(invariant) just after the loop exits @@ -237,8 +287,8 @@ void code_contractst::check_apply_loop_contracts( { code_assertt assertion{invariant_expr()}; assertion.add_source_location() = loop_end->source_location(); - converter.goto_convert(assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert(assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check that loop invariant is preserved"); } @@ -252,7 +302,7 @@ void code_contractst::check_apply_loop_contracts( decreases_clause_exprs[i]}; new_decreases_assignment.add_source_location() = loop_head->source_location(); - converter.goto_convert(new_decreases_assignment, havoc_code, mode); + converter.goto_convert(new_decreases_assignment, generated_code, mode); } // Generate: assertion that the multidimensional decreases clause's value @@ -263,21 +313,22 @@ void code_contractst::check_apply_loop_contracts( new_decreases_vars, old_decreases_vars)}; monotonic_decreasing_assertion.add_source_location() = loop_head->source_location(); - converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert( + monotonic_decreasing_assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check decreases clause on loop iteration"); // Discard the temporary variables that store decreases clause's value for(size_t i = 0; i < old_decreases_vars.size(); i++) { - havoc_code.add(goto_programt::make_dead( + generated_code.add(goto_programt::make_dead( old_decreases_vars[i], loop_head->source_location())); - havoc_code.add(goto_programt::make_dead( + generated_code.add(goto_programt::make_dead( new_decreases_vars[i], loop_head->source_location())); } } - insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code); + insert_before_swap_and_advance(goto_function.body, loop_end, generated_code); // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume(); @@ -613,22 +664,64 @@ bool code_contractst::apply_function_contract( } void code_contractst::apply_loop_contract( - const irep_idt &function, + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function) { local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); - // Iterate over the (natural) loops in the function, - // and apply any invariant annotations that we find. + // A graph node type that stores information about a loop. + // We create a DAG representing nesting of various loops in goto_function, + // sort them topologically, and instrument them in the top-sorted order. + // + // The goal here is not avoid explicit "subset checks" on nested write sets. + // When instrumenting in a top-sorted order, + // the outer loop would no longer observe the inner loop's write set, + // but only corresponding `havoc` statements, + // which can be instrumented in the usual way to achieve a "subset check". + + struct loop_graph_nodet : public graph_nodet + { + typedef const goto_programt::targett &targett; + typedef const typename natural_loops_mutablet::loopt &loopt; + + targett target; + loopt loop; + + loop_graph_nodet(targett t, loopt l) : target(t), loop(l) + { + } + }; + grapht loop_nesting_graph; + for(const auto &loop : natural_loops.loop_map) + loop_nesting_graph.add_node(loop.first, loop.second); + + for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer) + { + for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner) + { + if(inner == outer) + continue; + + if(loop_nesting_graph[outer].loop.contains( + loop_nesting_graph[inner].target)) + loop_nesting_graph.add_edge(outer, inner); + } + } + + // Iterate over the (natural) loops in the function, in topo-sorted order, + // and apply any loop contracts that we find. + for(const auto &idx : loop_nesting_graph.topsort()) { + const auto &loop_node = loop_nesting_graph[idx]; check_apply_loop_contracts( + function_name, goto_function, local_may_alias, - loop.first, - loop.second, - symbol_table.lookup_ref(function).mode); + loop_node.target, + loop_node.loop, + symbol_table.lookup_ref(function_name).mode); } } @@ -890,7 +983,11 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) // Insert aliasing assertions check_frame_conditions( - function_obj->first, function_obj->second.body, instruction_it, assigns); + function_obj->first, + function_obj->second.body, + instruction_it, + function_obj->second.body.instructions.end(), + assigns); return false; } @@ -899,11 +996,12 @@ void code_contractst::check_frame_conditions( const irep_idt &function, goto_programt &body, goto_programt::targett &instruction_it, + const goto_programt::targett &instruction_end, assigns_clauset &assigns) { goto_function_inline(goto_functions, function, ns, log.get_message_handler()); - for(; instruction_it != body.instructions.end(); ++instruction_it) + for(; instruction_it != instruction_end; ++instruction_it) { if(instruction_it->is_decl()) { diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index bd79f6e3b7c..b1c0e00909c 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -98,6 +98,7 @@ class code_contractst void apply_loop_contracts(); void check_apply_loop_contracts( + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, @@ -131,6 +132,7 @@ class code_contractst const irep_idt &, goto_programt &, goto_programt::targett &, + const goto_programt::targett &, assigns_clauset &); /// Inserts an assertion into the goto program to ensure that diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 25a50e3cb34..a488c4ae738 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -51,6 +51,10 @@ void get_modifies_lhs( for(const auto &mod : local_may_alias.get(t, ptr.pointer)) { const typecast_exprt typed_mod{mod, ptr.pointer.type()}; + if(mod.id() == ID_unknown) + { + throw analysis_exceptiont("Alias analysis returned UNKNOWN!"); + } if(ptr.offset.is_nil()) modifies.insert(dereference_exprt{typed_mod}); else From cec18baeb190058e5fac6584f3af189fee25acaa Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 12 Nov 2021 00:21:55 +0000 Subject: [PATCH 6/7] remove repeated inclusion checks in nested loops This commit introduces a new internal pragma, called `contracts:disable:assigns-check`, and annotates statements that have already been instrumented with inclusion checks to avoid instrumenting them again. --- src/goto-instrument/contracts/assigns.cpp | 4 ++ src/goto-instrument/contracts/contracts.cpp | 43 +++++++++++++++++---- src/goto-instrument/contracts/utils.cpp | 15 +++++++ src/goto-instrument/contracts/utils.h | 16 ++++++++ 4 files changed, 70 insertions(+), 8 deletions(-) diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index c79354e9621..ac87d9c4a35 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -117,6 +117,10 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() location)); instructions.destructive_append(skip_program); + + // The assignments above are only performed on locally defined temporaries + // and need not be checked for inclusion in the enclosing scope's write set. + add_pragma_disable_assigns_check(instructions); return instructions; } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index e2e310a0fd3..ccf6167d073 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -141,9 +141,6 @@ void code_contractst::check_apply_loop_contracts( generated_code, ID_loop_entry); - // Create 'loop_entry' history variables - insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); - // Generate: assert(invariant) just before the loop // We use a block scope to create a temporary assertion, // and immediately convert it to goto instructions. @@ -155,6 +152,14 @@ void code_contractst::check_apply_loop_contracts( "Check loop invariant before entry"); } + // Add 'loop_entry' history variables and base case assertion. + // These variables are local and thus + // need not be checked against the enclosing scope's write set. + insert_before_swap_and_advance( + goto_function.body, + loop_head, + add_pragma_disable_assigns_check(generated_code)); + // havoc the variables that may be modified modifiest modifies; if(assigns.is_nil()) @@ -177,7 +182,8 @@ void code_contractst::check_apply_loop_contracts( for(const auto &target : assigns.operands()) modifies.insert(target); - // create snapshots of the CARs -- must be done before havocing + // Create snapshots of write set CARs. + // This must be done before havocing the write set. for(const auto &car : loop_assigns.get_write_set()) { auto snapshot_instructions = car.generate_snapshot_instructions(); @@ -189,7 +195,17 @@ void code_contractst::check_apply_loop_contracts( havoc_assigns_targetst havoc_gen(modifies, ns); havoc_gen.append_full_havoc_code( loop_head->source_location(), generated_code); - insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + + // Add the havocing code, but only check against the enclosing scope's + // write set if it was manually specified. + if(assigns.is_nil()) + insert_before_swap_and_advance( + goto_function.body, + loop_head, + add_pragma_disable_assigns_check(generated_code)); + else + insert_before_swap_and_advance( + goto_function.body, loop_head, generated_code); // Generate: assume(invariant) just after havocing // We use a block scope to create a temporary assumption, @@ -744,7 +760,6 @@ void code_contractst::instrument_assign_statement( instruction_it->is_assign(), "The first instruction of instrument_assign_statement should always be" " an assignment"); - add_inclusion_check( program, assigns_clause, instruction_it, instruction_it->assign_lhs()); } @@ -834,7 +849,9 @@ void code_contractst::instrument_call_statement( alias_checking_instructions.destructive_append(skip_program); insert_before_swap_and_advance( - body, instruction_it, alias_checking_instructions); + body, + instruction_it, + add_pragma_disable_assigns_check(alias_checking_instructions)); // move past the call and then insert the invalidation instructions instruction_it++; @@ -866,7 +883,9 @@ void code_contractst::instrument_call_statement( invalidation_instructions.destructive_append(skip_program); insert_before_swap_and_advance( - body, instruction_it, invalidation_instructions); + body, + instruction_it, + add_pragma_disable_assigns_check(invalidation_instructions)); instruction_it--; } @@ -1003,6 +1022,14 @@ void code_contractst::check_frame_conditions( for(; instruction_it != instruction_end; ++instruction_it) { + const auto &pragmas = instruction_it->source_location().get_pragmas(); + if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end()) + continue; + + // Do not instrument this instruction again in the future, + // since we are going to instrument it now below. + add_pragma_disable_assigns_check(*instruction_it); + if(instruction_it->is_decl()) { // grab the declared symbol diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index b1c199229d5..c39cf81da43 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -14,6 +14,21 @@ Date: September 2021 #include #include +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr) +{ + instr.source_location_nonconst().add_pragma( + CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK); + return instr; +} + +goto_programt &add_pragma_disable_assigns_check(goto_programt &prog) +{ + Forall_goto_program_instructions(it, prog) + add_pragma_disable_assigns_check(*it); + return prog; +} + static void append_safe_havoc_code_for_expr( const source_locationt location, const namespacet &ns, diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 3be8c8f965d..70b691aec66 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -17,6 +17,8 @@ Date: September 2021 #include +#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" + /// \brief A class that overrides the low-level havocing functions in the base /// utility class, to havoc only when expressions point to valid memory, /// i.e. if all dereferences within an expression are valid @@ -42,6 +44,20 @@ class havoc_if_validt : public havoc_utilst const namespacet &ns; }; +/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking. +/// +/// \param instr: A mutable reference to the GOTO instruction. +/// \return The same reference after mutation (i.e., adding the pragma). +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr); + +/// \brief Adds pragmas on all instructions in a GOTO program +/// to disable inclusion checking on them. +/// +/// \param prog: A mutable reference to the GOTO program. +/// \return The same reference after mutation (i.e., adding the pragmas). +goto_programt &add_pragma_disable_assigns_check(goto_programt &prog); + /// \brief Generate a validity check over all dereferences in an expression /// /// This function generates a formula: From 2a9e3e25943ed24555d5bd1e7ef71dd5eb9df844 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 19 Nov 2021 18:08:47 +0000 Subject: [PATCH 7/7] minor improvements to assigns clause checking --- src/goto-instrument/contracts/contracts.cpp | 16 ++++------------ src/goto-instrument/contracts/contracts.h | 2 +- 2 files changed, 5 insertions(+), 13 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ccf6167d073..4cb4af3d077 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -179,8 +179,7 @@ void code_contractst::check_apply_loop_contracts( } else { - for(const auto &target : assigns.operands()) - modifies.insert(target); + modifies.insert(assigns.operands().cbegin(), assigns.operands().cend()); // Create snapshots of write set CARs. // This must be done before havocing the write set. @@ -269,16 +268,10 @@ void code_contractst::check_apply_loop_contracts( loop_head--; // Perform write set instrumentation before adding anything else to loop body. - // Copy the loop_body as we would increment the iterator while instrumenting. if(assigns.is_not_nil()) { - auto copy_loop_body = loop_body; check_frame_conditions( - function_name, - goto_function.body, - copy_loop_body, - loop_end, - loop_assigns); + function_name, goto_function.body, loop_body, loop_end, loop_assigns); } // Generate: assignments to store the multidimensional decreases clause's @@ -654,8 +647,7 @@ bool code_contractst::apply_function_contract( // Havoc all targets in the write set modifiest modifies; - for(const auto &target : targets.operands()) - modifies.insert(target); + modifies.insert(targets.operands().cbegin(), targets.operands().cend()); goto_programt assigns_havoc; havoc_assigns_targetst havoc_gen(modifies, ns); @@ -1014,7 +1006,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) void code_contractst::check_frame_conditions( const irep_idt &function, goto_programt &body, - goto_programt::targett &instruction_it, + goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, assigns_clauset &assigns) { diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index b1c0e00909c..08cc0080571 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -131,7 +131,7 @@ class code_contractst void check_frame_conditions( const irep_idt &, goto_programt &, - goto_programt::targett &, + goto_programt::targett, const goto_programt::targett &, assigns_clauset &);