diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc index 47c33e05abe..2ef3cb314e6 100644 --- a/regression/contracts/invar_check_nested_loops/test.desc +++ b/regression/contracts/invar_check_nested_loops/test.desc @@ -9,9 +9,9 @@ main.c ^\[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.assigns.\d+] line 23 Check that s is assignable: SUCCESS$ -^\[main.assigns.\d+] line 24 Check that a is assignable: SUCCESS$ -^\[main.assigns.\d+] line 27 Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+] .* line 23 Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+] .* line 24 Check that a is assignable: SUCCESS$ +^\[main.assigns.\d+] .* line 27 Check that s is assignable: SUCCESS$ ^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/loop_contracts_reject_overlapping_loops/main.c b/regression/contracts/loop_contracts_reject_overlapping_loops/main.c new file mode 100644 index 00000000000..92a3ad463a5 --- /dev/null +++ b/regression/contracts/loop_contracts_reject_overlapping_loops/main.c @@ -0,0 +1,19 @@ +#include + +int main() +{ + int i = 0, j = 0, k = 0; + + while(j < 10) + { + while(k < 10) + __CPROVER_loop_invariant(1 == 1) + { + while(i < 10) + { + i++; + } + } + j++; + } +} diff --git a/regression/contracts/loop_contracts_reject_overlapping_loops/test.desc b/regression/contracts/loop_contracts_reject_overlapping_loops/test.desc new file mode 100644 index 00000000000..1d58d3ce690 --- /dev/null +++ b/regression/contracts/loop_contracts_reject_overlapping_loops/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +activate-multi-line-match +Inner loop at: file main.c line 12 function main does not have contracts, but an enclosing loop does.\nPlease provide contracts for this loop, or unwind it first. +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test checks that our instrumentation routines verify that inner loops +either have contracts or are unwound, if any enclosing loop has contracts. diff --git a/regression/contracts/loop_guard_with_side_effects/main.c b/regression/contracts/loop_guard_with_side_effects/main.c new file mode 100644 index 00000000000..868e83cd1c7 --- /dev/null +++ b/regression/contracts/loop_guard_with_side_effects/main.c @@ -0,0 +1,29 @@ +#include +#include +#include + +bool check(unsigned *i, unsigned *j, unsigned *k) +{ + (*j)++; + return *i < *k; +} + +int main() +{ + unsigned i, j, k; + __CPROVER_assume(k < UINT_MAX); + + i = j = 0; + + while(check(&i, &j, &k)) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i == j && i <= k) + // clang-format on + { + i++; + } + + assert(i == k); + assert(j == k + 1); +} diff --git a/regression/contracts/loop_guard_with_side_effects/test.desc b/regression/contracts/loop_guard_with_side_effects/test.desc new file mode 100644 index 00000000000..e3a78a23c69 --- /dev/null +++ b/regression/contracts/loop_guard_with_side_effects/test.desc @@ -0,0 +1,26 @@ +CORE +main.c +--apply-loop-contracts _ --unsigned-overflow-check +\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$ +\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS +\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS +\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$ +\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ +\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that j is valid: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS +\[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$ +\[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in k \+ \(unsigned int\)1: SUCCESS +\[main.assertion\.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test demonstrates a case where the loop guard has side effects. +The loop contracts must specify the state of all modified variables, +including those in the loop guard. diff --git a/regression/contracts/loop_guard_with_side_effects_fail/main.c b/regression/contracts/loop_guard_with_side_effects_fail/main.c new file mode 100644 index 00000000000..7af53a31386 --- /dev/null +++ b/regression/contracts/loop_guard_with_side_effects_fail/main.c @@ -0,0 +1,26 @@ +#include +#include + +bool check(unsigned *i, unsigned *j, unsigned *k) +{ + (*j)++; + return *i < *k; +} + +int main() +{ + unsigned i, j, k; + + i = j = 0; + + while(check(&i, &j, &k)) + // clang-format off + __CPROVER_assigns(i) + __CPROVER_loop_invariant(0 <= i && i <= k) + // clang-format on + { + i++; + } + + assert(i == k); +} diff --git a/regression/contracts/loop_guard_with_side_effects_fail/test.desc b/regression/contracts/loop_guard_with_side_effects_fail/test.desc new file mode 100644 index 00000000000..014e3a92850 --- /dev/null +++ b/regression/contracts/loop_guard_with_side_effects_fail/test.desc @@ -0,0 +1,20 @@ +CORE +main.c +--apply-loop-contracts _ --unsigned-overflow-check +\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$ +\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$ +\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ +\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test demonstrates a case where the loop guard has side effects. +The writes performed in the guard must also be specified +in the assigns clause of the loop. diff --git a/regression/contracts/nonvacuous_loop_contracts/main.c b/regression/contracts/nonvacuous_loop_contracts/main.c new file mode 100644 index 00000000000..876845e399f --- /dev/null +++ b/regression/contracts/nonvacuous_loop_contracts/main.c @@ -0,0 +1,33 @@ +#include +#include + +int main() +{ + size_t size; + + char *buf = malloc(size); + char c; + + size_t start; + size_t end = start; + + while(end < size) + // clang-format off + __CPROVER_loop_invariant(start <= end && end <= size) + __CPROVER_decreases(size - end) + // clang-format on + { + if(buf[end] != c) + break; + end++; + } + + if(start > size) + { + assert(end == start); + } + else + { + assert(start <= end && end <= size); + } +} diff --git a/regression/contracts/nonvacuous_loop_contracts/test.desc b/regression/contracts/nonvacuous_loop_contracts/test.desc new file mode 100644 index 00000000000..e50b9896f18 --- /dev/null +++ b/regression/contracts/nonvacuous_loop_contracts/test.desc @@ -0,0 +1,25 @@ +CORE +main.c +--apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check +\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ +\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ +\[main.assigns.\d+\] line \d+ Check that end is valid: SUCCESS$ +\[main.assigns.\d+\] line \d+ Check that end is assignable: SUCCESS$ +\[main.assertion.\d+\] line \d+ assertion end == start: SUCCESS$ +\[main.assertion.\d+\] line \d+ assertion start <= end && end <= size: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test demonstrates a simplification that is now possible on loop contracts. + +Prior to this commit, loop contracts were unconditionally applied on loops, +and thus had to also consider the case when the loop doesn't run even once. + +The contracts that were previously necessary were: + __CPROVER_loop_invariant( + (start > size && end == start) || (start <= end && end <= size) + ) + __CPROVER_decreases( + max(start, size) - end + ) diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc index 341b1e7c028..098fce85fd7 100644 --- a/regression/contracts/variant_missing_invariant_warning/test.desc +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -2,7 +2,7 @@ CORE main.c --apply-loop-contracts 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.$ +^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used.*.$ ^\[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$ diff --git a/regression/contracts/variant_multi_instruction_loop_head/main.c b/regression/contracts/variant_multi_instruction_loop_head/main.c index 705dd64d99a..e20ca0d9402 100644 --- a/regression/contracts/variant_multi_instruction_loop_head/main.c +++ b/regression/contracts/variant_multi_instruction_loop_head/main.c @@ -5,7 +5,7 @@ int main() while(*y <= 0 && *y < 10) // clang-format off - __CPROVER_loop_invariant(1 == 1) + __CPROVER_loop_invariant(0 <= *y && *y <= 10) __CPROVER_decreases(10 - x) // clang-format on { diff --git a/regression/contracts/variant_multi_instruction_loop_head/test.desc b/regression/contracts/variant_multi_instruction_loop_head/test.desc index dfcc8fcf847..075f922e05e 100644 --- a/regression/contracts/variant_multi_instruction_loop_head/test.desc +++ b/regression/contracts/variant_multi_instruction_loop_head/test.desc @@ -1,19 +1,16 @@ CORE main.c --apply-loop-contracts -^VERIFICATION FAILED$ -^EXIT=10$ +\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ +\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ +\[main\.\d+\] line \d+ Check decreases clause on loop iteration: SUCCESS$ +\[main\.\d+\] line \d+ Check that loop instrumentation was not truncated: SUCCESS$ +\[main\.assigns\.\d+\] line \d+ Check that x is valid: SUCCESS$ +\[main\.assigns\.\d+\] line \d+ Check that x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ ^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. +This test checks that decreases clause is properly initialized +when the loop head and loop invariant compilation emit several goto instructions. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index b0cb2fbf708..33600207afd 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -140,123 +140,140 @@ void code_contractst::check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, + goto_programt::targett loop_end, const loopt &loop, + exprt assigns_clause, + exprt invariant, + exprt decreases_clause, const irep_idt &mode) { - PRECONDITION(!loop.empty()); - - // find the last back edge - goto_programt::targett loop_end = loop_head; - for(const auto &t : loop) - if( - t->is_goto() && t->get_target() == loop_head && - t->location_number > loop_end->location_number) - loop_end = t; - - // check for assigns, invariant, and decreases clauses - auto assigns_clause = 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)); - - if(invariant.is_nil()) - { - if(decreases_clause.is_nil() && assigns_clause.is_nil()) - return; - else - { - invariant = true_exprt(); - log.warning() - << "The loop at " << loop_head->source_location().as_string() - << " 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; - } - } - else - { - // form the conjunction - invariant = conjunction(invariant.operands()); - } + const auto loop_head_location = loop_head->source_location(); // Vector representing a (possibly multidimensional) decreases clause const auto &decreases_clause_exprs = decreases_clause.operands(); // Temporary variables for storing the multidimensional decreases clause // at the start of and end of a loop body - std::vector old_decreases_vars; - std::vector new_decreases_vars; + std::vector old_decreases_vars, new_decreases_vars; + + replace_symbolt replace; + code_contractst::add_quantified_variable(invariant, replace, mode); + replace(invariant); - // change - // H: loop; - // E: ... + // instrument + // + // ... preamble ... + // HEAD: + // ... eval guard ... + // if (!guard) + // goto EXIT; + // ... loop body ... + // goto HEAD; + // EXIT: + // ... postamble ... + // // to - // initialize loop_entry variables; - // H: assert(invariant); - // snapshot(write_set); - // havoc; - // assume(invariant); - // if(guard) goto E: - // 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: ... + // + // ... preamble ... + // ,- initialize loop_entry history vars; + // | entered_loop = false + // loop assigns check | initial_invariant_val = invariant_expr; + // - unchecked, temps | in_base_case = true; + // func assigns check | snapshot (write_set); + // - disabled via pragma | goto HEAD; + // | STEP: + // --. | assert (initial_invariant_val); + // loop assigns check | | in_base_case = false; + // - not applicable >======= havoc (assigns_set); + // func assigns check | | assume (invariant_expr); + // + deferred | `- old_variant_val = decreases_clause_expr; + // --' * HEAD: + // loop assigns check ,- ... eval guard ... + // + assertions added | if (!guard) + // func assigns check | goto EXIT; + // - disabled via pragma `- ... loop body ... + // ,- entered_loop = true + // | if (in_base_case) + // | goto STEP; + // loop assigns check | assert (invariant_expr); + // - unchecked, temps | new_variant_val = decreases_clause_expr; + // func assigns check | assert (new_variant_val < old_variant_val); + // - disabled via pragma | dead old_variant_val, new_variant_val; + // | * assume (false); + // | * EXIT: + // To be inserted at ,~~~|~~~~ assert (entered_loop ==> !in_base_case); + // every unique EXIT | | dead loop_entry history vars, in_base_case; + // (break, goto etc.) `~~~`- ~~ dead initial_invariant_val, entered_loop; + // ... postamble .. + // + // Asterisks (*) denote anchor points (goto targets) for instrumentations. + // We insert generated code above and/below these targets. + // + // Assertions for assigns clause checking are inserted in the loop body. // 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 - const auto &invariant_expr = [&]() { - auto invariant_copy = invariant; - replace_symbolt replace; - code_contractst::add_quantified_variable(invariant_copy, replace, mode); - replace(invariant_copy); - return invariant_copy; - }; + // to be inserted before the loop head + goto_programt pre_loop_head_instrs; - // Process "loop_entry" history variables - // Find and replace "loop_entry" expression in the "invariant" expression. - std::map parameter2history; + // Process "loop_entry" history variables. + // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant. + std::map history_var_map; replace_history_parameter( invariant, - parameter2history, - loop_head->source_location(), + history_var_map, + loop_head_location, mode, - generated_code, + pre_loop_head_instrs, ID_loop_entry); - // Generate: assert(invariant) just before the loop - // We use a block scope to create a temporary assertion, - // and immediately convert it to goto instructions. + // Create a temporary to track if we entered the loop, + // i.e., the loop guard was satisfied. + const auto entered_loop = + new_tmp_symbol( + bool_typet(), loop_head_location, mode, symbol_table, "__entered_loop") + .symbol_expr(); + pre_loop_head_instrs.add( + goto_programt::make_decl(entered_loop, loop_head_location)); + pre_loop_head_instrs.add( + goto_programt::make_assignment(entered_loop, false_exprt{})); + + // Create a snapshot of the invariant so that we can check the base case, + // if the loop is not vacuous and must be abstracted with contracts. + const auto initial_invariant_val = + new_tmp_symbol( + bool_typet(), loop_head_location, mode, symbol_table, "__init_invariant") + .symbol_expr(); + pre_loop_head_instrs.add( + goto_programt::make_decl(initial_invariant_val, loop_head_location)); { - code_assertt assertion{invariant_expr()}; - assertion.add_source_location() = loop_head->source_location(); - converter.goto_convert(assertion, generated_code, mode); - generated_code.instructions.back().source_location_nonconst().set_comment( - "Check loop invariant before entry"); + // Although the invariant at this point will not have side effects, + // it is still a C expression, and needs to be "goto_convert"ed. + // Note that this conversion may emit many GOTO instructions. + code_assignt initial_invariant_value_assignment{ + initial_invariant_val, invariant}; + initial_invariant_value_assignment.add_source_location() = + loop_head_location; + converter.goto_convert( + initial_invariant_value_assignment, pre_loop_head_instrs, mode); } - // 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)); + // Create a temporary variable to track base case vs inductive case + // instrumentation of the loop. + const auto in_base_case = + new_tmp_symbol( + bool_typet(), loop_head_location, mode, symbol_table, "__in_base_case") + .symbol_expr(); + pre_loop_head_instrs.add( + goto_programt::make_decl(in_base_case, loop_head_location)); + pre_loop_head_instrs.add( + goto_programt::make_assignment(in_base_case, true_exprt{})); + + // CAR snapshot instructions for checking assigns clause + goto_programt snapshot_instructions; + // track static local symbols instrument_spec_assignst instrument_spec_assigns( function_name, goto_functions, symbol_table, log.get_message_handler()); - - // assigns clause snapshots - goto_programt snapshot_instructions; - instrument_spec_assigns.track_static_locals_between( loop_head, loop_end, snapshot_instructions); @@ -273,7 +290,8 @@ void code_contractst::check_apply_loop_contracts( get_assigns(local_may_alias, loop, to_havoc); // TODO: if the set contains pairs (i, a[i]), // we must at least widen them to (i, pointer_object(a)) - log.debug() << "No loop assigns clause provided. Inferred targets {"; + + log.debug() << "No loop assigns clause provided. Inferred targets: {"; // Add inferred targets to the loop assigns clause. bool ran_once = false; for(const auto &target : to_havoc) @@ -285,14 +303,15 @@ void code_contractst::check_apply_loop_contracts( instrument_spec_assigns.track_spec_target( target, snapshot_instructions); } - log.debug() - << "}. Please specify an assigns clause if verification fails." - << messaget::eom; + log.debug() << "}" << messaget::eom; + + instrument_spec_assigns.get_static_locals( + std::inserter(to_havoc, to_havoc.end())); } catch(const analysis_exceptiont &exc) { log.error() << "Failed to infer variables being modified by the loop at " - << loop_head->source_location() + << loop_head_location << ".\nPlease specify an assigns clause.\nReason:" << messaget::eom; throw exc; @@ -311,51 +330,61 @@ void code_contractst::check_apply_loop_contracts( // Insert instrumentation // This must be done before havocing the write set. - // ^^^ FIXME this is not true ^^^ - insert_before_swap_and_advance( - goto_function.body, loop_head, snapshot_instructions); + // FIXME: this is not true for write set targets that + // might depend on other write set targets. + pre_loop_head_instrs.destructive_append(snapshot_instructions); + + // Insert a jump to the loop head + // (skipping over the step case initialization code below) + pre_loop_head_instrs.add( + goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location)); + + // The STEP case instructions follow. + // We skip past it initially, because of the unconditional jump above, + // but jump back here if we get past the loop guard while in_base_case. + + const auto step_case_target = + pre_loop_head_instrs.add(goto_programt::make_assignment( + in_base_case, false_exprt{}, loop_head_location)); + + // If we jump here, then the loop runs at least once, + // so add the base case assertion: + // assert(initial_invariant_val) + // We use a block scope for assertion, since it's immediately goto converted, + // and doesn't need to be kept around. + { + code_assertt assertion{initial_invariant_val}; + assertion.add_source_location() = loop_head_location; + converter.goto_convert(assertion, pre_loop_head_instrs, mode); + pre_loop_head_instrs.instructions.back() + .source_location_nonconst() + .set_comment("Check loop invariant before entry"); + } - optionalt cfg_empty_info; + // Insert the first block of pre_loop_head_instrs, + // with a pragma to disable assigns clause checking. + // All of the initialization code so far introduces local temporaries, + // which need not be checked against the enclosing scope's assigns clause. + goto_function.body.destructive_insert( + loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs)); - // Perform write set instrumentation on the entire loop. - instrument_spec_assigns.instrument_instructions( - goto_function.body, - loop_head, - loop_end, - skip_function_paramst::NO, - // do not use CFG info for now - cfg_empty_info); - - // insert havocing code + // Generate havocing code for assignment targets. havoc_assigns_targetst havoc_gen(to_havoc, ns); - havoc_gen.append_full_havoc_code( - loop_head->source_location(), generated_code); - - // Add the havocing code, but only check against the enclosing scope's - // write set if it was manually specified. - if(assigns_clause.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); + havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs); - // ^^^ FIXME ^^^ - // comment by delmasrd: I did not reactivate this behaviour - // because I think we always want to check the loop assignments against - // the surrounding clause - - insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + // Insert the second block of pre_loop_head_instrs: the havocing code. + // We do not `add_pragma_disable_assigns_check`, + // so that the enclosing scope's assigns clause instrumentation + // would pick these havocs up for inclusion (subset) checks. + goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs); // Generate: assume(invariant) just after havocing - // We use a block scope to create a temporary assumption, - // and immediately convert it to goto instructions. + // We use a block scope for assumption, since it's immediately goto converted, + // and doesn't need to be kept around. { - code_assumet assumption{invariant_expr()}; - assumption.add_source_location() = loop_head->source_location(); - converter.goto_convert(assumption, generated_code, mode); + code_assumet assumption{invariant}; + assumption.add_source_location() = loop_head_location; + converter.goto_convert(assumption, pre_loop_head_instrs, mode); } // Create fresh temporary variables that store the multidimensional @@ -363,19 +392,17 @@ void code_contractst::check_apply_loop_contracts( for(const auto &clause : decreases_clause.operands()) { const auto old_decreases_var = - new_tmp_symbol( - clause.type(), loop_head->source_location(), mode, symbol_table) + new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table) .symbol_expr(); - generated_code.add(goto_programt::make_decl( - old_decreases_var, loop_head->source_location())); + pre_loop_head_instrs.add( + goto_programt::make_decl(old_decreases_var, loop_head_location)); old_decreases_vars.push_back(old_decreases_var); const auto new_decreases_var = - new_tmp_symbol( - clause.type(), loop_head->source_location(), mode, symbol_table) + new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table) .symbol_expr(); - generated_code.add(goto_programt::make_decl( - new_decreases_var, loop_head->source_location())); + pre_loop_head_instrs.add( + goto_programt::make_decl(new_decreases_var, loop_head_location)); new_decreases_vars.push_back(new_decreases_var); } @@ -383,65 +410,77 @@ void code_contractst::check_apply_loop_contracts( 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; + << loop_head_location << messaget::eom; throw 0; // non-deterministically skip the loop if it is a do-while loop. - generated_code.add(goto_programt::make_goto( - loop_end, - side_effect_expr_nondett(bool_typet(), loop_head->source_location()))); + // pre_loop_head_instrs.add(goto_programt::make_goto( + // loop_end, side_effect_expr_nondett(bool_typet(), loop_head_location))); } - // 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, - add_pragma_disable_assigns_check(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). - // If the loop_head location shifts to a different function, - // assume that it's an inlined function and keep skipping. - // 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->source_location().get_function() != head_loc.get_function()) - 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--; - // Generate: assignments to store the multidimensional decreases clause's - // value just before the loop body (but just after the loop guard) + // value just before the loop_head if(!decreases_clause.is_nil()) { for(size_t i = 0; i < old_decreases_vars.size(); i++) { - code_assignt old_decreases_assignment{old_decreases_vars[i], - decreases_clause_exprs[i]}; - old_decreases_assignment.add_source_location() = - loop_head->source_location(); - converter.goto_convert(old_decreases_assignment, generated_code, mode); + code_assignt old_decreases_assignment{ + old_decreases_vars[i], decreases_clause_exprs[i]}; + old_decreases_assignment.add_source_location() = loop_head_location; + converter.goto_convert( + old_decreases_assignment, pre_loop_head_instrs, mode); } goto_function.body.destructive_insert( - loop_body, add_pragma_disable_assigns_check(generated_code)); + loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs)); } - // Generate: assert(invariant) just after the loop exits - // We use a block scope to create a temporary assertion, - // and immediately convert it to goto instructions. + // Insert the third and final block of pre_loop_head_instrs, + // with a pragma to disable assigns clause checking. + // The variables to store old variant value are local temporaries, + // which need not be checked against the enclosing scope's assigns clause. + goto_function.body.destructive_insert( + loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs)); + + optionalt cfg_empty_info; + + // Perform write set instrumentation on the entire loop. + instrument_spec_assigns.instrument_instructions( + goto_function.body, + loop_head, + loop_end, + skip_function_paramst::NO, + // do not use CFG info for now + cfg_empty_info); + + // Now we begin instrumenting at the loop_end. + // `pre_loop_end_instrs` are to be inserted before `loop_end`. + goto_programt pre_loop_end_instrs; + + // Record that we entered the loop. + pre_loop_end_instrs.add( + goto_programt::make_assignment(entered_loop, true_exprt{})); + + // Jump back to the step case to havoc the write set, assume the invariant, + // and execute an arbitrary iteration. + pre_loop_end_instrs.add(goto_programt::make_goto( + step_case_target, in_base_case, loop_head_location)); + + // The following code is only reachable in the step case, + // i.e., when in_base_case == false, + // because of the unconditional jump above. + + // Generate the inductiveness check: + // assert(invariant) + // We use a block scope for assertion, since it's immediately goto converted, + // and doesn't need to be kept around. { - code_assertt assertion{invariant_expr()}; - assertion.add_source_location() = loop_end->source_location(); - converter.goto_convert(assertion, generated_code, mode); - generated_code.instructions.back().source_location_nonconst().set_comment( - "Check that loop invariant is preserved"); + code_assertt assertion{invariant}; + assertion.add_source_location() = loop_head_location; + converter.goto_convert(assertion, pre_loop_end_instrs, mode); + pre_loop_end_instrs.instructions.back() + .source_location_nonconst() + .set_comment("Check that loop invariant is preserved"); } // Generate: assignments to store the multidimensional decreases clause's @@ -450,44 +489,82 @@ void code_contractst::check_apply_loop_contracts( { for(size_t i = 0; i < new_decreases_vars.size(); i++) { - code_assignt new_decreases_assignment{new_decreases_vars[i], - decreases_clause_exprs[i]}; - new_decreases_assignment.add_source_location() = - loop_head->source_location(); - converter.goto_convert(new_decreases_assignment, generated_code, mode); + code_assignt new_decreases_assignment{ + new_decreases_vars[i], decreases_clause_exprs[i]}; + new_decreases_assignment.add_source_location() = loop_head_location; + converter.goto_convert( + new_decreases_assignment, pre_loop_end_instrs, mode); } // Generate: assertion that the multidimensional decreases clause's value - // after the loop is smaller than the value before the loop. - // Here, we use the lexicographic order. + // after the loop is lexicographically smaller than its initial value. code_assertt monotonic_decreasing_assertion{ generate_lexicographic_less_than_check( new_decreases_vars, old_decreases_vars)}; - monotonic_decreasing_assertion.add_source_location() = - loop_head->source_location(); + monotonic_decreasing_assertion.add_source_location() = loop_head_location; converter.goto_convert( - monotonic_decreasing_assertion, generated_code, mode); - generated_code.instructions.back().source_location_nonconst().set_comment( - "Check decreases clause on loop iteration"); + monotonic_decreasing_assertion, pre_loop_end_instrs, mode); + pre_loop_end_instrs.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++) { - generated_code.add(goto_programt::make_dead( - old_decreases_vars[i], loop_head->source_location())); - generated_code.add(goto_programt::make_dead( - new_decreases_vars[i], loop_head->source_location())); + pre_loop_end_instrs.add( + goto_programt::make_dead(old_decreases_vars[i], loop_head_location)); + pre_loop_end_instrs.add( + goto_programt::make_dead(new_decreases_vars[i], loop_head_location)); } } insert_before_swap_and_advance( goto_function.body, loop_end, - add_pragma_disable_assigns_check(generated_code)); + add_pragma_disable_assigns_check(pre_loop_end_instrs)); // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume(); loop_end->set_condition(boolean_negate(loop_end->get_condition())); + + std::set seen_targets; + // Find all exit points of the loop, make temporary variables `DEAD`, + // and check that step case was checked for non-vacuous loops. + for(const auto &t : loop) + { + if(!t->is_goto()) + continue; + + auto exit_target = t->get_target(); + if( + loop.contains(exit_target) || + seen_targets.find(exit_target) != seen_targets.end()) + continue; + + seen_targets.insert(exit_target); + + goto_programt pre_loop_exit_instrs; + // Assertion to check that step case was checked if we entered the loop. + pre_loop_exit_instrs.add(goto_programt::make_assertion( + or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}}, + loop_head_location)); + pre_loop_exit_instrs.instructions.back() + .source_location_nonconst() + .set_comment("Check that loop instrumentation was not truncated"); + // Instructions to make all the temporaries go dead. + pre_loop_exit_instrs.add( + goto_programt::make_dead(in_base_case, loop_head_location)); + pre_loop_exit_instrs.add( + goto_programt::make_dead(initial_invariant_val, loop_head_location)); + for(const auto &v : history_var_map) + { + pre_loop_exit_instrs.add( + goto_programt::make_dead(to_symbol_expr(v.second), loop_head_location)); + } + // Insert these instructions, preserving the loop end target. + insert_before_swap_and_advance( + goto_function.body, exit_target, pre_loop_exit_instrs); + } } void code_contractst::add_quantified_variable( @@ -898,20 +975,171 @@ void code_contractst::apply_loop_contract( 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) + const typename natural_loops_mutablet::loopt &content; + const goto_programt::targett head_target, end_target; + exprt assigns_clause, invariant, decreases_clause; + + loop_graph_nodet( + const typename natural_loops_mutablet::loopt &loop, + const goto_programt::targett head, + const goto_programt::targett end, + const exprt &assigns, + const exprt &inv, + const exprt &decreases) + : content(loop), + head_target(head), + end_target(end), + assigns_clause(assigns), + invariant(inv), + decreases_clause(decreases) { } }; grapht loop_nesting_graph; - for(const auto &loop : natural_loops.loop_map) - loop_nesting_graph.add_node(loop.first, loop.second); + std::list to_check_contracts_on_children; + + for(const auto &loop_head_and_content : natural_loops.loop_map) + { + const auto &loop_content = loop_head_and_content.second; + if(loop_content.empty()) + continue; + + auto loop_head = loop_head_and_content.first; + auto loop_end = loop_head; + + // Find the last back edge to `loop_head` + for(const auto &t : loop_content) + { + if( + t->is_goto() && t->get_target() == loop_head && + t->location_number > loop_end->location_number) + loop_end = t; + } + + if(loop_end == loop_head) + { + log.error() << "Could not find end of the loop starting at: " + << loop_head->source_location() << messaget::eom; + throw 0; + } + + exprt assigns_clause = + static_cast(loop_end->condition().find(ID_C_spec_assigns)); + exprt invariant = static_cast( + loop_end->get_condition().find(ID_C_spec_loop_invariant)); + exprt decreases_clause = static_cast( + loop_end->get_condition().find(ID_C_spec_decreases)); + + if(invariant.is_nil()) + { + if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil()) + { + invariant = true_exprt{}; + // assigns clause is missing; we will try to automatic inference + log.warning() + << "The loop at " << loop_head->source_location().as_string() + << " does not have an invariant in its contract.\n" + << "Hence, a default invariant ('true') is being used.\n" + << "This choice is sound, but verification may fail" + << " if it is be too weak to prove the desired properties." + << messaget::eom; + } + } + else + { + invariant = conjunction(invariant.operands()); + if(decreases_clause.is_nil()) + { + log.warning() << "The loop at " + << loop_head->source_location().as_string() + << " does not have a decreases clause in its contract.\n" + << "Termination of this loop will not be verified." + << messaget::eom; + } + } + + const auto idx = loop_nesting_graph.add_node( + loop_content, + loop_head, + loop_end, + assigns_clause, + invariant, + decreases_clause); + + if( + assigns_clause.is_nil() && invariant.is_nil() && + decreases_clause.is_nil()) + continue; + + to_check_contracts_on_children.push_back(idx); + + // By definition the `loop_content` is a set of instructions computed + // by `natural_loops` based on the CFG. + // Since we perform assigns clause instrumentation by sequentially + // traversing instructions from `loop_head` to `loop_end`, here check that: + // 1. All instructions in `loop_content` are contained within the + // [loop_head, loop_end] iterator range + // 2. All instructions in the [loop_head, loop_end] range are contained + // in the `loop_content` set, except for the exceptions explained below. + + // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end + for(const auto &i : loop_content) + { + if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0) + { + log.error() << "Computed loop at " << loop_head->source_location() + << "contains an instruction beyond [loop_head, loop_end]:" + << messaget::eom; + goto_function.body.output_instruction( + ns, function_name, log.error(), *i); + throw 0; + } + } + + // Check 2. (loop_head <= i <= loop_end) ==> (i \in loop_content) + // + // We allow the following exceptions in this check: + // - `SKIP` or `LOCATION` instructions which are no-op + // - `ASSUME(false)` instructions which are introduced by function pointer + // or nested loop transformations, and have no successor instructions + // - `SET_RETURN_VALUE` instructions followed by an uninterrupted sequence + // of `DEAD` instructions and a `GOTO` jump out of the loop, + // which model C `return` statements. + // - `GOTO` jumps out of the loops, which model C `break` statements. + // These instructions are allowed to be missing from `loop_content`, + // and may be safely ignored for the purpose of our instrumentation. + for(auto i = loop_head; i < loop_end; ++i) + { + if(loop_content.contains(i)) + continue; + + if(i->is_skip() || i->is_location()) + continue; + + if(i->is_goto() && !loop_content.contains(i->get_target())) + continue; + + if(i->is_assume() && i->get_condition().is_false()) + continue; + + if(i->is_set_return_value()) + { + do + i++; + while(i->is_dead()); + + // because we increment `i` in the outer `for` loop + i--; + continue; + } + + log.error() << "Computed loop at: " << loop_head->source_location() + << "is missing an instruction:" << messaget::eom; + goto_function.body.output_instruction(ns, function_name, log.error(), *i); + throw 0; + } + } for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer) { @@ -920,10 +1148,47 @@ void code_contractst::apply_loop_contract( if(inner == outer) continue; - if(loop_nesting_graph[outer].loop.contains( - loop_nesting_graph[inner].target)) - loop_nesting_graph.add_edge(outer, inner); + if(loop_nesting_graph[outer].content.contains( + loop_nesting_graph[inner].head_target)) + { + if(!loop_nesting_graph[outer].content.contains( + loop_nesting_graph[inner].end_target)) + { + log.error() + << "Overlapping loops at:\n" + << loop_nesting_graph[outer].head_target->source_location() + << "\nand\n" + << loop_nesting_graph[inner].head_target->source_location() + << "\nLoops must be nested or sequential for contracts to be " + "enforced." + << messaget::eom; + } + loop_nesting_graph.add_edge(inner, outer); + } + } + } + + // make sure all children of a contractified loop also have contracts + while(!to_check_contracts_on_children.empty()) + { + const auto loop_idx = to_check_contracts_on_children.front(); + to_check_contracts_on_children.pop_front(); + + const auto &loop_node = loop_nesting_graph[loop_idx]; + if( + loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() && + loop_node.decreases_clause.is_nil()) + { + log.error() + << "Inner loop at: " << loop_node.head_target->source_location() + << " does not have contracts, but an enclosing loop does.\n" + << "Please provide contracts for this loop, or unwind it first." + << messaget::eom; + throw 0; } + + for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx)) + to_check_contracts_on_children.push_back(child_idx); } // Iterate over the (natural) loops in the function, in topo-sorted order, @@ -931,12 +1196,21 @@ void code_contractst::apply_loop_contract( for(const auto &idx : loop_nesting_graph.topsort()) { const auto &loop_node = loop_nesting_graph[idx]; + if( + loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() && + loop_node.decreases_clause.is_nil()) + continue; + check_apply_loop_contracts( function_name, goto_function, local_may_alias, - loop_node.target, - loop_node.loop, + loop_node.head_target, + loop_node.end_target, + loop_node.content, + loop_node.assigns_clause, + loop_node.invariant, + loop_node.decreases_clause, symbol_table.lookup_ref(function_name).mode); } } diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 611a87daeab..cca3172c86f 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -102,7 +102,11 @@ class code_contractst goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, + goto_programt::targett loop_end, const loopt &loop, + exprt assigns_clause, + exprt invariant, + exprt decreases_clause, const irep_idt &mode); // for "helper" classes to update symbol table. diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index 8dcfc810603..adf9d5a66a7 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -451,6 +451,20 @@ class instrument_spec_assignst skip_function_paramst skip_function_params, optionalt &cfg_info_opt); + /// Inserts the detected static local symbols into a target container. + /// \tparam C The type of the target container + /// \param inserter An insert_iterator on the target container + template + void get_static_locals(std::insert_iterator inserter) const + { + std::transform( + from_static_local.cbegin(), + from_static_local.cend(), + inserter, + // can use `const auto &` below once we switch to C++14 + [](const symbol_exprt_to_car_mapt::value_type &s) { return s.first; }); + } + protected: /// Name of the instrumented function const irep_idt &function_id;