diff --git a/regression/contracts/invariant_side_effects/main.c b/regression/contracts/invariant_side_effects/main.c new file mode 100644 index 00000000000..26d5748c67f --- /dev/null +++ b/regression/contracts/invariant_side_effects/main.c @@ -0,0 +1,16 @@ +#include +#include + +int main() +{ + unsigned N, *a = malloc(sizeof(unsigned int)); + + *a = 0; + while(*a < N) + __CPROVER_loop_invariant((0 <= *a) && (*a <= N)) + { + ++(*a); + } + + assert(*a == N); +} diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc new file mode 100644 index 00000000000..e15f86c30e0 --- /dev/null +++ b/regression/contracts/invariant_side_effects/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-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 \*a == N: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that C expressions are correctly converted to logic +when enforcing loop invariant annotations. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 6755378847f..36243abc5f5 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -20,7 +20,6 @@ Date: February 2016 #include -#include #include #include @@ -34,8 +33,6 @@ Date: February 2016 #include #include -#include "loop_utils.h" - /// Predicate to be used with the exprt::visit() function. The function /// found_return_value() will return `true` iff this predicate is called on an /// expr that contains `__CPROVER_return_value`. @@ -74,11 +71,12 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log) return result; } -static void check_apply_invariants( +void code_contractst::check_apply_invariants( goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, - const loopt &loop) + const loopt &loop, + const irep_idt &mode) { PRECONDITION(!loop.empty()); @@ -96,16 +94,18 @@ static void check_apply_invariants( if(invariant.is_nil()) return; - // change H: loop; E: ... + // change + // H: loop; + // E: ... // to - // H: assert(invariant); - // havoc; - // assume(invariant); - // if(guard) goto E: - // loop; - // assert(invariant); - // assume(false); - // E: ... + // H: assert(invariant); + // havoc; + // assume(invariant); + // if(guard) goto E: + // loop; + // assert(invariant); + // assume(false); + // E: ... // find out what can get changed in the loop modifiest modifies; @@ -116,17 +116,20 @@ static void check_apply_invariants( // assert the invariant { - goto_programt::targett a = havoc_code.add( - goto_programt::make_assertion(invariant, loop_head->source_location)); - a->source_location.set_comment("Check loop invariant before entry"); + code_assertt assertion{invariant}; + assertion.add_source_location() = loop_head->source_location; + converter.goto_convert(assertion, havoc_code, mode); + havoc_code.instructions.back().source_location.set_comment( + "Check loop invariant before entry"); } // havoc variables being written to build_havoc_code(loop_head, modifies, havoc_code); // assume the invariant - havoc_code.add( - goto_programt::make_assumption(invariant, loop_head->source_location)); + code_assumet assumption{invariant}; + assumption.add_source_location() = loop_head->source_location; + converter.goto_convert(assumption, havoc_code, mode); // non-deterministically skip the loop if it is a do-while loop if(!loop_head->is_goto()) @@ -142,11 +145,14 @@ static void check_apply_invariants( // assert the invariant at the end of the loop body { - goto_programt::instructiont a = - goto_programt::make_assertion(invariant, loop_end->source_location); - a.source_location.set_comment("Check that loop invariant is preserved"); - goto_function.body.insert_before_swap(loop_end, a); - ++loop_end; + code_assertt assertion{invariant}; + assertion.add_source_location() = loop_end->source_location; + 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); } // change the back edge into assume(false) or assume(guard) @@ -158,15 +164,6 @@ static void check_apply_invariants( loop_end->set_condition(boolean_negate(loop_end->get_condition())); } -void code_contractst::convert_to_goto( - const codet &code, - const irep_idt &mode, - goto_programt &program) -{ - goto_convertt converter(symbol_table, log.get_message_handler()); - converter.goto_convert(code, program, mode); -} - bool code_contractst::has_contract(const irep_idt fun_name) { const symbolt &function_symbol = ns.lookup(fun_name); @@ -322,7 +319,7 @@ code_contractst::create_ensures_instruction( // Create instructions corresponding to the ensures clause goto_programt ensures_program; - convert_to_goto(expression, mode, ensures_program); + converter.goto_convert(expression, ensures_program, mode); // return a pair containing: // 1. instructions corresponding to the ensures clause @@ -424,10 +421,10 @@ bool code_contractst::apply_function_contract( if(requires.is_not_nil()) { goto_programt assertion; - convert_to_goto( + converter.goto_convert( code_assertt(requires), - symbol_table.lookup_ref(function).mode, - assertion); + assertion, + symbol_table.lookup_ref(function).mode); auto lines_to_iterate = assertion.instructions.size(); goto_program.insert_before_swap(target, assertion); std::advance(target, lines_to_iterate); @@ -483,15 +480,21 @@ bool code_contractst::apply_function_contract( } void code_contractst::apply_loop_contract( + 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 + // 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( - goto_function, local_may_alias, loop.first, loop.second); + goto_function, + local_may_alias, + loop.first, + loop.second, + symbol_table.lookup_ref(function_name).mode); } const symbolt &code_contractst::new_tmp_symbol( @@ -966,8 +969,8 @@ void code_contractst::add_contract_check( replace(requires_cond); goto_programt assumption; - convert_to_goto( - code_assumet(requires_cond), function_symbol.mode, assumption); + converter.goto_convert( + code_assumet(requires_cond), assumption, function_symbol.mode); check.destructive_append(assumption); } @@ -1078,7 +1081,7 @@ bool code_contractst::enforce_contracts() if(has_contract(goto_function.first)) funs_to_enforce.insert(id2string(goto_function.first)); else - apply_loop_contract(goto_function.second); + apply_loop_contract(goto_function.first, goto_function.second); } return enforce_contracts(funs_to_enforce); } @@ -1098,7 +1101,7 @@ bool code_contractst::enforce_contracts( << messaget::eom; continue; } - apply_loop_contract(goto_function->second); + apply_loop_contract(goto_function->first, goto_function->second); if(!has_contract(fun)) { diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index e4e18d588fb..665c29a8984 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -19,6 +19,7 @@ Date: February 2016 #include #include +#include #include #include @@ -26,7 +27,10 @@ Date: February 2016 #include #include +#include "loop_utils.h" + class assigns_clauset; +class local_may_aliast; class replace_symbolt; class code_contractst @@ -36,8 +40,9 @@ class code_contractst : ns(goto_model.symbol_table), symbol_table(goto_model.symbol_table), goto_functions(goto_model.goto_functions), - temporary_counter(0), - log(log) + log(log), + converter(symbol_table, log.get_message_handler()) + { } @@ -89,26 +94,27 @@ class code_contractst const irep_idt &function_id, const irep_idt &mode); + void check_apply_invariants( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop, + const irep_idt &mode); + namespacet ns; protected: symbol_tablet &symbol_table; goto_functionst &goto_functions; - unsigned temporary_counter; messaget &log; + goto_convertt converter; std::unordered_set summarized; /// \brief Enforce contract of a single function bool enforce_contract(const std::string &); - /// \brief Create goto instructions based on code and add them to program. - void convert_to_goto( - const codet &code, - const irep_idt &mode, - goto_programt &program); - /// Insert assertion statements into the goto program to ensure that /// assigned memory is within the assignable memory frame. bool add_pointer_checks(const std::string &); @@ -159,7 +165,9 @@ class code_contractst const exprt &lhs, std::vector &aliasable_references); - void apply_loop_contract(goto_functionst::goto_functiont &goto_function); + void apply_loop_contract( + const irep_idt &function_name, + goto_functionst::goto_functiont &goto_function); /// \brief Does the named function have a contract? bool has_contract(const irep_idt); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index e35617b1ea9..20bc2c240b4 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -868,13 +868,11 @@ void goto_convertt::convert_loop_invariant( if(invariant.is_nil()) return; - goto_programt no_sideeffects; - clean_expr(invariant, no_sideeffects, mode); - - INVARIANT_WITH_DIAGNOSTICS( - no_sideeffects.instructions.empty(), - "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); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 36fb4e550ad..5244983d39c 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -97,7 +97,6 @@ class goto_convertt:public messaget void rewrite_boolean(exprt &dest); - static bool has_sideeffect(const exprt &expr); static bool has_function_call(const exprt &expr); void remove_side_effect(