From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 13:16:15 -0700 Subject: Changed computation of ghosts until pass 2 of resolution. Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions. --- Test/dafny0/NonGhostQuantifiers.dfy.expect | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'Test/dafny0/NonGhostQuantifiers.dfy.expect') diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect index 1e2fce17..6b737add 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect @@ -6,16 +6,16 @@ NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function defin NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c' -NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce 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 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 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 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 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 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 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 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 a bounded set of values for 'x' +NonGhostQuantifiers.dfy(192,13): 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 'c' +NonGhostQuantifiers.dfy(16,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 'n' +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 -- cgit v1.2.3 From 461d6b17aed0bd81adc86d4ce2148c0f1d790bbc Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 29 Oct 2015 16:08:48 -0700 Subject: Fix issue 91 - Change how we compute the bounds of quantified variables so that it does not depend on the order they appeared. --- Source/Dafny/Resolver.cs | 42 ++++++++++++++++------- Test/dafny0/NonGhostQuantifiers.dfy.expect | 6 +--- Test/dafny4/Bug91.dfy | 53 ++++++++++++++++++++++++++++++ Test/dafny4/Bug91.dfy.expect | 2 ++ 4 files changed, 87 insertions(+), 16 deletions(-) create mode 100644 Test/dafny4/Bug91.dfy create mode 100644 Test/dafny4/Bug91.dfy.expect (limited to 'Test/dafny0/NonGhostQuantifiers.dfy.expect') 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 knownBounds = null; + var orgCount = bvars.Count; + var bests = new List(); + 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(); for (var i = 0; i < bvars.Count; i++) { if (bests[i] == null) { @@ -9728,24 +9748,24 @@ namespace Microsoft.Dafny public static List DiscoverAllBounds_SingleVar(VT v, Expression expr) where VT : IVariable { expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr); - return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true); + return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true, null); } - private static List>> DiscoverAllBounds_Aux_MultipleVars(List bvars, Expression expr, bool polarity) where VT : IVariable { + private static List>> DiscoverAllBounds_Aux_MultipleVars(List bvars, Expression expr, bool polarity, List knownBounds) where VT : IVariable { Contract.Requires(bvars != null); Contract.Requires(expr != null); var bb = new List>>(); 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>(bvars[j], bounds)); } return bb; } /// - /// 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. /// - private static List DiscoverAllBounds_Aux_SingleVar(List bvars, int j, Expression expr, bool polarity) where VT : IVariable { + private static List DiscoverAllBounds_Aux_SingleVar(List bvars, int j, Expression expr, bool polarity, List 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. /// - static int SanitizeForBoundDiscovery(List boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) where VT : IVariable { + static int SanitizeForBoundDiscovery(List boundVars, int bvi, BinaryExpr.ResolvedOpcode op, List 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> + +function UnAckedMessages(s:SendState) : set +{ + 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 +{ + set m | UnAckedMessage2(s, m) :: m +} +*/ + +function UnAckedMessagesForDst(s:SendState, dst:int) : set + requires dst in s; +{ + set m | m in s[dst] :: m +} + +function UnAckedMessages3(s:SendState) : set +{ + set m,dst | dst in s && m in UnAckedMessagesForDst(s, dst) :: m +} + +function SeqToSet(s:seq) : set +{ + set i | i in s +} +/* does not verify, with element may not in domain error +function UnAckedMessages4(s:SendState) : set +{ + set m,dst | m in SeqToSet(s[dst]) && dst in s :: m +} +*/ + +function UnAckedLists(s:SendState) : set> +{ + set dst | dst in s :: s[dst] +} + +function UnAckedMessages5(s:SendState) : set +{ + 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 -- cgit v1.2.3