From 065957def8d08b4a08529e18c092ee7087895672 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 25 Jun 2010 21:07:18 +0000 Subject: Chalice: * renamed keyword "maxlock" to "waitlevel" * added -vs switch, for I/O suitable for VS integration --- Chalice/examples/Answer | 4 +- Chalice/examples/AssociationList.chalice | 12 +- .../CopyLessMessagePassing-with-ack.chalice | 8 +- .../CopyLessMessagePassing-with-ack2.chalice | 8 +- Chalice/examples/CopyLessMessagePassing.chalice | 4 +- Chalice/examples/HandOverHand.chalice | 14 +- Chalice/examples/OwickiGries.chalice | 2 +- Chalice/examples/ProdConsChannel.chalice | 12 +- Chalice/examples/Sieve.chalice | 8 +- Chalice/examples/cell.chalice | 6 +- Chalice/examples/counter.chalice | 16 +- Chalice/examples/dining-philosophers.chalice | 6 +- Chalice/examples/producer-consumer.chalice | 8 +- Chalice/examples/prog0.chalice | 2 +- Chalice/examples/prog3.chalice | 30 +- Chalice/examples/prog4.chalice | 4 +- Chalice/src/Boogie.scala | 524 ++--- Chalice/src/Chalice.scala | 239 +-- Chalice/src/Parser.scala | 10 +- Chalice/src/PrettyPrinter.scala | 2 +- Chalice/src/Resolver.scala | 2066 ++++++++++---------- Chalice/src/Translator.scala | 46 +- Util/Emacs/chalice-mode.el | 2 +- Util/latex/chalice.sty | 4 +- 24 files changed, 1522 insertions(+), 1515 deletions(-) diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer index 438a9dd6..d9856d2d 100644 --- a/Chalice/examples/Answer +++ b/Chalice/examples/Answer @@ -7,8 +7,8 @@ Boogie program verifier finished with 31 verified, 1 error 69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true. 80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true. 119.5: The held field of the target of the release statement might not be writable. - 128.7: The mu field of the target of the acquire statement might not be above maxlock. - 136.7: The mu field of the target of the acquire statement might not be above maxlock. + 128.7: The mu field of the target of the acquire statement might not be above waitlevel. + 136.7: The mu field of the target of the acquire statement might not be above waitlevel. 145.5: The held field of the target of the release statement might not be writable. Boogie program verifier finished with 24 verified, 6 errors diff --git a/Chalice/examples/AssociationList.chalice b/Chalice/examples/AssociationList.chalice index 6adcbef5..cc3ecfb4 100644 --- a/Chalice/examples/AssociationList.chalice +++ b/Chalice/examples/AssociationList.chalice @@ -18,17 +18,17 @@ class AssociationList { method Init() requires acc(head) && acc(mu) && mu == lockbottom - ensures acc(mu) && maxlock << this + ensures acc(mu) && waitlevel << this { head := new Node head.next := null share head - share this between maxlock and head + share this between waitlevel and head } method Add(key: int, value: Data) requires value != null - requires rd(mu) && maxlock << this + requires rd(mu) && waitlevel << this ensures rd(mu) { acquire this @@ -46,7 +46,7 @@ class AssociationList { } method Get(key: int) returns (d: Data) - requires rd(mu) && maxlock << this + requires rd(mu) && waitlevel << this ensures rd(mu) { d := null @@ -68,8 +68,8 @@ class AssociationList { invariant rd(p.next.key) && rd(p.next.value) && acc(p.next.next) invariant p.next.next != null ==> acc(p.next.next.mu,50) && p.next << p.next.next - invariant holds(p) && holds(p.next) && maxlock == p.next.mu - invariant p.next.next != null ==> maxlock << p.next.next + invariant holds(p) && holds(p.next) && waitlevel == p.next.mu + invariant p.next.next != null ==> waitlevel << p.next.next lockchange p, p.next.next { if (p.next.next == null) { diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice index 842e3d7d..79e4d75e 100644 --- a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice +++ b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice @@ -29,7 +29,7 @@ class Node { class Program { method Putter(e: C, x0: Node) - requires e!= null && acc(e.mu, 50) && e.mu == maxlock && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1)); + requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1)); { var x: Node := x0; var t: Node; @@ -42,7 +42,7 @@ class Program { send e(1, x); x := t; var ack; - assume maxlock << e.mu; // Chalice should be able to figure this out itself + assume waitlevel << e.mu; // Chalice should be able to figure this out itself receive ack, t := e; if(ack != 2) { assume false; /* abort */ } } @@ -50,12 +50,12 @@ class Program { } method Getter(f: C) - requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu; + requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu; { var x: Node := null; var msg := 1; while(msg != 0) - invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50)); + invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50)); { receive msg, x := f; if(msg == 0) { diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice index 51fd469c..41680258 100644 --- a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice +++ b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice @@ -32,7 +32,7 @@ class Node { class Program { method Putter(e: C, x0: Node, ackC: AckChannel) - requires e!= null && acc(e.mu, 50) && e.mu == maxlock && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1)); + requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1)); { var x: Node := x0; var t: Node; @@ -45,7 +45,7 @@ class Program { send e(1, x, ackC); x := t; var ack; - assume maxlock << ackC.mu; // Chalice should be able to figure this out itself? + assume waitlevel << ackC.mu; // Chalice should be able to figure this out itself? var ctmp: C; receive ctmp := ackC; if(ctmp != e) { assume false; /* abort */ } @@ -54,12 +54,12 @@ class Program { } method Getter(f: C, ackC: AckChannel) - requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu; + requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu; { var x: Node := null; var msg := 1; while(msg != 0) - invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50) && acc(ackC.mu, 50)); + invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50) && acc(ackC.mu, 50)); { var ackC2: AckChannel; receive msg, x, ackC2 := f; diff --git a/Chalice/examples/CopyLessMessagePassing.chalice b/Chalice/examples/CopyLessMessagePassing.chalice index 1363bb2a..f5ca2372 100644 --- a/Chalice/examples/CopyLessMessagePassing.chalice +++ b/Chalice/examples/CopyLessMessagePassing.chalice @@ -43,12 +43,12 @@ class Program { } method Getter(f: C) - requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu; + requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu; { var x: Node := null; var msg := 1; while(msg != 0) - invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50)); + invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50)); { receive msg, x := f; if(msg == 1) { diff --git a/Chalice/examples/HandOverHand.chalice b/Chalice/examples/HandOverHand.chalice index f0f6323a..8318a77c 100644 --- a/Chalice/examples/HandOverHand.chalice +++ b/Chalice/examples/HandOverHand.chalice @@ -18,7 +18,7 @@ class List { method Init() requires acc(mu) && mu == lockbottom && acc(head) && acc(sum) - ensures rd(mu,*) && maxlock << this + ensures rd(mu,*) && waitlevel << this ensures acc(sum,80) && sum == 0 { var t := new Node @@ -28,17 +28,17 @@ class List { share t head := t sum := 0 - share this between maxlock and t + share this between waitlevel and t } method Insert(x: int) - requires rd(mu) && maxlock << this + requires rd(mu) && waitlevel << this requires acc(sum,80) && 0 <= x ensures rd(mu) ensures acc(sum,80) && sum == old(sum) + x { acquire this - assert maxlock == this.mu; + assert waitlevel == this.mu; sum := sum + x var p: Node := head acquire p @@ -47,7 +47,7 @@ class List { while (p.next != null && p.next.val < x) invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50) - invariant holds(p) && maxlock == p.mu + invariant holds(p) && waitlevel == p.mu invariant p.next != null ==> acc(p.next.mu,50) && p << p.next invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val invariant acc(p.sum, 50) @@ -72,7 +72,7 @@ class List { } method Delete(x: int) returns (wasPresent: bool) - requires rd(mu) && maxlock << this + requires rd(mu) && waitlevel << this requires acc(sum,80) && 0 <= x ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum)) { @@ -87,7 +87,7 @@ class List { while (p.next != null && p.next.val < x) invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50) - invariant holds(p) && maxlock == p.mu && !assigned(c) + invariant holds(p) && waitlevel == p.mu && !assigned(c) invariant p.next != null ==> acc(p.next.mu,50) && p << p.next invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val invariant acc(p.sum, 50) diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/examples/OwickiGries.chalice index 63f029e8..f466b58a 100644 --- a/Chalice/examples/OwickiGries.chalice +++ b/Chalice/examples/OwickiGries.chalice @@ -17,7 +17,7 @@ class OwickiGries { } method Worker(b: bool) - requires rd(mu) && maxlock << mu + requires rd(mu) && waitlevel << mu requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50)) ensures rd(mu) ensures !b ==> acc(c0,50) && c0 == old(c0) + 1 diff --git a/Chalice/examples/ProdConsChannel.chalice b/Chalice/examples/ProdConsChannel.chalice index e8ab1a60..563d72b6 100644 --- a/Chalice/examples/ProdConsChannel.chalice +++ b/Chalice/examples/ProdConsChannel.chalice @@ -28,14 +28,14 @@ class Program { send ch(null) } method Consumer(ch: Ch) - requires rd(ch.mu) && maxlock << ch.mu + requires rd(ch.mu) && waitlevel << ch.mu requires credit(ch) ensures rd(ch.mu) { var c: Cell receive c := ch while (c != null) - invariant rd(ch.mu) && maxlock << ch.mu + invariant rd(ch.mu) && waitlevel << ch.mu invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch) { var i := c.val @@ -87,14 +87,14 @@ class Program { send ch(null) } method Consumer0(ch: Ch) - requires rd(ch.mu) && maxlock << ch.mu + requires rd(ch.mu) && waitlevel << ch.mu requires credit(ch) ensures rd(ch.mu) { var c: Cell receive c := ch while (c != null && c.val == 7) // this consumer may end early, but that's allowed - invariant rd(ch.mu) && maxlock << ch.mu + invariant rd(ch.mu) && waitlevel << ch.mu invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch) { var i := c.val @@ -102,7 +102,7 @@ class Program { } } method Consumer1(ch: Ch) - requires rd(ch.mu) && maxlock << ch.mu + requires rd(ch.mu) && waitlevel << ch.mu requires credit(ch) ensures rd(ch.mu) { @@ -113,7 +113,7 @@ class Program { } } method Consumer2(ch: Ch) - requires rd(ch.mu) && maxlock << ch.mu + requires rd(ch.mu) && waitlevel << ch.mu requires credit(ch) ensures rd(ch.mu) { diff --git a/Chalice/examples/Sieve.chalice b/Chalice/examples/Sieve.chalice index be282402..a7ec9d10 100644 --- a/Chalice/examples/Sieve.chalice +++ b/Chalice/examples/Sieve.chalice @@ -18,12 +18,12 @@ class Sieve { method Filter(prime: int, r: NumberStream, s: NumberStream) requires 2 <= prime; - requires rd(r.mu) && maxlock << r.mu; + requires rd(r.mu) && waitlevel << r.mu; requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1); { receive x := r; while (2 <= x) - invariant rd(r.mu) && rd(s.mu) && s << r && maxlock << r.mu; + invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu; invariant 2<= x ==> credit(r); invariant credit(s, -1); { @@ -45,12 +45,12 @@ class Sieve { while (2 <= p) invariant ch != null; invariant 2 <= p ==> credit(ch, 1); - invariant rd(ch.mu) && maxlock << ch.mu; + invariant rd(ch.mu) && waitlevel << ch.mu; { // print p--it's a prime! var cp := new ChalicePrint; call cp.Int(p); - var n := new NumberStream between maxlock and ch; + var n := new NumberStream between waitlevel and ch; fork Filter(p, ch, n); ch := n; receive p := ch; diff --git a/Chalice/examples/cell.chalice b/Chalice/examples/cell.chalice index d4003a3c..1cf82950 100644 --- a/Chalice/examples/cell.chalice +++ b/Chalice/examples/cell.chalice @@ -57,7 +57,7 @@ class Interval module Library2 { requires 0<=l && l <= r; requires acc(left) && acc(right); ensures valid; - ensures getLeft()==l + ensures getLeft()==l; ensures getRight()==r; { left := new Cell; @@ -143,10 +143,10 @@ class Program module Main { } method main3() returns (rt: Cell) - ensures rt!=null && rt.valid && rt.get() == 0 + ensures rt!=null && rt.valid && rt.get() == 0; { rt := new Cell; - call rt.init(0) + call rt.init(0); } method main4() { diff --git a/Chalice/examples/counter.chalice b/Chalice/examples/counter.chalice index 0cab7736..828cf005 100644 --- a/Chalice/examples/counter.chalice +++ b/Chalice/examples/counter.chalice @@ -34,7 +34,7 @@ class Program { } method bar(c: Counter) - requires c!=null && acc(c.mu) && maxlock << c.mu; + requires c!=null && acc(c.mu) && waitlevel << c.mu; requires eval(c.release, acc(c.value) && 0<=c.value); { lock (c) { @@ -81,7 +81,7 @@ class Program { } method foo(c: Counter) - requires c!=null && acc(c.mu) && maxlock << c.mu && eval(c.release, acc(c.value) && 10<=c.value); + requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value); ensures c!=null && holds(c) && acc(c.mu) && acc(c.value); lockchange c; { @@ -93,7 +93,7 @@ class Program { } method nestedGood0(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { lock (c) { release c @@ -102,7 +102,7 @@ class Program { } method nestedGood1(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { var t: Counter := c lock (t) { @@ -114,7 +114,7 @@ class Program { } method nestedBad0(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { lock (c) { release c @@ -122,7 +122,7 @@ class Program { } method nestedBad1(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { lock (c) { acquire c // error: already holds c @@ -130,7 +130,7 @@ class Program { } method nestedBad2(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { lock (c) { lock (c) { // error: already holds c @@ -139,7 +139,7 @@ class Program { } method nestedBad3(c: Counter) - requires c != null && acc(c.mu) && maxlock << c.mu; + requires c != null && acc(c.mu) && waitlevel << c.mu; { var t: Counter := c lock (t) { diff --git a/Chalice/examples/dining-philosophers.chalice b/Chalice/examples/dining-philosophers.chalice index 6a67174c..f4a7d1a6 100644 --- a/Chalice/examples/dining-philosophers.chalice +++ b/Chalice/examples/dining-philosophers.chalice @@ -17,12 +17,12 @@ class Philosopher module Philosophers { requires valid; requires acc(getLeft().mu, 10); requires acc(getRight().mu, 10); - requires maxlock << getLeft().mu; - requires maxlock << getRight().mu; + requires waitlevel << getLeft().mu; + requires waitlevel << getRight().mu; requires getLeft().mu << getRight().mu; { while(true) - invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && maxlock << getLeft().mu && maxlock << getRight().mu && getLeft().mu << getRight().mu; + invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && waitlevel << getLeft().mu && waitlevel << getRight().mu && getLeft().mu << getRight().mu; { unfold valid; acquire left; diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/examples/producer-consumer.chalice index f2c751d9..99756d65 100644 --- a/Chalice/examples/producer-consumer.chalice +++ b/Chalice/examples/producer-consumer.chalice @@ -34,13 +34,13 @@ class Producer module Producer { } method run() - requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu; + requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu; ensures rd(old(getBuffer()).mu); { var tmp: int; while(true) - invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu; + invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu; { unfold valid; acquire buffer; @@ -75,11 +75,11 @@ class Consumer module Consumer { } method run() - requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu; + requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu; ensures rd(old(getBuffer()).mu); { while(true) - invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu; + invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu; { unfold valid; acquire buffer; diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice index 7bcb1505..fb835a24 100644 --- a/Chalice/examples/prog0.chalice +++ b/Chalice/examples/prog0.chalice @@ -32,7 +32,7 @@ class C { call this.m(2,3,4); call a,b,c := o.m(); call x := m(200); - reorder o above maxlock; + reorder o above waitlevel; } method p(a,b,c) returns (x,y,z) requires 8 + 2 == 10; diff --git a/Chalice/examples/prog3.chalice b/Chalice/examples/prog3.chalice index 6c323d0e..f3b8210b 100644 --- a/Chalice/examples/prog3.chalice +++ b/Chalice/examples/prog3.chalice @@ -7,9 +7,9 @@ class Main { share d; var t0: T := new T; t0.d := d; - share t0 between maxlock and d + share t0 between waitlevel and d var t1: T := new T; t1.d := d; - share t1 between maxlock and d + share t1 between waitlevel and d var t0Token: token; fork t0Token := t0.run(); @@ -33,15 +33,15 @@ class Main { fork uToken := u.run(); acquire u; // a little unusual to acquire after a fork, but allowed - assert maxlock == u.mu; + assert waitlevel == u.mu; var v := new U; - share v; acquire v; // this line has the effect of increasing maxlock + share v; acquire v; // this line has the effect of increasing waitlevel - assert maxlock == v.mu; - assert maxlock != u.mu; + assert waitlevel == v.mu; + assert waitlevel != u.mu; assert u << v; - assert u << maxlock; + assert u << waitlevel; join uToken; // material for the smoke check release u; @@ -49,7 +49,7 @@ class Main { } method C() - ensures maxlock == old(maxlock); + ensures waitlevel == old(waitlevel); { var u := new U; share u; @@ -65,23 +65,23 @@ class Main { { } method MxCaller0() - ensures maxlock == old(maxlock); + ensures waitlevel == old(waitlevel); { } method MxCaller1() - ensures maxlock == old(maxlock); + ensures waitlevel == old(waitlevel); { call Mx0(); } method MxCaller2() - ensures maxlock == old(maxlock); // error + ensures waitlevel == old(waitlevel); // error { call Mx1(); } // error: missing lockchange method D(u: U) - requires u != null && rd(u.mu) && maxlock << u; - ensures maxlock == old(maxlock); + requires u != null && rd(u.mu) && waitlevel << u; + ensures waitlevel == old(waitlevel); { acquire u; release u; @@ -103,7 +103,7 @@ class T { var d: Data; invariant rd(d) && d != null && rd(d.mu) && rd(this.mu) && this << d; method run() - requires rd(mu) && maxlock << this; + requires rd(mu) && waitlevel << this; ensures rd(mu); { acquire this; @@ -117,7 +117,7 @@ class T { class U { method run() - requires rd(mu) && maxlock << this; + requires rd(mu) && waitlevel << this; ensures rd(mu); { } diff --git a/Chalice/examples/prog4.chalice b/Chalice/examples/prog4.chalice index 655c5815..bc6aef99 100644 --- a/Chalice/examples/prog4.chalice +++ b/Chalice/examples/prog4.chalice @@ -22,7 +22,7 @@ class LoopTargets { acquire t var s := true while (s) - invariant acc(t.mu) && maxlock == t.mu + invariant acc(t.mu) && waitlevel == t.mu { release t // error: loop invariant does not say holds(t) (414) acquire t @@ -37,7 +37,7 @@ class LoopTargets { var s := true while (s) invariant rd(t.mu) - invariant holds(t) && maxlock == t.mu + invariant holds(t) && waitlevel == t.mu { release t acquire t diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala index b60ce521..c353a5ba 100644 --- a/Chalice/src/Boogie.scala +++ b/Chalice/src/Boogie.scala @@ -7,274 +7,274 @@ import scala.util.parsing.input.Position import scala.util.parsing.input.NoPosition object Boogie { - - sealed abstract class Decl - case class Const(id: String, unique: boolean, t: BType) extends Decl - case class Proc(id: String, ins: List[BVar], outs: List[BVar], - mod: List[String], PrePost: List[String], - body: List[Stmt]) extends Decl - case class Function(id: String, ins: List[BVar], out: BVar) extends Decl - case class Axiom(expr: Expr) extends Decl + + sealed abstract class Decl + case class Const(id: String, unique: boolean, t: BType) extends Decl + case class Proc(id: String, ins: List[BVar], outs: List[BVar], + mod: List[String], PrePost: List[String], + body: List[Stmt]) extends Decl + case class Function(id: String, ins: List[BVar], out: BVar) extends Decl + case class Axiom(expr: Expr) extends Decl - sealed abstract class BType - case class NamedType(s: String) extends BType - case class ClassType(cl: Class) extends BType - case class IndexedType(id: String, t: BType) extends BType + sealed abstract class BType + case class NamedType(s: String) extends BType + case class ClassType(cl: Class) extends BType + case class IndexedType(id: String, t: BType) extends BType - sealed abstract class Stmt { - def Locals = List[BVar]() - } - case class Comment(comment: String) extends Stmt - case class Assert(e: Expr) extends Stmt { - def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this } - var pos = NoPosition : Position - var message = "" : String - } - case class Assume(e: Expr) extends Stmt - case class Assign(lhs: Expr, rhs: Expr) extends Stmt - case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt - case class Havoc(x: Expr) extends Stmt - case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt { - def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs) - } - case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt { - override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals)) - } - case class LocalVar(x: BVar) extends Stmt { - def this(id: String, tp: BType) = this(BVar(id, tp)) + sealed abstract class Stmt { + def Locals = List[BVar]() + } + case class Comment(comment: String) extends Stmt + case class Assert(e: Expr) extends Stmt { + def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this } + var pos = NoPosition : Position + var message = "" : String + } + case class Assume(e: Expr) extends Stmt + case class Assign(lhs: Expr, rhs: Expr) extends Stmt + case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt + case class Havoc(x: Expr) extends Stmt + case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt { + def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs) + } + case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt { + override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals)) + } + case class LocalVar(x: BVar) extends Stmt { + def this(id: String, tp: BType) = this(BVar(id, tp)) - override def Locals = List(x) - } + override def Locals = List(x) + } - sealed abstract class Expr { - def &&(that: Expr) = BinaryExpr("&&", this, that) - def ||(that: Expr) = BinaryExpr("||", this, that) - def ==@(that: Expr) = BinaryExpr("==", this, that) - def !=@(that: Expr) = BinaryExpr("!=", this, that) - def Equals(that: Expr) = BinaryExpr("==", this, that) - def ==>(that: Expr) = BinaryExpr("==>", this, that) - def <==>(that: Expr) = BinaryExpr("<==>", this, that) - def unary_! = UnaryExpr("!", this) - def <=(that: Expr) = BinaryExpr("<=", this, that) - def <(that: Expr) = BinaryExpr("<", this, that) - def >=(that: Expr) = BinaryExpr(">=", this, that) - def >(that: Expr) = BinaryExpr(">", this, that) - def +(that: Expr) = BinaryExpr("+", this, that) - def -(that: Expr) = BinaryExpr("-", this, that) - def *(that: Expr) = BinaryExpr("*", this, that) - def /(that: Expr) = BinaryExpr("/", this, that) - def %(that: Expr) = BinaryExpr("%", this, that) - def := (that: Expr) = Assign(this, that) - def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f)) - def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs) - } - case class IntLiteral(n: int) extends Expr - case class BoolLiteral(b: boolean) extends Expr - case class Null extends Expr - case class VarExpr(id: String) extends Expr { - def this(v: BVar) = this(v.id) - } - case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr { - def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps - def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps - this(MapSelect(map, arg0, arg1), VarExpr(arg2), null) - } - case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr - case class Old(e: Expr) extends Expr - case class UnaryExpr(op: String, e: Expr) extends Expr - case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr - case class FunctionApp(f: String, args: List[Expr]) extends Expr { - def this(f: String, a0: Expr) = this(f, List(a0)) - def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1)) - def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2)) - } - case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr { - def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body) - def this(x: BVar, body: Expr) = this(List(), List(x), List(), body) - def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body) - } - case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr { - def this(x: BVar, body: Expr) = this(List(x), List(), body) - } - case class Ite(con: Expr, then: Expr, els: Expr) extends Expr + sealed abstract class Expr { + def &&(that: Expr) = BinaryExpr("&&", this, that) + def ||(that: Expr) = BinaryExpr("||", this, that) + def ==@(that: Expr) = BinaryExpr("==", this, that) + def !=@(that: Expr) = BinaryExpr("!=", this, that) + def Equals(that: Expr) = BinaryExpr("==", this, that) + def ==>(that: Expr) = BinaryExpr("==>", this, that) + def <==>(that: Expr) = BinaryExpr("<==>", this, that) + def unary_! = UnaryExpr("!", this) + def <=(that: Expr) = BinaryExpr("<=", this, that) + def <(that: Expr) = BinaryExpr("<", this, that) + def >=(that: Expr) = BinaryExpr(">=", this, that) + def >(that: Expr) = BinaryExpr(">", this, that) + def +(that: Expr) = BinaryExpr("+", this, that) + def -(that: Expr) = BinaryExpr("-", this, that) + def *(that: Expr) = BinaryExpr("*", this, that) + def /(that: Expr) = BinaryExpr("/", this, that) + def %(that: Expr) = BinaryExpr("%", this, that) + def := (that: Expr) = Assign(this, that) + def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f)) + def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs) + } + case class IntLiteral(n: int) extends Expr + case class BoolLiteral(b: boolean) extends Expr + case class Null extends Expr + case class VarExpr(id: String) extends Expr { + def this(v: BVar) = this(v.id) + } + case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr { + def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps + def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps + this(MapSelect(map, arg0, arg1), VarExpr(arg2), null) + } + case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr + case class Old(e: Expr) extends Expr + case class UnaryExpr(op: String, e: Expr) extends Expr + case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr + case class FunctionApp(f: String, args: List[Expr]) extends Expr { + def this(f: String, a0: Expr) = this(f, List(a0)) + def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1)) + def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2)) + } + case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr { + def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body) + def this(x: BVar, body: Expr) = this(List(), List(x), List(), body) + def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body) + } + case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr { + def this(x: BVar, body: Expr) = this(List(x), List(), body) + } + case class Ite(con: Expr, then: Expr, els: Expr) extends Expr - case class BVar(id: String, t: BType) { - def this(id: String, t: BType, uniquifyName: boolean) = - this(if (uniquifyName) { - val n = S_BVar.VariableCount - S_BVar.VariableCount = S_BVar.VariableCount + 1 - id + "#_" + n - } else { - id - }, t) - val where: Expr = null - } - object S_BVar { var VariableCount = 0 } - def NewBVar(id: String, t: BType, uniquifyName: boolean) = { - val v = new Boogie.BVar(id, t, uniquifyName) - val e = new Boogie.VarExpr(v) - (v,e) - } - case class TVar(id: String) { - def this(id: String, uniquifyName: boolean) = - this(if (uniquifyName) { - val n = S_TVar.VariableCount - S_TVar.VariableCount = S_TVar.VariableCount + 1 - id + "#_" + n - } else { - id - }) - val where: Expr = null - } - object S_TVar { var VariableCount = 0 } - def NewTVar(id: String) = { - val v = new Boogie.TVar(id, true) - val e = new Boogie.NamedType(v.id) - (v,e) - } + case class BVar(id: String, t: BType) { + def this(id: String, t: BType, uniquifyName: boolean) = + this(if (uniquifyName) { + val n = S_BVar.VariableCount + S_BVar.VariableCount = S_BVar.VariableCount + 1 + id + "#_" + n + } else { + id + }, t) + val where: Expr = null + } + object S_BVar { var VariableCount = 0 } + def NewBVar(id: String, t: BType, uniquifyName: boolean) = { + val v = new Boogie.BVar(id, t, uniquifyName) + val e = new Boogie.VarExpr(v) + (v,e) + } + case class TVar(id: String) { + def this(id: String, uniquifyName: boolean) = + this(if (uniquifyName) { + val n = S_TVar.VariableCount + S_TVar.VariableCount = S_TVar.VariableCount + 1 + id + "#_" + n + } else { + id + }) + val where: Expr = null + } + object S_TVar { var VariableCount = 0 } + def NewTVar(id: String) = { + val v = new Boogie.TVar(id, true) + val e = new Boogie.NamedType(v.id) + (v,e) + } - var vsMode = false; // global variable settable from outside the class (non-ideal design) + var vsMode = false; // global variable settable from outside the class (non-ideal design) - // def out(s: String) = Console.out.print(s) - var indentLevel = 1 - def indent: String = { - def doIndent(i: int): String = { - if(i==0) { "" } else { " " + doIndent(i-1) } - } - doIndent(indentLevel); - } + // def out(s: String) = Console.out.print(s) + var indentLevel = 1 + def indent: String = { + def doIndent(i: int): String = { + if(i==0) { "" } else { " " + doIndent(i-1) } + } + doIndent(indentLevel); + } - def IndentMore(what: => String) = { - val prev = indentLevel - indentLevel = indentLevel + 1 - val result = what - indentLevel = prev - result - } - def nl = System.getProperty("line.separator"); - - def Print[T](list: List[T], sep: String, p: T => String): String = list match { - case Nil => "" - case x :: Nil => p(x) - case x :: xs => p(x) + sep + Print(xs, sep, p) - } - def PrintType(t: BType): String = t match { - case nt@ NamedType(s) => - s - case ClassType(cl) => - if (cl.IsRef) "ref" else cl.id - case IndexedType(id,t) => - id + " (" + PrintType(t) + ")" - } - def Print(d: Decl): String = d match { - case Const(id, u, t) => - "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl - case p: Proc => - "procedure " + p.id + - "(" + Print(p.ins, ", ", PrintVar) + ")" + - " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl + - (p.mod match { - case Nil => "" - case x :: xs => - indent + "modifies " + - Print(p.mod, ", ", { s: String => s }) + - ";" + nl - }) + - Print(p.PrePost, nl, { spec: String => indent + spec }) + nl + - "{" + nl + - Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) + - Print(p.body, "", PrintStmt) + - "}" + nl - case Function(id, ins, out) => - "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl - case Axiom(e) => - "axiom " + PrintExpr(e) + ";" + nl - } - def PrintVar(v: BVar): String = { - v.id + ": " + PrintType(v.t) + - (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" }) - } - def PrintStmt(s: Stmt): String = s match { - case Comment(msg) => indent + "// " + msg + nl - case assert@Assert(e) => - val pos = if (vsMode) { - val r = assert.pos.line - 1; - val c = assert.pos.column - 1; - r + "," + c + "," + r + "," + (c+5) + ":" - } else { - " " + assert.pos + ": " - } - indent + "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl - case Assume(e) => indent + "assume " + PrintExpr(e) + ";" + nl - case If(guard, thn, els) => - indent + "if (" + - (if (guard == null) "*" else PrintExpr(guard)) + - ") {" + nl + - IndentMore { Print(thn, "", PrintStmt) } + - indent + "} else {" + nl + - IndentMore { Print(els, "", PrintStmt) } + - indent + "}" + nl - case Assign(lhs, rhs) => - indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl - case AssignMap(lhs, index, rhs) => - indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl - case Havoc(lhs) => - indent + "havoc " + PrintExpr(lhs) + ";" + nl - case MapUpdate(map, a0, a1, rhs) => - indent + PrintExpr(map) + "[" + - PrintExpr(a0) + - (if (a1 != null) { ", " + a1 } else { "" }) + - "] := " + - PrintExpr(rhs) + ";" + nl - case _:LocalVar => "" /* print nothing */ - } - def PrintExpr(e: Expr): String = { - PrintExpr(e, false) - } - def PrintExpr(e: Expr, useParens: boolean): String = e match { - case IntLiteral(n) => n.toString - case BoolLiteral(b) => b.toString - case Null() => "null" - case VarExpr(id) => id - case MapSelect(map, arg0, arg1) => - PrintExpr(map) + "[" + PrintExpr(arg0, false) + - (if (arg1 != null) { ", " + arg1 } else { "" }) + - "]" - case MapStore(map, arg0, rhs) => - PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]" - case Old(e) => "old(" + PrintExpr(e, false) + ")" - case UnaryExpr(op, e) => - (if (useParens) { "(" } else "") + - op + PrintExpr(e, true) + - (if (useParens) ")" else "" ) - case BinaryExpr(op, e0, e1) => - // reduce parentheses in a special common case: - val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>"; - def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false } - (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) + - " " + op + " " + - PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) + - (if (useParens) ")" else "") - case FunctionApp(f, args) => - f + "(" + - Print(args, ", ", { e: Expr => PrintExpr(e, false) }) + - ")" - case Ite(con, then, els) => - "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")" - case Forall(ts, xs, triggers, body) => - "(forall" + - (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") + - Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) + - " :: " + - Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) + - PrintExpr(body) + - ")" - case Exists(xs, triggers, body) => - "(exists " + - Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) + - " :: " + - Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) + - PrintExpr(body) + - ")" - } + def IndentMore(what: => String) = { + val prev = indentLevel + indentLevel = indentLevel + 1 + val result = what + indentLevel = prev + result + } + def nl = System.getProperty("line.separator"); + + def Print[T](list: List[T], sep: String, p: T => String): String = list match { + case Nil => "" + case x :: Nil => p(x) + case x :: xs => p(x) + sep + Print(xs, sep, p) + } + def PrintType(t: BType): String = t match { + case nt@ NamedType(s) => + s + case ClassType(cl) => + if (cl.IsRef) "ref" else cl.id + case IndexedType(id,t) => + id + " (" + PrintType(t) + ")" + } + def Print(d: Decl): String = d match { + case Const(id, u, t) => + "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl + case p: Proc => + "procedure " + p.id + + "(" + Print(p.ins, ", ", PrintVar) + ")" + + " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl + + (p.mod match { + case Nil => "" + case x :: xs => + indent + "modifies " + + Print(p.mod, ", ", { s: String => s }) + + ";" + nl + }) + + Print(p.PrePost, nl, { spec: String => indent + spec }) + nl + + "{" + nl + + Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) + + Print(p.body, "", PrintStmt) + + "}" + nl + case Function(id, ins, out) => + "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl + case Axiom(e) => + "axiom " + PrintExpr(e) + ";" + nl + } + def PrintVar(v: BVar): String = { + v.id + ": " + PrintType(v.t) + + (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" }) + } + def PrintStmt(s: Stmt): String = s match { + case Comment(msg) => indent + "// " + msg + nl + case assert@Assert(e) => + val pos = if (vsMode) { + val r = assert.pos.line - 1; + val c = assert.pos.column - 1; + r + "," + c + "," + r + "," + (c+5) + ":" + } else { + " " + assert.pos + ": " + } + indent + "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl + case Assume(e) => indent + "assume " + PrintExpr(e) + ";" + nl + case If(guard, thn, els) => + indent + "if (" + + (if (guard == null) "*" else PrintExpr(guard)) + + ") {" + nl + + IndentMore { Print(thn, "", PrintStmt) } + + indent + "} else {" + nl + + IndentMore { Print(els, "", PrintStmt) } + + indent + "}" + nl + case Assign(lhs, rhs) => + indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl + case AssignMap(lhs, index, rhs) => + indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl + case Havoc(lhs) => + indent + "havoc " + PrintExpr(lhs) + ";" + nl + case MapUpdate(map, a0, a1, rhs) => + indent + PrintExpr(map) + "[" + + PrintExpr(a0) + + (if (a1 != null) { ", " + a1 } else { "" }) + + "] := " + + PrintExpr(rhs) + ";" + nl + case _:LocalVar => "" /* print nothing */ + } + def PrintExpr(e: Expr): String = { + PrintExpr(e, false) + } + def PrintExpr(e: Expr, useParens: boolean): String = e match { + case IntLiteral(n) => n.toString + case BoolLiteral(b) => b.toString + case Null() => "null" + case VarExpr(id) => id + case MapSelect(map, arg0, arg1) => + PrintExpr(map) + "[" + PrintExpr(arg0, false) + + (if (arg1 != null) { ", " + arg1 } else { "" }) + + "]" + case MapStore(map, arg0, rhs) => + PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]" + case Old(e) => "old(" + PrintExpr(e, false) + ")" + case UnaryExpr(op, e) => + (if (useParens) { "(" } else "") + + op + PrintExpr(e, true) + + (if (useParens) ")" else "" ) + case BinaryExpr(op, e0, e1) => + // reduce parentheses in a special common case: + val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>"; + def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false } + (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) + + " " + op + " " + + PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) + + (if (useParens) ")" else "") + case FunctionApp(f, args) => + f + "(" + + Print(args, ", ", { e: Expr => PrintExpr(e, false) }) + + ")" + case Ite(con, then, els) => + "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")" + case Forall(ts, xs, triggers, body) => + "(forall" + + (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") + + Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) + + " :: " + + Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) + + PrintExpr(body) + + ")" + case Exists(xs, triggers, body) => + "(exists " + + Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) + + " :: " + + Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) + + PrintExpr(body) + + ")" + } } diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 1a6e3e48..2f54b71f 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -10,125 +10,128 @@ import java.io.FileWriter import scala.util.parsing.input.Position object Chalice { - def main(args: Array[String]): unit = { - var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe" - // parse command-line arguments - var inputName: String = null - var printProgram = false - var vsMode = false; - def ReportError(pos: Position, msg: String) = { - if (vsMode) { - val r = pos.line - 1; - val c = pos.column - 1; - Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg); - } else { - Console.err.println(pos + ": " + msg) - } - } - var doTypecheck = true - var doTranslate = true - var checkLeaks = false - // level 0 or below: no defaults - // level 1: unfold predicates with receiver this in pre and postconditions - // level 2: unfold predicates and functions with receiver this in pre and postconditions - // level 3 or above: level 2 + autoMagic - var defaults = 0 - var autoFold = false - var autoMagic = false - var skipDeadlockChecks = false - var boogieArgs = " "; - var gen = false; + def main(args: Array[String]): unit = { + var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe" + // parse command-line arguments + var inputName: String = null + var printProgram = false + var vsMode = false; + def ReportError(pos: Position, msg: String) = { + if (vsMode) { + val r = pos.line - 1; + val c = pos.column - 1; + Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg); + } else { + Console.err.println(pos + ": " + msg) + } + } + var doTypecheck = true + var doTranslate = true + var checkLeaks = false + // level 0 or below: no defaults + // level 1: unfold predicates with receiver this in pre and postconditions + // level 2: unfold predicates and functions with receiver this in pre and postconditions + // level 3 or above: level 2 + autoMagic + var defaults = 0 + var autoFold = false + var autoMagic = false + var skipDeadlockChecks = false + var boogieArgs = " "; + var gen = false; - for (a <- args) { - if (a == "-print") printProgram = true - else if (a == "-noTranslate") doTranslate = false - else if (a == "-noTypecheck") doTypecheck = false - else if (a == "-vs") vsMode = true - else if (a == "-checkLeaks") checkLeaks = true - else if (a == "-noDeadlockChecks") skipDeadlockChecks = true - else if (a.startsWith("-boogie:")) boogiePath = a.substring(8) - else if (a == "-defaults") defaults = 3 - else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } } - else if (a == "-gen") { gen = true; } - else if (a == "-autoFold") autoFold = true - else if (a == "-autoMagic") autoMagic = true - else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe - else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return } - else { inputName = a } - } - // check the command-line arguments - if (inputName == null) { CommandLineError("missing input filename"); return } else { - val file = new File(inputName); - if(! file.exists()){ - CommandLineError("input file " + file.getName() + " could not be found"); return - } - } - // parse program - val parser = new Parser(); - parser.parseFile(inputName) match { - case e: parser.NoSuccess => - if (vsMode) - ReportError(e.next.pos, e.msg); - else - Console.err.println("Error: " + e) - case parser.Success(prog, _) => - if (printProgram) PrintProgram.P(prog) - if (doTypecheck) { - // typecheck program - Resolver.Resolve(prog) match { - case Resolver.Errors(msgs) => - if (!vsMode) Console.err.println("The program did not typecheck."); - msgs foreach { msg => ReportError(msg._1, msg._2) } - case Resolver.Success() => - if (doTranslate) { - // checking if Boogie.exe exists - val boogieFile = new File(boogiePath); - if(! boogieFile.exists() || ! boogieFile.isFile()) { - CommandLineError("Boogie.exe not found at " + boogiePath); return - } - // translate program to Boogie - val translator = new Translator(); - // set the translation options - TranslationOptions.checkLeaks = checkLeaks; - TranslationOptions.defaults = defaults; - TranslationOptions.autoFold = autoFold; - TranslationOptions.autoMagic = autoMagic; - TranslationOptions.skipDeadlockChecks = skipDeadlockChecks; - val bplProg = translator.translateProgram(prog); - // write to out.bpl - Boogie.vsMode = vsMode; - val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b }; - writeFile("out.bpl", bplText); - // run Boogie.exe on out.bpl - val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + "out.bpl"); - val input = new BufferedReader(new InputStreamReader(boogie.getInputStream())); - var line = input.readLine(); - var previous_line = null: String; - while(line!=null){ - println(line); - previous_line = line; - line = input.readLine(); - } - if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack - val converter = new ChaliceToCSharp(); - println("Code generated in out.cs."); - writeFile("out.cs", converter.convertProgram(prog)); - } - } - } - } - } - } + for (a <- args) { + if (a == "-print") printProgram = true + else if (a == "-noTranslate") doTranslate = false + else if (a == "-noTypecheck") doTypecheck = false + else if (a == "-vs") vsMode = true + else if (a == "-checkLeaks") checkLeaks = true + else if (a == "-noDeadlockChecks") skipDeadlockChecks = true + else if (a.startsWith("-boogie:")) boogiePath = a.substring(8) + else if (a == "-defaults") defaults = 3 + else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } } + else if (a == "-gen") { gen = true; } + else if (a == "-autoFold") autoFold = true + else if (a == "-autoMagic") autoMagic = true + else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe + else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return } + else { inputName = a } + } + // check the command-line arguments + if (inputName == null && vsMode) { + inputName = "" + } else if (inputName == null) { CommandLineError("missing input filename"); return } else { + val file = new File(inputName); + if(! file.exists()){ + CommandLineError("input file " + file.getName() + " could not be found"); return + } + } + // parse program + val parser = new Parser(); + parser.parseFile(inputName) match { + case e: parser.NoSuccess => + if (vsMode) + ReportError(e.next.pos, e.msg); + else + Console.err.println("Error: " + e) + case parser.Success(prog, _) => + if (printProgram) PrintProgram.P(prog) + if (doTypecheck) { + // typecheck program + Resolver.Resolve(prog) match { + case Resolver.Errors(msgs) => + if (!vsMode) Console.err.println("The program did not typecheck."); + msgs foreach { msg => ReportError(msg._1, msg._2) } + case Resolver.Success() => + if (doTranslate) { + // checking if Boogie.exe exists + val boogieFile = new File(boogiePath); + if(! boogieFile.exists() || ! boogieFile.isFile()) { + CommandLineError("Boogie.exe not found at " + boogiePath); return + } + // translate program to Boogie + val translator = new Translator(); + // set the translation options + TranslationOptions.checkLeaks = checkLeaks; + TranslationOptions.defaults = defaults; + TranslationOptions.autoFold = autoFold; + TranslationOptions.autoMagic = autoMagic; + TranslationOptions.skipDeadlockChecks = skipDeadlockChecks; + val bplProg = translator.translateProgram(prog); + // write to out.bpl + Boogie.vsMode = vsMode; + val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b }; + val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl" + writeFile(bplFilename, bplText); + // run Boogie.exe on out.bpl + val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename); + val input = new BufferedReader(new InputStreamReader(boogie.getInputStream())); + var line = input.readLine(); + var previous_line = null: String; + while(line!=null){ + println(line); + previous_line = line; + line = input.readLine(); + } + if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack + val converter = new ChaliceToCSharp(); + println("Code generated in out.cs."); + writeFile("out.cs", converter.convertProgram(prog)); + } + } + } + } + } + } - def writeFile(filename: String, text: String) { - val writer = new FileWriter(new File(filename)); - writer.write(text); - writer.flush(); - writer.close(); - } + def writeFile(filename: String, text: String) { + val writer = new FileWriter(new File(filename)); + writer.write(text); + writer.flush(); + writer.close(); + } - def CommandLineError(msg: String) = { - Console.err.println("Error: " + msg) - Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile") - } + def CommandLineError(msg: String) = { + Console.err.println("Error: " + msg) + Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile") + } } diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 4442526f..98ba0416 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -13,7 +13,11 @@ import scala.util.parsing.input.NoPosition class Parser extends StandardTokenParsers { def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = { - val tokens = new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path)); + val tokens = if (path == "") { + new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in)) + } else { + new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path)); + } phrase(programUnit)(tokens) } @@ -25,7 +29,7 @@ class Parser extends StandardTokenParsers { "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned", "call", "if", "else", "while", "invariant", "lockchange", "returns", "requires", "ensures", "where", - "int", "bool", "false", "true", "null", "maxlock", "lockbottom", + "int", "bool", "false", "true", "null", "waitlevel", "lockbottom", "module", "external", "predicate", "function", "free", "send", "receive", "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", @@ -406,7 +410,7 @@ class Parser extends StandardTokenParsers { | "false" ^^^ BoolLiteral(false) | "true" ^^^ BoolLiteral(true) | "null" ^^^ NullLiteral() - | "maxlock" ^^^ MaxLockLiteral() + | "waitlevel" ^^^ MaxLockLiteral() | "lockbottom" ^^^ LockBottomLiteral() | "this" ^^^ ExplicitThisExpr() | "result" ^^^ Result() diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index a97a04f9..dea0f2d5 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -199,7 +199,7 @@ object PrintProgram { case IntLiteral(n) => print(n) case BoolLiteral(b) => print(b) case NullLiteral() => print("null") - case MaxLockLiteral() => print("maxlock") + case MaxLockLiteral() => print("waitlevel") case LockBottomLiteral() => print("lockbottom") case _:ThisExpr => print("this") case _:Result => print("result") diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index 9e8e5b4a..4ce95b3e 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -7,1061 +7,1061 @@ import scala.util.parsing.input.Position import scala.util.parsing.input.Positional object Resolver { - sealed abstract class ResolverOutcome - case class Success extends ResolverOutcome - case class Errors(ss: List[(Position,String)]) extends ResolverOutcome + sealed abstract class ResolverOutcome + case class Success extends ResolverOutcome + case class Errors(ss: List[(Position,String)]) extends ResolverOutcome - var seqClasses = Map[String, SeqClass](); + var seqClasses = Map[String, SeqClass](); - class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) { - val Decls = decls - val CurrentClass = currentClass - var currentMember = null: Member; - def CurrentMember = currentMember: Member; - var errors: List[(Position,String)] = Nil - def Error(pos: Position, msg: String) { - errors = errors + (pos, msg) - } - def AddVariable(v: Variable): ProgramContext = { - new LProgramContext(v, this); - } - def LookupVariable(id: String): Option[Variable] = None - def IsVariablePresent(vr: Variable): boolean = false + class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) { + val Decls = decls + val CurrentClass = currentClass + var currentMember = null: Member; + def CurrentMember = currentMember: Member; + var errors: List[(Position,String)] = Nil + def Error(pos: Position, msg: String) { + errors = errors + (pos, msg) + } + def AddVariable(v: Variable): ProgramContext = { + new LProgramContext(v, this); + } + def LookupVariable(id: String): Option[Variable] = None + def IsVariablePresent(vr: Variable): boolean = false - private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, parent.CurrentClass) { - override def Error(pos: Position, msg: String) = parent.Error(pos, msg) - override def LookupVariable(id: String): Option[Variable] = { - if (id == v.id) Some(v) else parent.LookupVariable(id) - } - override def IsVariablePresent(vr: Variable): boolean = { - if (vr == v) true else parent.IsVariablePresent(vr) - } - override def CurrentMember() = { - parent.CurrentMember - } - } - } + private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, parent.CurrentClass) { + override def Error(pos: Position, msg: String) = parent.Error(pos, msg) + override def LookupVariable(id: String): Option[Variable] = { + if (id == v.id) Some(v) else parent.LookupVariable(id) + } + override def IsVariablePresent(vr: Variable): boolean = { + if (vr == v) true else parent.IsVariablePresent(vr) + } + override def CurrentMember() = { + parent.CurrentMember + } + } + } - def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = { - // register the channels as well as the classes and their members - var decls = Map[String,TopLevelDecl]() - for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) { - if (decls contains decl.id) { - return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id))) - } else { - decl match { - case cl: Class => - for (m <- cl.members) m match { - case _:MonitorInvariant => - case m: NamedMember => - m.Parent = cl - if (cl.mm contains m.Id) { - return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id))) - } else { - cl.mm = cl.mm + (m.Id -> m) - } - } - case ch: Channel => - } - decls = decls + (decl.id -> decl) - } - } - var errors = List[(Position,String)]() + def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = { + // register the channels as well as the classes and their members + var decls = Map[String,TopLevelDecl]() + for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) { + if (decls contains decl.id) { + return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id))) + } else { + decl match { + case cl: Class => + for (m <- cl.members) m match { + case _:MonitorInvariant => + case m: NamedMember => + m.Parent = cl + if (cl.mm contains m.Id) { + return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id))) + } else { + cl.mm = cl.mm + (m.Id -> m) + } + } + case ch: Channel => + } + decls = decls + (decl.id -> decl) + } + } + var errors = List[(Position,String)]() - // resolve types of members - val contextNoCurrentClass = new ProgramContext(decls, null) - for (decl <- prog) decl match { - case ch: Channel => - for (v <- ch.parameters) { - ResolveType(v.t, contextNoCurrentClass) - } - case cl: Class => - for (m <- cl.asInstanceOf[Class].members) m match { - case _:MonitorInvariant => - case Field(id,t) => - ResolveType(t, contextNoCurrentClass) - case Method(id, ins, outs, spec, body) => - for (v <- ins ++ outs) { - ResolveType(v.t, contextNoCurrentClass) - } - case _:Condition => - case _:Predicate => - case Function(id, ins, out, specs, definition) => - for (v <- ins) { - ResolveType(v.t, contextNoCurrentClass) - } - ResolveType(out, contextNoCurrentClass) + // resolve types of members + val contextNoCurrentClass = new ProgramContext(decls, null) + for (decl <- prog) decl match { + case ch: Channel => + for (v <- ch.parameters) { + ResolveType(v.t, contextNoCurrentClass) } - } - errors = errors ++ contextNoCurrentClass.errors; + case cl: Class => + for (m <- cl.asInstanceOf[Class].members) m match { + case _:MonitorInvariant => + case Field(id,t) => + ResolveType(t, contextNoCurrentClass) + case Method(id, ins, outs, spec, body) => + for (v <- ins ++ outs) { + ResolveType(v.t, contextNoCurrentClass) + } + case _:Condition => + case _:Predicate => + case Function(id, ins, out, specs, definition) => + for (v <- ins) { + ResolveType(v.t, contextNoCurrentClass) + } + ResolveType(out, contextNoCurrentClass) + } + } + errors = errors ++ contextNoCurrentClass.errors; - // now, resolve and typecheck all - // * Field types and Method formal-parameter types - // * Assign, FieldUpdate, and Call statements - // * VariableExpr and FieldSelect expressions - for (decl <- prog) decl match { - case ch: Channel => - val context = new ProgramContext(decls, ChannelClass(ch)) - var ctx = context - for (v <- ch.parameters) { - ctx = ctx.AddVariable(v) - } - ResolveExpr(ch.where, ctx, false, true)(false) - errors = errors ++ context.errors - case cl: Class => - val context = new ProgramContext(decls, cl) - for (m <- cl.members) { - context.currentMember = m; - m match { - case MonitorInvariant(e) => - ResolveExpr(e, context, true, true)(true) - if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")") - case _:Field => // nothing more to do - case m@Method(id, ins, outs, spec, body) => - var ctx = context - for (v <- ins ++ outs) { - ctx = ctx.AddVariable(v) - } - spec foreach { - case Precondition(e) => ResolveExpr(e, ctx, false, true)(false) - case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false) - case lc@LockChange(ee) => - if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") - ee foreach (e => ResolveExpr(e, ctx, true, false)(false)) - } - ResolveStmt(BlockStmt(body), ctx) - case Condition(id, None) => - case c@Condition(id, Some(e)) => - ResolveExpr(e, context, false, true)(false) - if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")") - case p@Predicate(id, e) => - var ctx = context; - ResolveExpr(e, ctx, false, true)(true); - if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")") - case f@Function(id, ins, out, spec, e) => - var ctx = context - for (v <- ins) { - ctx = ctx.AddVariable(v) - } - // TODO: disallow credit(...) expressions in function specifications - spec foreach { - case Precondition(e) => ResolveExpr(e, ctx, false, true)(false) - case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false) - case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function") - } - ResolveExpr(e, ctx, false, false)(false) - if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")") - } - } + // now, resolve and typecheck all + // * Field types and Method formal-parameter types + // * Assign, FieldUpdate, and Call statements + // * VariableExpr and FieldSelect expressions + for (decl <- prog) decl match { + case ch: Channel => + val context = new ProgramContext(decls, ChannelClass(ch)) + var ctx = context + for (v <- ch.parameters) { + ctx = ctx.AddVariable(v) + } + ResolveExpr(ch.where, ctx, false, true)(false) errors = errors ++ context.errors - } + case cl: Class => + val context = new ProgramContext(decls, cl) + for (m <- cl.members) { + context.currentMember = m; + m match { + case MonitorInvariant(e) => + ResolveExpr(e, context, true, true)(true) + if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")") + case _:Field => // nothing more to do + case m@Method(id, ins, outs, spec, body) => + var ctx = context + for (v <- ins ++ outs) { + ctx = ctx.AddVariable(v) + } + spec foreach { + case Precondition(e) => ResolveExpr(e, ctx, false, true)(false) + case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false) + case lc@LockChange(ee) => + if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") + ee foreach (e => ResolveExpr(e, ctx, true, false)(false)) + } + ResolveStmt(BlockStmt(body), ctx) + case Condition(id, None) => + case c@Condition(id, Some(e)) => + ResolveExpr(e, context, false, true)(false) + if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")") + case p@Predicate(id, e) => + var ctx = context; + ResolveExpr(e, ctx, false, true)(true); + if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")") + case f@Function(id, ins, out, spec, e) => + var ctx = context + for (v <- ins) { + ctx = ctx.AddVariable(v) + } + // TODO: disallow credit(...) expressions in function specifications + spec foreach { + case Precondition(e) => ResolveExpr(e, ctx, false, true)(false) + case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false) + case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function") + } + ResolveExpr(e, ctx, false, false)(false) + if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")") + } + } + errors = errors ++ context.errors + } - if (errors.length == 0) { - Success() - } else { - Errors(errors) - } - } + if (errors.length == 0) { + Success() + } else { + Errors(errors) + } + } - def ResolveType(t: Type, context: ProgramContext): unit = { - for(p <- t.params){ - ResolveType(p, context); - } - if(t.isInstanceOf[TokenType]){ - val tt = t.asInstanceOf[TokenType]; - ResolveType(tt.C, context); - if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class."); - tt.C.typ.LookupMember(tt.m) match { - case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc; - case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + "."); - } - return; - } - if (context.Decls contains t.FullName) { - context.Decls(t.FullName) match { - case cl: Class => t.typ = cl - case ch: Channel => t.typ = ChannelClass(ch) - case _ => - context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class") - t.typ = IntClass - } - } else { - if(seqClasses.contains(t.FullName)) { - t.typ = seqClasses(t.FullName) - } else if(t.id.equals("seq") && t.params.length == 1) { - val seqt = new SeqClass(t.params(0).typ); - seqClasses = seqClasses + ((seqt.FullName, seqt)); - t.typ = seqt; - } else { - context.Error(t.pos, "undeclared type " + t.FullName) - t.typ = IntClass - } - } - } + def ResolveType(t: Type, context: ProgramContext): unit = { + for(p <- t.params){ + ResolveType(p, context); + } + if(t.isInstanceOf[TokenType]){ + val tt = t.asInstanceOf[TokenType]; + ResolveType(tt.C, context); + if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class."); + tt.C.typ.LookupMember(tt.m) match { + case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc; + case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + "."); + } + return; + } + if (context.Decls contains t.FullName) { + context.Decls(t.FullName) match { + case cl: Class => t.typ = cl + case ch: Channel => t.typ = ChannelClass(ch) + case _ => + context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class") + t.typ = IntClass + } + } else { + if(seqClasses.contains(t.FullName)) { + t.typ = seqClasses(t.FullName) + } else if(t.id.equals("seq") && t.params.length == 1) { + val seqt = new SeqClass(t.params(0).typ); + seqClasses = seqClasses + ((seqt.FullName, seqt)); + t.typ = seqt; + } else { + context.Error(t.pos, "undeclared type " + t.FullName) + t.typ = IntClass + } + } + } - def getSeqType(param: Class, context: ProgramContext): Class = { - if(seqClasses.contains("seq<" + param.FullName + ">")) { - seqClasses("seq<" + param.FullName + ">") - } else { - val seqt = new SeqClass(param); - seqClasses = seqClasses + ((seqt.FullName, seqt)); - seqt - } - } + def getSeqType(param: Class, context: ProgramContext): Class = { + if(seqClasses.contains("seq<" + param.FullName + ">")) { + seqClasses("seq<" + param.FullName + ">") + } else { + val seqt = new SeqClass(param); + seqClasses = seqClasses + ((seqt.FullName, seqt)); + seqt + } + } - def ResolveStmt(s: Statement, context: ProgramContext): unit = s match { - case Assert(e) => - ResolveExpr(e, context, true, true)(false) - if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")") - case Assume(e) => - ResolveExpr(e, context, false, false)(false) // assume expressions remain at run-time, so OLD is not allowed - if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")") - CheckNoGhost(e, context) - case BlockStmt(ss) => - var ctx = context - for (s <- ss) s match { - case l @ LocalVar(id, t, c, g, rhs) => - ResolveType(l.v.t, ctx) - val oldCtx = ctx - ctx = ctx.AddVariable(l.v) - rhs match { - case None => - case Some(rhs) => - val lhs = VariableExpr(id) - lhs.pos = l.pos; - ResolveExpr(lhs, ctx, false, false)(false) - ResolveAssign(lhs, rhs, oldCtx) - } - case c: CallAsync => - ResolveStmt(c, ctx) - if (c.local != null) { - ctx = ctx.AddVariable(c.local) - } - case c: Call => - ResolveStmt(c, ctx) - for (v <- c.locals) { ctx = ctx.AddVariable(v) } - case r: Receive => - ResolveStmt(r, ctx) - for (v <- r.locals) { ctx = ctx.AddVariable(v) } - case s => - ResolveStmt(s, ctx) - } - case IfStmt(guard, thn, els) => - ResolveExpr(guard, context, false, false)(false) - if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")") - CheckNoGhost(guard, context) - ResolveStmt(thn, context) - els match { case None => case Some(s) => ResolveStmt(s, context) } - case w@ WhileStmt(guard, invs, lkch, body) => - ResolveExpr(guard, context, false, false)(false) - if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")") - CheckNoGhost(guard, context) - for (inv <- invs) { - ResolveExpr(inv, context, true, true)(false) - if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")") - } - for (l <- lkch) { - ResolveExpr(l, context, true, false)(false) - if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")") - } - ResolveStmt(body, context) - w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent - case Assign(lhs, rhs) => - ResolveExpr(lhs, context, false, false)(false) - ResolveAssign(lhs, rhs, context) - if (lhs.v != null && lhs.v.IsImmutable) { - if (lhs.v.IsGhost) - CheckNoGhost(rhs, context) - else - context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id) - } - case fu@FieldUpdate(lhs, rhs) => - ResolveExpr(lhs, context, false, false)(false) - if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context) - if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id) - ResolveExpr(rhs, context, false, false)(false) - if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName) - if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context) - case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above") - case c @ Call(declaresLocal, lhs, obj, id, args) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } - // lookup method - var typ: Class = IntClass - obj.typ.LookupMember(id) match { - case None => - context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) - case Some(m: Method) => - c.m = m - if (args.length != m.ins.length) - context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + - " (" + args.length + " instead of " + m.ins.length + ")") - else { - for((actual, formal) <- args zip m.ins){ - if(! canAssign(formal.t.typ, actual.typ)) - context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") - } - } - if (lhs.length != m.outs.length) - context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id + - " (" + lhs.length + " instead of " + m.outs.length + ")") - else - c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context) - case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) - } - case Install(obj, lowerBounds, upperBounds) => - ResolveExpr(obj, context, false, false)(false) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in reorder statement must be of a reference type (found " + obj.typ.FullName + ")") - if (obj.typ.IsChannel) context.Error(obj.pos, "object in reorder statement must not be a channel (found " + obj.typ.FullName + ")") - ResolveBounds(lowerBounds, upperBounds, context, "install") - case Share(obj, lowerBounds, upperBounds) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")") - if (obj.typ.IsChannel) context.Error(obj.pos, "object in share statement must not be a channel (found " + obj.typ.FullName + ")") - ResolveBounds(lowerBounds, upperBounds, context, "share") - case Unshare(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")") - if (obj.typ.IsChannel) context.Error(obj.pos, "object in unshare statement must not be a channel (found " + obj.typ.FullName + ")") - case Acquire(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")") - case Release(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")") - case RdAcquire(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")") - case RdRelease(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")") - case Lock(obj, b, rdLock) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) { - val sname = if (rdLock) "rd lock" else "lock"; - context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")") - - } - ResolveStmt(b, context) - case Downgrade(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")") - case Free(obj) => - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")") - case fld@Fold(e) => - ResolveExpr(e, context, false, true)(false); - CheckNoGhost(e, context); - if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.") - case ufld@Unfold(e) => - ResolveExpr(e, context, false, true)(false); - CheckNoGhost(e, context); - if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.") - case c@CallAsync(declaresLocal, token, obj, id, args) => - // resolve receiver - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - // resolve arguments - args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } - // lookup method - var typ: Class = IntClass - obj.typ.LookupMember(id) match { - case None => - context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) - case Some(m: Method) => - c.m = m - if (args.length != m.ins.length) - context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + - " (" + args.length + " instead of " + m.ins.length + ")") - else { - for((actual, formal) <- args zip m.ins){ - if(! canAssign(formal.t.typ, actual.typ)) - context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") - } - } - case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) - } - // resolve the token - if (declaresLocal) { - c.local = new Variable(token.id, TokenType(new Type(obj.typ), id)) - ResolveType(c.local.t, context) - token.Resolve(c.local) - } else if (token != null) { - ResolveExpr(token, context, false, false)(false) - if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id))) - context.Error(token.pos, "wrong token type") - } - case jn@JoinAsync(lhs, token) => - // resolve the assignees - var vars = Set[Variable]() - for (v <- lhs) { - ResolveExpr(v, context, false, false)(false) - if (v.v != null) { - if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter") - if (vars contains v.v) { - context.Error(v.pos, "duplicate actual out-parameter: " + v.id) - } else { - vars = vars + v.v - } - } - } - // resolve the token - ResolveExpr(token, context, false, false)(false); - if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null) - context.Error(token.pos, "the first argument of a join async must be a token") - else { - val m = token.typ.asInstanceOf[TokenClass].method; - jn.m = m - if (lhs.length != m.outs.length) - context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName + + def ResolveStmt(s: Statement, context: ProgramContext): unit = s match { + case Assert(e) => + ResolveExpr(e, context, true, true)(false) + if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")") + case Assume(e) => + ResolveExpr(e, context, false, false)(false) // assume expressions remain at run-time, so OLD is not allowed + if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")") + CheckNoGhost(e, context) + case BlockStmt(ss) => + var ctx = context + for (s <- ss) s match { + case l @ LocalVar(id, t, c, g, rhs) => + ResolveType(l.v.t, ctx) + val oldCtx = ctx + ctx = ctx.AddVariable(l.v) + rhs match { + case None => + case Some(rhs) => + val lhs = VariableExpr(id) + lhs.pos = l.pos; + ResolveExpr(lhs, ctx, false, false)(false) + ResolveAssign(lhs, rhs, oldCtx) + } + case c: CallAsync => + ResolveStmt(c, ctx) + if (c.local != null) { + ctx = ctx.AddVariable(c.local) + } + case c: Call => + ResolveStmt(c, ctx) + for (v <- c.locals) { ctx = ctx.AddVariable(v) } + case r: Receive => + ResolveStmt(r, ctx) + for (v <- r.locals) { ctx = ctx.AddVariable(v) } + case s => + ResolveStmt(s, ctx) + } + case IfStmt(guard, thn, els) => + ResolveExpr(guard, context, false, false)(false) + if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")") + CheckNoGhost(guard, context) + ResolveStmt(thn, context) + els match { case None => case Some(s) => ResolveStmt(s, context) } + case w@ WhileStmt(guard, invs, lkch, body) => + ResolveExpr(guard, context, false, false)(false) + if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")") + CheckNoGhost(guard, context) + for (inv <- invs) { + ResolveExpr(inv, context, true, true)(false) + if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")") + } + for (l <- lkch) { + ResolveExpr(l, context, true, false)(false) + if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")") + } + ResolveStmt(body, context) + w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent + case Assign(lhs, rhs) => + ResolveExpr(lhs, context, false, false)(false) + ResolveAssign(lhs, rhs, context) + if (lhs.v != null && lhs.v.IsImmutable) { + if (lhs.v.IsGhost) + CheckNoGhost(rhs, context) + else + context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id) + } + case fu@FieldUpdate(lhs, rhs) => + ResolveExpr(lhs, context, false, false)(false) + if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context) + if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id) + ResolveExpr(rhs, context, false, false)(false) + if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName) + if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context) + case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above") + case c @ Call(declaresLocal, lhs, obj, id, args) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } + // lookup method + var typ: Class = IntClass + obj.typ.LookupMember(id) match { + case None => + context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) + case Some(m: Method) => + c.m = m + if (args.length != m.ins.length) + context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + + " (" + args.length + " instead of " + m.ins.length + ")") + else { + for((actual, formal) <- args zip m.ins){ + if(! canAssign(formal.t.typ, actual.typ)) + context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + } + } + if (lhs.length != m.outs.length) + context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id + " (" + lhs.length + " instead of " + m.outs.length + ")") - else { - for((out, l) <- m.outs zip lhs){ - if(! canAssign(l.typ, out.t.typ)) - context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")") - } - } - - } - case w@Wait(obj, id) => - // resolve receiver - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - // lookup condition - obj.typ.LookupMember(id) match { - case None => - context.Error(w.pos, "wait on undeclared member " + id + " in class " + obj.typ.FullName) - case Some(c: Condition) => w.c = c - case _ => - context.Error(w.pos, "wait expression does not denote a condition: " + obj.typ.FullName + "." + id) - } - case s@Signal(obj, id, all) => - // resolve receiver - ResolveExpr(obj, context, false, false)(false) - CheckNoGhost(obj, context) - // lookup condition - obj.typ.LookupMember(id) match { - case None => - context.Error(s.pos, "signal on undeclared member " + id + " in class " + obj.typ.FullName) - case Some(c: Condition) => s.c = c - case _ => - context.Error(s.pos, "signal expression does not denote a condition: " + obj.typ.FullName + "." + id) - } - case s@Send(ch, args) => - ResolveExpr(ch, context, false, false)(false) - CheckNoGhost(ch, context) - args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } - // match types of arguments - ch.typ match { - case ChannelClass(channel) => - if (args.length != channel.parameters.length) - context.Error(s.pos, "wrong number of actual in-parameters in send for channel type " + ch.typ.FullName + - " (" + args.length + " instead of " + channel.parameters.length + ")") - else { - for ((actual, formal) <- args zip channel.parameters) { - if (! canAssign(formal.t.typ, actual.typ)) - context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") - } - } - case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel") - } - case r@Receive(declaresLocal, ch, outs) => - ResolveExpr(ch, context, false, false)(false) - CheckNoGhost(ch, context) - // match types of arguments - ch.typ match { - case ChannelClass(channel) => - if (outs.length != channel.parameters.length) - context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName + - " (" + outs.length + " instead of " + channel.parameters.length + ")") - else - r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context) - case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel") - } - } + else + c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context) + case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) + } + case Install(obj, lowerBounds, upperBounds) => + ResolveExpr(obj, context, false, false)(false) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in reorder statement must be of a reference type (found " + obj.typ.FullName + ")") + if (obj.typ.IsChannel) context.Error(obj.pos, "object in reorder statement must not be a channel (found " + obj.typ.FullName + ")") + ResolveBounds(lowerBounds, upperBounds, context, "install") + case Share(obj, lowerBounds, upperBounds) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")") + if (obj.typ.IsChannel) context.Error(obj.pos, "object in share statement must not be a channel (found " + obj.typ.FullName + ")") + ResolveBounds(lowerBounds, upperBounds, context, "share") + case Unshare(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")") + if (obj.typ.IsChannel) context.Error(obj.pos, "object in unshare statement must not be a channel (found " + obj.typ.FullName + ")") + case Acquire(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")") + case Release(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")") + case RdAcquire(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")") + case RdRelease(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")") + case Lock(obj, b, rdLock) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) { + val sname = if (rdLock) "rd lock" else "lock"; + context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")") + + } + ResolveStmt(b, context) + case Downgrade(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")") + case Free(obj) => + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")") + case fld@Fold(e) => + ResolveExpr(e, context, false, true)(false); + CheckNoGhost(e, context); + if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.") + case ufld@Unfold(e) => + ResolveExpr(e, context, false, true)(false); + CheckNoGhost(e, context); + if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.") + case c@CallAsync(declaresLocal, token, obj, id, args) => + // resolve receiver + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + // resolve arguments + args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } + // lookup method + var typ: Class = IntClass + obj.typ.LookupMember(id) match { + case None => + context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) + case Some(m: Method) => + c.m = m + if (args.length != m.ins.length) + context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + + " (" + args.length + " instead of " + m.ins.length + ")") + else { + for((actual, formal) <- args zip m.ins){ + if(! canAssign(formal.t.typ, actual.typ)) + context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + } + } + case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) + } + // resolve the token + if (declaresLocal) { + c.local = new Variable(token.id, TokenType(new Type(obj.typ), id)) + ResolveType(c.local.t, context) + token.Resolve(c.local) + } else if (token != null) { + ResolveExpr(token, context, false, false)(false) + if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id))) + context.Error(token.pos, "wrong token type") + } + case jn@JoinAsync(lhs, token) => + // resolve the assignees + var vars = Set[Variable]() + for (v <- lhs) { + ResolveExpr(v, context, false, false)(false) + if (v.v != null) { + if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter") + if (vars contains v.v) { + context.Error(v.pos, "duplicate actual out-parameter: " + v.id) + } else { + vars = vars + v.v + } + } + } + // resolve the token + ResolveExpr(token, context, false, false)(false); + if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null) + context.Error(token.pos, "the first argument of a join async must be a token") + else { + val m = token.typ.asInstanceOf[TokenClass].method; + jn.m = m + if (lhs.length != m.outs.length) + context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName + + " (" + lhs.length + " instead of " + m.outs.length + ")") + else { + for((out, l) <- m.outs zip lhs){ + if(! canAssign(l.typ, out.t.typ)) + context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")") + } + } + + } + case w@Wait(obj, id) => + // resolve receiver + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + // lookup condition + obj.typ.LookupMember(id) match { + case None => + context.Error(w.pos, "wait on undeclared member " + id + " in class " + obj.typ.FullName) + case Some(c: Condition) => w.c = c + case _ => + context.Error(w.pos, "wait expression does not denote a condition: " + obj.typ.FullName + "." + id) + } + case s@Signal(obj, id, all) => + // resolve receiver + ResolveExpr(obj, context, false, false)(false) + CheckNoGhost(obj, context) + // lookup condition + obj.typ.LookupMember(id) match { + case None => + context.Error(s.pos, "signal on undeclared member " + id + " in class " + obj.typ.FullName) + case Some(c: Condition) => s.c = c + case _ => + context.Error(s.pos, "signal expression does not denote a condition: " + obj.typ.FullName + "." + id) + } + case s@Send(ch, args) => + ResolveExpr(ch, context, false, false)(false) + CheckNoGhost(ch, context) + args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) } + // match types of arguments + ch.typ match { + case ChannelClass(channel) => + if (args.length != channel.parameters.length) + context.Error(s.pos, "wrong number of actual in-parameters in send for channel type " + ch.typ.FullName + + " (" + args.length + " instead of " + channel.parameters.length + ")") + else { + for ((actual, formal) <- args zip channel.parameters) { + if (! canAssign(formal.t.typ, actual.typ)) + context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + } + } + case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel") + } + case r@Receive(declaresLocal, ch, outs) => + ResolveExpr(ch, context, false, false)(false) + CheckNoGhost(ch, context) + // match types of arguments + ch.typ match { + case ChannelClass(channel) => + if (outs.length != channel.parameters.length) + context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName + + " (" + outs.length + " instead of " + channel.parameters.length + ")") + else + r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context) + case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel") + } + } - def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = { - var locals = List[Variable]() - var vars = Set[Variable]() - var ctx = context - for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) { - if (declareLocal) { - val local = new Variable(actual.id, new Type(formal.t.typ)) - locals = locals + local - ResolveType(local.t, ctx) - actual.Resolve(local) - vars = vars + actual.v - ctx = ctx.AddVariable(local) - } else { - ResolveExpr(actual, ctx, false, false)(false) - CheckNoGhost(actual, ctx) - if (actual.v != null) { - if (! canAssign(actual.typ, formal.t.typ)) - ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " + - formal.t.FullName + ", found: " + actual.typ.FullName + ")") - if (vars contains actual.v) - ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id) - else if (actual.v.IsImmutable) - ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter") - vars = vars + actual.v - } - } - } - locals - } + def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = { + var locals = List[Variable]() + var vars = Set[Variable]() + var ctx = context + for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) { + if (declareLocal) { + val local = new Variable(actual.id, new Type(formal.t.typ)) + locals = locals + local + ResolveType(local.t, ctx) + actual.Resolve(local) + vars = vars + actual.v + ctx = ctx.AddVariable(local) + } else { + ResolveExpr(actual, ctx, false, false)(false) + CheckNoGhost(actual, ctx) + if (actual.v != null) { + if (! canAssign(actual.typ, formal.t.typ)) + ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " + + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + if (vars contains actual.v) + ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id) + else if (actual.v.IsImmutable) + ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter") + vars = vars + actual.v + } + } + } + locals + } - def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) = - for (b <- lowerBounds ++ upperBounds) { - ResolveExpr(b, context, true, false)(false) - if (!b.typ.IsRef && !b.typ.IsMu) - context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")") - } + def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) = + for (b <- lowerBounds ++ upperBounds) { + ResolveExpr(b, context, true, false)(false) + if (!b.typ.IsRef && !b.typ.IsMu) + context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")") + } - def ComputeLoopTargets(s: Statement): Set[Variable] = s match { // local variables - case BlockStmt(ss) => - (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) } - case IfStmt(guard, thn, els) => - val vars = ComputeLoopTargets(thn) - els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) } - case w: WhileStmt => - // assume w.LoopTargets is non-null and that it was computed with a larger context - w.LoopTargets - case Assign(lhs, rhs) => - if (lhs.v != null) Set(lhs.v) else Set() // don't assume resolution was successful - case lv: LocalVar => - lv.rhs match { case None => Set() case Some(_) => Set(lv.v) } - case Call(_, lhs, obj, id, args) => - (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars } - case _ => Set() - } + def ComputeLoopTargets(s: Statement): Set[Variable] = s match { // local variables + case BlockStmt(ss) => + (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) } + case IfStmt(guard, thn, els) => + val vars = ComputeLoopTargets(thn) + els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) } + case w: WhileStmt => + // assume w.LoopTargets is non-null and that it was computed with a larger context + w.LoopTargets + case Assign(lhs, rhs) => + if (lhs.v != null) Set(lhs.v) else Set() // don't assume resolution was successful + case lv: LocalVar => + lv.rhs match { case None => Set() case Some(_) => Set(lv.v) } + case Call(_, lhs, obj, id, args) => + (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars } + case _ => Set() + } - def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = { - rhs match { - case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs - case _ => ResolveExpr(rhs, context, false, false)(false) - } - if (! canAssign(lhs.typ, rhs.typ)) - context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName) - if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context) - } + def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = { + rhs match { + case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs + case _ => ResolveExpr(rhs, context, false, false)(false) + } + if (! canAssign(lhs.typ, rhs.typ)) + context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName) + if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context) + } - // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field - def ResolveExpr(e: RValue, context: ProgramContext, - twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match { - case e @ NewRhs(id, initialization, lower, upper) => - if (context.Decls contains id) { - context.Decls(id) match { - case ch: Channel => - e.typ = ChannelClass(ch) - case cl: Class => - e.typ = cl - if (lower != Nil || upper != Nil) - context.Error(e.pos, "A new object of a class type is not allowed to have a wait-order bounds clause (use the share statement instead)") - } - // initialize the fields - var fieldNames = Set[String]() - for(ini@Init(f, init) <- initialization) { - if (fieldNames contains f) { - context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.") - } else { - fieldNames = fieldNames + f - e.typ.LookupMember(f) match { - case Some(field@Field(name, tp)) => - if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + "."); - ResolveExpr(init, context, false, false); - if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + "."); - ini.f = field; - case _ => - context.Error(e.pos, "The type " + id + " does not declare a field " + f + "."); - } - } - } - // resolve the bounds - ResolveBounds(lower, upper, context, "new") - } else { - context.Error(e.pos, "undefined class or channel " + id + " used in new expression") - e.typ = IntClass - } - case i:IntLiteral => - i.typ = IntClass - case b:BoolLiteral => - b.typ = BoolClass - case n:NullLiteral => - n.typ = NullClass - case mx:MaxLockLiteral => - mx.typ = MuClass - case mx:LockBottomLiteral => - mx.typ = MuClass - case r:Result => - assert(context.CurrentMember!=null); - r.typ = IntClass - if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){ - context.Error(r.pos, "The variable result can only be used in the postcondition of a function."); - } else { - r.typ = context.CurrentMember.asInstanceOf[Function].out.typ; - } - case ve @ VariableExpr(id) => - context.LookupVariable(id) match { - case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass - case Some(v) => ve.Resolve(v) } - case v:ThisExpr => v.typ = context.CurrentClass - case sel @ MemberAccess(e, id) => - ResolveExpr(e, context, twoStateContext, false) - var typ: Class = IntClass - e.typ.LookupMember(id) match { - case None => - context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName) - case Some(f: Field) => sel.f = f; typ = f.typ.typ - case Some(pred@Predicate(id, body)) => - if(! specContext) - context.Error(sel.pos, "predicate can only be used in positive predicate contexts") - sel.predicate = pred; - sel.isPredicate = true; - typ = BoolClass - case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id); - } - sel.typ = typ - case expr@ Access(e, perm) => - if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts") - ResolveExpr(e, context, twoStateContext, true) - perm match { - case None => - case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) } - expr.typ = BoolClass - case expr@ RdAccess(e,perm) => - if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts") - ResolveExpr(e, context, twoStateContext, true) - perm match { - case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false) - case _ => } - expr.typ = BoolClass - case expr@AccessAll(obj, perm) => - if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts") - ResolveExpr(obj, context, twoStateContext, false) - if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.") - perm match { - case None => - case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) } - expr.typ = BoolClass - case expr@RdAccessAll(obj,perm) => - if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts") - ResolveExpr(obj, context, twoStateContext, false) - if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.") - perm match { - case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false) - case _ => } - expr.typ = BoolClass - case expr@ Credit(e,n) => - if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts") - ResolveExpr(e, context, twoStateContext, false) - if(!e.typ.IsChannel) context.Error(expr.pos, "credit argument must denote a channel.") - ResolveExpr(expr.N, context, twoStateContext, false) - expr.typ = BoolClass - case expr@ Holds(e) => - if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates") - if(! specContext) - context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); - //todo: check that we are not in an invariant - ResolveExpr(e, context, twoStateContext, false) - expr.typ = BoolClass - case expr@ RdHolds(e) => - if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates") - ResolveExpr(e, context, twoStateContext, false) - expr.typ = BoolClass - case expr@ Assigned(id) => - context.LookupVariable(id) match { - case None => context.Error(expr.pos, "undefined local variable " + id) - case Some(v) => - expr.v = v - if (!(v.IsImmutable && v.IsGhost)) - context.Error(expr.pos, "assigned can only be used with ghost consts") - } - expr.typ = BoolClass - case expr@ Old(e) => - if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") } - ResolveExpr(e, context, twoStateContext, false) - expr.typ = e.typ - case ite@IfThenElse(con, then, els) => - ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext); - if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean"); - if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types"); - ite.typ = then.typ; - case expr@ Not(e) => - ResolveExpr(e, context, twoStateContext, false) - if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand") - expr.typ = BoolClass - case appl@FunctionApplication(obj, id, args) => - ResolveExpr(obj, context, twoStateContext, false); - args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)}; - // lookup function - appl.typ = IntClass - obj.typ.LookupMember(id) match { - case None => - context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName) - case Some(func@Function(f, ins, out, specs, body)) => - appl.f = func - appl.typ = func.out.typ; - if (args.length != ins.length) - context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id + - " (" + args.length + " instead of " + ins.length + ")") - else { - for((actual, formal) <- args zip func.ins){ - if(! canAssign(formal.t.typ, actual.typ)) - context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") - } - } - case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function") - } - case uf@Unfolding(pred, e) => - ResolveExpr(pred, context, twoStateContext, true); - ResolveExpr(e, context, twoStateContext, false); - if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.") - uf.typ = e.typ; - case bin: EqualityCompareExpr => - ResolveExpr(bin.E0, context, twoStateContext, false) - ResolveExpr(bin.E1, context, twoStateContext, false) - if (bin.E0.typ == bin.E1.typ) { /* all is well */ } - else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ } - else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ } - else - context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName) - bin.typ = BoolClass - case bin: LockBelow => - ResolveExpr(bin.E0, context, twoStateContext, false) - ResolveExpr(bin.E1, context, twoStateContext, false) - if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu)) - context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")") - if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu)) - context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")") - bin.typ = BoolClass - case app@Append(e0, e1) => - ResolveExpr(e0, context, twoStateContext, false); - ResolveExpr(e1, context, twoStateContext, false); - if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ")."); - if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ")."); - if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type."); - app.typ = e0.typ; - case at@At(e0, e1) => - ResolveExpr(e0, context, twoStateContext, false); - ResolveExpr(e1, context, twoStateContext, false); - if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ")."); - if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ")."); - if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass; - case drop@Drop(e0, e1) => - ResolveExpr(e0, context, twoStateContext, false); - ResolveExpr(e1, context, twoStateContext, false); - if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ")."); - if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ")."); - drop.typ = e0.typ; - case take@Take(e0, e1) => - ResolveExpr(e0, context, twoStateContext, false); - ResolveExpr(e1, context, twoStateContext, false); - if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ")."); - if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ")."); - take.typ = e0.typ; - case bin: BinaryExpr => - ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And]) - ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies])) - if (bin.E0.typ != bin.ExpectedLhsType) - context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" + - " (expected " + bin.ExpectedLhsType.FullName + - ", found " + bin.E0.typ.FullName + ")") - if (bin.E1.typ != bin.ExpectedRhsType) - context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" + - " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")") - bin.typ = bin.ResultType - case q: Quantification => - q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") } - ResolveExpr(q.Seq, context, twoStateContext, false); - if(! q.Seq.typ.IsSeq) - context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ")."); - else { - val elementType = q.Seq.typ.parameters(0); - var bodyContext = context; - var bvariables = Nil: List[Variable]; - q.Is foreach { i => - val variable = new Variable(i, new Type(elementType)); - bodyContext = bodyContext.AddVariable(variable); - bvariables = bvariables + variable; - } - ResolveExpr(q.E, bodyContext, twoStateContext, true); - if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " + q.E.typ.FullName + ")."); - q.variables = bvariables; - } - q.typ = BoolClass - case seq@EmptySeq(t) => - ResolveType(t, context) - seq.typ = getSeqType(t.typ, context); - case seq@ExplicitSeq(es) => - es foreach { e => ResolveExpr(e, context, twoStateContext, false) } - es match { - case Nil => seq.typ = getSeqType(IntClass, context); - case h :: t => - t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")}; - seq.typ = getSeqType(h.typ, context); - } - case ran@Range(min, max) => - ResolveExpr(min, context, twoStateContext, false); - if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ")."); - ResolveExpr(max, context, twoStateContext, false); - if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ")."); - ran.typ = getSeqType(IntClass, context); - case len@Length(e) => - ResolveExpr(e, context, twoStateContext, false); - if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ")."); - len.typ = IntClass; - case ev@Eval(h, e) => - if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates") - h match { - case AcquireState(obj) => - ResolveExpr(obj, context, twoStateContext, false) - if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference."); - case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false) - if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference."); - case c@CallState(token, obj, id, args) => - ResolveExpr(token, context, twoStateContext, false); - if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens"); - ResolveExpr(obj, context, false, false) - CheckNoGhost(obj, context) - args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) } - // lookup method - var typ: Class = IntClass - obj.typ.LookupMember(id) match { - case None => - context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) - case Some(m: Method) => - c.m = m - if (args.length != m.ins.length) - context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + - " (" + args.length + " instead of " + m.ins.length + ")") - else { - for((actual, formal) <- args zip m.ins){ - if(! canAssign(formal.t.typ, actual.typ)) - context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") - } - } - case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) - } - - - } - ResolveExpr(e, context, false, specContext) - ev.typ = e.typ; - } + // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field + def ResolveExpr(e: RValue, context: ProgramContext, + twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match { + case e @ NewRhs(id, initialization, lower, upper) => + if (context.Decls contains id) { + context.Decls(id) match { + case ch: Channel => + e.typ = ChannelClass(ch) + case cl: Class => + e.typ = cl + if (lower != Nil || upper != Nil) + context.Error(e.pos, "A new object of a class type is not allowed to have a wait-order bounds clause (use the share statement instead)") + } + // initialize the fields + var fieldNames = Set[String]() + for(ini@Init(f, init) <- initialization) { + if (fieldNames contains f) { + context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.") + } else { + fieldNames = fieldNames + f + e.typ.LookupMember(f) match { + case Some(field@Field(name, tp)) => + if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + "."); + ResolveExpr(init, context, false, false); + if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + "."); + ini.f = field; + case _ => + context.Error(e.pos, "The type " + id + " does not declare a field " + f + "."); + } + } + } + // resolve the bounds + ResolveBounds(lower, upper, context, "new") + } else { + context.Error(e.pos, "undefined class or channel " + id + " used in new expression") + e.typ = IntClass + } + case i:IntLiteral => + i.typ = IntClass + case b:BoolLiteral => + b.typ = BoolClass + case n:NullLiteral => + n.typ = NullClass + case mx:MaxLockLiteral => + mx.typ = MuClass + case mx:LockBottomLiteral => + mx.typ = MuClass + case r:Result => + assert(context.CurrentMember!=null); + r.typ = IntClass + if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){ + context.Error(r.pos, "The variable result can only be used in the postcondition of a function."); + } else { + r.typ = context.CurrentMember.asInstanceOf[Function].out.typ; + } + case ve @ VariableExpr(id) => + context.LookupVariable(id) match { + case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass + case Some(v) => ve.Resolve(v) } + case v:ThisExpr => v.typ = context.CurrentClass + case sel @ MemberAccess(e, id) => + ResolveExpr(e, context, twoStateContext, false) + var typ: Class = IntClass + e.typ.LookupMember(id) match { + case None => + context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName) + case Some(f: Field) => sel.f = f; typ = f.typ.typ + case Some(pred@Predicate(id, body)) => + if(! specContext) + context.Error(sel.pos, "predicate can only be used in positive predicate contexts") + sel.predicate = pred; + sel.isPredicate = true; + typ = BoolClass + case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id); + } + sel.typ = typ + case expr@ Access(e, perm) => + if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts") + ResolveExpr(e, context, twoStateContext, true) + perm match { + case None => + case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) } + expr.typ = BoolClass + case expr@ RdAccess(e,perm) => + if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts") + ResolveExpr(e, context, twoStateContext, true) + perm match { + case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false) + case _ => } + expr.typ = BoolClass + case expr@AccessAll(obj, perm) => + if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts") + ResolveExpr(obj, context, twoStateContext, false) + if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.") + perm match { + case None => + case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) } + expr.typ = BoolClass + case expr@RdAccessAll(obj,perm) => + if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts") + ResolveExpr(obj, context, twoStateContext, false) + if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.") + perm match { + case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false) + case _ => } + expr.typ = BoolClass + case expr@ Credit(e,n) => + if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts") + ResolveExpr(e, context, twoStateContext, false) + if(!e.typ.IsChannel) context.Error(expr.pos, "credit argument must denote a channel.") + ResolveExpr(expr.N, context, twoStateContext, false) + expr.typ = BoolClass + case expr@ Holds(e) => + if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates") + if(! specContext) + context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); + //todo: check that we are not in an invariant + ResolveExpr(e, context, twoStateContext, false) + expr.typ = BoolClass + case expr@ RdHolds(e) => + if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates") + ResolveExpr(e, context, twoStateContext, false) + expr.typ = BoolClass + case expr@ Assigned(id) => + context.LookupVariable(id) match { + case None => context.Error(expr.pos, "undefined local variable " + id) + case Some(v) => + expr.v = v + if (!(v.IsImmutable && v.IsGhost)) + context.Error(expr.pos, "assigned can only be used with ghost consts") + } + expr.typ = BoolClass + case expr@ Old(e) => + if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") } + ResolveExpr(e, context, twoStateContext, false) + expr.typ = e.typ + case ite@IfThenElse(con, then, els) => + ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext); + if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean"); + if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types"); + ite.typ = then.typ; + case expr@ Not(e) => + ResolveExpr(e, context, twoStateContext, false) + if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand") + expr.typ = BoolClass + case appl@FunctionApplication(obj, id, args) => + ResolveExpr(obj, context, twoStateContext, false); + args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)}; + // lookup function + appl.typ = IntClass + obj.typ.LookupMember(id) match { + case None => + context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName) + case Some(func@Function(f, ins, out, specs, body)) => + appl.f = func + appl.typ = func.out.typ; + if (args.length != ins.length) + context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id + + " (" + args.length + " instead of " + ins.length + ")") + else { + for((actual, formal) <- args zip func.ins){ + if(! canAssign(formal.t.typ, actual.typ)) + context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + } + } + case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function") + } + case uf@Unfolding(pred, e) => + ResolveExpr(pred, context, twoStateContext, true); + ResolveExpr(e, context, twoStateContext, false); + if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.") + uf.typ = e.typ; + case bin: EqualityCompareExpr => + ResolveExpr(bin.E0, context, twoStateContext, false) + ResolveExpr(bin.E1, context, twoStateContext, false) + if (bin.E0.typ == bin.E1.typ) { /* all is well */ } + else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ } + else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ } + else + context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName) + bin.typ = BoolClass + case bin: LockBelow => + ResolveExpr(bin.E0, context, twoStateContext, false) + ResolveExpr(bin.E1, context, twoStateContext, false) + if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu)) + context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")") + if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu)) + context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")") + bin.typ = BoolClass + case app@Append(e0, e1) => + ResolveExpr(e0, context, twoStateContext, false); + ResolveExpr(e1, context, twoStateContext, false); + if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ")."); + if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ")."); + if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type."); + app.typ = e0.typ; + case at@At(e0, e1) => + ResolveExpr(e0, context, twoStateContext, false); + ResolveExpr(e1, context, twoStateContext, false); + if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ")."); + if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ")."); + if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass; + case drop@Drop(e0, e1) => + ResolveExpr(e0, context, twoStateContext, false); + ResolveExpr(e1, context, twoStateContext, false); + if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ")."); + if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ")."); + drop.typ = e0.typ; + case take@Take(e0, e1) => + ResolveExpr(e0, context, twoStateContext, false); + ResolveExpr(e1, context, twoStateContext, false); + if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ")."); + if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ")."); + take.typ = e0.typ; + case bin: BinaryExpr => + ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And]) + ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies])) + if (bin.E0.typ != bin.ExpectedLhsType) + context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" + + " (expected " + bin.ExpectedLhsType.FullName + + ", found " + bin.E0.typ.FullName + ")") + if (bin.E1.typ != bin.ExpectedRhsType) + context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" + + " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")") + bin.typ = bin.ResultType + case q: Quantification => + q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") } + ResolveExpr(q.Seq, context, twoStateContext, false); + if(! q.Seq.typ.IsSeq) + context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ")."); + else { + val elementType = q.Seq.typ.parameters(0); + var bodyContext = context; + var bvariables = Nil: List[Variable]; + q.Is foreach { i => + val variable = new Variable(i, new Type(elementType)); + bodyContext = bodyContext.AddVariable(variable); + bvariables = bvariables + variable; + } + ResolveExpr(q.E, bodyContext, twoStateContext, true); + if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " + q.E.typ.FullName + ")."); + q.variables = bvariables; + } + q.typ = BoolClass + case seq@EmptySeq(t) => + ResolveType(t, context) + seq.typ = getSeqType(t.typ, context); + case seq@ExplicitSeq(es) => + es foreach { e => ResolveExpr(e, context, twoStateContext, false) } + es match { + case Nil => seq.typ = getSeqType(IntClass, context); + case h :: t => + t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")}; + seq.typ = getSeqType(h.typ, context); + } + case ran@Range(min, max) => + ResolveExpr(min, context, twoStateContext, false); + if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ")."); + ResolveExpr(max, context, twoStateContext, false); + if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ")."); + ran.typ = getSeqType(IntClass, context); + case len@Length(e) => + ResolveExpr(e, context, twoStateContext, false); + if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ")."); + len.typ = IntClass; + case ev@Eval(h, e) => + if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates") + h match { + case AcquireState(obj) => + ResolveExpr(obj, context, twoStateContext, false) + if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference."); + case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false) + if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference."); + case c@CallState(token, obj, id, args) => + ResolveExpr(token, context, twoStateContext, false); + if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens"); + ResolveExpr(obj, context, false, false) + CheckNoGhost(obj, context) + args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) } + // lookup method + var typ: Class = IntClass + obj.typ.LookupMember(id) match { + case None => + context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName) + case Some(m: Method) => + c.m = m + if (args.length != m.ins.length) + context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id + + " (" + args.length + " instead of " + m.ins.length + ")") + else { + for((actual, formal) <- args zip m.ins){ + if(! canAssign(formal.t.typ, actual.typ)) + context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")") + } + } + case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id) + } + + + } + ResolveExpr(e, context, false, specContext) + ev.typ = e.typ; + } - def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = { - cl.LookupMember("run") match { - case None => - context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" + - " (found type " + cl.id + ")") - None - case Some(m: Method) => - m.spec foreach { - case Precondition(e) => CheckRunSpecification(e, context, true) - case Postcondition(e) => CheckRunSpecification(e, context, false) - case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method") - } - if(0 - context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" + - " (found non-method member)") - None - } - } + def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = { + cl.LookupMember("run") match { + case None => + context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" + + " (found type " + cl.id + ")") + None + case Some(m: Method) => + m.spec foreach { + case Precondition(e) => CheckRunSpecification(e, context, true) + case Postcondition(e) => CheckRunSpecification(e, context, false) + case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method") + } + if(0 + context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" + + " (found non-method member)") + None + } + } - // assumes that lhs and rhs are resolved - def canAssign(lhs: Class, rhs: Class): Boolean = { - (lhs, rhs) match { - case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2) - case (TokenClass(c1, m1), _) => false - case (_, TokenClass(c2, m2)) => false - case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull) - } - } + // assumes that lhs and rhs are resolved + def canAssign(lhs: Class, rhs: Class): Boolean = { + (lhs, rhs) match { + case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2) + case (TokenClass(c1, m1), _) => false + case (_, TokenClass(c2, m2)) => false + case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull) + } + } - def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = { - def specOk(e: RValue): Unit = { - e match { - case ve: VariableExpr => - if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here") - case fs@ MemberAccess(e, id) => - if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here") - CheckNoGhost(e, context) - case a: Assigned => - if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here") - case _ => visitE(e, specOk) - } - } - specOk(expr) - } + def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = { + def specOk(e: RValue): Unit = { + e match { + case ve: VariableExpr => + if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here") + case fs@ MemberAccess(e, id) => + if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here") + CheckNoGhost(e, context) + case a: Assigned => + if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here") + case _ => visitE(e, specOk) + } + } + specOk(expr) + } - def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = { - def specOk(e: RValue): Unit = { - e match { - case ve: VariableExpr => - if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here") - case a: Assigned => - if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here") - case _ => visitE(e, specOk) - } - } - specOk(expr) - } + def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = { + def specOk(e: RValue): Unit = { + e match { + case ve: VariableExpr => + if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here") + case a: Assigned => + if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here") + case _ => visitE(e, specOk) + } + } + specOk(expr) + } - def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match { - case _:MaxLockLiteral => - if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention maxlock here") - case _:Literal => - case _:VariableExpr => - case _:ThisExpr => - case _:Result => - case MemberAccess(e, id) => - CheckRunSpecification(e, context, false) - case Access(e, perm) => - CheckRunSpecification(e, context, false) - perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) } - case RdAccess(e, perm) => - CheckRunSpecification(e, context, false) - perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => } - case AccessAll(obj, perm) => - CheckRunSpecification(obj, context, false) - perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) } - case RdAccessAll(obj, perm) => - CheckRunSpecification(obj, context, false) - perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => } - case expr@ Credit(e, n) => - CheckRunSpecification(e, context, false) - CheckRunSpecification(expr.N, context, false) - case Holds(e) => - context.Error(e.pos, "holds is not allowed in specification of run method") - case RdHolds(e) => - context.Error(e.pos, "rd holds is not allowed in specification of run method") - case _:Assigned => - case Old(e) => - CheckRunSpecification(e, context, false) // OLD occurs only in postconditions and monitor invariants, where maxlock is not allowed anyhow - case IfThenElse(con, then, els) => - CheckRunSpecification(con, context, false); - CheckRunSpecification(con, context, allowMaxLock); - CheckRunSpecification(con, context, allowMaxLock); - case Not(e) => - CheckRunSpecification(e, context, false) - case FunctionApplication(obj, id, args) => - obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} - case Unfolding(pred, e) => - CheckRunSpecification(pred, context, true); - CheckRunSpecification(e, context, allowMaxLock); - case LockBelow(e0,e1) => - CheckRunSpecification(e0, context, allowMaxLock) - CheckRunSpecification(e1, context, false) - case And(e0,e1) => - CheckRunSpecification(e0, context, allowMaxLock) - CheckRunSpecification(e1, context, allowMaxLock) - case Implies(e0,e1) => - CheckRunSpecification(e0, context, false) - CheckRunSpecification(e1, context, allowMaxLock) - case bin: BinaryExpr => - CheckRunSpecification(bin.E0, context, false) - CheckRunSpecification(bin.E1, context, false) - case q: Quantification => - CheckRunSpecification(q.Seq, context, false) - CheckRunSpecification(q.E, context, true) - case Length(e) => - CheckRunSpecification(e, context, false); - case ExplicitSeq(es) => - es foreach { e => CheckRunSpecification(e, context, false) } - case Range(min, max) => - CheckRunSpecification(min, context, false) - CheckRunSpecification(max, context, false) - case Eval(h, e) => - h match { - case AcquireState(obj) => CheckRunSpecification(obj, context, false); - case ReleaseState(obj) => CheckRunSpecification(obj, context, false); - case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false); args foreach { a: Expression => CheckRunSpecification(a, context, false)}; - } - CheckRunSpecification(e, context, allowMaxLock) - } + def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match { + case _:MaxLockLiteral => + if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention waitlevel here") + case _:Literal => + case _:VariableExpr => + case _:ThisExpr => + case _:Result => + case MemberAccess(e, id) => + CheckRunSpecification(e, context, false) + case Access(e, perm) => + CheckRunSpecification(e, context, false) + perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) } + case RdAccess(e, perm) => + CheckRunSpecification(e, context, false) + perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => } + case AccessAll(obj, perm) => + CheckRunSpecification(obj, context, false) + perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) } + case RdAccessAll(obj, perm) => + CheckRunSpecification(obj, context, false) + perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => } + case expr@ Credit(e, n) => + CheckRunSpecification(e, context, false) + CheckRunSpecification(expr.N, context, false) + case Holds(e) => + context.Error(e.pos, "holds is not allowed in specification of run method") + case RdHolds(e) => + context.Error(e.pos, "rd holds is not allowed in specification of run method") + case _:Assigned => + case Old(e) => + CheckRunSpecification(e, context, false) // OLD occurs only in postconditions and monitor invariants, where waitlevel is not allowed anyhow + case IfThenElse(con, then, els) => + CheckRunSpecification(con, context, false); + CheckRunSpecification(con, context, allowMaxLock); + CheckRunSpecification(con, context, allowMaxLock); + case Not(e) => + CheckRunSpecification(e, context, false) + case FunctionApplication(obj, id, args) => + obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} + case Unfolding(pred, e) => + CheckRunSpecification(pred, context, true); + CheckRunSpecification(e, context, allowMaxLock); + case LockBelow(e0,e1) => + CheckRunSpecification(e0, context, allowMaxLock) + CheckRunSpecification(e1, context, false) + case And(e0,e1) => + CheckRunSpecification(e0, context, allowMaxLock) + CheckRunSpecification(e1, context, allowMaxLock) + case Implies(e0,e1) => + CheckRunSpecification(e0, context, false) + CheckRunSpecification(e1, context, allowMaxLock) + case bin: BinaryExpr => + CheckRunSpecification(bin.E0, context, false) + CheckRunSpecification(bin.E1, context, false) + case q: Quantification => + CheckRunSpecification(q.Seq, context, false) + CheckRunSpecification(q.E, context, true) + case Length(e) => + CheckRunSpecification(e, context, false); + case ExplicitSeq(es) => + es foreach { e => CheckRunSpecification(e, context, false) } + case Range(min, max) => + CheckRunSpecification(min, context, false) + CheckRunSpecification(max, context, false) + case Eval(h, e) => + h match { + case AcquireState(obj) => CheckRunSpecification(obj, context, false); + case ReleaseState(obj) => CheckRunSpecification(obj, context, false); + case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false); args foreach { a: Expression => CheckRunSpecification(a, context, false)}; + } + CheckRunSpecification(e, context, allowMaxLock) + } - def visitE(expr: RValue, func: RValue => Unit): Unit = { - expr match { - case _:NewRhs => - case e: Literal => ; - case _:ThisExpr => ; - case _:Result => ; - case e:VariableExpr => ; - case acc@MemberAccess(e,f) => - func(e); - case Access(e, perm) => - func(e); perm match { case Some(p) => func(p); case _ => ; } - case RdAccess(e, perm) => - func(e); perm match { case Some(Some(p)) => func(p); case _ => ; } - case AccessAll(obj, perm) => - func(obj); perm match { case Some(p) => func(p); case _ => ; } - case RdAccessAll(obj, perm) => - func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; } - case Credit(e, n) => - func(e); n match { case Some(n) => func(n); case _ => } - case Holds(e) => func(e); - case RdHolds(e) => func(e); - case e: Assigned => e - case Old(e) => func(e); - case IfThenElse(con, then, els) => func(con); func(then); func(els); - case Not(e) => func(e); - case funapp@FunctionApplication(obj, id, args) => - func(obj); args foreach { arg => func(arg) }; - case Unfolding(pred, e) => - func(pred); func(e); - case Iff(e0,e1) => func(e0); func(e1); - case Implies(e0,e1) => func(e0); func(e1); - case And(e0,e1) =>func(e0); func(e1); - case Or(e0,e1) => func(e0); func(e1); - case Eq(e0,e1) => func(e0); func(e1); - case Neq(e0,e1) => func(e0); func(e1); - case Less(e0,e1) => func(e0); func(e1); - case AtMost(e0,e1) => func(e0); func(e1); - case AtLeast(e0,e1) => func(e0); func(e1); - case Greater(e0,e1) => func(e0); func(e1); - case LockBelow(e0,e1) => func(e0); func(e1); - case Plus(e0,e1) => func(e0); func(e1); - case Minus(e0,e1) => func(e0); func(e1); - case Times(e0,e1) => func(e0); func(e1); - case Div(e0,e1) => func(e0); func(e1); - case Mod(e0,e1) => func(e0); func(e1); - case Forall(i, seq, e) => func(seq); func(e); - case ExplicitSeq(es) => - es foreach { e => func(e) } - case Range(min, max) => - func(min); func(max); - case Append(e0, e1) => - func(e0); func(e1); - case at@At(e0, e1) => - func(e0); func(e1); - case Drop(e0, e1) => - func(e0); func(e1); - case Take(e0, e1) => - func(e0); func(e1); - case Length(e) => - func(e) - case Eval(h, e) => - h match { - case AcquireState(obj) => func(obj); - case ReleaseState(obj) => func(obj); - case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)}; - } - func(e); - } - } + def visitE(expr: RValue, func: RValue => Unit): Unit = { + expr match { + case _:NewRhs => + case e: Literal => ; + case _:ThisExpr => ; + case _:Result => ; + case e:VariableExpr => ; + case acc@MemberAccess(e,f) => + func(e); + case Access(e, perm) => + func(e); perm match { case Some(p) => func(p); case _ => ; } + case RdAccess(e, perm) => + func(e); perm match { case Some(Some(p)) => func(p); case _ => ; } + case AccessAll(obj, perm) => + func(obj); perm match { case Some(p) => func(p); case _ => ; } + case RdAccessAll(obj, perm) => + func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; } + case Credit(e, n) => + func(e); n match { case Some(n) => func(n); case _ => } + case Holds(e) => func(e); + case RdHolds(e) => func(e); + case e: Assigned => e + case Old(e) => func(e); + case IfThenElse(con, then, els) => func(con); func(then); func(els); + case Not(e) => func(e); + case funapp@FunctionApplication(obj, id, args) => + func(obj); args foreach { arg => func(arg) }; + case Unfolding(pred, e) => + func(pred); func(e); + case Iff(e0,e1) => func(e0); func(e1); + case Implies(e0,e1) => func(e0); func(e1); + case And(e0,e1) =>func(e0); func(e1); + case Or(e0,e1) => func(e0); func(e1); + case Eq(e0,e1) => func(e0); func(e1); + case Neq(e0,e1) => func(e0); func(e1); + case Less(e0,e1) => func(e0); func(e1); + case AtMost(e0,e1) => func(e0); func(e1); + case AtLeast(e0,e1) => func(e0); func(e1); + case Greater(e0,e1) => func(e0); func(e1); + case LockBelow(e0,e1) => func(e0); func(e1); + case Plus(e0,e1) => func(e0); func(e1); + case Minus(e0,e1) => func(e0); func(e1); + case Times(e0,e1) => func(e0); func(e1); + case Div(e0,e1) => func(e0); func(e1); + case Mod(e0,e1) => func(e0); func(e1); + case Forall(i, seq, e) => func(seq); func(e); + case ExplicitSeq(es) => + es foreach { e => func(e) } + case Range(min, max) => + func(min); func(max); + case Append(e0, e1) => + func(e0); func(e1); + case at@At(e0, e1) => + func(e0); func(e1); + case Drop(e0, e1) => + func(e0); func(e1); + case Take(e0, e1) => + func(e0); func(e1); + case Length(e) => + func(e) + case Eval(h, e) => + h match { + case AcquireState(obj) => func(obj); + case ReleaseState(obj) => func(obj); + case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)}; + } + func(e); + } + } } diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 6b85ed8a..7a85ef74 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -34,7 +34,7 @@ class Translator { decls flatMap { case cl: Class => translateClass(cl) case ch: Channel => translateClass(ChannelClass(ch)) /* TODO: admissibility check of where clause */ - /* TODO: maxlock not allowed in postcondition of things forked (or, rather, joined) */ + /* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */ } } @@ -156,7 +156,7 @@ class Translator { val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran); val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)}); val frameFunctionName = "##" + f.FullName; - + /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n :: wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body)) */ @@ -537,7 +537,7 @@ class Translator { val formalThis = new VariableExpr(formalThisV) val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t) val formalIns = for (v <- formalInsV) yield new VariableExpr(v) - + val (tokenV,tokenId) = NewBVar("token", tref, true) val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true) val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true) @@ -668,9 +668,9 @@ class Translator { bassert(nonNull(ch), ch.pos, "The channel might be null.") :: // check that credits are positive bassert(0 < new Boogie.MapSelect(etran.Credits, TrExpr(ch)), r.pos, "receive operation requires a credit") :: - // ...and check: maxlock << ch.mu + // ...and check: waitlevel << ch.mu bassert(CanRead(ch, "mu"), r.pos, "The mu field of the channel in the receive statement might not be readable.") :: - bassert(etran.MaxLockIsBelowX(etran.Heap.select(ch, "mu")), r.pos, "The channel must lie above maxlock in the wait order") :: + bassert(etran.MaxLockIsBelowX(etran.Heap.select(ch, "mu")), r.pos, "The channel must lie above waitlevel in the wait order") :: // introduce locals for the parameters (for (v <- formalThisV :: formalParamsV) yield BLocal(Variable2BVarWhere(v))) ::: // initialize the parameters; that is, set "this" to the channel and havoc the other formal parameters @@ -686,7 +686,7 @@ class Translator { new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1) } } - + def translateAllocation(cl: Class, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression], pos: Position): (Boogie.BVar, List[Boogie.Stmt]) = { val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true) val (ttV,tt) = Boogie.NewTVar("T") @@ -721,7 +721,7 @@ class Translator { bassume(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu"))) else bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") :: - bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.")) ::: + bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above waitlevel.")) ::: bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) :: // this isn't strictly necessary, it seems; but we might as well include it // remember the state right before releasing BLocal(lastSeenMuV) :: (lastSeenMu := etran.Heap.select(o, "mu")) :: @@ -770,7 +770,7 @@ class Translator { val (heldV, held) = Boogie.NewBVar("held", tint, true) val o = TrExpr(nonNullObj) bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the read-acquire statement might not be readable.") :: - bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above maxlock.") :: + bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above waitlevel.") :: bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) :: // this isn't strictly necessary, it seems; but we might as well include it bassume(! isHeld(o) && ! isRdHeld(o)) :: BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) :: @@ -857,7 +857,7 @@ class Translator { (loopEtran.oldEtran.Credits := loopEtran.Credits) :: // is oldCredits? // check invariant on entry to the loop Exhale(invs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") ::: - List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) ::: + List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) ::: // save values of local-variable loop targets (for (sv <- saveLocalsV) yield BLocal(Variable2BVarWhere(sv))) ::: (for ((v,sv) <- w.LoopTargetsList zip saveLocalsV) yield @@ -948,9 +948,9 @@ class Translator { Below(MuValue(lb), MuValue(ub)) }, lb.pos, "The lower bound at " + lb.pos + " might not be smaller than the upper bound at " + ub.pos + ".")) ::: // havoc mu BLocal(muV) :: Havoc(mu) :: bassume(mu !=@ bLockBottom) :: - // assume that mu is between the given bounds (or above maxlock if no bounds are given) + // assume that mu is between the given bounds (or above waitlevel if no bounds are given) (if (lowerBounds == Nil && upperBounds == Nil) { - // assume maxlock << mu + // assume waitlevel << mu List(bassume(etran.MaxLockIsBelowX(mu))) } else { (for (lb <- lowerBounds) yield @@ -1129,7 +1129,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E /********************************************************************** ***************** TR/DF ***************** **********************************************************************/ - + def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = { def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = { bassert(assumption ==> goal, pos, msg) @@ -1302,7 +1302,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case IntLiteral(n) => n case BoolLiteral(b) => b case NullLiteral() => bnull - case MaxLockLiteral() => throw new Exception("maxlock case should be handled in << and == and !=") + case MaxLockLiteral() => throw new Exception("waitlevel case should be handled in << and == and !=") case LockBottomLiteral() => bLockBottom case _:ThisExpr => VarExpr("this") case _:Result => VarExpr("result") @@ -1425,7 +1425,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass); evalEtran.Tr(e) } - + def translateForall(is: List[Variable], min: Expression, max: Expression, e: Expression): Expr = { var assumption = true: Expr; for(i <- is) { @@ -1745,7 +1745,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E isDefined(obj)(true), true) case CallState(token, obj, id, args) => val argsSeq = CallArgs(Heap.select(Tr(token), "joinable")); - + var i : int = 0; (CallHeap(Heap.select(Tr(token), "joinable")), CallMask(Heap.select(Tr(token), "joinable")), @@ -1760,7 +1760,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E ) } } - + // permissions def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field) @@ -1829,14 +1829,14 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E def IncPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncPerm", List(m, e, f, i)) def IncEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncEpsilons", List(m, e, f, i)) - - def MaxLockIsBelowX(x: Boogie.Expr) = { // maxlock << x + + def MaxLockIsBelowX(x: Boogie.Expr) = { // waitlevel << x val (oV, o) = Boogie.NewBVar("o", tref, false) new Boogie.Forall(oV, (contributesToWaitLevel(o, Heap, Credits)) ==> new Boogie.FunctionApp("MuBelow", Boogie.MapSelect(Heap, o, "mu"), x)) } - def MaxLockIsAboveX(x: Boogie.Expr) = { // x << maxlock + def MaxLockIsAboveX(x: Boogie.Expr) = { // x << waitlevel val (oV, o) = Boogie.NewBVar("o", tref, false) new Boogie.Exists(oV, (contributesToWaitLevel(o, Heap, Credits)) && @@ -1850,7 +1850,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) || (Boogie.MapSelect(Heap, r, "mu") ==@ x))) } - def MaxLockPreserved = { // old(maxlock) == maxlock + def MaxLockPreserved = { // old(waitlevel) == waitlevel // I don't know what the best encoding of this conding is, so I'll try a disjunction. // Disjunct b0 is easier to prove, but it is stronger than b1. @@ -1881,7 +1881,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E (Boogie.MapSelect(oldEtran.Heap, o, "mu") ==@ Boogie.MapSelect(Heap, p, "mu"))) b0 || b1 } - def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = { // e0(maxlock) << e1(maxlock) + def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = { // e0(waitlevel) << e1(waitlevel) // (exists o :: // e1(o.held) && // (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu))) @@ -2063,7 +2063,7 @@ object TranslationHelper { true } } - + def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr = { expr match{ @@ -2318,7 +2318,7 @@ object TranslationHelper { } replaceThis(expr) } - + def manipulate(expr: Expression, func: Expression => Expression): Expression = { val result = expr match { case e: Literal => expr diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el index dc3d469c..34a95a87 100644 --- a/Util/Emacs/chalice-mode.el +++ b/Util/Emacs/chalice-mode.el @@ -38,7 +38,7 @@ "above" "acc" "acquire" "and" "assert" "assigned" "assume" "below" "between" "call" "credit" "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds" - "if" "in" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil" + "if" "in" "ite" "join" "lock" "lockbottom" "waitlevel" "module" "new" "nil" "old" "rd" "receive" "release" "reorder" "result" "send" "share" "this" "unfold" "unfolding" "unshare" "while" "false" "true" "null")) . font-lock-keyword-face) diff --git a/Util/latex/chalice.sty b/Util/latex/chalice.sty index f9ba5234..4ef98f9c 100644 --- a/Util/latex/chalice.sty +++ b/Util/latex/chalice.sty @@ -22,7 +22,7 @@ if,in,int,invariant,ite,% join,% lock,lockbottom,lockchange,% - maxlock,method,module,% + method,module,% new,nil,null,% old,% predicate,% @@ -31,7 +31,7 @@ this,token,true,% unfold,unfolding,unshare,% var,% - while}, + waitlevel,while}, literate=% {=}{{=~}}1% {+=}{{+}{=}~}3% -- cgit v1.2.3