better error reporting for Buechi conversion

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$
 --

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$
 --

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$
 --

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$
 --

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
 --

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
 --

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$
 --

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$
 --

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;
   }
 }

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{

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};
   }
 }

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 &);

src/temporal-logic/temporal_logic.cpp

@@ -214,22 +214,3 @@ std::optional<exprt> 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);
-}

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<exprt> 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