improved and fixed compilation and resolution of assign-such-that statements

7 files changed, 158 insertions, 129 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4c334033..dd50c4eb 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1065,13 +1065,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

-        foreach (var lhs in s.Lhss) {

-          // assigning to a local ghost variable or to a ghost field is okay

-          if (!AssignStmt.LhsIsToGhost(lhs)) {

-            Error("compiling an assign-such-that statement with a non-ghost left-hand side is currently not supported (line {0})", stmt.Tok.line);

-            break;  // no need to say more

-          }

-        }

+        Error("compilation of assign-such-that statements is currently not supported (line {0})", stmt.Tok.line);

 

       } else if (stmt is VarDecl) {

         TrVarDecl((VarDecl)stmt, true, indent);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 945bf5c2..573cdfa7 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3754,135 +3754,119 @@ namespace Microsoft.Dafny
           Error(lhs, "cannot assign to non-ghost variable in a ghost context");

         }

       }

-      IToken firstEffectfulRhs = null;

-      CallRhs callRhs = null;

       // Resolve RHSs

       if (update == null) {

         var suchThat = (AssignSuchThatStmt)s;  // this is the other possible subclass

-        ResolveExpression(suchThat.Expr, true);

-        if (suchThat.AssumeToken == null) {

-          // to ease in the verification, only allow local variables as LHSs

-          var lhsNames = new Dictionary<string, object>();

-          foreach (var lhs in s.Lhss) {

-            if (!(lhs.Resolved is IdentifierExpr)) {

-              Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");

-            } else {

-              var ie = (IdentifierExpr)lhs.Resolved;

-              if (lhsNames.ContainsKey(ie.Name)) {

-                // disallow same LHS.

-                Error(s, "duplicate variable in left-hand side of assign-such-that statement: {0}", ie.Name);

-              } else {

-                lhsNames.Add(ie.Name, null);

-              }

-            }

-          }

-        }

-      } else {

-        foreach (var rhs in update.Rhss) {

-          bool isEffectful;

-          if (rhs is TypeRhs) {

-            var tr = (TypeRhs)rhs;

-            ResolveTypeRhs(tr, s, specContextOnly, codeContext);

-            isEffectful = tr.InitCall != null;

-          } else if (rhs is HavocRhs) {

-            isEffectful = false;

+        ResolveAssignSuchThatStmt(suchThat, specContextOnly);

+        return;

+      } 

+

+      IToken firstEffectfulRhs = null;

+      CallRhs callRhs = null;

+      foreach (var rhs in update.Rhss) {

+        bool isEffectful;

+        if (rhs is TypeRhs) {

+          var tr = (TypeRhs)rhs;

+          ResolveTypeRhs(tr, s, specContextOnly, codeContext);

+          isEffectful = tr.InitCall != null;

+        } else if (rhs is HavocRhs) {

+          isEffectful = false;

+        } else {

+          var er = (ExprRhs)rhs;

+          if (er.Expr is IdentifierSequence) {

+            var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);

+            isEffectful = cRhs != null;

+            callRhs = callRhs ?? cRhs;

+          } else if (er.Expr is FunctionCallExpr) {

+            var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);

+            isEffectful = cRhs != null;

+            callRhs = callRhs ?? cRhs;

           } else {

-            var er = (ExprRhs)rhs;

-            if (er.Expr is IdentifierSequence) {

-              var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);

-              isEffectful = cRhs != null;

-              callRhs = callRhs ?? cRhs;

-            } else if (er.Expr is FunctionCallExpr) {

-              var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);

-              isEffectful = cRhs != null;

-              callRhs = callRhs ?? cRhs;

-            } else {

-              ResolveExpression(er.Expr, true);

-              isEffectful = false;

-            }

-          }

-          if (isEffectful && firstEffectfulRhs == null) {

-            firstEffectfulRhs = rhs.Tok;

+            ResolveExpression(er.Expr, true);

+            isEffectful = false;

           }

         }

+        if (isEffectful && firstEffectfulRhs == null) {

+          firstEffectfulRhs = rhs.Tok;

+        }

       }

-      // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

-      var lhsNameSet = new Dictionary<string, object>();

