Fixed some issues with assignments in refinements, both soundness bugs in previous version and changes necessitated by recent parsing refactoring

3 files changed, 56 insertions, 23 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 43333f22..ef59d00a 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1216,8 +1216,10 @@ namespace Microsoft.Dafny
               }

             }

             bool doMerge = false;

-            if (cOld != null && cNew.Lhs.Resolved is IdentifierExpr && cOld.Lhs.Resolved is IdentifierExpr) {

-              if (((IdentifierExpr)cNew.Lhs.Resolved).Name == ((IdentifierExpr)cOld.Lhs.Resolved).Name) {

+            if (cOld != null && cNew.Lhs.WasResolved() && cOld.Lhs.WasResolved()) {

+              var newLhs = cNew.Lhs.Resolved as IdentifierExpr;

+              var oldLhs = cOld.Lhs.Resolved as IdentifierExpr;

+              if (newLhs != null && oldLhs != null && newLhs.Name == oldLhs.Name) {

                 if (!(cNew.Rhs is TypeRhs) && cOld.Rhs is HavocRhs) {

                   doMerge = true;

                 }

@@ -1325,13 +1327,13 @@ namespace Microsoft.Dafny
       if (old.Count != nw.Count)

         return false;

       for (int i = 0; i < old.Count; i++) {

-        var a = old[i].Resolved as IdentifierExpr;

-        var b = nw[i] as IdentifierSequence;

-        if (a != null && b != null)

-          if (b.Tokens.Count == 1 && b.Arguments == null)

-            if (a.Name == b.Tokens[0].val)

-              continue;

-        return false;

+        var a = old[i].WasResolved() ? old[i].Resolved as IdentifierExpr : null;

+        var b = nw[i] as NameSegment;

+        if (a != null && b != null && a.Name == b.Name) {

+          // cool

+        } else {

+          return false;

+        }

       }

       return true;

     }

@@ -1525,7 +1527,7 @@ namespace Microsoft.Dafny
     }

 

     // Checks that statement stmt, defined in the constructed module m, is a refinement of skip in the parent module

-    private bool CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) {

+    void CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) {

       foreach (var lhs in stmt.Lhss) {

         var l = lhs.Resolved;

         if (l is IdentifierExpr) {

@@ -1533,26 +1535,26 @@ namespace Microsoft.Dafny
           Contract.Assert(ident.Var is LocalVariable || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)

           if ((ident.Var is LocalVariable && RefinementToken.IsInherited(((LocalVariable)ident.Var).Tok, m)) || ident.Var is Formal) {

             // for some reason, formals are not considered to be inherited.

-            reporter.Error(l.tok, "cannot assign to variable defined previously");

-            return false;

+            reporter.Error(l.tok, "refinement method cannot assign to variable defined in parent module ('{0}')", ident.Var.Name);

           }

         } else if (l is MemberSelectExpr) {

-          if (RefinementToken.IsInherited(((MemberSelectExpr)l).Member.tok, m)) {

-            return false;

+          var member = ((MemberSelectExpr)l).Member;

+          if (RefinementToken.IsInherited(member.tok, m)) {

+            reporter.Error(l.tok, "refinement method cannot assign to a field defined in parent module ('{0}')", member.Name);

           }

         } else {

-          return false;

+          // must be an array element

+          reporter.Error(l.tok, "new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)");

         }

       }

       if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         foreach (var rhs in s.Rhss) {

-          if (s.Rhss[0].CanAffectPreviouslyKnownExpressions) {

-            return false;

+          if (rhs.CanAffectPreviouslyKnownExpressions) {

+            reporter.Error(rhs.Tok, "assignment RHS in refinement method is not allowed to affect previously defined state");

           }

         }

       }

-      return true;

     }

     // ---------------------- additional methods -----------------------------------------------------------------------------

 

diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index 34e30a05..70d0b989 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -10,7 +10,7 @@ abstract module R1 {
   }

 }

 

-abstract module R2 refines R1 {

+module R2 refines R1 {

   var g: nat;

   method m ...

   {

@@ -18,8 +18,36 @@ abstract module R2 refines R1 {
     var x := 3;

     t := {1}; // error: previous local

     r := 3; // error: out parameter

-    f := 4; // fine: all fields, will cause re-verification

+    f := 4; // error: previously defined field

     x := 6; // fine: new local

     g := 34;// fine: new field

   }

 }

+

+abstract module M0 {

+  class C {

+    method Init()

+      modifies this;

+    { }

+    method InitWithSideEffects(c: C)

+      modifies c;

+    { }

+    method mmm(arr: array<int>) {

+      var a: C :| true;

+      var b: C :| true;

+    }

+  }

+}

+

+module M1 refines M0 {

+  class C {

+    method mmm... {

+      var a := new C;  // fine

+      var b := new C.Init();  // fine

+      var c := new C.InitWithSideEffects(b);  // error: modifies previous state

+      if arr != null && 12 < arr.Length {

+        arr[12] := 26;  // error: modifies previously defined state

+      }

+    }

+  }

+}

diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect
index 060ee3e4..675d244e 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy.expect
+++ b/Test/dafny0/RefinementModificationChecking.dfy.expect
@@ -1,3 +1,6 @@
-RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously

-RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously

-2 resolution/type errors detected in RefinementModificationChecking.dfy

+RefinementModificationChecking.dfy(19,4): Error: refinement method cannot assign to variable defined in parent module ('t')

+RefinementModificationChecking.dfy(20,4): Error: refinement method cannot assign to variable defined in parent module ('r')

+RefinementModificationChecking.dfy(21,4): Error: refinement method cannot assign to a field defined in parent module ('f')

+RefinementModificationChecking.dfy(47,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state

+RefinementModificationChecking.dfy(49,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)

+5 resolution/type errors detected in RefinementModificationChecking.dfy