From 1e725f0c9382a3dd8be109d160581868c9567f61 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 27 Aug 2015 21:25:06 -0700
Subject: Further relax the loop detection conditions

Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.
---
 Test/triggers/loop-detection-is-not-too-strict.dfy  | 21 ++++++++++++++++++++-
 .../loop-detection-is-not-too-strict.dfy.expect     | 17 +++++++++++++----
 2 files changed, 33 insertions(+), 5 deletions(-)

(limited to 'Test/triggers')

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
index a5a30c81..81f764ad 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -7,8 +7,9 @@
 // equal to that trigger, as long as the only differences are variable
 
 predicate P(x: int, y: int)
+predicate Q(x: int)
 
-method Test() {
+method Test(z: int) {
   // P(x, y) and P(y, x) might look like they would cause a loop. Since they
   // only differ by their variables, though, they won't raise flags.
   assume forall x: int, y: int :: P(x, y) == P(y, x);
@@ -18,4 +19,22 @@ method Test() {
 
   // Contrast with the following:
   assume forall x: int, y: int :: P(x, y) == P(x, y+1);
+
+  // The following examples were made legal after an exchange where Chris
+  // pointed examples in the IronClad sources where things like this were
+  // incorrectly flagged.
+  assert forall x :: true || Q(x) || Q(0);
+  assert forall x :: true || Q(x) || Q(z);
+  assert forall x :: true || P(x, 1) || P(x, z);
+
+  // Support for the following was added following a discussion with Rustan; in
+  // the second one the expression `if z > 1 then z else 3 * z + 1` is not
+  // directly a constant expression, but it does not involve x, so it's ok:
+  assert forall x :: true || Q(x) || Q(0+1);
+  assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1);
+  // Sanity check:
+  assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1);
+
+  // WISH: It might also be good to zeta-reduce before loop detection.
+  assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));
 }
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 6f5ed3d7..705c2a8c 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -1,8 +1,17 @@
-loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers:
+loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:
+loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})
+loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})
  (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)}
+loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)}
+loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers:
+   {P(x, z)}, {P(x, 1)}
+loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)}
+loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)}
+loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)})
+ (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)}
 
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 4 verified, 0 errors
-- 
cgit v1.2.3