Dafny: parallel statements:

- removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases
- also allow old/fresh in ensures clauses of parallel statements
- allow TypeRhs and choose expressions in Call/Proof parallel statements
- disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements)

5 files changed, 259 insertions, 154 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 3d0492a8..379a690a 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -788,36 +788,8 @@ namespace Microsoft.Dafny {
       ResolveAttributes(m.Attributes, false);

 

       // ... continue resolving specification

-      bool twoState = true;

-      if (m.Mod.Expressions.Count == 0 && m.Outs.Count == 0) {

-        // In this special case, the current translation of parallel Call statements would be unsound.

-        // The reason is that the parallel Call statement does not advance the heap, so there had better

-        // not be any way to say that the post-heap is definitely different than the pre-heap.  For example,

-        // the following program, is permitted, would unsoundly verify:

-        //     ghost static method M(y: int)

-        //       ensures exists o: object :: o != null && fresh(o);

-        //     {

-        //       var p := new object;

-        //     }

-        //     method Main() {

-        //       parallel (x) { M(x); }

-        //       assert false;

-        //     }

-        // In fact, here is another method M that together with Main above would yield unsound verification:

-        //     class C { ghost var data: int; }

-        //     ghost static method M(y: int)

-        //       ensures exists c: C :: c != null && c.data != old(c.data);

-        //     {

-        //       var c := new C;

-        //       c.data := c.data + 1;

-        //     }

-        // So, it seems best just to disallow two-state postconditions in these cases.  Perhaps the error

-        // message will not explain enough of the reasons for this restriction, but the restriction does

-        // not seem to rule out any useful programs.

-        twoState = false;

-      }

       foreach (MaybeFreeExpression e in m.Ens) {

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, true);

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool))

         {

@@ -1542,7 +1514,7 @@ namespace Microsoft.Dafny {
           Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);

         }

         foreach (var ens in s.Ens) {

-          ResolveExpression(ens.E, false);  // Note, two-state features are not allowed (see the resolution of method postconditions in this file, and see the X_ examples in Test/dafny0/ParallelResolveErrors.dfy)

+          ResolveExpression(ens.E, true);

           Contract.Assert(ens.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(ens.E.Type, Type.Bool)) {

             Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);

@@ -1597,7 +1569,7 @@ namespace Microsoft.Dafny {
               }

             }

           }

-          CheckParallelBodyRestrictions(s.Body, s.Kind == ParallelStmt.ParBodyKind.Assign);