-      foreach (var lhs in s.Lhss) {

-        var ie = lhs.Resolved as IdentifierExpr;

-        if (ie != null) {

-          if (lhsNameSet.ContainsKey(ie.Name)) {

-            if (callRhs != null)

-              // only allow same LHS in a multiassignment, not a call statement

+      // syntactically disallow duplicate LHSs for call statements

+      if (callRhs != null) {

+        // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

+        var lhsNameSet = new Dictionary<string, object>();

+        foreach (var lhs in s.Lhss) {

+          var ie = lhs.Resolved as IdentifierExpr;

+          if (ie != null) {

+            if (lhsNameSet.ContainsKey(ie.Name)) {

               Error(s, "duplicate variable in left-hand side of call statement: {0}", ie.Name);

-          } else {

-            lhsNameSet.Add(ie.Name, null);

+            } else {

+              lhsNameSet.Add(ie.Name, null);

+            }

           }

         }

       }

-      if (update != null) {

-        // figure out what kind of UpdateStmt this is

-        if (firstEffectfulRhs == null) {

-          if (s.Lhss.Count == 0) {

-            Contract.Assert(update.Rhss.Count == 1);  // guaranteed by the parser

-            Error(s, "expected method call, found expression");

-          } else if (s.Lhss.Count != update.Rhss.Count) {

-            Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);

-          } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

-            Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");

-          } else if (ErrorCount == prevErrorCount) {

-            // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

-            for (int i = 0; i < s.Lhss.Count; i++) {

-              var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, update.Rhss[i]);

-              s.ResolvedStatements.Add(a);

-            }

+

+      // figure out what kind of UpdateStmt this is

+      if (firstEffectfulRhs == null) {

+        if (s.Lhss.Count == 0) {

+          Contract.Assert(update.Rhss.Count == 1);  // guaranteed by the parser

+          Error(s, "expected method call, found expression");

+        } else if (s.Lhss.Count != update.Rhss.Count) {

+          Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);

+        } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

+          Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");

+        } else if (ErrorCount == prevErrorCount) {

+          // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

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

+            var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, update.Rhss[i]);

+            s.ResolvedStatements.Add(a);

           }

+        }

 

-        } else if (update.CanMutateKnownState) {

-          if (1 < update.Rhss.Count) {

-            Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");

-          } else { // it might be ok, if it is a TypeRhs

-            Contract.Assert(update.Rhss.Count == 1);

-            if (callRhs != null) {

-              Error(callRhs.Tok, "cannot have method call in return statement.");

-            } else {

-              // we have a TypeRhs

-              Contract.Assert(update.Rhss[0] is TypeRhs);

-              var tr = (TypeRhs)update.Rhss[0];

-              Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.

-              if (tr.CanAffectPreviouslyKnownExpressions) {

-                Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");

-              }

-              var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);

-              s.ResolvedStatements.Add(a);

+      } else if (update.CanMutateKnownState) {

+        if (1 < update.Rhss.Count) {

+          Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");

+        } else { // it might be ok, if it is a TypeRhs

+          Contract.Assert(update.Rhss.Count == 1);

+          if (callRhs != null) {

+            Error(callRhs.Tok, "cannot have method call in return statement.");

+          } else {

+            // we have a TypeRhs

+            Contract.Assert(update.Rhss[0] is TypeRhs);

+            var tr = (TypeRhs)update.Rhss[0];

+            Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.

+            if (tr.CanAffectPreviouslyKnownExpressions) {

+              Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");

             }

+            var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);

+            s.ResolvedStatements.Add(a);

           }

+        }

 

+      } else {

+        // if there was an effectful RHS, that must be the only RHS

+        if (update.Rhss.Count != 1) {

+          Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

+        } else if (arrayRangeLhs != null) {

+          Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

+        } else if (callRhs == null) {

+          // must be a single TypeRhs

+          if (s.Lhss.Count != 1) {

+            Contract.Assert(2 <= s.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)

+            Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);

+          } else if (ErrorCount == prevErrorCount) {

+            var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]);

+            s.ResolvedStatements.Add(a);

+          }

         } else {

-          // if there was an effectful RHS, that must be the only RHS

-          if (update.Rhss.Count != 1) {

-            Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

-          } else if (arrayRangeLhs != null) {

-            Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

-          } else if (callRhs == null) {

-            // must be a single TypeRhs

-            if (s.Lhss.Count != 1) {

-              Contract.Assert(2 <= s.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)

-              Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);

-            } else if (ErrorCount == prevErrorCount) {

-              var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]);

