From caa2c1d6c2aa2976d5ef055e412374832981e566 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 3 Oct 2012 23:27:22 -0700 Subject: Dafny: complete implementation of iterators --- Binaries/DafnyPrelude.bpl | 6 ++++++ Source/Dafny/Translator.cs | 44 ++++++++++++++++++++++++++++++++--------- Test/dafny0/Answer | 29 ++++++++++++++++++++++++++- Test/dafny0/Iterators.dfy | 49 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 118 insertions(+), 10 deletions(-) diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 02d0f344..e6d05bea 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -633,6 +633,12 @@ procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: Set BoxType); $o == this || mod[$Box($o)] || nw[$Box($o)]); ensures $HeapSucc(old($Heap), $Heap); +procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType)) + returns (s: Set BoxType); + ensures (forall bx: BoxType :: { s[bx] } s[bx] <==> + read(newHeap, this, NW)[bx] || + ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc))); + // --------------------------------------------------------------- // -- Non-determinism -------------------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b74c5fb1..5d3d359a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -911,7 +911,10 @@ 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 - Bpl.Expr wh = FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType)); + var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType); + Bpl.Expr wh = BplAnd( + FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, oih), + FunctionCall(iter.tok, BuiltinFunction.HeapSucc, null, oih, etran.HeapExpr)); localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh))); // do an initial YieldHavoc @@ -4655,7 +4658,12 @@ namespace Microsoft.Dafny { } else { lhsType = ((MultiSelectExpr)lhs).Type; } - CheckSubrange(r.Tok, etran.TrExpr(rhs), lhsType, definedness); + var translatedRhs = etran.TrExpr(rhs); + CheckSubrange(r.Tok, translatedRhs, lhsType, definedness); + if (lhs is FieldSelectExpr) { + var fse = (FieldSelectExpr)lhs; + Check_NewRestrictions(fse.tok, obj, fse.Field, translatedRhs, definedness, etran); + } } // check for duplicate LHSs @@ -6066,7 +6074,7 @@ namespace Microsoft.Dafny { var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified? bLhss.Add(rhsCanAffectPreviouslyKnownExpressions ? null : bLhs); lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) { - builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs)); + bldr.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs)); }); } else if (lhs is FieldSelectExpr) { @@ -6090,11 +6098,12 @@ namespace Microsoft.Dafny { bLhss.Add(null); lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) { + Check_NewRestrictions(tok, obj, fse.Field, rhs, bldr, et); var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fse.Field)), rhs)); - builder.Add(cmd); + bldr.Add(cmd); // assume $IsGoodHeap($Heap); - builder.Add(AssumeGoodHeap(tok, et)); + bldr.Add(AssumeGoodHeap(tok, et)); }); } else if (lhs is SeqSelectExpr) { @@ -6126,9 +6135,9 @@ namespace Microsoft.Dafny { lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs)); - builder.Add(cmd); + bldr.Add(cmd); // assume $IsGoodHeap($Heap); - builder.Add(AssumeGoodHeap(tok, et)); + bldr.Add(AssumeGoodHeap(tok, et)); }); } else { @@ -6158,9 +6167,9 @@ namespace Microsoft.Dafny { lhsBuilders.Add(delegate(Bpl.Expr rhs, Bpl.StmtListBuilder bldr, ExpressionTranslator et) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs)); - builder.Add(cmd); + bldr.Add(cmd); // assume $IsGoodHeap($Heap); - builder.Add(AssumeGoodHeap(tok, etran)); + bldr.Add(AssumeGoodHeap(tok, etran)); }); } @@ -6306,6 +6315,23 @@ namespace Microsoft.Dafny { return null; } + void Check_NewRestrictions(IToken tok, Bpl.Expr obj, Field f, Bpl.Expr rhs, StmtListBuilder builder, ExpressionTranslator etran) { + Contract.Requires(tok != null); + Contract.Requires(obj != null); + Contract.Requires(f != null); + Contract.Requires(rhs != null); + Contract.Requires(builder != null); + Contract.Requires(etran != null); + var iter = f.EnclosingClass as IteratorDecl; + if (iter != null && f == iter.Member_New) { + // Assignments to an iterator _new field is only allowed to shrink the set, so: + // assert Set#Subset(rhs, obj._new); + var fId = new Bpl.IdentifierExpr(tok, GetField(f)); + var subset = FunctionCall(tok, BuiltinFunction.SetSubset, null, rhs, ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, obj, fId)); + builder.Add(Assert(tok, subset, "an assignment to " + f.Name + " is only allowed to shrink the set")); + } + } + Bpl.AssumeCmd AssumeGoodHeap(IToken tok, ExpressionTranslator etran) { Contract.Requires(tok != null); Contract.Requires(etran != null); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 4de9e965..671c7c91 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1643,6 +1643,24 @@ Iterators.dfy(174,28): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon15_Then +Iterators.dfy(205,7): Error: an assignment to _new is only allowed to shrink the set +Execution trace: + (0,0): anon0 + Iterators.dfy(194,3): anon17_LoopHead + (0,0): anon17_LoopBody + Iterators.dfy(194,3): anon18_Else + (0,0): anon5 + Iterators.dfy(194,3): anon20_Else + (0,0): anon21_Then +Iterators.dfy(209,21): Error: assertion violation +Execution trace: + (0,0): anon0 + Iterators.dfy(194,3): anon17_LoopHead + (0,0): anon17_LoopBody + Iterators.dfy(194,3): anon18_Else + (0,0): anon5 + Iterators.dfy(194,3): anon20_Else + (0,0): anon22_Then Iterators.dfy(37,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: @@ -1669,8 +1687,17 @@ Execution trace: (0,0): anon0 (0,0): anon4_Then (0,0): anon3 +Iterators.dfy(231,14): Error: assertion violation +Execution trace: + (0,0): anon0 + Iterators.dfy(222,3): anon15_LoopHead + (0,0): anon15_LoopBody + Iterators.dfy(222,3): anon16_Else + (0,0): anon8 + Iterators.dfy(222,3): anon19_Else + (0,0): anon20_Else -Dafny program verifier finished with 34 verified, 8 errors +Dafny program verifier finished with 38 verified, 11 errors -------------------- Superposition.dfy -------------------- diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 2473daa0..c6a0488b 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -184,3 +184,52 @@ static method AnotherMethod() returns (u: Cell, v: Cell) { u := new Cell; } + +iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell) + yield ensures r != null && fresh(r) && r !in _new; + yield ensures c != null && fresh(c); // but we don't say whether it's in _new + ensures false; // goes forever +{ + var myCells: seq := []; + while (true) + invariant forall z :: z in myCells ==> z in _new; + { + c := new Cell; + r := new Cell; + c.data, r.data := 12, 12; + myCells := myCells + [c]; + _new := _new - {r}; // remove our interest in 'r' + yield; + if (*) { + _new := _new + {c}; // fine, since 'c' is already in _new + _new := _new + {u}; // error: this does not shrink the set + } else if (*) { + assert c.data == 12; // still true, since 'c' is in _new + assert c in _new; // as is checked here as well + assert r.data == 12; // error: it may have changed + } else { + parallel (z | z in myCells) { + z.data := z.data + 1; // we're allowed to modify these, because they are all in _new + } + } + } +} + +method ClientOfNewReferences() +{ + var m := new DoleOutReferences.DoleOutReferences(null); + var i := 86; + while (i != 0) + invariant m.Valid() && fresh(m._new); + { + var more := m.MoveNext(); + assert more; // follows from 'ensures' clause of the iterator + if (*) { + m.r.data := i; // this change is allowed, because we own it + } else { + m.c.data := i; // this change, by itself, is allowed + assert m.Valid(); // error: ... however, don't expect m.Valid() to survive the change to m.c.data + } + i := i - 1; + } +} -- cgit v1.2.3