+          CheckParallelBodyRestrictions(s.Body, s.Kind);

         }

 

       } else if (stmt is MatchStmt) {

@@ -2045,22 +2017,22 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// This method performs some additional checks on the body "stmt" of a parallel statement

+    /// This method performs some additional checks on the body "stmt" of a parallel statement of kind "kind".

     /// </summary>

-    public void CheckParallelBodyRestrictions(Statement stmt, bool allowHeapUpdates) {

+    public void CheckParallelBodyRestrictions(Statement stmt, ParallelStmt.ParBodyKind kind) {

       Contract.Requires(stmt != null);

       if (stmt is PredicateStmt) {

         // cool

       } else if (stmt is PrintStmt) {

         Error(stmt, "print statement is not allowed inside a parallel statement");

       } else if (stmt is BreakStmt) {

-        // this case can be checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack

+        // this case is checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack

       } else if (stmt is ReturnStmt) {

         Error(stmt, "return statement is not allowed inside a parallel statement");

       } else if (stmt is ConcreteSyntaxStatement) {

         var s = (ConcreteSyntaxStatement)stmt;

         foreach (var ss in s.ResolvedStatements) {

-          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

+          CheckParallelBodyRestrictions(ss, kind);

         }

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

@@ -2069,16 +2041,23 @@ namespace Microsoft.Dafny {
           if (scope.ContainsDecl(idExpr.Var)) {

             Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");

           }

-        } else if (!allowHeapUpdates) {

-          Error(stmt, "the body of the enclosing parallel statement may not update heap locations");

+        } else if (kind != ParallelStmt.ParBodyKind.Assign) {

+          Error(stmt, "the body of the enclosing parallel statement is not allowed to update heap locations");

         }

         var rhs = s.Rhs;  // ExprRhs and HavocRhs are fine, but TypeRhs is not

         if (rhs is TypeRhs) {

-          Error(rhs.Tok, "new allocation not supported in parallel statements");

+          if (kind == ParallelStmt.ParBodyKind.Assign) {

+            Error(rhs.Tok, "new allocation not supported in parallel statements");

+          } else {

+            var t = (TypeRhs)rhs;

+            if (t.InitCall != null) {

+              CheckParallelBodyRestrictions(t.InitCall, kind);

+            }

+          }

         } else if (rhs is ExprRhs) {

           var r = ((ExprRhs)rhs).Expr.Resolved;

-          if (r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {

-            Error(r, "set choose operator not supported inside parallel statement");

+          if (kind == ParallelStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {

+            Error(r, "set choose operator not supported inside the enclosing parallel statement");

           }

         }

       } else if (stmt is VarDecl) {

@@ -2092,45 +2071,50 @@ namespace Microsoft.Dafny {
               Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");

             }

           } else {

-            Error(stmt, "the body of the enclosing parallel statement may not update heap locations");

+            Error(stmt, "the body of the enclosing parallel statement is not allowed to update heap locations");

           }

         }

-        if (s.Method.Mod.Expressions.Count != 0) {

-          Error(s, "in the body of a parallel statement, every method called must have an empty modifies list");

+        if (!s.Method.IsGhost) {

+          // The reason for this restriction is that the compiler is going to omit the parallel statement altogether--it has

+          // no effect.  However, print effects are not documented, so to make sure that the compiler does not omit a call to

+          // a method that prints something, all calls to non-ghost methods are disallowed.  (Note, if this restriction

+          // is somehow lifted in the future, then it is still necessary to enforce s.Method.Mod.Expressions.Count != 0 for

+          // calls to non-ghost methods.)

+          Error(s, "the body of the enclosing parallel statement is not allowed to call non-ghost methods");

         }

 

       } else if (stmt is BlockStmt) {

         var s = (BlockStmt)stmt;

         scope.PushMarker();

         foreach (var ss in s.Body) {

-          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

+          CheckParallelBodyRestrictions(ss, kind);

         }

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

         var s = (IfStmt)stmt;

-        CheckParallelBodyRestrictions(s.Thn, allowHeapUpdates);

+        CheckParallelBodyRestrictions(s.Thn, kind);

         if (s.Els != null) {

-          CheckParallelBodyRestrictions(s.Els, allowHeapUpdates);

+          CheckParallelBodyRestrictions(s.Els, kind);

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

+            CheckParallelBodyRestrictions(ss, kind);

           }

         }

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        CheckParallelBodyRestrictions(s.Body, allowHeapUpdates);

+        CheckParallelBodyRestrictions(s.Body, kind);

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

+            CheckParallelBodyRestrictions(ss, kind);

           }

         }

 

@@ -2153,7 +2137,7 @@ namespace Microsoft.Dafny {
         var s = (MatchStmt)stmt;

         foreach (var kase in s.Cases) {

           foreach (var ss in kase.Body) {

-            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

+            CheckParallelBodyRestrictions(ss, kind);

           }

         }

 

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index a936899e..0ab4c953 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1178,7 +1178,7 @@ namespace Microsoft.Dafny {
               }

             }

             // construct an expression (generator) for:  VF' << VF

-            ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap) {

+            ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {

               var decrToks = new List<IToken>();

               var decrTypes = new List<Type>();

               var decrCallee = new List<Bpl.Expr>();

@@ -1187,12 +1187,12 @@ namespace Microsoft.Dafny {
               foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) {

                 decrToks.Add(ee.tok);

                 decrTypes.Add(ee.Type);

-                decrCaller.Add(etran.TrExpr(ee));

+                decrCaller.Add(exprTran.TrExpr(ee));

                 Expression es = Substitute(ee, receiverReplacement, substMap);

                 es = Substitute(es, null, decrSubstMap);

-                decrCallee.Add(etran.TrExpr(es));

+                decrCallee.Add(exprTran.TrExpr(es));

               }

-              return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, etran, null, null, false, true);

+              return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, exprTran, null, null, false, true);

             };

 

 #if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE

@@ -2906,7 +2906,7 @@ namespace Microsoft.Dafny {
           etran.InMethodContext());

         req.Add(Requires(m.tok, true, context, null, null));

       }

-      mod.Add(etran.HeapExpr);

+      mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);

       mod.Add(etran.Tick());

 

       if (kind != 0) {

@@ -3665,7 +3665,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap);

