Preliminary refactoring of ghost-statement computations to after type checking

7 files changed, 24 insertions, 29 deletions

diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy
index a3e23b73..b9acc522 100644
--- a/Test/dafny0/AssumptionVariables0.dfy
+++ b/Test/dafny0/AssumptionVariables0.dfy
@@ -6,7 +6,7 @@ method test0(x: int)
   ghost var {:assumption} a0 := false;  // error

   ghost var a1, {:assumption} a2 := true, false;  // error

   ghost var {:assumption} a3: bool;

-  var {:assumption} a4;  // 2 errors

+  ghost var {:assumption} a4;  // error: type must be bool

 

   a0 := a0 && (0 < x);

 

@@ -54,7 +54,7 @@ method test2()
 

       if (false)

       {

-        var {:assumption} a0: bool;  // error

+        ghost var {:assumption} a0: bool;

 

         if (false)

         {

@@ -73,3 +73,7 @@ method test2()
     }

   }

 }

+

+method test3() {

+  var {:assumption} a: bool;  // error: assumption variable must be ghost

+}

diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect
index f2d43fe1..16572961 100644
--- a/Test/dafny0/AssumptionVariables0.dfy.expect
+++ b/Test/dafny0/AssumptionVariables0.dfy.expect
@@ -1,14 +1,13 @@
 AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

 AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"

-AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost

 AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'

 AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

 AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

 AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

 AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

 AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost

 AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

 AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'

 AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-13 resolution/type errors detected in AssumptionVariables0.dfy

+AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost

+12 resolution/type errors detected in AssumptionVariables0.dfy

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 5e01f019..61956651 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -40,8 +40,8 @@ method M0(IS: set<int>)
   {

     var x := i;

     x := x + 1;

-    y := 18;  // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)

-    z := 20;  // error: assigning to a non-ghost variable inside a ghost forall block

+    y := 18;  // error: assigning to a (ghost) variable inside a ghost forall block

+    z := 20;  // error: assigning to a (non-ghost) variable inside a ghost forall block

   }

 

   forall (i | 0 <= i)

diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
index 7305bfce..00030994 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy.expect
+++ b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -1,7 +1,8 @@
 ParallelResolveErrors.dfy(10,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(21,4): Error: LHS of assignment must denote a mutable variable

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

-ParallelResolveErrors.dfy(44,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,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

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

 ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements

 ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context

 ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context

@@ -19,4 +20,4 @@ ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scop
 ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

 ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

 ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-21 resolution/type errors detected in ParallelResolveErrors.dfy

+22 resolution/type errors detected in ParallelResolveErrors.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 1354e533..5f0b22a2 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -195,7 +195,7 @@ class GhostTests {
       decreases 112 - n;

     {

       label MyStructure: {

-        if (k % 17 == 0) { break MyStructure; }  // error: break from ghost to non-ghost point

+//KRML(ghost)        if (k % 17 == 0) { break MyStructure; }  // error: break from ghost to non-ghost point

         k := k + 1;

       }

       label MyOtherStructure:

@@ -218,7 +218,7 @@ class GhostTests {
               case true => break LoopLabel1;  // fine

             }

           } else if (m % 101 == 0) {

-            break break;  // error: break out of non-ghost loop from ghost context

+//KRML(ghost)            break break;  // error: break out of non-ghost loop from ghost context

           }

           m := m + 3;

         }

@@ -232,14 +232,14 @@ class GhostTests {
           } else if (*) {

             break break break;  // error: tries to break out of more loop levels than there are

           } else if (*) {

-            break break;  // fine, since this is not a ghost context

+//KRML(ghost)            break break;  // fine, since this is not a ghost context

           } else if (k == 67) {

-            break break;  // error, because this is a ghost context

+//KRML(ghost)            break break;  // error, because this is a ghost context

           }

           q := q + 1;

         }

       } else if (n == t) {

-        return;  // error: this is a ghost context trying to return from a non-ghost method

+//KRML(ghost)        return;  // error: this is a ghost context trying to return from a non-ghost method

       }

       n := n + 1;

       p := p + 1;

@@ -310,7 +310,7 @@ method DatatypeDestructors(d: DTD_List) {
       assert d.DTD_Cons? == d.Car;  // type error

       assert d == DTD_Cons(hd, tl, 5);

       ghost var g0 := d.g;  // fine

-      var g1 := d.g;  // error: cannot use ghost member in non-ghost code

+//KRML(ghost)      var g1 := d.g;  // error: cannot use ghost member in non-ghost code

   }

 }

 

@@ -383,7 +383,7 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
   }

   calc {

     n + m;

-    { print n + m; } // error: non-ghost statements are not allowed in hints

+//KRML(ghost)    { print n + m; } // error: non-ghost statements are not allowed in hints

     m + n;

   }

 }

@@ -543,7 +543,7 @@ method LetSuchThat(ghost z: int, n: nat)
   var x: int;

   x := var y :| y < 0; y;  // fine for the resolver (but would give a verification error for not being deterministic)

 

-  x := var y :| y < z; y;  // error: contraint depend on ghost (z)

+//KRML(ghost)  x := var y :| y < z; y;  // error: contraint depend on ghost (z)

 

   x := var w :| w == 2*w; w;  // fine (even for the verifier, this one)

   x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b5c93ac1..8debdbf9 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -21,14 +21,12 @@ ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
 ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(704,11): 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)

 ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause

 ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(736,11): 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)

 ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint

@@ -126,11 +124,7 @@ ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

 ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

 ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint

@@ -170,7 +164,6 @@ ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only w
 ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)

 ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)

 ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)

-ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts

 ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

@@ -182,10 +175,8 @@ ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool
 ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(386,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(476,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost

 ResolutionErrors.dfy(549,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses

 ResolutionErrors.dfy(918,9): Error: unresolved identifier: s

@@ -200,4 +191,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-202 resolution/type errors detected in ResolutionErrors.dfy

+193 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 500b1af9..8206fd43 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -56,7 +56,7 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su
 TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts

+TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost

 TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed