Merge pull request #712 from diffblue/BMC-full-LTL

BMC: support full LTL

regression/ebmc/smv/smv_ltlspec6.desc

@@ -0,0 +1,7 @@
+CORE broken-smt-backend
+smv_ltlspec6.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec6.smv

@@ -0,0 +1,29 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+DEFINE p := x != 0;
+DEFINE q := x = 3;
+
+-- various equivalences
+LTLSPEC (G p) <-> (G G p)
+LTLSPEC (G p) <-> (!F !p)
+LTLSPEC (G p) <-> (p & X G p)
+LTLSPEC (FALSE R p) -> (G p)
+LTLSPEC (G (p&q)) <-> ((G p) & (G q))
+
+LTLSPEC (F p) <-> (F F p)
+LTLSPEC (F p) <-> (!G x = 0)
+LTLSPEC (F p) <-> (p | X F p)
+LTLSPEC (F (p|q)) <-> ((F p) | (F q))
+
+LTLSPEC (X p) <-> (!X !p)

regression/ebmc/smv/smv_ltlspec_F1.desc

@@ -8,8 +8,8 @@ smv_ltlspec_F1.smv
 ^\[.*\] F x = 2: PROVED up to bound 10$
 ^\[.*\] F x = 1 & F x = 2: PROVED up to bound 10$
 ^\[.*\] F x = 0 & F x = 1: REFUTED$
-^\[.*\] F x = 0 \| F x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] F x = 0 -> FALSE: FAILURE: property not supported by BMC engine$
-^\[.*\] F x = 1 -> F x = 0: FAILURE: property not supported by BMC engine$
+^\[.*\] F x = 0 \| F x = 1: PROVED up to bound 10$
+^\[.*\] F x = 0 -> FALSE: PROVED up to bound 10$
+^\[.*\] F x = 1 -> F x = 0: REFUTED$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_F2.desc

@@ -6,10 +6,10 @@ smv_ltlspec_F2.smv
 ^\[.*\] !F x = 0: PROVED up to bound 10$
 ^\[.*\] !F x = 1: REFUTED$
 ^\[.*\] !F x = 2: REFUTED$
