Dafny: implemented compilation of parallel statements

Dafny: beefed up resolution of parallel statements

2 files changed, 228 insertions, 44 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 47f5a98a..23477186 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -895,9 +895,184 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is ParallelStmt) {

         var s = (ParallelStmt)stmt;

-        Error("parallel statements are not yet supported by the Dafny compiler; stay tuned");

-        // TODO

-        

+        if (s.Kind != ParallelStmt.ParBodyKind.Assign) {

+          // Call and Proof have no side effects, so they can simply be optimized away.

+          return;

+        }

+        var s0 = (AssignStmt)s.S0;

+        if (s0.Rhs is HavocRhs) {

+          // The parallel statement says to havoc a bunch of things.  This can be efficiently compiled

+          // into doing nothing.

+          return;

+        }

+        var rhs = ((ExprRhs)s0.Rhs).Expr;

+

+        // Compile:

+        //   parallel (w,x,y,z | Range(w,x,y,z)) {

+        //     LHS(w,x,y,z) := RHS(w,x,y,z);

+        //   }

+        // where w,x,y,z have types seq<W>,set<X>,int,bool and LHS has L-1 top-level subexpressions

+        // (that is, L denotes the number of top-level subexpressions of LHS plus 1),

+        // into:

+        //   var ingredients = new List< L-Tuple >();

+        //   foreach (W w in sq.UniqueElements) {

+        //     foreach (X x in st.Elements) {

+        //       for (BigInteger y = Lo; j < Hi; j++) {

+        //         for (bool z in Helper.AllBooleans) {

+        //           if (Range(w,x,y,z)) {

+        //             ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

+        //           }

+        //         }

+        //       }

+        //     }

+        //   }

+        //   foreach (L-Tuple l in ingredients) {

+        //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

+        //   }

+        //

+        // Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation

+        // here supports arrays only up to 6 dimensions.  This does not seem like a serious practical limitation.

+        // However, it may be more noticeable if the parallel statement supported parallel assignments in its

+        // body.  To support cases where tuples would need more than 8 components, .NET Tuple's would have to

+        // be nested.

+

+        // Temporary names

+        string ingredients = "_ingredients" + tmpVarCount;

+        string tup = "_tup" + tmpVarCount;

+        tmpVarCount++;

+

+        // Compute L

+        int L;

+        string tupleTypeArgs;

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          L = 2;

+          tupleTypeArgs = TypeName(lhs.Obj.Type);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          L = 3;

+          // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

+          tupleTypeArgs = TypeName(lhs.Seq.Type) + ",int";

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          L = 2 + lhs.Indices.Count;

+          if (8 < L) {

+            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in parallel statements");

+            return;

+          }

+          tupleTypeArgs = TypeName(lhs.Array.Type);

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

+            tupleTypeArgs += ",int";

+          }

+        }

+        tupleTypeArgs += "," + TypeName(rhs.Type);

+

+        // declare and construct "ingredients"

+        Indent(indent);

+        wr.WriteLine("var {0} = new List<System.Tuple<{1}>>();", ingredients, tupleTypeArgs);

+

+        var n = s.BoundVars.Count;

+        Contract.Assert(s.Bounds.Count == n);

+        for (int i = 0; i < n; i++) {

+          Indent(indent + i * IndentAmount);

+          var bound = s.Bounds[i];

+          var bv = s.BoundVars[i];

+          if (bound is QuantifierExpr.BoolBoundedPool) {

+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name);

+          } else if (bound is QuantifierExpr.IntBoundedPool) {

+            var b = (QuantifierExpr.IntBoundedPool)bound;

+            wr.Write("for (var @{0} = ", bv.Name);

+            TrExpr(b.LowerBound);

+            wr.Write("; @{0} < ", bv.Name);

+            TrExpr(b.UpperBound);

+            wr.Write("; @{0}++) {{ ", bv.Name);

+          } else if (bound is QuantifierExpr.SetBoundedPool) {

+            var b = (QuantifierExpr.SetBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Set);

+            wr.Write(").Elements) { ");

+          } else if (bound is QuantifierExpr.SeqBoundedPool) {

+            var b = (QuantifierExpr.SeqBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Seq);

+            wr.Write(").UniqueElements) { ");

+          } else {

+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

+          }

+          wr.WriteLine();

+        }

+

+        // if (range) {

+        //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

+        // }

+        Indent(indent + n * IndentAmount);

+        wr.Write("if (");

+        if (s.Range == null) {

+          wr.Write("true");

+        } else {

+          TrExpr(s.Range);

+        }

+        wr.WriteLine(") {");

+

+        Indent(indent + (n + 1) * IndentAmount);

+        wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          TrExpr(lhs.Obj);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          TrExpr(lhs.Seq);

+          wr.Write(", (int)(");

+          TrExpr(lhs.E0);

+          wr.Write(")");

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          TrExpr(lhs.Array);

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            wr.Write(", (int)(");

+            TrExpr(lhs.Indices[i]);

+            wr.Write(")");

+          }

+          wr.WriteLine("] = {0}.Item{1};", tup, L);

+        }

+        wr.Write(", ");

+        TrExpr(rhs);

+        wr.WriteLine("));");

+

+        Indent(indent + n * IndentAmount);

+        wr.WriteLine("}");

+

+        for (int i = n; 0 <= --i; ) {

+          Indent(indent + i * IndentAmount);

+          wr.WriteLine("}");

+        }

+

+        //   foreach (L-Tuple l in ingredients) {

+        //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

+        //   }

+        Indent(indent);

+        wr.WriteLine("foreach (var {0} in {1}) {{", tup, ingredients);

