summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-21 19:09:37 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-21 19:09:37 -0700
commit84b52a48efda3e9658b772dbc02d34a6f6c9d16b (patch)
treec5ebcbf04525051ee046197cd46b5d6111d45245 /Source/Dafny/Translator.cs
parentb41056b45861f6ddb41e2a5e4d7c6d816684f095 (diff)
Adjust WF checks to use unsplit quantifiers.
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. The issue boiled down to being able to verify (forall x :: x != null && x.a == 0). Of course, the assumption that WF checks produce for a quantifier is a quantifier, so it uses the split expression.
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r--Source/Dafny/Translator.cs32
1 files changed, 17 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));