From b5fe0b2be818b32ae5f2144f7e7d7c1dff519779 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 6 Aug 2025 13:16:24 -0700 Subject: [PATCH] EBMC: tautology checker This adds a property tautology check ask the first step to the engine selection. While it should be rare that this pass proves a property, the fact that it does may suggest that the property is unintentionally vacuous. --- .../ebmc-spot/sva-buechi/sequence5.desc | 2 +- regression/ebmc-spot/sva-buechi/sva_and1.desc | 2 +- regression/ebmc-spot/sva-buechi/sva_iff1.desc | 2 +- .../ebmc-spot/sva-buechi/sva_implies1.desc | 2 +- regression/ebmc-spot/sva-buechi/sva_not1.desc | 2 +- .../ebmc/engine-heuristic/tautology1.desc | 16 ++++ .../ebmc/engine-heuristic/tautology1.smv | 10 +++ src/ebmc/Makefile | 1 + src/ebmc/instrument_buechi.cpp | 23 +++-- src/ebmc/property_checker.cpp | 18 +++- src/ebmc/tautology_check.cpp | 84 +++++++++++++++++++ src/ebmc/tautology_check.h | 25 ++++++ 12 files changed, 174 insertions(+), 13 deletions(-) create mode 100644 regression/ebmc/engine-heuristic/tautology1.desc create mode 100644 regression/ebmc/engine-heuristic/tautology1.smv create mode 100644 src/ebmc/tautology_check.cpp create mode 100644 src/ebmc/tautology_check.h diff --git a/regression/ebmc-spot/sva-buechi/sequence5.desc b/regression/ebmc-spot/sva-buechi/sequence5.desc index a331f43e8..c991148e1 100644 --- a/regression/ebmc-spot/sva-buechi/sequence5.desc +++ b/regression/ebmc-spot/sva-buechi/sequence5.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/sequence5.sv --buechi -^\[main\.p0\] 1: PROVED up to bound \d+$ +^\[main\.p0\] 1: PROVED \(tautology\)$ ^\[main\.p1\] 0: REFUTED$ ^\[main\.p2\] 1'bx: REFUTED$ ^\[main\.p3\] 1'bz: REFUTED$ diff --git a/regression/ebmc-spot/sva-buechi/sva_and1.desc b/regression/ebmc-spot/sva-buechi/sva_and1.desc index 11606f320..e90d5e423 100644 --- a/regression/ebmc-spot/sva-buechi/sva_and1.desc +++ b/regression/ebmc-spot/sva-buechi/sva_and1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/sva_and1.sv --buechi -^\[main\.p0\] always \(1 and 1\): PROVED up to bound \d+$ +^\[main\.p0\] always \(1 and 1\): PROVED \(tautology\)$ ^\[main\.p1\] always \(1 and 0\): REFUTED$ ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$ ^EXIT=10$ diff --git a/regression/ebmc-spot/sva-buechi/sva_iff1.desc b/regression/ebmc-spot/sva-buechi/sva_iff1.desc index b2a7ad54a..c22d15290 100644 --- a/regression/ebmc-spot/sva-buechi/sva_iff1.desc +++ b/regression/ebmc-spot/sva-buechi/sva_iff1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/sva_iff1.sv --buechi -^\[main\.p0\] always \(1 iff 1\): PROVED up to bound \d+$ +^\[main\.p0\] always \(1 iff 1\): PROVED \(tautology\)$ ^\[main\.p1\] always \(1 iff 0\): REFUTED$ ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$ ^EXIT=10$ diff --git a/regression/ebmc-spot/sva-buechi/sva_implies1.desc b/regression/ebmc-spot/sva-buechi/sva_implies1.desc index 518185134..19d096ae5 100644 --- a/regression/ebmc-spot/sva-buechi/sva_implies1.desc +++ b/regression/ebmc-spot/sva-buechi/sva_implies1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/sva_implies1.sv --buechi -^\[main\.p0\] always \(1 implies 1\): PROVED up to bound \d+$ +^\[main\.p0\] always \(1 implies 1\): PROVED \(tautology\)$ ^\[main\.p1\] always \(1 implies 0\): REFUTED$ ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$ ^EXIT=10$ diff --git a/regression/ebmc-spot/sva-buechi/sva_not1.desc b/regression/ebmc-spot/sva-buechi/sva_not1.desc index 5831727ec..5fa7ec963 100644 --- a/regression/ebmc-spot/sva-buechi/sva_not1.desc +++ b/regression/ebmc-spot/sva-buechi/sva_not1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/sva_not1.sv --buechi -^\[main\.p0] always not 0: PROVED up to bound \d+$ +^\[main\.p0] always not 0: PROVED \(tautology\)$ ^\[main\.p1] always not 1: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/ebmc/engine-heuristic/tautology1.desc b/regression/ebmc/engine-heuristic/tautology1.desc new file mode 100644 index 000000000..882a17e74 --- /dev/null +++ b/regression/ebmc/engine-heuristic/tautology1.desc @@ -0,0 +1,16 @@ +CORE +tautology1.smv + +^\[.*\] 2 > 1: PROVED \(tautology\)$ +^\[.*\] G 2 > 1: PROVED \(tautology\)$ +^\[.*\] X 2 > 1: PROVED \(tautology\)$ +^\[.*\] F 2 > 1: PROVED \(tautology\)$ +^\[.*\] 2 > 1: PROVED \(tautology\)$ +^\[.*\] AG 2 > 1: PROVED \(tautology\)$ +^\[.*\] AX 2 > 1: PROVED \(tautology\)$ +^\[.*\] AF 2 > 1: PROVED \(tautology\)$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/engine-heuristic/tautology1.smv b/regression/ebmc/engine-heuristic/tautology1.smv new file mode 100644 index 000000000..96489f71e --- /dev/null +++ b/regression/ebmc/engine-heuristic/tautology1.smv @@ -0,0 +1,10 @@ +MODULE main + +LTLSPEC 2>1 +LTLSPEC G 2>1 +LTLSPEC X 2>1 +LTLSPEC F 2>1 +CTLSPEC 2>1 +CTLSPEC AG 2>1 +CTLSPEC AX 2>1 +CTLSPEC AF 2>1 diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 44193f002..6dad84f45 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -36,6 +36,7 @@ SRC = \ show_formula_solver.cpp \ show_properties.cpp \ show_trans.cpp \ + tautology_check.cpp \ transition_system.cpp \ waveform.cpp \ #empty line diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp index e082aeb08..22e9c1126 100644 --- a/src/ebmc/instrument_buechi.cpp +++ b/src/ebmc/instrument_buechi.cpp @@ -64,15 +64,24 @@ void instrument_buechi( transition_system.trans_expr.trans() = and_exprt{transition_system.trans_expr.trans(), buechi.trans}; - // Replace the normalized property expression. - // Note that we have negated the property, - // so this is the negation of the Buechi acceptance condition. - property.normalized_expr = - F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}}; + // Replace the normalized property expression + // by the Buechi acceptance condition. + exprt::operandst property_conjuncts; + + if(!buechi.liveness_signal.is_false()) + { + // Note that we have negated the property, + // so this is the negation of the Buechi acceptance condition. + property_conjuncts.push_back( + F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}}); + } if(!buechi.error_signal.is_true()) - property.normalized_expr = and_exprt{ - property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}}; + { + property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}}); + } + + property.normalized_expr = conjunction(property_conjuncts); message.debug() << "New property: " << format(property.normalized_expr) << messaget::eom; diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index d18d72921..664300cc2 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "netlist.h" #include "output_file.h" #include "report_results.h" +#include "tautology_check.h" #include #include @@ -382,7 +383,22 @@ property_checker_resultt engine_heuristic( message.status() << "No engine given, attempting heuristic engine selection" << messaget::eom; - // First check whether we have a low completenes threshold + // First check if we can tell that the property is a tautology + message.status() << "Tautology check" << messaget::eom; + + auto tautology_check_result = + tautology_check(cmdline, properties, solver_factory, message_handler); + + properties.properties = tautology_check_result.properties; + + if(!properties.has_unfinished_property()) + return tautology_check_result; // done + + properties.reset_failure(); + properties.reset_inconclusive(); + properties.reset_unsupported(); + + // Check whether we have a low completenes threshold message.status() << "Attempting completeness threshold" << messaget::eom; auto completeness_threshold_result = completeness_threshold( diff --git a/src/ebmc/tautology_check.cpp b/src/ebmc/tautology_check.cpp new file mode 100644 index 000000000..45241aecb --- /dev/null +++ b/src/ebmc/tautology_check.cpp @@ -0,0 +1,84 @@ +/*******************************************************************\ + +Module: Property Tautology Check + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "tautology_check.h" + +#include + +#include +#include + +static bool is_tautology( + const exprt &expr, + const ebmc_solver_factoryt &solver_factory, + message_handlert &message_handler) +{ + auto is_tautology_p = [&solver_factory, &message_handler](const exprt &expr) + { + // rec. call + return is_tautology(expr, solver_factory, message_handler); + }; + + if(!has_temporal_operator(expr)) + { + // State predicate. Let's ask the SAT solver. + if(expr.is_true()) + return true; + + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + auto solver = solver_factory(ns, message_handler); + + switch(solver.decision_procedure()(not_exprt{expr})) + { + case decision_proceduret::resultt::D_UNSATISFIABLE: + return true; + + case decision_proceduret::resultt::D_SATISFIABLE: + case decision_proceduret::resultt::D_ERROR: + default: + return false; + } + } + else // has temporal operator + { + if(expr.id() == ID_G && is_tautology_p(to_G_expr(expr).op())) + return true; + else if(expr.id() == ID_F && is_tautology_p(to_F_expr(expr).op())) + return true; + else if(expr.id() == ID_X && is_tautology_p(to_X_expr(expr).op())) + return true; + else if(expr.id() == ID_AG && is_tautology_p(to_AG_expr(expr).op())) + return true; + else if(expr.id() == ID_AF && is_tautology_p(to_AF_expr(expr).op())) + return true; + else if(expr.id() == ID_AX && is_tautology_p(to_AX_expr(expr).op())) + return true; + else // other temporal operator + return false; + } +} + +property_checker_resultt tautology_check( + const cmdlinet &, + const ebmc_propertiest &properties, + const ebmc_solver_factoryt &solver_factory, + message_handlert &message_handler) +{ + property_checker_resultt result{properties}; + + for(auto &property : result.properties) + { + if(is_tautology(property.normalized_expr, solver_factory, message_handler)) + { + property.proved("tautology"); + } + } + + return result; +} diff --git a/src/ebmc/tautology_check.h b/src/ebmc/tautology_check.h new file mode 100644 index 000000000..99020bf53 --- /dev/null +++ b/src/ebmc/tautology_check.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Property Tautology Check + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_TAUTOLOGY_CHECK_H +#define CPROVER_EBMC_TAUTOLOGY_CHECK_H + +#include "ebmc_solver_factory.h" +#include "property_checker.h" + +class cmdlinet; +class ebmc_propertiest; +class message_handlert; + +[[nodiscard]] property_checker_resultt tautology_check( + const cmdlinet &, + const ebmc_propertiest &, + const ebmc_solver_factoryt &, + message_handlert &); + +#endif