+    delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);

 

     void TrParallelCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,

       Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {

@@ -3693,9 +3693,13 @@ namespace Microsoft.Dafny {
       //     Tr( Call );

       //     assume false;

       //   } else {

-      //     assume (forall x,y :: Range(x,y) && additionalRange ==> Post( E(x,y), Args(x,y) ));

+      //     initHeap := $Heap;

+      //     advance $Heap, Tick;

+      //     assume (forall x,y :: (Range(x,y) && additionalRange)[INIT] &&

+      //                           ==> Post[old($Heap) := initHeap]( E(x,y)[INIT], Args(x,y)[INIT] ));

       //   }

-      // where Post(this,args) is the postcondition of method M.

+      // where Post(this,args) is the postcondition of method M and

+      // INIT is the substitution [old($Heap),$Heap := old($Heap),initHeap].

 

       if (definedness != null) {

         // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

@@ -3713,7 +3717,7 @@ namespace Microsoft.Dafny {
         TrStmt_CheckWellformed(range, definedness, locals, etran, false);

         definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

         if (additionalRange != null) {

-          var es = additionalRange(new Dictionary<IVariable, Expression>());

+          var es = additionalRange(new Dictionary<IVariable, Expression>(), etran);

           definedness.Add(new Bpl.AssumeCmd(es.tok, es));

         }

 

@@ -3724,24 +3728,51 @@ namespace Microsoft.Dafny {
 

       // Now for the other branch, where the postcondition of the call is exported.

       {

+        var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));

+        otherTmpVarCount++;

+        locals.Add(initHeapVar);

+        var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar);

+        var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

+        // initHeap := $Heap;

+        exporter.Add(Bpl.Cmd.SimpleAssign(tok, initHeap, etran.HeapExpr));

+        if (s0.Method.Ens.Exists(ens => MentionsOldState(ens.E))) {

+          // advance $Heap, Tick;

+          exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, 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));

+            }

+          }

+        } 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())));

+        }

+

         var bvars = new Bpl.VariableSeq();

         Dictionary<IVariable, Expression> substMap;

-        var ante = etran.TrBoundVariablesRename(boundVars, bvars, out substMap);

-        ante = BplAnd(ante, etran.TrExpr(Substitute(range, null, substMap)));

+        var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);

+        ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap)));

         if (additionalRange != null) {

-          ante = BplAnd(ante, additionalRange(substMap));

+          ante = BplAnd(ante, additionalRange(substMap, initEtran));

         }

 

+        // Note, in the following, we need to do a bit of a song and dance.  The actual arguements of the

+        // call should be translated using "initEtran", whereas the method postcondition should be translated

+        // using "callEtran".  To accomplish this, we translate the argument and then tuck the resulting

+        // Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution.

+        // TODO

         var argsSubstMap = new Dictionary<IVariable, Expression>();  // maps formal arguments to actuals

         Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);

         for (int i = 0; i < s0.Method.Ins.Count; i++) {

-          argsSubstMap.Add(s0.Method.Ins[i], s0.Args[i]);

+          var arg = Substitute(s0.Args[i], null, substMap);  // substitute the renamed bound variables for the declared ones

+          argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));

         }

+        var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap)), s0.Receiver.Type);

+        var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap);

         Bpl.Expr post = Bpl.Expr.True;

         foreach (var ens in s0.Method.Ens) {

-          var p = Substitute(ens.E, s0.Receiver, argsSubstMap);  // substitute the call's actuals for the method's formals

-          p = Substitute(p, null, substMap);  // substitute the renamed bound variables for the declared ones

-          post = BplAnd(post, etran.TrExpr(p));

+          var p = Substitute(ens.E, receiver, argsSubstMap);  // substitute the call's actuals for the method's formals

+          post = BplAnd(post, callEtran.TrExpr(p));

         }

 

         Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post));

@@ -3767,7 +3798,9 @@ namespace Microsoft.Dafny {
       //     assert Post;

       //     assume false;

       //   } else {

-      //     assume (forall x,y :: Range(x,y) ==> Post(x,y));

+      //     initHeap := $Heap;

+      //     advance $Heap, Tick;

+      //     assume (forall x,y :: Range(x,y)[old($Heap),$Heap := old($Heap),initHeap] ==> Post(x,y));

       //   }

 

       // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

@@ -3804,11 +3837,31 @@ namespace Microsoft.Dafny {
 

       // Now for the other branch, where the ensures clauses are exported.

 

+      var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));

+      otherTmpVarCount++;

+      locals.Add(initHeapVar);

+      var initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);

+      var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

+      // initHeap := $Heap;

+      exporter.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr));

+      if (s.Ens.Exists(ens => MentionsOldState(ens.E))) {

+        // advance $Heap;

+        exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick())));

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, new List<FrameExpression>(), initEtran, etran, initEtran)) {

+          if (tri.IsFree) {

+            exporter.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

+          }

+        }

