diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_05/main.c b/regression/goto-synthesizer/loop_contracts_synthesis_05/main.c new file mode 100644 index 00000000000..bc16e35563a --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_05/main.c @@ -0,0 +1,51 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + __CPROVER_assume(b != NULL); + + b->data = malloc(SIZE); + __CPROVER_assume(b->data != NULL); + + b->data[5] = 0; + unsigned result = 0; + + unsigned arr[3] = {0, 0, 0}; + + for(unsigned int i = 0; i < SIZE; i++) + // clang-format off + // __CPROVER_assigns(i, result) + // clang-format on + { + result += 1; + } + + for(unsigned int i = 0; i < SIZE; i++) + // clang-format off + // __CPROVER_assigns(i, arr[0]) + // clang-format on + { + arr[0] += 1; + } + + for(unsigned j = 0; j < SIZE; j++) + // __CPROVER_assigns(j, __CPROVER_POINTER_OBJECT(b->data)) + { + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + // __CPROVER_assigns(i, j, __CPROVER_POINTER_OBJECT(b->data)) + // clang-format on + { + b->data[i] = 1; + } + } +} diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_05/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_05/test.desc new file mode 100644 index 00000000000..d8c28eaf4cb --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_05/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--pointer-check +^EXIT=0$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that result is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that arr\[(.*)0\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test is a variation of contracts/loop_assigns-01. +It shows that we can synthesize loop assigns pointer_object(b->data) that +cannot be inferred by goto-instrument. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6caea9b9955..28a620ed3d1 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1457,11 +1457,11 @@ void code_contractst::apply_loop_contracts( if(original_loop_number_map.count(it_instr) != 0) continue; - // Store loop number for - // ASSIGN ENTERED_LOOP = TRUE + // Store loop number for two type of instrumented instructions. + // ASSIGN ENTERED_LOOP = false --- head of transformed loops. + // ASSIGN ENTERED_LOOP = true --- end of transformed loops. if( - is_assignment_to_instrumented_variable(it_instr, ENTERED_LOOP) && - it_instr->assign_rhs() == true_exprt()) + is_transformed_loop_end(it_instr) || is_transformed_loop_head(it_instr)) { const auto &assign_lhs = expr_try_dynamic_cast(it_instr->assign_lhs()); diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index af2acd36785..8d97b354355 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -708,9 +708,14 @@ void instrument_spec_assignst::inclusion_check_assertion( comment += " is assignable"; source_location.set_comment(comment); - dest.add(goto_programt::make_assertion( - inclusion_check_full(car, allow_null_lhs, include_stack_allocated), - source_location)); + exprt inclusion_check = + inclusion_check_full(car, allow_null_lhs, include_stack_allocated); + // Record what target is checked. + auto &checked_assigns = + static_cast(inclusion_check.add(ID_checked_assigns)); + checked_assigns = car.target(); + + dest.add(goto_programt::make_assertion(inclusion_check, source_location)); } exprt instrument_spec_assignst::inclusion_check_single( diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 0d8f222b66b..1a357e2921d 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -448,14 +448,20 @@ void generate_history_variables_initialization( program.destructive_append(history); } +bool is_transformed_loop_head(const goto_programt::const_targett &target) +{ + // The head of a transformed loop is + // ASSIGN entered_loop = false + return is_assignment_to_instrumented_variable(target, ENTERED_LOOP) && + target->assign_rhs() == false_exprt(); +} + bool is_transformed_loop_end(const goto_programt::const_targett &target) { - // The end of the loop end of transformed loop is + // The end of a transformed loop is // ASSIGN entered_loop = true - if(!is_assignment_to_instrumented_variable(target, ENTERED_LOOP)) - return false; - - return target->assign_rhs() == true_exprt(); + return is_assignment_to_instrumented_variable(target, ENTERED_LOOP) && + target->assign_rhs() == true_exprt(); } bool is_assignment_to_instrumented_variable( diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 0741b9a2dae..b7ddab46397 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -210,7 +210,10 @@ void generate_history_variables_initialization( const irep_idt &mode, goto_programt &program); -/// Return true if `target` is the loop end of some transformed code. +/// Return true if `target` is the head of some transformed loop. +bool is_transformed_loop_head(const goto_programt::const_targett &target); + +/// Return true if `target` is the end of some transformed loop. bool is_transformed_loop_end(const goto_programt::const_targett &target); /// Return true if `target` is an assignment to an instrumented variable with diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 4ede29ac02d..9b1576281fe 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -32,6 +32,7 @@ Author: Qinheping Hu #include #include #include +#include #include #include #include @@ -93,11 +94,47 @@ optionst cegis_verifiert::get_options() return options; } -optionalt cegis_verifiert::get_cause_loop_id( +std::list +cegis_verifiert::get_cause_loop_id_for_assigns(const goto_tracet &goto_trace) +{ + std::list result; + + // We say a loop is the cause loop of an assignable-violation if the inclusion + // check is in the loop. + + // So we check what loops the last step of the trace is in. + // Transformed loop head: + // ASSIGN entered_loop = false + // Transformed loop end: + // ASSIGN entered_loop = true + for(const auto &step : goto_trace.steps) + { + // We are entering a loop. + if(is_transformed_loop_head(step.pc)) + { + result.push_front( + loop_idt(step.function_id, original_loop_number_map[step.pc])); + } + // We are leaving a loop. + else if(is_transformed_loop_end(step.pc)) + { + const loop_idt loop_id( + step.function_id, original_loop_number_map[step.pc]); + INVARIANT( + result.front() == loop_id, "Leaving a loop we haven't entered."); + result.pop_front(); + } + } + + INVARIANT(!result.empty(), "The assignable violation is not in a loop."); + return result; +} + +std::list cegis_verifiert::get_cause_loop_id( const goto_tracet &goto_trace, const goto_programt::const_targett violation) { - optionalt result; + std::list result; // build the dependence graph const namespacet ns(goto_model.symbol_table); @@ -165,7 +202,8 @@ optionalt cegis_verifiert::get_cause_loop_id( // if it is dependent on the loop havoc. if(reachable_set.count(dependence_graph[from].get_node_id())) { - result = loop_idt(step.function_id, original_loop_number_map[step.pc]); + result.push_back( + loop_idt(step.function_id, original_loop_number_map[step.pc])); return result; } } @@ -434,9 +472,12 @@ optionalt cegis_verifiert::verify() original_functions[fun_entry.first].copy_from(fun_entry.second.body); } - // Annotate the candidates tot the goto_model for checking. + // Annotate the candidates to the goto_model for checking. annotate_invariants(invariant_candidates, goto_model); + // Annotate assigns + annotate_assigns(assigns_map, goto_model); + // Control verbosity. // We allow non-error output message only when verbosity is set to at least 9. const unsigned original_verbosity = log.get_message_handler().get_verbosity(); @@ -495,15 +536,15 @@ optionalt cegis_verifiert::verify() if(property_it.second.status != property_statust::FAIL) continue; + // Store the violation that we want to fix with synthesized + // assigns/invariant. first_violation = property_it.first; - exprt violated_predicate = property_it.second.pc->condition(); - - // The pointer checked in the null-pointer-check violation. - exprt checked_pointer = true_exprt(); // Type of the violation cext::violation_typet violation_type = cext::violation_typet::cex_other; + // Decide the violation type from the description of violation + // The violation is a pointer OOB check. if((property_it.second.description.find( "dereference failure: pointer outside object bounds in") != @@ -516,11 +557,6 @@ optionalt cegis_verifiert::verify() if(property_it.second.description.find("pointer NULL") != std::string::npos) { violation_type = cext::violation_typet::cex_null_pointer; - checked_pointer = property_it.second.pc->condition() - .operands()[0] - .operands()[1] - .operands()[0]; - INVARIANT(checked_pointer.id() == ID_symbol, "Checking pointer symbol"); } // The violation is a loop-invariant-preservation check. @@ -537,51 +573,97 @@ optionalt cegis_verifiert::verify() violation_type = cext::violation_typet::cex_not_hold_upon_entry; } - // The loop which could be the cause of the violation. - // We say a loop is the cause loop if the violated predicate is dependent - // upon the write set of the loop. - optionalt cause_loop_id = get_cause_loop_id( - checker->get_traces()[property_it.first], property_it.second.pc); + // The violation is an assignable check. + if(property_it.second.description.find("assignable") != std::string::npos) + { + violation_type = cext::violation_typet::cex_assignable; + } - if(!cause_loop_id.has_value()) + // Compute the cause loop---the loop for which we synthesize loop contracts, + // and the counterexample. + + // If the violation is an assignable check, we synthesize assigns targets. + // In the case, cause loops are all loops the violation is in. We keep + // adding the new assigns target to the most-inner loop that does not + // contain the new target until the assignable violation is resolved. + + // For other cases, we synthesize loop invariant clauses. We synthesize + // invariants for one loop at a time. So we return only the first cause loop + // although there can be multiple ones. + + log.debug() << "Start to compute cause loop ids." << messaget::eom; + + const auto &trace = checker->get_traces()[property_it.first]; + + // Doing assigns-synthesis or invariant-synthesis + if(violation_type == cext::violation_typet::cex_assignable) + { + cext result(violation_type); + result.cause_loop_ids = get_cause_loop_id_for_assigns(trace); + result.checked_pointer = static_cast( + property_it.second.pc->condition().find(ID_checked_assigns)); + restore_functions(); + return result; + } + + // We construct the full counterexample only for violations other than + // assignable checks. + + // Although there can be multiple cause loop ids. We only synthesize + // loop invariants for the first cause loop. + const std::list cause_loop_ids = + get_cause_loop_id(trace, property_it.second.pc); + + if(cause_loop_ids.empty()) { - log.debug() << "No cause loop found!\n"; + log.debug() << "No cause loop found!" << messaget::eom; restore_functions(); return cext(violation_type); } - log.debug() << "Found cause loop with function id: " - << cause_loop_id.value().function_id - << ", and loop number: " << cause_loop_id.value().loop_number - << "\n"; - // Decide whether the violation is in the cause loop. - bool violation_in_loop = is_instruction_in_transfomed_loop( - cause_loop_id.value(), - goto_model.get_goto_function(cause_loop_id.value().function_id), + bool is_violation_in_loop = is_instruction_in_transfomed_loop( + cause_loop_ids.front(), + goto_model.get_goto_function(cause_loop_ids.front().function_id), property_it.second.pc->location_number); + log.debug() << "Found cause loop with function id: " + << cause_loop_ids.front().function_id + << ", and loop number: " << cause_loop_ids.front().loop_number + << messaget::eom; + // We always strengthen in_clause if the violation is // invariant-not-preserved. if(violation_type == cext::violation_typet::cex_not_preserved) - violation_in_loop = true; + is_violation_in_loop = true; restore_functions(); auto return_cex = build_cex( - checker->get_traces()[property_it.first], + trace, get_loop_head( - cause_loop_id.value().loop_number, + cause_loop_ids.front().loop_number, goto_model.goto_functions - .function_map[cause_loop_id.value().function_id]) + .function_map[cause_loop_ids.front().function_id]) ->source_location()); - return_cex.violated_predicate = violated_predicate; - return_cex.cause_loop_id = cause_loop_id; - return_cex.checked_pointer = checked_pointer; - return_cex.is_violation_in_loop = violation_in_loop; + return_cex.violated_predicate = property_it.second.pc->condition(); + return_cex.cause_loop_ids = cause_loop_ids; + return_cex.is_violation_in_loop = is_violation_in_loop; return_cex.violation_type = violation_type; + // The pointer checked in the null-pointer-check violation. + if(violation_type == cext::violation_typet::cex_null_pointer) + { + return_cex.checked_pointer = property_it.second.pc->condition() + .operands()[0] + .operands()[1] + .operands()[0]; + INVARIANT( + return_cex.checked_pointer.id() == ID_symbol, + "Checking pointer symbol"); + } + return return_cex; } diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index e0c53b46047..a5aa54f85d2 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -31,6 +31,7 @@ class cext cex_null_pointer, cex_not_preserved, cex_not_hold_upon_entry, + cex_assignable, cex_other }; @@ -84,7 +85,7 @@ class cext std::set live_variables; violation_typet violation_type; - optionalt cause_loop_id; + std::list cause_loop_ids; }; /// Verifier that take a goto program as input, and ouptut formatted @@ -94,9 +95,11 @@ class cegis_verifiert public: cegis_verifiert( const invariant_mapt &invariant_candidates, + const std::map> &assigns_map, goto_modelt &goto_model, messaget &log) : invariant_candidates(invariant_candidates), + assigns_map(assigns_map), goto_model(goto_model), log(log) { @@ -116,13 +119,18 @@ class cegis_verifiert // TODO: replace the checker with CBMC api once it is implemented. optionst get_options(); - // Compute the cause loop of `violation`. + // Compute the cause loops of `violation`. // We say a loop is the cause loop if the violated predicate is dependent // upon the write set of the loop. - optionalt get_cause_loop_id( + std::list get_cause_loop_id( const goto_tracet &goto_trace, const goto_programt::const_targett violation); + // Compute the cause loops of a assignable-violation. + // We say a loop is the cause loop if the assignable check is in the loop. + std::list + get_cause_loop_id_for_assigns(const goto_tracet &goto_trace); + /// Restore transformed functions to original functions. void restore_functions(); @@ -139,6 +147,7 @@ class cegis_verifiert unsigned location_number_of_target); const invariant_mapt &invariant_candidates; + const std::map> &assigns_map; goto_modelt &goto_model; messaget log; diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index fb857e6f670..985919c7830 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -17,8 +17,10 @@ Author: Qinheping Hu #include #include #include +#include #include +#include #include "cegis_verifier.h" #include "expr_enumerator.h" @@ -92,7 +94,7 @@ void enumerative_loop_contracts_synthesizert::init_candidates() loop_idt new_id(function_p.first, loop_end->loop_number); - // we only synthesize invariants for unannotated loops + // we only synthesize invariants and assigns for unannotated loops if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil()) { // Store the loop guard. @@ -106,9 +108,58 @@ void enumerative_loop_contracts_synthesizert::init_candidates() // Initialize invariant clauses as `true`. in_invariant_clause_map[new_id] = true_exprt(); pos_invariant_clause_map[new_id] = true_exprt(); + + // Initialize assigns clauses. + if(loop_end->condition().find(ID_C_spec_assigns).is_nil()) + { + assigns_map[new_id] = {}; + } + } + } + } +} + +void enumerative_loop_contracts_synthesizert::synthesize_assigns( + const exprt &checked_pointer, + const std::list cause_loop_ids) +{ + namespacet ns(goto_model.symbol_table); + auto new_assign = checked_pointer; + + // Add the new assigns target to the most-inner loop that doesn't contain + // the new assigns target yet. + for(const auto &loop_id : cause_loop_ids) + { + // Widen index and dereference to whole object. + if(new_assign.id() == ID_index || new_assign.id() == ID_dereference) + { + address_of_exprt address_of_new_assigns(new_assign); + havoc_utils_is_constantt is_constant(assigns_map[loop_id], ns); + if(!is_constant(address_of_new_assigns)) + { + new_assign = pointer_object(address_of_new_assigns); } } + + const auto &source_location = + get_loop_head( + loop_id.loop_number, + goto_model.goto_functions.function_map[loop_id.function_id]) + ->source_location(); + + // Simplify expr to avoid offset that is out of scope. + // In the case of nested loops, After widening, pointer_object(ptr + i) + // can contain the pointer ptr in the scope of both loops, and the offset + // i which is only in the scope of the inner loop. + // After simplification, pointer_object(ptr + i) -> pointer_object(ptr). + new_assign = simplify_expr(new_assign, ns); + new_assign.add_source_location() = source_location; + + // Avoid adding same target. + if(assigns_map[loop_id].insert(new_assign).second) + return; } + INVARIANT(false, "Failed to synthesize a new assigns target."); } void enumerative_loop_contracts_synthesizert::build_tmp_post_map() @@ -257,7 +308,8 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause( new_in_clauses, pos_invariant_clause_map, neg_guards); // The verifier we use to check current invariant candidates. - cegis_verifiert verifier(combined_invariant, goto_model, log); + cegis_verifiert verifier( + combined_invariant, assigns_map, goto_model, log); // A good strengthening clause if // 1. all checks pass, or @@ -288,7 +340,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() in_invariant_clause_map, pos_invariant_clause_map, neg_guards); // The verifier we use to check current invariant candidates. - cegis_verifiert verifier(combined_invariant, goto_model, log); + cegis_verifiert verifier(combined_invariant, assigns_map, goto_model, log); // Set of symbols the violation may be dependent on. // We enumerate strenghening clauses built from symbols from the set. @@ -301,7 +353,6 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() while(return_cex.has_value()) { exprt new_invariant_clause = true_exprt(); - // Synthsize the new_clause // We use difference strategies for different type of violations. switch(return_cex->violation_type) @@ -320,47 +371,55 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() terminal_symbols = construct_terminals(dependent_symbols); new_invariant_clause = synthesize_strengthening_clause( terminal_symbols, - return_cex->cause_loop_id.value(), + return_cex->cause_loop_ids.front(), verifier.first_violation); break; + case cext::violation_typet::cex_assignable: + synthesize_assigns( + return_cex->checked_pointer, return_cex->cause_loop_ids); + break; case cext::violation_typet::cex_not_hold_upon_entry: case cext::violation_typet::cex_other: INVARIANT(false, "unsupported violation type"); break; } - INVARIANT(return_cex->cause_loop_id.has_value(), "No cause loop found!"); - - INVARIANT( - new_invariant_clause != true_exprt(), - "failed to synthesized meaningful clause"); - - // There could be tmp_post varialbes in the synthesized clause. - // We substitute them with their original variables. - replace_tmp_post(new_invariant_clause, tmp_post_map); - - const auto &cause_loop_id = return_cex->cause_loop_id.value(); - // Update the dependent symbols. - dependent_symbols = compute_dependent_symbols( - cause_loop_id, new_invariant_clause, return_cex->live_variables); - - // add the new cluase to the candidate invariants. - if(return_cex->is_violation_in_loop) - { - in_invariant_clause_map[cause_loop_id] = - and_exprt(in_invariant_clause_map[cause_loop_id], new_invariant_clause); - } - else + // Assigns map has already been updated in the switch block. + // Update invariants map for other types of violations. + if(return_cex->violation_type != cext::violation_typet::cex_assignable) { - // violation happens post-loop. - pos_invariant_clause_map[cause_loop_id] = and_exprt( - pos_invariant_clause_map[cause_loop_id], new_invariant_clause); - } + INVARIANT(!return_cex->cause_loop_ids.empty(), "No cause loop found!"); + INVARIANT( + new_invariant_clause != true_exprt(), + "failed to synthesized meaningful clause"); + + // There could be tmp_post varialbes in the synthesized clause. + // We substitute them with their original variables. + replace_tmp_post(new_invariant_clause, tmp_post_map); + + const auto &cause_loop_id = return_cex->cause_loop_ids.front(); + // Update the dependent symbols. + dependent_symbols = compute_dependent_symbols( + cause_loop_id, new_invariant_clause, return_cex->live_variables); + + // add the new cluase to the candidate invariants. + if(return_cex->is_violation_in_loop) + { + in_invariant_clause_map[cause_loop_id] = and_exprt( + in_invariant_clause_map[cause_loop_id], new_invariant_clause); + } + else + { + // violation happens post-loop. + pos_invariant_clause_map[cause_loop_id] = and_exprt( + pos_invariant_clause_map[cause_loop_id], new_invariant_clause); + } - // Re-combine invariant clauses and update the candidate map. - combined_invariant = combine_in_and_post_invariant_clauses( - in_invariant_clause_map, pos_invariant_clause_map, neg_guards); + // Re-combine invariant clauses and update the candidate map. + combined_invariant = combine_in_and_post_invariant_clauses( + in_invariant_clause_map, pos_invariant_clause_map, neg_guards); + } return_cex = verifier.verify(); } diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index ee14c8c6da7..8c5c3d99780 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h @@ -40,6 +40,11 @@ class enumerative_loop_contracts_synthesizert invariant_mapt synthesize_all() override; exprt synthesize(loop_idt loop_id) override; + std::map> get_assigns_map() const + { + return assigns_map; + } + private: /// Initialize invariants as true for all unannotated loops. void init_candidates(); @@ -68,12 +73,20 @@ class enumerative_loop_contracts_synthesizert const loop_idt &cause_loop_id, const irep_idt &violation_id); - /// Synthesize invariant of form - /// (in_inv || !guard) && (!guard -> pos_inv) + /// Synthesize assigns target and update assigns_map. + void synthesize_assigns( + const exprt &checked_pointer, + const std::list cause_loop_ids); + + /// Synthesize invariant of form + /// (in_inv || !guard) && (!guard -> pos_inv) invariant_mapt in_invariant_clause_map; invariant_mapt pos_invariant_clause_map; invariant_mapt neg_guards; + /// Synthesized assigns clauses. + std::map> assigns_map; + /// Map from tmp_post variables to their original variables. std::unordered_map tmp_post_map; }; diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 979323adf5c..685088d7419 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -54,6 +54,7 @@ int goto_synthesizer_parse_optionst::doit() // Synthesize loop invariants and annotate them into `goto_model` enumerative_loop_contracts_synthesizert synthesizer(goto_model, log); annotate_invariants(synthesizer.synthesize_all(), goto_model); + annotate_assigns(synthesizer.get_assigns_map(), goto_model); // Apply loop contracts. std::set to_exclude_from_nondet_static( diff --git a/src/goto-synthesizer/synthesizer_utils.cpp b/src/goto-synthesizer/synthesizer_utils.cpp index f035ccabe76..1bd2c89c378 100644 --- a/src/goto-synthesizer/synthesizer_utils.cpp +++ b/src/goto-synthesizer/synthesizer_utils.cpp @@ -116,6 +116,28 @@ void annotate_invariants( } } +void annotate_assigns( + const std::map> &assigns_map, + goto_modelt &goto_model) +{ + for(const auto &assigns_map_entry : assigns_map) + { + loop_idt loop_id = assigns_map_entry.first; + irep_idt function_id = loop_id.function_id; + unsigned int loop_number = loop_id.loop_number; + + // get the last instruction of the target loop + auto &function = goto_model.goto_functions.function_map[function_id]; + goto_programt::targett loop_end = get_loop_end(loop_number, function); + + exprt &condition = loop_end->condition_nonconst(); + auto assigns = exprt(ID_target_list); + for(const auto &e : assigns_map_entry.second) + assigns.add_to_operands(e); + condition.add(ID_C_spec_assigns) = assigns; + } +} + invariant_mapt combine_in_and_post_invariant_clauses( const invariant_mapt &in_clauses, const invariant_mapt &post_clauses, diff --git a/src/goto-synthesizer/synthesizer_utils.h b/src/goto-synthesizer/synthesizer_utils.h index c8f9c6ecb50..571e7f76f25 100644 --- a/src/goto-synthesizer/synthesizer_utils.h +++ b/src/goto-synthesizer/synthesizer_utils.h @@ -51,6 +51,12 @@ void annotate_invariants( const invariant_mapt &invariant_map, goto_modelt &goto_model); +/// Annotate the assigns in `assigns_map` to their corresponding +/// loops. Corresponding loops are specified by keys of `assigns_map` +void annotate_assigns( + const std::map> &assigns_map, + goto_modelt &goto_model); + /// Combine invariant of form /// (in_inv || !guard) && (!guard -> pos_inv) invariant_mapt combine_in_and_post_invariant_clauses( diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 46421875ea2..ad1263d89a6 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -902,6 +902,7 @@ IREP_ID_TWO(overflow_result_mult, overflow_result-*) IREP_ID_TWO(overflow_result_shl, overflow_result-shl) IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-) IREP_ID_ONE(field_sensitive_ssa) +IREP_ID_ONE(checked_assigns) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree