Merge

7 files changed, 102 insertions, 6 deletions

diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
new file mode 100644
index 00000000..09032453
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This example was listed in IronClad's notebook as one place were z3 picked

+// much too liberal triggers. THe Boogie code for this is shown below:

+//

+// forall k#2: Seq Box :: $Is(k#2, TSeq(TInt)) && $IsAlloc(k#2, TSeq(TInt), $Heap)

+//                   ==> Seq#Equal(_module.__default.HashtableLookup($Heap, h1#0, k#2),

+//                                 _module.__default.HashtableLookup($Heap, h2#0, k#2))

+//

+// and z3 would pick $Is(k#2, TSeq(TInt)) or $IsAlloc(k#2, TSeq(TInt), $Heap) as

+// triggers.

+

+type Key = seq<int>

+type Value = seq<int>

+

+type Hashtable = map<Key, Value>

+function HashtableLookup(h: Hashtable, k: Key): Value

+

+lemma HashtableAgreement(h1:Hashtable, h2:Hashtable, k:Key)

+  requires forall k :: HashtableLookup(h1,k) == HashtableLookup(h2,k) {

+    assert true || (k in h1) == (k in h2);

+}

diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
new file mode 100644
index 00000000..46ec143e
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
@@ -0,0 +1,4 @@
+auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy(21,11): Info: Selected triggers:

+   {HashtableLookup(h2, k)}, {HashtableLookup(h1, k)}

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 7922e88d..501cfa51 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1
 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:

    {f(10)}, {f.requires(10)}

 function-applications-are-triggers.dfy(12,5): Info: Selected triggers:

-   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}

+   {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}

 

 Dafny program verifier finished with 2 verified, 0 errors

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

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
new file mode 100644
index 00000000..06541b70
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test checks for tricky cases of redundancy suppression when building

+// triggers.

+

+predicate P(x: int, y: int)

+predicate Q(x: int)

+predicate R(x: int)

+

+method M() {

+  // For this term, it is enough to order the terms by number of variables

+  assert forall x, y :: true || P(x, y) || Q(y) || R(x);

+  assert forall x, y :: true || Q(y) || P(x, y) || R(x);

+  assert forall x, y :: true || Q(y) || R(x) || P(x, y);

+}

+

+predicate PP(x: int, y: int, z: int)

+predicate QQ(x: int, y: int)

+predicate RR(x: int, y: int)

+predicate SS(x: int, y: int)

+

+method MM() {

+  // Not for this one, though

+  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);

+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);

+}

diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
new file mode 100644
index 00000000..78c9e7ca
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
@@ -0,0 +1,12 @@
+redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:

+   {R(x), Q(y)}, {P(x, y)}

+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:

+   {P(x, y)}, {R(x), Q(y)}

+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}

+

+Dafny program verifier finished with 11 verified, 0 errors