diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 423 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 36 | ||||
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 95 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny1/Queue.dfy | 4 |
6 files changed, 373 insertions, 191 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 45817bdc..52449d81 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3348,159 +3348,24 @@ namespace Microsoft.Dafny { if (s.Kind == ParallelStmt.ParBodyKind.Assign) {
Contract.Assert(s.Ens.Count == 0);
var s0 = (AssignStmt)s.S0;
-
- // The statement:
- // parallel (x,y | Range(x,y)) {
- // (a) E(x,y) . f := G(x,y);
- // (b) A(x,y) [ I0(x,y), I1(x,y), ... ] := G(x,y);
- // }
- // translate into:
- // if (*) {
- // // check definedness of Range
- // var x,y;
- // havoc x,y;
- // CheckWellDefined( Range );
- // assume Range;
- // // check definedness of the other expressions
- // (a)
- // CheckWellDefined( E.F );
- // check that E.f is in the modifies frame;
- // CheckWellDefined( G );
- // check nat restrictions for the RHS
- // (b)
- // CheckWellDefined( A[I0,I1,...] );
- // check that A[I0,I1,...] is in the modifies frame;
- // CheckWellDefined( G );
- // check nat restrictions for the RHS
- // // check for duplicate LHSs
- // var x', y';
- // havoc x', y';
- // assume Range[x,y := x',y'];
- // assume !(x == x' && y == y');
- // (a)
- // assert E(x,y) != E(x',y');
- // (b)
- // assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... );
- //
- // assume false;
- //
- // } else {
- // var oldHeap := $Heap;
- // havoc $Heap;
- // assume $HeapSucc(oldHeap, $Heap);
- // (a)
- // assume (forall<alpha> o: ref, F: Field alpha ::
- // $Heap[o,F] = oldHeap[o,F] ||
- // (exists x,y :: Range(x,y) && o == E(x,y) && F = f));
- // assume (forall x,y :: Range ==> $Heap[ E[$Heap:=oldHeap], F] == G[$Heap:=oldHeap]);
- // (b)
- // assume (forall<alpha> o: ref, F: Field alpha ::
- // $Heap[o,F] = oldHeap[o,F] ||
- // (exists x,y :: Range(x,y) && o == A(x,y) && F = Index(I0,I1,...)));
- // assume (forall x,y :: Range ==> $Heap[ A[$Heap:=oldHeap], Index(I0,I1,...)] == G[$Heap:=oldHeap]);
- // }
-
- var definedness = new StmtListBuilder();
- var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
- if (s.Range != null) {
- Expression range = Substitute(s.Range, null, substMap);
- TrStmt_CheckWellformed(range, definedness, locals, etran, false);
- definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range)));
- }
-
- var lhs = Substitute(s0.Lhs.Resolved, null, substMap);
- TrStmt_CheckWellformed(lhs, definedness, locals, etran, false);
- Bpl.Expr obj, F;
- string description = GetObjFieldDetails(lhs, etran, out obj, out F);
- definedness.Add(Assert(lhs.tok, Bpl.Expr.SelectTok(lhs.tok, etran.TheFrame(lhs.tok), obj, F),
- "assignment may update " + description + " not in the enclosing context's modifies clause"));
- if (s0.Rhs is ExprRhs) {
- var rhs = Substitute(((ExprRhs)s0.Rhs).Expr, null, substMap);
- TrStmt_CheckWellformed(rhs, definedness, locals, etran, false);
- // TODO: check nat restrictions for the RHS
- }
-
- // check for duplicate LHSs
- var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
- var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);
- if (s.Range != null) {
- Expression range = Substitute(s.Range, null, substMapPrime);
- definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));
- }
- // assume !(x == x' && y == y');
- Bpl.Expr eqs = Bpl.Expr.True;
- foreach (var bv in s.BoundVars) {
- var x = substMap[bv];
- var xPrime = substMapPrime[bv];
- // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too?
- eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime)));
- }
- definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));
- Bpl.Expr objPrime, FPrime;
- GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);
- definedness.Add(Assert(s0.Tok,
- Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),
- "left-hand sides for different parallel-statement bound variables may refer to the same location"));
-
- definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
-
- // Now for the translation of the update itself
-
+ var definedness = new Bpl.StmtListBuilder();
var updater = new Bpl.StmtListBuilder();
- Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(stmt.Tok, locals);
- var prevEtran = new ExpressionTranslator(this, predef, prevHeap);
- updater.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, prevHeap, etran.HeapExpr));
- updater.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
- updater.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));
-
- // Here comes:
- // assume (forall<alpha> o: ref, f: Field alpha ::
- // $Heap[o,f] = oldHeap[o,f] ||
- // (exists x,y :: Range(x,y)[$Heap:=oldHeap] &&
- // o == Object(x,y)[$Heap:=oldHeap] && f == Field(x,y)[$Heap:=oldHeap]));
- Bpl.TypeVariable alpha = new Bpl.TypeVariable(stmt.Tok, "alpha");
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$o", predef.RefType));
- Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
- Bpl.BoundVariable fVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$f", predef.FieldName(stmt.Tok, alpha)));
- Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
- Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, f);
- Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(stmt.Tok, prevHeap, o, f);
- Bpl.VariableSeq xBvars = new Bpl.VariableSeq();
- var xBody = etran.TrBoundVariables(s.BoundVars, xBvars);
- if (s.Range != null) {
- xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range));
- }
- Bpl.Expr xObj, xField;
- GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
- xBody = BplAnd(xBody, Bpl.Expr.Eq(o, xObj));
- xBody = BplAnd(xBody, Bpl.Expr.Eq(f, xField));
- Bpl.Expr xObjField = new Bpl.ExistsExpr(s.Tok, xBvars, xBody);
- Bpl.Expr body = Bpl.Expr.Or(Bpl.Expr.Eq(heapOF, oldHeapOF), xObjField);
- Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
- updater.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
-
- if (s0.Rhs is ExprRhs) {
- // assume (forall x,y :: Range(x,y)[$Heap:=oldHeap] ==>
- // $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] ));
- xBvars = new Bpl.VariableSeq();
- Bpl.Expr xAnte = etran.TrBoundVariables(s.BoundVars, xBvars);
- if (s.Range != null) {
- xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range));
- }
- GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
- var xHeapOF = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, xObj, xField);
- var g = prevEtran.TrExpr(((ExprRhs)s0.Rhs).Expr);
- qq = new Bpl.ForallExpr(stmt.Tok, xBvars, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));
- updater.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
- }
+ TrParallelAssign(s, s0, definedness, updater, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, updater.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
} else if (s.Kind == ParallelStmt.ParBodyKind.Call) {
// TODO: call forall
+
} else if (s.Kind == ParallelStmt.ParBodyKind.Proof) {
- // TODO
+ var definedness = new Bpl.StmtListBuilder();
+ var exporter = new Bpl.StmtListBuilder();
+ TrParallelProof(s, definedness, exporter, locals, etran);
+ // All done, so put the two pieces together
+ builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
+ builder.Add(CaptureState(stmt.Tok));
+
} else {
Contract.Assert(false); // unexpected kind
}
@@ -3573,6 +3438,240 @@ namespace Microsoft.Dafny { }
}
+ void TrParallelAssign(ParallelStmt s, AssignStmt s0,
+ Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ // The statement:
+ // parallel (x,y | Range(x,y)) {
+ // (a) E(x,y) . f := G(x,y);
+ // (b) A(x,y) [ I0(x,y), I1(x,y), ... ] := G(x,y);
+ // }
+ // translate into:
+ // if (*) {
+ // // check definedness of Range
+ // var x,y;
+ // havoc x,y;
+ // CheckWellDefined( Range );
+ // assume Range;
+ // // check definedness of the other expressions
+ // (a)
+ // CheckWellDefined( E.F );
+ // check that E.f is in the modifies frame;
+ // CheckWellDefined( G );
+ // check nat restrictions for the RHS
+ // (b)
+ // CheckWellDefined( A[I0,I1,...] );
+ // check that A[I0,I1,...] is in the modifies frame;
+ // CheckWellDefined( G );
+ // check nat restrictions for the RHS
+ // // check for duplicate LHSs
+ // var x', y';
+ // havoc x', y';
+ // assume Range[x,y := x',y'];
+ // assume !(x == x' && y == y');
+ // (a)
+ // assert E(x,y) != E(x',y');
+ // (b)
+ // assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... );
+ //
+ // assume false;
+ //
+ // } else {
+ // var oldHeap := $Heap;
+ // havoc $Heap;
+ // assume $HeapSucc(oldHeap, $Heap);
+ // (a)
+ // assume (forall<alpha> o: ref, F: Field alpha ::
+ // $Heap[o,F] = oldHeap[o,F] ||
+ // (exists x,y :: Range(x,y) && o == E(x,y) && F = f));
+ // assume (forall x,y :: Range ==> $Heap[ E[$Heap:=oldHeap], F] == G[$Heap:=oldHeap]);
+ // (b)
+ // assume (forall<alpha> o: ref, F: Field alpha ::
+ // $Heap[o,F] = oldHeap[o,F] ||
+ // (exists x,y :: Range(x,y) && o == A(x,y) && F = Index(I0,I1,...)));
+ // assume (forall x,y :: Range ==> $Heap[ A[$Heap:=oldHeap], Index(I0,I1,...)] == G[$Heap:=oldHeap]);
+ // }
+
+ var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
+ if (s.Range != null) {
+ Expression range = Substitute(s.Range, null, substMap);
+ TrStmt_CheckWellformed(range, definedness, locals, etran, false);
+ definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range)));
+ }
+
+ var lhs = Substitute(s0.Lhs.Resolved, null, substMap);
+ TrStmt_CheckWellformed(lhs, definedness, locals, etran, false);
+ Bpl.Expr obj, F;
+ string description = GetObjFieldDetails(lhs, etran, out obj, out F);
+ definedness.Add(Assert(lhs.tok, Bpl.Expr.SelectTok(lhs.tok, etran.TheFrame(lhs.tok), obj, F),
+ "assignment may update " + description + " not in the enclosing context's modifies clause"));
+ if (s0.Rhs is ExprRhs) {
+ var r = (ExprRhs)s0.Rhs;
+ var rhs = Substitute(r.Expr, null, substMap);
+ TrStmt_CheckWellformed(rhs, definedness, locals, etran, false);
+ // TODO: check nat restrictions for the RHS
+ // CheckSubrange(rhs.tok, bRhs, checkSubrangeType, definedness);
+ }
+
+ // check for duplicate LHSs
+ var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
+ var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);
+ if (s.Range != null) {
+ Expression range = Substitute(s.Range, null, substMapPrime);
+ definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));
+ }
+ // assume !(x == x' && y == y');
+ Bpl.Expr eqs = Bpl.Expr.True;
+ foreach (var bv in s.BoundVars) {
+ var x = substMap[bv];
+ var xPrime = substMapPrime[bv];
+ // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too?
+ eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime)));
+ }
+ definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));
+ Bpl.Expr objPrime, FPrime;
+ GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);
+ definedness.Add(Assert(s0.Tok,
+ Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),
+ "left-hand sides for different parallel-statement bound variables may refer to the same location"));
+
+ definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+
+ // Now for the translation of the update itself
+
+ Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(s.Tok, locals);
+ var prevEtran = new ExpressionTranslator(this, predef, prevHeap);
+ updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr));
+ updater.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
+ updater.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));
+
+ // Here comes:
+ // assume (forall<alpha> o: ref, f: Field alpha ::
+ // $Heap[o,f] = oldHeap[o,f] ||
+ // (exists x,y :: Range(x,y)[$Heap:=oldHeap] &&
+ // o == Object(x,y)[$Heap:=oldHeap] && f == Field(x,y)[$Heap:=oldHeap]));
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(s.Tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(s.Tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$f", predef.FieldName(s.Tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(s.Tok, fVar);
+ Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(s.Tok, etran.HeapExpr, o, f);
+ Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(s.Tok, prevHeap, o, f);
+ Bpl.VariableSeq xBvars = new Bpl.VariableSeq();
+ var xBody = etran.TrBoundVariables(s.BoundVars, xBvars);
+ if (s.Range != null) {
+ xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range));
+ }
+ Bpl.Expr xObj, xField;
+ GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
+ xBody = BplAnd(xBody, Bpl.Expr.Eq(o, xObj));
+ xBody = BplAnd(xBody, Bpl.Expr.Eq(f, xField));
+ Bpl.Expr xObjField = new Bpl.ExistsExpr(s.Tok, xBvars, xBody);
+ Bpl.Expr body = Bpl.Expr.Or(Bpl.Expr.Eq(heapOF, oldHeapOF), xObjField);
+ Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
+ updater.Add(new Bpl.AssumeCmd(s.Tok, qq));
+
+ if (s0.Rhs is ExprRhs) {
+ // assume (forall x,y :: Range(x,y)[$Heap:=oldHeap] ==>
+ // $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] ));
+ xBvars = new Bpl.VariableSeq();
+ Bpl.Expr xAnte = etran.TrBoundVariables(s.BoundVars, xBvars);
+ if (s.Range != null) {
+ xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range));
+ }
+ var rhs = ((ExprRhs)s0.Rhs).Expr;
+ var g = prevEtran.TrExpr(rhs);
+ GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
+ var xHeapOF = ExpressionTranslator.ReadHeap(s.Tok, etran.HeapExpr, xObj, xField);
+
+ Type lhsType;
+ if (lhs is FieldSelectExpr) {
+ lhsType = ((FieldSelectExpr)lhs).Type;
+ } else {
+ lhsType = null;
+ }
+ g = etran.CondApplyBox(rhs.tok, g, rhs.Type, lhsType);
+
+ qq = new Bpl.ForallExpr(s.Tok, xBvars, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));
+ updater.Add(new Bpl.AssumeCmd(s.Tok, qq));
+ }
+ }
+
+ void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ // Translate:
+ // parallel (x,y | Range(x,y))
+ // ensures Post(x,y);
+ // {
+ // Body;
+ // }
+ // as:
+ // if (*) {
+ // var x,y;
+ // havoc x,y;
+ // CheckWellDefined( Range );
+ // assume Range(x,y);
+ // Tr( Body );
+ // CheckWellDefined( Post );
+ // assert Post;
+ // assume false;
+ // } else {
+ // assume (forall x,y :: Range(x,y) ==> Post(x,y));
+ // }
+
+ // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals
+ // here (rather than a TrBoundVariables). However, there is currently no way to apply
+ // a substMap to a statement (in particular, to s.Body), so that doesn't work here.
+ Bpl.VariableSeq bvars = new Bpl.VariableSeq();
+ var ante = etran.TrBoundVariables(s.BoundVars, bvars, true);
+ locals.AddRange(bvars);
+ var havocIds = new Bpl.IdentifierExprSeq();
+ foreach (Bpl.Variable bv in bvars) {
+ havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv));
+ }
+ definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));
+ definedness.Add(new Bpl.AssumeCmd(s.Tok, ante));
+ if (s.Range != null) {
+ TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
+ definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
+ }
+
+ TrStmt(s.Body, definedness, locals, etran);
+
+ // check that postconditions hold
+ foreach (var ens in s.Ens) {
+ TrStmt_CheckWellformed(ens.E, definedness, locals, etran, false);
+ if (!ens.IsFree) {
+ bool splitHappened; // we actually don't care
+ foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
+ if (!split.IsFree) {
+ definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of parallel statement"));
+ }
+ }
+ }
+ }
+
+ definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+
+ // Now for the other branch, where the ensures clauses are exported.
+
+ bvars = new Bpl.VariableSeq();
+ Dictionary<IVariable, Expression> substMap;
+ ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);
+ if (s.Range != null) {
+ var range = Substitute(s.Range, null, substMap);
+ TrStmt_CheckWellformed(range, definedness, locals, etran, false);
+ ante = BplAnd(ante, etran.TrExpr(range));
+ }
+
+ Bpl.Expr post = Bpl.Expr.True;
+ foreach (var ens in s.Ens) {
+ var p = Substitute(ens.E, null, substMap);
+ post = BplAnd(post, etran.TrExpr(p));
+ }
+
+ Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, bvars, Bpl.Expr.Imp(ante, post));
+ exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));
+ }
+
private string GetObjFieldDetails(Expression lhs, ExpressionTranslator etran, out Bpl.Expr obj, out Bpl.Expr F) {
string description;
if (lhs is FieldSelectExpr) {
@@ -5326,12 +5425,22 @@ namespace Microsoft.Dafny { }
public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {
+ return TrBoundVariables(boundVars, bvars, false);
+ }
+
+ public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars, bool translateAsLocals) {
Contract.Requires(boundVars != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
Bpl.Expr typeAntecedent = Bpl.Expr.True;
foreach (BoundVar bv in boundVars) {
- Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));
+ var tid = new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type));
+ Bpl.Variable bvar;
+ if (translateAsLocals) {
+ bvar = new Bpl.LocalVariable(bv.tok, tid);
+ } else {
+ bvar = new Bpl.BoundVariable(bv.tok, tid);
+ }
bvars.Add(bvar);
Bpl.Expr wh = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, bvar), bv.Type, this);
if (wh != null) {
@@ -5341,6 +5450,28 @@ namespace Microsoft.Dafny { return typeAntecedent;
}
+ public Bpl.Expr TrBoundVariablesRename(List<BoundVar> boundVars, Bpl.VariableSeq bvars, out Dictionary<IVariable, Expression> substMap) {
+ Contract.Requires(boundVars != null);
+ Contract.Requires(bvars != null);
+
+ substMap = new Dictionary<IVariable, Expression>();
+ Bpl.Expr typeAntecedent = Bpl.Expr.True;
+ foreach (BoundVar bv in boundVars) {
+ var newBoundVar = new BoundVar(bv.tok, bv.Name, bv.Type);
+ IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.UniqueName);
+ ie.Var = newBoundVar; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(bv, ie);
+ Bpl.Variable bvar = new Bpl.BoundVariable(newBoundVar.tok, new Bpl.TypedIdent(newBoundVar.tok, newBoundVar.UniqueName, translator.TrType(newBoundVar.Type)));
+ bvars.Add(bvar);
+ var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar);
+ Bpl.Expr wh = translator.GetWhereClause(bv.tok, bIe, newBoundVar.Type, this);
+ if (wh != null) {
+ typeAntecedent = translator.BplAnd(typeAntecedent, wh);
+ }
+ }
+ return typeAntecedent;
+ }
+
public ExprSeq FunctionInvocationArguments(FunctionCallExpr e) {
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<ExprSeq>() != null);
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index cd132ef3..612b96ba 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -57,12 +57,12 @@ class Queue<T> { tail.next := n;
tail := n;
- foreach (m in spine) {
+ parallel (m | m in spine) {
m.tailContents := m.tailContents + [t];
}
contents := head.tailContents;
- foreach (m in spine) {
+ parallel (m | m in spine) {
m.footprint := m.footprint + n.footprint;
}
footprint := footprint + n.footprint;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a3e5e11f..4b3d9814 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -947,6 +947,42 @@ Execution trace: Dafny program verifier finished with 27 verified, 6 errors
+-------------------- Parallel.dfy --------------------
+Parallel.dfy(29,18): Error: possible violation of postcondition of parallel statement
+Execution trace:
+ (0,0): anon0
+ (0,0): anon17_Else
+ (0,0): anon7
+ (0,0): anon20_Else
+ (0,0): anon10
+ (0,0): anon21_Then
+ (0,0): anon22_Then
+ (0,0): anon14
+Parallel.dfy(34,19): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon17_Else
+ (0,0): anon7
+ (0,0): anon20_Else
+ (0,0): anon10
+ (0,0): anon21_Then
+ (0,0): anon22_Then
+Parallel.dfy(76,19): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Else
+ (0,0): anon3
+ (0,0): anon11_Then
+Parallel.dfy(82,20): Error: possible violation of postcondition of parallel statement
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Else
+ (0,0): anon3
+ (0,0): anon11_Then
+ (0,0): anon12_Then
+
+Dafny program verifier finished with 12 verified, 4 errors
+
-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(44,22): Error: assertion violation
Execution trace:
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 0928c070..88a67957 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -1,48 +1,16 @@ -/*
-method ParallelStatement_Syntax()
-{
- parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
- a[i] := a[(i + 1) % a.Length] + 3;
- }
-
- parallel (o | o in spine) {
- o.f := o.f + Repr;
- }
-
- parallel (x, y | x in S && 0 <= y+x < 100) {
- Lemma(x, y);
- }
-
- parallel (p | 0 <= p)
- ensures F(p) <= Sum(p) * (p-1) + 100;
- {
- assert G(p);
- ghost var t;
- if (p % 2 == 0) {
- assert G(p) == F(p+2);
- t := p*p;
- } else {
- assume H(p, 20) < 100; // don't know how to justify this
- t := p;
- }
- PowerLemma(p, t);
- t := t + 1;
- PowerLemma(p, t);
- }
-}
-*/
-
class C {
- var f: set<object>;
+ var data: int;
+ var st: set<object>;
}
+// This method more or less just tests the syntax, resolution, and basic verification
method ParallelStatement_Resolve(
a: array<int>,
spine: set<C>,
Repr: set<object>,
S: set<int>
)
- requires a != null;
+ requires a != null && null !in spine;
modifies a, spine;
{
parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
@@ -50,7 +18,7 @@ method ParallelStatement_Resolve( }
parallel (o | o in spine) {
- o.f := o.f + Repr;
+ o.st := o.st + Repr;
}
parallel (x, y | x in S && 0 <= y+x < 100) {
@@ -58,12 +26,12 @@ method ParallelStatement_Resolve( }
parallel (p | 0 <= p)
- ensures F(p) <= Sum(p) * (p-1) + 100;
+ ensures F(p) <= Sum(p) * (p-1) + 100; // error (no connection is known between F and Sum)
{
assert 0 <= G(p);
ghost var t;
if (p % 2 == 0) {
- assert G(p) == F(p+2);
+ assert G(p) == F(p+2); // error (there's nothing that gives any relation between F and G)
t := p*p;
} else {
assume H(p, 20) < 100; // don't know how to justify this
@@ -79,6 +47,53 @@ method Lemma(x: int, y: int) ghost method PowerLemma(x: int, y: int)
function F(x: int): int
-function G(x: int): int
+function G(x: int): nat
function H(x: int, y: int): int
function Sum(x: int): int
+
+// ---------------------------------------------------------------------
+
+method M0(S: set<C>)
+ requires null !in S;
+ modifies S;
+ ensures forall o :: o in S ==> o.data == 85;
+ ensures forall o :: o != null && o !in S ==> o.data == old(o.data);
+{
+ parallel (s | s in S) {
+ s.data := 85;
+ }
+}
+
+method M1(S: set<C>, x: C)
+ requires null !in S && x in S;
+{
+ parallel (s | s in S)
+ ensures s.data < 100;
+ {
+ assume s.data == 85;
+ }
+ if (*) {
+ assert x.data == 85; // error (cannot be inferred from parallel ensures clause)
+ } else {
+ assert x.data < 120;
+ }
+
+ parallel (s | s in S)
+ ensures s.data < 70; // error
+ {
+ assume s.data == 85;
+ }
+}
+
+method M2() returns (a: array<int>)
+ ensures a != null;
+ ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j];
+{
+ a := new int[250];
+ parallel (i: nat | i < 125) {
+ a[i] := 423;
+ }
+ parallel (i | 125 <= i < 250) {
+ a[i] := 300 + i;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index bfa88b54..a670ced5 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -16,7 +16,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
- Termination.dfy DTypes.dfy
+ Termination.dfy DTypes.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index bfb588be..0edfab81 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -85,12 +85,12 @@ class Queue<T> { tail.next := n;
tail := n;
- foreach (m in spine) {
+ parallel (m | m in spine) {
m.tailContents := m.tailContents + [t];
}
contents := head.tailContents;
- foreach (m in spine) {
+ parallel (m | m in spine) {
m.footprint := m.footprint + n.footprint;
}
footprint := footprint + n.footprint;
|