summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg41
-rw-r--r--Source/Dafny/DafnyAst.ssc4
-rw-r--r--Source/Dafny/Parser.ssc37
-rw-r--r--Source/Dafny/Resolver.ssc5
-rw-r--r--Source/Dafny/Translator.ssc3
-rw-r--r--Test/VSI-Benchmarks/b3.dfy3
-rw-r--r--Test/VSI-Benchmarks/b4.dfy3
-rw-r--r--Test/VSI-Benchmarks/b5.dfy4
-rw-r--r--Test/VSI-Benchmarks/b6.dfy2
-rw-r--r--Test/VSI-Benchmarks/b7.dfy3
-rw-r--r--Test/VSI-Benchmarks/b8.dfy8
-rw-r--r--Test/dafny0/BinaryTree.dfy9
-rw-r--r--Test/dafny0/Queue.dfy4
-rw-r--r--Test/dafny0/Termination.dfy1
-rw-r--r--Test/dafny0/TypeParameters.dfy1
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());
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 06:38:56 +0000