Dafny: fixed lack of assign-such-that restriction in parallel statement

3 files changed, 27 insertions, 9 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 93ed3b4a..adf530aa 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2097,6 +2097,11 @@ namespace Microsoft.Dafny {
         // 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 AssignSuchThatStmt) {

+        var s = (AssignSuchThatStmt)stmt;

+        foreach (var lhs in s.Lhss) {

+          CheckParallelBodyLhs(s.Tok, lhs.Resolved, kind);

+        }

       } else if (stmt is ConcreteSyntaxStatement) {

         var s = (ConcreteSyntaxStatement)stmt;

         foreach (var ss in s.ResolvedStatements) {

@@ -2104,14 +2109,7 @@ namespace Microsoft.Dafny {
         }

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

-        var idExpr = s.Lhs.Resolved as IdentifierExpr;

-        if (idExpr != null) {

-          if (scope.ContainsDecl(idExpr.Var)) {

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

-          }

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

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

-        }

+        CheckParallelBodyLhs(s.Tok, s.Lhs.Resolved, kind);

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

         if (rhs is TypeRhs) {

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

@@ -2214,6 +2212,17 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void CheckParallelBodyLhs(IToken tok, Expression lhs, ParallelStmt.ParBodyKind kind) {

+      var idExpr = lhs as IdentifierExpr;

+      if (idExpr != null) {

+        if (scope.ContainsDecl(idExpr.Var)) {

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

+        }

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

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

+      }

+    }

+

     Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {

       Contract.Requires(rr != null);

       Contract.Requires(stmt != null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 22c24816..589a43e2 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1078,7 +1078,9 @@ ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels
 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

+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause

+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations

+15 resolution/type errors detected in ParallelResolveErrors.dfy

 

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

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

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 98f1ae3a..ab711d02 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -99,3 +99,10 @@ method M1() {
     }

   }

 }

+

+method M2() {

+  var a := new int[100];

+  parallel (x | 0 <= x < 100) {

+    a[x] :| a[x] > 0;  // error: not allowed to update heap location in a parallel statement with a(n implicit) assume

+  }

+}