Fixed resolution bug where "var x := x" was allowed.

6 files changed, 95 insertions, 23 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f281d9fc..99de2757 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1163,7 +1163,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
   }

   [ ":="                           (. assignTok = t;

                                       lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

-                                      lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

                                    .)

     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index cca4e56c..600c8d3d 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2837,6 +2837,7 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(Locals));

+      Contract.Invariant(Locals.Count != 0);

     }

 

     public VarDeclStmt(IToken tok, IToken endTok, List<LocalVariable> locals, ConcreteUpdateStatement update)

@@ -2845,6 +2846,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

       Contract.Requires(locals != null);

+      Contract.Requires(locals.Count != 0);

 

       Locals = locals;

       Update = update;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index b8800af7..d78c35a6 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1812,7 +1812,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Get();

 				assignTok = t;

 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

-				lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

 				

 				Rhs(out r, lhs0);

 				rhss.Add(r); 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 4fea4f83..0904e544 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4058,21 +4058,68 @@ namespace Microsoft.Dafny
         ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

+        // We have three cases.

+        Contract.Assert(s.Update == null || s.Update is UpdateStmt || s.Update is AssignSuchThatStmt);

+        // 0.  There is no .Update.  This is easy, we will just resolve the locals.

+        // 1.  The .Update is an AssignSuchThatStmt.  This is also straightforward:  first

+        //     resolve the locals, which adds them to the scope, and then resolve the .Update.

+        // 2.  The .Update is an UpdateStmt, which, resolved, means either a CallStmt or a bunch

+        //     of parallel AssignStmt's.  Here, the right-hand sides should be resolved before

+        //     the local variables have been added to the scope, but the left-hand sides should

+        //     resolve to the newly introduced variables.

+        // To accommodate these options, we first reach into the UpdateStmt, if any, to resolve

+        // the left-hand sides of the UpdateStmt.  This will have the effect of shielding them

+        // from a subsequent resolution (since expression resolution will do nothing if the .Type

+        // field is already assigned.

+        // Alright, so it is:

+

+        // Resolve the types of the locals

         foreach (var local in s.Locals) {

           ResolveType(local.Tok, local.OptionalType, ResolveTypeOption.InferTypeProxies, null);

           local.type = local.OptionalType;

-          // now that the declaration has been processed, add the name to the scope

-          if (!scope.Push(local.Name, local)) {

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

-          }

           if (specContextOnly) {

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

             local.IsGhost = true;

           }

         }

-        if (s.Update != null) {

+        // Resolve the UpdateStmt, if any

+        if (s.Update is UpdateStmt) {

+          var upd = (UpdateStmt)s.Update;

+          // resolve the LHS

+          Contract.Assert(upd.Lhss.Count == s.Locals.Count);

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

+            var local = s.Locals[i];

+            var lhs = (IdentifierExpr)upd.Lhss[i];  // the LHS in this case will be an IdentifierExpr, because that's how the parser creates the VarDeclStmt

+            Contract.Assert(lhs.Type == null);  // not yet resolved

+            lhs.Var = local;

+            lhs.Type = local.Type;

+          }

+          // there is one more place where a newly declared local may be lurking

+          if (upd.Rhss.Count == 1 && upd.Rhss[0] is TypeRhs) {

+            var rhs = (TypeRhs)upd.Rhss[0];

+            Contract.Assert(s.Locals.Count != 0);  // this is always true of a VarDeclStmt

+            var local = s.Locals[0];

+            if (rhs != null && rhs.ReceiverArgumentForInitCall != null) {

+              var lhs = (IdentifierExpr)rhs.ReceiverArgumentForInitCall;  // as above, we expect this to be an IdentifierExpr, because that's how the parser sets things up

+              Contract.Assert(lhs.Type == null || (upd.Lhss.Count == 1 && upd.Lhss[0] == lhs));  // if it's been resolved before, it's because it's aliased with a Lhss

+              lhs.Var = local;

+              lhs.Type = local.type;

+            }

+          }

+          // resolve the whole thing

+          ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

+        }

+        // Add the locals to the scope

+        foreach (var local in s.Locals) {

+          if (!scope.Push(local.Name, local)) {

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

+          }

+        }

+        // Resolve the AssignSuchThatStmt, if any

+        if (s.Update is AssignSuchThatStmt) {

           ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

         }

+        // Update the VarDeclStmt's ghost status according to its components

         if (!s.IsGhost) {

           s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);

         }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3b0ca15b..a8ddb8a8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -80,23 +80,28 @@ TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(55,6): Error: Duplicate local-variable name: x

 TypeTests.dfy(58,8): Error: Duplicate local-variable name: x

 TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

-TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(79,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(80,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(82,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(83,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(84,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type

-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(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(67,11): Error: unresolved identifier: x

+TypeTests.dfy(69,28): Error: unresolved identifier: z

+TypeTests.dfy(70,29): Error: unresolved identifier: w1

+TypeTests.dfy(70,47): Error: unresolved identifier: w0

+TypeTests.dfy(73,28): Error: unresolved identifier: e

+TypeTests.dfy(88,17): Error: member F in type C does not refer to a method

+TypeTests.dfy(89,17): Error: a method called as an initialization method must not have any result arguments

+TypeTests.dfy(98,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(99,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(100,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(104,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

+TypeTests.dfy(110,6): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(111,9): Error: sorry, cannot instantiate type parameter with a subrange type

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

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

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

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

+TypeTests.dfy(136,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

-28 resolution/type errors detected in TypeTests.dfy

+33 resolution/type errors detected in TypeTests.dfy

 

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

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

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index ca89b08a..143fa579 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -62,6 +62,26 @@ method DuplicateVarName(x: int) returns (y: int)
                // treated like an outermost-scoped local in this regard)

 }

 

+method ScopeTests()

+{

+  var x := x;  // error: the 'x' in the RHS is not in scope

+  var y :| y == y;  // fine, 'y' is in scope in the RHS

+  var z := DuplicateVarName(z);  // error: the 'z' in the RHS is not in scope

+  var w0, w1 := IntTransform(w1), IntTransform(w0);  // errors two

+  var c := new MyClass.Init(null);  // fine

+  var d := new MyClass.Init(c);  // fine

+  var e := new MyClass.Init(e);  // error: the 'e' in the RHS is not in scope

+  e := new MyClass.Init(e);  // fine (no variable is being introduced here)

+  e.c := new MyClass.Init(e);  // also fine

+}

+

+function IntTransform(w: int): int

+

+class MyClass {

+  var c: MyClass;

+  constructor Init(c: MyClass)

+}

+

 // ---------------------

 

 method InitCalls() {