-              s.ResolvedStatements.Add(a);

-            }

-          } else {

-            // a call statement

-            if (ErrorCount == prevErrorCount) {

-              var resolvedLhss = new List<Expression>();

-              foreach (var ll in s.Lhss) {

-                resolvedLhss.Add(ll.Resolved);

-              }

-              var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

-              s.ResolvedStatements.Add(a);

+          // a call statement

+          if (ErrorCount == prevErrorCount) {

+            var resolvedLhss = new List<Expression>();

+            foreach (var ll in s.Lhss) {

+              resolvedLhss.Add(ll.Resolved);

             }

+            var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

+            s.ResolvedStatements.Add(a);

           }

         }

       }

@@ -3893,6 +3877,26 @@ namespace Microsoft.Dafny
       s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);

     }

 

+    private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly) {

+      Contract.Requires(s != null);

+

+      if (s.AssumeToken == null) {

+        // to ease in the verification of the existence check, only allow local variables as LHSs

+        foreach (var lhs in s.Lhss) {

+          if (!(lhs.Resolved is IdentifierExpr)) {

+            Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");

+          }

+        }

+      }

+

+      s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);

+      var ec = ErrorCount;

+      ResolveExpression(s.Expr, true);

+      if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {

+        CheckIsNonGhost(s.Expr);

+      }

+    }

+

     bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {

       Contract.Requires(alternatives != null);

       Contract.Requires(codeContext != null);

@@ -5371,6 +5375,12 @@ namespace Microsoft.Dafny
         if (!moduleInfo.IsGhost)

           CheckIsNonGhost(((NamedExpr)expr).Body);

         return;

+      } else if (expr is ChainingExpression) {

+        // We don't care about the different operators; we only want the operands, so let's get them directly from

+        // the chaining expression

+        var e = (ChainingExpression)expr;

+        e.Operands.ForEach(CheckIsNonGhost);

+        return;

       }

 

       foreach (var ee in expr.SubExpressions) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 370e3c38..e7fda470 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,10 +91,11 @@ TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a sub
 TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

 TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type

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

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

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

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

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

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

-36 resolution/type errors detected in TypeTests.dfy

+37 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -556,7 +557,9 @@ ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)

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

 ResolutionErrors.dfy(382,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)

-62 resolution/type errors detected in ResolutionErrors.dfy

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

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

+64 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 7c919b2a..d5fecdf8 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -423,3 +423,27 @@ class Lamb {
   method Jesus() { }

   method Gwen() { }

 }

+

+// ------------------- assign-such-that and ghosts ------------------------------

+

+method AssignSuchThatFromGhost()

+{

+  var x: int;

+  ghost var g: int;

+

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

+  

+  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 :| 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

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 7b409a67..43ee1d8e 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -530,7 +530,7 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
 

 method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)

 {

-  var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

+  ghost var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

   assert b < a;

   k :| k == old(2*k);  // note, the 'old' has no effect on local variables like k

   assert k == 0;

@@ -571,7 +571,7 @@ method AssignSuchThat4()
 

 method AssignSuchThat5()

 {

-  var n := new Node;

+  ghost var n := new Node;

   n :| fresh(n);  // fine

   assert false;  // error

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 2dea7a52..42457918 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -101,10 +101,8 @@ method M()
   ghost var k: int, l: int;

   var m: int;

 

-  // These three statements are allowed by the resolver, but the compiler will complain

-  // if it ever gets them.

   k :| k < 10;

-  k, m :| 0 <= k < m;

+  k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost

   m :| m < 10;

 

   // Because of the ghost guard, these 'if' statements are ghost contexts, so only

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index da62f91c..d8938aa7 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -19,7 +19,7 @@ ghost module A {
       ensures Contents == old(Contents);

       ensures thing in Contents && L.Function.Apply(matchCriterion, thing);

     {

-      var k :| k in Contents && L.Function.Apply(matchCriterion, k);

+      var k :| assume k in Contents && L.Function.Apply(matchCriterion, k);

       thing := k;

     }

   }

@@ -52,7 +52,7 @@ module B refines A {
       }

       var k := arr[i];

       ...;

-      var a :| Contents == set x | x in a;

+      var a :| assume Contents == set x | x in a;

       arr := a;

     }

   }