From c55cb226f4de90b080aa809d883d52c3386db063 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 26 Aug 2015 18:36:34 -0700 Subject: Improve the redundancy detection algorithm used while constructing sets of terms Based on an issue noted by Chris with redundancy removal resuls being dependent on the order of the terms. Interestingly, one of our tests already had an instance of that problem. Also fix the issue with nested quantifiers getting redundant triggers. --- .../function-applications-are-triggers.dfy.expect | 2 +- .../redundancy-detection-is-bidirectional.dfy | 29 ++++++++++++++++++++++ ...edundancy-detection-is-bidirectional.dfy.expect | 12 +++++++++ 3 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy.expect (limited to 'Test') 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/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy new file mode 100644 index 00000000..df1d78c3 --- /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 tests 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 -- cgit v1.2.3 From 7a993f6c87eaa82f383b1c5e7411f1878d4edf30 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 16:10:25 -0700 Subject: Small fix: there is no loop in (forall x :: Q(x) && Q(0)) Again, spotted by Chris :) --- Source/Dafny/Triggers/QuantifiersCollection.cs | 4 +++- Source/Dafny/Triggers/TriggerExtensions.cs | 8 ++++---- Test/triggers/redundancy-detection-is-bidirectional.dfy | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 114d5f5d..b77afccb 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -100,7 +100,9 @@ namespace Microsoft.Dafny.Triggers { // quantifier that matches one of the terms of the trigger (this ensures that // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even // ignore terms that almost match a trigger term, modulo a single variable - // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). + // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). + // The last thing that we ignore is matching variables against constants, + // to ensure that P(x) is not flagged as looping with P(0). // This ignoring logic is implemented by the CouldCauseLoops method. foreach (var q in quantifiers) { diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 71414eee..dccd996d 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -33,7 +33,7 @@ namespace Microsoft.Dafny.Triggers { internal bool CouldCauseLoops(List terms) { var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr)); + return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr)); } } @@ -79,15 +79,15 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); } - internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) { + internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; if (expr1 is IdentifierExpr) { - return expr2 is IdentifierExpr; + return expr2 is IdentifierExpr || expr2 is LiteralExpr; } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2)); + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy index df1d78c3..06541b70 100644 --- a/Test/triggers/redundancy-detection-is-bidirectional.dfy +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" -// This tests checks for tricky cases of redundancy suppression when building +// This test checks for tricky cases of redundancy suppression when building // triggers. predicate P(x: int, y: int) -- cgit v1.2.3 From 1e725f0c9382a3dd8be109d160581868c9567f61 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel 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. --- Source/Dafny/Triggers/QuantifiersCollection.cs | 7 +++++-- Source/Dafny/Triggers/TriggerExtensions.cs | 23 +++++++++++++++++----- Source/Dafny/Triggers/TriggersCollector.cs | 3 ++- Test/triggers/loop-detection-is-not-too-strict.dfy | 21 +++++++++++++++++++- .../loop-detection-is-not-too-strict.dfy.expect | 17 ++++++++++++---- 5 files changed, 58 insertions(+), 13 deletions(-) (limited to 'Test') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index b77afccb..50458ab7 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -101,8 +101,11 @@ namespace Microsoft.Dafny.Triggers { // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even // ignore terms that almost match a trigger term, modulo a single variable // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). - // The last thing that we ignore is matching variables against constants, - // to ensure that P(x) is not flagged as looping with P(0). + // In addition, we ignore cases where the only differences between a trigger + // and a trigger match are places where a variable is replaced with an + // expression whose free variables do not intersect that of the quantifier + // in which that expression is found. For examples of this behavious, see + // triggers/literals-do-not-cause-loops. // This ignoring logic is implemented by the CouldCauseLoops method. foreach (var q in quantifiers) { diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index dccd996d..d4a822a8 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -31,9 +31,15 @@ namespace Microsoft.Dafny.Triggers { return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); } - internal bool CouldCauseLoops(List terms) { + /// + /// This method checks whether this match could actually cause a loop, given a set of terms participating in a trigger; + /// to compute an answer, we match the Expr of this match against the Exprs of each of these term, allowing for harmless + /// variations. If any of these tests does match, this term likely won't cause a loop. + /// The boundVars list is useful to determine that forall x :: P(x) == P(y+z) does not loop. + /// + internal bool CouldCauseLoops(List terms, ISet boundVars) { var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr)); + return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars)); } } @@ -79,15 +85,22 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); } - internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) { + internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet boundVars) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; if (expr1 is IdentifierExpr) { - return expr2 is IdentifierExpr || expr2 is LiteralExpr; + if (expr2 is IdentifierExpr) { + return true; + } else { + var freeInE2 = Translator.ComputeFreeVariables(expr2); + freeInE2.IntersectWith(boundVars); + return !freeInE2.Any(); + } } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2)); + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, + expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index d78bcb9e..cc3b1978 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -69,7 +69,8 @@ namespace Microsoft.Dafny.Triggers { internal IEnumerable LoopingSubterms(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier var matchingSubterms = this.MatchingSubterms(quantifier); - return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); + var boundVars = new HashSet(quantifier.BoundVars); + return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars)); } internal List MatchingSubterms(QuantifierExpr quantifier) { 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 From 71bcbeb4ce808f463d86b7a877e3e550e839fb17 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 22:52:14 -0700 Subject: Add a small test from the IronClad notebook --- ...ix-an-issue-listed-in-the-ironclad-notebook.dfy | 23 ++++++++++++++++++++++ ...ssue-listed-in-the-ironclad-notebook.dfy.expect | 4 ++++ 2 files changed, 27 insertions(+) create mode 100644 Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy create mode 100644 Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect (limited to 'Test') 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 +type Value = seq + +type Hashtable = map +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 -- cgit v1.2.3