summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl6
-rw-r--r--Source/Dafny/Translator.cs44
-rw-r--r--Test/dafny0/Answer29
-rw-r--r--Test/dafny0/Iterators.dfy49
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<Cell> := [];
+ 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;
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:25:40 +0000