-^\[.*\] !\(F x = 1 & F x = 2\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(F x = 0 & F x = 1\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 1 & F x = 2\): REFUTED$
+^\[.*\] !\(F x = 0 & F x = 1\): PROVED up to bound 10$
 ^\[.*\] !\(F x = 0 \| F x = 1\): REFUTED$
-^\[.*\] !\(F x = 0 -> FALSE\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(F x = 1 -> F x = 0\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 0 -> FALSE\): REFUTED$
+^\[.*\] !\(F x = 1 -> F x = 0\): PROVED up to bound 10$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G1.desc

@@ -8,8 +8,8 @@ smv_ltlspec_G1.smv
 ^\[.*\] G x != 2: REFUTED$
 ^\[.*\] G x != 5 & G x != 6: PROVED up to bound 10$
 ^\[.*\] G x != 2 & G x != 5: REFUTED$
-^\[.*\] G x != 5 \| G x != 2: FAILURE: property not supported by BMC engine$
-^\[.*\] G x != 2 -> FALSE: FAILURE: property not supported by BMC engine$
-^\[.*\] G x != 5 -> G x != 2: FAILURE: property not supported by BMC engine$
+^\[.*\] G x != 5 \| G x != 2: PROVED up to bound 10$
+^\[.*\] G x != 2 -> FALSE: PROVED up to bound 10$
+^\[.*\] G x != 5 -> G x != 2: REFUTED$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G2.desc

@@ -6,10 +6,10 @@ smv_ltlspec_G2.smv
 ^\[.*\] !G x != 5: REFUTED$
 ^\[.*\] !G x != 6: REFUTED$
 ^\[.*\] !G x != 2: PROVED up to bound 10$
-^\[.*\] !\(G x != 5 & G x != 6\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(G x != 2 & G x != 5\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 5 & G x != 6\): REFUTED$
+^\[.*\] !\(G x != 2 & G x != 5\): PROVED up to bound 10$
 ^\[.*\] !\(G x != 5 \| G x != 2\): REFUTED$
-^\[.*\] !\(G x != 2 -> FALSE\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(G x != 5 -> G x != 2\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 2 -> FALSE\): REFUTED$
+^\[.*\] !\(G x != 5 -> G x != 2\): PROVED up to bound 10$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_R1.desc

@@ -1,12 +1,12 @@
 CORE broken-smt-backend
 smv_ltlspec_R1.smv
 --bound 10
-^\[.*\] x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] FALSE R x != 4: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
+^\[.*\] FALSE R x != 4: REFUTED$
+^\[.*\] x = 2 R x = 1: REFUTED$
+^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: REFUTED$
+^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$
+^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/smv/smv_ltlspec_U1.desc

@@ -1,11 +1,11 @@
 CORE broken-smt-backend
 smv_ltlspec_U1.smv
 --bound 10
-\[.*\] x = 1 U x = 2: FAILURE: property not supported by BMC engine$
-\[.*\] x != 0 U FALSE: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 3: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: FAILURE: property not supported by BMC engine$
+\[.*\] x = 1 U x = 2: PROVED up to bound 10$
+\[.*\] x != 0 U FALSE: PROVED up to bound 10$
+\[.*\] x = 1 U x = 3: REFUTED$
+\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: PROVED up to bound 10$
+\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_until1.desc

@@ -1,12 +1,11 @@
-KNOWNBUG
+CORE
 sva_until1.sv
 --bound 1
-^\[main\.p0\] always (main.a until_with main.b): REFUTED$
-^\[main\.p1\] always (main.a until main.b): REFUTED$
-^\[main\.p2\] always (main.a s_until main.b): REFUTED$
+^\[main\.p0\] always \(main.a until_with main.b\): REFUTED$
+^\[main\.p1\] always \(main.a until main.b\): REFUTED$
+^\[main\.p2\] always \(main.a s_until main.b\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-These properties are not supported by the BMC engine.

src/temporal-logic/normalize_property.cpp

@@ -62,7 +62,7 @@ exprt normalize_pre_not(not_exprt expr)
   else if(op.id() == ID_sva_s_eventually)
   {
     // ¬ sva_s_eventually φ --> sva_always ¬φ
-    return sva_always_exprt{not_exprt{to_sva_eventually_expr(op).op()}};
+    return sva_always_exprt{not_exprt{to_sva_s_eventually_expr(op).op()}};
   }
 
   return std::move(expr);
@@ -100,7 +100,7 @@ exprt normalize_pre_sva_non_overlapped_implication(
 exprt normalize_pre_sva_not(sva_not_exprt expr)
 {
   // Same as regular 'not'. These do not apply to sequences.
-  return not_exprt{expr.op()};
+  return normalize_pre_not(not_exprt{expr.op()});
 }
 
 exprt normalize_pre_sva_and(sva_and_exprt expr)

src/trans-word-level/property.cpp

@@ -40,44 +40,7 @@ Function: bmc_supports_LTL_property
 
 bool bmc_supports_LTL_property(const exprt &expr)
 {
-  // We support
-  // * formulas that contain no temporal operator besides X
-  // * Gφ, where φ contains no temporal operator besides X
-  // * Fφ, where φ contains no temporal operator besides X
-  // * GFφ, where φ contains no temporal operator besides X
-  // * conjunctions of supported LTL properties
-  auto non_X_LTL_operator = [](const exprt &expr)
-  { return is_LTL_operator(expr) && expr.id() != ID_X; };
-
-  if(!has_subexpr(expr, non_X_LTL_operator))
-  {
-    return true;
-  }
-  else if(expr.id() == ID_F)
-  {
-    return !has_subexpr(to_F_expr(expr).op(), non_X_LTL_operator);
-  }
-  else if(expr.id() == ID_G)
-  {
-    auto &op = to_G_expr(expr).op();
-    if(op.id() == ID_F)
-    {
-      return !has_subexpr(to_F_expr(op).op(), non_X_LTL_operator);
-    }
-    else
-    {
-      return !has_subexpr(op, non_X_LTL_operator);
-    }
-  }
-  else if(expr.id() == ID_and)
-  {
-    for(auto &op : expr.operands())
-      if(!bmc_supports_LTL_property(op))
-        return false;
-    return true;
-  }
-  else
-    return false;
+  return true;
 }
 
 /*******************************************************************\
@@ -414,12 +377,13 @@ static obligationst property_obligations_rec(
     }
   }
   else if(
-    property_expr.id() == ID_sva_until || property_expr.id() == ID_sva_s_until)
+    property_expr.id() == ID_sva_until ||
+    property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
   {
     // non-overlapping until
     // we need a lasso to refute these
 
-    // we expand: p U q <=> q || (p && X(p U q))
+    // we expand: p U q <=> q ∨ (p ∧ X(p U q))
     exprt tmp_q = to_binary_expr(property_expr).op1();
     tmp_q = property_obligations_rec(tmp_q, solver, current, no_timeframes, ns)
               .conjunction()
@@ -437,11 +401,40 @@ static obligationst property_obligations_rec(
     {
       auto obligations_rec = property_obligations_rec(
         property_expr, solver, next, no_timeframes, ns);
-      expansion = and_exprt(expansion, obligations_rec.conjunction().second);
+      expansion = and_exprt{expansion, obligations_rec.conjunction().second};
     }
 
     DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-    return obligationst{no_timeframes - 1, or_exprt(tmp_q, expansion)};
+    return obligationst{no_timeframes - 1, or_exprt{tmp_q, expansion}};
+  }
+  else if(property_expr.id() == ID_R)
+  {
+    // we expand: p R q <=> q ∧ (p ∨ X(p R q))
+    auto &R_expr = to_R_expr(property_expr);
+    auto tmp_q =
+      property_obligations_rec(R_expr.rhs(), solver, current, no_timeframes, ns)
+        .conjunction()
+        .second;
+
+    auto tmp_p =
+      property_obligations_rec(R_expr.lhs(), solver, current, no_timeframes, ns)
+        .conjunction()
+        .second;
+
+    const auto next = current + 1;
+    exprt expansion;
+
+    if(next < no_timeframes)
+    {
+      auto obligations_rec = property_obligations_rec(
+        property_expr, solver, next, no_timeframes, ns);
+      expansion = or_exprt{tmp_p, obligations_rec.conjunction().second};
+    }
+    else
+      expansion = tmp_p;
+
+    DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
+    return obligationst{no_timeframes - 1, and_exprt{tmp_q, expansion}};
   }
   else if(
     property_expr.id() == ID_sva_until_with ||
@@ -493,6 +486,17 @@ static obligationst property_obligations_rec(
 
     return obligationst{t, disjunction(disjuncts)};
   }
+  else if(
+    property_expr.id() == ID_equal &&
+    to_equal_expr(property_expr).lhs().type().id() == ID_bool)
+  {
+    // we rely on NNF: a<=>b ---> a=>b && b=>a
+    auto &equal_expr = to_equal_expr(property_expr);
+    auto tmp = and_exprt{
+      implies_exprt{equal_expr.lhs(), equal_expr.rhs()},
+      implies_exprt{equal_expr.rhs(), equal_expr.lhs()}};
+    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+  }
   else if(property_expr.id() == ID_implies)
   {
     // we rely on NNF
@@ -528,8 +532,79 @@ static obligationst property_obligations_rec(
   }
   else if(property_expr.id() == ID_not)
   {
-    return obligationst{
-      instantiate_property(property_expr, current, no_timeframes, ns)};
+    // We need NNF, try to eliminate the negation.
+    auto &op = to_not_expr(property_expr).op();
+
+    if(op.id() == ID_U)
+    {
+      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+      auto &U = to_U_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_R)
+    {
+      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+      auto &R = to_R_expr(op);
+      auto U = U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+      return property_obligations_rec(U, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_G)
+    {
+      // ¬G φ ≡ F ¬φ
+      auto &G = to_G_expr(op);
+      auto F = F_exprt{not_exprt{G.op()}};
+      return property_obligations_rec(F, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_F)
+    {
+      // ¬F φ ≡ G ¬φ
+      auto &F = to_F_expr(op);
+      auto G = G_exprt{not_exprt{F.op()}};
+      return property_obligations_rec(G, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_X)
+    {
+      // ¬X φ ≡ X ¬φ
+      auto &X = to_X_expr(op);
+      auto negX = X_exprt{not_exprt{X.op()}};
+      return property_obligations_rec(negX, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_implies)
+    {
+      // ¬(a->b) --> a && ¬b
+      auto &implies_expr = to_implies_expr(op);
+      auto and_expr =
+        and_exprt{implies_expr.lhs(), not_exprt{implies_expr.rhs()}};
+      return property_obligations_rec(
+        and_expr, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_and)
+    {
+      auto operands = op.operands();
+      for(auto &op : operands)
+        op = not_exprt{op};
+      auto or_expr = or_exprt{std::move(operands)};
+      return property_obligations_rec(
+        or_expr, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_or)
+    {
+      auto operands = op.operands();
+      for(auto &op : operands)
+        op = not_exprt{op};
+      auto and_expr = and_exprt{std::move(operands)};
+      return property_obligations_rec(
+        and_expr, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_not)
+    {
+      return property_obligations_rec(
+        to_not_expr(op).op(), solver, current, no_timeframes, ns);
+    }
+    else
+      return obligationst{
+        instantiate_property(property_expr, current, no_timeframes, ns)};
   }
   else
   {