diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index 6b39e0fe4..10d19ba63 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "bmc.h" #include +#include #include #include @@ -191,6 +192,17 @@ void bmc_with_iterative_constraint_strengthening( } } +/// Extension of solver.handle(...) from expressions to vectors of expressions +static exprt::operandst +handles(const exprt::operandst &exprs, decision_proceduret &solver) +{ + exprt::operandst result; + result.reserve(exprs.size()); + for(auto &expr : exprs) + result.push_back(solver.handle(expr)); + return result; +} + property_checker_resultt bmc( std::size_t bound, bool convert_only, @@ -211,13 +223,21 @@ property_checker_resultt bmc( auto solver_wrapper = solver_factory(ns, message_handler); auto &solver = solver_wrapper.decision_procedure(); + auto no_timeframes = bound + 1; ::unwind( - transition_system.trans_expr, message_handler, solver, bound + 1, ns, true); + transition_system.trans_expr, + message_handler, + solver, + no_timeframes, + ns, + true); // convert the properties message.status() << "Properties" << messaget::eom; + bool requires_lasso_constraints = false; + for(auto &property : properties.properties) { if(property.is_disabled() || property.is_failure()) @@ -230,8 +250,13 @@ property_checker_resultt bmc( continue; } - property.timeframe_handles = ::property( - property.normalized_expr, message_handler, solver, bound + 1, ns); + auto obligations = + ::property(property.normalized_expr, message_handler, no_timeframes); + + if(uses_lasso_symbol(obligations)) + requires_lasso_constraints = true; + + property.timeframe_handles = handles(obligations, solver); // If it's an assumption, then add it as constraint. if(property.is_assumed()) @@ -239,11 +264,11 @@ property_checker_resultt bmc( } // lasso constraints, if needed - if(properties.requires_lasso_constraints()) + if(requires_lasso_constraints) { message.status() << "Adding lasso constraints" << messaget::eom; lasso_constraints( - solver, bound + 1, ns, transition_system.main_symbol->name); + solver, no_timeframes, ns, transition_system.main_symbol->name); } if(convert_only) diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h index 67816d047..9d8e3287f 100644 --- a/src/ebmc/ebmc_properties.h +++ b/src/ebmc/ebmc_properties.h @@ -199,11 +199,6 @@ class ebmc_propertiest propertyt() = default; - bool requires_lasso_constraints() const - { - return ::requires_lasso_constraints(normalized_expr); - } - bool is_exists_path() const { return ::is_exists_path(original_expr); @@ -236,15 +231,6 @@ class ebmc_propertiest return false; } - bool requires_lasso_constraints() const - { - for(const auto &p : properties) - if(!p.is_disabled() && p.requires_lasso_constraints()) - return true; - - return false; - } - static ebmc_propertiest from_command_line( const cmdlinet &, const transition_systemt &, diff --git a/src/ebmc/liveness_to_safety.cpp b/src/ebmc/liveness_to_safety.cpp index 22239b356..eb1a27ab7 100644 --- a/src/ebmc/liveness_to_safety.cpp +++ b/src/ebmc/liveness_to_safety.cpp @@ -114,10 +114,29 @@ class liveness_to_safetyt } }; +/// returns true iff the given property is supported +/// by the liveness-to-safety translation +static bool property_supported(const exprt &expr) +{ + return expr.id() == ID_sva_always && + (to_sva_always_expr(expr).op().id() == ID_sva_eventually || + to_sva_always_expr(expr).op().id() == ID_sva_s_eventually); +} + +static bool have_supported_property(const ebmc_propertiest &properties) +{ + for(auto &property : properties.properties) + if(!property.is_disabled()) + if(property_supported(property.normalized_expr)) + return true; + + return false; +} + void liveness_to_safetyt::operator()() { - // Do we have a liveness property? - if(!properties.requires_lasso_constraints()) + // Do we have a supported property? + if(!have_supported_property(properties)) return; // no // gather the state variables @@ -231,15 +250,10 @@ void liveness_to_safetyt::operator()() for(auto &property : properties.properties) { - if(!property.is_disabled() && property.requires_lasso_constraints()) + if(!property.is_disabled()) { // We want GFp. - if( - property.normalized_expr.id() == ID_sva_always && - (to_sva_always_expr(property.normalized_expr).op().id() == - ID_sva_eventually || - to_sva_always_expr(property.normalized_expr).op().id() == - ID_sva_s_eventually)) + if(property_supported(property.normalized_expr)) { translate_GFp(property); } diff --git a/src/trans-word-level/lasso.cpp b/src/trans-word-level/lasso.cpp index ef2faca98..c15e5a64e 100644 --- a/src/trans-word-level/lasso.cpp +++ b/src/trans-word-level/lasso.cpp @@ -59,13 +59,15 @@ Function: lasso_symbol \*******************************************************************/ +#define LASSO_PREFIX "lasso::" + symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i) { // True when states i and k are equal. // We require kid() == ID_sva_until || subexpr_it->id() == ID_sva_s_until || - subexpr_it->id() == ID_sva_eventually || - subexpr_it->id() == ID_sva_s_eventually || subexpr_it->id() == ID_AF || - subexpr_it->id() == ID_F || subexpr_it->id() == ID_U) - { - return true; - } + if(subexpr_it->id() == ID_symbol) + if(to_symbol_expr(*subexpr_it).get_identifier().starts_with(LASSO_PREFIX)) + { + return true; + } } return false; } + +/*******************************************************************\ + +Function: uses_lasso_symbol + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool uses_lasso_symbol(const exprt::operandst &exprs) +{ + for(auto &expr : exprs) + if(::uses_lasso_symbol(expr)) + return true; + return false; +} diff --git a/src/trans-word-level/lasso.h b/src/trans-word-level/lasso.h index a53c2acd3..1ca2f5b14 100644 --- a/src/trans-word-level/lasso.h +++ b/src/trans-word-level/lasso.h @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef CPROVER_TRANS_WORD_LEVEL_LASSO_H #define CPROVER_TRANS_WORD_LEVEL_LASSO_H +#include #include #include @@ -26,7 +27,7 @@ void lasso_constraints( /// Precondition: k #include #include -#include #include #include @@ -24,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "instantiate_word_level.h" +#include "lasso.h" #include "obligations.h" #include "sequence.h" @@ -797,9 +797,7 @@ Function: property exprt::operandst property( const exprt &property_expr, message_handlert &message_handler, - decision_proceduret &solver, - std::size_t no_timeframes, - const namespacet &) + std::size_t no_timeframes) { // The first element of the pair is the length of the // counterexample, and the second is the condition that @@ -815,7 +813,7 @@ exprt::operandst property( DATA_INVARIANT( t >= 0 && t < no_timeframes, "obligation must have valid timeframe"); auto t_int = numeric_cast_v(t); - prop_handles[t_int] = solver.handle(conjunction(obligation_it.second)); + prop_handles[t_int] = conjunction(obligation_it.second); } return prop_handles; diff --git a/src/trans-word-level/property.h b/src/trans-word-level/property.h index 64d6feaef..9bf58cb7c 100644 --- a/src/trans-word-level/property.h +++ b/src/trans-word-level/property.h @@ -12,35 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include - -#include +/// returns a vector of obligation expressions, one per timeframe exprt::operandst property( const exprt &property_expr, message_handlert &, - decision_proceduret &solver, - std::size_t no_timeframes, - const namespacet &); + std::size_t no_timeframes); /// Is the given property supported by word-level unwinding? bool bmc_supports_property(const exprt &); -/// Adds a constraint that can be used to determine whether the -/// given state has already been seen earlier in the trace. -void lasso_constraints( - decision_proceduret &, - const mp_integer &no_timeframes, - const namespacet &, - const irep_idt &module_identifier); - -/// Is there a loop from i back to k? -/// Precondition: k