diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc index f5522104e07..95405e44617 100644 --- a/regression/contracts/invar_check_multiple_loops/test.desc +++ b/regression/contracts/invar_check_multiple_loops/test.desc @@ -5,8 +5,10 @@ main.c ^SIGNAL=0$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.3\] .* Check loop invariant before entry: SUCCESS$ -^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check decreases clause on loop iteration: 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.1\] .* assertion x == y \+ 2 \* n: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_check_nested_loops/main.c b/regression/contracts/invar_check_nested_loops/main.c index 4c9617fbd26..8ea27e7bd99 100644 --- a/regression/contracts/invar_check_nested_loops/main.c +++ b/regression/contracts/invar_check_nested_loops/main.c @@ -7,7 +7,7 @@ int main() for(int i = 0; i < n; ++i) // clang-format off - __CPROVER_loop_invariant(i <= n && s == i) + __CPROVER_loop_invariant(0 <= i && i <= n && s == i) __CPROVER_decreases(n - i) // clang-format on { diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc index 2035a258ee6..56cce65d6c0 100644 --- a/regression/contracts/invar_check_nested_loops/test.desc +++ b/regression/contracts/invar_check_nested_loops/test.desc @@ -4,9 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$ ^\[main.2\] .* Check loop invariant before entry: SUCCESS$ ^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.4\] .* Check decreases clause on loop iteration: SUCCESS$ ^\[main.assertion.1\] .* assertion s == n: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/variant_function_call_fail/main.c b/regression/contracts/variant_function_call_fail/main.c new file mode 100644 index 00000000000..7f33ca35ef6 --- /dev/null +++ b/regression/contracts/variant_function_call_fail/main.c @@ -0,0 +1,23 @@ +#define N 10 + +int foo(int i); + +int main() +{ + int i = 0; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(foo(i)) + // clang-format on + { + i++; + } + + return 0; +} + +int foo(int i) +{ + return N - i; +} diff --git a/regression/contracts/variant_function_call_fail/test.desc b/regression/contracts/variant_function_call_fail/test.desc new file mode 100644 index 00000000000..2fdfb1f8405 --- /dev/null +++ b/regression/contracts/variant_function_call_fail/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts +^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ +^EXIT=70$ +^SIGNAL=0$ +-- +-- +This test fails because the decreases clause contains a function call. Decreases +clauses must not contain loops, since we want to ensure that the +calculation of decreases clauses will terminate. To enforce this requirement, +for now, we simply ban decreases clauses from containing function calls. +In the future, we may allow function calls (but definitely not loops) to appear +inside decreases clauses. diff --git a/regression/contracts/variant_missing_invariant_warning/main.c b/regression/contracts/variant_missing_invariant_warning/main.c new file mode 100644 index 00000000000..2fa5b695d24 --- /dev/null +++ b/regression/contracts/variant_missing_invariant_warning/main.c @@ -0,0 +1,13 @@ +int main() +{ + unsigned i = 10; + while(i != 0) + // clang-format off + __CPROVER_decreases(i) + // clang-format on + { + i--; + } + + return 0; +} diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc new file mode 100644 index 00000000000..30e327c36a5 --- /dev/null +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts +activate-multi-line-match +^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.$ +^\[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$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test succeeds, but it gives a warning that the user has not provided a loop +invariant. Hence, a default loop invariant (i.e. true) will be used. diff --git a/regression/contracts/variant_not_decreasing_fail/main.c b/regression/contracts/variant_not_decreasing_fail/main.c new file mode 100644 index 00000000000..a2913e961ac --- /dev/null +++ b/regression/contracts/variant_not_decreasing_fail/main.c @@ -0,0 +1,16 @@ + +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_not_decreasing_fail/test.desc b/regression/contracts/variant_not_decreasing_fail/test.desc new file mode 100644 index 00000000000..84e9b8fae5e --- /dev/null +++ b/regression/contracts/variant_not_decreasing_fail/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts +^main.c function main$ +^\[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: FAILURE$ +^.* 1 of 3 failed \(2 iterations\)$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the decreases clause is not monotinically decreasing. diff --git a/regression/contracts/variant_parsing_statement_fail/test.desc b/regression/contracts/variant_parsing_statement_fail/test.desc index a65b9fc5dae..84fbc0df122 100644 --- a/regression/contracts/variant_parsing_statement_fail/test.desc +++ b/regression/contracts/variant_parsing_statement_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-all-contracts +--apply-loop-contracts activate-multi-line-match ^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$ ^PARSING ERROR$ @@ -8,6 +8,6 @@ activate-multi-line-match ^SIGNAL=0$ -- -- -This test fails because the loop variant is a statement (more precisely, +This test fails because the decreases clause is a statement (more precisely, an assignment) rather than an expression (more precisely, an ACSL binding expression). diff --git a/regression/contracts/variant_parsing_tuple_fail/test.desc b/regression/contracts/variant_parsing_tuple_fail/test.desc index e47f0b1ee48..f98beefcaf1 100644 --- a/regression/contracts/variant_parsing_tuple_fail/test.desc +++ b/regression/contracts/variant_parsing_tuple_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-all-contracts +--apply-loop-contracts activate-multi-line-match ^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$ ^PARSING ERROR$ @@ -8,6 +8,6 @@ activate-multi-line-match ^SIGNAL=0$ -- -- -This test fails because the loop variant has two arguments instead of just one. -Currently, we only support loop variants of single arguments - we do not -support loop variants of tuples (yet). +This test fails because the decreases clause has two arguments instead of just one. +Currently, we only support decreases clauses of single arguments - we do not +support decreases clauses of tuples (yet). diff --git a/regression/contracts/variant_side_effects_fail/main.c b/regression/contracts/variant_side_effects_fail/main.c new file mode 100644 index 00000000000..fa2f12acb04 --- /dev/null +++ b/regression/contracts/variant_side_effects_fail/main.c @@ -0,0 +1,15 @@ +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases((N+=0) - i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_side_effects_fail/test.desc b/regression/contracts/variant_side_effects_fail/test.desc new file mode 100644 index 00000000000..6f6c47d36a6 --- /dev/null +++ b/regression/contracts/variant_side_effects_fail/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--apply-loop-contracts +^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ +^EXIT=70$ +^SIGNAL=0$ +-- +-- +This test fails because the decreases clause contains a side effect, namely +incrementing variable N by zero. In this case, although the value of N +remains unchanged after the increment operation, we read from and write to N. +So this constitues a side effect. Decreases clauses are banned from containing +side effects, since decreases clauses should not modify program states. diff --git a/regression/contracts/variant_weak_invariant_fail/main.c b/regression/contracts/variant_weak_invariant_fail/main.c new file mode 100644 index 00000000000..c9ab28d2403 --- /dev/null +++ b/regression/contracts/variant_weak_invariant_fail/main.c @@ -0,0 +1,16 @@ + +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(i <= N) + __CPROVER_decreases(N - i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_weak_invariant_fail/test.desc b/regression/contracts/variant_weak_invariant_fail/test.desc new file mode 100644 index 00000000000..0cec1b04c87 --- /dev/null +++ b/regression/contracts/variant_weak_invariant_fail/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--apply-loop-contracts +^main.c function main$ +^\[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: FAILURE$ +^.* 1 of 3 failed \(2 iterations\)$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the loop invariant is not strong enough for the +termination proof. We must add 0 <= i to the loop invariant. diff --git a/regression/contracts/variant_while_true_pass/main.c b/regression/contracts/variant_while_true_pass/main.c new file mode 100644 index 00000000000..2684f85f885 --- /dev/null +++ b/regression/contracts/variant_while_true_pass/main.c @@ -0,0 +1,20 @@ + +int main() +{ + int i = 0; + int N = 10; + while(1 == 1) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(N - i) + // clang-format on + { + if(i == 10) + { + break; + } + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_while_true_pass/test.desc b/regression/contracts/variant_while_true_pass/test.desc new file mode 100644 index 00000000000..ae57398ec60 --- /dev/null +++ b/regression/contracts/variant_while_true_pass/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--apply-loop-contracts +^main.c function main$ +^\[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$ +^.*0 of 3 failed \(1 iterations\)$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test succeeds. The purpose of this test is to check whether a decreases +clause can successfully prove the termination of a loop (i) whose exit condition +is 1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index e6d5bb35a3c..4caf9bf9e8d 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -112,8 +112,9 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log) return result; } -void code_contractst::check_apply_invariants( +void code_contractst::check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, + const irep_idt &function_name, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop, @@ -129,11 +130,25 @@ void code_contractst::check_apply_invariants( t->location_number > loop_end->location_number) loop_end = t; - // see whether we have an invariant + // see whether we have an invariant and a decreases clause 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()) - return; + { + if(decreases_clause.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." + << messaget::eom; + } + } // change // H: loop; @@ -142,9 +157,12 @@ void code_contractst::check_apply_invariants( // H: assert(invariant); // havoc; // assume(invariant); + // old_decreases_value = decreases_clause(current_environment); // if(guard) goto E: // loop; + // new_decreases_value = decreases_clause(current_environment); // assert(invariant); + // assert(new_decreases_value < old_decreases_value); // assume(false); // E: ... @@ -188,6 +206,32 @@ void code_contractst::check_apply_invariants( converter.goto_convert(assumption, havoc_code, mode); } + // Temporary variables that store the decreases clause's values before and + // after the loop + symbol_exprt old_decreases_symbol = + new_tmp_symbol( + decreases_clause.type(), loop_head->source_location, function_name, mode) + .symbol_expr(); + symbol_exprt new_decreases_symbol = + new_tmp_symbol( + decreases_clause.type(), loop_head->source_location, function_name, mode) + .symbol_expr(); + + if(!decreases_clause.is_nil()) + { + // Generate: a declaration of the temporary variable that stores the + // decreases clause's value before the loop + havoc_code.add(goto_programt::make_decl( + old_decreases_symbol, loop_head->source_location)); + + // Generate: an assignment to store the decreases clause's value before the + // loop + code_assignt old_decreases_assignment{old_decreases_symbol, + decreases_clause}; + old_decreases_assignment.add_source_location() = loop_head->source_location; + converter.goto_convert(old_decreases_assignment, havoc_code, mode); + } + // non-deterministically skip the loop if it is a do-while loop if(!loop_head->is_goto()) { @@ -209,14 +253,46 @@ void code_contractst::check_apply_invariants( converter.goto_convert(assertion, havoc_code, mode); havoc_code.instructions.back().source_location.set_comment( "Check that loop invariant is preserved"); - auto offset = havoc_code.instructions.size(); - goto_function.body.insert_before_swap(loop_end, havoc_code); - std::advance(loop_end, offset); } + if(!decreases_clause.is_nil()) + { + // Generate: a declaration of a temporary variable that stores the decreases + // clause after one arbitrary iteration of the loop + havoc_code.add(goto_programt::make_decl( + new_decreases_symbol, loop_head->source_location)); + + // Generate: an assignment to store the decreases clause's value after one + // iteration of the loop + code_assignt new_decreases_assignment{new_decreases_symbol, + decreases_clause}; + new_decreases_assignment.add_source_location() = loop_head->source_location; + converter.goto_convert(new_decreases_assignment, havoc_code, mode); + + // Generate: assertion that the decreases clause's value after the loop is + // smaller than the value before the loop + code_assertt monotonic_decreasing_assertion{ + binary_relation_exprt(new_decreases_symbol, ID_lt, old_decreases_symbol)}; + 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.set_comment( + "Check decreases clause on loop iteration"); + + // Discard the temporary variables that store decreases clause's values + havoc_code.add(goto_programt::make_dead( + old_decreases_symbol, loop_head->source_location)); + havoc_code.add(goto_programt::make_dead( + new_decreases_symbol, loop_head->source_location)); + } + + auto offset = havoc_code.instructions.size(); + goto_function.body.insert_before_swap(loop_end, havoc_code); + std::advance(loop_end, offset); + // change the back edge into assume(false) or assume(guard) loop_end->targets.clear(); - loop_end->type=ASSUME; + loop_end->type = ASSUME; if(loop_head->is_goto()) loop_end->set_condition(false_exprt()); else @@ -559,12 +635,15 @@ void code_contractst::apply_loop_contract( // Iterate over the (natural) loops in the function, // and apply any invariant annotations that we find. for(const auto &loop : natural_loops.loop_map) - check_apply_invariants( + { + check_apply_loop_contracts( goto_function, + function_name, local_may_alias, loop.first, loop.second, symbol_table.lookup_ref(function_name).mode); + } } const symbolt &code_contractst::new_tmp_symbol( diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index a70acad5b75..0137613a0d4 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -98,12 +98,14 @@ class code_contractst const irep_idt &function_id, const irep_idt &mode); - void check_apply_invariants( + void check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, + const irep_idt &function_name, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode); + const namespacet &get_namespace() const; // for "helper" classes to update symbol table. diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 20bc2c240b4..455e1322090 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -857,25 +857,40 @@ void goto_convertt::convert_assume( dest.add(goto_programt::make_assumption(op, code.source_location())); } -void goto_convertt::convert_loop_invariant( +void goto_convertt::convert_loop_contracts( const codet &code, goto_programt::targett loop, const irep_idt &mode) { - exprt invariant= - static_cast(code.find(ID_C_spec_loop_invariant)); + exprt invariant = + static_cast(code.find(ID_C_spec_loop_invariant)); + exprt decreases_clause = + static_cast(code.find(ID_C_spec_decreases)); - if(invariant.is_nil()) - return; - - if(has_subexpr(invariant, ID_side_effect)) + if(!invariant.is_nil()) { - throw incorrect_goto_program_exceptiont( - "Loop invariant is not side-effect free.", code.find_source_location()); + if(has_subexpr(invariant, ID_side_effect)) + { + throw incorrect_goto_program_exceptiont( + "Loop invariant is not side-effect free.", code.find_source_location()); + } + + PRECONDITION(loop->is_goto()); + loop->guard.add(ID_C_spec_loop_invariant).swap(invariant); } - PRECONDITION(loop->is_goto()); - loop->guard.add(ID_C_spec_loop_invariant).swap(invariant); + if(!decreases_clause.is_nil()) + { + if(has_subexpr(decreases_clause, ID_side_effect)) + { + throw incorrect_goto_program_exceptiont( + "Decreases clause is not side-effect free.", + code.find_source_location()); + } + + PRECONDITION(loop->is_goto()); + loop->guard.add(ID_C_spec_decreases).swap(decreases_clause); + } } void goto_convertt::convert_for( @@ -956,8 +971,8 @@ void goto_convertt::convert_for( goto_programt::targett y = tmp_y.add( goto_programt::make_goto(u, true_exprt(), code.source_location())); - // loop invariant - convert_loop_invariant(code, y, mode); + // loop invariant and decreases clause + convert_loop_contracts(code, y, mode); dest.destructive_append(sideeffects); dest.destructive_append(tmp_v); @@ -1014,8 +1029,8 @@ void goto_convertt::convert_while( goto_programt tmp_x; convert(code.body(), tmp_x, mode); - // loop invariant - convert_loop_invariant(code, y, mode); + // loop invariant and decreases clause + convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_branch); dest.destructive_append(tmp_x); @@ -1083,8 +1098,8 @@ void goto_convertt::convert_dowhile( // y: if(c) goto w; y->complete_goto(w); - // loop invariant - convert_loop_invariant(code, y, mode); + // loop invariant and decreases clause + convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_w); dest.destructive_append(sideeffects); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 5244983d39c..0f644dad6ad 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -236,7 +236,7 @@ class goto_convertt:public messaget goto_programt &dest, const irep_idt &mode); void convert_cpp_delete(const codet &code, goto_programt &dest); - void convert_loop_invariant( + void convert_loop_contracts( const codet &code, goto_programt::targett loop, const irep_idt &mode);