diff options
| -rw-r--r-- | Dafny/Translator.cs | 59 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 34 |
3 files changed, 96 insertions, 3 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index c3073733..b74c5fb1 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4162,6 +4162,7 @@ namespace Microsoft.Dafny { }
}
YieldHavoc(iter.tok, iter, builder, etran);
+ builder.Add(CaptureState(s.Tok));
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
@@ -4806,13 +4807,18 @@ namespace Microsoft.Dafny { // initHeap := $Heap;
exporter.Add(Bpl.Cmd.SimpleAssign(tok, initHeap, etran.HeapExpr));
if (s0.Method.Ens.Exists(ens => MentionsOldState(ens.E))) {
+ var heapIdExpr = (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr;
// advance $Heap, Tick;
- exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick())));
+ exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(heapIdExpr, etran.Tick())));
foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List<FrameExpression>(), initEtran, etran, initEtran)) {
if (tri.IsFree) {
exporter.Add(new Bpl.AssumeCmd(tok, tri.Expr));
}
}
+ if (codeContext is IteratorDecl) {
+ var iter = (IteratorDecl)codeContext;
+ RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);
+ }
} else {
// As an optimization, create the illusion that the $Heap is unchanged by the parallel body.
exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(etran.Tick())));
@@ -4850,6 +4856,32 @@ namespace Microsoft.Dafny { }
}
+ void RecordNewObjectsIn_New(IToken tok, IteratorDecl iter, Bpl.Expr initHeap, Bpl.IdentifierExpr currentHeap,
+ Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ Contract.Requires(tok != null);
+ Contract.Requires(iter != null);
+ Contract.Requires(initHeap != null);
+ Contract.Requires(currentHeap != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+ // Add all newly allocated objects to the set this._new
+ var updatedSet = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$iter_newUpdate" + otherTmpVarCount, predef.SetType(iter.tok, predef.BoxType)));
+ otherTmpVarCount++;
+ locals.Add(updatedSet);
+ var updatedSetIE = new Bpl.IdentifierExpr(iter.tok, updatedSet);
+ // call $iter_newUpdate := $IterCollectNewObjects(initHeap, $Heap, this, _new);
+ var th = new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType);
+ var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New));
+ Bpl.Cmd cmd = new CallCmd(iter.tok, "$IterCollectNewObjects",
+ new List<Bpl.Expr>() { initHeap, etran.HeapExpr, th, nwField },
+ new List<Bpl.IdentifierExpr>() { updatedSetIE });
+ builder.Add(cmd);
+ // $Heap[this, _new] := $iter_newUpdate;
+ cmd = Bpl.Cmd.SimpleAssign(iter.tok, currentHeap, ExpressionTranslator.UpdateHeap(iter.tok, currentHeap, th, nwField, updatedSetIE));
+ builder.Add(cmd);
+ }
+
void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// Translate:
// parallel (x,y | Range(x,y))
@@ -5204,6 +5236,16 @@ namespace Microsoft.Dafny { bLhss[i] = new Bpl.IdentifierExpr(lhs.tok, var.Name, ty);
}
}
+ Bpl.IdentifierExpr initHeap = null;
+ if (codeContext is IteratorDecl) {
+ // var initHeap := $Heap;
+ var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapCallStmt#" + otherTmpVarCount, predef.HeapType));
+ otherTmpVarCount++;
+ locals.Add(initHeapVar);
+ initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);
+ // initHeap := $Heap;
+ builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr));
+ }
ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);
for (int i = 0; i < lhsBuilders.Count; i++) {
var lhs = s.Lhs[i];
@@ -5223,6 +5265,11 @@ namespace Microsoft.Dafny { lhsBuilders[i](bRhs, builder, etran);
}
+ if (codeContext is IteratorDecl) {
+ var iter = (IteratorDecl)codeContext;
+ Contract.Assert(initHeap != null);
+ RecordNewObjectsIn_New(s.Tok, iter, initHeap, (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr, builder, locals, etran);
+ }
builder.Add(CaptureState(s.Tok));
}
@@ -6214,6 +6261,16 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr heap = (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr;
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, heap, ExpressionTranslator.UpdateHeap(tok, heap, nw, alloc, Bpl.Expr.True));
builder.Add(cmd);
+ if (codeContext is IteratorDecl) {
+ var iter = (IteratorDecl)codeContext;
+ // $Heap[this, _new] := Set#UnionOne<BoxType>($Heap[this, _new], $Box($nw));
+ var th = new Bpl.IdentifierExpr(tok, etran.This, predef.RefType);
+ var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New));
+ var thisDotNew = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, th, nwField);
+ var unionOne = FunctionCall(tok, BuiltinFunction.SetUnionOne, predef.BoxType, thisDotNew, FunctionCall(tok, BuiltinFunction.Box, null, nw));
+ var heapRhs = ExpressionTranslator.UpdateHeap(tok, etran.HeapExpr, th, nwField, unionOne);
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, heap, heapRhs));
+ }
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
if (tRhs.InitCall != null) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index df0451d5..4de9e965 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1639,6 +1639,10 @@ Execution trace: (0,0): anon0
(0,0): anon4_Then
(0,0): anon3
+Iterators.dfy(174,28): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon15_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:
@@ -1666,7 +1670,7 @@ Execution trace: (0,0): anon4_Then
(0,0): anon3
-Dafny program verifier finished with 27 verified, 7 errors
+Dafny program verifier finished with 34 verified, 8 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index e1461622..2473daa0 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -117,7 +117,7 @@ method TestIterB() }
}
-// -----------------------------------------------------------
+// ------------------ yield statements, and_decreases variables ----------------------------------
iterator IterC(c: Cell)
requires c != null;
@@ -152,3 +152,35 @@ method TestIterC() more := iter.MoveNext(); // error: iter.Valid() may not hold
}
+// ------------------ allocations inside an iterator ------------------
+
+iterator AllocationIterator(x: Cell)
+{
+ assert _new == {};
+ var h := new Cell;
+ assert _new == {h};
+
+ SomeMethod();
+ assert x !in _new;
+ assert null !in _new;
+ assert h in _new;
+
+ ghost var saveNew := _new;
+ var u, v := AnotherMethod();
+ assert u in _new;
+ if {
+ case true => assert v in _new - saveNew ==> v != null && fresh(v);
+ case true => assert !fresh(v) ==> v !in _new;
+ case true => assert v in _new; // error: it may be, but, then again, it may not be
+ }
+}
+
+static method SomeMethod()
+{
+}
+
+static method AnotherMethod() returns (u: Cell, v: Cell)
+ ensures u != null && fresh(u);
+{
+ u := new Cell;
+}
|