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)

3 files changed, 123 insertions, 85 deletions

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;

-}

-

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