The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.

15 files changed, 76 insertions, 52 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9ab826ac..022dc912 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -25,6 +25,28 @@ static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
 static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");

 static Scope<string>! parseVarScope = new Scope<string>();

 

+// helper routine for parsing call statements

+private static void RecordCallLhs(IdentifierExpr! e,

+                                  List<IdentifierExpr!>! lhs,

+                                  List<VarDecl!>! newVars) {

+  lhs.Add(e);

+  if (parseVarScope.Find(e.Name) == null) {

+    VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null);

+    newVars.Add(d);

+    parseVarScope.Push(e.Name, e.Name);

+  }

+}

+

+// helper routine for parsing call statements

+private static Expression! ConvertToLocal(Expression! e)

+{

+  FieldSelectExpr fse = e as FieldSelectExpr;

+  if (fse != null && fse.Obj is ImplicitThisExpr) {

+    return new IdentifierExpr(fse.tok, fse.FieldName);

+  }

+  return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)

+}

+

 ///<summary>

 /// Parses top level declarations from "filename" and appends them to "classes".

 /// Returns the number of parsing errors encountered.

@@ -522,28 +544,31 @@ CallStmt<out Statement! s>
 = (. Token! x, id;

      Expression! e;

      List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

+     List<VarDecl!> newVars = new List<VarDecl!>();

   .)

   "call"                       (. x = token; .)

   CallStmtSubExpr<out e>

   

   [ ","                        /* call a,b,c,... := ... */

-                               (. if (e is IdentifierExpr) {

-                                    lhs.Add((IdentifierExpr)e);

+                               (. e = ConvertToLocal(e);

+                                  if (e is IdentifierExpr) {

+                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);

                                   } else if (e is FieldSelectExpr) {

                                     SemErr(e.tok, "each LHS of call statement must be a variable, not a field");

                                   } else {

                                     SemErr(e.tok, "each LHS of call statement must be a variable");

                                   }

                                .)

-    Ident<out id>              (. lhs.Add(new IdentifierExpr(id, id.val)); .)

-    { "," Ident<out id>        (. lhs.Add(new IdentifierExpr(id, id.val)); .)

+    Ident<out id>              (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)

+    { "," Ident<out id>        (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)

     }

     ":="

     CallStmtSubExpr<out e>

 

   | ":="                       /* call a := ... */

-                               (. if (e is IdentifierExpr) {

-                                    lhs.Add((IdentifierExpr)e);

+                               (. e = ConvertToLocal(e);

+                                  if (e is IdentifierExpr) {

+                                    RecordCallLhs((IdentifierExpr)e, lhs, newVars);

                                   } else if (e is FieldSelectExpr) {

                                     SemErr(e.tok, "each LHS of call statement must be a variable, not a field");

                                   } else {

@@ -558,10 +583,10 @@ CallStmt<out Statement! s>
      It denotes the RHS, so to be legal it must be a FunctionCallExpr.  */

   (. if (e is FunctionCallExpr) {

        FunctionCallExpr fce = (FunctionCallExpr)e;

-       s = new CallStmt(x, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args

+       s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args

      } else {

        SemErr("RHS of call statement must denote a method invocation");

-       s = new CallStmt(x, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());

+       s = new CallStmt(x, newVars, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());

      }

   .)

   .

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 59d1d0ae..4b97edbd 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -645,13 +645,15 @@ namespace Microsoft.Dafny
   }

   

   public class CallStmt : Statement {

+    public readonly List<VarDecl!>! NewVars;

     public readonly List<IdentifierExpr!>! Lhs;

     public readonly Expression! Receiver;

     public readonly string! MethodName;

     public readonly List<Expression!>! Args;

     public Method Method;  // filled in by resolution

     

-    public CallStmt(Token! tok, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

+    public CallStmt(Token! tok, List<VarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {

+      this.NewVars = newVars;

       this.Lhs = lhs;

       this.Receiver = receiver;

       this.MethodName = methodName;

diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 0dc7df24..0fd3e612 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -23,6 +23,28 @@ static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
 static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");

 static Scope<string>! parseVarScope = new Scope<string>();

 

+// helper routine for parsing call statements

+private static void RecordCallLhs(IdentifierExpr! e,

+                                  List<IdentifierExpr!>! lhs,

+                                  List<VarDecl!>! newVars) {

+  lhs.Add(e);

+  if (parseVarScope.Find(e.Name) == null) {

+    VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null);

+    newVars.Add(d);

+    parseVarScope.Push(e.Name, e.Name);

+  }

+}

+

+// helper routine for parsing call statements

+private static Expression! ConvertToLocal(Expression! e)

+{

+  FieldSelectExpr fse = e as FieldSelectExpr;

+  if (fse != null && fse.Obj is ImplicitThisExpr) {

+    return new IdentifierExpr(fse.tok, fse.FieldName);

+  }

+  return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)

+}

+

 ///<summary>

 /// Parses top level declarations from "filename" and appends them to "classes".

 /// Returns the number of parsing errors encountered.

@@ -671,6 +693,7 @@ public static int Parse (List<ClassDecl!>! classes) {
 		Token! x, id;

 		Expression! e;

 		List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();

+		List<VarDecl!> newVars = new List<VarDecl!>();

 		

 		Expect(42);

 		x = token; 

@@ -678,8 +701,9 @@ public static int Parse (List<ClassDecl!>! classes) {
 		if (t.kind == 8 || t.kind == 35) {

 			if (t.kind == 8) {

 				Get();

+				e = ConvertToLocal(e);

 				if (e is IdentifierExpr) {

-				 lhs.Add((IdentifierExpr)e);

+				  RecordCallLhs((IdentifierExpr)e, lhs, newVars);

 				} else if (e is FieldSelectExpr) {

 				  SemErr(e.tok, "each LHS of call statement must be a variable, not a field");

 				} else {

@@ -687,18 +711,19 @@ public static int Parse (List<ClassDecl!>! classes) {
 				}

 				

 				Ident(out id);

-				lhs.Add(new IdentifierExpr(id, id.val)); 

+				RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

 				while (t.kind == 8) {

 					Get();

 					Ident(out id);

-					lhs.Add(new IdentifierExpr(id, id.val)); 

+					RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); 

 				}

 				Expect(35);

 				CallStmtSubExpr(out e);

 			} else {

 				Get();

+				e = ConvertToLocal(e);

 				if (e is IdentifierExpr) {

-				 lhs.Add((IdentifierExpr)e);

+				  RecordCallLhs((IdentifierExpr)e, lhs, newVars);

 				} else if (e is FieldSelectExpr) {

 				  SemErr(e.tok, "each LHS of call statement must be a variable, not a field");

 				} else {

@@ -711,10 +736,10 @@ public static int Parse (List<ClassDecl!>! classes) {
 		Expect(9);

 		if (e is FunctionCallExpr) {

 		 FunctionCallExpr fce = (FunctionCallExpr)e;

-		 s = new CallStmt(x, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args

+		 s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args);  // this actually does an ownership transfer of fce.Args

 		} else {

 		  SemErr("RHS of call statement must denote a method invocation");

-		  s = new CallStmt(x, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());

+		  s = new CallStmt(x, newVars, lhs, dummyExpr, "dummyMethodName", new List<Expression!>());

 		}

 		

 	}

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 2159d3dc..47727562 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -684,6 +684,11 @@ namespace Microsoft.Dafny {
       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         

+        // resolve any local variables declared here

+        foreach (VarDecl local in s.NewVars) {

+          ResolveStatement(local);

+        }

+        

         // resolve left-hand side

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

         foreach (IdentifierExpr lhs in s.Lhs) {

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 09be93fa..1028058f 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1304,6 +1304,9 @@ namespace Microsoft.Dafny {
       } else if (stmt is CallStmt) {

         AddComment(builder, stmt, "call statement");

         CallStmt s = (CallStmt)stmt;

+        foreach (VarDecl local in s.NewVars) {

+          TrStmt(local, builder, locals, etran);

+        }

         Bpl.ExprSeq ins = new Bpl.ExprSeq();

         ins.Add(etran.TrExpr(s.Receiver));

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

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index a11dec52..4f717f48 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -94,7 +94,6 @@ class Benchmark3 {
    

     decreases |q.contents|;

     {  

-      var m,k;

       call m,k := RemoveMin(q);

       perm := perm + [p[k]]; //adds  index of min to perm

       p := p[k+1..]+ p[..k]; //remove index of min from p  

@@ -126,7 +125,6 @@ class Benchmark3 {
       invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far   

       decreases n-j;

     {

-		var x;

 		call x:= q.Dequeue();

 		call q.Enqueue(x);

 		if ( x < m) {k := j; m := x;}

@@ -140,7 +138,6 @@ class Benchmark3 {
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 

       decreases k-j;

     {     

-      var x;

       call x := q.Dequeue();

       call q.Enqueue(x);

       j:= j +1;

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ac58b7d1..5a9d46c8 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -30,7 +30,6 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       present := false;

@@ -55,7 +54,6 @@ class Map<Key,Value> {
     ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>

                 values[i] == old(values)[i]);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       keys := keys + [key];

@@ -88,7 +86,6 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&

               values[h..] == old(values)[h+1..]);

   {

-    var j;

     call j := FindIndex(key);

     if (0 <= j) {

       keys := keys[..j] + keys[j+1..];

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 9d384c38..8026e60f 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -99,7 +99,6 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents)[1..] + old(contents)[..1];

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -113,7 +112,6 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -163,7 +161,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

@@ -191,7 +188,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index f6e7879f..48306e9b 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -114,7 +114,7 @@ class Client
 		call c.Add(45);

 		call c.Add(78);

 		

-		var iter,b,x, s:= [ ];

+		var s:= [ ];

 		

 		call iter:=c.GetIterator();

 		call b:= iter.MoveNext();

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 95267823..f7d51058 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -129,12 +129,10 @@ class Client {
 		call rd.Open();

 		

 		var q:= new Queue<int>;	

-		var ch;

 		while (true)

 		 invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

 		 decreases |rd.stream|;

 		{

-				var eos:bool;

 				call eos := rd.AtEndOfStream();

 				if (eos) 

 				{

@@ -146,7 +144,6 @@ class Client {
 	    }

 	    

 	    call rd.Close();

-	    var perm;

 	    call q,perm := Sort(q);

 	    

 	    var wr:= new Stream;

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 643609d0..51172419 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -61,7 +61,6 @@ class Glossary {
       //  ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)

       // we leave out the decreases clause - unbounded stream

     {

-      var term,definition;

       call term,definition := readDefinition(rs);

       if (term == null)

       {

@@ -72,7 +71,6 @@ class Glossary {
     }    

     

     call rs.Close();

-    var p;

     call q,p := Sort(q);

     var wr := new WriterStream;

     call wr.Create();

@@ -84,7 +82,6 @@ class Glossary {
       invariant q !in wr.footprint;

       decreases |q.contents|;

     {

-      var term, present, definition;

       call term:= q.Dequeue();

       call present,definition:= glossary.Find(term);

       assume present; // to change this into an assert we need the loop invariant ** above that we commented out

@@ -103,7 +100,6 @@ class Glossary {
         decreases |definition| -i;

       {

         var w := definition[i];

-        var d;

         assume w != null; // to convert this into an assert we need invariant *** above

         call present, d := glossary.Find(w);

         if (present)

@@ -135,7 +131,6 @@ class Glossary {
         invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

         invariant null !in definition;

       {

-        var w;

         call w := rs.GetWord();

         if (w == null)

         {

@@ -275,7 +270,6 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       present := false;

@@ -300,7 +294,6 @@ class Map<Key,Value> {
     ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>

                 values[i] == old(values)[i]);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       keys := keys + [key];

@@ -333,7 +326,6 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&

               values[h..] == old(values)[h+1..]);

   {

-    var j;

     call j := FindIndex(key);

     if (0 <= j) {

       keys := keys[..j] + keys[j+1..];

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 7a5fb3c7..138a22df 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -42,7 +42,6 @@ class IntSet {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents) + {x};

   { 

-    var t;

     call t := InsertHelper(x, root);

     root := t;

     contents := root.contents;

@@ -64,12 +63,10 @@ class IntSet {
       m := n;

     } else {

       if (x < n.data) {

-        var t;

         call t := InsertHelper(x, n.left);

         n.left := t;

         n.footprint := n.footprint + n.left.footprint;

       } else {

-        var t;

         call t := InsertHelper(x, n.right);

         n.right := t;

         n.footprint := n.footprint + n.right.footprint;

@@ -86,7 +83,6 @@ class IntSet {
     ensures contents == old(contents) - {x};

   {

     if (root != null) {

-      var newRoot;

       call newRoot := root.Remove(x);

       root := newRoot;

       if (root == null) {

@@ -169,13 +165,11 @@ class Node {
   {

     node := this;

     if (left != null && x < data) {

-      var t;

       call t := left.Remove(x);

       left := t;

       contents := contents - {x};

       if (left != null) { footprint := footprint + left.footprint; }

     } else if (right != null && data < x) {

-      var t;

       call t := right.Remove(x);

       right := t;

       contents := contents - {x};

@@ -189,7 +183,6 @@ class Node {
         node := left;

       } else {

         // rotate

-        var min, r;

         call min, r := right.RemoveMin();

         data := min;  right := r;

         contents := contents - {x};

@@ -211,7 +204,6 @@ class Node {
       min := data;

       node := right;

     } else {

-      var t;

       call min, t := left.RemoveMin();

       left := t;

       node := this;

@@ -229,7 +221,6 @@ class Main {
 

     call s.Insert(12);

     call s.Insert(24);

-    var present;

     call present := s.Find(x);

     assert present <==> x == 12 || x == 24;

   }

diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
index ab83a75d..5c22ec92 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny0/Queue.dfy
@@ -49,7 +49,6 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents)[1..] + old(contents)[..1];

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -63,7 +62,6 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -163,7 +161,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

@@ -191,7 +188,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 43fe63df..ee9d9613 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -28,7 +28,6 @@ class Termination {
   }

 

   method Lex() {

-    var x: int, y: int;

     call x := Update();

     call y := Update();

     while (!(x == 0 && y == 0))

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a5764be5..3f57f369 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -13,7 +13,6 @@ class C<U> {
   method Main(u: U)

   {

     var t := F(3,u) && F(this,u);

-    var kz;

     call kz := M(t,u);

     assert kz && (G() || !G());

   }