Fixed bug where resolution was overly restrictive with ghost variables appearing in reads clauses.

Fixed bug in the checking of reads subset for field frame targets ("back ticks")

6 files changed, 162 insertions, 19 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b6b0ab0b..167b56c2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3224,7 +3224,7 @@ namespace Microsoft.Dafny
         }

       }

       foreach (FrameExpression fr in f.Reads) {

-        ResolveFrameExpression(fr, "reads", f.IsGhost, f);

+        ResolveFrameExpression(fr, true, f.IsGhost, f);

       }

       foreach (Expression r in f.Ens) {

         ResolveExpression(r, new ResolveOpts(f, false));  // since this is a function, the postcondition is still a one-state predicate

@@ -3252,9 +3252,15 @@ namespace Microsoft.Dafny
       scope.PopMarker();

     }

 

-    void ResolveFrameExpression(FrameExpression fe, string kind, bool isGhostContext, ICodeContext codeContext) {

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="fe"></param>

+    /// <param name="readsFrame">True indicates "reads", false indicates "modifies".</param>

+    /// <param name="isGhostContext"></param>

+    /// <param name="codeContext"></param>

+    void ResolveFrameExpression(FrameExpression fe, bool readsFrame, bool isGhostContext, ICodeContext codeContext) {

       Contract.Requires(fe != null);

-      Contract.Requires(kind != null);

       Contract.Requires(codeContext != null);

       ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));

       Type t = fe.E.Type;

@@ -3268,7 +3274,7 @@ namespace Microsoft.Dafny
         t = collType.Arg;

       }

       if (!UnifyTypes(t, new ObjectType())) {

-        Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);

+        Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type);

       } else if (fe.FieldName != null) {

         NonProxyType nptype;

         MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype);

@@ -3277,8 +3283,8 @@ namespace Microsoft.Dafny
           // error has already been reported by ResolveMember

         } else if (!(member is Field)) {

           Error(fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name);

-        } else if (isGhostContext && !member.IsGhost) {

-          Error(fe.E, "in a ghost context, only ghost fields can be mentioned as frame targets ({0})", fe.FieldName);

+        } else if (!readsFrame && isGhostContext && !member.IsGhost) {

+          Error(fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName);

         } else {

           Contract.Assert(ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

           fe.Field = (Field)member;

@@ -3343,7 +3349,7 @@ namespace Microsoft.Dafny
         }

         ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false));

         foreach (FrameExpression fe in m.Mod.Expressions) {

-          ResolveFrameExpression(fe, "modifies", m.IsGhost, m);

+          ResolveFrameExpression(fe, false, m.IsGhost, m);

           if (m is Lemma) {

             Error(fe.tok, "lemmas are not allowed to have modifies clauses");

           } else if (m is CoLemma) {

@@ -3469,10 +3475,10 @@ namespace Microsoft.Dafny
         }

       }

       foreach (FrameExpression fe in iter.Reads.Expressions) {

-        ResolveFrameExpression(fe, "reads", false, iter);

+        ResolveFrameExpression(fe, true, false, iter);

       }

       foreach (FrameExpression fe in iter.Modifies.Expressions) {

-        ResolveFrameExpression(fe, "modifies", false, iter);

+        ResolveFrameExpression(fe, false, false, iter);

       }

       foreach (MaybeFreeExpression e in iter.Requires) {

         ResolveExpression(e.E, new ResolveOpts(iter, false));

@@ -4761,7 +4767,7 @@ namespace Microsoft.Dafny
         if (s.Mod.Expressions != null) {

           ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));

           foreach (FrameExpression fe in s.Mod.Expressions) {

-            ResolveFrameExpression(fe, "modifies", bodyMustBeSpecOnly, codeContext);

+            ResolveFrameExpression(fe, false, bodyMustBeSpecOnly, codeContext);

             Translator.ComputeFreeVariables(fe.E, fvs, ref usesHeap, ref usesOldHeap, ref usesThis, false);

           }

         }

