diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 32 | ||||
| -rw-r--r-- | Test/triggers/wf-checks-use-the-original-quantifier.dfy | 28 | ||||
| -rw-r--r-- | Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect | 17 |
3 files changed, 62 insertions, 15 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 6f1a5833..524466c9 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4437,7 +4437,7 @@ namespace Microsoft.Dafny { var e = (ComprehensionExpr)expr;
var canCall = CanCallAssumption(e.Term, etran);
var q = e as QuantifierExpr;
-
+
if (q != null && q.SplitQuantifier != null) {
return CanCallAssumption(q.SplitQuantifierExpression, etran);
}
@@ -4735,12 +4735,7 @@ namespace Microsoft.Dafny { // If the quantifier is universal, then continue as:
// assume (\forall x :: body(x));
// Create local variables corresponding to the type arguments:
-
- if (e.SplitQuantifier != null) {
- CheckWellformedAndAssume(e.SplitQuantifierExpression, options, locals, builder, etran);
- return;
- }
-
+
var typeArgumentCopies = Map(e.TypeArgs, tp => e.Refresh(tp, CurrentIdGenerator));
var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp)));
var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));
@@ -4748,15 +4743,24 @@ namespace Microsoft.Dafny { // Create local variables corresponding to the in-parameters:
var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran, typeMap);
// Get the body of the quantifier and suitably substitute for the type variables and bound variables
- var body = Substitute(e.LogicalBody(), null, substMap, typeMap);
+ var body = Substitute(e.LogicalBody(true), null, substMap, typeMap);
CheckWellformedAndAssume(body, options, locals, builder, etran);
+
if (e is ForallExpr) {
- builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));
+ // Although we do the WF check on the original quantifier, we assume the split one.
+ // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify.
+ builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(e.SplitQuantifierExpression ?? e)));
}
return;
}
+
// resort to the behavior of simply checking well-formedness followed by assuming the translated expression
CheckWellformed(expr, options, locals, builder, etran);
+
+ // NOTE: If the CheckWellformed call above found a split quantifier, it ignored
+ // the splitting and proceeded to decompose the full quantifier as
+ // normal. This call to TrExpr, on the other hand, will indeed use the
+ // split quantifier.
builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));
}
@@ -5276,10 +5280,8 @@ namespace Microsoft.Dafny { var q = e as QuantifierExpr;
var lam = e as LambdaExpr;
- if (q != null && q.SplitQuantifier != null) {
- CheckWellformedWithResult(q.SplitQuantifierExpression, options, result, resultType, locals, builder, etran);
- return;
- }
+ // This is a WF check, so we look at the original quantifier, not the split one.
+ // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify.
var typeMap = new Dictionary<TypeParameter, Type>();
var copies = new List<TypeParameter>();
@@ -5298,7 +5300,6 @@ namespace Microsoft.Dafny { var newEtran = etran;
builder.Add(new Bpl.CommentCmd("Begin Comprehension WF check"));
BplIfIf(e.tok, lam != null, null, builder, newBuilder => {
-
if (lam != null) {
// Havoc heap, unless oneShot
if (!lam.OneShot) {
@@ -13098,7 +13099,8 @@ namespace Microsoft.Dafny { return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
}
- Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector();
+ // Using an empty set of old expressions is ok here; the only uses of the triggersCollector will be to check for trigger killers.
+ Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector(new HashSet<Expression>());
private bool CanSafelySubstitute(ISet<IVariable> protectedVariables, IVariable variable, Expression substitution) {
return !(protectedVariables.Contains(variable) && triggersCollector.IsTriggerKiller(substitution));
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy b/Test/triggers/wf-checks-use-the-original-quantifier.dfy new file mode 100644 index 00000000..a1a2bd90 --- /dev/null +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy @@ -0,0 +1,28 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test checks that typical expressions requiring WF checks do not suddenly
+// loose expressivity due to quantifier splitting. Without special care, the
+// expression (forall x :: x != null && x.a == 0) could fail to verify.
+
+// The logic about split quantifiers is that Boogie (and z3) should never realize
+// that there was an unsplit quantifier. The WF check code does not produce a
+// quantifier, at least in it's checking part; thus, it should use original
+// quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null
+// check, and a problem spotted by Chris, made into a test case saved in
+// triggers/wf-checks-use-the-original-quantifier.dfy.
+
+// Of course, the assumption that WF checks produce for a quantifier is a
+// quantifier, so the assumption part that comes after the WF check does use the
+// split expression.
+
+// This test case is inspired by the example that Chris gave.
+
+predicate P(b: nat)
+function f(a: int): int
+class C { var x: int; }
+
+method M(s: set<C>)
+ requires forall n: nat :: 0 <= f(n) && P(f(n))
+ requires forall c, c' | c in s && c' in s :: c != null && c'!= null && c.x == c'.x {
+}
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect new file mode 100644 index 00000000..6b152262 --- /dev/null +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect @@ -0,0 +1,17 @@ +wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}:
+ Selected triggers: {f(n)}
+ Rejected triggers: {P(f(n))} (more specific than {f(n)})
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}:
+ Selected triggers: {f(n)}
+ Rejected triggers: {P(f(n))} (more specific than {f(n)})
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}:
+ Selected triggers:
+ {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}:
+ Selected triggers:
+ {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}:
+ Selected triggers:
+ {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
+
+Dafny program verifier finished with 4 verified, 0 errors
|