Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

1 files changed, 247 insertions, 31 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 2fab6bf3..d3514b2b 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -102,7 +102,7 @@ class EE {
 }

 

 // --------------- ghost tests -------------------------------------

-

+module HereAreMoreGhostTests {

 datatype GhostDt =

   Nil(ghost extraInfo: int) |

   Cons(data: int, tail: GhostDt, ghost moreInfo: int)

@@ -154,7 +154,7 @@ class GhostTests {
     ensures false;

   {

     while (true)

-      decreases *;  // error:  not allowed in ghost context

+//KRML-confirmed      decreases *;  // error:  not allowed in ghost context

     {

     }

   }

@@ -228,7 +228,7 @@ class GhostTests {
           if (p == 67) {

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

           } else if (*) {

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

+//KRML-confirmed            break break break;  // error: tries to break out of more loop levels than there are

           }

           q := q + 1;

         }

@@ -238,7 +238,7 @@ class GhostTests {
       p := p + 1;

     }

   }

-method BreakMayNotBeFineHere_Ghost(ghost t: int)

+  method BreakMayNotBeFineHere_Ghost(ghost t: int)

   {

     var n := 0;

     ghost var k := 0;

@@ -297,7 +297,7 @@ method BreakMayNotBeFineHere_Ghost(ghost t: int)
     }

   }

 }

-

