From 998bb30bc9d19b2049ef3513cb5ee4b9b452dcb4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 20 Sep 2024 18:16:24 -0700 Subject: [PATCH] BMC: support full LTL Full LTL is supported by the word-level BMC engine. --- regression/ebmc/smv/smv_ltlspec6.desc | 7 + regression/ebmc/smv/smv_ltlspec6.smv | 29 ++++ regression/ebmc/smv/smv_ltlspec_F1.desc | 6 +- regression/ebmc/smv/smv_ltlspec_F2.desc | 8 +- regression/ebmc/smv/smv_ltlspec_G1.desc | 6 +- regression/ebmc/smv/smv_ltlspec_G2.desc | 8 +- regression/ebmc/smv/smv_ltlspec_R1.desc | 12 +- regression/ebmc/smv/smv_ltlspec_U1.desc | 10 +- regression/verilog/SVA/sva_until1.desc | 9 +- src/temporal-logic/normalize_property.cpp | 4 +- src/trans-word-level/property.cpp | 163 ++++++++++++++++------ 11 files changed, 186 insertions(+), 76 deletions(-) create mode 100644 regression/ebmc/smv/smv_ltlspec6.desc create mode 100644 regression/ebmc/smv/smv_ltlspec6.smv diff --git a/regression/ebmc/smv/smv_ltlspec6.desc b/regression/ebmc/smv/smv_ltlspec6.desc new file mode 100644 index 00000000..cbb97eb4 --- /dev/null +++ b/regression/ebmc/smv/smv_ltlspec6.desc @@ -0,0 +1,7 @@ +CORE broken-smt-backend +smv_ltlspec6.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec6.smv b/regression/ebmc/smv/smv_ltlspec6.smv new file mode 100644 index 00000000..5bc2c5cd --- /dev/null +++ b/regression/ebmc/smv/smv_ltlspec6.smv @@ -0,0 +1,29 @@ +MODULE main + +VAR x : 0..3; + +ASSIGN + init(x) := 1; + + next(x) := + case + x=3 : 3; + TRUE: x+1; + esac; + +DEFINE p := x != 0; +DEFINE q := x = 3; + +-- various equivalences +LTLSPEC (G p) <-> (G G p) +LTLSPEC (G p) <-> (!F !p) +LTLSPEC (G p) <-> (p & X G p) +LTLSPEC (FALSE R p) -> (G p) +LTLSPEC (G (p&q)) <-> ((G p) & (G q)) + +LTLSPEC (F p) <-> (F F p) +LTLSPEC (F p) <-> (!G x = 0) +LTLSPEC (F p) <-> (p | X F p) +LTLSPEC (F (p|q)) <-> ((F p) | (F q)) + +LTLSPEC (X p) <-> (!X !p) diff --git a/regression/ebmc/smv/smv_ltlspec_F1.desc b/regression/ebmc/smv/smv_ltlspec_F1.desc index a6f78bcc..e716671d 100644 --- a/regression/ebmc/smv/smv_ltlspec_F1.desc +++ b/regression/ebmc/smv/smv_ltlspec_F1.desc @@ -8,8 +8,8 @@ smv_ltlspec_F1.smv ^\[.*\] F x = 2: PROVED up to bound 10$ ^\[.*\] F x = 1 & F x = 2: PROVED up to bound 10$ ^\[.*\] F x = 0 & F x = 1: REFUTED$ -^\[.*\] F x = 0 \| F x = 1: FAILURE: property not supported by BMC engine$ -^\[.*\] F x = 0 -> FALSE: FAILURE: property not supported by BMC engine$ -^\[.*\] F x = 1 -> F x = 0: FAILURE: property not supported by BMC engine$ +^\[.*\] F x = 0 \| F x = 1: PROVED up to bound 10$ +^\[.*\] F x = 0 -> FALSE: PROVED up to bound 10$ +^\[.*\] F x = 1 -> F x = 0: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec_F2.desc b/regression/ebmc/smv/smv_ltlspec_F2.desc index 979ab536..7b672c25 100644 --- a/regression/ebmc/smv/smv_ltlspec_F2.desc +++ b/regression/ebmc/smv/smv_ltlspec_F2.desc @@ -6,10 +6,10 @@ smv_ltlspec_F2.smv ^\[.*\] !F x = 0: PROVED up to bound 10$ ^\[.*\] !F x = 1: REFUTED$ ^\[.*\] !F x = 2: REFUTED$ -^\[.*\] !\(F x = 1 & F x = 2\): FAILURE: property not supported by BMC engine$ -^\[.*\] !\(F x = 0 & F x = 1\): FAILURE: property not supported by BMC engine$ +^\[.*\] !\(F x = 1 & F x = 2\): REFUTED$ +^\[.*\] !\(F x = 0 & F x = 1\): PROVED up to bound 10$ ^\[.*\] !\(F x = 0 \| F x = 1\): REFUTED$ -^\[.*\] !\(F x = 0 -> FALSE\): FAILURE: property not supported by BMC engine$ -^\[.*\] !\(F x = 1 -> F x = 0\): FAILURE: property not supported by BMC engine$ +^\[.*\] !\(F x = 0 -> FALSE\): REFUTED$ +^\[.*\] !\(F x = 1 -> F x = 0\): PROVED up to bound 10$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec_G1.desc b/regression/ebmc/smv/smv_ltlspec_G1.desc index 93e357d6..f36e383c 100644 --- a/regression/ebmc/smv/smv_ltlspec_G1.desc +++ b/regression/ebmc/smv/smv_ltlspec_G1.desc @@ -8,8 +8,8 @@ smv_ltlspec_G1.smv ^\[.*\] G x != 2: REFUTED$ ^\[.*\] G x != 5 & G x != 6: PROVED up to bound 10$ ^\[.*\] G x != 2 & G x != 5: REFUTED$ -^\[.*\] G x != 5 \| G x != 2: FAILURE: property not supported by BMC engine$ -^\[.*\] G x != 2 -> FALSE: FAILURE: property not supported by BMC engine$ -^\[.*\] G x != 5 -> G x != 2: FAILURE: property not supported by BMC engine$ +^\[.*\] G x != 5 \| G x != 2: PROVED up to bound 10$ +^\[.*\] G x != 2 -> FALSE: PROVED up to bound 10$ +^\[.*\] G x != 5 -> G x != 2: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec_G2.desc b/regression/ebmc/smv/smv_ltlspec_G2.desc index 8748a933..e32cce87 100644 --- a/regression/ebmc/smv/smv_ltlspec_G2.desc +++ b/regression/ebmc/smv/smv_ltlspec_G2.desc @@ -6,10 +6,10 @@ smv_ltlspec_G2.smv ^\[.*\] !G x != 5: REFUTED$ ^\[.*\] !G x != 6: REFUTED$ ^\[.*\] !G x != 2: PROVED up to bound 10$ -^\[.*\] !\(G x != 5 & G x != 6\): FAILURE: property not supported by BMC engine$ -^\[.*\] !\(G x != 2 & G x != 5\): FAILURE: property not supported by BMC engine$ +^\[.*\] !\(G x != 5 & G x != 6\): REFUTED$ +^\[.*\] !\(G x != 2 & G x != 5\): PROVED up to bound 10$ ^\[.*\] !\(G x != 5 \| G x != 2\): REFUTED$ -^\[.*\] !\(G x != 2 -> FALSE\): FAILURE: property not supported by BMC engine$ -^\[.*\] !\(G x != 5 -> G x != 2\): FAILURE: property not supported by BMC engine$ +^\[.*\] !\(G x != 2 -> FALSE\): REFUTED$ +^\[.*\] !\(G x != 5 -> G x != 2\): PROVED up to bound 10$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec_R1.desc b/regression/ebmc/smv/smv_ltlspec_R1.desc index a262be27..0d2e21a8 100644 --- a/regression/ebmc/smv/smv_ltlspec_R1.desc +++ b/regression/ebmc/smv/smv_ltlspec_R1.desc @@ -1,12 +1,12 @@ CORE broken-smt-backend smv_ltlspec_R1.smv --bound 10 -^\[.*\] x >= 1 R x = 1: FAILURE: property not supported by BMC engine$ -^\[.*\] FALSE R x != 4: FAILURE: property not supported by BMC engine$ -^\[.*\] x = 2 R x = 1: FAILURE: property not supported by BMC engine$ -^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: FAILURE: property not supported by BMC engine$ -^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: FAILURE: property not supported by BMC engine$ -^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: FAILURE: property not supported by BMC engine$ +^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$ +^\[.*\] FALSE R x != 4: REFUTED$ +^\[.*\] x = 2 R x = 1: REFUTED$ +^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: REFUTED$ +^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$ +^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/smv/smv_ltlspec_U1.desc b/regression/ebmc/smv/smv_ltlspec_U1.desc index fc922183..c9ab5ee0 100644 --- a/regression/ebmc/smv/smv_ltlspec_U1.desc +++ b/regression/ebmc/smv/smv_ltlspec_U1.desc @@ -1,11 +1,11 @@ CORE broken-smt-backend smv_ltlspec_U1.smv --bound 10 -\[.*\] x = 1 U x = 2: FAILURE: property not supported by BMC engine$ -\[.*\] x != 0 U FALSE: FAILURE: property not supported by BMC engine$ -\[.*\] x = 1 U x = 3: FAILURE: property not supported by BMC engine$ -\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: FAILURE: property not supported by BMC engine$ -\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: FAILURE: property not supported by BMC engine$ +\[.*\] x = 1 U x = 2: PROVED up to bound 10$ +\[.*\] x != 0 U FALSE: PROVED up to bound 10$ +\[.*\] x = 1 U x = 3: REFUTED$ +\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: PROVED up to bound 10$ +\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: PROVED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sva_until1.desc b/regression/verilog/SVA/sva_until1.desc index 4e6a5111..7c43408d 100644 --- a/regression/verilog/SVA/sva_until1.desc +++ b/regression/verilog/SVA/sva_until1.desc @@ -1,12 +1,11 @@ -KNOWNBUG +CORE sva_until1.sv --bound 1 -^\[main\.p0\] always (main.a until_with main.b): REFUTED$ -^\[main\.p1\] always (main.a until main.b): REFUTED$ -^\[main\.p2\] always (main.a s_until main.b): REFUTED$ +^\[main\.p0\] always \(main.a until_with main.b\): REFUTED$ +^\[main\.p1\] always \(main.a until main.b\): REFUTED$ +^\[main\.p2\] always \(main.a s_until main.b\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -These properties are not supported by the BMC engine. diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 5f720c16..184304d1 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -62,7 +62,7 @@ exprt normalize_pre_not(not_exprt expr) else if(op.id() == ID_sva_s_eventually) { // ¬ sva_s_eventually φ --> sva_always ¬φ - return sva_always_exprt{not_exprt{to_sva_eventually_expr(op).op()}}; + return sva_always_exprt{not_exprt{to_sva_s_eventually_expr(op).op()}}; } return std::move(expr); @@ -100,7 +100,7 @@ exprt normalize_pre_sva_non_overlapped_implication( exprt normalize_pre_sva_not(sva_not_exprt expr) { // Same as regular 'not'. These do not apply to sequences. - return not_exprt{expr.op()}; + return normalize_pre_not(not_exprt{expr.op()}); } exprt normalize_pre_sva_and(sva_and_exprt expr) diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 4b074b14..0614eb4c 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -40,44 +40,7 @@ Function: bmc_supports_LTL_property bool bmc_supports_LTL_property(const exprt &expr) { - // We support - // * formulas that contain no temporal operator besides X - // * Gφ, where φ contains no temporal operator besides X - // * Fφ, where φ contains no temporal operator besides X - // * GFφ, where φ contains no temporal operator besides X - // * conjunctions of supported LTL properties - auto non_X_LTL_operator = [](const exprt &expr) - { return is_LTL_operator(expr) && expr.id() != ID_X; }; - - if(!has_subexpr(expr, non_X_LTL_operator)) - { - return true; - } - else if(expr.id() == ID_F) - { - return !has_subexpr(to_F_expr(expr).op(), non_X_LTL_operator); - } - else if(expr.id() == ID_G) - { - auto &op = to_G_expr(expr).op(); - if(op.id() == ID_F) - { - return !has_subexpr(to_F_expr(op).op(), non_X_LTL_operator); - } - else - { - return !has_subexpr(op, non_X_LTL_operator); - } - } - else if(expr.id() == ID_and) - { - for(auto &op : expr.operands()) - if(!bmc_supports_LTL_property(op)) - return false; - return true; - } - else - return false; + return true; } /*******************************************************************\ @@ -414,12 +377,13 @@ static obligationst property_obligations_rec( } } else if( - property_expr.id() == ID_sva_until || property_expr.id() == ID_sva_s_until) + property_expr.id() == ID_sva_until || + property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U) { // non-overlapping until // we need a lasso to refute these - // we expand: p U q <=> q || (p && X(p U q)) + // we expand: p U q <=> q ∨ (p ∧ X(p U q)) exprt tmp_q = to_binary_expr(property_expr).op1(); tmp_q = property_obligations_rec(tmp_q, solver, current, no_timeframes, ns) .conjunction() @@ -437,11 +401,40 @@ static obligationst property_obligations_rec( { auto obligations_rec = property_obligations_rec( property_expr, solver, next, no_timeframes, ns); - expansion = and_exprt(expansion, obligations_rec.conjunction().second); + expansion = and_exprt{expansion, obligations_rec.conjunction().second}; } DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return obligationst{no_timeframes - 1, or_exprt(tmp_q, expansion)}; + return obligationst{no_timeframes - 1, or_exprt{tmp_q, expansion}}; + } + else if(property_expr.id() == ID_R) + { + // we expand: p R q <=> q ∧ (p ∨ X(p R q)) + auto &R_expr = to_R_expr(property_expr); + auto tmp_q = + property_obligations_rec(R_expr.rhs(), solver, current, no_timeframes, ns) + .conjunction() + .second; + + auto tmp_p = + property_obligations_rec(R_expr.lhs(), solver, current, no_timeframes, ns) + .conjunction() + .second; + + const auto next = current + 1; + exprt expansion; + + if(next < no_timeframes) + { + auto obligations_rec = property_obligations_rec( + property_expr, solver, next, no_timeframes, ns); + expansion = or_exprt{tmp_p, obligations_rec.conjunction().second}; + } + else + expansion = tmp_p; + + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{no_timeframes - 1, and_exprt{tmp_q, expansion}}; } else if( property_expr.id() == ID_sva_until_with || @@ -493,6 +486,17 @@ static obligationst property_obligations_rec( return obligationst{t, disjunction(disjuncts)}; } + else if( + property_expr.id() == ID_equal && + to_equal_expr(property_expr).lhs().type().id() == ID_bool) + { + // we rely on NNF: a<=>b ---> a=>b && b=>a + auto &equal_expr = to_equal_expr(property_expr); + auto tmp = and_exprt{ + implies_exprt{equal_expr.lhs(), equal_expr.rhs()}, + implies_exprt{equal_expr.rhs(), equal_expr.lhs()}}; + return property_obligations_rec(tmp, solver, current, no_timeframes, ns); + } else if(property_expr.id() == ID_implies) { // we rely on NNF @@ -528,8 +532,79 @@ static obligationst property_obligations_rec( } else if(property_expr.id() == ID_not) { - return obligationst{ - instantiate_property(property_expr, current, no_timeframes, ns)}; + // We need NNF, try to eliminate the negation. + auto &op = to_not_expr(property_expr).op(); + + if(op.id() == ID_U) + { + // ¬(φ U ψ) ≡ (¬φ R ¬ψ) + auto &U = to_U_expr(op); + auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}}; + return property_obligations_rec(R, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_R) + { + // ¬(φ R ψ) ≡ (¬φ U ¬ψ) + auto &R = to_R_expr(op); + auto U = U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}}; + return property_obligations_rec(U, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_G) + { + // ¬G φ ≡ F ¬φ + auto &G = to_G_expr(op); + auto F = F_exprt{not_exprt{G.op()}}; + return property_obligations_rec(F, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_F) + { + // ¬F φ ≡ G ¬φ + auto &F = to_F_expr(op); + auto G = G_exprt{not_exprt{F.op()}}; + return property_obligations_rec(G, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_X) + { + // ¬X φ ≡ X ¬φ + auto &X = to_X_expr(op); + auto negX = X_exprt{not_exprt{X.op()}}; + return property_obligations_rec(negX, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_implies) + { + // ¬(a->b) --> a && ¬b + auto &implies_expr = to_implies_expr(op); + auto and_expr = + and_exprt{implies_expr.lhs(), not_exprt{implies_expr.rhs()}}; + return property_obligations_rec( + and_expr, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_and) + { + auto operands = op.operands(); + for(auto &op : operands) + op = not_exprt{op}; + auto or_expr = or_exprt{std::move(operands)}; + return property_obligations_rec( + or_expr, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_or) + { + auto operands = op.operands(); + for(auto &op : operands) + op = not_exprt{op}; + auto and_expr = and_exprt{std::move(operands)}; + return property_obligations_rec( + and_expr, solver, current, no_timeframes, ns); + } + else if(op.id() == ID_not) + { + return property_obligations_rec( + to_not_expr(op).op(), solver, current, no_timeframes, ns); + } + else + return obligationst{ + instantiate_property(property_expr, current, no_timeframes, ns)}; } else {