Merge pull request #1173 from diffblue/ltl_sva_to_string-throws

`ltl_sva_to_stringt::operator(expr)` now throws error class

Author: tautschnig

regression/ebmc-spot/sva-buechi/sequence_first_match1.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_first_match1.sv
+--buechi --bound 5
+^error: failed to convert sva_sequence_first_match$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^\[.*\] first_match\(main\.x == 0\): PROVED up to bound 5$
+^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED up to bound 5$
+--

regression/ebmc-spot/sva-buechi/sequence_first_match2.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_first_match2.sv
+--buechi --bound 5
+^error: failed to convert sva_sequence_first_match$
+^EXIT=6$
+^SIGNAL=0$
+--
+^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: REFUTED$
+^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
+^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: REFUTED$
+^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_throughout1.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_throughout1.sv
+--buechi --bound 10
+^error: failed to convert sva_sequence_throughout$
+^EXIT=6$
+^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

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/sequence_within1.sv
+--buechi --bound 20
+^error: failed to convert sva_sequence_within$
+^EXIT=6$
+^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/unbounded1.desc

@@ -0,0 +1,7 @@
+CORE
+../../verilog/SVA/unbounded1.sv
+--buechi --module main --bound 1
+^error: failed to convert sva_cycle_delay$
+^EXIT=6$
+^SIGNAL=0$
+--

src/temporal-logic/ltl_sva_to_string.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/arith_tools.h>
 #include <util/string2int.h>
 
-#include <ebmc/ebmc_error.h>
 #include <verilog/sva_expr.h>
 
 #include "ltl.h"
@@ -378,8 +377,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
         if(from == 0)
         {
           // requires treatment of empty sequences on lhs
-          throw ebmc_errort{}
-            << "cannot convert 0.. ranged sequence concatenation to Buechi";
+          throw ltl_sva_to_string_unsupportedt{expr};
         }
         else if(delay.is_unbounded()) // f ##[n:$] g
         {
@@ -448,7 +446,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_empty_match())
     {
-      throw ebmc_errort{} << "cannot convert [*0] to Buechi";
+      throw ltl_sva_to_string_unsupportedt{expr};
     }
     else if(repetition.is_singleton())
     {
@@ -547,5 +545,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     return resultt{precedencet::ATOM, s};
   }
   else
-    throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi";
+  {
+    throw ltl_sva_to_string_unsupportedt{expr};
+  }
 }

src/temporal-logic/ltl_sva_to_string.h

@@ -12,10 +12,22 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/numbering.h>
 #include <util/std_expr.h>
 
