summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Chalice/examples/Answer4
-rw-r--r--Chalice/examples/AssociationList.chalice12
-rw-r--r--Chalice/examples/CopyLessMessagePassing-with-ack.chalice8
-rw-r--r--Chalice/examples/CopyLessMessagePassing-with-ack2.chalice8
-rw-r--r--Chalice/examples/CopyLessMessagePassing.chalice4
-rw-r--r--Chalice/examples/HandOverHand.chalice14
-rw-r--r--Chalice/examples/OwickiGries.chalice2
-rw-r--r--Chalice/examples/ProdConsChannel.chalice12
-rw-r--r--Chalice/examples/Sieve.chalice8
-rw-r--r--Chalice/examples/cell.chalice6
-rw-r--r--Chalice/examples/counter.chalice16
-rw-r--r--Chalice/examples/dining-philosophers.chalice6
-rw-r--r--Chalice/examples/producer-consumer.chalice8
-rw-r--r--Chalice/examples/prog0.chalice2
-rw-r--r--Chalice/examples/prog3.chalice30
-rw-r--r--Chalice/examples/prog4.chalice4
-rw-r--r--Chalice/src/Boogie.scala524
-rw-r--r--Chalice/src/Chalice.scala239
-rw-r--r--Chalice/src/Parser.scala10
-rw-r--r--Chalice/src/PrettyPrinter.scala2
-rw-r--r--Chalice/src/Resolver.scala2066
-rw-r--r--Chalice/src/Translator.scala46
-rw-r--r--Util/Emacs/chalice-mode.el2
-rw-r--r--Util/latex/chalice.sty4
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<T.run>;
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 = "<stdin>"
+ } 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 == "<stdin>") {
+ 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<m.ins.length || 0<m.outs.length) {
- context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
- " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None
- } else
- Some(m)
- case _ =>
- 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<m.ins.length || 0<m.outs.length) {
+ context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+ " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None
+ } else
+ Some(m)
+ case _ =>
+ 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%