From ac413a0b81bfeb75fbcc24b681d830b0fa6d03ce Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 6 Jan 2025 18:14:28 +0000 Subject: [PATCH] Engine heuristic: fix for assumptions unsupported by k-induction The k-induction engine now correctly reports unsupported assumptions, and is then skipped by the engine selection heuristic. Fixes #921. --- regression/ebmc/engine-heuristic/basic1.desc | 10 +++++++ regression/ebmc/engine-heuristic/basic1.sv | 8 ++++++ regression/ebmc/k-induction/k-induction6.desc | 7 ++--- regression/ebmc/k-induction/k-induction7.desc | 11 ++++++++ regression/ebmc/k-induction/k-induction7.sv | 15 +++++++++++ src/ebmc/ebmc_properties.cpp | 4 +-- src/ebmc/ebmc_properties.h | 27 ++++++++++++++++++- src/ebmc/k_induction.cpp | 25 ++++++++++++++++- src/ebmc/property_checker.cpp | 6 +++-- src/ebmc/property_checker.h | 8 +++++- 10 files changed, 111 insertions(+), 10 deletions(-) create mode 100644 regression/ebmc/engine-heuristic/basic1.desc create mode 100644 regression/ebmc/engine-heuristic/basic1.sv create mode 100644 regression/ebmc/k-induction/k-induction7.desc create mode 100644 regression/ebmc/k-induction/k-induction7.sv diff --git a/regression/ebmc/engine-heuristic/basic1.desc b/regression/ebmc/engine-heuristic/basic1.desc new file mode 100644 index 000000000..15ebc6b69 --- /dev/null +++ b/regression/ebmc/engine-heuristic/basic1.desc @@ -0,0 +1,10 @@ +CORE +baseic1.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 000000000..4c7ada49c --- /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/k-induction/k-induction6.desc b/regression/ebmc/k-induction/k-induction6.desc index 7b106e616..0d32dc6e8 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: FAILURE: property 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 000000000..e677a5e08 --- /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: FAILURE: property 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 000000000..c48fbb156 --- /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/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp index daa0d07c8..5ad2db6be 100644 --- a/src/ebmc/ebmc_properties.cpp +++ b/src/ebmc/ebmc_properties.cpp @@ -78,9 +78,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 8ebd1c861..68aca09a6 100644 --- a/src/ebmc/ebmc_properties.h +++ b/src/ebmc/ebmc_properties.h @@ -103,6 +103,11 @@ class ebmc_propertiest return status == statust::INCONCLUSIVE; } + void assumed() + { + status = statust::ASSUMED; + } + void unknown() { status = statust::UNKNOWN; @@ -164,6 +169,11 @@ class ebmc_propertiest { return ::is_exists_path(original_expr); } + + bool is_assumption() const + { + return original_expr.id() == ID_sva_assume; + } }; typedef std::list propertiest; @@ -209,10 +219,25 @@ 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(); } }; diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index 9123617d4..189b76e79 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -170,16 +170,39 @@ 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.failure("assumption unsupported by k-induction"); + } + } + // Fail unsupported properties for(auto &property : properties.properties) { - if(!supported(property)) + if(!supported(property) && !property.is_assumed()) property.failure("property 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(); } diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 39b5ee9cd..bef572767 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -384,12 +384,14 @@ property_checker_resultt engine_heuristic( k_induction( 1, transition_system, properties, solver_factory, message_handler); - properties.reset_failure_to_unknown(); + properties.reset_failure(); + properties.reset_inconclusive(); if(!properties.has_unknown_property()) return property_checker_resultt{properties}; // done // Now try BMC with bound 5, word-level + message.status() << "Attempting BMC with bound 5" << messaget::eom; bmc( 5, // bound @@ -400,7 +402,7 @@ property_checker_resultt engine_heuristic( solver_factory, message_handler); - properties.reset_failure_to_unknown(); + properties.reset_failure(); if(!properties.has_unknown_property()) return property_checker_resultt{properties}; // done diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h index d1fe7f008..bd59e6b88 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; }