diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_06/main.c b/regression/goto-synthesizer/loop_contracts_synthesis_06/main.c new file mode 100644 index 00000000000..1404e030909 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_06/main.c @@ -0,0 +1,19 @@ +#include +#define SIZE 80 + +void main() +{ + unsigned long len; + __CPROVER_assume(len <= SIZE); + __CPROVER_assume(len >= 8); + char *array = malloc(len); + __CPROVER_assume(array != 0); + + array[len - 1] = 0; + unsigned i = 0; + + while(array[i] != 0) + { + i++; + } +} diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_06/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_06/test.desc new file mode 100644 index 00000000000..7b2dfafa82a --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_06/test.desc @@ -0,0 +1,12 @@ +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.*\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether CBMC synthesizes loop invariants for checks in the loop guard. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_06/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_06/test_dump.desc new file mode 100644 index 00000000000..fd7582e2d62 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_06/test_dump.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET +assigns i +-- +Checks if synthesized contracts are dumped correctly. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_07/main.c b/regression/goto-synthesizer/loop_contracts_synthesis_07/main.c new file mode 100644 index 00000000000..f5cffa22ae4 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_07/main.c @@ -0,0 +1,19 @@ +#include +#define SIZE 80 + +void main() +{ + unsigned long len; + __CPROVER_assume(len <= SIZE); + __CPROVER_assume(len >= 8); + char *array = malloc(len); + __CPROVER_assume(array != 0); + + unsigned i = 0; + + while(i <= len - 2) + { + i++; + } + unsigned result = array[i]; +} diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_07/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_07/test.desc new file mode 100644 index 00000000000..ac1d728439d --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_07/test.desc @@ -0,0 +1,13 @@ +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.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.pointer\_dereference.\d+].*SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether CBMC synthesizes loop invariants for checks located after the loop body. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_07/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_07/test_dump.desc new file mode 100644 index 00000000000..317580b4f4e --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_07/test_dump.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +loop 1 assigns i +loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET +-- +Checks if synthesized contracts are dumped correctly. diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 9b1576281fe..37f7dda54d7 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -211,7 +211,63 @@ std::list cegis_verifiert::get_cause_loop_id( return result; } -bool cegis_verifiert::is_instruction_in_transfomed_loop( +cext::violation_locationt cegis_verifiert::get_violation_location( + const loop_idt &loop_id, + const goto_functiont &function, + unsigned location_number_of_target) +{ + if(is_instruction_in_transformed_loop_condition( + loop_id, function, location_number_of_target)) + { + return cext::violation_locationt::in_condition; + } + + if(is_instruction_in_transformed_loop( + loop_id, function, location_number_of_target)) + { + return cext::violation_locationt::in_loop; + } + + return cext::violation_locationt::after_loop; +} + +bool cegis_verifiert::is_instruction_in_transformed_loop_condition( + const loop_idt &loop_id, + const goto_functiont &function, + unsigned location_number_of_target) +{ + // The transformed loop condition is a set of instructions from + // loop havocing instructions + // to + // if(!guard) GOTO EXIT + unsigned location_number_of_havocing = 0; + for(auto it = function.body.instructions.begin(); + it != function.body.instructions.end(); + ++it) + { + // Record the location number of the beginning of a transformed loop. + if( + loop_havoc_set.count(it) && + original_loop_number_map[it] == loop_id.loop_number) + { + location_number_of_havocing = it->location_number; + } + + // Reach the end of the evaluation of the transformed loop condition. + if(location_number_of_havocing != 0 && it->is_goto()) + { + if((location_number_of_havocing < location_number_of_target && + location_number_of_target < it->location_number)) + { + return true; + } + location_number_of_havocing = 0; + } + } + return false; +} + +bool cegis_verifiert::is_instruction_in_transformed_loop( const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target) @@ -458,9 +514,9 @@ optionalt cegis_verifiert::verify() // // 1. annotate and apply the loop contracts stored in `invariant_candidates`. // - // 2. run the CBMC API to verify the intrumented goto model. As the API is not - // merged yet, we preprocess the goto model and run the symex checker on it - // to simulate CBMC API. + // 2. run the CBMC API to verify the instrumented goto model. As the API is + // not merged yet, we preprocess the goto model and run the symex checker + // on it to simulate CBMC API. // TODO: ^^^ replace the symex checker once the real API is merged. // // 3. construct the formatted counterexample from the violated property and @@ -530,7 +586,7 @@ optionalt cegis_verifiert::verify() } properties = checker->get_properties(); - // Find the violation and construct conterexample from its trace. + // Find the violation and construct counterexample from its trace. for(const auto &property_it : properties) { if(property_it.second.status != property_statust::FAIL) @@ -622,21 +678,22 @@ optionalt cegis_verifiert::verify() return cext(violation_type); } - // Decide whether the violation is in the cause loop. - 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; + auto violation_location = cext::violation_locationt::in_loop; // We always strengthen in_clause if the violation is // invariant-not-preserved. - if(violation_type == cext::violation_typet::cex_not_preserved) - is_violation_in_loop = true; + if(violation_type != cext::violation_typet::cex_not_preserved) + { + // Get the location of the violation + violation_location = get_violation_location( + cause_loop_ids.front(), + goto_model.get_goto_function(cause_loop_ids.front().function_id), + property_it.second.pc->location_number); + } restore_functions(); @@ -649,7 +706,7 @@ optionalt cegis_verifiert::verify() ->source_location()); 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_location = violation_location; return_cex.violation_type = violation_type; // The pointer checked in the null-pointer-check violation. diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index a5aa54f85d2..b126c1a2369 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -35,6 +35,13 @@ class cext cex_other }; + enum class violation_locationt + { + in_loop, + after_loop, + in_condition + }; + cext( const std::unordered_map &object_sizes, const std::unordered_map &havoced_values, @@ -61,16 +68,15 @@ class cext exprt checked_pointer; exprt violated_predicate; - // true if the violation happens in the cause loop - // false if the violation happens after the cause loop - bool is_violation_in_loop = true; + // Location where the violation happens + violation_locationt violation_location = violation_locationt::in_loop; // We collect havoced evaluations of havoced variables and their object sizes // and pointer offsets. // __CPROVER_OBJECT_SIZE std::unordered_map object_sizes; - // all the valuation of havoced variables with primitived type. + // all the valuation of havoced variables with primitive type. std::unordered_map havoced_values; // __CPROVER_POINTER_OFFSET std::unordered_map havoced_pointer_offsets; @@ -88,7 +94,7 @@ class cext std::list cause_loop_ids; }; -/// Verifier that take a goto program as input, and ouptut formatted +/// Verifier that take a goto program as input, and output formatted /// counterexamples for counterexample-guided-synthesis. class cegis_verifiert { @@ -131,6 +137,12 @@ class cegis_verifiert std::list get_cause_loop_id_for_assigns(const goto_tracet &goto_trace); + // Compute the location of the violation. + cext::violation_locationt get_violation_location( + const loop_idt &loop_id, + const goto_functiont &function, + unsigned location_number_of_target); + /// Restore transformed functions to original functions. void restore_functions(); @@ -141,7 +153,14 @@ class cegis_verifiert /// Decide whether the target instruction is in the body of the transformed /// loop specified by `loop_id`. - bool is_instruction_in_transfomed_loop( + bool is_instruction_in_transformed_loop( + const loop_idt &loop_id, + const goto_functiont &function, + unsigned location_number_of_target); + + /// Decide whether the target instruction is between the loop-havoc and the + /// evaluation of the loop guard. + bool is_instruction_in_transformed_loop_condition( const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target); @@ -160,7 +179,7 @@ class cegis_verifiert std::unordered_map original_loop_number_map; - /// Loop havoc instructions instrumneted during applying loop contracts. + /// Loop havoc instructions instrumented during applying loop contracts. std::unordered_set loop_havoc_set; }; diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index cf27ef17b91..f5e80e55025 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -217,7 +217,7 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_same_object_predicate( { // The same object predicate says that the checked pointer points to the // same object as it pointed before entering the loop. - // It works for the array-manuplating loops where only offset of pointer + // It works for the array-manipulating loops where only offset of pointer // are modified but not the object pointers point to. return same_object( checked_pointer, unary_exprt(ID_loop_entry, checked_pointer)); @@ -228,7 +228,7 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause( const loop_idt &cause_loop_id, const irep_idt &violation_id) { - // Synthesis of strengthning clauses is a enumerate-and-check proecess. + // Synthesis of strengthening clauses is a enumerate-and-check process. // We first construct the enumerator for the following grammar. // And then enumerate clause and check that if it can make the invariant // inductive. @@ -343,9 +343,9 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() 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. + // We enumerate strengthening clauses built from symbols from the set. std::set dependent_symbols; - // Set of symbols we used to enumerate strenghening clauses. + // Set of symbols we used to enumerate strengthening clauses. std::vector terminal_symbols; auto return_cex = verifier.verify(); @@ -353,7 +353,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() while(return_cex.has_value()) { exprt new_invariant_clause = true_exprt(); - // Synthsize the new_clause + // Synthesize the new_clause // We use difference strategies for different type of violations. switch(return_cex->violation_type) { @@ -394,7 +394,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() new_invariant_clause != true_exprt(), "failed to synthesized meaningful clause"); - // There could be tmp_post varialbes in the synthesized clause. + // There could be tmp_post variables in the synthesized clause. // We substitute them with their original variables. replace_tmp_post(new_invariant_clause, tmp_post_map); @@ -403,15 +403,34 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() 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) + // add the new clause to the candidate invariants. + if( + return_cex->violation_location == + cext::violation_locationt::in_condition) + { + // When the violation happens in the loop guard, the new clause + // should hold for the both cases of + // 1. loop guard holds --- loop_guard -> in_invariant + // 2. loop guard doesn't hold --- !loop_guard -> pos_invariant + in_invariant_clause_map[cause_loop_id] = and_exprt( + in_invariant_clause_map[cause_loop_id], new_invariant_clause); + pos_invariant_clause_map[cause_loop_id] = and_exprt( + pos_invariant_clause_map[cause_loop_id], new_invariant_clause); + } + else if( + return_cex->violation_location == cext::violation_locationt::in_loop) { + // When the violation happens in the loop body, the new clause + // should hold for the case of + // loop guard holds --- loop_guard -> in_invariant in_invariant_clause_map[cause_loop_id] = and_exprt( in_invariant_clause_map[cause_loop_id], new_invariant_clause); } else { - // violation happens post-loop. + // When the violation happens after the loop body, the new clause + // should hold for the case of + // loop guard doesn't hold --- !loop_guard -> pos_invariant pos_invariant_clause_map[cause_loop_id] = and_exprt( pos_invariant_clause_map[cause_loop_id], new_invariant_clause); }