Merge pull request #721 from diffblue/sva_until_with

SVA until_with

Author: tautschnig

regression/ebmc/SVA-LTL/simple_passing_LTL_properties.desc

@@ -4,13 +4,15 @@ simple_passing_LTL_properties.sv
 ^Adding lasso constraints$
 ^EXIT=0$
 ^SIGNAL=0$
-^\[top\.p0\] .* PROVED up to bound 10$
-^\[top\.p1\] .* PROVED up to bound 10$
-^\[top\.p2\] .* PROVED up to bound 10$
-^\[top\.p3\] .* PROVED up to bound 10$
-^\[top\.p4\] .* PROVED up to bound 10$
-^\[top\.p5\] .* PROVED up to bound 10$
-^\[top\.p6\] .* PROVED up to bound 10$
-^\[top\.p7\] .* PROVED up to bound 10$
-^\[top\.p8\] .* PROVED up to bound 10$
+^\[top\.p00\] .* PROVED up to bound 10$
+^\[top\.p01\] .* PROVED up to bound 10$
+^\[top\.p02\] .* PROVED up to bound 10$
+^\[top\.p03\] .* PROVED up to bound 10$
+^\[top\.p04\] .* PROVED up to bound 10$
+^\[top\.p05\] .* PROVED up to bound 10$
+^\[top\.p06\] .* PROVED up to bound 10$
+^\[top\.p07\] .* PROVED up to bound 10$
+^\[top\.p08\] .* PROVED up to bound 10$
+^\[top\.p09\] .* PROVED up to bound 10$
+^\[top\.p10\] .* PROVED up to bound 10$
 --

regression/ebmc/SVA-LTL/simple_passing_LTL_properties.sv

@@ -11,15 +11,17 @@ module top(input clock, input i1);
     counter=counter+1;
   end
 
-  p0: assert property (my_bit);
-  p1: assert property (always my_bit);
-  p2: assert property (counter==3 |-> nexttime counter==4);
-  p3: assert property (counter==3 |=> counter==4);
-  p4: assert property (counter==3 |=> nexttime counter==5);
-  p5: assert property (s_eventually counter==8);
-  p6: assert property (counter==0 |-> s_eventually counter==8);
-  p7: assert property (counter==0 |-> counter<=5 until counter==6);
-  p8: assert property (counter==0 |-> counter<=5 until_with counter==5);
+  p00: assert property (my_bit);
+  p01: assert property (always my_bit);
+  p02: assert property (counter==3 |-> nexttime counter==4);
+  p03: assert property (counter==3 |=> counter==4);
+  p04: assert property (counter==3 |=> nexttime counter==5);
+  p05: assert property (s_eventually counter==8);
+  p06: assert property (counter==0 |-> s_eventually counter==8);
+  p07: assert property (counter==0 |-> counter<=5 until counter==6);
+  p08: assert property (counter==0 |-> counter<=5 s_until counter==6);
+  p09: assert property (counter==0 |-> counter<=5 until_with counter==5);
+  p10: assert property (counter==0 |-> counter<=5 s_until_with counter==5);
 
 endmodule
 

src/hw_cbmc_irep_ids.h

@@ -11,6 +11,7 @@ IREP_ID_ONE(ER)
 IREP_ID_ONE(U)
 IREP_ID_ONE(weak_U)
 IREP_ID_ONE(R)
+IREP_ID_ONE(strong_R)
 IREP_ID_ONE(A)
 IREP_ID_ONE(F)
 IREP_ID_ONE(E)

src/temporal-logic/temporal_expr.h

@@ -262,6 +262,29 @@ static inline R_exprt &to_R_expr(exprt &expr)
   return static_cast<R_exprt &>(expr);
 }
 
+class strong_R_exprt : public binary_predicate_exprt
+{
+public:
+  explicit strong_R_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_strong_R, std::move(op1))
+  {
+  }
+};
+
+static inline const strong_R_exprt &to_strong_R_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_strong_R);
+  strong_R_exprt::check(expr);
+  return static_cast<const strong_R_exprt &>(expr);
+}
+
+static inline strong_R_exprt &to_strong_R_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_strong_R);
+  strong_R_exprt::check(expr);
+  return static_cast<strong_R_exprt &>(expr);
+}
+
 class ER_exprt : public binary_predicate_exprt
 {
 public:

src/trans-word-level/property.cpp

@@ -371,9 +371,7 @@ static obligationst property_obligations_rec(
       return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only
     }
   }
