Fix issue 91 - Change how we compute the bounds of quantified variables so that

it does not depend on the order they appeared.

4 files changed, 87 insertions, 16 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 74ff60e7..21476ede 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -9715,8 +9715,28 @@ namespace Microsoft.Dafny
         var c = GetImpliedTypeConstraint(bv, bv.Type, null);

         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);

       }

-      var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);

-      var bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));

+      List<ComprehensionExpr.BoundedPool> knownBounds = null;

+      var orgCount = bvars.Count;

+      var bests = new List<ComprehensionExpr.BoundedPool>();

+      bool changed = true;

+      // compute the bounds of the BV until no new information is obtained.

+      while (changed) {

+        changed = false;

+        var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity, knownBounds);

+        bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));

+        // check to see if we found new bounds in this iteration

+        int count = 0;

+        for (int i = 0; i < bests.Count; i++) {

+          if (bests[i] == null) {

+            count++;

+          }

+        }

+        if (count >0 && count != orgCount) {

+          changed = true;

+          knownBounds = bests;

+          orgCount = count;

+        }

+      }

       missingBounds = new List<VT>();

       for (var i = 0; i < bvars.Count; i++) {

         if (bests[i] == null) {

@@ -9728,24 +9748,24 @@ namespace Microsoft.Dafny
 

     public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {

       expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr);

-      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);

+      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true, null);

     }

 

-    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity) where VT : IVariable {

+    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {

       Contract.Requires(bvars != null);

       Contract.Requires(expr != null);

       var bb = new List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>();

       for (var j = 0; j < bvars.Count; j++) {

-        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity);

+        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds);

         bb.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bvars[j], bounds));

       }

       return bb;

     }

 

     /// <summary>

-    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]".

+    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]" that is not bounded.

     /// </summary>

-    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity) where VT : IVariable {

+    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {

       Contract.Requires(bvars != null);

       Contract.Requires(0 <= j && j < bvars.Count);

       Contract.Requires(expr != null);

@@ -9774,7 +9794,7 @@ namespace Microsoft.Dafny
         }

         var e0 = c.E0;

         var e1 = c.E1;

-        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

+        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, knownBounds, ref e0, ref e1);

         if (whereIsBv < 0) {

           continue;

         }

@@ -9870,7 +9890,7 @@ namespace Microsoft.Dafny
     /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".

     /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.

     /// </summary>

-    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) where VT : IVariable {

+    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, List<ComprehensionExpr.BoundedPool> knownBounds, ref Expression e0, ref Expression e1) where VT : IVariable {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(boundVars != null);

@@ -9965,10 +9985,10 @@ namespace Microsoft.Dafny
       }

 

       // Finally, check that the other side does not contain "bv" or any of the bound variables

-      // listed after "bv" in the quantifier.

+      // listed after "bv" in the quantifier that is not bounded.

       var fv = FreeVariables(thatSide);

       for (int i = bvi; i < boundVars.Count; i++) {

-        if (fv.Contains(boundVars[i])) {

+        if (fv.Contains(boundVars[i]) && (knownBounds == null || knownBounds[i] == null)) {

           return -1;

         }

       }

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect
index 6b737add..0abf0b6c 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy.expect
+++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect
@@ -11,11 +11,7 @@ NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'

 NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'd'

 NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'

 NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y'

 NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x'

 NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in NonGhostQuantifiers.dfy

+16 resolution/type errors detected in NonGhostQuantifiers.dfy

diff --git a/Test/dafny4/Bug91.dfy b/Test/dafny4/Bug91.dfy
new file mode 100644
index 00000000..75f8de22
--- /dev/null
+++ b/Test/dafny4/Bug91.dfy
@@ -0,0 +1,53 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+type SendState = map<int, seq<int>>

+

+function UnAckedMessages(s:SendState) : set<int>

+{

+    set m,dst | dst in s && m in s[dst] :: m

+}

+

+predicate UnAckedMessage2(s:SendState, m:int)

+{

+    exists dst :: dst in s && m in s[dst]

+}

+

+/* the following bound can't be determined since we only know what to do with binary operations

+function UnAckedMessagesA(s:SendState) : set<int>

+{

+    set m | UnAckedMessage2(s, m) :: m

+}

+*/

+

+function UnAckedMessagesForDst(s:SendState, dst:int) : set<int>

+    requires dst in s;

+{

+    set m | m in s[dst] :: m

+}

+

+function UnAckedMessages3(s:SendState) : set<int>

+{

+    set m,dst | dst in s && m in UnAckedMessagesForDst(s, dst) :: m

+}

+

+function SeqToSet<T>(s:seq<T>) : set<T>

+{

+    set i | i in s 

+}

+/* does not verify, with element may not in domain error

+function UnAckedMessages4(s:SendState) : set<int>

+{

+    set m,dst | m in SeqToSet(s[dst]) && dst in s :: m

+}

+*/

+

+function UnAckedLists(s:SendState) : set<seq<int>>

+{

+    set dst | dst in s :: s[dst]

+}

+

+function UnAckedMessages5(s:SendState) : set<int>

+{

+    set m, list | list in UnAckedLists(s) && m in list :: m

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug91.dfy.expect b/Test/dafny4/Bug91.dfy.expect
new file mode 100644
index 00000000..76f19e0d
--- /dev/null
+++ b/Test/dafny4/Bug91.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 7 verified, 0 errors