diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 26 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 71 | ||||
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 2 |
6 files changed, 76 insertions, 46 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 572a1e29..02d0f344 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -606,14 +606,32 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } // -- Useful macros ----------------------------------------------
// ---------------------------------------------------------------
-// havoc $Heap \ {this} \ S
-procedure {:inline} $YieldHavoc(this: ref, S: Set BoxType);
+// havoc everything in $Heap, except {this}+rds+nw
+procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc everything in $Heap, except rds-mod-{this}
+procedure $IterHavoc0(this: ref, rds: Set BoxType, mod: Set BoxType);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ rds[$Box($o)] && !mod[$Box($o)] && $o != this ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc $Heap at {this}+mod+nw
+procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: 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)]);
+ $o == this || mod[$Box($o)] || nw[$Box($o)]);
+ ensures $HeapSucc(old($Heap), $Heap);
// ---------------------------------------------------------------
// -- Non-determinism --------------------------------------------
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index fb47f020..ccf96486 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1163,9 +1163,6 @@ namespace Microsoft.Dafny { {
public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
- public readonly List<Field> OutsFields;
- public readonly List<Field> OutsHistoryFields; // these are the 'xs' variables
- public readonly List<Field> DecreasesFields; // filled in during resolution
public readonly Specification<FrameExpression> Reads;
public readonly Specification<FrameExpression> Modifies;
public readonly Specification<Expression> Decreases;
@@ -1176,6 +1173,12 @@ namespace Microsoft.Dafny { public readonly List<MaybeFreeExpression> YieldEnsures;
public readonly BlockStmt Body;
public readonly bool SignatureIsOmitted;
+ public readonly List<Field> OutsFields;
+ public readonly List<Field> OutsHistoryFields; // these are the 'xs' variables
+ public readonly List<Field> DecreasesFields; // filled in during resolution
+ public SpecialField Member_Modifies; // filled in during resolution
+ public SpecialField Member_Reads; // filled in during resolution
+ public SpecialField Member_New; // filled in during resolution
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
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index dc49013d..ae43dae4 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -544,12 +544,10 @@ namespace Microsoft.Dafny iter.Members.Add(f);
});
// add the additional special variables as fields
- foreach (var p in new List<Tuple<string, bool>>() {
- new Tuple<string, bool>("_reads", false),
- new Tuple<string, bool>("_modifies", false),
- new Tuple<string, bool>("_new", true) })
- {
- var field = new SpecialField(iter.tok, p.Item1, p.Item1, "", "", true, p.Item2, p.Item2, new SetType(new ObjectType()), null);
+ iter.Member_Reads = new SpecialField(iter.tok, "_reads", "_reads", "", "", true, false, false, new SetType(new ObjectType()), null);
+ iter.Member_Modifies = new SpecialField(iter.tok, "_modifies", "_modifies", "", "", true, false, false, new SetType(new ObjectType()), null);
+ iter.Member_New = new SpecialField(iter.tok, "_new", "_new", "", "", true, true, true, new SetType(new ObjectType()), null);
+ foreach (var field in new List<Field>() { iter.Member_Reads, iter.Member_Modifies, iter.Member_New }) {
field.EnclosingClass = iter; // resolve here
members.Add(field.Name, field);
iter.Members.Add(field);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a65da1ca..70a24310 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -813,20 +813,20 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
- // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies)
- builder.Add(new Bpl.HavocCmd(iter.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
- // assume the usual two-state boilerplate information
- // TODO: the following line does not do exactly what we want:
- 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));
- }
- }
-
- // assume the automatic yield-requires precondition (which is always well-formed): this.Valid()
+ // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this})
var th = new ThisExpr(iter.tok);
th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here
+ var rds = new FieldSelectExpr(iter.tok, th, iter.Member_Reads.Name);
+ rds.Field = iter.Member_Reads; // resolve here
+ rds.Type = iter.Member_Reads.Type; // resolve here
+ var mod = new FieldSelectExpr(iter.tok, th, iter.Member_Modifies.Name);
+ mod.Field = iter.Member_Modifies; // resolve here
+ mod.Type = iter.Member_Modifies.Type; // resolve here
+ builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc0",
+ new List<Bpl.Expr>() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(mod) },
+ new List<Bpl.IdentifierExpr>()));
+
+ // assume the automatic yield-requires precondition (which is always well-formed): this.Valid()
var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, new List<Expression>());
validCall.Function = iter.Member_Valid; // resolve here
validCall.Type = Type.Bool; // resolve here
@@ -839,7 +839,12 @@ namespace Microsoft.Dafny { }
// simulate a modifies this, this._modifies, this._new;
- // TODO
+ var nw = new FieldSelectExpr(iter.tok, th, iter.Member_New.Name);
+ nw.Field = iter.Member_New; // resolve here
+ nw.Type = iter.Member_New.Type; // resolve here
+ builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc1",
+ new List<Bpl.Expr>() { etran.TrExpr(th), etran.TrExpr(mod), etran.TrExpr(nw) },
+ new List<Bpl.IdentifierExpr>()));
// check wellformedness of postconditions
var yeBuilder = new Bpl.StmtListBuilder();
@@ -906,8 +911,8 @@ namespace Microsoft.Dafny { 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)));
+ Bpl.Expr wh = FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType));
+ localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh)));
// do an initial YieldHavoc
YieldHavoc(iter.tok, iter, builder, etran);
@@ -3225,7 +3230,11 @@ namespace Microsoft.Dafny { if (a == null) {
return null;
}
- Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class._System.set" : (ct is SeqType ? "class._System.seq" : "class._System.multiset"), predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok,
+ ct is SetType ? "class._System.set" :
+ ct is SeqType ? "class._System.seq" :
+ "class._System.multiset",
+ predef.ClassNameType);
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
UserDefinedType ct = (UserDefinedType)type;
@@ -4129,13 +4138,13 @@ namespace Microsoft.Dafny { 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));
+ var yeEtran = 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);
+ var ss = TrSplitExpr(p.E, yeEtran, 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
@@ -4143,7 +4152,7 @@ namespace Microsoft.Dafny { 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)));
+ builder.Add(new Bpl.AssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E)));
}
}
YieldHavoc(iter.tok, iter, builder, etran);
@@ -4435,32 +4444,34 @@ namespace Microsoft.Dafny { /// <summary>
/// Generate:
- /// $_OldIterHeap := Heap;
/// havoc Heap \ {this} \ _reads \ _new;
+ /// assume this.Valid();
/// assume YieldRequires;
+ /// $_OldIterHeap := Heap;
/// </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()));
+ var th = new ThisExpr(tok);
+ th.Type = Resolver.GetThisType(tok, iter); // resolve here
+ var rds = new FieldSelectExpr(tok, th, iter.Member_Reads.Name);
+ rds.Field = iter.Member_Reads; // resolve here
+ rds.Type = iter.Member_Reads.Type; // resolve here
+ var nw = new FieldSelectExpr(tok, th, iter.Member_New.Name);
+ nw.Field = iter.Member_New; // resolve here
+ nw.Type = iter.Member_New.Type; // resolve here
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.Expr>() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(nw) },
new List<Bpl.IdentifierExpr>()));
-#endif
// assume YieldRequires;
foreach (var p in iter.YieldRequires) {
builder.Add(new Bpl.AssumeCmd(tok, etran.TrExpr(p.E)));
}
+ // $_OldIterHeap := Heap;
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr));
}
List<Tuple<List<BoundVar>, Expression>> GeneratePartialGuesses(List<BoundVar> bvars, Expression expression) {
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index 68fec344..64d1ebd3 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -15,7 +15,7 @@ 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; // note, not allowed to assign to iterator's yield-parameters (except via 'this')
+ iter.x := 12; // allowed (but this destroys the validity of 'iter'
iter.xs := []; // error: not allowed to assign to iterator's yield-history variables
var j := 0;
while (j < 100) {
@@ -57,7 +57,7 @@ module Mx { requires g0.u;
{
g0.t := true; // error: not allowed to assign to .t
- g0.u := true; // note, not allowed to assign to iterator's yield-parameters (except via 'this'), but this is checked by the verifier
+ g0.u := true; // allowed (but this destroys the validity of 'iter'
var g1 := new GenericIterator.GenericIterator(20);
assert g1.u < 200; // .u is an integer
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 3f06e445..36ba94cb 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -121,7 +121,7 @@ iterator IterC(c: Cell) yield ensures c.data == old(c.data);
ensures true;
{
- if (*) { yield; }
+ if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
c.data := *;
}
|