Make quantifier splitting a two step process

This fixes a bug that affected Monad.dfy

5 files changed, 60 insertions, 8 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c4ea0a5a..c7aae173 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4796,7 +4796,7 @@ namespace Microsoft.Dafny {
     }

     public override IEnumerable<Expression> SubExpressions

     {

-      get {

+      get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place

         foreach (var e in base.SubExpressions) { yield return e; }

         foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }

         

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 557eee93..9bc24c30 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -68,6 +68,7 @@ namespace Microsoft.Dafny
       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         splitter.Visit(decl);

       }

+      splitter.Commit();

     }

   }

 

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 83059f8d..865aa33e 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -1,11 +1,19 @@
 using Microsoft.Boogie;

 using System;

 using System.Collections.Generic;

+using System.Diagnostics.Contracts;

 using System.Linq;

 using System.Text;

 

 namespace Microsoft.Dafny.Triggers {

   class QuantifierSplitter : BottomUpVisitor {

+    /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times.

+    /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier 

+    /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these 

+    /// split quantifiers got re-split, creating a situation where the direct children of a split quantifier were 

+    /// also split quantifiers.

+    private Dictionary<QuantifierExpr, List<Expression>> splits = new Dictionary<QuantifierExpr, List<Expression>>();

+

     private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) {

       if (opCode == BinaryExpr.Opcode.And) {

         return BinaryExpr.Opcode.Or;

@@ -24,8 +32,15 @@ namespace Microsoft.Dafny.Triggers {
     //   forall x :: P(x) ==> (Q(x) && R(x))

 

     private static UnaryOpExpr Not(Expression expr) {

-      var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };

-      return not;

+      return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };

+    }

+

+    private static Attributes CopyAttributes(Attributes source) {

+      if (source == null) {

+        return null;

+      } else {

+        return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev));

+      }

     }

 

     internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {

@@ -83,16 +98,29 @@ namespace Microsoft.Dafny.Triggers {
         yield return quantifier;

       }

     }

+    

+    private static bool AllowsSplitting(QuantifierExpr quantifier) {

+      bool splitAttr = true;

+      return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr;

+    }

 

     protected override void VisitOneExpr(Expression expr) {

       var quantifier = expr as QuantifierExpr;

-      if (quantifier != null && quantifier.SplitQuantifier == null) {

-        bool splitAttr = true;

-        if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) {

-          var split = SplitQuantifier(quantifier).ToList();

-          quantifier.SplitQuantifier = split;

+      if (quantifier != null) {

+        Contract.Assert(quantifier.SplitQuantifier == null);

+        if (!splits.ContainsKey(quantifier) && AllowsSplitting(quantifier)) {

+          splits[quantifier] = SplitQuantifier(quantifier).ToList();

         }

       }

     }

+

+    /// <summary>

+    /// See comments above definition of splits for reason why this method exists

+    /// </summary>

+    internal void Commit() {

+      foreach (var quantifier in splits.Keys) {

+        quantifier.SplitQuantifier = splits[quantifier];

+      }

+    }

   }

 }

diff --git a/Test/triggers/regression-tests.dfy b/Test/triggers/regression-tests.dfy
new file mode 100644
index 00000000..263e424a
--- /dev/null
+++ b/Test/triggers/regression-tests.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This tests checks that quantifier splitting is resilient to the fact that
+// certain statements (like calc) can return duplicate subexpressions. This was
+// once a problem, because a quantifier that got returned twice would get split
+// on the first pass over it, and would have its nely created children re-split
+// on the second pass. This created a split quantifier whose children were split
+// quantifiers, which violated an invariant of spliit quantifiers.
+
+abstract module Base { }
+
+module Blah refines Base {
+  lemma A() {
+    calc {
+	    forall b :: b;
+   	}
+  }
+}
+
diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect
new file mode 100644
index 00000000..a03810fb
--- /dev/null
+++ b/Test/triggers/regression-tests.dfy.expect
@@ -0,0 +1,3 @@
+regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on.

+

+Dafny program verifier finished with 2 verified, 0 errors