Dafny: improved and corrected physical/ghost distinction

5 files changed, 25 insertions, 19 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index b26e1288..0b736242 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -2300,7 +2300,7 @@ namespace Microsoft.Dafny {
     {

     }

 

-    public List<BoundedPool> Bounds;  // initialized and filled in by resolver; it remains null for quantifiers in specification contexts

+    public List<BoundedPool> Bounds;  // initialized and filled in by resolver

     // invariant bounds == null || bounds.Count == BoundVars.Count;

 

     public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 09bed6dd..e261c8a1 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1120,6 +1120,9 @@ namespace Microsoft.Dafny {
       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         ResolveAttributeArgs(s.Args, false, false);

+        if (specContextOnly) {

+          Error(stmt, "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)");

+        }

           

       } else if (stmt is BreakStmt) {

         BreakStmt s = (BreakStmt)stmt;

@@ -1161,6 +1164,9 @@ namespace Microsoft.Dafny {
             if (!var.IsMutable) {

               Error(stmt, "LHS of assignment must denote a mutable variable or field");

             }

+            if (!lvalueIsGhost && specContextOnly) {

+              Error(stmt, "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)");

+            }

           }

         } else if (s.Lhs is FieldSelectExpr) {

           // LHS is fine, but restrict the RHS to ExprRhs

@@ -1269,6 +1275,10 @@ namespace Microsoft.Dafny {
         if (!scope.Push(s.Name, s)) {

           Error(s, "Duplicate local-variable name: {0}", s.Name);

         }

+        if (specContextOnly) {

+          // a local variable in a specification-only context might as well be ghost

+          s.IsGhost = true;

+        }

       

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

@@ -2180,14 +2190,7 @@ namespace Microsoft.Dafny {
         expr.Type = Type.Bool;

 

         if (prevErrorCount == ErrorCount) {

-          if (specContext) {

-            // any quantifier is allowed

-          } else {

-            // ...but in non-spec contexts, it is necessary to compile the quantifier, so only certain quantifiers

-            // whose bound variables draw their values from bounded pools of values are allowed.  To check for such

-            // "bounded pools", this resolving code looks for certain patterns.

-            e.Bounds = DiscoverBounds(e);

-          }

+          e.Bounds = DiscoverBounds(e, specContext);

         }

         

       } else if (expr is WildcardExpr) {

@@ -2319,10 +2322,11 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Tries to find a bounded pool for each of the bound variables of "e".  If this process fails, appropriate

-    /// error messages are reported and "null" is returned.

+    /// error messages are reported and "null" is returned, unless "friendlyTry" is "true", in which case no

+    /// error messages are reported.

     /// Requires "e" to be successfully resolved.

     /// </summary>

-    List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e) {

+    List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e, bool friendlyTry) {

       Contract.Requires(e != null);

       Contract.Requires(e.Type != null);  // a sanity check (but not a complete proof) that "e" has been resolved

       Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == e.BoundVars.Count);

@@ -2397,7 +2401,9 @@ namespace Microsoft.Dafny {
           CHECK_NEXT_CONJUNCT: ;

           }

           // we have checked every conjunct in the range expression and still have not discovered good bounds

-          Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+          if (!friendlyTry) {

+            Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+          }

           return null;

         }

       CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

@@ -2901,7 +2907,8 @@ namespace Microsoft.Dafny {
         }

         return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);

       } else if (expr is QuantifierExpr) {

-        return true;

+        var e = (QuantifierExpr)expr;

+        return e.Bounds == null;  // if the resolver found bounds, then the quantifier can be compiled

       } else if (expr is WildcardExpr) {

         return false;

       } else if (expr is ITEExpr) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b1e12099..08570842 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -407,7 +407,8 @@ NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

 NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

 NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

-7 resolution/type errors detected in NonGhostQuantifiers.dfy

+NonGhostQuantifiers.dfy(120,8): 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)

+8 resolution/type errors detected in NonGhostQuantifiers.dfy

 

 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index dd730e90..ea256a58 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -108,7 +108,6 @@ class MyClass<T> {
     if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b

   }

   // And if statements

-/****

   method N(s: seq<int>) returns (ghost g: int, h: int)

   {

     if ( (forall x :: x in s ==> 0 <= x) ) {

@@ -117,9 +116,8 @@ class MyClass<T> {
     if ( (forall x :: x*x in s ==> x < 100) ) {  // this is fine, since the whole statement is a ghost statement

       g := 2;

     }

-    if ( (forall x :: x*x in s ==> x < 50) ) {  // error: cannot compile this guard of a non-ghost if statement

-      h := 6;

+    if ( (forall x :: x*x in s ==> x < 50) ) {

+      h := 6;  // error: cannot compile this guard of a non-ghost if statement

     }

   }

-****/

 }

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index eed06bb1..77af9327 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -4,7 +4,7 @@ method Pick<T>(S: set<T>) returns (t: T);
   requires S != {};

   ensures t in S;

 

-static function Knows<Person>(a: Person, b: Person): bool;

+static function method Knows<Person>(a: Person, b: Person): bool;

   requires a != b;  // forbid asking about the reflexive case

 

 static function IsCelebrity<Person>(c: Person, people: set<Person>): bool