+        Indent(indent + IndentAmount);

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          wr.WriteLine("{0}.Item1.@{1} = {0}.Item2;", tup, lhs.FieldName);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          wr.WriteLine("{0}.Item1[{0}.Item2] = {0}.Item3;", tup);

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          wr.Write("{0}.Item1[");

+          string sep = "";

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            wr.Write("{0}{1}.Item{2}", sep, tup, i + 2);

+            sep = ", ";

+          }

+          wr.WriteLine("] = {0}.Item{1};", tup, L);

+        }

+        Indent(indent);

+        wr.WriteLine("}");

+

       } else if (stmt is ForeachStmt) {

         ForeachStmt s = (ForeachStmt)stmt;

         // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2fa86d5e..43c72000 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -12,7 +12,7 @@ using Microsoft.Boogie;
 namespace Microsoft.Dafny {

   public class Resolver {

     public int ErrorCount = 0;

-    protected virtual void Error(IToken tok, string msg, params object[] args) {

+    void Error(IToken tok, string msg, params object[] args) {

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;

@@ -43,6 +43,16 @@ namespace Microsoft.Dafny {
       Contract.Requires(msg != null);

       Error(e.tok, msg, args);

     }

+    void Warning(IToken tok, string msg, params object[] args) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      ConsoleColor col = Console.ForegroundColor;

+      Console.ForegroundColor = ConsoleColor.Yellow;

+      Console.WriteLine("{0}({1},{2}): Warning: {3}",

+          tok.filename, tok.line, tok.col - 1,

+          string.Format(msg, args));

+      Console.ForegroundColor = col;

+    }

 

     readonly BuiltIns builtIns;

     readonly Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes = new Dictionary<string/*!*/,TopLevelDecl/*!*/>();

@@ -1570,40 +1580,27 @@ namespace Microsoft.Dafny {
         scope.PopMarker();

 

         if (prevErrorCount == ErrorCount) {

-          // check for supported kinds

-          if (s.Ens.Count == 0) {

-            // The supported kinds are Assign and Call.  See if it's one of them.

+          // determine the Kind and run some additional checks on the body

+          if (s.Ens.Count != 0) {

+            // The only supported kind with ensures clauses is Proof.

+            s.Kind = ParallelStmt.ParBodyKind.Proof;

+          } else {

+            // There are two special cases:

+            // * Assign, which is the only kind of the parallel statement that allows a heap update.

+            // * Call, which is a single call statement with no side effects or output parameters.

+            // The effect of Assign and the postcondition of Call will be seen outside the parallel

+            // statement.

             Statement s0 = s.S0;

             if (s0 is AssignStmt) {

-              var lhs = ((AssignStmt)s0).Lhs.Resolved;

-              if (lhs is IdentifierExpr) {

-                Error(s0, "a parallel statement must not update local variables declared outside the parallel body");

-              } else if (lhs is FieldSelectExpr) {

-                // cool

-              } else if (lhs is SeqSelectExpr && ((SeqSelectExpr)lhs).SelectOne) {

-                // cool

-              } else if (lhs is MultiSelectExpr) {

-                // cool

-              } else {

-                Contract.Assert(false);  // unexpected assignment LHS

-              }

-              var rhs = ((AssignStmt)s0).Rhs;  // ExprRhs and HavocRhs are fine, but TypeRhs is not

-              // TODO: Occurrences of Choose in RHS must also be handled or disallowed (this happen when Choose is treated like a method member of the set type)

-              if (rhs is TypeRhs) {

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

-              }

               s.Kind = ParallelStmt.ParBodyKind.Assign;

             } else if (s0 is CallStmt) {

-              CheckNoForeignUpdates(s0);

               s.Kind = ParallelStmt.ParBodyKind.Call;

             } else {

-              Error(s, "the body of an ensures-less parallel statement must be one assignment statement or one call statement");

+              s.Kind = ParallelStmt.ParBodyKind.Proof;

+              Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");

             }

-          } else {

-            // The only supported kind with ensures clauses is Proof.  See if that's what the body really is.

-            CheckNoForeignUpdates(s.Body);

-            s.Kind = ParallelStmt.ParBodyKind.Proof;

           }

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

         }

 

       } else if (stmt is MatchStmt) {

@@ -2064,30 +2061,42 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public void CheckNoForeignUpdates(Statement stmt) {

+    /// <summary>

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

+    /// </summary>

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

       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) {

-        // TODO: 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 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

       } 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) {

-          CheckNoForeignUpdates(ss);

+          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

         }

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

-        var idExpr = s.Lhs as IdentifierExpr;

+        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 {

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

+        } else if (!allowHeapUpdates) {

+          Error(stmt, "the body of the enclosing parallel statement may not 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");

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

+          }

         }

       } else if (stmt is VarDecl) {

         // cool

@@ -2100,7 +2109,7 @@ 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 updated heap locations");

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

           }

         }

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

@@ -2111,34 +2120,34 @@ namespace Microsoft.Dafny {
         var s = (BlockStmt)stmt;

         scope.PushMarker();

         foreach (var ss in s.Body) {

-          CheckNoForeignUpdates(ss);

+          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

         }

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

         var s = (IfStmt)stmt;

-        CheckNoForeignUpdates(s.Thn);

+        CheckParallelBodyRestrictions(s.Thn, allowHeapUpdates);

         if (s.Els != null) {

-          CheckNoForeignUpdates(s.Els);

+          CheckParallelBodyRestrictions(s.Els, allowHeapUpdates);

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        CheckNoForeignUpdates(s.Body);

+        CheckParallelBodyRestrictions(s.Body, allowHeapUpdates);

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }

 

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

         foreach (var kase in s.Cases) {

           foreach (var ss in kase.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }