Dafny: allow parallel statements with an empty list of bound variables

8 files changed, 102 insertions, 28 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index c2cb9353..6ede64fb 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -907,6 +907,10 @@ namespace Microsoft.Dafny {
         if (s.Kind != ParallelStmt.ParBodyKind.Assign) {

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

           return;

+        } else if (s.BoundVars.Count == 0) {

+          // the bound variables just spell out a single point, so the parallel statement is equivalent to one execution of the body

+          TrStmt(s.Body, indent);

+          return;

         }

         var s0 = (AssignStmt)s.S0;

         if (s0.Rhs is HavocRhs) {

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index a15d236a..5b9689b4 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -941,9 +941,9 @@ PrintStmt<out Statement/*!*/ s>
 ParallelStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      IToken/*!*/ x;

-     List<BoundVar/*!*/> bvars;

-     Attributes attrs;

-     Expression range;

+     List<BoundVar/*!*/> bvars = null;

+     Attributes attrs = null;

+     Expression range = null;

      var ens = new List<MaybeFreeExpression/*!*/>();

      bool isFree;

      Expression/*!*/ e;

@@ -952,8 +952,14 @@ ParallelStmt<out Statement/*!*/ s>
   .)

   "parallel"                                (. x = t; .)

   "("

-  QuantifierDomain<out bvars, out attrs, out range>

-                                            (. if (range == null) { range = new LiteralExpr(x, true); } .)

+  [                                         (. List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; .)

+    QuantifierDomain<out bvarsX, out attrsX, out rangeX>

+                                            (. bvars = bvarsX; attrs = attrsX; range = rangeX;

+                                            .)

+  ]

+                                            (. if (bvars == null) { bvars = new List<BoundVar>(); }

+                                               if (range == null) { range = new LiteralExpr(x, true); }

+                                            .)

   ")"

   {                                         (. isFree = false; .)

     [ "free"                                (. isFree = true; .)

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 35829a15..58dcc262 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1794,7 +1794,7 @@ namespace Microsoft.Dafny {
 

   public class ParallelStmt : Statement

   {

-    public readonly List<BoundVar/*!*/> BoundVars;

+    public readonly List<BoundVar/*!*/> BoundVars;  // note, can be the empty list, in which case Range denotes "true"

     public readonly Expression/*!*/ Range;

     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Ens;

     public readonly Statement Body;  // used only until resolution; afterwards, use BodyAssign

@@ -1826,6 +1826,7 @@ namespace Microsoft.Dafny {
     void ObjectInvariant() {

       Contract.Invariant(BoundVars != null);

       Contract.Invariant(Range != null);

+      Contract.Invariant(BoundVars.Count != 0 || LiteralExpr.IsTrue(Range));

       Contract.Invariant(Ens != null);

       Contract.Invariant(Body != null);

     }

@@ -1835,6 +1836,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(boundVars));

       Contract.Requires(range != null);

+      Contract.Requires(boundVars.Count != 0 || LiteralExpr.IsTrue(range));

       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(body != null);

       this.BoundVars = boundVars;

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index f070c6df..18415db0 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1277,9 +1277,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ParallelStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		IToken/*!*/ x;

-		List<BoundVar/*!*/> bvars;

-		Attributes attrs;

-		Expression range;

+		List<BoundVar/*!*/> bvars = null;

+		Attributes attrs = null;

+		Expression range = null;

 		var ens = new List<MaybeFreeExpression/*!*/>();

 		bool isFree;

 		Expression/*!*/ e;

@@ -1289,8 +1289,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(65);

 		x = t; 

 		Expect(32);

-		QuantifierDomain(out bvars, out attrs, out range);

-		if (range == null) { range = new LiteralExpr(x, true); } 

+		if (la.kind == 1) {

+			List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; 

+			QuantifierDomain(out bvarsX, out attrsX, out rangeX);

+			bvars = bvarsX; attrs = attrsX; range = rangeX;

+			

+		}

+		if (bvars == null) { bvars = new List<BoundVar>(); }

+		if (range == null) { range = new LiteralExpr(x, true); }

+		

 		Expect(33);

 		while (la.kind == 28 || la.kind == 30) {

 			isFree = false; 

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index fab8362f..f98f7cbe 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -574,7 +574,9 @@ namespace Microsoft.Dafny {
       } else if (stmt is ParallelStmt) {

         var s = (ParallelStmt)stmt;

         wr.Write("parallel (");

-        PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);

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

+          PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);

+        }

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

           wr.Write(") ");

         } else {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 0ab4c953..7e44cb44 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3409,23 +3409,31 @@ namespace Microsoft.Dafny {
         var s = (ParallelStmt)stmt;

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

           Contract.Assert(s.Ens.Count == 0);

-          var s0 = (AssignStmt)s.S0;

-          var definedness = new Bpl.StmtListBuilder();

-          var updater = new Bpl.StmtListBuilder();

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

+          if (s.BoundVars.Count == 0) {

+            TrStmt(s.Body, builder, locals, etran);

+          } else {

+            var s0 = (AssignStmt)s.S0;

+            var definedness = new Bpl.StmtListBuilder();

+            var updater = new Bpl.StmtListBuilder();

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

           Contract.Assert(s.Ens.Count == 0);

-          var s0 = (CallStmt)s.S0;

-          var definedness = new Bpl.StmtListBuilder();

-          var exporter = new Bpl.StmtListBuilder();

-          TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, 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));

+          if (s.BoundVars.Count == 0) {

+            TrStmt(s.Body, builder, locals, etran);

+          } else {

+            var s0 = (CallStmt)s.S0;

+            var definedness = new Bpl.StmtListBuilder();

+            var exporter = new Bpl.StmtListBuilder();

+            TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, 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 if (s.Kind == ParallelStmt.ParBodyKind.Proof) {

           var definedness = new Bpl.StmtListBuilder();

@@ -3869,7 +3877,10 @@ namespace Microsoft.Dafny {
         post = BplAnd(post, etran.TrExpr(p));

       }

 

-      Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, bvars, Bpl.Expr.Imp(ante, post));

+      Bpl.Expr qq = Bpl.Expr.Imp(ante, post);

+      if (bvars.Length != 0) {

+        qq = new Bpl.ForallExpr(s.Tok, bvars, qq);

+      }

       exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));

     }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 73c24335..fb716976 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1133,8 +1133,13 @@ Execution trace:
     (0,0): anon0

     (0,0): anon6_Else

     (0,0): anon5

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

 

-Dafny program verifier finished with 34 verified, 12 errors

+Dafny program verifier finished with 41 verified, 13 errors

 

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

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

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 24f85e5d..ac11c1eb 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -269,3 +269,40 @@ method TwoState_Main3()
   }

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

 }

+

+// ------- empty parallel statement -----------------------------------------

+

+var emptyPar: int;

+

+method Empty_Parallel0()

+  modifies this;

+  ensures emptyPar == 8;

+{

+  parallel () {

+    this.emptyPar := 8;

+  }

+}

+

+function EmptyPar_P(x: int): bool

+ghost method EmptyPar_Lemma(x: int)

+  ensures EmptyPar_P(x);

+

+method Empty_Parallel1()

+  ensures EmptyPar_P(8);

+{

+  parallel () {

+    EmptyPar_Lemma(8);

+  }

+}

+

+method Empty_Parallel2()

+{

+  parallel ()

+    ensures exists k :: EmptyPar_P(k);

+  {

+    var y := 8;

+    assume EmptyPar_P(y);

+  }

+  assert exists k :: EmptyPar_P(k);  // yes

+  assert EmptyPar_P(8);  // error: the parallel statement's ensures clause does not promise this

+}