From 251c257f187efeb50a03ed7d9f76f0451d85e67d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 21 Dec 2022 01:33:14 -0600 Subject: [PATCH] Add counterexample-guided loop assigns synthesis Implement the functionality described below. Motivation --- This loop assigns synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop assigns targets. It is based on the same CEGIS framework as the loop invariant synthesizer w ith the following difference. Use Cases --- Our loop invariants synthesizer will synthesize invariants clauses for all loops without loop invariant annotation. The loop assigns synthesizer will synthesize assigns clauses for all loops without loop invariant annotation **and** loop assigns annotation. Cause Loop ID --- In the loop invariant synthesizer, we say a loop is a cause loop if the violation is dependent on the loop's havoc instructions. Because invariant clauses affect the havoced values which could flow into variables outside the loop. In the loop assigns synthesizer, we say a loop is a cause loop if the violation is in the loop. Because assigns clauses only affect the CAR of its own loop body. Synthesizer --- For an assignable violation with checked target `T`, the new assigns target will be `T`. If `T` is a non-constant target, e.g., `ptr[i]` with `i` also an assigns target, we widen it to `__CPROVER_POINTER_OBJECT(T)`. We add the new target to cause loop one by one starting from the most-inner one. Until the assignable violation is resolved. --- .../loop_contracts_synthesis_05/main.c | 51 ++++++ .../loop_contracts_synthesis_05/test.desc | 18 ++ src/goto-instrument/contracts/contracts.cpp | 8 +- .../contracts/instrument_spec_assigns.cpp | 11 +- src/goto-instrument/contracts/utils.cpp | 16 +- src/goto-instrument/contracts/utils.h | 5 +- src/goto-synthesizer/cegis_verifier.cpp | 154 ++++++++++++++---- src/goto-synthesizer/cegis_verifier.h | 15 +- ...enumerative_loop_contracts_synthesizer.cpp | 127 +++++++++++---- .../enumerative_loop_contracts_synthesizer.h | 17 +- .../goto_synthesizer_parse_options.cpp | 1 + src/goto-synthesizer/synthesizer_utils.cpp | 22 +++ src/goto-synthesizer/synthesizer_utils.h | 6 + src/util/irep_ids.def | 1 + 14 files changed, 364 insertions(+), 88 deletions(-) create mode 100644 regression/goto-synthesizer/loop_contracts_synthesis_05/main.c create mode 100644 regression/goto-synthesizer/loop_contracts_synthesis_05/test.desc 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