+      } else {

+        // As an optimization, create the illusion that the $Heap is unchanged by the parallel body.

+        exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq(etran.Tick())));

+      }

+

       bvars = new Bpl.VariableSeq();

       Dictionary<IVariable, Expression> substMap;

-      ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);

+      ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);

       var range = Substitute(s.Range, null, substMap);

-      ante = BplAnd(ante, etran.TrExpr(range));

+      ante = BplAnd(ante, initEtran.TrExpr(range));

 

       Bpl.Expr post = Bpl.Expr.True;

       foreach (var ens in s.Ens) {

@@ -5039,6 +5092,19 @@ namespace Microsoft.Dafny {
         Contract.Requires(heap != null);

       }

 

+      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Bpl.Expr oldHeap)

+        : this(translator, predef, heap, "this") {

+        Contract.Requires(translator != null);

+        Contract.Requires(predef != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(oldHeap != null);

+

+        var old = new ExpressionTranslator(translator, predef, oldHeap);

+        old.oldEtran = old;

+        this.oldEtran = old;

+

+      }

+

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)

         : this(translator, predef, heap, thisVar, null, 0, "$_Frame") {

         Contract.Requires(translator != null);

@@ -5060,6 +5126,7 @@ namespace Microsoft.Dafny {
 

           if (oldEtran == null) {

             oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);

+            oldEtran.oldEtran = oldEtran;

           }

           return oldEtran;

         }

@@ -6968,6 +7035,22 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Returns true iff 'expr' is a two-state expression, that is, if it mentions "old(...)" or "fresh(...)".

+    /// </summary>

+    static bool MentionsOldState(Expression expr) {

+      Contract.Requires(expr != null);

+      if (expr is OldExpr || expr is FreshExpr) {

+        return true;

+      }

+      foreach (var ee in expr.SubExpressions) {

+        if (MentionsOldState(ee)) {

+          return true;

+        }

+      }

+      return false;

+    }

+

     public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3be192cc..73c24335 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1019,24 +1019,21 @@ Execution trace:
 Dafny program verifier finished with 27 verified, 6 errors

 

 -------------------- ParallelResolveErrors.dfy --------------------

-ParallelResolveErrors.dfy(8,6): Error: LHS of assignment must denote a mutable variable or field

