From 6c05d42fe1830c7689bc3bf8989caf8a5d63ed4f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Oct 2025 19:05:27 -0700 Subject: [PATCH] better error reporting when Buechi conversion is given unsupported property This improves the error reporting when the Buechi conversion is given an unsupported property. --- .../sva-buechi/cover_sequence1.bmc.desc | 4 +- .../sva-buechi/cover_sequence2.bmc.desc | 8 +- .../ebmc-spot/sva-buechi/sequence2.bmc.desc | 2 +- .../sva-buechi/sequence_repetition1.bmc.desc | 8 +- .../sva-buechi/sequence_throughout1.desc | 9 +- .../sva-buechi/sequence_within1.desc | 13 +- regression/ebmc-spot/sva-buechi/strong1.desc | 2 +- .../ebmc-spot/sva-buechi/unbounded1.desc | 4 +- src/ebmc/instrument_buechi.cpp | 125 +++++++++--------- src/temporal-logic/ltl_sva_to_string.cpp | 14 +- src/temporal-logic/ltl_to_buechi.cpp | 3 +- src/temporal-logic/ltl_to_buechi.h | 10 ++ src/temporal-logic/temporal_logic.cpp | 19 --- src/temporal-logic/temporal_logic.h | 4 - 14 files changed, 113 insertions(+), 112 deletions(-) diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc index 09ded4191..128b3c8a0 100644 --- a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/cover_sequence1.sv --buechi --bound 10 --numbered-trace -^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: not convertible to Buechi$ -^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc index 0dda3d634..cfdbfd026 100644 --- a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc @@ -1,10 +1,10 @@ CORE ../../verilog/SVA/cover_sequence2.sv --buechi --bound 5 -^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$ -^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$ -^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$ -^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc index 974f6c1ef..72b846c4d 100644 --- a/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc @@ -2,7 +2,7 @@ CORE ../../verilog/SVA/sequence2.sv --buechi --bound 10 ^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$ -^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_strong not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc index 5b64f65ef..e9afa1219 100644 --- a/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc @@ -2,11 +2,11 @@ CORE ../../verilog/SVA/sequence_repetition1.sv --buechi --bound 10 ^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$ -^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$ -^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$ +^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: sva_sequence_goto_repetition not convertible to Buechi$ +^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: sva_sequence_non_consecutive_repetition not convertible to Buechi$ ^\[.*\] main\.x == 0 \[\*2\]: REFUTED$ -^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$ -^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$ +^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: sva_sequence_goto_repetition not convertible to Buechi$ +^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: sva_sequence_non_consecutive_repetition not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc b/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc index a40e404fe..11eed1555 100644 --- a/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc +++ b/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc @@ -1,12 +1,11 @@ CORE ../../verilog/SVA/sequence_throughout1.sv --buechi --bound 10 -^error: failed to convert sva_sequence_throughout$ -^EXIT=6$ +^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$ +^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$ +^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$ +^EXIT=10$ ^SIGNAL=0$ -- -^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): PROVED up to bound 10$ -^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): REFUTED$ -^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): REFUTED$ ^warning: ignoring -- diff --git a/regression/ebmc-spot/sva-buechi/sequence_within1.desc b/regression/ebmc-spot/sva-buechi/sequence_within1.desc index 7e842c87a..7b0a3af54 100644 --- a/regression/ebmc-spot/sva-buechi/sequence_within1.desc +++ b/regression/ebmc-spot/sva-buechi/sequence_within1.desc @@ -1,14 +1,13 @@ CORE ../../verilog/SVA/sequence_within1.sv --buechi --bound 20 -^error: failed to convert sva_sequence_within$ -^EXIT=6$ +^\[main\.p0\] main\.x == 0 within main\.x == 1: UNSUPPORTED: sva_sequence_within not convertible to Buechi$ +^\[main\.p1\] main\.x == 0 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$ +^\[main\.p2\] main\.x == 5 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$ +^\[main\.p3\] main\.x == 10 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$ +^\[main\.p4\] main\.x == 11 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$ +^EXIT=10$ ^SIGNAL=0$ -- -^\[main\.p0\] main\.x == 0 within main\.x == 1: REFUTED$ -^\[main\.p1\] main\.x == 0 within \(##10 1\): PROVED up to bound 20$ -^\[main\.p2\] main\.x == 5 within \(##10 1\): PROVED up to bound 20$ -^\[main\.p3\] main\.x == 10 within \(##10 1\): PROVED up to bound 20$ -^\[main\.p4\] main\.x == 11 within \(##10 1\): REFUTED$ ^warning: ignoring -- diff --git a/regression/ebmc-spot/sva-buechi/strong1.desc b/regression/ebmc-spot/sva-buechi/strong1.desc index aee695e79..c65dd91b6 100644 --- a/regression/ebmc-spot/sva-buechi/strong1.desc +++ b/regression/ebmc-spot/sva-buechi/strong1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/strong1.sv --buechi --bound 4 -^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/unbounded1.desc b/regression/ebmc-spot/sva-buechi/unbounded1.desc index 0b0841f64..6fde0df12 100644 --- a/regression/ebmc-spot/sva-buechi/unbounded1.desc +++ b/regression/ebmc-spot/sva-buechi/unbounded1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/unbounded1.sv --buechi --module main --bound 1 -^error: failed to convert sva_cycle_delay$ -^EXIT=6$ +^\[.*\] always \(main\.a ##\[0:main\.upper\] main\.b\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$ +^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp index b17db5b10..7604429d2 100644 --- a/src/ebmc/instrument_buechi.cpp +++ b/src/ebmc/instrument_buechi.cpp @@ -25,9 +25,7 @@ void instrument_buechi( continue; // This is for LTL and some fragment of SVA only. - if( - !is_LTL(property.normalized_expr) && - !is_Buechi_SVA(property.normalized_expr)) + if(!is_LTL(property.normalized_expr) && !is_SVA(property.normalized_expr)) { property.unsupported("not convertible to Buechi"); continue; @@ -37,65 +35,74 @@ void instrument_buechi( message.debug() << "Translating " << property.description << " to Buechi" << messaget::eom; - // make the automaton for the negation of the property - auto buechi = - ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler); - - // make a fresh symbol for the state of the automaton - namespacet ns(transition_system.symbol_table); - auto property_symbol = ns.lookup(property.identifier); - - auxiliary_symbolt new_state_symbol{ - id2string(property_symbol.name) + "::buechi_state", - buechi.state_symbol.type(), - property_symbol.mode}; - new_state_symbol.is_state_var = true; - new_state_symbol.module = property_symbol.module; - - buechi.rename_state_symbol(new_state_symbol.symbol_expr()); - - // add the new symbol to the symbol table - transition_system.symbol_table.add(std::move(new_state_symbol)); - - // add the automaton to the transition system - transition_system.trans_expr.init() = - and_exprt{transition_system.trans_expr.init(), buechi.init}; - - transition_system.trans_expr.trans() = - and_exprt{transition_system.trans_expr.trans(), buechi.trans}; - - // Replace the normalized property expression - // by the Buechi acceptance condition. - exprt::operandst property_conjuncts; - - bool have_liveness = false, have_safety = false; - - if(!buechi.liveness_signal.is_false()) + try { - // 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}}}); - have_liveness = true; + // make the automaton for the negation of the property + auto buechi = + ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler); + + // make a fresh symbol for the state of the automaton + namespacet ns(transition_system.symbol_table); + auto property_symbol = ns.lookup(property.identifier); + + auxiliary_symbolt new_state_symbol{ + id2string(property_symbol.name) + "::buechi_state", + buechi.state_symbol.type(), + property_symbol.mode}; + new_state_symbol.is_state_var = true; + new_state_symbol.module = property_symbol.module; + + buechi.rename_state_symbol(new_state_symbol.symbol_expr()); + + // add the new symbol to the symbol table + transition_system.symbol_table.add(std::move(new_state_symbol)); + + // add the automaton to the transition system + transition_system.trans_expr.init() = + and_exprt{transition_system.trans_expr.init(), buechi.init}; + + transition_system.trans_expr.trans() = + and_exprt{transition_system.trans_expr.trans(), buechi.trans}; + + // Replace the normalized property expression + // by the Buechi acceptance condition. + exprt::operandst property_conjuncts; + + bool have_liveness = false, have_safety = false; + + 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}}}); + have_liveness = true; + } + + if(!buechi.error_signal.is_true()) + { + property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}}); + have_safety = true; + } + + if(have_liveness && have_safety) + message.debug() << "Buechi automaton has liveness and safety components" + << messaget::eom; + else if(have_liveness) + message.debug() << "Buechi automaton is liveness only" << messaget::eom; + else if(have_safety) + message.debug() << "Buechi automaton is safety only" << messaget::eom; + + property.normalized_expr = conjunction(property_conjuncts); + + message.debug() << "New property: " << format(property.normalized_expr) + << messaget::eom; } - - if(!buechi.error_signal.is_true()) + catch(ltl_to_buechi_unsupportedt error) { - property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}}); - have_safety = true; + property.unsupported( + error.expr.id_string() + " not convertible to Buechi"); + continue; } - - if(have_liveness && have_safety) - message.debug() << "Buechi automaton has liveness and safety components" - << messaget::eom; - else if(have_liveness) - message.debug() << "Buechi automaton is liveness only" << messaget::eom; - else if(have_safety) - message.debug() << "Buechi automaton is safety only" << messaget::eom; - - property.normalized_expr = conjunction(property_conjuncts); - - message.debug() << "New property: " << format(property.normalized_expr) - << messaget::eom; } } diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index d5d288703..44dd1569c 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -297,9 +297,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) auto new_expr = R_exprt{until_with.rhs(), until_with.lhs()}; // swapped return infix(" R ", new_expr, mode); } - else if( - expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || - expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) + else if(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak) { PRECONDITION(mode == PROPERTY); auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); @@ -308,6 +306,10 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) // weak closure return resultt{precedencet::ATOM, '{' + op_rec.s + '}'}; } + else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong) + { + throw ltl_sva_to_string_unsupportedt{expr}; + } else if(expr.id() == ID_sva_or) { // can be sequence or property @@ -514,6 +516,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n] { + // ltl2tgba produces the wrong anser for [->n] and [=n] + throw ltl_sva_to_string_unsupportedt{expr}; + PRECONDITION(mode == SVA_SEQUENCE); auto &repetition = to_sva_sequence_goto_repetition_expr(expr); unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()}; @@ -542,6 +547,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) else if( expr.id() == ID_sva_sequence_non_consecutive_repetition) // something[=n] { + // ltl2tgba produces the wrong anser for [->n] and [=n] + throw ltl_sva_to_string_unsupportedt{expr}; + PRECONDITION(mode == SVA_SEQUENCE); auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr); unary_exprt new_expr{ diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp index 2e119b99b..0b8c59227 100644 --- a/src/temporal-logic/ltl_to_buechi.cpp +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -264,6 +264,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) } catch(ltl_sva_to_string_unsupportedt error) { - throw ebmc_errort{} << "failed to convert " << error.expr.id(); + // re-throw + throw ltl_to_buechi_unsupportedt{error.expr}; } } diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h index d842302ac..28efe4991 100644 --- a/src/temporal-logic/ltl_to_buechi.h +++ b/src/temporal-logic/ltl_to_buechi.h @@ -37,6 +37,16 @@ struct buechi_transt void rename_state_symbol(const symbol_exprt &new_state_symbol); }; +class ltl_to_buechi_unsupportedt +{ +public: + explicit ltl_to_buechi_unsupportedt(exprt __expr) : expr(std::move(__expr)) + { + } + + exprt expr; +}; + class message_handlert; buechi_transt ltl_to_buechi(const exprt &formula, message_handlert &); diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index bdb3ddf1d..cb01a8216 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -214,22 +214,3 @@ std::optional LTL_to_CTL(exprt expr) else return {}; } - -bool is_Buechi_SVA(const exprt &expr) -{ - auto unsupported_operator = [](const exprt &expr) - { - // ltl2tgba produces the wrong anser for [->n] and [=n] - if( - expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_strong || - expr.id() == ID_sva_sequence_goto_repetition || - expr.id() == ID_sva_sequence_non_consecutive_repetition) - { - return true; - } - else - return is_temporal_operator(expr) && !is_SVA_operator(expr); - }; - - return !has_subexpr(expr, unsupported_operator); -} diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index 0192122a1..e799a3624 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -81,8 +81,4 @@ bool is_SVA_always_s_eventually_p(const exprt &); /// returns {} if not possible std::optional LTL_to_CTL(exprt); -/// Returns true iff the given expression is an SVA expression that -/// we can convert into a Buechi automaton -bool is_Buechi_SVA(const exprt &); - #endif