diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc index 93180a052..5b49c63d3 100644 --- a/regression/verilog/SVA/cover1.desc +++ b/regression/verilog/SVA/cover1.desc @@ -1,8 +1,11 @@ -KNOWNBUG +CORE cover1.sv ---bound 10 -^\[main\.property\.p0\] cover main\.counter == 1: REFUTED$ -^\[main\.property\.p1\] cover main\.counter == 100: REFUTED$ +--bound 10 --numbered-trace +^\[main\.property\.p0\] cover main\.counter == 1: PROVED$ +^Trace:$ +^main\.counter@0 = 0$ +^main\.counter@1 = 1$ +^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index 9fa25915a..70d29598e 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -402,7 +402,7 @@ void bdd_enginet::compute_counterexample( throw "unexpected result from SAT solver"; } - property.counterexample = + property.witness_trace = compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns); } diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index c83c0896e..6fd683f74 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -98,17 +98,25 @@ void bmc( message.status() << "Checking " << property.name << messaget::eom; - auto assumption = not_exprt(conjunction(property.timeframe_handles)); + auto assumption = not_exprt{conjunction(property.timeframe_handles)}; decision_proceduret::resultt dec_result = solver(assumption); switch(dec_result) { case decision_proceduret::resultt::D_SATISFIABLE: - property.refuted(); - message.result() << "SAT: counterexample found" << messaget::eom; - - property.counterexample = compute_trans_trace( + if(property.is_exists_path()) + { + property.proved(); + message.result() << "SAT: path found" << messaget::eom; + } + else // universal path property + { + property.refuted(); + message.result() << "SAT: counterexample found" << messaget::eom; + } + + property.witness_trace = compute_trans_trace( property.timeframe_handles, solver, bound + 1, @@ -117,9 +125,18 @@ void bmc( break; case decision_proceduret::resultt::D_UNSATISFIABLE: - message.result() << "UNSAT: No counterexample found within bound" - << messaget::eom; - property.proved_with_bound(bound); + if(property.is_exists_path()) + { + message.result() << "UNSAT: No path found within bound" + << messaget::eom; + property.refuted_with_bound(bound); + } + else // universal path property + { + message.result() << "UNSAT: No counterexample found within bound" + << messaget::eom; + property.proved_with_bound(bound); + } break; case decision_proceduret::resultt::D_ERROR: diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index 14f2645d8..c62d9f666 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -95,7 +95,7 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver) namespacet ns(transition_system.symbol_table); - property.counterexample = + property.witness_trace = compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns); } break; diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp index 3cab9980b..b2f191910 100644 --- a/src/ebmc/ebmc_properties.cpp +++ b/src/ebmc/ebmc_properties.cpp @@ -26,6 +26,8 @@ std::string ebmc_propertiest::propertyt::status_as_string() const return "PROVED up to bound " + std::to_string(bound); case statust::REFUTED: return "REFUTED"; + case statust::REFUTED_WITH_BOUND: + return "REFUTED up to bound " + std::to_string(bound); case statust::UNKNOWN: return "UNKNOWN"; case statust::INCONCLUSIVE: diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h index 4f941faac..ae4b3bd17 100644 --- a/src/ebmc/ebmc_properties.h +++ b/src/ebmc/ebmc_properties.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include #include #include @@ -37,23 +38,24 @@ class ebmc_propertiest enum class statust { - UNKNOWN, // no work done yet - DISABLED, // turned off by user - PROVED, // property is true, unbounded - PROVED_WITH_BOUND, // property is true, with bound - REFUTED, // property is false, possibly counterexample - DROPPED, // given up - FAILURE, // error during anaysis - INCONCLUSIVE // analysis can't determine truth + UNKNOWN, // no work done yet + DISABLED, // turned off by user + PROVED, // property is true, unbounded + PROVED_WITH_BOUND, // property is true, with bound + REFUTED, // property is false, possibly counterexample + REFUTED_WITH_BOUND, // property is false, with bound + DROPPED, // given up + FAILURE, // error during anaysis + INCONCLUSIVE // analysis can't determine truth } status = statust::UNKNOWN; std::size_t bound = 0; - std::optional counterexample; + std::optional witness_trace; std::optional failure_reason; - bool has_counterexample() const + bool has_witness_trace() const { - return counterexample.has_value(); + return witness_trace.has_value(); } bool is_unknown() const @@ -122,6 +124,12 @@ class ebmc_propertiest status = statust::REFUTED; } + void refuted_with_bound(std::size_t _bound) + { + status = statust::REFUTED_WITH_BOUND; + bound = _bound; + } + void drop() { status = statust::DROPPED; @@ -146,6 +154,11 @@ class ebmc_propertiest { return ::requires_lasso_constraints(normalized_expr); } + + bool is_exists_path() const + { + return ::is_exists_path(original_expr); + } }; typedef std::list propertiest; diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 09bf64e2c..b7f75a9fe 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -58,9 +58,8 @@ void report_results( json_property["identifier"] = json_stringt(id2string(property.name)); json_property["status"] = json_stringt(property.status_as_string()); - if(property.has_counterexample()) - json_property["counterexample"] = - json(property.counterexample.value(), ns); + if(property.has_witness_trace()) + json_property["trace"] = json(property.witness_trace.value(), ns); json_properties.push_back(std::move(json_property)); } @@ -81,8 +80,8 @@ void report_results( xml_result.set_attribute("property", id2string(property.name)); xml_result.set_attribute("status", property.status_as_string()); - if(property.has_counterexample()) - xml_result.new_element() = xml(property.counterexample.value(), ns); + if(property.has_witness_trace()) + xml_result.new_element() = xml(property.witness_trace.value(), ns); std::cout << xml_result << '\n' << std::flush; } @@ -109,6 +108,7 @@ void report_results( case statust::PROVED: message.status() << messaget::green; break; case statust::PROVED_WITH_BOUND: message.status() << messaget::green; break; case statust::REFUTED: message.status() << messaget::bright_red; break; + case statust::REFUTED_WITH_BOUND: message.status() << messaget::bright_red; break; case statust::DROPPED: message.status() << messaget::red; break; case statust::FAILURE: message.status() << messaget::red; break; case statust::UNKNOWN: message.status() << messaget::yellow; break; @@ -121,24 +121,28 @@ void report_results( message.status() << messaget::reset << messaget::eom; - if(property.has_counterexample()) + if(property.has_witness_trace()) { + auto term = [&property]() { + return property.is_exists_path() ? "Trace" : "Counterexample"; + }; + if(cmdline.isset("trace")) { - message.status() << "Counterexample:\n" << messaget::eom; + message.status() << term() << ":\n" << messaget::eom; show_trans_trace( - property.counterexample.value(), message, ns, std::cout); + property.witness_trace.value(), message, ns, std::cout); } else if(cmdline.isset("numbered-trace")) { - message.status() << "Counterexample:\n" << messaget::eom; + message.status() << term() << ":" << messaget::eom; show_trans_trace_numbered( - property.counterexample.value(), message, ns, std::cout); + property.witness_trace.value(), message, ns, std::cout); } else if(cmdline.isset("waveform")) { - message.status() << "Counterexample:" << messaget::eom; - show_waveform(property.counterexample.value(), ns); + message.status() << term() << ":" << messaget::eom; + show_waveform(property.witness_trace.value(), ns); } } } @@ -148,13 +152,13 @@ void report_results( { for(const auto &property : properties.properties) { - if(property.has_counterexample()) + if(property.has_witness_trace()) { std::string vcdfile = cmdline.get_value("vcd"); std::ofstream vcd(widen_if_needed(vcdfile)); messaget message(message_handler); - show_trans_trace_vcd(property.counterexample.value(), message, ns, vcd); + show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd); break; } diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index aa7416670..77d7fae14 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -36,3 +36,8 @@ bool has_temporal_operator(const exprt &expr) return false; } + +bool is_exists_path(const exprt &expr) +{ + return expr.id() == ID_sva_cover; +} diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index f636e942d..54392d43a 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -18,4 +18,8 @@ bool has_temporal_operator(const exprt &); /// as its root bool is_temporal_operator(const exprt &); +/// Returns true iff the given expression is an existential path +/// property. +bool is_exists_path(const exprt &); + #endif