-ParallelResolveErrors.dfy(13,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

-ParallelResolveErrors.dfy(31,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(43,13): Error: set choose operator not supported inside parallel statement

-ParallelResolveErrors.dfy(48,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(60,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(64,18): Error: return statement is not allowed inside a parallel statement

-ParallelResolveErrors.dfy(71,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(94,43): Error: fresh expressions are not allowed in this context

-ParallelResolveErrors.dfy(101,50): Error: old expressions are not allowed in this context

-ParallelResolveErrors.dfy(124,12): Error: old expressions are not allowed in this context

-ParallelResolveErrors.dfy(144,45): Error: fresh expressions are not allowed in this context

-17 resolution/type errors detected in ParallelResolveErrors.dfy

+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field

+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement

+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements

+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods

+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement

+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop

+14 resolution/type errors detected in ParallelResolveErrors.dfy

 

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

@@ -1116,8 +1113,28 @@ Execution trace:
     (0,0): anon19_Then

     (0,0): anon20_Then

     (0,0): anon5

+Parallel.dfy(214,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+Parallel.dfy(226,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+Parallel.dfy(254,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon5

+Parallel.dfy(270,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon5

 

-Dafny program verifier finished with 24 verified, 8 errors

+Dafny program verifier finished with 34 verified, 12 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 539974fd..24f85e5d 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -53,7 +53,7 @@ method ParallelStatement_Resolve(
   }

 }

 

-method Lemma(c: C, x: int, y: int)

+ghost method Lemma(c: C, x: int, y: int)

   requires c != null;

   ensures c.data <= x+y;

 ghost method PowerLemma(x: int, y: int)

@@ -198,3 +198,74 @@ method OmittedRange() {
     DontDoMuch(x);

   }

 }

+

+// ----------------------- two-state postconditions ---------------------------------

+

+class TwoState_C { ghost var data: int; }

+

+ghost static method TwoState0(y: int)

+  ensures exists o: TwoState_C :: o != null && fresh(o);

+{

+  var p := new TwoState_C;

+}

+

+method TwoState_Main0() {

+  parallel (x) { TwoState0(x); }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+ghost static method TwoState1(y: int)

+  ensures exists c: TwoState_C :: c != null && c.data != old(c.data);

+{

+  var c := new TwoState_C;

+  c.data := c.data + 1;

+}

+

+method TwoState_Main1() {

+  parallel (x) { TwoState1(x); }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+method X_Legit(c: TwoState_C)

+  requires c != null;

+  modifies c;

+{

+  c.data := c.data + 1;

+  parallel (x | c.data <= x)

+    ensures old(c.data) < x;  // note that the 'old' refers to the method's initial state

+  {

+  }

+}

+

+// At first glance, this looks like a version of TwoState_Main0 above, but with an

+// ensures clause.

+// However, there's an important difference in the translation, which is that the

+// occurrence of 'fresh' here refers to the initial state of the TwoStateMain2

+// method, not the beginning of the 'parallel' statement.

+// Still, care needs to be taken in the translation to make sure that the parallel

+// statement's effect on the heap is not optimized away.

+method TwoState_Main2()

+{

+  parallel (x: int)

+    ensures exists o: TwoState_C :: o != null && fresh(o);

+  {

+    TwoState0(x);

+  }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+// At first glance, this looks like an inlined version of TwoState_Main0 above.

+// However, there's an important difference in the translation, which is that the

+// occurrence of 'fresh' here refers to the initial state of the TwoStateMain3

+// method, not the beginning of the 'parallel' statement.

+// Still, care needs to be taken in the translation to make sure that the parallel

+// statement's effect on the heap is not optimized away.

+method TwoState_Main3()

+{

+  parallel (x: int)

+    ensures exists o: TwoState_C :: o != null && fresh(o);

+  {

+    var p := new TwoState_C;

+  }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 9afa311a..98f1ae3a 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -1,5 +1,14 @@
 class C {

   var data: int;

+  ghost var gdata: int;

+  ghost method Init_ModifyNothing() { }

+  ghost method Init_ModifyThis() modifies this;

+  {

+    data := 6;  // error: assignment to a non-ghost field

+    gdata := 7;

+  }

+  ghost method Init_ModifyStuff(c: C) modifies this, c; { }

+  method NonGhostMethod() { print "hello\n"; }

 }

 

 method M0(IS: set<int>)

@@ -50,7 +59,12 @@ method M0(IS: set<int>)
   parallel (i | 0 <= i < 20)

     ensures true;

   {

-    var c := new C;  // error: new allocation not allowed

+    var c := new C;  // allowed

+    var d := new C.Init_ModifyNothing();

+    var e := new C.Init_ModifyThis();

+    var f := new C.Init_ModifyStuff(e);

+    c.Init_ModifyStuff(d);

+    c.NonGhostMethod();  // error: only allowed to call ghost methods (because of possible 'print' statements, sigh)

   }

 }

 

@@ -85,67 +99,3 @@ method M1() {
     }

   }

 }

-

-// -------------------------------------------------------------------------------------

-// Some soundness considerations

-// -------------------------------------------------------------------------------------

-

-ghost static method X_M0(y: int)

-  ensures exists o: object :: o != null && fresh(o);  // error: not allowed 'fresh' here

-{

-  var p := new object;

-}

-

-class X_C { ghost var data: int; }

-ghost static method X_M1(y: int)

-  ensures exists c: X_C :: c != null && c.data != old(c.data);  // error: not allowed 'old' here

-{

-  var c := new X_C;

-  c.data := c.data + 1;

-}

-

-method X_Main() {

-  if (*) {

-    parallel (x) { X_M0(x); }

-  } else {

-    parallel (x) { X_M1(x); }

-  }

-  assert false;

-}

-

-

-// The following seems to be a legitimate use of a two-state predicate in the postcondition of the parallel statement

-method X_Legit(c: X_C)

-  requires c != null;

-  modifies c;

-{

-  c.data := c.data + 1;

-  parallel (x | c.data <= x)

-    ensures old(c.data) < x;  // error: not allowed 'old' here

-  {

-  }

-}

-

-// X_M2 is like X_M0, but with an out-parameter

-ghost static method X_M2(y: int) returns (r: int)

-  ensures exists o: object :: o != null && fresh(o);  // 'fresh' is allowed here (because there's something coming "out" of this ghost method, namely 'r'

-{

-  var p := new object;

-}

-

-// The following method exhibits a case where M2 and a two-state parallel ensures would lead to an unsoundness

-// with the current translation.

-method X_AnotherMain(c: X_C)

-  requires c != null;

-  modifies c;

-{

-  c.data := c.data + 1;

-  parallel (x: int)

-    ensures exists o: object :: o != null && fresh(o);  // error: not allowed 'fresh' here

-  {

-    var s := X_M2(x);

-  }

-  assert false;

-}

-

-// -------------------------------------------------------------------------------------