diff options
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerExtensions.cs | 23 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggersCollector.cs | 3 | ||||
| -rw-r--r-- | Test/triggers/loop-detection-is-not-too-strict.dfy | 21 | ||||
| -rw-r--r-- | Test/triggers/loop-detection-is-not-too-strict.dfy.expect | 17 |
5 files changed, 58 insertions, 13 deletions
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<TriggerTerm> terms) {
+ /// <summary>
+ /// 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.
+ /// </summary>
+ internal bool CouldCauseLoops(List<TriggerTerm> terms, ISet<BoundVar> 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<BoundVar> 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<BoundVar> holes, Dictionary<IVariable, Expression> 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<TriggerMatch> 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<BoundVar>(quantifier.BoundVars);
+ return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars));
}
internal List<TriggerMatch> 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
|