diff --git a/regression/contracts-dfcc/loop_assigns_inference-01/test.desc b/regression/contracts-dfcc/loop_assigns_inference-01/test.desc index da609994d99..4200eeb2ad6 100644 --- a/regression/contracts-dfcc/loop_assigns_inference-01/test.desc +++ b/regression/contracts-dfcc/loop_assigns_inference-01/test.desc @@ -1,18 +1,18 @@ -KNOWNBUG +CORE dfcc-only main.c ---dfcc main --apply-loop-contracts +--dfcc main --apply-loop-contracts _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ ^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ ^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ ^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$ ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- This test checks loop locals are correctly removed during assigns inference so that the assign clause is correctly inferred. -This test failed when using dfcc for loop contracts. diff --git a/regression/contracts-dfcc/loop_assigns_inference-04/main.c b/regression/contracts-dfcc/loop_assigns_inference-04/main.c new file mode 100644 index 00000000000..fd6886eef0a --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-04/main.c @@ -0,0 +1,22 @@ +struct hole +{ + int pos; +}; + +void set_len(struct hole *h, unsigned long int new_len) +{ + h->pos = new_len; +} + +int main() +{ + int i = 0; + struct hole h; + h.pos = 0; + for(i = 0; i < 5; i++) + // __CPROVER_assigns(h.pos, i) + __CPROVER_loop_invariant(h.pos == i) + { + set_len(&h, h.pos + 1); + } +} diff --git a/regression/contracts-dfcc/loop_assigns_inference-04/test.desc b/regression/contracts-dfcc/loop_assigns_inference-04/test.desc new file mode 100644 index 00000000000..86e1d3951ad --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-04/test.desc @@ -0,0 +1,14 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$ +^\[set_len.assigns.\d+\] line \d+ Check that h\-\>pos is assignable: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks assigns h->pos is inferred correctly. diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/main.c b/regression/contracts/invar_havoc_dynamic_array_const_idx/main.c index 10d2c7a1904..69d7285b4c2 100644 --- a/regression/contracts/invar_havoc_dynamic_array_const_idx/main.c +++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/main.c @@ -10,7 +10,7 @@ void main() data[4] = 0; for(unsigned i = 0; i < SIZE; i++) - __CPROVER_loop_invariant(i <= SIZE) + __CPROVER_assigns(data[1], i) __CPROVER_loop_invariant(i <= SIZE) { data[1] = i; } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 42a036c54c5..3330c6f2617 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -309,8 +309,7 @@ static struct contract_clausest default_loop_contract_clauses( const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, - goto_functiont &goto_function, - local_may_aliast &local_may_alias, + const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, const namespacet &ns) @@ -361,13 +360,11 @@ static struct contract_clausest default_loop_contract_clauses( else { // infer assigns clause targets if none given - auto inferred = dfcc_infer_loop_assigns( - local_may_alias, goto_function, loop, message_handler, ns); log.warning() << "No assigns clause provided for loop " << function_id << "." << loop.latch->loop_number << " at " << loop.head->source_location() << ". The inferred set {"; bool first = true; - for(const auto &expr : inferred) + for(const auto &expr : inferred_assigns) { if(!first) { @@ -379,7 +376,7 @@ static struct contract_clausest default_loop_contract_clauses( log.warning() << "} might be incomplete or imprecise, please provide an " "assigns clause if the analysis fails." << messaget::eom; - result.assigns.swap(inferred); + result.assigns = inferred_assigns; } if(result.decreases_clauses.empty()) @@ -400,7 +397,7 @@ static dfcc_loop_infot gen_dfcc_loop_info( goto_functiont &goto_function, const std::map &loop_info_map, dirtyt &dirty, - local_may_aliast &local_may_alias, + const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, dfcc_libraryt &library, @@ -436,8 +433,7 @@ static dfcc_loop_infot gen_dfcc_loop_info( loop_nesting_graph, loop_id, function_id, - goto_function, - local_may_alias, + inferred_assigns, check_side_effect, message_handler, ns); @@ -488,6 +484,7 @@ static dfcc_loop_infot gen_dfcc_loop_info( } dfcc_cfg_infot::dfcc_cfg_infot( + goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, @@ -506,6 +503,9 @@ dfcc_cfg_infot::dfcc_cfg_infot( // Clean up possible fake loops that are due to do { ... } while(0); simplify_gotos(goto_program, ns); + // From loop number to the inferred loop assigns. + std::map inferred_loop_assigns_map; + if(loop_contract_config.apply_loop_contracts) { messaget log(message_handler); @@ -526,9 +526,23 @@ dfcc_cfg_infot::dfcc_cfg_infot( auto topsorted = loop_nesting_graph.topsort(); + bool has_loops_with_contracts = false; for(const auto idx : topsorted) { topsorted_loops.push_back(idx); + has_loops_with_contracts |= has_contract( + loop_nesting_graph[idx].latch, loop_contract_config.check_side_effect); + } + + // We infer loop assigns for all loops in the function. + if(has_loops_with_contracts) + { + dfcc_infer_loop_assigns_for_function( + inferred_loop_assigns_map, + goto_model.goto_functions, + goto_function, + message_handler, + ns); } } @@ -548,10 +562,11 @@ dfcc_cfg_infot::dfcc_cfg_infot( // generate dfcc_cfg_loop_info for loops and add to loop_info_map dirtyt dirty(goto_function); - local_may_aliast local_may_alias(goto_function); for(const auto &loop_id : topsorted_loops) { + auto inferred_loop_assigns = + inferred_loop_assigns_map[loop_nesting_graph[loop_id].latch->loop_number]; loop_info_map.insert( {loop_id, gen_dfcc_loop_info( @@ -561,7 +576,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( goto_function, loop_info_map, dirty, - local_may_alias, + inferred_loop_assigns, loop_contract_config.check_side_effect, message_handler, library, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index 8de5666a6b7..59583869780 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -21,6 +21,7 @@ Date: March 2023 #include #include +#include #include #include @@ -242,6 +243,7 @@ class dfcc_cfg_infot { public: dfcc_cfg_infot( + goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp index aff88ec9139..c4e7026741c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp @@ -13,10 +13,13 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include + #include #include #include +#include "dfcc_loop_nesting_graph.h" #include "dfcc_root_object.h" /// Builds a call expression `object_whole(expr)` @@ -154,10 +157,75 @@ std::unordered_set gen_loop_locals_set( return loop_locals; } -assignst dfcc_infer_loop_assigns( +/// Append all identifiers in `expr` into `identifiers`. +static void +append_ids_in_expr(const exprt &expr, std::unordered_set &identifiers) +{ + auto ids = find_symbol_identifiers(expr); + identifiers.insert(ids.begin(), ids.end()); +} + +/// Find all identifiers in `src`. +static std::unordered_set +find_symbol_identifiers(const goto_programt &src) +{ + std::unordered_set identifiers; + forall_goto_program_instructions(i_it, src) + { + // compute forward edges first + switch(i_it->type()) + { + case ASSERT: + case ASSUME: + case GOTO: + append_ids_in_expr(i_it->condition(), identifiers); + break; + + case FUNCTION_CALL: + append_ids_in_expr(i_it->call_lhs(), identifiers); + for(const auto &e : i_it->call_arguments()) + append_ids_in_expr(e, identifiers); + break; + case ASSIGN: + case OTHER: + + case SET_RETURN_VALUE: + case DECL: + case DEAD: + for(const auto &e : i_it->code().operands()) + { + append_ids_in_expr(e, identifiers); + } + break; + + case END_THREAD: + case END_FUNCTION: + case ATOMIC_BEGIN: + case ATOMIC_END: + case SKIP: + case LOCATION: + case CATCH: + case THROW: + case START_THREAD: + break; + case NO_INSTRUCTION_TYPE: + case INCOMPLETE_GOTO: + UNREACHABLE; + break; + } + } + return identifiers; +} + +/// Infer loop assigns in the given `loop`. Loop assigns should depend +/// on some identifiers in `candidate_targets`. `function_assigns_map` +/// contains the function contracts used to infer loop assigns of +/// function_call instructions. +static assignst dfcc_infer_loop_assigns_for_loop( const local_may_aliast &local_may_alias, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop, + const std::unordered_set &candidate_targets, message_handlert &message_handler, const namespacet &ns) { @@ -176,6 +244,12 @@ assignst dfcc_infer_loop_assigns( assignst result; for(const auto &expr : assigns) { + // Skip targets that only depend on non-visible identifiers. + if(!depends_on(expr, candidate_targets)) + { + continue; + } + if(depends_on(expr, loop_locals)) { // Target depends on loop locals, attempt widening to the root object @@ -196,7 +270,9 @@ assignst dfcc_infer_loop_assigns( { address_of_exprt address_of_expr(expr); address_of_expr.add_source_location() = expr.source_location(); - if(!is_constant(address_of_expr)) + // Widen assigns targets to object_whole if `expr` is a dereference or + // with constant address. + if(expr.id() == ID_dereference || !is_constant(address_of_expr)) { // Target address is not constant, widening to the whole object result.emplace(make_object_whole_call_expr(address_of_expr, ns)); @@ -210,3 +286,105 @@ assignst dfcc_infer_loop_assigns( return result; } + +/// Remove assignments to `__CPROVER_dead_object` to avoid aliasing all targets +/// that are assigned to `__CPROVER_dead_object`. +static void remove_dead_object_assignment(goto_functiont &goto_function) +{ + Forall_goto_program_instructions(i_it, goto_function.body) + { + if(i_it->is_assign()) + { + auto &lhs = i_it->assign_lhs(); + + if( + lhs.id() == ID_symbol && + to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object") + { + i_it->turn_into_skip(); + } + } + } +} + +void dfcc_infer_loop_assigns_for_function( + std::map &inferred_loop_assigns_map, + goto_functionst &goto_functions, + goto_functiont &goto_function, + message_handlert &message_handler, + const namespacet &ns) +{ + messaget log(message_handler); + + // Collect all candidate targets---identifiers visible in `goto_function`. + const auto candidate_targets = find_symbol_identifiers(goto_function.body); + + // We infer loop assigns based on the copy of `goto_function`. + goto_functiont goto_function_copy; + goto_function_copy.copy_from(goto_function); + + // Map from targett in `goto_function_copy` to loop number. + std:: + unordered_map + loop_number_map; + + // Build the loop id map before inlining attempt. So that we can later + // distinguish loops in the original body and loops added by inlining. + const auto loop_nesting_graph = + build_loop_nesting_graph(goto_function_copy.body); + { + auto topsorted = loop_nesting_graph.topsort(); + // skip function without loop. + if(topsorted.empty()) + return; + + for(const auto id : topsorted) + { + loop_number_map.emplace( + loop_nesting_graph[id].head, loop_nesting_graph[id].latch->loop_number); + } + } + + // We avoid inlining `malloc` and `free` whose variables are not assigns. + auto malloc_body = goto_functions.function_map.extract(irep_idt("malloc")); + auto free_body = goto_functions.function_map.extract(irep_idt("free")); + + // Inline all function calls in goto_function_copy. + goto_program_inline( + goto_functions, goto_function_copy.body, ns, log.get_message_handler()); + // Update the body to make sure all goto correctly jump to valid targets. + goto_function_copy.body.update(); + // Build the loop graph after inlining. + const auto inlined_loop_nesting_graph = + build_loop_nesting_graph(goto_function_copy.body); + + // Alias analysis. + remove_dead_object_assignment(goto_function_copy); + local_may_aliast local_may_alias(goto_function_copy); + + auto inlined_topsorted = inlined_loop_nesting_graph.topsort(); + + for(const auto inlined_id : inlined_topsorted) + { + // We only infer loop assigns for loops in the original function. + if( + loop_number_map.find(inlined_loop_nesting_graph[inlined_id].head) != + loop_number_map.end()) + { + const auto loop_number = + loop_number_map[inlined_loop_nesting_graph[inlined_id].head]; + const auto inlined_loop = inlined_loop_nesting_graph[inlined_id]; + + inferred_loop_assigns_map[loop_number] = dfcc_infer_loop_assigns_for_loop( + local_may_alias, + goto_function_copy, + inlined_loop, + candidate_targets, + message_handler, + ns); + } + } + // Restore the function boyd of `malloc` and `free`. + goto_functions.function_map.insert(std::move(malloc_body)); + goto_functions.function_map.insert(std::move(free_body)); +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h index 259a5b0ff47..72be4ea00a5 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h @@ -22,15 +22,6 @@ class messaget; class namespacet; class message_handlert; -// \brief Infer assigns clause targets for a loop from its instructions and a -// may alias analysis at the function level. -assignst dfcc_infer_loop_assigns( - const local_may_aliast &local_may_alias, - goto_functiont &goto_function, - const dfcc_loop_nesting_graph_nodet &loop_instructions, - message_handlert &message_handler, - const namespacet &ns); - /// Collect identifiers that are local to `loop`. std::unordered_set gen_loop_locals_set( const irep_idt &function_id, @@ -39,4 +30,15 @@ std::unordered_set gen_loop_locals_set( message_handlert &message_handler, const namespacet &ns); +/// \brief Infer assigns clause targets for loops in `goto_function` from their +/// instructions and an alias analysis at the function level (with inlining), +/// and store the result in `inferred_loop_assigns_map`, a map from loop +/// numbers to the set of inferred assigns targets. +void dfcc_infer_loop_assigns_for_function( + std::map &inferred_loop_assigns_map, + goto_functionst &goto_functions, + goto_functiont &goto_function, + message_handlert &message_handler, + const namespacet &ns); + #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index b37d6a7c55c..5e0fdd92c5e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -399,6 +399,7 @@ void dfcc_instrumentt::instrument_goto_program( // build control flow graph information dfcc_cfg_infot cfg_info( + goto_model, function_id, goto_function, write_set, @@ -448,6 +449,7 @@ void dfcc_instrumentt::instrument_goto_function( // build control flow graph information dfcc_cfg_infot cfg_info( + goto_model, function_id, goto_function, write_set,