-  else if(
-    property_expr.id() == ID_sva_until ||
-    property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
+  else if(property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
   {
     auto &p = to_binary_expr(property_expr).lhs();
     auto &q = to_binary_expr(property_expr).rhs();
@@ -383,11 +381,11 @@ static obligationst property_obligations_rec(
 
     return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
-  else if(property_expr.id() == ID_weak_U)
+  else if(property_expr.id() == ID_sva_until || property_expr.id() == ID_weak_U)
   {
     // we expand: p W q ≡ q ∨ ( p ∧ X(p W q) )
-    auto &p = to_weak_U_expr(property_expr).lhs();
-    auto &q = to_weak_U_expr(property_expr).rhs();
+    auto &p = to_binary_expr(property_expr).lhs();
+    auto &q = to_binary_expr(property_expr).rhs();
 
     // Once we reach the end of the unwinding, replace X(p W q) by 'true'.
     auto tmp = or_exprt{
@@ -411,23 +409,33 @@ static obligationst property_obligations_rec(
 
     return property_obligations_rec(expansion, current, no_timeframes, ns);
   }
-  else if(
-    property_expr.id() == ID_sva_until_with ||
-    property_expr.id() == ID_sva_s_until_with)
+  else if(property_expr.id() == ID_strong_R)
   {
-    // overlapping until
-
-    // we rewrite using 'next'
-    binary_exprt tmp = to_binary_expr(property_expr);
-    if(property_expr.id() == ID_sva_until_with)
-      tmp.id(ID_sva_until);
-    else
-      tmp.id(ID_sva_s_until);
+    auto &p = to_strong_R_expr(property_expr).lhs();
+    auto &q = to_strong_R_expr(property_expr).rhs();
 
-    tmp.op1() = X_exprt{tmp.op1()};
+    // p strongR q ≡ Fp ∧ (p R q)
+    exprt tmp = and_exprt{F_exprt{q}, weak_U_exprt{p, q}};
 
     return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
+  else if(property_expr.id() == ID_sva_until_with)
+  {
+    // Rewrite to LTL (weak) R.
+    // Note that lhs and rhs are flipped.
+    auto &until_with = to_sva_until_with_expr(property_expr);
+    auto R = R_exprt{until_with.rhs(), until_with.lhs()};
+    return property_obligations_rec(R, solver, current, no_timeframes, ns);
+  }
+  else if(property_expr.id() == ID_sva_s_until_with)
+  {
+    // Rewrite to LTL (strong) R.
+    // Note that lhs and rhs are flipped.
+    auto &s_until_with = to_sva_s_until_with_expr(property_expr);
+    auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()};
+    return property_obligations_rec(
+      strong_R, solver, current, no_timeframes, ns);
+  }
   else if(property_expr.id() == ID_and)
   {
     // Generate seperate sets of obligations for each conjunct,
@@ -571,6 +579,40 @@ static obligationst property_obligations_rec(
       return property_obligations_rec(
         to_not_expr(op).op(), current, no_timeframes, ns);
     }
+    else if(op.id() == ID_sva_until)
+    {
+      // ¬(φ W ψ) ≡ (¬φ strongR ¬ψ)
+      auto &W = to_sva_until_expr(op);
+      auto strong_R = strong_R_exprt{not_exprt{W.lhs()}, not_exprt{W.rhs()}};
+      return property_obligations_rec(
+        strong_R, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_sva_s_until)
+    {
+      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+      auto &U = to_sva_s_until_expr(op);
+      auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+      return property_obligations_rec(R, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_sva_until_with)
+    {
+      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+      // Note LHS and RHS are swapped.
+      auto &until_with = to_sva_until_with_expr(op);
+      auto R = R_exprt{until_with.rhs(), until_with.lhs()};
+      auto U = sva_until_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+      return property_obligations_rec(U, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_sva_s_until_with)
+    {
+      // ¬(φ strongR ψ) ≡ (¬φ W ¬ψ)
+      // Note LHS and RHS are swapped.
+      auto &s_until_with = to_sva_s_until_with_expr(op);
+      auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()};
+      auto W =
+        weak_U_exprt{not_exprt{strong_R.lhs()}, not_exprt{strong_R.rhs()}};
+      return property_obligations_rec(W, solver, current, no_timeframes, ns);
+    }
     else
       return obligationst{
         instantiate_property(property_expr, current, no_timeframes)};