diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 13 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 3 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 41 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 234 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 485 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 25 | ||||
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 117 |
11 files changed, 845 insertions, 96 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ca526173..572a1e29 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -603,6 +603,19 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
// ---------------------------------------------------------------
+// -- Useful macros ----------------------------------------------
+// ---------------------------------------------------------------
+
+// havoc $Heap \ {this} \ S
+procedure {:inline} $YieldHavoc(this: ref, S: Set BoxType);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
+ $o == this ||
+ S[$Box($o)]);
+
+// ---------------------------------------------------------------
// -- Non-determinism --------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 408e9797..095534e6 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -113,7 +113,7 @@ namespace Microsoft.Dafny if (member is Field) {
Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
- return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
+ return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
} else if (member is Function) {
var f = (Function)member;
return CloneFunction(f);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index dcc9a3ca..bc972495 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -437,7 +437,8 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> [ BlockStmt<out body, out bodyStart, out bodyEnd>
]
(. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
- new Specification<FrameExpression>(mod, modAttrs), new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
req, ens, yieldReq, yieldEns,
body, attrs, signatureOmitted);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 012619ee..6b056200 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -73,7 +73,7 @@ namespace Microsoft.Dafny { for (int d = 0; d < dims; d++) {
string name = dims == 1 ? "Length" : "Length" + d;
string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";
- Field len = new SpecialField(Token.NoToken, name, compiledName, "new BigInteger(", ")", false, false, Type.Int, null);
+ Field len = new SpecialField(Token.NoToken, name, compiledName, "new BigInteger(", ")", false, false, false, Type.Int, null);
len.EnclosingClass = arrayClass; // resolve here
arrayClass.Members.Add(len);
}
@@ -898,7 +898,7 @@ namespace Microsoft.Dafny { public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base)
public readonly List<TopLevelDecl/*!*/> TopLevelDecls = new List<TopLevelDecl/*!*/>(); // filled in by the parser; readonly after that
- public readonly Graph<ICallable/*!*/> CallGraph = new Graph<ICallable/*!*/>(); // filled in during resolution
+ public readonly Graph<MemberDecl/*!*/> CallGraph = new Graph<MemberDecl/*!*/>(); // filled in during resolution
public int Height; // height in the topological sorting of modules; filled in during resolution
public readonly bool IsGhost;
public readonly bool IsAbstract; // True iff this module represents an abstract interface
@@ -1153,7 +1153,9 @@ namespace Microsoft.Dafny { List<TypeParameter> TypeArgs { get; }
List<Formal> Ins { get ; }
List<Formal> Outs { get; }
+ Specification<FrameExpression> Modifies { get; }
ModuleDefinition EnclosingModule { get; } // to be called only after signature-resolution is complete
+ bool MustReverify { get; }
}
public class IteratorDecl : ClassDecl, ICodeContext
@@ -1161,6 +1163,7 @@ namespace Microsoft.Dafny { public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
public readonly List<Formal> OutsHistory; // these are the 'xs' variables
+ public readonly List<Formal> ExtraVars; // _reads, _modifies, _new
public readonly Specification<FrameExpression> Reads;
public readonly Specification<FrameExpression> Modifies;
public readonly Specification<Expression> Decreases;
@@ -1170,6 +1173,9 @@ namespace Microsoft.Dafny { public readonly List<MaybeFreeExpression> YieldEnsures;
public readonly BlockStmt Body;
public readonly bool SignatureIsOmitted;
+ public Constructor Member_Init; // created during registration phase of resolution; its specification is filled in during resolution
+ public Predicate Member_Valid; // created during registration phase of resolution; its specification is filled in during resolution
+ public Method Member_MoveNext; // created during registration phase of resolution; its specification is filled in during resolution
public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,
List<Formal> ins, List<Formal> outs,
Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,
@@ -1207,8 +1213,16 @@ namespace Microsoft.Dafny { OutsHistory = new List<Formal>();
foreach (var p in Outs) {
- OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(p.Type), false, true));
+ var tp = p.Type;
+ if (tp.IsSubrangeType) {
+ tp = new IntType(); // because SeqType(NatType) is now allowed (despite the fact that the history variable is readonly, which is unfortunate)
+ }
+ OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(tp), false, true));
}
+ ExtraVars = new List<Formal>();
+ ExtraVars.Add(new Formal(tok, "_reads", new SetType(new ObjectType()), true, true));
+ ExtraVars.Add(new Formal(tok, "_modifies", new SetType(new ObjectType()), true, true));
+ ExtraVars.Add(new Formal(tok, "_new", new SetType(new ObjectType()), false, true));
}
bool ICodeContext.IsGhost { get { return false; } }
@@ -1216,7 +1230,9 @@ namespace Microsoft.Dafny { List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List<Formal> ICodeContext.Ins { get { return this.Ins; } }
List<Formal> ICodeContext.Outs { get { return this.Outs; } }
+ Specification<FrameExpression> ICodeContext.Modifies { get { return this.Modifies; } }
ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }
+ bool ICodeContext.MustReverify { get { return false; } }
}
/// <summary>
@@ -1273,26 +1289,30 @@ namespace Microsoft.Dafny { }
public class Field : MemberDecl {
- public readonly bool IsMutable;
+ public readonly bool IsMutable; // says whether or not the field can ever change values
+ public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
public readonly Type Type;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Type != null);
+ Contract.Invariant(!IsUserMutable || IsMutable); // IsUserMutable ==> IsMutable
}
public Field(IToken tok, string name, bool isGhost, Type type, Attributes attributes)
- : this(tok, name, isGhost, true, type, attributes) {
+ : this(tok, name, isGhost, true, true, type, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
}
- public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)
+ public Field(IToken tok, string name, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
: base(tok, name, false, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
+ Contract.Requires(!isUserMutable || isMutable);
IsMutable = isMutable;
+ IsUserMutable = isUserMutable;
Type = type;
}
}
@@ -1302,13 +1322,14 @@ namespace Microsoft.Dafny { public readonly string CompiledName;
public readonly string PreString;
public readonly string PostString;
- public SpecialField(IToken tok, string name, string compiledName, string preString, string postString, bool isGhost, bool isMutable, Type type, Attributes attributes)
- : base(tok, name, isGhost, isMutable, type, attributes) {
+ public SpecialField(IToken tok, string name, string compiledName, string preString, string postString, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
+ : base(tok, name, isGhost, isMutable, isUserMutable, type, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(compiledName != null);
Contract.Requires(preString != null);
Contract.Requires(postString != null);
+ Contract.Requires(!isUserMutable || isMutable);
Contract.Requires(type != null);
CompiledName = compiledName;
@@ -1323,7 +1344,7 @@ namespace Microsoft.Dafny { public readonly Formal CorrespondingFormal;
public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal correspondingFormal, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)
- : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)
+ : base(tok, name, compiledName, preString, postString, isGhost, false, false, type, attributes)
{
Contract.Requires(tok != null);
Contract.Requires(enclosingCtor != null);
@@ -1736,12 +1757,14 @@ namespace Microsoft.Dafny { List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List<Formal> ICodeContext.Ins { get { return this.Ins; } }
List<Formal> ICodeContext.Outs { get { return this.Outs; } }
+ Specification<FrameExpression> ICodeContext.Modifies { get { return Mod; } }
ModuleDefinition ICodeContext.EnclosingModule {
get {
Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete
return this.EnclosingClass.Module;
}
}
+ bool ICodeContext.MustReverify { get { return this.MustReverify; } }
}
public class Constructor : Method
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6b4be0eb..9331775f 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -499,7 +499,8 @@ bool IsAttribute() { BlockStmt(out body, out bodyStart, out bodyEnd);
}
iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
- new Specification<FrameExpression>(mod, modAttrs), new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
req, ens, yieldReq, yieldEns,
body, attrs, signatureOmitted);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1e2424ed..fe602f86 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -269,7 +269,15 @@ namespace Microsoft.Dafny { PrintAttributes(field.Attributes);
wr.Write(" {0}: ", field.Name);
PrintType(field.Type);
- wr.WriteLine(";");
+ wr.Write(";");
+ if (field.IsUserMutable) {
+ // nothing more to say
+ } else if (field.IsMutable) {
+ wr.Write(" // may change, but not directly by program");
+ } else {
+ wr.Write(" // immutable");
+ }
+ wr.WriteLine();
}
public void PrintFunction(Function f, int indent) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1fd828a0..bde3afb1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5,6 +5,7 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
+using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie;
@@ -277,8 +278,9 @@ namespace Microsoft.Dafny var datatypeDependencies = new Graph<IndDatatypeDecl>();
int prevErrorCount = ErrorCount;
ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies);
- if (ErrorCount == prevErrorCount)
+ if (ErrorCount == prevErrorCount) {
ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ }
}
@@ -508,7 +510,7 @@ namespace Microsoft.Dafny if (members.ContainsKey(p.Name)) {
Error(p, "Name of in-parameter is used by another member of the iterator: {0}", p.Name);
} else {
- var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);
+ var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, false, p.Type, null);
field.EnclosingClass = iter; // resolve here
members.Add(p.Name, field);
iter.Members.Add(field);
@@ -518,7 +520,7 @@ namespace Microsoft.Dafny if (members.ContainsKey(p.Name)) {
Error(p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name);
} else {
- var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);
+ var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, false, p.Type, null);
field.EnclosingClass = iter; // resolve here
members.Add(p.Name, field);
iter.Members.Add(field);
@@ -529,7 +531,7 @@ namespace Microsoft.Dafny if (members.ContainsKey(p.Name)) {
Error(p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name);
} else {
- var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, p.Type, null);
+ var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", true, true, false, p.Type, null);
field.EnclosingClass = iter; // resolve here
yieldHistoryVariables.Add(field); // just record this field for now (until all parameters have been added as members)
}
@@ -539,37 +541,48 @@ namespace Microsoft.Dafny members.Add(f.Name, f);
iter.Members.Add(f);
});
+ // finally, add the additional special variables as fields
+ foreach (var p in iter.ExtraVars) {
+ var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, !p.InParam, false, p.Type, null);
+ field.EnclosingClass = iter; // resolve here
+ members.Add(field.Name, field);
+ iter.Members.Add(field);
+ }
// Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list. What that is
// saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the
// iterator type) does.
- // Also add "Valid" and "MoveNext"
+ // --- here comes the constructor
var init = new Constructor(iter.tok, iter.Name, new List<TypeParameter>(), iter.Ins,
- /* TODO: Fill in the spec here */
new List<MaybeFreeExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<MaybeFreeExpression>(),
new Specification<Expression>(new List<Expression>(), null),
null, null, false);
+ // --- here comes predicate Valid()
var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(), iter.tok,
new List<Formal>(),
new List<Expression>(),
- new List<FrameExpression>()/*TODO: does this need to be filled?*/,
+ new List<FrameExpression>(),
new List<Expression>(),
new Specification<Expression>(new List<Expression>(), null),
- null/*TODO: does this need to be fileld?*/, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
+ null, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
+ // --- here comes method MoveNext
var moveNext = new Method(iter.tok, "MoveNext", false, false, new List<TypeParameter>(),
new List<Formal>(), new List<Formal>() { new Formal(iter.tok, "more", Type.Bool, false, false) },
- /* TODO: Do the first 3 of the specification components on the next line need to be filled in? */
new List<MaybeFreeExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<MaybeFreeExpression>(),
new Specification<Expression>(new List<Expression>(), null),
null, null, false);
+ // add these implicit members to the class
init.EnclosingClass = iter;
valid.EnclosingClass = iter;
moveNext.EnclosingClass = iter;
iter.HasConstructor = true;
+ iter.Member_Init = init;
+ iter.Member_Valid = valid;
+ iter.Member_MoveNext = moveNext;
MemberDecl member;
if (members.TryGetValue(init.Name, out member)) {
Error(member.tok, "member name '{0}' is already predefined for this iterator", init.Name);
@@ -639,7 +652,7 @@ namespace Microsoft.Dafny // create and add the query "method" (field, really)
string queryName = ctor.Name + "?";
- var query = new SpecialField(ctor.tok, queryName, "is_" + ctor.CompileName, "", "", false, false, Type.Bool, null);
+ var query = new SpecialField(ctor.tok, queryName, "is_" + ctor.CompileName, "", "", false, false, false, Type.Bool, null);
query.EnclosingClass = dt; // resolve here
members.Add(queryName, query);
ctor.QueryField = query;
@@ -743,8 +756,9 @@ namespace Microsoft.Dafny }
MemberDecl CloneMember(MemberDecl member) {
if (member is Field) {
+ Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
- return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
+ return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), null);
} else if (member is Function) {
var f = (Function)member;
return CloneFunction(f.tok, f, f.IsGhost);
@@ -1063,9 +1077,12 @@ namespace Microsoft.Dafny ResolveTypeParameters(iter.TypeArgs, false, iter);
ResolveIterator(iter);
allTypeParameters.PopMarker();
+ ResolveClassMemberBodies(iter); // resolve the automatically generated members
} else if (d is ClassDecl) {
- ResolveClassMemberBodies((ClassDecl)d);
+ var cl = (ClassDecl)d;
+ ResolveAttributes(cl.Attributes, false);
+ ResolveClassMemberBodies(cl);
}
allTypeParameters.PopMarker();
}
@@ -1961,7 +1978,6 @@ namespace Microsoft.Dafny Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
- ResolveAttributes(cl.Attributes, false);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
if (member is Field) {
@@ -2511,6 +2527,8 @@ namespace Microsoft.Dafny void ResolveIterator(IteratorDecl iter) {
Contract.Requires(iter != null);
+ var initialErrorCount = ErrorCount;
+
// Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
scope.PushMarker();
scope.AllowInstance = false; // disallow 'this' from use, which means that the special fields and methods added are not accessible in the syntactically given spec
@@ -2523,11 +2541,6 @@ namespace Microsoft.Dafny foreach (FrameExpression fe in iter.Modifies.Expressions) {
ResolveFrameExpression(fe, "modifies");
}
- foreach (Expression e in iter.Decreases.Expressions) {
- ResolveExpression(e, false);
- // any type is fine
- }
-
foreach (MaybeFreeExpression e in iter.Requires) {
ResolveExpression(e.E, false);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
@@ -2535,10 +2548,21 @@ namespace Microsoft.Dafny Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
+ foreach (Expression e in iter.Decreases.Expressions) {
+ ResolveExpression(e, false);
+ // any type is fine
+ }
- // In the postcondition, the yield-history variables are also in scope
+ // Now add the yield-history variables to the scope
iter.OutsHistory.ForEach(p => scope.Push(p.Name, p));
+ foreach (MaybeFreeExpression e in iter.YieldRequires) {
+ ResolveExpression(e.E, false);
+ Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E.Type, Type.Bool)) {
+ Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
+ }
+ }
foreach (MaybeFreeExpression e in iter.Ensures) {
ResolveExpression(e.E, true);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
@@ -2547,20 +2571,13 @@ namespace Microsoft.Dafny }
}
- // For the attributes, yield precondition, yield postcondition, and body, the yield-parameters are also available
+ // Finally, add the yield-parameters and extra variables to the scope
scope.PushMarker(); // make the yield-parameters appear in the same scope as the outer-most locals of the body (since this is what is done for methods)
iter.Outs.ForEach(p => scope.Push(p.Name, p));
+ iter.ExtraVars.ForEach(p => scope.Push(p.Name, p));
ResolveAttributes(iter.Attributes, false);
- foreach (MaybeFreeExpression e in iter.YieldRequires) {
- ResolveExpression(e.E, false);
- Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
- }
- }
-
foreach (MaybeFreeExpression e in iter.YieldEnsures) {
ResolveExpression(e.E, true);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
@@ -2569,13 +2586,161 @@ namespace Microsoft.Dafny }
}
+ var postSpecErrorCount = ErrorCount;
+
// Resolve body
if (iter.Body != null) {
ResolveBlockStatement(iter.Body, false, iter);
}
- scope.PopMarker(); // for the yield-parameters and outermost-level locals
+ scope.PopMarker(); // for the yield-parameters, extra variables, and outermost-level locals
scope.PopMarker(); // for the in-parameters and yield-history variables
+
+ if (postSpecErrorCount == initialErrorCount) {
+ CreateIteratorMethodSpecs(iter);
+ }
+ }
+
+ /// <summary>
+ /// Assumes the specification of the iterator itself has been successfully resolved.
+ /// </summary>
+ void CreateIteratorMethodSpecs(IteratorDecl iter) {
+ if (iter.Outs.Count != iter.OutsHistory.Count) {
+ // something must have gone wrong during registration, so don't worry about filling in the specs
+ return;
+ }
+
+ // ---------- here comes the constructor ----------
+ // same requires clause as the iterator itself
+ iter.Member_Init.Req.AddRange(iter.Requires);
+ // modifies this;
+ iter.Member_Init.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));
+ var ens = iter.Member_Init.Ens;
+ foreach (var p in iter.Ins) {
+ // ensures this.x == x;
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,
+ new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new IdentifierExpr(p.tok, p.Name))));
+ }
+ foreach (var p in iter.OutsHistory) {
+ // ensures this.ys == [];
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,
+ new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List<Expression>()))));
+ }
+ // ensures this.Valid();
+ ens.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>())));
+ // ensures this._reads == old(ReadsClause);
+ var modSetSingletons = new List<Expression>();
+ Expression frameSet = new SetDisplayExpr(iter.tok, modSetSingletons);
+ foreach (var fr in iter.Reads.Expressions) {
+ if (fr.FieldName != null) {
+ Error(fr.tok, "sorry, a reads clause for an iterator is not allowed to designate specific fields");
+ } else if (fr.E.Type.IsRefType) {
+ modSetSingletons.Add(fr.E);
+ } else {
+ frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E);
+ }
+ }
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
+ new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"),
+ new OldExpr(iter.tok, frameSet))));
+ // ensures this._modifies == old(ModifiesClause);
+ modSetSingletons = new List<Expression>();
+ frameSet = new SetDisplayExpr(iter.tok, modSetSingletons);
+ foreach (var fr in iter.Modifies.Expressions) {
+ if (fr.FieldName != null) {
+ Error(fr.tok, "sorry, a modifies clause for an iterator is not allowed to designate specific fields");
+ } else if (fr.E.Type.IsRefType) {
+ modSetSingletons.Add(fr.E);
+ } else {
+ frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E);
+ }
+ }
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
+ new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"),
+ new OldExpr(iter.tok, frameSet))));
+ // ensures this._new == {};
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
+ new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
+ new SetDisplayExpr(iter.tok, new List<Expression>()))));
+
+ // ---------- here comes predicate Valid() ----------
+ var reads = iter.Member_Valid.Reads;
+ reads.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); // reads this;
+ reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"), null)); // reads this._reads;
+ reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // reads this._new;
+
+ // ---------- here comes method MoveNext() ----------
+ // Build a substitution from the formals/variables to the corresponding fields. Note, because these substitutions
+ // will be applied to an already resolved expression, the recursive idempotent Resolve operation on these method
+ // specifications may not reach down to these new parts. Hence, these must be resolved right away (and they had better
+ // produce the same types as the subexpression they are replacing).
+ var substMap = new Dictionary<IVariable, Expression>();
+ foreach (var p in iter.Ins.Concat(iter.Outs.Concat(iter.OutsHistory.Concat(iter.ExtraVars)))) {
+ var f = (Field)iter.Members.Find(member => member is Field && member.Name == p.Name);
+ if (f == null) {
+ // something must have gone wrong during registration, so don't worry about adding this parameter to the substitution map
+ } else {
+ var th = new ThisExpr(p.tok);
+ th.Type = GetThisType(p.tok, iter); // resolve here
+ var pe = new FieldSelectExpr(p.tok, th, p.Name);
+ pe.Field = f; pe.Type = p.Type; // resolve here
+ substMap.Add(p, pe);
+ }
+ }
+ var subst = new Translator.Substituter(null, substMap);
+ // requires this.Valid();
+ var req = iter.Member_MoveNext.Req;
+ req.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>())));
+ // requires YieldRequires[subst];
+ foreach (var yp in iter.YieldRequires) {
+ req.Add(new MaybeFreeExpression(subst.Substitute(yp.E), yp.IsFree, subst.SubstAttributes(yp.Attributes)));
+ }
+ // modifies this, this._modifies, this._new;
+ iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));
+ iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null));
+ iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));
+ // ensures more ==> this.Valid();
+ ens = iter.Member_MoveNext.Ens;
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
+ new IdentifierExpr(iter.tok, "more"),
+ new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>()))));
+ // ensures fresh(_new - old(_new));
+ ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok,
+ new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,
+ new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
+ new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
+ // ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys);
+ Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count);
+ for (int i = 0; i < iter.Outs.Count; i++) {
+ var y = iter.Outs[i];
+ var ys = iter.OutsHistory[i];
+ var ite = new ITEExpr(iter.tok, new IdentifierExpr(iter.tok, "more"),
+ new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add,
+ new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
+ new SeqDisplayExpr(iter.tok, new List<Expression>() { new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })),
+ new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
+ var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite);
+ ens.Add(new MaybeFreeExpression(eq));
+ }
+ // ensures more ==> YieldEnsures[subst];
+ foreach (var ye in iter.YieldEnsures) {
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
+ new IdentifierExpr(iter.tok, "more"), subst.Substitute(ye.E)),
+ ye.IsFree));
+ }
+ // ensures !more ==> Ensures[subst];
+ foreach (var e in iter.Ensures) {
+ ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
+ new UnaryExpr(iter.tok, UnaryExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")),
+ subst.Substitute(e.E)),
+ e.IsFree));
+ }
+ // decreases DecreasesClause[subst];
+ foreach (var d in iter.Decreases.Expressions) {
+ // TODO: in the following line, "old(E)" should also be replaced by "at(iter._preHeap, E)"
+ iter.Member_MoveNext.Decreases.Expressions.Add(subst.Substitute(d));
+ }
+ iter.Member_MoveNext.Decreases.Attributes = subst.SubstAttributes(iter.Decreases.Attributes);
}
/// <summary>
@@ -3116,7 +3281,7 @@ namespace Microsoft.Dafny }
}
}
- if (!fse.Field.IsMutable) {
+ if (!fse.Field.IsUserMutable) {
Error(stmt, "LHS of assignment does not denote a mutable field");
}
}
@@ -3693,7 +3858,7 @@ namespace Microsoft.Dafny // resolve the method name
NonProxyType nptype;
MemberDecl member = ResolveMember(s.Tok, receiverType, s.MethodName, out nptype);
- ICodeContext callee = null;
+ Method callee = null;
if (member == null) {
// error has already been reported by ResolveMember
} else if (member is Method) {
@@ -3809,7 +3974,7 @@ namespace Microsoft.Dafny }
} else if (resolvedLhs is FieldSelectExpr) {
var ll = (FieldSelectExpr)resolvedLhs;
- if (!ll.Field.IsMutable) {
+ if (!ll.Field.IsUserMutable) {
Error(resolvedLhs, "LHS of assignment must denote a mutable field");
}
}
@@ -3818,10 +3983,11 @@ namespace Microsoft.Dafny // Resolution termination check
ModuleDefinition callerModule = codeContext.EnclosingModule;
- ModuleDefinition calleeModule = callee.EnclosingModule;
+ ModuleDefinition calleeModule = ((ICodeContext)callee).EnclosingModule;
if (callerModule == calleeModule) {
// intra-module call; this is allowed; add edge in module's call graph
- callerModule.CallGraph.AddEdge(codeContext, callee);
+ var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
+ callerModule.CallGraph.AddEdge(caller, callee);
} else {
//Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
//
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8d2eff05..bd000e8b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5,6 +5,7 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
+using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
@@ -35,7 +36,7 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
Contract.Invariant(cce.NonNullDictionaryAndValues(fields));
Contract.Invariant(cce.NonNullDictionaryAndValues(fieldFunctions));
- Contract.Invariant(currentMethod == null || currentMethod.EnclosingClass.Module == currentModule);
+ Contract.Invariant(codeContext == null || codeContext.EnclosingModule == currentModule);
}
readonly Bpl.Program sink;
@@ -347,10 +348,8 @@ namespace Microsoft.Dafny { // submodules have already been added as a top level module, ignore this.
} else if (d is ClassDecl) {
AddClassMembers((ClassDecl)d);
- var iter = d as IteratorDecl;
- if (iter != null && iter.Body != null) {
- // also translate the body of the iterator
- //KRML throw new NotImplementedException(); // TODO
+ if (d is IteratorDecl) {
+ AddIteratorSpecAndBody((IteratorDecl)d);
}
} else {
Contract.Assert(false);
@@ -382,8 +381,6 @@ namespace Microsoft.Dafny { return sink;
}
-
-
void AddDatatype(DatatypeDecl dt)
{
Contract.Requires(dt != null);
@@ -646,7 +643,11 @@ namespace Microsoft.Dafny { // wellformedness check for method specification
Bpl.Procedure proc = AddMethod(m, 0, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
- AddMethodImpl(m, proc, true);
+ if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {
+ // skip the well-formedness check, because it has already been done for the iterator
+ } else {
+ AddMethodImpl(m, proc, true);
+ }
// the method itself
proc = AddMethod(m, 1, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
@@ -667,6 +668,294 @@ namespace Microsoft.Dafny { }
}
+ void AddIteratorSpecAndBody(IteratorDecl iter) {
+ Contract.Requires(iter != null);
+
+ bool isRefinementMethod = RefinementToken.IsInherited(iter.tok, iter.Module);
+
+ // wellformedness check for method specification
+ Bpl.Procedure proc = AddIteratorProc(iter, 0, isRefinementMethod);
+ sink.TopLevelDeclarations.Add(proc);
+ AddIteratorWellformed(iter, proc);
+ // the method itself
+ if (iter.Body != null) {
+ proc = AddIteratorProc(iter, 1, isRefinementMethod);
+ sink.TopLevelDeclarations.Add(proc);
+ if (isRefinementMethod) {
+ proc = AddIteratorProc(iter, 3, isRefinementMethod);
+ sink.TopLevelDeclarations.Add(proc);
+ }
+ // ...and its implementation
+ AddIteratorImpl(iter, proc);
+ }
+ }
+
+ /// <summary>
+ /// This method is expected to be called at most 3 times for each procedure in the program:
+ /// * once with kind==0, which says to create a procedure for the wellformedness check of the
+ /// method's specification
+ /// * once with kind==1, which says to create the ordinary procedure for the method, always
+ /// suitable for inter-module callers, and for non-refinement methods also suitable for
+ /// the implementation and intra-module callers of the method
+ /// * possibly once with kind==3 (allowed only if isRefinementMethod), which says to create
+ /// a procedure suitable for the implementation of a refinement method
+ /// </summary>
+ Bpl.Procedure AddIteratorProc(IteratorDecl iter, int kind, bool isRefinementMethod) {
+ Contract.Requires(iter != null);
+ Contract.Requires(0 <= kind && kind < 4 && kind != 2);
+ Contract.Requires(isRefinementMethod || kind < 2);
+ Contract.Requires(predef != null);
+ Contract.Requires(currentModule == null && codeContext == null);
+ Contract.Ensures(currentModule == null && codeContext == null);
+ Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);
+
+ currentModule = iter.Module;
+ codeContext = iter;
+
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);
+
+ Bpl.VariableSeq inParams, outParams;
+ GenerateMethodParameters(iter.tok, iter, etran, out inParams, out outParams);
+
+ var req = new Bpl.RequiresSeq();
+ var mod = new Bpl.IdentifierExprSeq();
+ var ens = new Bpl.EnsuresSeq();
+ if (kind == 0 || (kind == 1 && !isRefinementMethod) || kind == 3) { // the other cases have no need for a free precondition
+ // free requires mh == ModuleContextHeight && InMethodContext;
+ Bpl.Expr context = Bpl.Expr.And(
+ Bpl.Expr.Eq(Bpl.Expr.Literal(iter.Module.Height), etran.ModuleContextHeight()),
+ etran.InMethodContext());
+ req.Add(Requires(iter.tok, true, context, null, null));
+ }
+ mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);
+ mod.Add(etran.Tick());
+
+ if (kind != 0) {
+ string comment = "user-defined preconditions";
+ foreach (var p in iter.Requires) {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
+ if (kind == 2 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
+ // this precondition was inherited into this module, so just ignore it
+ } else {
+ req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
+ }
+ }
+ comment = null;
+ }
+ comment = "user-defined postconditions";
+ foreach (MaybeFreeExpression p in iter.Ensures) {
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
+ ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
+ } else {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
+ if (kind == 3 && RefinementToken.IsInherited(s.E.tok, currentModule)) {
+ // this postcondition was inherited into this module, so just ignore it
+ } else {
+ ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ }
+ }
+ }
+ comment = null;
+ }
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, etran.Old, etran, etran.Old)) {
+ ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
+ }
+ }
+
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);
+ string name;
+ switch (kind) {
+ case 0: name = "CheckWellformed$$" + iter.FullCompileName; break;
+ case 1: name = iter.FullCompileName; break;
+ case 3: name = string.Format("RefinementImpl_{0}$${1}", iter.Module.Name, iter.FullCompileName); break;
+ default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected kind
+ }
+ Bpl.Procedure proc = new Bpl.Procedure(iter.tok, name, typeParams, inParams, outParams, req, mod, ens);
+
+ currentModule = null;
+ codeContext = null;
+
+ return proc;
+ }
+
+ void AddIteratorWellformed(IteratorDecl iter, Procedure proc) {
+ currentModule = iter.Module;
+ codeContext = iter;
+
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);
+ Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+
+ var builder = new Bpl.StmtListBuilder();
+ var etran = new ExpressionTranslator(this, predef, iter.tok);
+ var localVariables = new Bpl.VariableSeq();
+ GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables);
+
+ foreach (var p in iter.OutsHistory) {
+ // var ys: seq<...>;
+ // TODO: should this variable have a 'where' clause?
+ localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));
+ }
+ foreach (var p in iter.ExtraVars) {
+ // var extra: T;
+ // TODO: should this variable have a 'where' clause?
+ localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));
+ }
+
+
+
+ Bpl.StmtList stmts;
+ // check well-formedness of the preconditions, and then assume each one of them
+ foreach (var p in iter.Requires) {
+ CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
+ builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
+ }
+ // Note: the reads and modifies clauses are not checked for well-formedness (is that sound?), because it used to
+ // be that the syntax was not rich enough for programmers to specify modifies clauses and always being
+ // absolutely well-defined.
+ // check well-formedness of the decreases clauses
+ foreach (var p in iter.Decreases.Expressions)
+ {
+ CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
+ }
+
+ // play havoc with the heap according to the modifies clause and inverse of the reads clause
+ // TODO: something like: builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
+ // assume the usual two-state boilerplate information
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions/*TODO: should this also include the Reads clause?*/, etran.Old, etran, etran.Old))
+ {
+ if (tri.IsFree) {
+ builder.Add(new Bpl.AssumeCmd(iter.tok, tri.Expr));
+ }
+ }
+
+ // also play havoc with the out parameters
+ if (outParams.Length != 0) { // don't create an empty havoc statement
+ Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
+ foreach (Bpl.Variable b in outParams) {
+ Contract.Assert(b != null);
+ outH.Add(new Bpl.IdentifierExpr(b.tok, b));
+ }
+ builder.Add(new Bpl.HavocCmd(iter.tok, outH));
+ }
+
+ // check wellformedness of yield requires
+ foreach (var p in iter.YieldRequires) {
+ CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
+ builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
+ }
+
+ // TODO: do another havoc
+
+ // check wellformedness of postconditions
+ var yeBuilder = new Bpl.StmtListBuilder();
+ var endBuilder = new Bpl.StmtListBuilder();
+ foreach (var p in iter.YieldEnsures) {
+ CheckWellformed(p.E, new WFOptions(), localVariables, yeBuilder, etran);
+ yeBuilder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
+ }
+ foreach (var p in iter.Ensures) {
+ CheckWellformed(p.E, new WFOptions(), localVariables, endBuilder, etran);
+ endBuilder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
+ }
+ builder.Add(new Bpl.IfCmd(iter.tok, null, yeBuilder.Collect(iter.tok), null, endBuilder.Collect(iter.tok)));
+
+ stmts = builder.Collect(iter.tok);
+
+ QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
+
+ Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,
+ typeParams, inParams, outParams,
+ localVariables, stmts, kv);
+ sink.TopLevelDeclarations.Add(impl);
+
+ currentModule = null;
+ codeContext = null;
+ loopHeapVarCount = 0;
+ otherTmpVarCount = 0;
+ _tmpIEs.Clear();
+ }
+
+ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) {
+ Contract.Requires(iter != null);
+ Contract.Requires(proc != null);
+ Contract.Requires(sink != null && predef != null);
+ Contract.Requires(iter.Body != null);
+ Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+
+ currentModule = iter.Module;
+ codeContext = iter;
+
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);
+ Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);
+ Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
+ GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables);
+ // add locals for the yield-history variables and the extra variables
+ foreach (var p in iter.OutsHistory) {
+ // var ys: seq<...>;
+ // TODO: should this variable have a 'where' clause?
+ localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));
+ // ys := [];
+ var ys = etran.TrVar(p.tok, p);
+ builder.Add(Bpl.Cmd.SimpleAssign(p.tok, ys, FunctionCall(p.tok, BuiltinFunction.SeqEmpty, predef.BoxType)));
+ }
+ foreach (var p in iter.ExtraVars) {
+ // var extra: T;
+ // TODO: should this variable have a 'where' clause?
+ localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))));
+ }
+ // also add the _yieldCount variable, and assume its initial value to be 0
+ yieldCountVariable = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "_yieldCount", Bpl.Type.Int));
+ yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran); // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption
+ localVariables.Add(yieldCountVariable);
+ builder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0))));
+ // add a variable $_OldIterHeap
+ // TODO: should this variable have a 'where' clause?
+ localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType)));
+
+ // do an initial YieldHavoc
+ YieldHavoc(iter.tok, iter, builder, etran);
+
+ // translate the body of the method
+ var stmts = TrStmt2StmtList(builder, iter.Body, localVariables, etran);
+
+ QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
+
+ Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,
+ typeParams, inParams, outParams,
+ localVariables, stmts, kv);
+ sink.TopLevelDeclarations.Add(impl);
+
+ currentModule = null;
+ codeContext = null;
+ yieldCountVariable = null;
+ loopHeapVarCount = 0;
+ otherTmpVarCount = 0;
+ _tmpIEs.Clear();
+ }
+
+ Bpl.Expr YieldCountAssumption(IteratorDecl iter, ExpressionTranslator etran) {
+ Contract.Requires(iter != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(yieldCountVariable != null);
+ Bpl.Expr wh = Bpl.Expr.True;
+ foreach (var ys in iter.OutsHistory) {
+ // add the conjunct: _yieldCount == |ys|
+ wh = Bpl.Expr.And(wh, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable),
+ FunctionCall(iter.tok, BuiltinFunction.SeqLength, null, etran.TrVar(iter.tok, ys))));
+
+ }
+ return wh;
+ }
+
void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(me != null);
@@ -1066,7 +1355,8 @@ namespace Microsoft.Dafny { }
ModuleDefinition currentModule = null; // the name of the module whose members are currently being translated
- Method currentMethod = null; // the method whose implementation is currently being translated
+ ICodeContext codeContext = null; // the method/iterator whose implementation is currently being translated
+ LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated
int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
Dictionary<string, Bpl.IdentifierExpr> _tmpIEs = new Dictionary<string, Bpl.IdentifierExpr>();
@@ -1139,11 +1429,11 @@ namespace Microsoft.Dafny { Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(wellformednessProc || m.Body != null);
- Contract.Requires(currentModule == null && currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
- Contract.Ensures(currentModule == null && currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
currentModule = m.EnclosingClass.Module;
- currentMethod = m;
+ codeContext = m;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
@@ -1292,7 +1582,7 @@ namespace Microsoft.Dafny { // play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
// assume the usual two-state boilerplate information
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod.Mod.Expressions, etran.Old, etran, etran.Old))
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old))
{
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
@@ -1326,7 +1616,7 @@ namespace Microsoft.Dafny { sink.TopLevelDeclarations.Add(impl);
currentModule = null;
- currentMethod = null;
+ codeContext = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
@@ -1345,6 +1635,19 @@ namespace Microsoft.Dafny { DefineFrame(m.tok, m.Mod.Expressions, builder, localVariables, null);
}
+ void GenerateIteratorImplPrelude(IteratorDecl iter, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams,
+ Bpl.StmtListBuilder builder, Bpl.VariableSeq localVariables) {
+ Contract.Requires(iter != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(localVariables != null);
+ Contract.Requires(predef != null);
+
+ // set up the information used to verify the method's modifies clause
+ DefineFrame(iter.tok, iter.Modifies.Expressions, builder, localVariables, null);
+ }
+
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
@@ -2773,9 +3076,28 @@ namespace Microsoft.Dafny { }
}
}
+ if (yieldCountVariable != null) {
+ var decr = new List<Expression>();
+ decr.Add(new BoogieWrapper(new Bpl.IdentifierExpr(tok, yieldCountVariable), new EverIncreasingType()));
+ decr.AddRange(theDecreases);
+ theDecreases = decr;
+ }
return theDecreases;
}
+ /// <summary>
+ /// This Dafny type, which exists only during translation of Dafny into Boogie, represents
+ /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),
+ /// not the usual (\lambda x,y :: x LESS y AND 0 ATMOST y).
+ /// </summary>
+ public class EverIncreasingType : BasicType
+ {
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ return "_increasingInt";
+ }
+ }
+
Expression FrameToObjectSet(List<FrameExpression> fexprs) {
Contract.Requires(fexprs != null);
Contract.Ensures(Contract.Result<Expression>() != null);
@@ -3047,17 +3369,17 @@ namespace Microsoft.Dafny { Contract.Requires(0 <= kind && kind < 4);
Contract.Requires(isRefinementMethod || kind < 2);
Contract.Requires(predef != null);
- Contract.Requires(currentModule == null && currentMethod == null);
- Contract.Ensures(currentModule == null && currentMethod == null);
+ Contract.Requires(currentModule == null && codeContext == null);
+ Contract.Ensures(currentModule == null && codeContext == null);
Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);
currentModule = m.EnclosingClass.Module;
- currentMethod = m;
+ codeContext = m;
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
Bpl.VariableSeq inParams, outParams;
- GenerateMethodParameters(m, etran, out inParams, out outParams);
+ GenerateMethodParameters(m.tok, m, etran, out inParams, out outParams);
Bpl.RequiresSeq req = new Bpl.RequiresSeq();
Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
@@ -3123,7 +3445,7 @@ namespace Microsoft.Dafny { Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);
currentModule = null;
- currentMethod = null;
+ codeContext = null;
return proc;
}
@@ -3135,12 +3457,12 @@ namespace Microsoft.Dafny { // to the refining method.
Method m = methodCheck.Refined;
currentModule = m.EnclosingClass.Module;
- currentMethod = m;
+ codeContext = m;
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
Bpl.VariableSeq inParams, outParams;
- GenerateMethodParameters(m, etran, out inParams, out outParams);
+ GenerateMethodParameters(m.tok, m, etran, out inParams, out outParams);
Bpl.RequiresSeq req = new Bpl.RequiresSeq();
Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
@@ -3274,7 +3596,7 @@ namespace Microsoft.Dafny { // Clean up
currentModule = null;
- currentMethod = null;
+ codeContext = null;
otherTmpVarCount = 0;
_tmpIEs.Clear();
}
@@ -3393,14 +3715,15 @@ namespace Microsoft.Dafny { currentModule = null;
}
- private void GenerateMethodParameters(Method m, ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) {
+ private void GenerateMethodParameters(IToken tok, ICodeContext m, ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) {
inParams = new Bpl.VariableSeq();
outParams = new Bpl.VariableSeq();
if (!m.IsStatic) {
+ var receiverType = m is MemberDecl ? Resolver.GetReceiverType(tok, (MemberDecl)m) : Resolver.GetThisType(tok, (IteratorDecl)m);
Bpl.Expr wh = Bpl.Expr.And(
- Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),
- etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetReceiverType(m.tok, m)));
- Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);
+ Bpl.Expr.Neq(new Bpl.IdentifierExpr(tok, "this", predef.RefType), predef.Null),
+ etran.GoodRef(tok, new Bpl.IdentifierExpr(tok, "this", predef.RefType), receiverType));
+ Bpl.Formal thVar = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", predef.RefType, wh), true);
inParams.Add(thVar);
}
foreach (Formal p in m.Ins) {
@@ -3560,6 +3883,8 @@ namespace Microsoft.Dafny { return Bpl.Type.Bool;
} else if (type is IntType) {
return Bpl.Type.Int;
+ } else if (type is EverIncreasingType) {
+ return Bpl.Type.Int;
} else if (type.IsTypeParameter) {
return predef.BoxType;
} else if (type.IsRefType) {
@@ -3618,7 +3943,7 @@ namespace Microsoft.Dafny { Contract.Requires(errorMessage != null);
Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
- if (RefinementToken.IsInherited(refinesToken, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {
+ if (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
// produce an assume instead
return new Bpl.AssumeCmd(tok, condition);
} else {
@@ -3637,7 +3962,7 @@ namespace Microsoft.Dafny { Contract.Requires(condition != null);
Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
- if (RefinementToken.IsInherited(refinesTok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {
+ if (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
// produce a "skip" instead
return new Bpl.AssumeCmd(tok, Bpl.Expr.True);
} else {
@@ -3657,7 +3982,7 @@ namespace Microsoft.Dafny { Contract.Requires(condition != null);
Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
- if (RefinementToken.IsInherited(tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {
+ if (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
// produce an assume instead
return new Bpl.AssumeCmd(tok, condition, kv);
} else {
@@ -3696,7 +4021,7 @@ namespace Microsoft.Dafny { Contract.Requires(block != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
- Contract.Requires(currentMethod != null && predef != null);
+ Contract.Requires(codeContext != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
@@ -3708,7 +4033,7 @@ namespace Microsoft.Dafny { Contract.Requires(block != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
- Contract.Requires(currentMethod != null && predef != null);
+ Contract.Requires(codeContext != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
TrStmt(block, builder, locals, etran);
@@ -3721,7 +4046,7 @@ namespace Microsoft.Dafny { Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
- Contract.Requires(currentMethod != null && predef != null);
+ Contract.Requires(codeContext != null && predef != null);
if (stmt is PredicateStmt) {
if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {
AddComment(builder, stmt, "assert statement");
@@ -3772,7 +4097,52 @@ namespace Microsoft.Dafny { }
builder.Add(new Bpl.ReturnCmd(stmt.Tok));
} else if (stmt is YieldStmt) {
- //KRML throw new NotImplementedException(); // TODO
+ var s = (YieldStmt)stmt;
+ AddComment(builder, s, "yield statement");
+ Contract.Assert(codeContext is IteratorDecl);
+ var iter = (IteratorDecl)codeContext;
+ // ys := ys + [y];
+ Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count);
+ for (int i = 0; i < iter.Outs.Count; i++) {
+ var y = iter.Outs[i];
+ var dafnyY = new IdentifierExpr(s.Tok, y.Name);
+ dafnyY.Var = y; dafnyY.Type = y.Type; // resolve here
+ var ys = iter.OutsHistory[i];
+ var dafnyYs = new IdentifierExpr(s.Tok, ys.Name);
+ dafnyYs.Var = ys; dafnyYs.Type = ys.Type; // resolve here
+ var dafnySingletonY = new SeqDisplayExpr(s.Tok, new List<Expression>() { dafnyY });
+ dafnySingletonY.Type = ys.Type; // resolve here
+ var rhs = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Add, dafnyYs, dafnySingletonY);
+ rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat;
+ rhs.Type = ys.Type; // resolve here
+ var cmd = Bpl.Cmd.SimpleAssign(s.Tok, etran.TrVar(s.Tok, ys), etran.TrExpr(rhs));
+ builder.Add(cmd);
+ }
+ // yieldCount := yieldCount + 1; assume yieldCount == |ys|;
+ var yc = new Bpl.IdentifierExpr(s.Tok, yieldCountVariable);
+ var incYieldCount = Bpl.Cmd.SimpleAssign(s.Tok, yc, Bpl.Expr.Binary(s.Tok, Bpl.BinaryOperator.Opcode.Add, yc, Bpl.Expr.Literal(1)));
+ builder.Add(incYieldCount);
+ builder.Add(new Bpl.AssumeCmd(s.Tok, YieldCountAssumption(iter, etran)));
+ // assert YieldEnsures[subst]; // where 'subst' replaces "old(E)" with "E" being evaluated in $_OldIterHeap
+ var prevYieldHeap = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(s.Tok, "$_OldIterHeap", predef.HeapType));
+ foreach (var p in iter.YieldEnsures) {
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
+ // do nothing
+ } else {
+ bool splitHappened; // actually, we don't care
+ var ss = TrSplitExpr(p.E, prevYieldHeap, out splitHappened);
+ foreach (var split in ss) {
+ if (RefinementToken.IsInherited(split.E.tok, currentModule)) {
+ // this postcondition was inherited into this module, so just ignore it
+ } else if (!split.IsFree) {
+ builder.Add(AssertNS(split.E.tok, split.E, "possible violation of yield-ensures condition", stmt.Tok));
+ }
+ }
+ builder.Add(new Bpl.AssumeCmd(stmt.Tok, prevYieldHeap.TrExpr(p.E)));
+ }
+ }
+ YieldHavoc(iter.tok, iter, builder, etran);
+
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
AddComment(builder, s, "assign-such-that statement");
@@ -4058,6 +4428,36 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// Generate:
+ /// $_OldIterHeap := Heap;
+ /// havoc Heap \ {this} \ _reads \ _new;
+ /// assume YieldRequires;
+ /// </summary>
+ void YieldHavoc(IToken tok, IteratorDecl iter, StmtListBuilder builder, ExpressionTranslator etran) {
+ Contract.Requires(tok != null);
+ Contract.Requires(iter != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(etran != null);
+ // $_OldIterHeap := Heap;
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr));
+#if SOON
+ // havoc Heap \ {this} \ _reads \ _new;
+ // TODO: this requires a different design! 'this' is not accessible here. (For now, just use the local variables.)
+ var setType = TrType(new SetType(new ObjectType()));
+ builder.Add(new Bpl.CallCmd(tok, "$YieldHavoc",
+ new List<Bpl.Expr>() {
+ new Bpl.IdentifierExpr(tok, "_reads", setType),
+ new Bpl.IdentifierExpr(tok, "_new", setType)
+ },
+ new List<Bpl.IdentifierExpr>()));
+#endif
+ // assume YieldRequires;
+ foreach (var p in iter.YieldRequires) {
+ builder.Add(new Bpl.AssumeCmd(tok, etran.TrExpr(p.E)));
+ }
+ }
+
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);
@@ -4626,7 +5026,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
}
// include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod.Mod.Expressions, etranPreLoop, etran, etran.Old))
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, codeContext.Modifies.Expressions, etranPreLoop, etran, etran.Old))
{
if (tri.IsFree) {
invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
@@ -4863,9 +5263,10 @@ namespace Microsoft.Dafny { // Check termination
ModuleDefinition module = method.EnclosingClass.Module;
if (module == currentModule) {
- if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
+ var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
+ if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(caller)) {
bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);
+ List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);
CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, null);
}
@@ -4892,7 +5293,7 @@ namespace Microsoft.Dafny { // Make the call
string name;
- if (RefinementToken.IsInherited(method.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {
+ if (RefinementToken.IsInherited(method.tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);
} else {
name = method.FullCompileName;
@@ -5198,6 +5599,10 @@ namespace Microsoft.Dafny { less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), e0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), e0), atmost);
}
+ } else if (ty is EverIncreasingType) {
+ eq = Bpl.Expr.Eq(e0, e1);
+ less = Bpl.Expr.Gt(e0, e1);
+ atmost = Bpl.Expr.Ge(e0, e1);
} else if (ty is SetType) {
eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1);
less = etran.ProperSubset(tok, e0, e1);
@@ -7470,7 +7875,7 @@ namespace Microsoft.Dafny { if (f.Body != null && !(f.Body.Resolved is MatchExpr)) {
if (RefinementToken.IsInherited(fexp.tok, currentModule) &&
f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&
- (currentMethod == null || !currentMethod.MustReverify)) {
+ (codeContext == null || !codeContext.MustReverify)) {
// The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything
// that needed to be proved about the function was proved already in the previous module, even without the body definition).
} else {
@@ -7621,7 +8026,7 @@ namespace Microsoft.Dafny { }
// TODO: Is the the following call to ContainsChange expensive? It's linear in the size of "expr", but we get here many times in TrSpliExpr, so wouldn't the total
// time in the size of the expression passed to the first TrSpliExpr be quadratic?
- if (RefinementToken.IsInherited(expr.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {
+ if (RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {
// If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively
// change the token of the translated expression to make it look like it's not inherited. This will cause "e" to
// be verified again in the refining module.
@@ -8645,7 +9050,7 @@ namespace Microsoft.Dafny { }
}
- Attributes SubstAttributes(Attributes attrs) {
+ public Attributes SubstAttributes(Attributes attrs) {
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
if (attrs != null) {
List<Attributes.Argument> newArgs = new List<Attributes.Argument>(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bde6a07c..ecde4fb1 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1616,16 +1616,27 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met 5 resolution/type errors detected in TailCalls.dfy
-------------------- IteratorResolution.dfy --------------------
-IteratorResolution.dfy(56,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(57,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(61,18): Error: arguments must have the same type (got _T0 and int)
-IteratorResolution.dfy(73,19): Error: RHS (of type bool) not assignable to LHS (of type int)
-IteratorResolution.dfy(76,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
-5 resolution/type errors detected in IteratorResolution.dfy
+IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(60,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
+IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int)
+IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
+IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)
+IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(18,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field
+9 resolution/type errors detected in IteratorResolution.dfy
-------------------- Iterators.dfy --------------------
+Iterators.dfy(36,14): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(1,10): Related location: This is the precondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon31_Then
+ (0,0): anon3
+ (0,0): anon32_Then
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 16 verified, 1 error
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index fe9e2563..dca4cb93 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -14,6 +14,9 @@ module Mx { method IteratorUser() {
var iter := new ExampleIterator.ExampleIterator(15);
+ iter.k := 12; // error: not allowed to assign to iterator's in-parameters
+ iter.x := 12; // error: not allowed to assign to iterator's yield-parameters
+ iter.xs := []; // error: not allowed to assign to iterator's yield-history variables
var j := 0;
while (j < 100) {
var more := iter.MoveNext();
@@ -74,6 +77,11 @@ module Mx { }
var h2 := new GenericIteratorResult; // error: constructor is not mentioned
+
+ var h3 := new GenericIterator.GenericIterator(30);
+ if (h3.t == h3.u) {
+ assert !h3.t; // error: type mismatch
+ }
}
}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 76a30330..680c2812 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -11,20 +11,133 @@ iterator MyIntIter() yields (x: int, y: int) yield;
}
+iterator Naturals(u: int) yields (n: nat)
+ requires u < 25; // just to have some precondition
+ ensures false; // never ends
+{
+ n := 0;
+ while (true)
+ {
+ yield n;
+ n := n + 1;
+ }
+}
+
method Main() {
var m := new MyIter.MyIter(12);
+ assert m.ys == m.xs == [];
var a := m.x;
- // assert !a; // error: type mismatch
if (a <= 13) {
print "-- ", m.x, " --\n";
}
+ var mer := m.MoveNext();
+ if (mer) {
+ mer := m.MoveNext();
+ mer := m.MoveNext(); // error
+ }
+
var n := new MyIntIter.MyIntIter();
var patience := 10;
- while (patience != 0) {
+ while (patience != 0)
+ invariant n.Valid() && fresh(n._new);
+ {
var more := n.MoveNext();
if (!more) { break; }
print n.x, ", ", n.y, "\n";
patience := patience - 1;
}
+
+ var o := new Naturals.Naturals(18);
+ var remaining := 100;
+ while (remaining != 0)
+ invariant o.Valid() && fresh(o._new);
+ {
+ var more := o.MoveNext();
+ assert more;
+ print o.n, " ";
+ remaining := remaining - 1;
+ if (remaining % 10 == 0) { print "\n"; }
+ }
+}
+
+// -----------------------------------------------------------
+
+class Cell {
+ var data: int;
+}
+
+iterator IterA(c: Cell)
+ requires c != null;
+ modifies c;
+{
+ while (true) {
+ c.data := *;
+ yield;
+ }
+}
+
+method TestIterA()
+{
+ var c := new Cell;
+ var iter := new IterA.IterA(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ assert tmp == c.data; // error
+}
+
+// -----------------------------------------------------------
+
+iterator IterB(c: Cell)
+ requires c != null;
+ modifies c;
+ yield ensures c.data == old(c.data); // error: cannot prove this without a reads clause
+ ensures true;
+{
+ if (*) { yield; }
+ c.data := *;
+}
+
+method TestIterB()
+{
+ var c := new Cell;
+ var iter := new IterB.IterB(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ if (more) {
+ assert tmp == c.data; // no prob
+ } else {
+ assert tmp == c.data; // error: the postcondition says nothing about this
+ }
+}
+
+// -----------------------------------------------------------
+
+iterator IterC(c: Cell)
+ requires c != null;
+ modifies c;
+ reads c;
+ yield ensures c.data == old(c.data); // error: cannot prove this without a reads clause
+ ensures true;
+{
+ if (*) { yield; }
+ c.data := *;
+}
+
+method TestIterC()
+{
+ var c := new Cell;
+ var iter := new IterC.IterC(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ if (more) {
+ assert tmp == c.data; // no prob
+ } else {
+ assert tmp == c.data; // error: the postcondition says nothing about this
+ }
+
+ iter := new IterC.IterC(c);
+ c.data := 17;
+ more := iter.MoveNext(); // error: iter.Valid() may not hold
}
+
|