From 3db6f751759a687b63dfe9998138239b890cafe4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 3 Oct 2012 13:31:25 -0700 Subject: Dafny: more part of verifying iterators --- Binaries/DafnyPrelude.bpl | 26 +++++++++++--- Source/Dafny/DafnyAst.cs | 9 +++-- Source/Dafny/Resolver.cs | 10 +++--- Source/Dafny/Translator.cs | 71 ++++++++++++++++++++++---------------- Test/dafny0/IteratorResolution.dfy | 4 +-- 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 $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 $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 $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 Ins; public readonly List Outs; - public readonly List OutsFields; - public readonly List OutsHistoryFields; // these are the 'xs' variables - public readonly List DecreasesFields; // filled in during resolution public readonly Specification Reads; public readonly Specification Modifies; public readonly Specification Decreases; @@ -1176,6 +1173,12 @@ namespace Microsoft.Dafny { public readonly List YieldEnsures; public readonly BlockStmt Body; public readonly bool SignatureIsOmitted; + public readonly List OutsFields; + public readonly List OutsHistoryFields; // these are the 'xs' variables + public readonly List 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>() { - new Tuple("_reads", false), - new Tuple("_modifies", false), - new Tuple("_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() { 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() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(mod) }, + new List())); + + // 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()); 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() { etran.TrExpr(th), etran.TrExpr(mod), etran.TrExpr(nw) }, + new List())); // 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 { /// /// Generate: - /// $_OldIterHeap := Heap; /// havoc Heap \ {this} \ _reads \ _new; + /// assume this.Valid(); /// assume YieldRequires; + /// $_OldIterHeap := Heap; /// 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() { - new Bpl.IdentifierExpr(tok, "_reads", setType), - new Bpl.IdentifierExpr(tok, "_new", setType) - }, + new List() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(nw) }, new List())); -#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, Expression>> GeneratePartialGuesses(List 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 := *; } -- cgit v1.2.3