diff --git a/regression/ebmc/engine-heuristic/basic1.desc b/regression/ebmc/engine-heuristic/basic1.desc new file mode 100644 index 00000000..6ca1327a --- /dev/null +++ b/regression/ebmc/engine-heuristic/basic1.desc @@ -0,0 +1,10 @@ +CORE +basic1.sv + +^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$ +^\[main\.p0\] always main\.x: PROVED up to bound 5$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/engine-heuristic/basic1.sv b/regression/ebmc/engine-heuristic/basic1.sv new file mode 100644 index 00000000..4c7ada49 --- /dev/null +++ b/regression/ebmc/engine-heuristic/basic1.sv @@ -0,0 +1,8 @@ +module main(input clk, input x); + + // not supported by k-induction + a0: assume property (not s_eventually !x); + + p0: assert property (x); + +endmodule diff --git a/regression/ebmc/engine-heuristic/basic2.desc b/regression/ebmc/engine-heuristic/basic2.desc new file mode 100644 index 00000000..e8adb78c --- /dev/null +++ b/regression/ebmc/engine-heuristic/basic2.desc @@ -0,0 +1,11 @@ +CORE +basic2.sv + +^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$ +^\[main\.a1\] always !main\.x: ASSUMED$ +^\[main\.p0\] always !main\.z: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/engine-heuristic/basic2.sv b/regression/ebmc/engine-heuristic/basic2.sv new file mode 100644 index 00000000..c48fbb15 --- /dev/null +++ b/regression/ebmc/engine-heuristic/basic2.sv @@ -0,0 +1,15 @@ +module main(input clk, input x, input y); + + reg z = 0; + always_ff @(posedge clk) z <= z || x; + + // unsupported assumption + a0: assume property (not s_eventually !y); + + // supported assumption + a1: assume property (!x); + + // inductive property + p0: assert property (!z); + +endmodule diff --git a/regression/ebmc/k-induction/k-induction-unsupported2.desc b/regression/ebmc/k-induction/k-induction-unsupported2.desc index 6f004501..da7ac0bf 100644 --- a/regression/ebmc/k-induction/k-induction-unsupported2.desc +++ b/regression/ebmc/k-induction/k-induction-unsupported2.desc @@ -3,7 +3,7 @@ k-induction-unsupported2.sv --module main --k-induction ^EXIT=10$ ^SIGNAL=0$ -^\[main\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$ +^\[main\.p0\] always s_eventually main\.x == 10: UNSUPPORTED: unsupported by k-induction$ ^\[main\.p1\] always main\.x <= 10: PROVED$ -- ^warning: ignoring diff --git a/regression/ebmc/k-induction/k-induction6.desc b/regression/ebmc/k-induction/k-induction6.desc index 7b106e61..76f743ed 100644 --- a/regression/ebmc/k-induction/k-induction6.desc +++ b/regression/ebmc/k-induction/k-induction6.desc @@ -1,9 +1,10 @@ -KNOWNBUG +CORE k-induction6.sv - +--k-induction +^\[main\.a0\] always not s_eventually !main\.x: UNSUPPORTED: unsupported by k-induction$ +^\[main\.p0\] always main\.x: INCONCLUSIVE$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -The property should hold, but is reported as refuted. diff --git a/regression/ebmc/k-induction/k-induction7.desc b/regression/ebmc/k-induction/k-induction7.desc new file mode 100644 index 00000000..b12da494 --- /dev/null +++ b/regression/ebmc/k-induction/k-induction7.desc @@ -0,0 +1,11 @@ +CORE +k-induction7.sv +--k-induction +^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$ +^\[main\.a1\] always !main\.x: ASSUMED$ +^\[main\.p0\] always !main\.z: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/k-induction/k-induction7.sv b/regression/ebmc/k-induction/k-induction7.sv new file mode 100644 index 00000000..c48fbb15 --- /dev/null +++ b/regression/ebmc/k-induction/k-induction7.sv @@ -0,0 +1,15 @@ +module main(input clk, input x, input y); + + reg z = 0; + always_ff @(posedge clk) z <= z || x; + + // unsupported assumption + a0: assume property (not s_eventually !y); + + // supported assumption + a1: assume property (!x); + + // inductive property + p0: assert property (!z); + +endmodule diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index b1c35d48..bb51b478 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -180,7 +180,7 @@ property_checker_resultt bdd_enginet::operator()() try { // any properties left? - if(!properties.has_unknown_property()) + if(!properties.has_unfinished_property()) return property_checker_resultt{properties}; // possibly apply liveness-to-safety diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp index daa0d07c..e20983a7 100644 --- a/src/ebmc/ebmc_properties.cpp +++ b/src/ebmc/ebmc_properties.cpp @@ -18,6 +18,8 @@ Author: Daniel Kroening, dkr@amazon.com std::string ebmc_propertiest::propertyt::status_as_string() const { + auto suffix = failure_reason.has_value() ? ": " + failure_reason.value() : ""; + switch(status) { case statust::ASSUMED: @@ -31,14 +33,15 @@ std::string ebmc_propertiest::propertyt::status_as_string() const case statust::REFUTED_WITH_BOUND: return "REFUTED up to bound " + std::to_string(bound); case statust::UNKNOWN: - return "UNKNOWN"; + return "UNKNOWN" + suffix; + case statust::UNSUPPORTED: + return "UNSUPPORTED" + suffix; case statust::INCONCLUSIVE: - return "INCONCLUSIVE"; + return "INCONCLUSIVE" + suffix; case statust::FAILURE: - return failure_reason.has_value() ? "FAILURE: " + failure_reason.value() - : "FAILURE"; + return "FAILURE" + suffix; case statust::DROPPED: - return "DROPPED"; + return "DROPPED" + suffix; case statust::DISABLED: default: UNREACHABLE; @@ -78,9 +81,9 @@ ebmc_propertiest ebmc_propertiest::from_transition_system( id2string(symbol.location.get_comment()); // Don't try to prove assumption properties. - if(symbol.value.id() == ID_sva_assume) + if(properties.properties.back().is_assumption()) { - properties.properties.back().status = propertyt::statust::ASSUMED; + properties.properties.back().assumed(); properties.properties.back().normalized_expr = normalize_property(to_sva_assume_expr(symbol.value).op()); } diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h index 8ebd1c86..4f777dd3 100644 --- a/src/ebmc/ebmc_properties.h +++ b/src/ebmc/ebmc_properties.h @@ -40,6 +40,7 @@ class ebmc_propertiest UNKNOWN, // no work done yet DISABLED, // turned off by user ASSUMED, // property is assumed to be true, unbounded + UNSUPPORTED, // property is unsupported PROVED, // property is true, unbounded PROVED_WITH_BOUND, // property is true, with bound REFUTED, // property is false, possibly counterexample @@ -98,24 +99,38 @@ class ebmc_propertiest return status == statust::FAILURE; } + bool is_unsupported() const + { + return status == statust::UNSUPPORTED; + } + bool is_inconclusive() const { return status == statust::INCONCLUSIVE; } + void assumed() + { + status = statust::ASSUMED; + failure_reason = {}; + } + void unknown() { status = statust::UNKNOWN; + failure_reason = {}; } void disable() { status = statust::DISABLED; + failure_reason = {}; } void proved() { status = statust::PROVED; + failure_reason = {}; } void proved_with_bound(std::size_t _bound) @@ -127,17 +142,20 @@ class ebmc_propertiest void refuted() { status = statust::REFUTED; + failure_reason = {}; } void refuted_with_bound(std::size_t _bound) { status = statust::REFUTED_WITH_BOUND; bound = _bound; + failure_reason = {}; } void drop() { status = statust::DROPPED; + failure_reason = {}; } void failure(const std::optional &reason = {}) @@ -146,9 +164,16 @@ class ebmc_propertiest failure_reason = reason; } + void unsupported(const std::optional &reason = {}) + { + status = statust::UNSUPPORTED; + failure_reason = reason; + } + void inconclusive() { status = statust::INCONCLUSIVE; + failure_reason = {}; } std::string status_as_string() const; @@ -164,16 +189,30 @@ class ebmc_propertiest { return ::is_exists_path(original_expr); } + + bool is_assumption() const + { + return original_expr.id() == ID_sva_assume; + } }; typedef std::list propertiest; propertiest properties; - bool has_unknown_property() const + bool has_unfinished_property() const { for(const auto &p : properties) - if(p.is_unknown()) + { + if(p.is_assumption()) + { + } + else if( + p.is_unknown() || p.is_unsupported() || p.is_failure() || + p.is_inconclusive()) + { return true; + } + } return false; } @@ -209,12 +248,40 @@ class ebmc_propertiest return result; } - void reset_failure_to_unknown() + /// Resets properties/assumptions in FAILURE state to + /// ASSUMED/UNKNOWN respectively. + void reset_failure() { for(auto &p : properties) if(p.is_failure()) + { + if(p.is_assumption()) + p.assumed(); + else + p.unknown(); + } + } + + /// Resets properties in INCONCLUSIVE state to UNKNOWN. + void reset_inconclusive() + { + for(auto &p : properties) + if(p.is_inconclusive()) p.unknown(); } + + /// Resets properties in UNSUPPORTED state to UNKNOWN/ASSUMED. + void reset_unsupported() + { + for(auto &p : properties) + if(p.is_unsupported()) + { + if(p.is_assumption()) + p.assumed(); + else + p.unknown(); + } + } }; #endif // CPROVER_EBMC_PROPERTIES_H diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index 9123617d..123a6f81 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -170,16 +170,42 @@ Function: k_inductiont::operator() void k_inductiont::operator()() { + // Unsupported assumption? Mark as such. + bool assumption_unsupported = false; + for(auto &property : properties.properties) + { + if(!supported(property) && property.is_assumed()) + { + assumption_unsupported = true; + property.unsupported("unsupported by k-induction"); + } + } + // Fail unsupported properties for(auto &property : properties.properties) { - if(!supported(property)) - property.failure("property unsupported by k-induction"); + if( + !supported(property) && !property.is_assumed() && !property.is_disabled()) + { + property.unsupported("unsupported by k-induction"); + } } // do induction base induction_base(); + // Any refuted properties are really inconclusive if there are + // unsupported assumptions, as the assumption might have + // proven the property. + if(assumption_unsupported) + { + for(auto &property : properties.properties) + { + if(property.is_refuted()) + property.unknown(); + } + } + // do induction step induction_step(); } @@ -231,8 +257,12 @@ void k_inductiont::induction_step() for(auto &p_it : properties.properties) { - if(p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed()) + if( + p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed() || + p_it.is_unsupported()) + { continue; + } // If it's not failed, then it's supported. DATA_INVARIANT(supported(p_it), "property must be supported"); diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 39b5ee9c..833392ad 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -372,7 +372,7 @@ property_checker_resultt engine_heuristic( auto solver_factory = ebmc_solver_factory(cmdline); - if(!properties.has_unknown_property()) + if(!properties.has_unfinished_property()) return property_checker_resultt{properties}; // done message.status() << "No engine given, attempting heuristic engine selection" @@ -384,12 +384,15 @@ property_checker_resultt engine_heuristic( k_induction( 1, transition_system, properties, solver_factory, message_handler); - properties.reset_failure_to_unknown(); - - if(!properties.has_unknown_property()) + if(!properties.has_unfinished_property()) return property_checker_resultt{properties}; // done + properties.reset_failure(); + properties.reset_inconclusive(); + properties.reset_unsupported(); + // Now try BMC with bound 5, word-level + message.status() << "Attempting BMC with bound 5" << messaget::eom; bmc( 5, // bound @@ -400,11 +403,11 @@ property_checker_resultt engine_heuristic( solver_factory, message_handler); - properties.reset_failure_to_unknown(); - - if(!properties.has_unknown_property()) + if(!properties.has_unfinished_property()) return property_checker_resultt{properties}; // done + properties.reset_failure(); + // Give up return property_checker_resultt{properties}; // done } diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h index d1fe7f00..bd59e6b8 100644 --- a/src/ebmc/property_checker.h +++ b/src/ebmc/property_checker.h @@ -50,12 +50,18 @@ class property_checker_resultt bool all_properties_proved() const { for(const auto &p : properties) - if( + { + if(p.is_assumption()) + { + // ignore + } + else if( !p.is_proved() && !p.is_proved_with_bound() && !p.is_disabled() && !p.is_assumed()) { return false; } + } return true; } diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 88523d15..6469c0d9 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -111,6 +111,7 @@ void report_results( case statust::DROPPED: message.status() << messaget::red; break; case statust::FAILURE: message.status() << messaget::red; break; case statust::UNKNOWN: message.status() << messaget::yellow; break; + case statust::UNSUPPORTED: message.status() << messaget::yellow; break; case statust::DISABLED: break; case statust::INCONCLUSIVE: message.status() << messaget::yellow; break; } diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 1a44dca7..70acd2fb 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -696,6 +696,7 @@ void property( auto obligations = property_obligations(property_expr, no_timeframes); // Map obligations onto timeframes. + prop_handles.clear(); prop_handles.resize(no_timeframes, true_exprt()); for(auto &obligation_it : obligations.map) {