@@ -4904,7 +4910,7 @@ namespace Microsoft.Dafny
         ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));

         foreach (FrameExpression fe in s.Mod.Expressions) {

           // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message

-          ResolveFrameExpression(fe, "modifies", specContextOnly, codeContext);

+          ResolveFrameExpression(fe, false, specContextOnly, codeContext);

         }

         if (s.Body != null) {

           ResolveBlockStatement(s.Body, specContextOnly, codeContext);

@@ -7023,7 +7029,7 @@ namespace Microsoft.Dafny
         }

 

         foreach (var read in e.Reads) {

-          ResolveFrameExpression(read, "reads", false, opts.codeContext);

+          ResolveFrameExpression(read, true, false, opts.codeContext);

         }

 

         ResolveExpression(e.Term, opts);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index cdf9eb86..3ce7dad5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13581,7 +13581,9 @@ namespace Microsoft.Dafny {
 

       public FrameExpression SubstFrameExpr(FrameExpression frame) {

         Contract.Requires(frame != null);

-        return new FrameExpression(frame.tok, Substitute(frame.E), frame.FieldName);

+        var fe = new FrameExpression(frame.tok, Substitute(frame.E), frame.FieldName);

+        fe.Field = frame.Field;  // resolve here

+        return fe;

       }

 

       protected AssignmentRhs SubstRHS(AssignmentRhs rhs) {

diff --git a/Test/dafny0/Backticks.dfy b/Test/dafny0/Backticks.dfy
new file mode 100644
index 00000000..08606b55
--- /dev/null
+++ b/Test/dafny0/Backticks.dfy
@@ -0,0 +1,80 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+class C {

+  var x: int

+  var y: int

+  ghost var z: int

+

+  function F(): int

+    reads `x

+  {

+    x

+  }

+

+  function G(): int

+    reads `x

+  {

+    F()

+  }

+

+  function H(): int

+    reads this

+  {

+    F()

+  }

+

+  function I(n: nat): int

+    reads this

+  {

+    x + y + z + J(n)

+  }

+

+  function J(n: nat): int

+    reads `x, this`z

+    decreases {this}, n, 0

+  {

+    if n == 0 then 5 else

+    I(n-1)  // error: insufficient reads clause

+  }

+

+  function K(n: nat): int

+    reads `x

+    decreases {this}, n+1

+  {

+    L(n)

+  }

+

+  function L(n: nat): int

+    reads `x

+  {

+    if n < 2 then 5 else K(n-2)

+  }

+

+  method M()

+    modifies `x

+  {

+    N();

+  }

+

+  method N()

+    modifies `x

+  {

+    x := x + 1;

+  }

+

+  method O(n: nat)

+    modifies this

+  {

+    P(n);

+  }

+  method P(n: nat)

+    modifies `x

+    decreases n, 0

+  {

+    x := x + 1;

+    if n != 0 {

+      O(n-1);  // error: insufficient modifies clause to make call

+    }

+  }

+}

diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect
new file mode 100644
index 00000000..82fc2933
--- /dev/null
+++ b/Test/dafny0/Backticks.dfy.expect
@@ -0,0 +1,11 @@
+Backticks.dfy(38,5): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Else

+Backticks.dfy(77,7): Error: call may violate context's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+

+Dafny program verifier finished with 13 verified, 2 errors

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e324393d..bb51b01f 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1259,3 +1259,45 @@ module SignatureCompletion {
   function F2<A,B>(s: set, x: A -> B): int

   function F3<A,B>(x: A -> B, s: set): int

 }

+

+// -------------- more fields as frame targets --------------------

+

+module FrameTargetFields {

+  class C {

+    var x: int

+    var y: int

+    ghost var z: int

+

+    method M()

+      modifies this

+    {

+      var n := 0;

+      ghost var save := y;

+      while n < x

+        modifies `x

+      {

+        n, x := n + 1, x - 1;

+      }

+      assert y == save;

+    }

+

+    ghost method N()

+      modifies this

+      modifies `y  // resolution error: cannot mention non-ghost here

+      modifies `z  // cool

+    {

+    }

+

+    method P()

+      modifies this

+    {

+      ghost var h := x;

+      while 0 <= h

+        modifies `x  // resolution error: cannot mention non-ghost here

+        modifies `z  // cool

+      {

+        h, z := h - 1, 5 * z;

+      }

+    }

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 3b768c84..7789c6f8 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -85,6 +85,8 @@ ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecifie
 ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+ResolutionErrors.dfy(1286,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

+ResolutionErrors.dfy(1296,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

 ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

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

@@ -108,11 +110,11 @@ ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer',
 ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

 ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor

 ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

-ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

+ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

 ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x

 ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x

 ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x

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

 ResolutionErrors.dfy(1129,2): 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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-184 resolution/type errors detected in ResolutionErrors.dfy

+186 resolution/type errors detected in ResolutionErrors.dfy