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.

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