Merge pull request #1026 from diffblue/sva-constant-bounds

SVA: typing for constant bounds of ranged/indexed operators

Author: tautschnig

src/temporal-logic/normalize_property.cpp

@@ -38,9 +38,7 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 {
   if(expr.is_unbounded())
   {
-    if(
-      expr.from().is_constant() &&
-      numeric_cast_v<mp_integer>(to_constant_expr(expr.from())) == 0)
+    if(numeric_cast_v<mp_integer>(expr.from()) == 0)
     {
       // ##[0:$] φ --> s_eventually φ
       return sva_s_eventually_exprt{expr.op()};

src/trans-word-level/sequence.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "sequence.h"
 
+#include <util/arith_tools.h>
 #include <util/ebmc_util.h>
 
 #include <verilog/sva_expr.h>
@@ -23,14 +24,11 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
   {
     auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);
+    const auto from = numeric_cast_v<mp_integer>(sva_cycle_delay_expr.from());
 
     if(sva_cycle_delay_expr.to().is_nil()) // ##1 something
     {
-      mp_integer offset;
-      if(to_integer_non_constant(sva_cycle_delay_expr.from(), offset))
-        throw "failed to convert sva_cycle_delay offset";
-
-      const auto u = t + offset;
+      const auto u = t + from;
 
       // Do we exceed the bound? Make it 'true'
       if(u >= no_timeframes)
@@ -44,9 +42,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
     }
     else
     {
-      mp_integer from, to;
-      if(to_integer_non_constant(sva_cycle_delay_expr.from(), from))
-        throw "failed to convert sva_cycle_delay offsets";
+      mp_integer to;
 
       if(sva_cycle_delay_expr.to().id() == ID_infinity)
       {

src/verilog/sva_expr.h

@@ -137,22 +137,22 @@ static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr)
 class sva_indexed_nexttime_exprt : public binary_predicate_exprt
 {
 public:
-  sva_indexed_nexttime_exprt(exprt index, exprt op)
+  sva_indexed_nexttime_exprt(constant_exprt index, exprt op)
     : binary_predicate_exprt(
         std::move(index),
         ID_sva_indexed_nexttime,
         std::move(op))
   {
   }
 
-  const exprt &index() const
+  const constant_exprt &index() const
   {
-    return op0();
+    return static_cast<const constant_exprt &>(op0());
   }
 
-  exprt &index()
+  constant_exprt &index()
   {
-    return op0();
+    return static_cast<constant_exprt &>(op0());
   }
 
   const exprt &op() const
@@ -190,22 +190,22 @@ to_sva_indexed_nexttime_expr(exprt &expr)
 class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt
 {
 public:
-  sva_indexed_s_nexttime_exprt(exprt index, exprt op)
+  sva_indexed_s_nexttime_exprt(constant_exprt index, exprt op)
     : binary_predicate_exprt(
         std::move(index),
         ID_sva_indexed_s_nexttime,
         std::move(op))
   {
   }
 
-  const exprt &index() const
+  const constant_exprt &index() const
   {
-    return op0();
+    return static_cast<const constant_exprt &>(op0());
   }
 
-  exprt &index()
+  constant_exprt &index()
   {
-    return op0();
+    return static_cast<constant_exprt &>(op0());
   }
 
   const exprt &op() const
@@ -239,31 +239,34 @@ to_sva_indexed_s_nexttime_expr(exprt &expr)
   return static_cast<sva_indexed_s_nexttime_exprt &>(expr);
 }
 
+/// For ranged SVA operators. The lower bound must be a constant
+/// post elaboration. The upper end need not be bounded,
+/// i.e., given as $
 class sva_ranged_predicate_exprt : public ternary_exprt
 {
 public:
   sva_ranged_predicate_exprt(
     irep_idt __id,
-    exprt __lower,
+    constant_exprt __lower,
     exprt __upper,
     exprt __op)
     : ternary_exprt(
         __id,
         std::move(__lower),
         std::move(__upper),
         std::move(__op),
-        bool_typet())
+        bool_typet{})
   {
   }
 
-  const exprt &lower() const
+  const constant_exprt &lower() const
   {
-    return op0();
+    return static_cast<const constant_exprt &>(op0());
   }
 
-  exprt &lower()
+  constant_exprt &lower()
   {
-    return op0();
+    return static_cast<constant_exprt &>(op0());
   }
 
   const exprt &upper() const
@@ -292,11 +295,44 @@ class sva_ranged_predicate_exprt : public ternary_exprt
   using ternary_exprt::op2;
 };
 
-class sva_eventually_exprt : public sva_ranged_predicate_exprt
+/// A specialisation of sva_ranged_predicate_exprt where both bounds
+/// are constants.
+class sva_bounded_range_predicate_exprt : public sva_ranged_predicate_exprt
 {
 public:
-  sva_eventually_exprt(exprt __lower, exprt __upper, exprt __op)
+  sva_bounded_range_predicate_exprt(
+    irep_idt __id,
+    constant_exprt __lower,
+    constant_exprt __upper,
+    exprt __op)
     : sva_ranged_predicate_exprt(
+        __id,
+        std::move(__lower),
+        std::move(__upper),
+        std::move(__op))
+  {
+  }
+
+  const constant_exprt &upper() const
+  {
+    return static_cast<const constant_exprt &>(
+      sva_ranged_predicate_exprt::upper());
+  }
+
+  constant_exprt &upper()
+  {
+    return static_cast<constant_exprt &>(sva_ranged_predicate_exprt::upper());
+  }
+};
+
+class sva_eventually_exprt : public sva_bounded_range_predicate_exprt
+{
+public:
+  sva_eventually_exprt(
+    constant_exprt __lower,
+    constant_exprt __upper,
+    exprt __op)
+    : sva_bounded_range_predicate_exprt(
         ID_sva_eventually,
         std::move(__lower),
         std::move(__upper),
@@ -347,7 +383,10 @@ static inline sva_s_eventually_exprt &to_sva_s_eventually_expr(exprt &expr)
 class sva_ranged_s_eventually_exprt : public sva_ranged_predicate_exprt
 {
 public:
-  explicit sva_ranged_s_eventually_exprt(exprt lower, exprt upper, exprt op)
+  explicit sva_ranged_s_eventually_exprt(
+    constant_exprt lower,
+    exprt upper,
+    exprt op)
     : sva_ranged_predicate_exprt(
         ID_sva_ranged_s_eventually,
         std::move(lower),
@@ -399,7 +438,7 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
 class sva_ranged_always_exprt : public sva_ranged_predicate_exprt
 {
 public:
-  sva_ranged_always_exprt(exprt lower, exprt upper, exprt op)
+  sva_ranged_always_exprt(constant_exprt lower, exprt upper, exprt op)
     : sva_ranged_predicate_exprt(
         ID_sva_ranged_always,
         std::move(lower),
@@ -424,11 +463,11 @@ static inline sva_ranged_always_exprt &to_sva_ranged_always_expr(exprt &expr)
   return static_cast<sva_ranged_always_exprt &>(expr);
 }
 
-class sva_s_always_exprt : public sva_ranged_predicate_exprt
+class sva_s_always_exprt : public sva_bounded_range_predicate_exprt
 {
 public:
-  sva_s_always_exprt(exprt lower, exprt upper, exprt op)
-    : sva_ranged_predicate_exprt(
+  sva_s_always_exprt(constant_exprt lower, constant_exprt upper, exprt op)
+    : sva_bounded_range_predicate_exprt(
         ID_sva_s_always,
         std::move(lower),
         std::move(upper),
@@ -841,7 +880,8 @@ static inline sva_followed_by_exprt &to_sva_followed_by_expr(exprt &expr)
 class sva_cycle_delay_exprt : public ternary_exprt
 {
 public:
-  sva_cycle_delay_exprt(exprt from, exprt to, exprt op)
+  /// The upper bound may be $
+  sva_cycle_delay_exprt(constant_exprt from, exprt to, exprt op)
     : ternary_exprt(
         ID_sva_cycle_delay,
         std::move(from),
@@ -851,7 +891,7 @@ class sva_cycle_delay_exprt : public ternary_exprt
   {
   }
 
-  sva_cycle_delay_exprt(exprt cycles, exprt op)
+  sva_cycle_delay_exprt(constant_exprt cycles, exprt op)
     : ternary_exprt(
         ID_sva_cycle_delay,
         std::move(cycles),
@@ -861,14 +901,14 @@ class sva_cycle_delay_exprt : public ternary_exprt
   {
   }
 
-  const exprt &from() const
+  const constant_exprt &from() const
   {
-    return op0();
+    return static_cast<const constant_exprt &>(op0());
   }
 
-  exprt &from()
+  constant_exprt &from()
   {
-    return op0();
+    return static_cast<constant_exprt &>(op0());
   }
 
   // may be nil (just the singleton 'from') or