LTL_sequence_matches now throws sva_sequence_match_unsupportedt

This allows reporting the sequence expression that is unsupported.

Author: kroening

src/temporal-logic/sva_sequence_match.cpp

@@ -64,9 +64,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
     auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
 
-    if(matches_lhs.empty() || matches_rhs.empty())
-      return {};
-
     std::vector<sva_sequence_matcht> result;
 
     // cross product
@@ -86,9 +83,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     auto &repetition = to_sva_sequence_repetition_star_expr(sequence);
     auto matches_op = LTL_sequence_matches(repetition.op());
 
-    if(matches_op.empty())
-      return {};
-
     std::vector<sva_sequence_matcht> result;
 
     if(repetition.repetitions_given())
@@ -97,7 +91,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
       {
         if(repetition.is_unbounded()) // [*n:$]
         {
-          return {}; // no support
+          throw sva_sequence_match_unsupportedt{sequence}; // no support
         }
         else // [*n:m]
         {
@@ -118,7 +112,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
       }
     }
     else         // [*]
-      return {}; // no support
+      throw sva_sequence_match_unsupportedt{sequence}; // no support
 
     return result;
   }
@@ -128,9 +122,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     auto matches = LTL_sequence_matches(delay.op());
     auto from_int = numeric_cast_v<mp_integer>(delay.from());
 
-    if(matches.empty())
-      return {};
-
     if(!delay.is_range())
     {
       // delay as instructed
@@ -143,7 +134,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     }
     else if(delay.is_unbounded())
     {
-      return {}; // can't encode
+      throw sva_sequence_match_unsupportedt{sequence}; // can't encode
     }
     else
     {
@@ -175,9 +166,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     auto matches_lhs = LTL_sequence_matches(and_expr.lhs());
     auto matches_rhs = LTL_sequence_matches(and_expr.rhs());
 
-    if(matches_lhs.empty() || matches_rhs.empty())
-      return {};
-
     std::vector<sva_sequence_matcht> result;
 
     for(auto &match_lhs : matches_lhs)
@@ -214,7 +202,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     {
       auto op_matches = LTL_sequence_matches(op);
       if(op_matches.empty())
-        return {}; // not supported
+        throw sva_sequence_match_unsupportedt{sequence}; // not supported
       for(auto &match : op_matches)
         result.push_back(std::move(match));
     }
@@ -223,6 +211,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
   }
   else
   {
-    return {}; // unsupported
+    throw sva_sequence_match_unsupportedt{sequence}; // not supported
   }
 }

src/temporal-logic/sva_sequence_match.h

@@ -26,6 +26,12 @@ struct sva_sequence_matcht
   {
   }
 
+  // a match with given sequence of conditions
+  explicit sva_sequence_matcht(std::vector<exprt> __cond_vector)
+    : cond_vector(std::move(__cond_vector))
+  {
+  }
+
   std::vector<exprt> cond_vector;
 
   std::size_t length()
@@ -40,9 +46,26 @@ struct sva_sequence_matcht
 
   // generate true ##1 ... ##1 true with length n
   static sva_sequence_matcht true_match(const mp_integer &n);
+
+  bool operator==(const sva_sequence_matcht &other) const
+  {
+    return cond_vector == other.cond_vector;
+  }
+};
+
+class sva_sequence_match_unsupportedt
+{
+public:
+  explicit sva_sequence_match_unsupportedt(exprt __expr)
+    : expr(std::move(__expr))
+  {
+  }
+
+  exprt expr;
 };
 
-// the set of potential matches for the given sequence expression
+/// The set of potential matches for the given sequence expression.
+/// Throws sva_sequence_match_unsupportedt when given sequence that cannot be translated.
 std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &);
 
 #endif // CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H

src/temporal-logic/sva_to_ltl.cpp

