summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs80
-rw-r--r--Source/Dafny/Dafny.atg8
-rw-r--r--Source/Dafny/DafnyAst.cs5
-rw-r--r--Source/Dafny/Parser.cs6
-rw-r--r--Source/Dafny/Resolver.cs112
-rw-r--r--Source/Dafny/Translator.cs139
-rw-r--r--Test/dafny0/Answer6
-rw-r--r--Test/dafny0/SmallTests.dfy15
-rw-r--r--Test/dafny2/Answer4
-rw-r--r--Test/dafny2/MonotonicHeapstate.dfy143
-rw-r--r--Test/dafny2/runtest.bat1
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs17
12 files changed, 439 insertions, 97 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 57623068..18721cf3 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1160,11 +1160,11 @@ namespace Microsoft.Dafny {
var ind = indent + i * IndentAmount;
var bound = s.Bounds[i];
var bv = s.BoundVars[i];
- if (bound is QuantifierExpr.BoolBoundedPool) {
+ if (bound is ComprehensionExpr.BoolBoundedPool) {
Indent(ind);
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.IntBoundedPool) {
- var b = (QuantifierExpr.IntBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
SpillLetVariableDecls(b.LowerBound, ind);
SpillLetVariableDecls(b.UpperBound, ind);
Indent(ind);
@@ -1173,22 +1173,22 @@ namespace Microsoft.Dafny {
wr.Write("; @{0} < ", bv.CompileName);
TrExpr(b.UpperBound);
wr.Write("; @{0}++) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.SetBoundedPool) {
- var b = (QuantifierExpr.SetBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
SpillLetVariableDecls(b.Set, ind);
Indent(ind);
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Set);
wr.Write(").Elements) { ");
- } else if (bound is QuantifierExpr.SeqBoundedPool) {
- var b = (QuantifierExpr.SeqBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
SpillLetVariableDecls(b.Seq, ind);
Indent(ind);
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Seq);
wr.Write(").UniqueElements) { ");
- } else if (bound is QuantifierExpr.DatatypeBoundedPool) {
- var b = (QuantifierExpr.DatatypeBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
+ var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
@@ -2053,32 +2053,32 @@ namespace Microsoft.Dafny {
var bound = e.Bounds[i];
var bv = e.BoundVars[i];
// emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
- if (bound is QuantifierExpr.BoolBoundedPool) {
+ if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("Dafny.Helpers.QuantBool(");
- } else if (bound is QuantifierExpr.IntBoundedPool) {
- var b = (QuantifierExpr.IntBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantInt(");
TrExpr(b.LowerBound);
wr.Write(", ");
TrExpr(b.UpperBound);
wr.Write(", ");
- } else if (bound is QuantifierExpr.SetBoundedPool) {
- var b = (QuantifierExpr.SetBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantSet(");
TrExpr(b.Set);
wr.Write(", ");
- } else if (bound is QuantifierExpr.MapBoundedPool) {
- var b = (QuantifierExpr.MapBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.MapBoundedPool) {
+ var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantMap(");
TrExpr(b.Map);
wr.Write(", ");
- } else if (bound is QuantifierExpr.SeqBoundedPool) {
- var b = (QuantifierExpr.SeqBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantSeq(");
TrExpr(b.Seq);
wr.Write(", ");
- } else if (bound is QuantifierExpr.DatatypeBoundedPool) {
- var b = (QuantifierExpr.DatatypeBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
+ var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantDatatype(");
wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl));
@@ -2120,32 +2120,32 @@ namespace Microsoft.Dafny {
for (int i = 0; i < n; i++) {
var bound = e.Bounds[i];
var bv = e.BoundVars[i];
- if (bound is QuantifierExpr.BoolBoundedPool) {
+ if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.IntBoundedPool) {
- var b = (QuantifierExpr.IntBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("for (var @{0} = ", bv.CompileName);
TrExpr(b.LowerBound);
wr.Write("; @{0} < ", bv.CompileName);
TrExpr(b.UpperBound);
wr.Write("; @{0}++) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.SetBoundedPool) {
- var b = (QuantifierExpr.SetBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Set);
wr.Write(").Elements) { ");
- } else if (bound is QuantifierExpr.MapBoundedPool) {
- var b = (QuantifierExpr.MapBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.MapBoundedPool) {
+ var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Map);
wr.Write(").Domain) { ");
- } else if (bound is QuantifierExpr.SeqBoundedPool) {
- var b = (QuantifierExpr.SeqBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Seq);
wr.Write(").Elements) { ");
- } else if (bound is QuantifierExpr.DatatypeBoundedPool) {
- var b = (QuantifierExpr.DatatypeBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
+ var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
@@ -2189,27 +2189,27 @@ namespace Microsoft.Dafny {
Contract.Assert(e.Bounds.Count == n && n == 1);
var bound = e.Bounds[0];
var bv = e.BoundVars[0];
- if (bound is QuantifierExpr.BoolBoundedPool) {
+ if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.IntBoundedPool) {
- var b = (QuantifierExpr.IntBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("for (var @{0} = ", bv.CompileName);
TrExpr(b.LowerBound);
wr.Write("; @{0} < ", bv.CompileName);
TrExpr(b.UpperBound);
wr.Write("; @{0}++) {{ ", bv.CompileName);
- } else if (bound is QuantifierExpr.SetBoundedPool) {
- var b = (QuantifierExpr.SetBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Set);
wr.Write(").Elements) { ");
- } else if (bound is QuantifierExpr.MapBoundedPool) {
- var b = (QuantifierExpr.MapBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.MapBoundedPool) {
+ var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Map);
wr.Write(").Domain) { ");
- } else if (bound is QuantifierExpr.SeqBoundedPool) {
- var b = (QuantifierExpr.SeqBoundedPool)bound;
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Seq);
wr.Write(").Elements) { ");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ebf01c4c..d8d95079 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -17,6 +17,7 @@ COMPILER Dafny
static ModuleDecl theModule;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
+static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
@@ -849,12 +850,13 @@ UpdateStmt<out Statement/*!*/ s>
.)
.
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
-= (. IToken/*!*/ x, newToken; Expression/*!*/ e;
+= (. Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);
+ IToken/*!*/ x, newToken; Expression/*!*/ e;
List<Expression> ee = null;
Type ty = null;
CallStmt initCall = null;
List<Expression> args;
- r = null; // to please compiler
+ r = dummyRhs; // to please compiler
Attributes attrs = null;
.)
( "new" (. newToken = t; .)
@@ -899,7 +901,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
| "*" (. r = new HavocRhs(t); .)
| Expression<out e> (. r = new ExprRhs(e); .)
)
- { Attribute<ref attrs> } (. if (r != null) r.Attributes = attrs; .)
+ { Attribute<ref attrs> } (. r.Attributes = attrs; .)
.
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null; bool isGhost = false;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 98319473..1c43a530 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3490,6 +3490,11 @@ namespace Microsoft.Dafny {
public readonly Expression Set;
public SetBoundedPool(Expression set) { Set = set; }
}
+ public class SuperSetBoundedPool : BoundedPool
+ {
+ public readonly Expression LowerBound;
+ public SuperSetBoundedPool(Expression set) { LowerBound = set; }
+ }
public class MapBoundedPool : BoundedPool
{
public readonly Expression Map;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d01fe161..a81b256e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -37,6 +37,7 @@ public class Parser {
static ModuleDecl theModule;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
+static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
@@ -1638,12 +1639,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {
+ Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);
IToken/*!*/ x, newToken; Expression/*!*/ e;
List<Expression> ee = null;
Type ty = null;
CallStmt initCall = null;
List<Expression> args;
- r = null; // to please compiler
+ r = dummyRhs; // to please compiler
Attributes attrs = null;
if (la.kind == 61) {
@@ -1712,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 6) {
Attribute(ref attrs);
}
- if (r != null) r.Attributes = attrs;
+ r.Attributes = attrs;
}
void Lhs(out Expression e) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 17f35b1e..6534d2ba 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2870,7 +2870,7 @@ namespace Microsoft.Dafny
bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));
if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
- s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, missingBounds);
+ s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
bodyMustBeSpecOnly = true;
}
@@ -4198,7 +4198,7 @@ namespace Microsoft.Dafny
if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
- e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, missingBounds);
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, false, missingBounds);
if (missingBounds.Count != 0) {
// Report errors here about quantifications that depend on the allocation state.
var mb = missingBounds;
@@ -4242,7 +4242,7 @@ namespace Microsoft.Dafny
if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
- e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
e.MissingBounds = missingBounds;
foreach (var bv in e.MissingBounds) {
@@ -4278,7 +4278,7 @@ namespace Microsoft.Dafny
if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
- e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
e.MissingBounds = missingBounds;
foreach (var bv in e.MissingBounds) {
@@ -4990,34 +4990,52 @@ namespace Microsoft.Dafny
/// <summary>
/// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process
/// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds".
+ /// If "returnAllBounds" is false, then:
+ /// -- at most one BoundedPool per variable is returned
+ /// -- every IntBoundedPool returned has both a lower and an upper bound
+ /// -- no SuperSetBoundedPool is returned
+ /// If "returnAllBounds" is true, then:
+ /// -- a variable may give rise to BoundedPool's
+ /// -- IntBoundedPool bounds may have just one component
+ /// -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one
+ /// variable only has lower bounds, no upper bounds)
/// Requires "expr" to be successfully resolved.
/// </summary>
- List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, List<BoundVar> missingBounds) {
+ public static List<ComprehensionExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {
Contract.Requires(tok != null);
Contract.Requires(bvars != null);
Contract.Requires(missingBounds != null);
Contract.Requires(expr != null);
Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "expr" has been resolved
Contract.Ensures(
- (Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&
- Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count &&
+ (returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||
+ (!returnAllBounds &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>() != null &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>().Count == bvars.Count &&
Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||
- (Contract.Result<List<QuantifierExpr.BoundedPool>>() == null &&
+ (!returnAllBounds &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>() == null &&
Contract.OldValue(missingBounds.Count) < missingBounds.Count));
- var bounds = new List<QuantifierExpr.BoundedPool>();
+ var bounds = new List<ComprehensionExpr.BoundedPool>();
bool foundError = false;
for (int j = 0; j < bvars.Count; j++) {
var bv = bvars[j];
if (bv.Type is BoolType) {
// easy
- bounds.Add(new QuantifierExpr.BoolBoundedPool());
+ bounds.Add(new ComprehensionExpr.BoolBoundedPool());
} else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {
- bounds.Add(new QuantifierExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
+ bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
} else {
// Go through the conjuncts of the range expression to look for bounds.
Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
+ bool foundBoundsForBv = false;
+ if (lowerBound != null) {
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
+ lowerBound = null;
+ foundBoundsForBv = true;
+ }
foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
var c = conjunct as BinaryExpr;
if (c == null) {
@@ -5032,33 +5050,48 @@ namespace Microsoft.Dafny
switch (c.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.InSet:
if (whereIsBv == 0) {
- bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Subset:
+ if (returnAllBounds && whereIsBv == 1) {
+ bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));
+ foundBoundsForBv = true;
}
break;
case BinaryExpr.ResolvedOpcode.InMultiSet:
if (whereIsBv == 0) {
- bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
case BinaryExpr.ResolvedOpcode.InSeq:
if (whereIsBv == 0) {
- bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
case BinaryExpr.ResolvedOpcode.InMap:
if (whereIsBv == 0) {
- bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
case BinaryExpr.ResolvedOpcode.EqCommon:
if (bv.Type is IntType) {
var otherOperand = whereIsBv == 0 ? e1 : e0;
- bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ } else if (returnAllBounds && bv.Type is SetType) {
+ var otherOperand = whereIsBv == 0 ? e1 : e0;
+ bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(otherOperand));
+ foundBoundsForBv = true;
}
break;
case BinaryExpr.ResolvedOpcode.Gt:
@@ -5081,16 +5114,22 @@ namespace Microsoft.Dafny
default:
break;
}
- if (lowerBound != null && upperBound != null) {
+ if ((lowerBound != null && upperBound != null) ||
+ (returnAllBounds && (lowerBound != null || upperBound != null))) {
// we have found two halves
- bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));
- goto CHECK_NEXT_BOUND_VARIABLE;
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
+ lowerBound = null;
+ upperBound = null;
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
}
CHECK_NEXT_CONJUNCT: ;
}
- // we have checked every conjunct in the range expression and still have not discovered good bounds
- missingBounds.Add(bv); // record failing bound variable
- foundError = true;
+ if (!foundBoundsForBv) {
+ // we have checked every conjunct in the range expression and still have not discovered good bounds
+ missingBounds.Add(bv); // record failing bound variable
+ foundError = true;
+ }
}
CHECK_NEXT_BOUND_VARIABLE: ; // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)
}
@@ -5105,7 +5144,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>
- int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {
+ static int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
Contract.Requires(boundVars != null);
@@ -5229,7 +5268,7 @@ namespace Microsoft.Dafny
/// Requires "expr" to be successfully resolved.
/// Ensures that what is returned is not a ConcreteSyntaxExpression.
/// </summary>
- IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {
+ static IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {
// We consider 5 cases. To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).
// * X ==> Y is treated as a shorthand for !X || Y, and so is described by the remaining cases
// * X && Y P(_) = P(X),P(Y) and N(_) = !(X && Y)
@@ -5332,7 +5371,7 @@ namespace Microsoft.Dafny
}
}
- Expression Plus(Expression e, int n) {
+ public static Expression Plus(Expression e, int n) {
Contract.Requires(0 <= n);
var nn = new LiteralExpr(e.tok, n);
@@ -5343,12 +5382,23 @@ namespace Microsoft.Dafny
return p;
}
+ public static Expression Minus(Expression e, int n) {
+ Contract.Requires(0 <= n);
+
+ var nn = new LiteralExpr(e.tok, n);
+ nn.Type = Type.Int;
+ var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);
+ p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ p.Type = Type.Int;
+ return p;
+ }
+
/// <summary>
/// Returns the set of free variables in "expr".
/// Requires "expr" to be successfully resolved.
/// Ensures that the set returned has no aliases.
/// </summary>
- ISet<IVariable> FreeVariables(Expression expr) {
+ static ISet<IVariable> FreeVariables(Expression expr) {
Contract.Requires(expr != null);
Contract.Ensures(expr.Type != null);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2e322029..1b8a23ee 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2154,6 +2154,20 @@ namespace Microsoft.Dafny {
}
}
+ Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ if (a == Bpl.Expr.False) {
+ return b;
+ } else if (b == Bpl.Expr.False) {
+ return a;
+ } else {
+ return Bpl.Expr.Or(a, b);
+ }
+ }
+
Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -2161,6 +2175,8 @@ namespace Microsoft.Dafny {
if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
return b;
+ } else if (a == Bpl.Expr.False) {
+ return Bpl.Expr.True;
} else {
return Bpl.Expr.Imp(a, b);
}
@@ -3791,11 +3807,19 @@ namespace Microsoft.Dafny {
Contract.Assume(false); // unexpected case
}
}
- var bvs = new VariableSeq();
- var typeAntecedent = etran.TrBoundVariables(bvars, bvs);
- var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));
- var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));
- builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));
+
+ List<Tuple<List<BoundVar>, Expression>> partialGuesses = GeneratePartialGuesses(bvars, Substitute(s.Expr, null, substMap));
+ Bpl.Expr w = Bpl.Expr.False;
+ foreach (var tup in partialGuesses) {
+ var body = etran.TrExpr(tup.Item2);
+ if (tup.Item1.Count != 0) {
+ var bvs = new VariableSeq();
+ var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);
+ body = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, body));
+ }
+ w = BplOr(body, w);
+ }
+ builder.Add(Assert(s.Tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate"));
}
// End by doing the assume
builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));
@@ -4025,6 +4049,103 @@ namespace Microsoft.Dafny {
}
}
+ List<Tuple<List<BoundVar>, Expression>> GeneratePartialGuesses(List<BoundVar> bvars, Expression expression) {
+ if (bvars.Count == 0) {
+ var tup = new Tuple<List<BoundVar>, Expression>(new List<BoundVar>(), expression);
+ return new List<Tuple<List<BoundVar>, Expression>>() { tup };
+ }
+ var result = new List<Tuple<List<BoundVar>, Expression>>();
+ var x = bvars[0];
+ var otherBvars = bvars.GetRange(1, bvars.Count - 1);
+ foreach (var tup in GeneratePartialGuesses(otherBvars, expression)) {
+ // in the special case that x does not even occur in expression, we can just ignore x
+ if (!ContainsFreeVariable(tup.Item2, false, x)) {
+ result.Add(tup);
+ continue;
+ }
+ // one possible result is to quantify over all the variables
+ var vs = new List<BoundVar>() { x };
+ vs.AddRange(tup.Item1);
+ result.Add(new Tuple<List<BoundVar>, Expression>(vs, tup.Item2));
+ // other possibilities involve guessing a value for x
+ foreach (var guess in GuessWitnesses(x, tup.Item2)) {
+ var substMap = new Dictionary<IVariable, Expression>();
+ substMap.Add(x, guess);
+ result.Add(new Tuple<List<BoundVar>, Expression>(tup.Item1, Substitute(tup.Item2, null, substMap)));
+ }
+ }
+ return result;
+ }
+
+ IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {
+ Contract.Requires(x != null);
+ Contract.Requires(expr != null);
+ var lookForBounds = false;
+ if (x.Type is BoolType) {
+ var lit = new LiteralExpr(x.tok, false);
+ lit.Type = Type.Bool; // resolve here
+ yield return lit;
+ lit = new LiteralExpr(x.tok, true);
+ lit.Type = Type.Bool; // resolve here
+ yield return lit;
+ } else if (x.Type.IsRefType) {
+ var lit = new LiteralExpr(x.tok);
+ lit.Type = x.Type;
+ yield return lit;
+ } else if (x.Type.IsIndDatatype) {
+ var dt = x.Type.AsIndDatatype;
+ Expression zero = Zero(x.tok, x.Type);
+ if (zero != null) {
+ yield return zero;
+ }
+ } else if (x.Type is SetType) {
+ var empty = new SetDisplayExpr(x.tok, new List<Expression>());
+ empty.Type = x.Type;
+ yield return empty;
+ lookForBounds = true;
+ } else if (x.Type is MultiSetType) {
+ var empty = new MultiSetDisplayExpr(x.tok, new List<Expression>());
+ empty.Type = x.Type;
+ yield return empty;
+ lookForBounds = true;
+ } else if (x.Type is SeqType) {
+ var empty = new SeqDisplayExpr(x.tok, new List<Expression>());
+ empty.Type = x.Type;
+ yield return empty;
+ lookForBounds = true;
+ } else if (x.Type is IntType) {
+ var lit = new LiteralExpr(x.tok, 0);
+ lit.Type = Type.Int; // resolve here
+ yield return lit;
+ lookForBounds = true;
+ }
+ if (lookForBounds) {
+ var missingBounds = new List<BoundVar>();
+ var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds);
+ if (missingBounds.Count == 0) {
+ foreach (var bound in bounds) {
+ if (bound is ComprehensionExpr.IntBoundedPool) {
+ var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+ if (bnd.LowerBound != null) yield return bnd.LowerBound;
+ if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);
+ } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
+ var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;
+ yield return bnd.LowerBound;
+ }
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Return a zero-equivalent value for "typ", or return null (for any reason whatsoever).
+ /// </summary>
+ Expression Zero(Bpl.IToken tok, Type typ) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typ != null);
+ return null; // TODO: this can be improved
+ }
+
void TrParallelAssign(ParallelStmt s, AssignStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// The statement:
@@ -4804,12 +4925,10 @@ namespace Microsoft.Dafny {
}
static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)
- {
+ {
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
-
-
Contract.Requires(e0.Type is IntType && e1.Type is IntType);
Contract.Ensures(Contract.Result<Expression>() != null);
BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
@@ -4819,7 +4938,7 @@ namespace Microsoft.Dafny {
}
static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)
- {
+ {
Contract.Requires(tok != null);
Contract.Requires(test != null);
Contract.Requires(e0 != null);
@@ -4833,7 +4952,7 @@ namespace Microsoft.Dafny {
}
public IEnumerable<Expression> Conjuncts(Expression expr)
- {
+ {
Contract.Requires(expr != null);
Contract.Requires(expr.Type is BoolType);
Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 70527966..f9b2c66e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -286,7 +286,7 @@ SmallTests.dfy(576,10): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 68 verified, 26 errors
+Dafny program verifier finished with 70 verified, 26 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -1748,7 +1748,7 @@ SmallTests.dfy(576,10): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 68 verified, 26 errors
+Dafny program verifier finished with 70 verified, 26 errors
out.tmp.dfy(33,11): Error: index out of range
Execution trace:
(0,0): anon0
@@ -1893,7 +1893,7 @@ out.tmp.dfy(522,10): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 68 verified, 26 errors
+Dafny program verifier finished with 70 verified, 26 errors
-------------------- LetExpr.dfy --------------------
LetExpr.dfy(5,12): Error: assertion violation
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index e74a9943..7b409a67 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -521,9 +521,9 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
ensures x == a && y == b;
{
if (*) {
- x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;
+ x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;
} else {
- var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;
+ var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;
x, y := xx, yy;
}
}
@@ -532,10 +532,10 @@ method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)
{
var k :| assume 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
assert b < a;
- k :| assume k == old(2*k); // note, the 'old' has no effect on local variables like k
+ k :| k == old(2*k); // note, the 'old' has no effect on local variables like k
assert k == 0;
var S := {2, 4, 7};
- var T :| assume T <= S;
+ var T :| T <= S;
assert 3 !in T;
assert T == {}; // error: T may be larger
}
@@ -572,7 +572,7 @@ method AssignSuchThat4()
method AssignSuchThat5()
{
var n := new Node;
- n :| assume fresh(n); // fine
+ n :| fresh(n); // fine
assert false; // error
}
@@ -582,3 +582,8 @@ method AssignSuchThat6()
n :| assume n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;'
assert false; // no problemo
}
+
+method AssignSuchThat7<T>(A: set<T>, x: T) {
+ var B :| A <= B;
+ assert x in A ==> x in B;
+}
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index f466d813..447f4365 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -50,3 +50,7 @@ Dafny program verifier finished with 11 verified, 0 errors
-------------------- SegmentSum.dfy --------------------
Dafny program verifier finished with 3 verified, 0 errors
+
+-------------------- MonotonicHeapstate.dfy --------------------
+
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
new file mode 100644
index 00000000..4844086e
--- /dev/null
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -0,0 +1,143 @@
+module M0 {
+ datatype Kind = Constant | Ident | Binary;
+
+ class Expr {
+ var kind: Kind;
+ var value: int; // value if kind==Constant; id if kind==VarDecl; operator if kind==Binary
+ var left: Expr; // if kind==Binary
+ var right: Expr; // if kind==Binary
+
+ ghost var Repr: set<object>;
+
+ predicate Valid()
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ (left != null ==> left in Repr && this !in left.Repr && right !in left.Repr && left.Repr <= Repr && left.Valid()) &&
+ (right != null ==> right in Repr && this !in right.Repr && left !in right.Repr && right.Repr <= Repr && right.Valid()) &&
+ (kind == Binary ==> left != null && right != null && left.Repr !! right.Repr)
+ }
+
+ constructor CreateConstant(x: int)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ {
+ kind, value := Constant, x;
+ left, right := null, null;
+ Repr := {this};
+ }
+
+ constructor CreateIdent(name: int)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ {
+ kind, value := Ident, name;
+ left, right := null, null;
+ Repr := {this};
+ }
+
+ constructor CreateBinary(op: int, left: Expr, right: Expr)
+ requires left != null && left.Valid() && this !in left.Repr;
+ requires right != null && right.Valid() && this !in right.Repr;
+ requires left.Repr !! right.Repr;
+ modifies this;
+ ensures Valid() && fresh(Repr - {this} - left.Repr - right.Repr);
+ {
+ kind, value := Binary, op;
+ this.left, this.right := left, right;
+ Repr := {this} + left.Repr + right.Repr;
+ }
+ }
+}
+
+// Introduce the idea of resolved
+module M1 refines M0 {
+ class Expr {
+ ghost var resolved: bool;
+
+ predicate Valid()
+ {
+ resolved ==>
+ (kind == Binary ==> left.resolved && right.resolved)
+ }
+
+ constructor CreateConstant...
+ {
+ resolved := false;
+ }
+
+ constructor CreateIdent...
+ {
+ resolved := false;
+ }
+
+ constructor CreateBinary...
+ {
+ resolved := false;
+ }
+
+ method Resolve()
+ requires Valid(); // it's okay if it's already resolved
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures resolved;
+ decreases Repr;
+ {
+ if (kind == Binary) {
+ left.Resolve();
+ right.Resolve();
+ }
+ Repr := Repr + (if left != null then left.Repr else {}) + (if right != null then right.Repr else {});
+ resolved := true;
+ }
+ }
+}
+
+// Give "resolved" some meaning
+module M2 refines M1 {
+ class VarDecl {
+ }
+
+ class Expr {
+ var decl: VarDecl; // if kind==Ident, filled in during resolution
+
+ predicate Valid()
+ {
+ resolved ==>
+ (kind == Ident ==> decl != null)
+ }
+
+ method Resolve...
+ {
+ if (kind == Ident) {
+ decl := new VarDecl;
+ }
+ }
+ }
+}
+
+// Finally, supposing each VarDecl has a value, evaluate a resolved expression
+module M3 refines M2 {
+ class VarDecl {
+ var val: int;
+ }
+
+ class Expr {
+ method Eval() returns (r: int)
+ requires Valid();
+ requires resolved;
+ decreases Repr;
+ {
+ match (kind) {
+ case Constant =>
+ r := value;
+ case Ident =>
+ r := decl.val; // note how this statement relies on "decl" being non-null, which follows from the expression being resolved
+ case Binary =>
+ var x := left.Eval();
+ var y := right.Eval();
+ r := x + y;
+ }
+ }
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 25dbed54..909f67f5 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,6 +16,7 @@ for %%f in (
StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
+ MonotonicHeapstate.dfy
) do (
echo.
echo -------------------- %%f --------------------
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 3298be4b..b7b2cd6d 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -39,9 +39,11 @@ namespace DafnyLanguage
static void Initialize() {
if (Dafny.DafnyOptions.O == null) {
- Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
- Dafny.DafnyOptions.O.DafnyPrelude = "c:\\boogie\\Binaries\\DafnyPrelude.bpl";
- Dafny.DafnyOptions.O.ApplyDefaultOptions();
+ var options = new Dafny.DafnyOptions();
+ options.ProverKillTime = 10;
+ options.ErrorTrace = 0;
+ options.ApplyDefaultOptions();
+ Dafny.DafnyOptions.Install(options);
}
}
@@ -388,12 +390,21 @@ namespace DafnyLanguage
Contract.Requires(msg != null);
Tok = tok;
Msg = CleanUp(msg);
+ AddNestingsAsAux(tok);
}
public void AddAuxInfo(Bpl.IToken tok, string msg) {
Contract.Requires(tok != null);
Contract.Requires(1 <= tok.line && 1 <= tok.col);
Contract.Requires(msg != null);
Aux.Add(new DafnyErrorAuxInfo(tok, msg));
+ AddNestingsAsAux(tok);
+ }
+ void AddNestingsAsAux(Bpl.IToken tok) {
+ while (tok is Dafny.NestedToken) {
+ var nt = (Dafny.NestedToken)tok;
+ tok = nt.Inner;
+ Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));
+ }
}
public void AddAuxInfo(Bpl.QKeyValue attr) {
while (attr != null) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 21:27:52 +0000