diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c index 2208c1b74c6e..1b37be10878e 100644 --- a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c @@ -1,8 +1,8 @@ void foo() { - int nondet_var; - int __VERIFIER_var; - int __CPROVER_var; + int nondet_var = nondet_int(); + int __VERIFIER_var = nondet_int(); + int __CPROVER_var = nondet_int(); for(int i = 10; i > 0; i--) // clang-format off __CPROVER_assigns(i) diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c index fa1b4a5b6224..146a02bdb926 100644 --- a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c +++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c @@ -1,8 +1,8 @@ void foo() { - int nondet_var; - int __VERIFIER_var; - int __CPROVER_var; + int nondet_var = nondet_int(); + int __VERIFIER_var = nondet_int(); + int __CPROVER_var = nondet_int(); for(int i = 10; i > 0; i--) // clang-format off __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var) diff --git a/regression/contracts-dfcc/invar_loop-entry_check/main.c b/regression/contracts-dfcc/invar_loop-entry_check/main.c index 5e8b4bb5a004..e4e05dddeb6a 100644 --- a/regression/contracts-dfcc/invar_loop-entry_check/main.c +++ b/regression/contracts-dfcc/invar_loop-entry_check/main.c @@ -12,7 +12,7 @@ void main() x1 = &z1; while(y1 > 0) - __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1)) + __CPROVER_loop_invariant(y1 >= 0 && *x1 == __CPROVER_loop_entry(*x1)) { --y1; *x1 = *x1 + 1; @@ -24,7 +24,7 @@ void main() x2 = z2; while(y2 > 0) - __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2)) + __CPROVER_loop_invariant(y2 >= 0 && x2 == __CPROVER_loop_entry(x2)) { --y2; x2 = x2 + 1; @@ -34,11 +34,12 @@ void main() int y3; s s0, s1, *s2 = &s0; + s0.n = nondet_int(); s2->n = malloc(sizeof(int)); s1.n = s2->n; while(y3 > 0) - __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n)) + __CPROVER_loop_invariant(y3 >= 0 && s2->n == __CPROVER_loop_entry(s2->n)) { --y3; s0.n = s0.n + 1; diff --git a/regression/contracts-dfcc/invar_loop-entry_check/test.desc b/regression/contracts-dfcc/invar_loop-entry_check/test.desc index 22d1c09a32aa..635d418e08f1 100644 --- a/regression/contracts-dfcc/invar_loop-entry_check/test.desc +++ b/regression/contracts-dfcc/invar_loop-entry_check/test.desc @@ -11,10 +11,10 @@ main.c ^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$ ^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$ -^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$ -^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$ -^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+] line 41 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+] line 41 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+] line 41 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+] line 41 Check step was unwound for loop .*: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$ ^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$ diff --git a/regression/contracts-dfcc/invar_loop-entry_fail/main.c b/regression/contracts-dfcc/invar_loop-entry_fail/main.c index e902c8ab8416..208bc014f8a2 100644 --- a/regression/contracts-dfcc/invar_loop-entry_fail/main.c +++ b/regression/contracts-dfcc/invar_loop-entry_fail/main.c @@ -6,7 +6,7 @@ void main() x = z; while(y > 0) - __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x)) + __CPROVER_loop_invariant(y >= 0 && x == __CPROVER_loop_entry(x)) { --y; x = x + 1; diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/main.c b/regression/contracts-dfcc/loop_assigns_inference-02/main.c index 063b47929ee4..adf6da2dec06 100644 --- a/regression/contracts-dfcc/loop_assigns_inference-02/main.c +++ b/regression/contracts-dfcc/loop_assigns_inference-02/main.c @@ -10,11 +10,14 @@ void main() void foo() { int *b = malloc(SIZE * sizeof(int)); + int *j; for(unsigned i = 0; i < SIZE; i++) // clang-format off __CPROVER_loop_invariant(i <= SIZE) // clang-format on { + j = malloc(SIZE * sizeof(int)); b[i] = 1; + free(j); } } diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc index 3ac2c189a995..7c6886eef4f0 100644 --- a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc +++ b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc @@ -3,12 +3,12 @@ main.c --no-malloc-may-fail --dfcc main --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ -^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ -^\[foo.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ -^\[foo.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line 14 Check invariant after step for loop .*: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line 14 Check step was unwound for loop .*: SUCCESS$ ^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/loop_assigns_inference-03/main.c b/regression/contracts-dfcc/loop_assigns_inference-03/main.c index c969cde10a0a..232a4db0c40d 100644 --- a/regression/contracts-dfcc/loop_assigns_inference-03/main.c +++ b/regression/contracts-dfcc/loop_assigns_inference-03/main.c @@ -7,7 +7,7 @@ void main() int b[SIZE]; for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_loop_invariant(i <= SIZE) + __CPROVER_loop_invariant((i == 0 || b[0] == 1) && i <= SIZE) // clang-format on { b[i] = 1; 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 d20a80dc7599..42a036c54c5b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -253,26 +253,6 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns) return false; } -/// Collect identifiers that are local to this loop only -/// (excluding nested loop). -static std::unordered_set gen_loop_locals_set( - const dfcc_loop_nesting_grapht &loop_nesting_graph, - const std::size_t loop_id) -{ - std::unordered_set loop_locals; - for(const auto &target : loop_nesting_graph[loop_id].instructions) - { - auto loop_id_opt = dfcc_get_loop_id(target); - if( - target->is_decl() && loop_id_opt.has_value() && - loop_id_opt.value() == loop_id) - { - loop_locals.insert(target->decl_symbol().get_identifier()); - } - } - return loop_locals; -} - /// Compute subset of locals that must be tracked in the loop's write set. /// A local must be tracked if it is dirty or if it may be assigned by one /// of the inner loops. @@ -329,6 +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 bool check_side_effect, message_handlert &message_handler, @@ -381,7 +362,7 @@ static struct contract_clausest default_loop_contract_clauses( { // infer assigns clause targets if none given auto inferred = dfcc_infer_loop_assigns( - local_may_alias, loop.instructions, loop.head->source_location(), ns); + 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 {"; @@ -416,6 +397,7 @@ 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, @@ -424,8 +406,25 @@ static dfcc_loop_infot gen_dfcc_loop_info( dfcc_libraryt &library, symbol_table_baset &symbol_table) { - std::unordered_set loop_locals = - gen_loop_locals_set(loop_nesting_graph, loop_id); + const namespacet ns(symbol_table); + std::unordered_set loop_locals = gen_loop_locals_set( + function_id, + goto_function, + loop_nesting_graph[loop_id], + message_handler, + ns); + + // Exclude locals of inner nested loops. + for(const auto &inner_loop : loop_nesting_graph.get_predecessors(loop_id)) + { + INVARIANT( + loop_info_map.find(inner_loop) != loop_info_map.end(), + "DFCC should gen_dfcc_loop_info for inner loops first."); + for(const auto &inner_local : loop_info_map.at(inner_loop).local) + { + loop_locals.erase(inner_local); + } + } std::unordered_set loop_tracked = gen_tracked_set( loop_nesting_graph.get_predecessors(loop_id), @@ -433,11 +432,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, + goto_function, local_may_alias, check_side_effect, message_handler, @@ -559,6 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( loop_nesting_graph, loop_id, function_id, + goto_function, loop_info_map, dirty, local_may_alias, 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 611b09ffbc56..96c73eed241b 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,6 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include #include #include @@ -46,23 +47,127 @@ depends_on(const exprt &expr, std::unordered_set identifiers) return false; } +/// Collect identifiers that are local to this loop. +/// A identifier is or is equivalent to a loop local if +/// 1. it is declared inside the loop, or +/// 2. there is no write or read of it outside the loop. +/// 3. it is not used in loop contracts. +std::unordered_set gen_loop_locals_set( + const irep_idt &function_id, + goto_functiont &goto_function, + const dfcc_loop_nesting_graph_nodet &loop_node, + message_handlert &message_handler, + const namespacet &ns) +{ + std::unordered_set loop_locals; + std::unordered_set non_loop_locals; + + const auto &loop = loop_node.instructions; + + // All identifiers declared outside the loop. + std::unordered_set non_loop_decls; + // Ranges of all read/write outside the loop. + rw_range_sett non_loop_rw_range_set(ns, message_handler); + + Forall_goto_program_instructions(i_it, goto_function.body) + { + // All variables declared in loops are loop locals. + if(i_it->is_decl() && loop.contains(i_it)) + { + loop_locals.insert(i_it->decl_symbol().get_identifier()); + } + // Record all other declared variables and their ranges. + else if(i_it->is_decl()) + { + non_loop_decls.insert(i_it->decl_symbol().get_identifier()); + } + // Record all writing/reading outside the loop. + else if( + (i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it)) + { + goto_rw(function_id, i_it, non_loop_rw_range_set); + } + } + + // Check if declared variables are loop locals. + for(const auto &decl_id : non_loop_decls) + { + bool is_loop_local = true; + // No write to the declared variable. + for(const auto &writing_rw : non_loop_rw_range_set.get_w_set()) + { + if(decl_id == writing_rw.first) + { + is_loop_local = false; + break; + } + } + + // No read to the declared variable. + for(const auto &writing_rw : non_loop_rw_range_set.get_r_set()) + { + if(decl_id == writing_rw.first) + { + is_loop_local = false; + break; + } + } + + const auto latch_target = loop_node.latch; + + // Loop locals are not used in loop contracts. + for(const auto &id : + find_symbol_identifiers(get_loop_assigns(latch_target))) + { + if(decl_id == id) + { + is_loop_local = false; + break; + } + } + + for(const auto &id : + find_symbol_identifiers(get_loop_invariants(latch_target))) + { + if(decl_id == id) + { + is_loop_local = false; + break; + } + } + + for(const auto &id : + find_symbol_identifiers(get_loop_decreases(latch_target))) + { + if(decl_id == id) + { + is_loop_local = false; + break; + } + } + + // Collect all loop locals. + if(is_loop_local) + loop_locals.insert(decl_id); + } + + return loop_locals; +} + assignst dfcc_infer_loop_assigns( const local_may_aliast &local_may_alias, - const loopt &loop_instructions, - const source_locationt &loop_head_location, + goto_functiont &goto_function, + const dfcc_loop_nesting_graph_nodet &loop, + message_handlert &message_handler, const namespacet &ns) { // infer assignst assigns; - infer_loop_assigns(local_may_alias, loop_instructions, assigns); + infer_loop_assigns(local_may_alias, loop.instructions, assigns); // compute locals - std::unordered_set loop_locals; - for(const auto &target : loop_instructions) - { - if(target->is_decl()) - loop_locals.insert(target->decl_symbol().get_identifier()); - } + std::unordered_set loop_locals = + gen_loop_locals_set(irep_idt(), goto_function, loop, message_handler, ns); // widen or drop targets that depend on loop-locals or are non-constant, // ie. depend on other locations assigned by the loop. 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 ac7738690097..259a5b0ff475 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 @@ -14,16 +14,29 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include + +#include "dfcc_loop_nesting_graph.h" + 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( const local_may_aliast &local_may_alias, - const loopt &loop_instructions, - const source_locationt &loop_head_location, + 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, + goto_functiont &goto_function, + const dfcc_loop_nesting_graph_nodet &loop, + message_handlert &message_handler, const namespacet &ns); #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 7f6acd75e7f8..4d896a5d0cce 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -298,6 +298,13 @@ dfcc_instrument_loopt::add_prehead_instructions( code_function_callt call = library.write_set_create_call( addr_of_loop_write_set, from_integer(assigns.size(), size_type()), + from_integer(0, size_type()), + false_exprt(), + false_exprt(), + false_exprt(), + false_exprt(), + true_exprt(), + true_exprt(), loop_head_location); pre_loop_head_instrs.add( goto_programt::make_function_call(call, loop_head_location));