SMV: properties must not contain next(...)

regression/smv/CTL/smv_ctlspec2.desc

@@ -0,0 +1,7 @@
+CORE
+smv_ctlspec2.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/CTL/smv_ctlspec2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- error, next(...) is not allowed
+SPEC AG next(x)

regression/smv/CTL/smv_ctlspec3.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+smv_ctlspec3.smv
+
+^file .* line 5: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/CTL/smv_ctlspec3.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : boolean;
+
+DEFINE y := next(x);
+
+-- error, next(...) is not allowed
+SPEC AG y

regression/smv/LTL/smv_ltlspec7.desc

@@ -0,0 +1,7 @@
+CORE
+smv_ltlspec7.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/LTL/smv_ltlspec7.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- error, next(...) is not allowed
+LTLSPEC G next(x)

src/smvlang/smv_typecheck.cpp

@@ -642,6 +642,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   if(expr.id()==ID_symbol || 
      expr.id()==ID_next_symbol)
   {
+    // next_symbol is only allowed in TRANS mode
+    if(expr.id() == ID_next_symbol && mode != TRANS && mode != OTHER)
+      throw errort().with_location(expr.find_source_location())
+        << "next(...) is not allowed here";
+
     const irep_idt &identifier=expr.get(ID_identifier);
     bool next=expr.id()==ID_next_symbol;
 

src/trans-word-level/instantiate_word_level.cpp

@@ -72,23 +72,22 @@ symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  explicit wl_instantiatet(const mp_integer &_no_timeframes)
-    : no_timeframes(_no_timeframes)
+  wl_instantiatet(const mp_integer &_no_timeframes, bool _next_symbol_allowed)
+    : no_timeframes(_no_timeframes), next_symbol_allowed(_next_symbol_allowed)
   {
   }
 
   /// Instantiate the given expression for timeframe t
-  [[nodiscard]] std::pair<mp_integer, exprt>
-  operator()(exprt expr, const mp_integer &t) const
+  [[nodiscard]] exprt operator()(exprt expr, const mp_integer &t) const
   {
     return instantiate_rec(std::move(expr), t);
   }
 
 protected:
   const mp_integer &no_timeframes;
+  bool next_symbol_allowed;
 
-  [[nodiscard]] std::pair<mp_integer, exprt>
-  instantiate_rec(exprt, const mp_integer &t) const;
+  [[nodiscard]] exprt instantiate_rec(exprt, const mp_integer &t) const;
   [[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
 };
 
@@ -104,20 +103,20 @@ Function: wl_instantiatet::instantiate_rec
 
 \*******************************************************************/
 
-std::pair<mp_integer, exprt>
-wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
+exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 {
   expr.type() = instantiate_rec(expr.type(), t);
 
   if(expr.id() == ID_next_symbol)
   {
+    PRECONDITION(next_symbol_allowed);
     expr.id(ID_symbol);
     auto u = t + 1;
-    return {u, timeframe_symbol(u, to_symbol_expr(std::move(expr)))};
+    return timeframe_symbol(u, to_symbol_expr(std::move(expr)));
   }
   else if(expr.id() == ID_symbol)
   {
-    return {t, timeframe_symbol(t, to_symbol_expr(std::move(expr)))};
+    return timeframe_symbol(t, to_symbol_expr(std::move(expr)));
   }
   else if(
     expr.id() == ID_typecast && expr.type().id() == ID_bool &&
@@ -144,7 +143,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
     if(ticks > t)
     {
       // return the 'default value' for the type
-      return {t, verilog_past.default_value()};
+      return verilog_past.default_value();
     }
     else
     {
@@ -159,15 +158,12 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   }
   else
   {
-    mp_integer max = t;
     for(auto &op : expr.operands())
     {
-      auto tmp = instantiate_rec(op, t);
-      op = tmp.second;
-      max = std::max(max, tmp.first);
+      op = instantiate_rec(op, t);
     }
 
-    return {max, expr};
+    return expr;
   }
 }
 
@@ -205,8 +201,8 @@ exprt instantiate(
   const mp_integer &t,
   const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes);
-  return wl_instantiate(expr, t).second;
+  wl_instantiatet wl_instantiate(no_timeframes, true);
+  return wl_instantiate(expr, t);
 }
 
 /*******************************************************************\
@@ -221,11 +217,11 @@ Function: instantiate_property
 
 \*******************************************************************/
 
-std::pair<mp_integer, exprt> instantiate_property(
+exprt instantiate_property(
   const exprt &expr,
   const mp_integer &current,
   const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes);
+  wl_instantiatet wl_instantiate(no_timeframes, false);
   return wl_instantiate(expr, current);
 }

src/trans-word-level/instantiate_word_level.h

@@ -12,19 +12,24 @@ Author: Daniel Kroening, [email protected]
 #include <util/mp_arith.h>
 #include <util/std_expr.h>
 
+// Instantiate a expression in the given time frame.
+// May contain next_symbol, but must not contain any temporal operators.
 exprt instantiate(
   const exprt &expr,
   const mp_integer &current,
   const mp_integer &no_timeframes);
 
-std::pair<mp_integer, exprt> instantiate_property(
+// Instantiate an atomic state predicate in the given time frame.
+// Must not contain next_symbol or any temporal operators.
+exprt instantiate_property(
   const exprt &,
   const mp_integer &current,
   const mp_integer &no_timeframes);
 
 std::string
 timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
 
+// Instantiate a symbol in the given time frame.
 symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt);
 
 #endif

src/trans-word-level/property.cpp

@@ -517,8 +517,7 @@ static obligationst property_obligations_rec(
   {
     // we rely on NNF
     auto &if_expr = to_if_expr(property_expr);
-    auto cond =
-      instantiate_property(if_expr.cond(), current, no_timeframes).second;
+    auto cond = instantiate_property(if_expr.cond(), current, no_timeframes);
     auto obligations_true =
       property_obligations_rec(if_expr.true_case(), current, no_timeframes)
         .conjunction();
@@ -577,7 +576,7 @@ static obligationst property_obligations_rec(
     {
       // state formula
       return obligationst{
-        instantiate_property(property_expr, current, no_timeframes)};
+        current, instantiate_property(property_expr, current, no_timeframes)};
     }
   }
   else if(property_expr.id() == ID_sva_implies)
@@ -721,7 +720,7 @@ static obligationst property_obligations_rec(
   else
   {
     return obligationst{
-      instantiate_property(property_expr, current, no_timeframes)};
+      current, instantiate_property(property_expr, current, no_timeframes)};
   }
 }
 

src/trans-word-level/sequence.cpp

@@ -456,7 +456,7 @@ sequence_matchest instantiate_sequence(
     // a state predicate
     auto &predicate = to_sva_boolean_expr(expr).op();
     auto instantiated = instantiate_property(predicate, t, no_timeframes);
-    return {{instantiated.first, instantiated.second}};
+    return {{t, instantiated}};
   }
   else
   {