diff options
Diffstat (limited to 'Test')
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
|