diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/main.c b/regression/goto-synthesizer/loop_contracts_synthesis_08/main.c new file mode 100644 index 00000000000..8a6ca9ce7f0 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_08/main.c @@ -0,0 +1,17 @@ +#include +#define SIZE 80 + +void main() +{ + unsigned long len; + __CPROVER_assume(len <= SIZE); + __CPROVER_assume(len >= 8); + const char *i = malloc(len); + const char *end = i + len; + char s = 0; + + while(i != end) + { + s = *i++; + } +} diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc new file mode 100644 index 00000000000..2b98c115ec7 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check +^EXIT=0$ +^SIGNAL=0$ +^\[main.pointer\_dereference.\d+\] .* SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Check whether assigns clauses are synthesize before invariant clauses. diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 37f7dda54d7..e2bf5599234 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -53,6 +53,34 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) return false; } +static const exprt & +get_checked_pointer_from_null_pointer_check(const exprt &violation) +{ + // A NULL-pointer check is the negation of an equation between the checked + // pointer and a NULL pointer. + // ! (POINTER_OBJECT(NULL) == POINTER_OBJECT(ptr)) + const equal_exprt &equal_expr = to_equal_expr(to_not_expr(violation).op()); + + const pointer_object_exprt &lhs_pointer_object = + to_pointer_object_expr(equal_expr.lhs()); + const pointer_object_exprt &rhs_pointer_object = + to_pointer_object_expr(equal_expr.rhs()); + + const exprt &lhs_pointer = lhs_pointer_object.operands()[0]; + const exprt &rhs_pointer = rhs_pointer_object.operands()[0]; + + // NULL == ptr + if( + can_cast_expr(lhs_pointer) && + is_null_pointer(*expr_try_dynamic_cast(lhs_pointer))) + { + return rhs_pointer; + } + + // Not a equation with NULL on one side. + UNREACHABLE; +} + optionst cegis_verifiert::get_options() { optionst options; @@ -94,6 +122,44 @@ optionst cegis_verifiert::get_options() return options; } +cext::violation_typet +cegis_verifiert::extract_violation_type(const std::string &description) +{ + // The violation is a pointer OOB check. + if((description.find( + "dereference failure: pointer outside object bounds in") != + std::string::npos)) + { + return cext::violation_typet::cex_out_of_boundary; + } + + // The violation is a null pointer check. + if(description.find("pointer NULL") != std::string::npos) + { + return cext::violation_typet::cex_null_pointer; + } + + // The violation is a loop-invariant-preservation check. + if(description.find("preserved") != std::string::npos) + { + return cext::violation_typet::cex_not_preserved; + } + + // The violation is a loop-invariant-preservation check. + if(description.find("invariant before entry") != std::string::npos) + { + return cext::violation_typet::cex_not_hold_upon_entry; + } + + // The violation is an assignable check. + if(description.find("assignable") != std::string::npos) + { + return cext::violation_typet::cex_assignable; + } + + return cext::violation_typet::cex_other; +} + std::list cegis_verifiert::get_cause_loop_id_for_assigns(const goto_tracet &goto_trace) { @@ -586,143 +652,118 @@ optionalt cegis_verifiert::verify() } properties = checker->get_properties(); - // Find the violation and construct counterexample from its trace. - for(const auto &property_it : properties) + bool target_violation_found = false; + auto target_violation_info = properties.begin()->second; + + // Find target violation---the violation we want to fix next. + // A target violation is an assignable violation or the first violation that + // is not assignable violation. + for(const auto &property : properties) { - if(property_it.second.status != property_statust::FAIL) + if(property.second.status != property_statust::FAIL) continue; - // Store the violation that we want to fix with synthesized - // assigns/invariant. - first_violation = property_it.first; - - // 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") != - std::string::npos)) - { - violation_type = cext::violation_typet::cex_out_of_boundary; - } - - // The violation is a null pointer check. - if(property_it.second.description.find("pointer NULL") != std::string::npos) + // assignable violation found + if(property.second.description.find("assignable") != std::string::npos) { - violation_type = cext::violation_typet::cex_null_pointer; - } - - // The violation is a loop-invariant-preservation check. - if(property_it.second.description.find("preserved") != std::string::npos) - { - violation_type = cext::violation_typet::cex_not_preserved; - } - - // The violation is a loop-invariant-preservation check. - if( - property_it.second.description.find("invariant before entry") != - std::string::npos) - { - violation_type = cext::violation_typet::cex_not_hold_upon_entry; + target_violation = property.first; + target_violation_info = property.second; + break; } - // The violation is an assignable check. - if(property_it.second.description.find("assignable") != std::string::npos) + // Store the violation that we want to fix with synthesized + // assigns/invariant. + if(!target_violation_found) { - violation_type = cext::violation_typet::cex_assignable; + target_violation = property.first; + target_violation_info = property.second; + target_violation_found = true; } + } - // 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. + // Decide the violation type from the description of violation + cext::violation_typet violation_type = + extract_violation_type(target_violation_info.description); - log.debug() << "Start to compute cause loop ids." << messaget::eom; + // Compute the cause loop---the loop for which we synthesize loop contracts, + // and the counterexample. - const auto &trace = checker->get_traces()[property_it.first]; + // 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. - // 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; - } + // 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. - // We construct the full counterexample only for violations other than - // assignable checks. + log.debug() << "Start to compute cause loop ids." << messaget::eom; - // 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); + const auto &trace = checker->get_traces()[target_violation]; + // 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( + target_violation_info.pc->condition().find(ID_checked_assigns)); + restore_functions(); + return result; + } - if(cause_loop_ids.empty()) - { - log.debug() << "No cause loop found!" << messaget::eom; - restore_functions(); + // We construct the full counterexample only for violations other than + // assignable checks. - return cext(violation_type); - } + // 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, target_violation_info.pc); - 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; + if(cause_loop_ids.empty()) + { + log.debug() << "No cause loop found!" << messaget::eom; + restore_functions(); - 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) - { - // 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); - } + return cext(violation_type); + } - restore_functions(); + 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 return_cex = build_cex( - trace, - get_loop_head( - cause_loop_ids.front().loop_number, - goto_model.goto_functions - .function_map[cause_loop_ids.front().function_id]) - ->source_location()); - return_cex.violated_predicate = property_it.second.pc->condition(); - return_cex.cause_loop_ids = cause_loop_ids; - return_cex.violation_location = violation_location; - 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"); - } + 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) + { + // 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), + target_violation_info.pc->location_number); + } - return return_cex; + restore_functions(); + + auto return_cex = build_cex( + trace, + get_loop_head( + cause_loop_ids.front().loop_number, + goto_model.goto_functions + .function_map[cause_loop_ids.front().function_id]) + ->source_location()); + return_cex.violated_predicate = target_violation_info.pc->condition(); + return_cex.cause_loop_ids = cause_loop_ids; + return_cex.violation_location = violation_location; + 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 = get_checked_pointer_from_null_pointer_check( + target_violation_info.pc->condition()); } - UNREACHABLE; + return return_cex; } diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index b126c1a2369..099672c20fa 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -117,7 +117,7 @@ class cegis_verifiert /// Result counterexample. propertiest properties; - irep_idt first_violation; + irep_idt target_violation; protected: // Get the options same as using CBMC api without any flag, and @@ -137,6 +137,9 @@ class cegis_verifiert std::list get_cause_loop_id_for_assigns(const goto_tracet &goto_trace); + // Extract the violation type from violation description. + cext::violation_typet extract_violation_type(const std::string &description); + // Compute the location of the violation. cext::violation_locationt get_violation_location( const loop_idt &loop_id, diff --git a/src/goto-synthesizer/dump_loop_contracts.cpp b/src/goto-synthesizer/dump_loop_contracts.cpp index f679b5ac52d..785c119a3b4 100644 --- a/src/goto-synthesizer/dump_loop_contracts.cpp +++ b/src/goto-synthesizer/dump_loop_contracts.cpp @@ -91,16 +91,16 @@ void dump_loop_contracts( "loop " + std::to_string(invariant_entry.first.loop_number + 1) + " assigns "; - bool in_fisrt_iter = true; + bool in_first_iter = true; for(const auto &a : it_assigns->second) { - if(!in_fisrt_iter) + if(!in_first_iter) { assign_string += ","; } else { - in_fisrt_iter = false; + in_first_iter = false; } assign_string += expr2c( simplify_expr(a, ns), ns, expr2c_configurationt::clean_configuration); diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index f5e80e55025..6a0e9dc5e2c 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -94,6 +94,9 @@ void enumerative_loop_contracts_synthesizert::init_candidates() loop_idt new_id(function_p.first, loop_end->loop_number); + log.debug() << "Initialize candidates for the loop at " + << loop_end->source_location() << messaget::eom; + // we only synthesize invariants and assigns for unannotated loops if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil()) { @@ -372,7 +375,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() new_invariant_clause = synthesize_strengthening_clause( terminal_symbols, return_cex->cause_loop_ids.front(), - verifier.first_violation); + verifier.target_violation); break; case cext::violation_typet::cex_assignable: diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index 8c5c3d99780..e97081f787a 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h @@ -53,7 +53,7 @@ class enumerative_loop_contracts_synthesizert /// to their original variables. void build_tmp_post_map(); - /// Compute the depedent symbols for a loop with invariant-not-preserved + /// Compute the dependent symbols for a loop with invariant-not-preserved /// violation which happen after `new_clause` was added. std::set compute_dependent_symbols( const loop_idt &cause_loop_id, diff --git a/src/goto-synthesizer/expr_enumerator.cpp b/src/goto-synthesizer/expr_enumerator.cpp index a86efc3add0..c57d2ef2523 100644 --- a/src/goto-synthesizer/expr_enumerator.cpp +++ b/src/goto-synthesizer/expr_enumerator.cpp @@ -208,7 +208,7 @@ std::vector get_ones_pos(std::size_t v) return result; } -/// Construct parition of `n` elements from a bit vector `v`. +/// Construct partition of `n` elements from a bit vector `v`. /// For a bit vector with ones at positions (computed by `get_ones_pos`) /// (ones[0], ones[1], ..., ones[k-2]), /// the corresponding partition is @@ -255,7 +255,7 @@ std::list non_leaf_enumeratort::get_partitions( // Initial `v` is with ones at positions (n-k+1, n-k+2, ..., n-2, n-1). std::size_t v = 0; - // Initial `end` (the last bit vectorr we enumerate) is with ones at + // Initial `end` (the last bit vector we enumerate) is with ones at // positions (1, 2, 3, ..., k-1). std::size_t end = 0; for(size_t i = 0; i < k - 1; i++) @@ -412,5 +412,5 @@ void enumerator_factoryt::attach_productions( { const auto &ret = productions_map.insert({id, enumerators}); INVARIANT( - ret.second, "Cannnot attach enumerators to a non-existing nonterminal."); + ret.second, "Cannot attach enumerators to a non-existing nonterminal."); } diff --git a/src/goto-synthesizer/expr_enumerator.h b/src/goto-synthesizer/expr_enumerator.h index 3369f989fca..138e584b163 100644 --- a/src/goto-synthesizer/expr_enumerator.h +++ b/src/goto-synthesizer/expr_enumerator.h @@ -158,7 +158,7 @@ class non_leaf_enumeratort : public enumerator_baset /// enumerated by the enumerator e_i. /// \param partition_check an optional function checking whether a partition /// can be safely discarded. - /// \param ns namesapce used by `simplify_expr`. + /// \param ns namespace used by `simplify_expr`. non_leaf_enumeratort( const enumeratorst &enumerators, const std::function partition_check, @@ -337,7 +337,7 @@ class recursive_enumerator_placeholdert : public enumerator_baset /// \param factory the enumerator factory---a grammar---this enumerator /// belongs to. /// \param id the identifier of this placeholder. - /// \param ns namesapce used for `simplify_expr`. + /// \param ns namespace used for `simplify_expr`. recursive_enumerator_placeholdert( enumerator_factoryt &factory, const std::string &id,