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/loop_assigns_inference-04/main.c b/regression/contracts/loop_assigns_inference-04/main.c new file mode 100644 index 00000000000..fd6886eef0a --- /dev/null +++ b/regression/contracts/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/loop_assigns_inference-04/test.desc b/regression/contracts/loop_assigns_inference-04/test.desc new file mode 100644 index 00000000000..4a019f2d1b2 --- /dev/null +++ b/regression/contracts/loop_assigns_inference-04/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks assigns h->pos is inferred correctly. 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 d20a80dc759..b72b2537343 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -329,7 +329,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, - local_may_aliast &local_may_alias, + const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, const namespacet &ns) @@ -380,13 +380,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, loop.instructions, loop.head->source_location(), 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) { @@ -398,7 +396,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()) @@ -416,14 +414,16 @@ static dfcc_loop_infot gen_dfcc_loop_info( const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, + 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, symbol_table_baset &symbol_table) { + const namespacet ns(symbol_table); std::unordered_set loop_locals = gen_loop_locals_set(loop_nesting_graph, loop_id); @@ -433,12 +433,11 @@ static dfcc_loop_infot gen_dfcc_loop_info( dirty, loop_info_map); - const namespacet ns(symbol_table); struct contract_clausest contract_clauses = default_loop_contract_clauses( loop_nesting_graph, loop_id, function_id, - local_may_alias, + inferred_assigns, check_side_effect, message_handler, ns); @@ -489,6 +488,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, @@ -507,6 +507,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); @@ -527,9 +530,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); } } @@ -549,19 +566,21 @@ 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( loop_nesting_graph, loop_id, function_id, + 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 611b09ffbc5..e8259fa2e07 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,9 +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)` @@ -46,10 +50,73 @@ depends_on(const exprt &expr, std::unordered_set identifiers) return false; } -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; +} + +assignst dfcc_infer_loop_assigns_for_loop( const local_may_aliast &local_may_alias, + goto_functiont &goto_function, const loopt &loop_instructions, + const std::unordered_set &candidate_targets, const source_locationt &loop_head_location, + message_handlert &message_handler, const namespacet &ns) { // infer @@ -105,3 +172,102 @@ 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. + 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()); + 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.instructions, + candidate_targets, + inlined_loop.head->source_location(), + message_handler, + ns); + } + } + 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 ac773869009..3e33fb089f7 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 @@ -17,13 +17,26 @@ Author: Remi Delmas, delmasrd@amazon.com class source_locationt; 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( +assignst dfcc_infer_loop_assigns_for_loop( const local_may_aliast &local_may_alias, + goto_functiont &goto_function, const loopt &loop_instructions, + const std::unordered_set &candidate_targets, const source_locationt &loop_head_location, + message_handlert &message_handler, + const namespacet &ns); + +// \brief Infer assigns clause targets for loops in `goto_function` from their +// instructions and a may alias analysis at the function level (with inlining). +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, diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index f05998a023a..e099b8c28c7 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -53,38 +53,90 @@ void get_assigns_lhs( assignst &assigns, std::function predicate) { - if( - (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) && - predicate(lhs)) + assignst new_assigns; + + if(lhs.id() == ID_symbol || lhs.id() == ID_index) { - assigns.insert(lhs); + // All variables `v` and their indexing expressions `v[idx]` are assigns. + new_assigns.insert(lhs); + } + else if(lhs.id() == ID_member) + { + auto op = to_member_expr(lhs).struct_op(); + auto component_name = to_member_expr(lhs).get_component_name(); + + // Insert expressions of form `v.member`. + if(op.id() == ID_symbol) + { + new_assigns.insert(lhs); + } + // For expressions of form `v->member`, insert all targets `u->member`, + // where `u` and `v` alias. + else if(op.id() == ID_dereference) + { + const pointer_arithmetict ptr(to_dereference_expr(op).pointer()); + for(const auto &mod : local_may_alias.get(t, ptr.pointer)) + { + if(mod.id() == ID_unknown) + { + continue; + } + const exprt typed_mod = + typecast_exprt::conditional_cast(mod, ptr.pointer.type()); + exprt to_insert; + if(ptr.offset.is_nil()) + { + // u->member + to_insert = member_exprt( + dereference_exprt{typed_mod}, component_name, lhs.type()); + } + else + { + // (u+offset)->member + to_insert = member_exprt( + dereference_exprt{plus_exprt{typed_mod, ptr.offset}}, + component_name, + lhs.type()); + } + new_assigns.insert(to_insert); + } + } } else if(lhs.id() == ID_dereference) { + // All dereference `*v` and their alias `*u` are assigns. const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer()); for(const auto &mod : local_may_alias.get(t, ptr.pointer)) { - const typecast_exprt typed_mod{mod, ptr.pointer.type()}; if(mod.id() == ID_unknown) { continue; } + const exprt typed_mod = + typecast_exprt::conditional_cast(mod, ptr.pointer.type()); exprt to_insert; if(ptr.offset.is_nil()) to_insert = dereference_exprt{typed_mod}; else to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}}; - if(predicate(to_insert)) - assigns.insert(std::move(to_insert)); + new_assigns.insert(std::move(to_insert)); } } else if(lhs.id() == ID_if) { const if_exprt &if_expr = to_if_expr(lhs); - get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns); - get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns); + get_assigns_lhs( + local_may_alias, t, if_expr.true_case(), assigns, predicate); + get_assigns_lhs( + local_may_alias, t, if_expr.false_case(), assigns, predicate); } + + std::copy_if( + new_assigns.begin(), + new_assigns.end(), + std::inserter(assigns, assigns.begin()), + predicate); } void get_assigns(