+class ltl_sva_to_string_unsupportedt
+{
+public:
+  explicit ltl_sva_to_string_unsupportedt(exprt __expr)
+    : expr(std::move(__expr))
+  {
+  }
+
+  exprt expr;
+};
+
 /// create formula strings for external LTL to Buechi tools
 class ltl_sva_to_stringt
 {
 public:
+  // throws ltl_sva_to_string_unsupportedt when the conversion fails
   std::string operator()(const exprt &expr)
   {
     return rec(expr, PROPERTY).s;

src/temporal-logic/ltl_to_buechi.cpp

@@ -84,98 +84,109 @@ exprt hoa_label_to_expr(
 buechi_transt
 ltl_to_buechi(const exprt &property, message_handlert &message_handler)
 {
-  // Turn the skeleton of the property into a string
   ltl_sva_to_stringt ltl_sva_to_string;
-  auto string = ltl_sva_to_string(property);
 
-  // Run Spot's ltl2tgba
-  std::ostringstream hoa_stream;
+  try
+  {
+    // Turn the skeleton of the property into a string
+    auto string = ltl_sva_to_string(property);
 
-  messaget message(message_handler);
+    // Run Spot's ltl2tgba
+    std::ostringstream hoa_stream;
 
-  message.debug() << "ltl2tgba property: " << string << messaget::eom;
+    messaget message(message_handler);
 
-  // State-based Buchi acceptance. Should compare with transition-based
-  // acceptance.
-  // Use --complete to be able to have multiple properties in one
-  // model.
-  auto run_result = run(
-    "ltl2tgba",
-    {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string},
-    "",
-    hoa_stream,
-    "");
+    message.debug() << "ltl2tgba property: " << string << messaget::eom;
 
-  if(run_result != 0)
-    throw ebmc_errort{} << "failed to run ltl2tgba";
+    // State-based Buchi acceptance. Should compare with transition-based
+    // acceptance.
+    // Use --complete to be able to have multiple properties in one
+    // model.
+    auto run_result = run(
+      "ltl2tgba",
+      {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string},
+      "",
+      hoa_stream,
+      "");
 
-  auto hoa = hoat::from_string(hoa_stream.str());
+    if(run_result != 0)
+      throw ebmc_errort{} << "failed to run ltl2tgba";
 
-  message.debug() << hoa << messaget::eom;
+    auto hoa = hoat::from_string(hoa_stream.str());
 
-  auto max_state_number = hoa.max_state_number();
-  auto state_type = range_typet{0, max_state_number};
-  const auto buechi_state = symbol_exprt{"buechi::state", state_type};
-  const auto buechi_next_state = next_symbol_exprt{"buechi::state", state_type};
+    message.debug() << hoa << messaget::eom;
 
-  // construct the initial state constraint
-  std::vector<exprt> init_disjuncts;
+    auto max_state_number = hoa.max_state_number();
+    auto state_type = range_typet{0, max_state_number};
+    const auto buechi_state = symbol_exprt{"buechi::state", state_type};
+    const auto buechi_next_state =
+      next_symbol_exprt{"buechi::state", state_type};
 
-  for(auto &item : hoa.header)
-    if(item.first == "Start:")
-    {
-      if(item.second.size() != 1)
-        throw ebmc_errort() << "Start header must have one token";
-      auto state_number = string2integer(item.second.front());
-      init_disjuncts.push_back(
-        equal_exprt{buechi_state, from_integer(state_number, state_type)});
-    }
+    // construct the initial state constraint
+    std::vector<exprt> init_disjuncts;
 
-  auto init = disjunction(init_disjuncts);
+    for(auto &item : hoa.header)
+      if(item.first == "Start:")
+      {
+        if(item.second.size() != 1)
+          throw ebmc_errort() << "Start header must have one token";
+        auto state_number = string2integer(item.second.front());
+        init_disjuncts.push_back(
+          equal_exprt{buechi_state, from_integer(state_number, state_type)});
+      }
 
-  message.debug() << "Buechi initial state: " << format(init) << messaget::eom;
+    auto init = disjunction(init_disjuncts);
 
-  // construct the liveness signal
-  std::vector<exprt> liveness_disjuncts;
+    message.debug() << "Buechi initial state: " << format(init)
+                    << messaget::eom;
 
-  for(auto &state : hoa.body)
-    if(!state.first.acc_sig.empty())
-    {
-      liveness_disjuncts.push_back(equal_exprt{
-        buechi_state, from_integer(state.first.number, state_type)});
-    }
+    // construct the liveness signal
+    std::vector<exprt> liveness_disjuncts;
 
-  auto liveness_signal = disjunction(liveness_disjuncts);
+    for(auto &state : hoa.body)
+      if(!state.first.acc_sig.empty())
+      {
+        liveness_disjuncts.push_back(equal_exprt{
+          buechi_state, from_integer(state.first.number, state_type)});
+      }
 
-  message.debug() << "Buechi liveness signal: " << format(liveness_signal)
-                  << messaget::eom;
+    auto liveness_signal = disjunction(liveness_disjuncts);
 
-  // construct the transition relation
-  std::vector<exprt> trans_disjuncts;
+    message.debug() << "Buechi liveness signal: " << format(liveness_signal)
+                    << messaget::eom;
 
-  for(auto &state : hoa.body)
-  {
-    auto pre =
-      equal_exprt{buechi_state, from_integer(state.first.number, state_type)};
-    for(auto &edge : state.second)
+    // construct the transition relation
+    std::vector<exprt> trans_disjuncts;
+
+    for(auto &state : hoa.body)
     {
-      if(edge.dest_states.size() != 1)
-        throw ebmc_errort() << "edge must have one destination state";
-      auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string);
-      auto post = equal_exprt{
-        buechi_next_state, from_integer(edge.dest_states.front(), state_type)};
-      trans_disjuncts.push_back(and_exprt{pre, cond, post});
+      auto pre =
+        equal_exprt{buechi_state, from_integer(state.first.number, state_type)};
+      for(auto &edge : state.second)
+      {
+        if(edge.dest_states.size() != 1)
+          throw ebmc_errort() << "edge must have one destination state";
+        auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string);
+        auto post = equal_exprt{
+          buechi_next_state,
+          from_integer(edge.dest_states.front(), state_type)};
+        trans_disjuncts.push_back(and_exprt{pre, cond, post});
+      }
     }
-  }
 
-  auto trans = disjunction(trans_disjuncts);
+    auto trans = disjunction(trans_disjuncts);
 
-  message.debug() << "Buechi transition constraint: " << format(trans)
-                  << messaget::eom;
+    message.debug() << "Buechi transition constraint: " << format(trans)
+                    << messaget::eom;
 
-  return {
-    buechi_state,
-    std::move(init),
-    std::move(trans),
-    std::move(liveness_signal)};
+    return {
+      buechi_state,
+      std::move(init),
+      std::move(trans),
+      std::move(liveness_signal)};
+  }
+  catch(ltl_sva_to_string_unsupportedt error)
+  {
+    throw ebmc_errort{} << "failed to convert " << error.expr.id();
+  }
 }