@@ -137,72 +137,82 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     expr.id() == ID_sva_non_overlapped_implication)
   {
     auto &implication = to_sva_implication_base_expr(expr);
-    auto matches = LTL_sequence_matches(implication.sequence());
 
-    if(matches.empty())
-      return {};
+    try
+    {
+      auto matches = LTL_sequence_matches(implication.sequence());
 
-    // All matches must be followed
-    // by the property being true
-    exprt::operandst conjuncts;
+      // All matches must be followed
+      // by the property being true
+      exprt::operandst conjuncts;
 
-    auto property_rec = SVA_to_LTL(implication.property());
+      auto property_rec = SVA_to_LTL(implication.property());
 
-    if(!property_rec.has_value())
-      return {};
+      if(!property_rec.has_value())
+        return {};
 
-    for(auto &match : matches)
-    {
-      const auto overlapped = expr.id() == ID_sva_overlapped_implication;
-      if(match.empty_match() && overlapped)
-      {
-        // ignore the empty match
-      }
-      else
+      for(auto &match : matches)
       {
-        auto delay = match.length() + (overlapped ? 0 : 1) - 1;
-        auto delayed_property = n_Xes(delay, property_rec.value());
-        conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
+        const auto overlapped = expr.id() == ID_sva_overlapped_implication;
+        if(match.empty_match() && overlapped)
+        {
+          // ignore the empty match
+        }
+        else
+        {
+          auto delay = match.length() + (overlapped ? 0 : 1) - 1;
+          auto delayed_property = n_Xes(delay, property_rec.value());
+          conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
+        }
       }
-    }
 
-    return conjunction(conjuncts);
+      return conjunction(conjuncts);
+    }
+    catch(sva_sequence_match_unsupportedt)
+    {
+      return {};
+    }
   }
   else if(
     expr.id() == ID_sva_nonoverlapped_followed_by ||
     expr.id() == ID_sva_overlapped_followed_by)
   {
     auto &followed_by = to_sva_followed_by_expr(expr);
-    auto matches = LTL_sequence_matches(followed_by.sequence());
 
-    if(matches.empty())
-      return {};
+    try
+    {
+      auto matches = LTL_sequence_matches(followed_by.sequence());
 
-    // There must be at least one match that is followed
-    // by the property being true
-    exprt::operandst disjuncts;
+      // There must be at least one match that is followed
+      // by the property being true
+      exprt::operandst disjuncts;
 
-    auto property_rec = SVA_to_LTL(followed_by.property());
+      auto property_rec = SVA_to_LTL(followed_by.property());
 
-    if(!property_rec.has_value())
-      return {};
+      if(!property_rec.has_value())
+        return {};
 
-    for(auto &match : matches)
-    {
-      const auto overlapped = expr.id() == ID_sva_overlapped_followed_by;
-      if(match.empty_match() && overlapped)
-      {
-        // ignore the empty match
-      }
-      else
+      for(auto &match : matches)
       {
-        auto delay = match.length() + (overlapped ? 0 : 1) - 1;
-        auto delayed_property = n_Xes(delay, property_rec.value());
-        disjuncts.push_back(and_exprt{ltl(match), delayed_property});
+        const auto overlapped = expr.id() == ID_sva_overlapped_followed_by;
+        if(match.empty_match() && overlapped)
+        {
+          // ignore the empty match
+        }
+        else
+        {
+          auto delay = match.length() + (overlapped ? 0 : 1) - 1;
+          auto delayed_property = n_Xes(delay, property_rec.value());
+          disjuncts.push_back(and_exprt{ltl(match), delayed_property});
+        }
       }
-    }
 
-    return disjunction(disjuncts);
+      return disjunction(disjuncts);
+    }
+    catch(sva_sequence_match_unsupportedt)
+    {
+      return {};
+    }
   }
   else if(expr.id() == ID_sva_sequence_property)
   {
@@ -215,21 +225,25 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
   {
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
 
-    // evaluates to true if there's at least one non-empty match of the sequence
-    auto matches = LTL_sequence_matches(sequence);
+    try
+    {
+      // evaluates to true if there's at least one non-empty match of the sequence
+      auto matches = LTL_sequence_matches(sequence);
 
-    if(matches.empty())
-      return {};
+      exprt::operandst disjuncts;
 
-    exprt::operandst disjuncts;
+      for(auto &match : matches)
+      {
+        if(!match.empty_match())
+          disjuncts.push_back(ltl(match));
+      }
 
-    for(auto &match : matches)
+      return disjunction(disjuncts);
+    }
+    catch(sva_sequence_match_unsupportedt)
     {
-      if(!match.empty_match())
-        disjuncts.push_back(ltl(match));
+      return {};
     }
-
-    return disjunction(disjuncts);
   }
   else if(expr.id() == ID_sva_s_until)
   {

unit/Makefile

@@ -6,6 +6,7 @@ SRC = unit_tests.cpp
 # Test source files
 SRC += smvlang/expr2smv.cpp \
        temporal-logic/ltl_sva_to_string.cpp \
+       temporal-logic/sva_sequence_match.cpp \
        temporal-logic/nnf.cpp \
        # Empty last line
 

unit/temporal-logic/sva_sequence_match.cpp

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module: SVA Sequence Matches
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/arith_tools.h>
+#include <util/mathematical_types.h>
+
+#include <temporal-logic/sva_sequence_match.h>
+#include <testing-utils/use_catch.h>
+#include <verilog/sva_expr.h>
+
+SCENARIO("Generating the matches for an SVA sequence")
+{
+  const auto sequence_type = verilog_sva_sequence_typet{};
+
+  GIVEN("A boolean formula")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+
+    REQUIRE(
+      LTL_sequence_matches(sva_boolean_exprt{p, sequence_type}) ==
+      std::vector<sva_sequence_matcht>{sva_sequence_matcht{p}});
+  }
+
+  GIVEN("##1 p")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+    auto one = from_integer(1, integer_typet{});
+
+    REQUIRE(
+      LTL_sequence_matches(
+        sva_cycle_delay_exprt{one, sva_boolean_exprt{p, sequence_type}}) ==
+      std::vector<sva_sequence_matcht>{sva_sequence_matcht{{true_exprt{}, p}}});
+  }
+
+  GIVEN("##[*] p")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+
+    CHECK_THROWS_AS(
+      LTL_sequence_matches(
+        sva_cycle_delay_star_exprt{sva_boolean_exprt{p, sequence_type}}),
+      sva_sequence_match_unsupportedt);
+  }
+}