+} //HereAreMoreGhostTests

 method DuplicateLabels(n: int) {

   var x;

   if (n < 7) {

@@ -364,17 +364,17 @@ method DatatypeDestructors(d: DTD_List) {
   }

 }

 method DatatypeDestructors_Ghost(d: DTD_List) {

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

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

 }

 

 // ------------------- print statements ---------------------------------------

-

+module GhostPrintAttempts {

 method PrintOnlyNonGhosts(a: int, ghost b: int)

 {

   print "a: ", a, "\n";

   print "b: ", b, "\n";  // error: print statement cannot take ghosts

 }

-

+}

 // ------------------- auto-added type arguments ------------------------------

 

 class GenericClass<T> { var data: T; }

@@ -439,11 +439,11 @@ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
 {

   calc {

     n + m;

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

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

     m + n;

   }

 }

-

+module MyOwnModule {

 class SideEffectChecks {

   ghost var ycalc: int;

 

@@ -461,11 +461,11 @@ class SideEffectChecks {
     var x: int;

     calc {

       0;

-      { Mod(0); }     // methods with side-effects are not allowed

+      { Mod(0); }     // error: methods with side-effects are not allowed

       ycalc;

-      { ycalc := 1; } // heap updates are not allowed

+      { ycalc := 1; } // error: heap updates are not allowed

       1;

-      { x := 1; }     // updates to locals defined outside of the hint are not allowed

+      { x := 1; }     // error: updates to locals defined outside of the hint are not allowed

       x;

       {

         var x: int;

@@ -475,7 +475,7 @@ class SideEffectChecks {
     }

   }

 }

-

+}

 // ------------------- nameless constructors ------------------------------

 

 class YHWH {

@@ -523,13 +523,13 @@ method AssignSuchThatFromGhost()
   var x: int;

   ghost var g: int;

 

-  x := g;  // error: ghost cannot flow into non-ghost

+  x := g;  // error: ghost cannot flow into non-ghost//KRML-confirmed

 

   x := *;

   assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,

                   // the compiler will complain)

 

-  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well

+  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed

 

   x :| assume x == g;  // this is cool, since it's an assume (but, of course, the

                        // compiler will complain)

@@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat)
 }

 method LetSuchThat_Ghost(ghost z: int, n: nat)

 {

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

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

 }

 

 // ------------ quantified variables whose types are not inferred ----------

@@ -677,9 +677,9 @@ module GhostAllocationTests {
       5;

       { var y := new G; }  // error: 'new' not allowed in ghost contexts

       2 + 3;

-      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context

+      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context//KRML-confirmed

       1 + 4;

-      { GhostNew5(g); }  // error: cannot call method with nonempty modifies

+      { GhostNew5(g); }  // error: cannot call method with nonempty modifies//KRML-confirmed

       -5 + 10;

     }

   }

@@ -735,7 +735,7 @@ module StatementsInExpressions {
     {

       calc {

         5;

-        { SideEffect(); }  // error: cannot call method with side effects

+        { SideEffect(); }  // error: cannot call method with side effects//KRML

         5;

       }

     }

@@ -745,7 +745,7 @@ module StatementsInExpressions {
       calc {

         6;

         { assert 6 < 8; }

-        { NonGhostMethod(); }  // error: cannot call non-ghost method

+        { NonGhostMethod(); }  // error: cannot call non-ghost method//KRML-confirmed

         { var x := 8;

           while x != 0

             decreases *;  // error: cannot use 'decreases *' in a ghost context

@@ -759,12 +759,12 @@ module StatementsInExpressions {
             x := x - 1;

           }

         }

-        { MyField := 12; }  // error: cannot assign to a field

-        { MyGhostField := 12; }  // error: cannot assign to any field

-        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause

+        { MyField := 12; }  // error: cannot assign to a field//KRML-confirmed

+        { MyGhostField := 12; }  // error: cannot assign to any field//KRML-confirmed

+        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause//KRML-confirmed

         { var x := 8;

           while x != 0

-            modifies this;  // error: cannot use a modifies clause on a loop

+            modifies this;  // error: cannot use a modifies clause on a loop//KRML-confirmed

           {

             x := x - 1;

           }

@@ -783,7 +783,7 @@ module StatementsInExpressions {
       calc {

         6;

         { assert 6 < 8; }

-        { NonGhostMethod(); }  // error: cannot call non-ghost method

+        { NonGhostMethod(); }  // error: cannot call non-ghost method//KRML-confirmed

         { var x := 8;

           while x != 0

             decreases *;  // error: cannot use 'decreases *' in a ghost context

@@ -791,12 +791,12 @@ module StatementsInExpressions {
             x := x - 1;

           }

         }

-        { MyField := 12; }  // error: cannot assign to a field

-        { MyGhostField := 12; }  // error: cannot assign to any field

-        { M(); }  // error: cannot call (ghost) method with a modifies clause

+        { MyField := 12; }  // error: cannot assign to a field//KRML-confirmed

+        { MyGhostField := 12; }  // error: cannot assign to any field//KRML-confirmed

+        { M(); }  // error: cannot call (ghost) method with a modifies clause//KRML-confirmed

         { var x := 8;

           while x != 0

-            modifies this;  // error: cannot use a modifies clause on a loop

+            modifies this;  // error: cannot use a modifies clause on a loop//KRML-confirmed

           {

             x := x - 1;

           }

@@ -822,7 +822,7 @@ module StatementsInExpressions {
     {

       MyLemma();

       MyGhostMethod();   // error: modifi2es state

-      OrdinaryMethod();  // error: not a ghost

+      OrdinaryMethod();  // error: not a ghost//KRML-confirmed

       OutParamMethod();  // error: has out-parameters

       10

     }

@@ -1446,3 +1446,219 @@ module SuchThat {
     w

   }

 }

+

+// ---------------------- NEW STUFF ----------------------------------------

+

+module GhostTests {

+  class G { }

+  

+  method GhostNew4(n: nat)

+  {

+    var g := new G;

+    calc {

+      5;

+      2 + 3;

+      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context//ADD:680

+      1 + 4;

+      { GhostNew5(g); }  // error: cannot call method with nonempty modifies//ADD:682

+      -5 + 10;

+    }

+  }

+

+  ghost method GhostNew5(g: G)

+    modifies g;

+  {

+  }

+  

+  class MyClass {

+    ghost method SideEffect()

+      modifies this;

+    {

+    }

+

+    method NonGhostMethod()

+    {

+    }

+

+    ghost method M()

+      modifies this;

+    {

+      calc {

+        5;

+        { SideEffect(); }  // error: cannot call method with side effects//ADD:738

+        5;

+      }

+    }

+    function F(): int

+    {

+      calc {

+        6;

+        { assert 6 < 8; }

+        { NonGhostMethod(); }  // error: cannot call non-ghost method//ADD:748

+        { var x := 8;

+          while x != 0

+          {

+            x := x - 1;

+          }

+        }

+        { var x := 8;

+          while x != 0

+          {

+            x := x - 1;

+          }

+        }

+        { MyField := 12; }  // error: cannot assign to a field, and especially not a non-ghost field//ADD:762

+        { MyGhostField := 12; }  // error: cannot assign to any field//ADD:763

+        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause//ADD:764

+        { var x := 8;

+          while x != 0

+            modifies this;  // error: cannot use a modifies clause on a loop//ADD:767

+          {

+            x := x - 1;

+          }

+        }

+        6;

+      }

+      5

+    }

+    var MyField: int;

+    ghost var MyGhostField: int;

+    method N()

+    {

+      var y :=

+      calc {

+        6;

+        { assert 6 < 8; }

+        { NonGhostMethod(); }  // error: cannot call non-ghost method//ADD:786

+        { var x := 8;

+          while x != 0

+          {

+            x := x - 1;

+          }

+        }

+        { MyField := 12; }  // error: cannot assign to a field, and especially not a non-ghost field//ADD:794

+        { MyGhostField := 12; }  // error: cannot assign to any field//ADD:795

+        { M(); }  // error: cannot call (ghost) method with a modifies clause//ADD:796

+        { var x := 8;

+          while x != 0

+            modifies this;  // error: cannot use a modifies clause on a loop//ADD:799

+          {

+            x := x - 1;

+          }

+        }

+        { var x := 8;

+          while x != 0

+          {

+            x := x - 1;

+          }

+        }

+        6;

+      }

+      5;

+    }

+    ghost method MyLemma()

+    ghost method MyGhostMethod()

+      modifies this;

+    method OrdinaryMethod()

+    ghost method OutParamMethod() returns (y: int)

+

+    function UseLemma(): int

+    {

+      MyLemma();

+      OrdinaryMethod();  // error: not a ghost//ADD:825

+      10

+    }

+  }

+}

+

+module EvenMoreGhostTests {

+  ghost method NiceTry()

+    ensures false;

+  {

+    while (true)

+      decreases *;  // error:  not allowed in ghost context//ADD:157

+    {

+    }

+  }

+  method BreakMayNotBeFineHere()

+  {

+    var n := 0;

+    var p := 0;

+    while (true)

+    {

+      var dontKnow;

+      if (n == 112) {

+      } else if (dontKnow == 708) {

+        while * {

+          label IfNest:

+          if (p == 67) {

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

+          } else if (*) {

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

+          }

+        }

+      }

+    }

+  }

+  ghost method Bad()

+  {

+    var x: int;

+    calc {

+      1;

+//******      { x := 1; }     // error: updates to locals defined outside of the hint are not allowed

+      x;

+      {

+        var x: int;

+        x := 1;       // this is OK

+      }

+      1;

+    }

+  }

+}

+

+module BadGhostTransfer {

+  datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)

+

+  method DatatypeDestructors_Ghost(d: DTD_List) {

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

+  }

+  method AssignSuchThatFromGhost()

+  {

+    var x: int;

+    ghost var g: int;

+

+    x := g;  // error: ghost cannot flow into non-ghost//ADD:526

+

+    x := *;

+    assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,

+                    // the compiler will complain)

+

+    x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well//ADD:532

+

+    x :| assume x == g;  // this is cool, since it's an assume (but, of course, the

+                         // compiler will complain)

+

+    x :| x == 5;

+    g :| g <= g;

+    g :| assume g < g;  // the compiler will complain here, despite the LHS being

+                        // ghost -- and rightly so, since an assume is used

+  }

+}

+

+module MoreGhostPrintAttempts {

+  method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)

+  {

+    calc {

+      n + m;

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

+      m + n;

+    }

+  }

+}

+

+module MoreLetSuchThatExpr {

+  method LetSuchThat_Ghost(ghost z: int, n: nat)

+  {

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

+  }

+}