diff options
| author |  stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
| commit | 29997a5dd73bfe92292caf1c26fea6b04082a7c9 (patch) | |
| tree | 075d85b62fe670d744384aabfc83b01199d36ca0 /Chalice/tests/examples | |
| parent | 9dfd07f5afe943abf40eaa7a9351ea92748b59ab (diff) | |
Chalice: New permission model that provides more abstraction and more flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/).
This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced:
- Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed
- Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases
- Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.)
Currently not working - but planned to be updated as well - are the following features:
- Stepwise refinements
- autoFold
- read locks
There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice.
A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs)
- workitem 10200: Issue with the axiom of framing functions
- workitem 10197: The translation of old(waitlevel) resultet in Boogie error
- workitem 10196: Quantification over empty sequences
- workitem 10195: Contradiction when descending sequences are used
- workitem 10192: Invalid translation of old-construct in certain cases
- workitem 10190: Stack overflow when parsing large comment blocks
- workitem 10147: Duplicated method parameters and return values are not detected
Diffstat (limited to 'Chalice/tests/examples')
63 files changed, 3367 insertions, 0 deletions
diff --git a/Chalice/tests/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice new file mode 100644 index 00000000..cc3ecfb4 --- /dev/null +++ b/Chalice/tests/examples/AssociationList.chalice @@ -0,0 +1,113 @@ +class Client {
+ method Main(d: Data)
+ requires d != null
+ {
+ var a := new AssociationList
+ call a.Init()
+ call a.Add(5, d)
+ call a.Add(10, d)
+ var t: Data
+ call t := a.Get(10)
+ }
+}
+
+class AssociationList {
+ var head: Node // sentinel
+ invariant rd(head) && head != null
+ invariant rd(mu) && rd(head.mu) && this << head
+
+ method Init()
+ requires acc(head) && acc(mu) && mu == lockbottom
+ ensures acc(mu) && waitlevel << this
+ {
+ head := new Node
+ head.next := null
+ share head
+ share this between waitlevel and head
+ }
+
+ method Add(key: int, value: Data)
+ requires value != null
+ requires rd(mu) && waitlevel << this
+ ensures rd(mu)
+ {
+ acquire this
+ var p: Node := head
+ acquire p
+ release this
+
+ var n := new Node
+ n.key := key
+ n.value := value
+ n.next := p.next
+ p.next := n
+ share n between p and n.next
+ release p
+ }
+
+ method Get(key: int) returns (d: Data)
+ requires rd(mu) && waitlevel << this
+ ensures rd(mu)
+ {
+ d := null
+ acquire this
+ var p: Node := head
+ acquire p
+ release this
+
+ if (p.next != null) {
+ acquire p.next
+ if (p.next.key == key) {
+ d := p.next.value
+ } else {
+ var done := false
+ while (!done)
+ // invariant: holds p and p.next
+ invariant p != null && rd(p.key) && rd(p.value) && acc(p.next) && acc(p.mu,50) && p.next != null
+ invariant acc(p.next.mu) && p << p.next
+ 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) && waitlevel == p.next.mu
+ invariant p.next.next != null ==> waitlevel << p.next.next
+ lockchange p, p.next.next
+ {
+ if (p.next.next == null) {
+ done := true // key not present
+ } else {
+ acquire p.next.next
+ if (p.next.next.key == key) {
+ done := true // key is present
+ d := p.next.next.value
+ // move p.next.next closer to the head by one step
+
+ var t: Node := p.next
+ p.next := t.next
+ t.next := p.next.next
+ p.next.next := t
+ reorder t between p.next and t.next
+ release t
+ } else {
+ var t: Node := p
+ p := p.next
+ release t
+ }
+ }
+ }
+ }
+ release p.next
+ }
+ release p
+ }
+}
+
+class Data { }
+
+class Node
+{
+ var key: int
+ var value: Data
+ var next: Node
+ invariant rd(key) && rd(value) && acc(next) && acc(mu,50)
+ invariant next != null ==> acc(next.mu,50) && this << next
+}
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt new file mode 100644 index 00000000..719af1af --- /dev/null +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -0,0 +1,6 @@ +Verification of AssociationList.chalice
+
+ 19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.
+ 64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+
+Boogie program verifier finished with 10 verified, 2 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice new file mode 100644 index 00000000..2646f96a --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice @@ -0,0 +1,83 @@ +// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)
+
+// msg tag indicates what the type of the message
+// channel is freed by Getter when it completes
+// ack works, but an assume is needed and negative credits are sent over channels!
+
+// Conjecture: it is ok to send debit for yourself over yourself.
+// Why: Suppose a channel that allows self-debt is involved in a deadlock. The either that channel is empty, which means there's no difference between the situation with or with self-debt. Or the channel is non-empty. This means that we can make progress by receiving the message stored in the channel! Does this make any sense?
+
+channel C(msg: int, n: Node) where
+ (msg == 0 ==> credit(this, -1)) && // ack
+ (msg == 1 ==> n != null && acc(n.next) && acc(n.mu) && credit(this, -1)) && // cell
+ (msg == 2 ==> acc(this.mu, 50)); // done
+
+
+class Node {
+ var next: Node;
+
+ function length(): int
+ requires this.list;
+ {
+ unfolding this.list in 1 + (next == null ? 0 : next.length())
+ }
+
+ predicate list {
+ acc(next) && acc(mu) && (next != null ==> next.list)
+ }
+}
+
+class Program {
+ method Putter(e: C, x0: Node)
+ 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;
+
+ while(x != null)
+ invariant (x != null ==> x.list) && acc(e.mu, 50) && credit(e, - 1);
+ {
+ unfold x.list;
+ t := x.next;
+ send e(1, x);
+ x := t;
+ var ack;
+ assume waitlevel << e.mu; // Chalice should be able to figure this out itself
+ receive ack, t := e;
+ if(ack != 2) { assume false; /* abort */ }
+ }
+ send e(2, null);
+ }
+
+ method Getter(f: C)
+ 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) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));
+ {
+ receive msg, x := f;
+ if(msg == 0) {
+ }
+ if(msg == 1) {
+ free x;
+ send f(2, null);
+ }
+ if(msg != 0 || msg != 1) { assume false; /* abort */ }
+ }
+ free f; // close the channel
+ }
+
+ method Main(x: Node)
+ requires x != null;
+ requires x.list;
+ {
+ var e := new C;
+ fork Putter(e, x);
+ fork Getter(e);
+ }
+}
+
+
+
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt new file mode 100644 index 00000000..46633611 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing-with-ack.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice new file mode 100644 index 00000000..7744d291 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice @@ -0,0 +1,89 @@ +// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)
+
+// msg tag indicates what the type of the message
+// channel is freed by Getter when it completes
+// ack-channel instead of single channel with ack message channel
+// using Owicki-Gries ghostfields can be used to remove the "assume false;" statements
+
+// Conjecture: it is ok to send debit credit(d, -x) over a channel c as long as
+// a) d.mu << c.mu
+// b) leaking positive or negative debit is not allowed
+
+channel AckChannel(ch: C) where ch != null && credit(ch, -1); // ack
+
+channel C(msg: int, n: Node, ackC: AckChannel) where
+ (msg == 0 || msg == 1) &&
+ (msg == 0 ==> acc(this.mu, 50) && acc(ackC.mu, 50)) &&
+ (msg == 1 ==> n != null && acc(n.next) && acc(n.mu) && credit(ackC, -1)); // cell
+
+class Node {
+ var next: Node;
+
+ function length(): int
+ requires this.list;
+ {
+ unfolding this.list in 1 + (next == null ? 0 : next.length())
+ }
+
+ predicate list {
+ acc(next) && acc(mu) && (next != null ==> next.list)
+ }
+}
+
+class Program {
+ method Putter(e: C, x0: Node, ackC: AckChannel)
+ 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;
+
+ while(x != null)
+ invariant (x != null ==> x.list) && acc(e.mu, 50) && acc(ackC.mu, 50) && e.mu << ackC.mu && credit(e, - 1);
+ {
+ unfold x.list;
+ t := x.next;
+ send e(1, x, ackC);
+ x := t;
+ var ack;
+ 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 */ }
+ }
+ send e(0, null, ackC);
+ }
+
+ method Getter(f: C, ackC: AckChannel)
+ 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) && 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;
+ if(ackC2 != ackC) { assume false; /* abort */ }
+ if(msg == 0) {
+ }
+ if(msg == 1) {
+ free x;
+ send ackC(f);
+ }
+ }
+ free f; // close the channel
+ }
+
+ method Main(x: Node)
+ requires x != null;
+ requires x.list;
+ {
+ var e := new C;
+ var ackC := new AckChannel above e;
+ fork Putter(e, x, ackC);
+ fork Getter(e, ackC);
+ }
+}
+
+
+
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt new file mode 100644 index 00000000..e8c42507 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing-with-ack2.chalice
+
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.chalice b/Chalice/tests/examples/CopyLessMessagePassing.chalice new file mode 100644 index 00000000..4b8a9389 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing.chalice @@ -0,0 +1,72 @@ +// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)
+
+// msg tag indicates what the type of the message
+// channel is freed by Getter when it completes
+
+// todo: accept ack message before sending the next one (requires sending negative credit!)
+
+channel C(msg: int, n: Node) where n!= null && acc(n.next) && acc(n.mu) && (msg == 1 ==> credit(this, 1)) && (msg == 0 ==> acc(this.mu, 50));
+
+class Node {
+ var next: Node;
+
+ function length(): int
+ requires this.list;
+ {
+ unfolding this.list in 1 + (next == null ? 0 : next.length())
+ }
+
+ predicate list {
+ acc(next) && acc(mu) && (next != null ==> next.list)
+ }
+}
+
+class Program {
+ method Putter(e: C, x0: Node)
+ requires e!= null && acc(e.mu, 50) && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));
+ {
+ var x: Node := x0;
+ var t: Node;
+
+ while(x != null)
+ invariant (x != null ==> x.list) && (x!=null ==> acc(e.mu, 50)) && (x != null ==> credit(e, - 1));
+ {
+ unfold x.list;
+ t := x.next;
+ if(t != null) {
+ send e(1, x);
+ } else {
+ send e(0, x);
+ }
+ x := t;
+ }
+ }
+
+ method Getter(f: C)
+ 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) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));
+ {
+ receive msg, x := f;
+ if(msg == 1) {
+ free x;
+ }
+ }
+ free f; // close the channel
+ }
+
+ method Main(x: Node)
+ requires x != null;
+ requires x.list;
+ {
+ var e := new C;
+ fork Putter(e, x);
+ fork Getter(e);
+ }
+}
+
+
+
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt new file mode 100644 index 00000000..d6fd8be3 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/ForkJoin.chalice b/Chalice/tests/examples/ForkJoin.chalice new file mode 100644 index 00000000..e79cded9 --- /dev/null +++ b/Chalice/tests/examples/ForkJoin.chalice @@ -0,0 +1,77 @@ +/* Example taken from ESOP submission */
+
+class T {
+ var k: int;
+ var l: int;
+
+ method run()
+ requires acc(k);
+ ensures acc(k) && k == old(k) + 1;
+ {
+ k := k + 1;
+ }
+}
+
+class Program {
+ method main() {
+ var x := new T;
+ x.k := 17;
+ x.l := 20;
+ fork tok := x.run();
+ x.l := 10;
+ join tok;
+ assert x.k == 18 && x.l == 10;
+ }
+
+ method justJoin(tok: token<T.run>, x: T) returns (rt: int)
+ requires x!=null && tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork x.run(), acc(x.k));
+ ensures rt == old(eval(tok.fork x.run(), x.k)) + 1;
+ {
+ join tok;
+ rt := x.k;
+ }
+}
+
+/* example using asynchronous method calls */
+
+class C {
+ var x: int;
+
+ method m(v: int) returns (rt: int)
+ ensures rt == v + 1;
+ {
+ rt := v + 1;
+ }
+}
+
+class Program2 {
+ method main1(){
+ var c := new C;
+ var tok: token<C.m>;
+ fork tok := c.m(5);
+
+ // do some computation
+
+ var x : int;
+ join x := tok;
+ assert x == 6;
+ }
+
+ method main2(){
+ var c := new C;
+ var tok: token<C.m>;
+ fork tok := c.m(5);
+
+ // do some computation
+
+ call foo(tok, c);
+ }
+
+ method foo(tok: token<C.m>, o: C)
+ requires tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork o.m(5), true);
+ {
+ var x: int;
+ join x := tok;
+ assert x == 6;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt new file mode 100644 index 00000000..06d44bec --- /dev/null +++ b/Chalice/tests/examples/ForkJoin.output.txt @@ -0,0 +1,4 @@ +Verification of ForkJoin.chalice
+
+
+Boogie program verifier finished with 18 verified, 0 errors
diff --git a/Chalice/tests/examples/HandOverHand.chalice b/Chalice/tests/examples/HandOverHand.chalice new file mode 100644 index 00000000..31818ca6 --- /dev/null +++ b/Chalice/tests/examples/HandOverHand.chalice @@ -0,0 +1,132 @@ +class List {
+ ghost var sum: int
+ var head: Node
+ invariant acc(head) && head != null
+ invariant rd(head.val) && head.val == -1
+ invariant rd(mu) && acc(head.mu,50) && this << head
+ invariant acc(sum,20) && acc(head.sum, 50) && sum == head.sum
+
+ method Main()
+ {
+ var list := new List
+ call list.Init()
+ call list.Insert(8)
+ call list.Insert(12)
+ call list.Insert(4)
+ assert list.sum == 24
+ }
+
+ method Init()
+ requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)
+ ensures rd*(mu) && waitlevel << this
+ ensures acc(sum,80) && sum == 0
+ {
+ var t := new Node
+ t.val := -1
+ t.next := null
+ t.sum := 0
+ share t
+ head := t
+ sum := 0
+ share this between waitlevel and t
+ }
+
+ method Insert(x: int)
+ 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 waitlevel == this.mu;
+ sum := sum + x
+ var p: Node := head
+ acquire p
+ p.sum := p.sum + x
+ release this
+
+ while (p.next != null && p.next.val < x)
+ invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
+ invariant holds(p) && waitlevel == p.mu
+ invariant !old(holds(p)) && !old(rd holds(p))
+ invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
+ invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
+ invariant acc(p.sum, 50)
+ invariant p.next == null ==> p.sum == x
+ invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum + x
+ invariant p.val <= x
+ lockchange p
+ {
+ var nx: Node := p.next
+ acquire nx
+ nx.sum := nx.sum + x
+ release p
+ p := nx
+ }
+ var t := new Node
+ t.val := x
+ t.next := p.next
+ if (t.next == null) { t.sum := 0 } else { t.sum := p.next.val + p.next.sum }
+ share t between p and p.next
+ p.next := t
+ release p
+ }
+
+ method Delete(x: int) returns (wasPresent: bool)
+ requires rd(mu) && waitlevel << this
+ requires acc(sum,80) && 0 <= x
+ ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum))
+ {
+ ghost const c
+
+ acquire this
+ sum := sum - c
+ var p: Node := head
+ acquire p
+ p.sum := p.sum - c
+ release this
+
+ while (p.next != null && p.next.val < x)
+ invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
+ invariant holds(p) && waitlevel == p.mu && !assigned(c)
+ invariant !old(holds(p)) && !old(rd holds(p))
+ invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
+ invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
+ invariant acc(p.sum, 50)
+ invariant p.next == null ==> p.sum == 0 - c
+ invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum - c
+ invariant p.val <= x
+ lockchange p
+ {
+ var nx: Node := p.next
+ acquire nx
+ nx.sum := nx.sum - c
+ release p
+ p := nx
+ }
+ if (p.next != null && p.next.val == x) {
+ wasPresent := true
+ c := x
+ var nx: Node := p.next
+ acquire nx
+ p.next := nx.next
+ unshare nx
+ } else {
+ wasPresent := false
+ c := 0
+ }
+ release p
+ }
+}
+
+class Node {
+ ghost var sum: int
+ var val: int
+ var next: Node
+ invariant acc(next) && rd(val)
+ invariant next != null ==> rd(next.val) && val <= next.val
+ invariant acc(sum, 50)
+ invariant next == null ==> sum == 0
+ invariant next != null ==> acc(next.sum, 50) && sum == next.val + next.sum
+ invariant acc(mu,50) && (next != null ==> acc(next.mu,50) && this << next)
+}
diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt new file mode 100644 index 00000000..a57fe677 --- /dev/null +++ b/Chalice/tests/examples/HandOverHand.output.txt @@ -0,0 +1,4 @@ +Verification of HandOverHand.chalice
+
+
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Chalice/tests/examples/ImplicitLocals.chalice b/Chalice/tests/examples/ImplicitLocals.chalice new file mode 100644 index 00000000..15ebe8e0 --- /dev/null +++ b/Chalice/tests/examples/ImplicitLocals.chalice @@ -0,0 +1,27 @@ +class C {
+ var k: int;
+
+ method MyMethod() returns (x: int, y: C)
+ requires acc(k)
+ ensures acc(y.k) && x < y.k
+ {
+ x := k - 15;
+ y := this;
+ }
+
+ method B() {
+ var c := new C;
+ call a, b := c.MyMethod();
+ assert a < b.k;
+ }
+
+ method D() {
+ var ch := new Ch;
+ var c := new C;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, b := ch;
+ assert a < b.k;
+ }
+}
+
+channel Ch(x: int, y: C) where acc(y.k) && x < y.k;
diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt new file mode 100644 index 00000000..c3f518ed --- /dev/null +++ b/Chalice/tests/examples/ImplicitLocals.output.txt @@ -0,0 +1,4 @@ +Verification of ImplicitLocals.chalice
+
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Chalice/tests/examples/LoopLockChange.chalice b/Chalice/tests/examples/LoopLockChange.chalice new file mode 100644 index 00000000..5ccce089 --- /dev/null +++ b/Chalice/tests/examples/LoopLockChange.chalice @@ -0,0 +1,142 @@ +class LoopLockChange { + + method Test0() + requires rd(mu) && waitlevel << mu + lockchange this; + { + acquire this; + + var b := true; + while(b) // error: lockchange clause of loop must include all lock changes that happened before the loop + { + b := false; + } + } + + method Test1() + requires rd(mu) && waitlevel << mu + lockchange this; + { + acquire this; + + var b := true; + while(b) + lockchange this; + { + b := false; + } + } + + method Test2() + requires rd(mu) && waitlevel << mu + lockchange this; + { + var b := true; + while(b) // error: insufficient lockchange clause + invariant rd(mu); + invariant b ==> waitlevel << mu + { + acquire this; + b := false; + } + } + + method Test3() + requires rd(mu) && waitlevel << mu + lockchange this; + { + var b := true; + while(b) + invariant rd(mu); + invariant b ==> waitlevel << mu + lockchange this; + { + acquire this; + b := false; + } + } + + method Test4(p: LoopLockChange) + requires rd(p.mu) && waitlevel << p.mu + requires rd(mu) && waitlevel << mu + { + var current: LoopLockChange := this; + var b := true; + while(b) + invariant rd(current.mu) + invariant b ==> rd(p.mu); + invariant b ==> waitlevel << current.mu + lockchange current; // error: after the loop body, current does no longer point to the object whose lock was acquired + { + acquire current; + current := p; + b := false; + } + assume false; // to prevent complaint about method's lockchange clause + } + + + method Test5(p: LoopLockChange) + requires rd(p.mu) && waitlevel << p.mu + requires rd(mu) && waitlevel << mu + lockchange this; + { + var current: LoopLockChange := this; + var b := true; + while(b) + invariant rd(current.mu) + invariant b ==> rd(p.mu); + invariant b ==> current == this; + invariant b ==> waitlevel << current.mu + lockchange this; + { + acquire current; + current := p; + b := false; + } + } + + + method Test6() + requires rd(mu) && waitlevel << mu + { + var b := true; + while(b) + invariant rd(mu); + invariant b ==> waitlevel << mu + invariant b ==> !(rd holds(this)) + invariant !b ==> holds(this) + lockchange this; + { + acquire this; + b := false; + } + release this; + } + + + method Test7() + requires rd(mu) && waitlevel << mu + { + acquire this; + release this; + } + + +// The following test requires a better treatment of allocation, which we don't have yet +/* method Test8() + { + var tmp : LoopLockChange := this; + var b := false; + while(b) + { + tmp := new LoopLockChange; + share tmp; + acquire tmp; + b := false; + } + assert !holds(tmp); + } +*/ +} + diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt new file mode 100644 index 00000000..c6c69a24 --- /dev/null +++ b/Chalice/tests/examples/LoopLockChange.output.txt @@ -0,0 +1,7 @@ +Verification of LoopLockChange.chalice
+
+ 10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+ 35.5: The loop might lock/unlock more than the lockchange clause allows.
+ 65.5: The loop might lock/unlock more than the lockchange clause allows.
+
+Boogie program verifier finished with 14 verified, 3 errors
diff --git a/Chalice/tests/examples/OwickiGries.chalice b/Chalice/tests/examples/OwickiGries.chalice new file mode 100644 index 00000000..f466b58a --- /dev/null +++ b/Chalice/tests/examples/OwickiGries.chalice @@ -0,0 +1,35 @@ +class OwickiGries {
+ var counter: int
+ ghost var c0: int
+ ghost var c1: int
+ invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1
+
+ method Main() {
+ var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 }
+ share og
+
+ fork tk0 := og.Worker(false)
+ fork tk1 := og.Worker(true)
+ join tk0; join tk1
+
+ acquire og; unshare og
+ assert og.counter == 2
+ }
+
+ method Worker(b: bool)
+ 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
+ ensures b ==> acc(c1,50) && c1 == old(c1) + 1
+ {
+ lock (this) {
+ counter := counter + 1
+ if (!b) {
+ c0 := c0 + 1
+ } else {
+ c1 := c1 + 1
+ }
+ }
+ }
+}
diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt new file mode 100644 index 00000000..ff585ab1 --- /dev/null +++ b/Chalice/tests/examples/OwickiGries.output.txt @@ -0,0 +1,4 @@ +Verification of OwickiGries.chalice
+
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.chalice b/Chalice/tests/examples/PetersonsAlgorithm.chalice new file mode 100644 index 00000000..8760b04b --- /dev/null +++ b/Chalice/tests/examples/PetersonsAlgorithm.chalice @@ -0,0 +1,79 @@ +class Peterson {
+ var x0: bool;
+ var x1: bool;
+ var turn: bool;
+ ghost var cs0: bool;
+ ghost var cs1: bool;
+ ghost var b0: bool;
+ ghost var b1: bool;
+
+ invariant acc(x0,50) && acc(x1,50) && acc(turn);
+ invariant acc(cs0,50) && acc(cs1,50) && acc(b0,50) && acc(b1,50);
+ invariant cs0 ==> x0 && !b0 && (!x1 || !turn || b1);
+ invariant cs1 ==> x1 && !b1 && (!x0 || turn || b0);
+
+ method Main() {
+ var p := new Peterson{ x0 := false, x1 := false,
+ cs0 := false, cs1 := false, b0 := false, b1 := false };
+ share p;
+ fork p.Process0();
+ fork p.Process1();
+ // The purpose of the following loop is simply to prove mutual exclusion, that is,
+ // to prove that !(cs0 && cs1) follows from the monitor invariant.
+ while (true)
+ invariant rd(p.mu) && waitlevel << p.mu;
+ {
+ lock (p) { assert !(p.cs0 && p.cs1); }
+ }
+ }
+
+ method Process0()
+ requires rd(mu) && waitlevel << mu;
+ requires acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0;
+ {
+ while (true)
+ invariant rd(mu) && waitlevel << mu;
+ invariant acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0;
+ {
+ [[ x0 := true; b0 := true; ]]
+ [[ turn := true; b0 := false; ]]
+ // await (!x1 || !turn)
+ var waiting := true;
+ while (waiting)
+ invariant rd(mu) && waitlevel << mu && acc(cs0,50);
+ invariant acc(x0,50) && acc(b0,50) && x0 && !b0;
+ invariant !waiting ==> cs0;
+ {
+ [[ if (!x1) { waiting := false; cs0 := true; } ]]
+ [[ if (!turn) { waiting := false; cs0 := true; } ]]
+ }
+ // critical section...
+ [[ cs0 := false; x0 := false; ]]
+ }
+ }
+
+ method Process1()
+ requires rd(mu) && waitlevel << mu;
+ requires acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1;
+ {
+ while (true)
+ invariant rd(mu) && waitlevel << mu;
+ invariant acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1;
+ {
+ [[ x1 := true; b1 := true; ]]
+ [[ turn := false; b1 := false; ]]
+ // await (!x0 || turn)
+ var waiting := true;
+ while (waiting)
+ invariant rd(mu) && waitlevel << mu && acc(cs1,50);
+ invariant acc(x1,50) && acc(b1,50) && x1 && !b1;
+ invariant !waiting ==> cs1;
+ {
+ [[ if (!x0) { waiting := false; cs1 := true; } ]]
+ [[ if (turn) { waiting := false; cs1 := true; } ]]
+ }
+ // critical section...
+ [[ cs1 := false; x1 := false; ]]
+ }
+ }
+}
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt new file mode 100644 index 00000000..bf470e3a --- /dev/null +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -0,0 +1,4 @@ +Verification of PetersonsAlgorithm.chalice
+
+
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Chalice/tests/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice new file mode 100644 index 00000000..563d72b6 --- /dev/null +++ b/Chalice/tests/examples/ProdConsChannel.chalice @@ -0,0 +1,126 @@ +class Cell {
+ var val: int
+}
+
+channel Ch(c: Cell) where
+ c != null ==> acc(c.val) && 0 <= c.val && credit(this)
+
+class Program {
+ method Main() {
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ join tk0
+ join tk1
+ }
+ method Producer(ch: Ch)
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1
+ }
+ send ch(null)
+ }
+ method Consumer(ch: Ch)
+ 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) && waitlevel << ch.mu
+ invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
+ {
+ var i := c.val
+ receive c := ch
+ }
+ }
+
+ // variations
+ method Main0() { // error: debt remains after body
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ // join tk0
+ join tk1
+ }
+ method Main1() {
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ join tk0
+ // join tk1
+ } // no problem
+ method Producer0(ch: Ch) // error: debt remains after body
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1
+ }
+ // send ch(null)
+ }
+ method Producer1(ch: Ch)
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1 + c.val // error: can no longer read c.val
+ }
+ send ch(null)
+ }
+ method Consumer0(ch: Ch)
+ 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) && waitlevel << ch.mu
+ invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
+ {
+ var i := c.val
+ receive c := ch
+ }
+ }
+ method Consumer1(ch: Ch)
+ requires rd(ch.mu) && waitlevel << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert 0 <= c.val // follows from where clause
+ }
+ }
+ method Consumer2(ch: Ch)
+ requires rd(ch.mu) && waitlevel << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert c.val < 2 // error: does not follow from where clause
+ }
+ }
+}
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt new file mode 100644 index 00000000..1cfe7dfb --- /dev/null +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -0,0 +1,8 @@ +Verification of ProdConsChannel.chalice
+
+ 47.3: Method body is not allowed to leave any debt.
+ 61.3: Method body is not allowed to leave any debt.
+ 85.20: Location might not be readable.
+ 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
+
+Boogie program verifier finished with 19 verified, 4 errors
diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/examples/RockBand-automagic.chalice new file mode 100644 index 00000000..d231ae5a --- /dev/null +++ b/Chalice/tests/examples/RockBand-automagic.chalice @@ -0,0 +1,111 @@ +// verify this program with -checkLeaks -defaults -autoFold -autoMagic
+
+class Client {
+ method Main() {
+ var b := new RockBand
+ call b.Init()
+ call b.Play()
+ call b.Play()
+ call b.Dispose()
+ }
+}
+
+class RockBand module M {
+ var gigs: int
+ var gt: Guitar
+ var doowops: seq<Vocalist>
+ var b3: Organ
+ predicate Valid {
+ /*acc(gigs) &&*/ 0 <= gigs &&
+ /*acc(gt) && gt != null &&*/ gt.Valid &&
+ acc(gt.mu) &&
+ acc(doowops) &&
+ /*acc(b3) && b3 != null &&*/ b3.Valid &&
+ acc(b3.mu)
+ }
+
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ gigs := 0
+ gt := new Guitar
+ call gt.Init()
+ b3 := new Organ
+ call b3.Init()
+ }
+
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ call gt.Dispose()
+ call b3.Dispose()
+ free this
+ }
+
+ method Play()
+ requires Valid
+ ensures Valid
+ {
+ gigs := gigs + 1
+ call gt.Strum()
+ call b3.Grind()
+ }
+}
+
+class Guitar module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Strum()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
+
+class Vocalist module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Strum()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
+
+class Organ module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Grind()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt new file mode 100644 index 00000000..d494e16a --- /dev/null +++ b/Chalice/tests/examples/RockBand-automagic.output.txt @@ -0,0 +1,11 @@ +Verification of RockBand-automagic.chalice
+
+ 19.27: Location might not be readable.
+ 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
+ 41.10: Location might not be readable.
+ 50.5: Location might not be writable
+ 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
+ 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
+
+Boogie program verifier finished with 28 verified, 7 errors
diff --git a/Chalice/tests/examples/RockBand.chalice b/Chalice/tests/examples/RockBand.chalice new file mode 100644 index 00000000..49b99a68 --- /dev/null +++ b/Chalice/tests/examples/RockBand.chalice @@ -0,0 +1,111 @@ +// verify this program with -checkLeaks -defaults -autoFold
+
+class Client {
+ method Main() {
+ var b := new RockBand
+ call b.Init()
+ call b.Play()
+ call b.Play()
+ call b.Dispose()
+ }
+}
+
+class RockBand module M {
+ var gigs: int
+ var gt: Guitar
+ var doowops: seq<Vocalist>
+ var b3: Organ
+ predicate Valid {
+ acc(gigs) && 0 <= gigs &&
+ acc(gt) && gt != null && gt.Valid &&
+ acc(gt.mu) && // to enable an eventual free
+ acc(doowops) && //forall d: Vocalist in doowops :: d != null && d.Valid} &&
+ acc(b3) && b3 != null && b3.Valid &&
+ acc(b3.mu) // to enable an eventual free
+ }
+
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ gigs := 0
+ gt := new Guitar
+ call gt.Init()
+ b3 := new Organ
+ call b3.Init()
+ }
+
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ call gt.Dispose()
+ call b3.Dispose()
+ free this
+ }
+
+ method Play()
+ requires Valid
+ ensures Valid
+ {
+ gigs := gigs + 1
+ call gt.Strum()
+ call b3.Grind()
+ }
+}
+
+class Guitar module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Strum()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
+
+class Vocalist module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Strum()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
+
+class Organ module Musicians {
+ predicate Valid { true }
+ method Init()
+ requires acc(this.*)
+ ensures Valid
+ {
+ }
+ method Dispose()
+ requires Valid && acc(mu)
+ {
+ free this
+ }
+ method Grind()
+ requires Valid
+ ensures Valid
+ {
+ }
+}
diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt new file mode 100644 index 00000000..3fb1b1c6 --- /dev/null +++ b/Chalice/tests/examples/RockBand.output.txt @@ -0,0 +1,10 @@ +Verification of RockBand.chalice
+
+ 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
+ 41.10: Location might not be readable.
+ 50.5: Location might not be writable
+ 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
+ 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
+
+Boogie program verifier finished with 29 verified, 6 errors
diff --git a/Chalice/tests/examples/Sieve.chalice b/Chalice/tests/examples/Sieve.chalice new file mode 100644 index 00000000..d7223d04 --- /dev/null +++ b/Chalice/tests/examples/Sieve.chalice @@ -0,0 +1,63 @@ +channel NumberStream(x: int) where 2 <= x ==> credit(this);
+
+class Sieve {
+ method Counter(n: NumberStream, to: int) // sends the plurals along n
+ requires rd(n.mu) && credit(n,-1) && 0 <= to;
+ {
+ var i := 2;
+ while (i < to)
+ invariant rd(n.mu);
+ invariant 2 <= i;
+ invariant credit(n, -1)
+ {
+ send n(i);
+ i := i + 1;
+ }
+ send n(-1);
+ }
+
+ method Filter(prime: int, r: NumberStream, s: NumberStream)
+ requires 2 <= prime;
+ 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 && waitlevel << r.mu;
+ invariant 2<= x ==> credit(r);
+ invariant credit(s, -1);
+ {
+ if (x % prime != 0) { // suppress multiples of prime
+ send s(x);
+ }
+ receive x := r;
+
+ }
+ send s(-1);
+ }
+
+ method Start()
+ {
+ var ch := new NumberStream;
+ fork Counter(ch, 101);
+ var p: int;
+ receive p := ch;
+ while (2 <= p)
+ invariant ch != null;
+ invariant 2 <= p ==> credit(ch, 1);
+ 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 waitlevel and ch;
+ fork Filter(p, ch, n);
+ ch := n;
+ receive p := ch;
+ }
+ }
+}
+
+external class ChalicePrint {
+ method Int(x: int) { }
+}
diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt new file mode 100644 index 00000000..b8b74b59 --- /dev/null +++ b/Chalice/tests/examples/Sieve.output.txt @@ -0,0 +1,4 @@ +Verification of Sieve.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/examples/cell-defaults.chalice new file mode 100644 index 00000000..4781db97 --- /dev/null +++ b/Chalice/tests/examples/cell-defaults.chalice @@ -0,0 +1,152 @@ +// verify this program with -defaults -autoFold -autoMagic
+
+class Cell module Library {
+ var x: int;
+
+ method init(v: int)
+ requires acc(this.x) && 0<=v;
+ ensures valid && this.get() == v;
+ {
+ x := v;
+ }
+
+ method set(v: int)
+ requires valid && 0<=v;
+ ensures valid && get()==v;
+ {
+ x := v;
+ }
+
+ method increment()
+ requires valid;
+ ensures valid && get() == old(get()) + 1;
+ {
+ x := x + 1;
+ }
+
+ method dispose()
+ requires valid && acc(mu);
+ ensures true;
+ {
+ free this;
+ }
+
+ function get(): int
+ requires valid;
+ ensures 0<=result;
+ {
+ x
+ }
+
+ predicate valid {
+ acc(this.x) && 0<=x
+ }
+
+ invariant valid;
+}
+
+class Interval module Library2 {
+ var left: Cell;
+ var right: Cell;
+
+ method init(l: int, r: int)
+ requires 0<=l && l <= r;
+ requires acc(left) && acc(right);
+ ensures valid;
+ ensures getLeft()==l
+ ensures getRight()==r;
+ {
+ left := new Cell;
+ call left.init(l);
+ right := new Cell;
+ call right.init(r);
+ }
+
+ method setLeft(l: int)
+ requires valid;
+ requires 0<=l && l<=getRight();
+ ensures valid;
+ ensures getLeft()==l && getRight()==old(getRight());
+ {
+ call left.set(l);
+ }
+
+ method setRight(r: int)
+ requires valid;
+ requires 0<=r && getLeft()<=r;
+ ensures valid;
+ ensures getLeft()==old(getLeft()) && getRight()==r;
+ {
+ call right.set(r);
+ }
+
+ method shift(v: int)
+ requires valid;
+ requires 0<=v;
+ ensures valid;
+ ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;
+ {
+ call left.set(left.get()+v);
+ call right.set(right.get()+v);
+ }
+
+ function getLeft() : int
+ requires valid;
+ {
+ left.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
+ }
+
+ function getRight() : int
+ requires valid;
+ {
+ right.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
+ }
+
+ predicate valid
+ {
+ left.valid && right.valid && left.get() <= right.get()
+ }
+}
+
+class Program module Main {
+ method main(){
+ var c1 := new Cell;
+ call c1.init(5);
+ call c1.set(6);
+
+ var c2 := new Cell;
+ call c2.init(10);
+ call c2.set(11);
+
+ assert c1.get() == 6;
+ }
+
+ method main2(){
+ var c: Cell;
+
+ c := new Cell;
+ call c.init(0);
+ call c.dispose();
+
+ assert c.valid; // should fail
+ }
+
+ method main3() returns (rt: Cell)
+ ensures rt!=null && rt.valid && rt.get() == 0
+ {
+ rt := new Cell;
+ call rt.init(0)
+ }
+
+ method main4() {
+ var c: Cell;
+
+ c := new Cell;
+ call c.init(0);
+ share c;
+
+ acquire c;
+ call c.set(1);
+ release c;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt new file mode 100644 index 00000000..ee7ae4e5 --- /dev/null +++ b/Chalice/tests/examples/cell-defaults.output.txt @@ -0,0 +1,17 @@ +Verification of cell-defaults.chalice
+
+ 6.3: The postcondition at 8.13 might not hold. Insufficient fraction at 8.13 for Cell.valid.
+ 17.5: Location might not be writable
+ 24.5: Location might not be writable
+ 31.5: The field x of the target of the free statement might not be writable.
+ 38.5: Location might not be readable.
+ 52.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Interval.valid.
+ 71.10: Location might not be readable.
+ 80.10: Location might not be readable.
+ 89.10: Location might not be readable.
+ 96.5: Location might not be readable.
+ 102.5: Location might not be readable.
+ 107.5: Location might not be readable.
+ 131.5: Assertion might not hold. Insufficient fraction at 131.12 for Cell.valid.
+
+Boogie program verifier finished with 19 verified, 13 errors
diff --git a/Chalice/tests/examples/cell.chalice b/Chalice/tests/examples/cell.chalice new file mode 100644 index 00000000..1cf82950 --- /dev/null +++ b/Chalice/tests/examples/cell.chalice @@ -0,0 +1,163 @@ +class Cell module Library {
+ var x: int;
+
+ method init(v: int)
+ requires acc(this.x) && 0<=v;
+ ensures valid && this.get() == v;
+ {
+ x := v;
+ fold valid;
+ }
+
+ method set(v: int)
+ requires valid && 0<=v;
+ ensures valid && get()==v;
+ {
+ unfold valid;
+ x := v;
+ fold valid;
+ }
+
+ method increment()
+ requires valid;
+ ensures valid && get() == old(get()) + 1;
+ {
+ unfold valid;
+ x := x + 1;
+ fold valid;
+ }
+
+ method dispose()
+ requires valid && acc(mu);
+ ensures true;
+ {
+ unfold valid;
+ free this;
+ }
+
+ function get(): int
+ requires valid;
+ ensures 0<=result;
+ {
+ unfolding valid in x
+ }
+
+ predicate valid {
+ acc(this.x) && 0<=x
+ }
+
+ invariant valid;
+}
+
+class Interval module Library2 {
+ var left: Cell;
+ var right: Cell;
+
+ method init(l: int, r: int)
+ requires 0<=l && l <= r;
+ requires acc(left) && acc(right);
+ ensures valid;
+ ensures getLeft()==l;
+ ensures getRight()==r;
+ {
+ left := new Cell;
+ call left.init(l);
+ right := new Cell;
+ call right.init(r);
+ fold valid;
+ }
+
+ method setLeft(l: int)
+ requires valid;
+ requires 0<=l && l<=getRight();
+ ensures valid;
+ ensures getLeft()==l && getRight()==old(getRight());
+ {
+ unfold valid;
+ call left.set(l);
+ fold valid;
+ }
+
+ method setRight(r: int)
+ requires valid;
+ requires 0<=r && getLeft()<=r;
+ ensures valid;
+ ensures getLeft()==old(getLeft()) && getRight()==r;
+ {
+ unfold valid;
+ call right.set(r);
+ fold valid;
+ }
+
+ method shift(v: int)
+ requires valid;
+ requires 0<=v;
+ ensures valid;
+ ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;
+ {
+ unfold valid;
+ call left.set(left.get()+v);
+ call right.set(right.get()+v);
+ fold valid;
+ }
+
+ function getLeft() : int
+ requires valid;
+ {
+ unfolding valid in left.get()
+ }
+
+ function getRight() : int
+ requires valid;
+ {
+ unfolding valid in right.get()
+ }
+
+ predicate valid
+ {
+ acc(left) && acc(right) && left!=null && right!=null && left.valid && right.valid && left.get() <= right.get()
+ }
+}
+
+class Program module Main {
+ method main(){
+ var c1 := new Cell;
+ call c1.init(5);
+ call c1.set(6);
+
+ var c2 := new Cell;
+ call c2.init(10);
+ call c2.set(11);
+
+ assert c1.get() == 6;
+ }
+
+ method main2(){
+ var c: Cell;
+
+ c := new Cell;
+ call c.init(0);
+ call c.dispose();
+
+ assert c.valid; // should fail
+ }
+
+ method main3() returns (rt: Cell)
+ ensures rt!=null && rt.valid && rt.get() == 0;
+ {
+ rt := new Cell;
+ call rt.init(0);
+ }
+
+ method main4() {
+ var c: Cell;
+
+ c := new Cell;
+ call c.init(0);
+ share c;
+
+ acquire c;
+ call c.set(1);
+ release c;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt new file mode 100644 index 00000000..3ca21dd2 --- /dev/null +++ b/Chalice/tests/examples/cell.output.txt @@ -0,0 +1,5 @@ +Verification of cell.chalice
+
+ 142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
+
+Boogie program verifier finished with 31 verified, 1 error
diff --git a/Chalice/tests/examples/counter.chalice b/Chalice/tests/examples/counter.chalice new file mode 100644 index 00000000..828cf005 --- /dev/null +++ b/Chalice/tests/examples/counter.chalice @@ -0,0 +1,152 @@ +class Counter {
+ var value: int;
+
+ invariant acc(value) && old(value)<=value;
+}
+
+class Program {
+
+ method main1(){
+ var counter := new Counter;
+ counter.value := 0;
+ share counter;
+
+ acquire counter;
+ var tmp1 := counter.value;
+ release counter;
+
+ acquire counter;
+ var tmp2 := counter.value;
+ release counter;
+
+ assert tmp1 <= tmp2;
+ }
+
+ method main2(){
+ var counter := new Counter;
+ counter.value := 0;
+ share counter;
+
+ acquire counter;
+ release counter;
+
+ call bar(counter);
+ }
+
+ method bar(c: Counter)
+ requires c!=null && acc(c.mu) && waitlevel << c.mu;
+ requires eval(c.release, acc(c.value) && 0<=c.value);
+ {
+ lock (c) {
+ assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
+ }
+ }
+
+ method main3() returns (counter: Counter)
+ lockchange counter;
+ {
+ counter := new Counter;
+ counter.value := 0;
+ share counter;
+ acquire counter;
+ call doRelease(counter, counter.value);
+ }
+
+ method doRelease(c: Counter, i: int)
+ requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
+ lockchange c;
+ {
+ release c; // ok, because of atAcquire conjunct in the precondition
+ }
+
+ method main4(){
+ var counter := new Counter;
+ counter.value := 0;
+ share counter;
+
+ acquire counter;
+ counter.value := counter.value - 1;
+ release counter; // error: should fail
+ }
+
+ method main5(){
+ var counter := new Counter;
+ counter.value := 10;
+ share counter;
+
+ call foo(counter);
+
+ unshare counter;
+ assert 10<=counter.value; // error: should fail
+ }
+
+ method foo(c: Counter)
+ 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;
+ {
+ acquire c;
+ unshare c;
+ c.value := 5;
+ share c;
+ acquire c;
+ }
+
+ method nestedGood0(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ lock (c) {
+ release c
+ acquire c
+ }
+ }
+
+ method nestedGood1(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ var t: Counter := c
+ lock (t) {
+ t := new Counter
+ share t
+ acquire t
+ } // this line releases the original value for t
+ release t
+ }
+
+ method nestedBad0(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ lock (c) {
+ release c
+ } // error: no longer holds c
+ }
+
+ method nestedBad1(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ lock (c) {
+ acquire c // error: already holds c
+ }
+ }
+
+ method nestedBad2(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ lock (c) {
+ lock (c) { // error: already holds c
+ }
+ }
+ }
+
+ method nestedBad3(c: Counter)
+ requires c != null && acc(c.mu) && waitlevel << c.mu;
+ {
+ var t: Counter := c
+ lock (t) {
+ release t
+ t := new Counter
+ share t
+ acquire t
+ } // error: this line attempts to release the original t
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt new file mode 100644 index 00000000..6fdd2d7c --- /dev/null +++ b/Chalice/tests/examples/counter.output.txt @@ -0,0 +1,10 @@ +Verification of counter.chalice
+
+ 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 target of the release statement might not be locked by the current thread.
+ 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 target of the release statement might not be locked by the current thread.
+
+Boogie program verifier finished with 24 verified, 6 errors
diff --git a/Chalice/tests/examples/dining-philosophers.chalice b/Chalice/tests/examples/dining-philosophers.chalice new file mode 100644 index 00000000..f4a7d1a6 --- /dev/null +++ b/Chalice/tests/examples/dining-philosophers.chalice @@ -0,0 +1,93 @@ +class Philosopher module Philosophers {
+ var left: Fork;
+ var right: Fork;
+
+ method init(f1: Fork, f2: Fork)
+ requires f1!=null && f2!=null;
+ requires acc(this.*);
+ ensures valid;
+ ensures getLeft()==f1 && getRight()==f2;
+ {
+ left := f1;
+ right := f2;
+ fold valid;
+ }
+
+ method run()
+ requires valid;
+ requires acc(getLeft().mu, 10);
+ requires acc(getRight().mu, 10);
+ 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) && waitlevel << getLeft().mu && waitlevel << getRight().mu && getLeft().mu << getRight().mu;
+ {
+ unfold valid;
+ acquire left;
+ acquire right;
+ //eat
+ release left;
+ release right;
+ fold valid;
+ }
+ }
+
+ function getLeft(): Fork
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in left
+ }
+
+ function getRight(): Fork
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in right
+ }
+
+ predicate valid {
+ acc(left) && acc(right) && left!=null && right!=null
+ }
+}
+
+class Fork module Dining {
+ invariant true;
+}
+
+class Program module Main {
+ method main(){
+ // create forks
+ var f1 := new Fork;
+ var f2 := new Fork;
+ var f3 := new Fork;
+
+ share f1;
+ share f2 above f1;
+ share f3 above f1, f2;
+
+ // create philosophers
+ var aristotle := new Philosopher;
+ call aristotle.init(f1, f2);
+
+ var plato := new Philosopher;
+ call plato.init(f2, f3);
+
+ var kant := new Philosopher;
+ call kant.init(f1, f3);
+
+ assert f2.mu << f3.mu;
+
+ // start eating
+ fork tk0 := aristotle.run();
+ fork tk1 := plato.run();
+ fork tk2 := kant.run();
+
+ // everyone's done
+ join tk0;
+ join tk1;
+ join tk2;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt new file mode 100644 index 00000000..2bf72597 --- /dev/null +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -0,0 +1,4 @@ +Verification of dining-philosophers.chalice
+
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/generate_reference.bat b/Chalice/tests/examples/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/generate_reference_all.bat b/Chalice/tests/examples/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/iterator.chalice b/Chalice/tests/examples/iterator.chalice new file mode 100644 index 00000000..fd5d0352 --- /dev/null +++ b/Chalice/tests/examples/iterator.chalice @@ -0,0 +1,150 @@ +class List module Collections {
+ var contents: seq<int>;
+
+ method init()
+ requires acc(contents);
+ ensures valid && size(100)==0;
+ {
+ contents := nil<int>;
+ fold valid;
+ }
+
+ method add(x: int)
+ requires valid;
+ ensures valid && size(100) == old(size(100)+1) && get(size(100)-1, 100) == x;
+ ensures forall i in [0..size(100)-1] :: get(i, 100) == old(get(i, 100));
+ {
+ unfold valid;
+ contents := contents ++ [x];
+ fold valid;
+ }
+
+ function get(index: int, f: int): int
+ requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));
+ ensures forall i in [1..f] :: get(index, f) == get(index, i);
+ {
+ unfolding acc(valid, f) in contents[index]
+ }
+
+ function size(f: int): int
+ requires 0<f && f<=100 && acc(valid, f);
+ ensures 0<=result;
+ ensures forall i in [1..f] :: size(f) == size(i);
+ {
+ unfolding acc(valid, f) in |contents|
+ }
+
+ predicate valid {
+ acc(contents)
+ }
+}
+
+class Iterator module Collections {
+ var list: List;
+ var index: int;
+ var frac: int;
+
+ method init(l: List, f: int)
+ requires 0<f && f<=100;
+ requires acc(list) && acc(index) && acc(frac);
+ requires l!=null;
+ requires acc(l.valid, f);
+ ensures valid;
+ ensures getList()==l;
+ ensures getFraction()==f;
+ {
+ list := l;
+ this.index := 0;
+ frac := f;
+ fold valid;
+ }
+
+ method next() returns (rt: int)
+ requires valid && hasNext();
+ ensures valid;
+ ensures getList()==old(getList());
+ ensures getFraction()==old(getFraction());
+ {
+ unfold valid;
+ rt := list.get(index, frac);
+ index := index + 1;
+ fold valid;
+ }
+
+ method dispose()
+ requires valid;
+ ensures acc(old(getList()).valid, old(getFraction()));
+ {
+ unfold valid;
+ }
+
+ function hasNext(): bool
+ requires valid;
+ {
+ unfolding valid in index<list.size(frac)
+ }
+
+ function getFraction(): int
+ requires valid;
+ ensures 0<result && result<=100;
+ {
+ unfolding valid in frac
+ }
+
+ function getList(): List
+ requires valid;
+ ensures getList()!=null;
+ {
+ unfolding valid in list
+ }
+
+ predicate valid
+ {
+ acc(list) && acc(index) && acc(frac) && 0<frac && frac<=100 && list!=null && acc(list.valid, frac) && 0<=index && index<=list.size(frac)
+ }
+}
+
+class Program module Main {
+ method main(){
+ var tmp: int;
+ //create a new list
+ var list := new List;
+ call list.init();
+ call list.add(5);
+ call list.add(6);
+
+ // create a new iterator
+ var iter1 := new Iterator;
+ assert list!=null; // needed here: triggering problem?
+ assert list.size(100)==2;
+ assert list.size(50)==2;
+ call iter1.init(list, 10);
+
+ // create a second iterator
+ var iter2 := new Iterator;
+ assert list!=null; // needed here: triggering problem?
+ call iter2.init(list, 10);
+
+ // iterate over the list
+ while(iter1.hasNext())
+ invariant iter1.valid && iter1.getList()==list && iter1.getFraction()==10;
+ {
+ call tmp := iter1.next();
+ }
+
+ // iterate over the list
+ while(iter2.hasNext())
+ invariant iter2.valid && iter2.getList()==list && iter2.getFraction()==10;
+ {
+ call tmp := iter2.next();
+ }
+
+ // dispose the iterators
+ call iter1.dispose();
+ call iter2.dispose();
+
+ // full access to the list
+ assert list.valid;
+ assert list.size(50)==2;
+ }
+}
diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt new file mode 100644 index 00000000..a03f7c0c --- /dev/null +++ b/Chalice/tests/examples/iterator.output.txt @@ -0,0 +1,4 @@ +Verification of iterator.chalice
+
+
+Boogie program verifier finished with 22 verified, 0 errors
diff --git a/Chalice/tests/examples/iterator2.chalice b/Chalice/tests/examples/iterator2.chalice new file mode 100644 index 00000000..4020ece3 --- /dev/null +++ b/Chalice/tests/examples/iterator2.chalice @@ -0,0 +1,134 @@ +/* Iterator pattern in Chalice. */
+
+class List module Collections {
+ var contents: seq<int>;
+
+ method init()
+ requires acc(contents);
+ ensures valid && size()==0;
+ {
+ contents := nil<int>;
+ fold valid;
+ }
+
+ method add(x: int)
+ requires valid;
+ ensures valid && size() == old(size()+1) && get(size()-1) == x; // I don't know why this happens.
+ ensures forall i in [0..size()-1] :: get(i) == old(get(i));
+ {
+ unfold valid;
+ contents := contents ++ [x];
+ fold valid;
+ }
+
+ function get(index: int): int
+ requires rd(valid) && 0<=index && index<size();
+ {
+ unfolding rd(valid) in contents[index]
+ }
+
+ function size(): int
+ requires rd(valid);
+ ensures 0<=result;
+ {
+ unfolding rd(valid) in |contents|
+ }
+
+ predicate valid {
+ acc(contents)
+ }
+}
+
+class Iterator module Collections {
+ var list: List;
+ var index: int;
+
+ method init(l: List)
+ requires acc(list) && acc(index);
+ requires l!=null;
+ requires acc(l.valid,rd(l.valid));
+ ensures valid;
+ ensures getList()==l;
+ {
+ list := l;
+ this.index := 0;
+ fold valid;
+ }
+
+ method next() returns (rt: int)
+ requires valid && hasNext();
+ ensures valid;
+ ensures getList()==old(getList());
+ {
+ unfold valid;
+ rt := list.get(index);
+ index := index + 1;
+ fold valid;
+ }
+
+ method dispose()
+ requires valid;
+ ensures acc(old(getList()).valid,rd(old(getList()).valid));
+ {
+ unfold valid;
+ }
+
+ function hasNext(): bool
+ requires valid;
+ {
+ unfolding valid in index<list.size()
+ }
+
+ function getList(): List
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in list
+ }
+
+ predicate valid
+ {
+ acc(list) && acc(index) && list!=null && rd(list.valid) && 0<=index && index<=list.size()
+ }
+}
+
+class Program module Main {
+ method main(){
+ var tmp: int;
+ //create a new list
+ var list := new List;
+ call list.init();
+ call list.add(5);
+ call list.add(6);
+
+ // create a new iterator
+ var iter1 := new Iterator;
+ call iter1.init(list);
+
+ // create a second iterator
+ var iter2 := new Iterator;
+ call iter2.init(list);
+
+ // iterate over the list
+ while(iter1.hasNext())
+ invariant iter1.valid && iter1.getList()==list;
+ {
+ call tmp := iter1.next();
+ }
+
+ // iterate over the list
+ while(iter2.hasNext())
+ invariant iter2.valid && iter2.getList()==list;
+ {
+ call tmp := iter2.next();
+ }
+
+ // dispose the iterators
+ call iter1.dispose();
+ call iter2.dispose();
+
+ // full access to the list
+ assert list.valid;
+ assert list.size()==2;
+ }
+}
diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt new file mode 100644 index 00000000..512a2e26 --- /dev/null +++ b/Chalice/tests/examples/iterator2.output.txt @@ -0,0 +1,4 @@ +Verification of iterator2.chalice
+
+
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Chalice/tests/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice new file mode 100644 index 00000000..acde86ab --- /dev/null +++ b/Chalice/tests/examples/linkedlist.chalice @@ -0,0 +1,61 @@ +/* Recursive implementation and specification of a linked list. */
+
+class Node {
+ var next: Node;
+ var value: int;
+
+ method init(v: int)
+ requires acc(next) && acc(value);
+ ensures valid && size() == 1;
+ {
+ next := null;
+ value := v;
+ fold this.valid;
+ }
+
+ method add(x: int)
+ requires valid;
+ ensures valid;
+ ensures size() == old(size())+1;
+ {
+ unfold this.valid;
+ if(next==null) {
+ var n : Node;
+ n := new Node;
+ call n.init(x);
+ next := n;
+ } else {
+ call next.add(x);
+ }
+ fold this.valid;
+ }
+
+ method addFirst(x: int) returns (rt: Node)
+ requires valid;
+ ensures rt!=null && rt.valid;
+ ensures rt.size() == old(size()) + 1;
+ {
+ var n: Node;
+ n := new Node;
+ n.value := x;
+ n.next := this;
+ fold n.valid;
+ rt := n;
+ }
+
+ function at(i: int): int
+ requires valid && 0<=i && i<size();
+ {
+ unfolding valid in i==0 ? value : next.at(i-1) // no warning anymore... fishy!
+ }
+
+ function size(): int
+ requires valid;
+ {
+ unfolding this.valid in (next!=null ? 1+ next.size() : 1)
+ }
+
+ predicate valid {
+ acc(next) && acc(value) && (next!=null ==> next.valid)
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt new file mode 100644 index 00000000..b164664d --- /dev/null +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -0,0 +1,5 @@ +Verification of linkedlist.chalice
+
+ 49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.
+
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Chalice/tests/examples/producer-consumer.chalice b/Chalice/tests/examples/producer-consumer.chalice new file mode 100644 index 00000000..25253bfb --- /dev/null +++ b/Chalice/tests/examples/producer-consumer.chalice @@ -0,0 +1,202 @@ +class Program {
+ method main(){
+ var buffer := new Queue;
+ call buffer.init();
+ share buffer;
+
+ var producer := new Producer;
+ call producer.init(buffer);
+ fork tkP := producer.run();
+
+ var consumer := new Consumer;
+ call consumer.init(buffer);
+ fork tkC := consumer.run();
+
+ join tkP;
+ join tkC;
+
+ acquire buffer;
+ unshare buffer;
+
+ var tmp := buffer.size();
+ }
+}
+
+class Producer module Producer {
+ var buffer: Queue;
+
+ method init(buff: Queue)
+ requires acc(buffer) && buff!=null;
+ ensures valid && getBuffer()==buff;
+ {
+ buffer := buff;
+ fold valid;
+ }
+
+ method run()
+ requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
+ ensures rd(old(getBuffer()).mu);
+ {
+ var tmp: int;
+
+ while(true)
+ invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
+ {
+ unfold valid;
+ acquire buffer;
+ call buffer.enqueue(5);
+ release buffer;
+ fold valid;
+ }
+ unfold valid;
+ }
+
+ function getBuffer(): Queue
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in buffer
+ }
+
+ predicate valid {
+ acc(buffer) && buffer!=null
+ }
+}
+
+class Consumer module Consumer {
+ var buffer: Queue;
+
+ method init(buff: Queue)
+ requires acc(buffer) && buff!=null;
+ ensures valid && getBuffer()==buff;
+ {
+ buffer := buff;
+ fold valid;
+ }
+
+ method run()
+ requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
+ ensures rd(old(getBuffer()).mu);
+ {
+ while(true)
+ invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
+ {
+ unfold valid;
+ acquire buffer;
+ if(0<=buffer.size()){
+ call buffer.enqueue(5);
+ }
+ release buffer;
+ fold valid;
+ }
+ unfold valid;
+ }
+
+ function getBuffer(): Queue
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in buffer
+ }
+
+ predicate valid {
+ acc(buffer) && buffer!=null
+ }
+}
+
+class Queue module Queue {
+ var contents: List;
+
+ invariant valid;
+
+ method init()
+ requires acc(contents);
+ ensures valid;
+ ensures size()==0;
+ {
+ contents := new List;
+ call contents.init();
+ fold valid;
+ }
+
+ method enqueue(x: int)
+ requires valid;
+ ensures valid;
+ ensures size() == old(size())+1;
+ {
+ unfold valid;
+ call contents.add(x);
+ fold valid;
+ }
+
+ method dequeue() returns (rt: int)
+ requires valid && 0<size();
+ ensures valid;
+ ensures size() == old(size())-1;
+ {
+ unfold valid;
+ call rt := contents.removeFirst();
+ fold valid;
+ }
+
+ function size(): int
+ requires valid;
+ {
+ unfolding valid in contents.size()
+ }
+
+ predicate valid {
+ acc(contents) && contents!=null && contents.valid
+ }
+}
+
+class List module Collections {
+ var contents: seq<int>;
+
+ method init()
+ requires acc(contents);
+ ensures valid && size()==0;
+ {
+ contents := nil<int>;
+ fold valid;
+ }
+
+ method add(x: int)
+ requires valid;
+ ensures valid && size() == old(size()+1) && get(size()-1) == x;
+ ensures forall i in [0..size()-1] :: get(i) == old(get(i));
+ {
+ unfold valid;
+ contents := contents ++ [x];
+ fold valid;
+ }
+
+ method removeFirst() returns (rt: int)
+ requires valid && 0<size();
+ ensures valid && size() == old(size()-1);
+ ensures forall i in [0..size()] :: get(i) == old(get(i+1));
+ {
+ unfold valid;
+ rt := contents[0];
+ contents := contents[1..];
+ fold valid;
+ }
+
+
+ function get(index: int): int
+ requires rd(valid) && 0<=index && index<size();
+ {
+ unfolding rd(valid) in contents[index]
+ }
+
+ function size(): int
+ requires rd(valid);
+ ensures 0<=result;
+ {
+ unfolding rd(valid) in |contents|
+ }
+
+ predicate valid {
+ acc(contents)
+ }
+}
diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt new file mode 100644 index 00000000..ebf7c738 --- /dev/null +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -0,0 +1,4 @@ +Verification of producer-consumer.chalice
+
+
+Boogie program verifier finished with 36 verified, 0 errors
diff --git a/Chalice/tests/examples/prog0.chalice b/Chalice/tests/examples/prog0.chalice new file mode 100644 index 00000000..fb835a24 --- /dev/null +++ b/Chalice/tests/examples/prog0.chalice @@ -0,0 +1,109 @@ +class C {
+ method m() {
+ assert 4 + (a * 5) + (2 + 3) * (a + a);
+ a := a + 3;
+ b := a - b - c + 4 * d + 20 + --25;
+ b := ((((a - b) - c) + 4 * d) + 20) + --25;
+ c := a - (b - (c + (4 * d + (20 + 25))));
+ assert (X ==> Y) ==> Z <==> A ==> B ==> C;
+ assume A && B && (C || D || E) && F;
+ var x;
+ var y := 12 + !(x.f.g).h - (!x).f + (!x.f);
+ var z := new C;
+ y := new D;
+ o.f := 5;
+ (a + b).y := new T;
+ reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;
+ reorder X ==> Y below x+5;
+ reorder o.f above this, null;
+ share o;
+ unshare o;
+ acquire o;
+ release o;
+ rd acquire o;
+ rd release o;
+ downgrade o;
+ var tok: token<C.m>;
+ fork tok := o.m();
+ join tok;
+ assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;
+ x := this.f;
+ call m(2,3,4);
+ call this.m(2,3,4);
+ call a,b,c := o.m();
+ call x := m(200);
+ reorder o above waitlevel;
+ }
+ method p(a,b,c) returns (x,y,z)
+ requires 8 + 2 == 10;
+ ensures 8 + 5 > 10;
+ requires x == y+1;
+ ensures old(x) < x;
+ {
+ if (x == 7) {
+ y := y + 1; z := z + 2;
+ } else if (x == 8) {
+ y := 2;
+ } else {
+ z := 10;
+ }
+ { // empty block
+ }
+ if (x == 9) { }
+ if (x == 10) { x := 10; } else { }
+ var n := 0;
+ while (n < 100) { n := n - 1; }
+ while (n != 0)
+ invariant n % 2 == 0;
+ invariant sqrt2 * sqrt2 == 2;
+ {
+ n := n - 2;
+ }
+ call v,x := s.M(65);
+ }
+}
+class D { }
+
+// ----- tests specifically of implicit locals in CALL and RECEIVE statements
+
+class ImplicitC {
+ var k: int;
+
+ method MyMethod() returns (x: int, y: ImplicitC)
+ requires acc(k)
+ ensures acc(y.k) && x < y.k
+ {
+ x := k - 15;
+ y := this;
+ }
+
+ method B0() {
+ var c := new ImplicitC;
+ call a, b := c.MyMethodX(); // error: method not found (so what is done with a,b?)
+ assert a < b.k;
+ }
+
+ method B1() {
+ var c := new ImplicitC;
+ call a, a := c.MyMethod(); // error: a occurs twice
+ assert a < b.k;
+ }
+
+ method D0() {
+ var ch := new Ch;
+ var c := new ImplicitC;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, b := chX; // error: channel not found (so what is done with a,b?)
+ assert a < b.k;
+ }
+
+ method D1() {
+ var ch := new Ch;
+ var c := new ImplicitC;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, a := ch; // error: a occurs twice
+ assert a < b.k;
+ }
+}
+
+channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;
diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/examples/prog0.output.txt new file mode 100644 index 00000000..7949fa88 --- /dev/null +++ b/Chalice/tests/examples/prog0.output.txt @@ -0,0 +1,146 @@ +Verification of prog0.chalice
+
+The program did not typecheck.
+3.17: undeclared member a in class C
+3.37: undeclared member a in class C
+3.41: undeclared member a in class C
+3.12: assert statement requires a boolean expression (found int)
+4.5: undeclared member a in class C
+4.10: undeclared member a in class C
+5.5: undeclared member b in class C
+5.10: undeclared member a in class C
+5.14: undeclared member b in class C
+5.18: undeclared member c in class C
+5.26: undeclared member d in class C
+6.5: undeclared member b in class C
+6.14: undeclared member a in class C
+6.18: undeclared member b in class C
+6.23: undeclared member c in class C
+6.32: undeclared member d in class C
+7.5: undeclared member c in class C
+7.10: undeclared member a in class C
+7.15: undeclared member b in class C
+7.20: undeclared member c in class C
+7.29: undeclared member d in class C
+8.13: undeclared member X in class C
+8.19: undeclared member Y in class C
+8.13: incorrect type of ==> LHS (expected bool, found int)
+8.19: incorrect type of ==> RHS (expected bool, found int)
+8.26: undeclared member Z in class C
+8.26: incorrect type of ==> RHS (expected bool, found int)
+8.33: undeclared member A in class C
+8.39: undeclared member B in class C
+8.45: undeclared member C in class C
+8.39: incorrect type of ==> LHS (expected bool, found int)
+8.45: incorrect type of ==> RHS (expected bool, found int)
+8.33: incorrect type of ==> LHS (expected bool, found int)
+9.12: undeclared member A in class C
+9.17: undeclared member B in class C
+9.12: incorrect type of && LHS (expected bool, found int)
+9.17: incorrect type of && RHS (expected bool, found int)
+9.23: undeclared member C in class C
+9.28: undeclared member D in class C
+9.23: incorrect type of || LHS (expected bool, found int)
+9.28: incorrect type of || RHS (expected bool, found int)
+9.33: undeclared member E in class C
+9.33: incorrect type of || RHS (expected bool, found int)
+9.39: undeclared member F in class C
+9.39: incorrect type of && RHS (expected bool, found int)
+11.21: undeclared member f in class int
+11.21: undeclared member g in class int
+11.21: undeclared member h in class int
+<undefined position>: not-expression requires boolean operand
+<undefined position>: incorrect type of + RHS (expected int, found bool)
+11.33: not-expression requires boolean operand
+11.33: undeclared member f in class bool
+11.43: undeclared member f in class int
+11.42: not-expression requires boolean operand
+11.42: incorrect type of + RHS (expected int, found bool)
+13.5: type mismatch in assignment, lhs=int rhs=D
+14.5: undeclared member o in class C
+14.5: undeclared member f in class int
+15.6: undeclared member a in class C
+15.10: undeclared member b in class C
+15.5: undeclared member y in class int
+15.18: undefined class or channel T used in new expression
+16.19: undeclared member O in class C
+16.14: == requires operands of the same type, found int and bool
+16.31: undeclared member O in class C
+16.13: != requires operands of the same type, found bool and int
+16.13: object in reorder statement must be of a reference type (found bool)
+16.41: undeclared member a in class C
+16.41: install bound must be of a reference type or Mu type (found int)
+16.43: undeclared member b in class C
+16.43: install bound must be of a reference type or Mu type (found int)
+16.45: undeclared member c in class C
+16.45: install bound must be of a reference type or Mu type (found int)
+16.51: install bound must be of a reference type or Mu type (found int)
+16.53: install bound must be of a reference type or Mu type (found int)
+17.13: undeclared member X in class C
+17.19: undeclared member Y in class C
+17.13: incorrect type of ==> LHS (expected bool, found int)
+17.19: incorrect type of ==> RHS (expected bool, found int)
+17.13: object in reorder statement must be of a reference type (found bool)
+17.27: install bound must be of a reference type or Mu type (found int)
+18.13: undeclared member o in class C
+18.13: undeclared member f in class int
+18.13: object in reorder statement must be of a reference type (found int)
+19.11: undeclared member o in class C
+19.11: object in share statement must be of a reference type (found int)
+20.13: undeclared member o in class C
+20.13: object in unshare statement must be of a reference type (found int)
+21.13: undeclared member o in class C
+21.13: object in acquire statement must be of a reference type (found int)
+22.13: undeclared member o in class C
+22.13: object in release statement must be of a reference type (found int)
+23.16: undeclared member o in class C
+23.16: object in rd acquire statement must be of a reference type (found int)
+24.16: undeclared member o in class C
+24.16: object in rd release statement must be of a reference type (found int)
+25.15: undeclared member o in class C
+25.15: object in downgrade statement must be of a reference type (found int)
+27.17: undeclared member o in class C
+27.5: call of undeclared member m in class int
+27.10: wrong token type
+29.12: rd expression is allowed only in positive predicate contexts
+29.15: undeclared member x in class C
+29.20: acc expression is allowed only in positive predicate contexts
+29.24: undeclared member y in class C
+29.12: incorrect type of + LHS (expected int, found bool)
+29.20: incorrect type of + RHS (expected int, found bool)
+29.29: acc expression is allowed only in positive predicate contexts
+29.33: undeclared member z in class C
+29.29: incorrect type of + RHS (expected int, found bool)
+29.51: undeclared member k in class C
+29.57: undeclared member f in class null
+29.12: assert statement requires a boolean expression (found int)
+30.10: undeclared member f in class C
+31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
+32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
+33.19: undeclared member o in class C
+33.5: call of undeclared member m in class int
+34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
+34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
+35.13: undeclared member o in class C
+35.13: object in reorder statement must be of a reference type (found int)
+58.17: undeclared member sqrt2 in class C
+58.25: undeclared member sqrt2 in class C
+62.17: undeclared member s in class C
+62.5: call of undeclared member M in class int
+82.5: call of undeclared member MyMethodX in class ImplicitC
+83.12: undefined local variable a
+83.16: undefined local variable b
+83.16: undeclared member k in class int
+88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+88.13: duplicate actual out-parameter: a
+89.16: undeclared member b in class ImplicitC
+89.16: undeclared member k in class int
+96.21: undeclared member chX in class ImplicitC
+96.5: receive expression (which has type int) does not denote a channel
+97.12: undefined local variable a
+97.16: undefined local variable b
+97.16: undeclared member k in class int
+104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+104.16: duplicate actual out-parameter: a
+105.16: undeclared member b in class ImplicitC
+105.16: undeclared member k in class int
diff --git a/Chalice/tests/examples/prog1.chalice b/Chalice/tests/examples/prog1.chalice new file mode 100644 index 00000000..133de36d --- /dev/null +++ b/Chalice/tests/examples/prog1.chalice @@ -0,0 +1,86 @@ +// 7 errors expected
+
+class C {
+ var x: int;
+ invariant acc(x) && 0 <= x;
+
+ method seq0() returns (r: int)
+ {
+ r := x; // error: cannot access this.x here (90)
+ }
+ method seq1() returns (r: int)
+ requires acc(x);
+ {
+ r := x;
+ }
+ method seq2() returns (r: int)
+ requires rd(x);
+ {
+ r := x;
+ }
+ method seq3() returns (r: int)
+ requires rd(x);
+ {
+ r := x;
+ x := x + 1; // error: cannot write to this.x here (184)
+ }
+
+ method main0()
+ {
+ var c := new C;
+ c.x := 0;
+ share c;
+ var t := c.x; // error: cannot access c.x now (254)
+ }
+ method main1()
+ {
+ var c := new C;
+ c.x := 2;
+ share c;
+ acquire c;
+ c.x := c.x - 1;
+ release c; // error: monitor invariant might not hold (362)
+ }
+ method main2()
+ {
+ var c := new C;
+ c.x := 2;
+ share c;
+ acquire c;
+ c.x := c.x + 1;
+ release c; // good!
+ }
+ method main3()
+ {
+ var c := new C;
+ c.x := 2;
+ share c;
+ rd acquire c;
+ var tmp := c.x + 1; // fine
+ c.x := tmp; // error: cannot write to c.x here (582)
+ rd release c;
+ }
+ method main4()
+ {
+ var c := new C;
+ c.x := 2;
+ share c;
+ acquire c;
+ c.x := c.x + 1;
+ unshare c;
+ c.x := c.x + 1;
+ }
+ method main5()
+ {
+ var c := new C;
+ unshare c; // error: cannot unshare an object that isn't shared (754)
+ }
+ method main6()
+ {
+ var c := new C;
+ c.x := 0;
+ share c; acquire c;
+ unshare c;
+ unshare c; // error: cannot unshare an object that isn't shared (862)
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt new file mode 100644 index 00000000..eb552ac2 --- /dev/null +++ b/Chalice/tests/examples/prog1.output.txt @@ -0,0 +1,11 @@ +Verification of prog1.chalice
+
+ 9.10: Location might not be readable.
+ 25.5: Location might not be writable
+ 33.14: Location might not be readable.
+ 42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
+ 60.5: Location might not be writable
+ 76.5: The target of the unshare statement might not be shared.
+ 84.5: The target of the unshare statement might not be shared.
+
+Boogie program verifier finished with 16 verified, 7 errors
diff --git a/Chalice/tests/examples/prog2.chalice b/Chalice/tests/examples/prog2.chalice new file mode 100644 index 00000000..55fe8ff5 --- /dev/null +++ b/Chalice/tests/examples/prog2.chalice @@ -0,0 +1,93 @@ +// 4 errors expected
+
+class C {
+ method M(x: int) returns (y: bool)
+ requires 0 <= x;
+ ensures y <==> x == 10;
+ {
+ y := true;
+ if (x != 10) { y := !y; }
+ }
+
+ method Caller0()
+ {
+ var b: bool;
+ call b := M(12);
+ assert !b;
+ call b := M(10);
+ assert b;
+ }
+ method Caller1()
+ {
+ var b: bool;
+ call b := M(11);
+ assert b; // error (258)
+ }
+
+ var F: int;
+
+ method P(n: int)
+ requires acc(F);
+ ensures F == old(F) + n; // error
+ {
+ F := F + n;
+ }
+ method Caller2()
+ requires acc(F);
+ {
+ var prev := F;
+ call P(2);
+ assert false; // succeeds because postcondition of P is not well-defined (i.e. we do not havoc this.F, so the verifier assumes the value is the same in pre and post)
+ }
+
+ method Q(n: int)
+ requires acc(F);
+ ensures acc(F) && F == old(F) + n;
+ {
+ F := F + n;
+ }
+ method Caller3()
+ requires acc(F);
+ ensures acc(F);
+ {
+ var prev := F;
+ call Q(2);
+ assert F == prev + 2;
+ }
+}
+
+class Consts {
+ method M0() returns (z: int)
+ ensures z == 5
+ {
+ const a := 5
+ z := a
+ }
+ method M1() {
+ ghost const a
+ a := 5
+ }
+ method M2() {
+ ghost const a
+ a := 5
+ a := 5 // error (569)
+ }
+ method M3(b: bool) {
+ ghost const a
+ if (b) { a := 5 }
+ assert a < 10 // error (611)
+ }
+ method M4(b: bool) {
+ ghost const a
+ if (b) { a := 5 }
+ ghost var x := a
+ if (!b) { a := 7 }
+ assert a < 10
+ assert b ==> x == 5 // cool, huh?
+ }
+ method M5(b: bool) {
+ ghost const a
+ if (b) { a := 5 }
+ assert assigned(a) ==> a == 5
+ }
+}
diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt new file mode 100644 index 00000000..1581039d --- /dev/null +++ b/Chalice/tests/examples/prog2.output.txt @@ -0,0 +1,8 @@ +Verification of prog2.chalice
+
+ 24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
+ 31.13: Location might not be readable.
+ 73.5: Const variable can be assigned to only once.
+ 78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.
+
+Boogie program verifier finished with 24 verified, 4 errors
diff --git a/Chalice/tests/examples/prog3.chalice b/Chalice/tests/examples/prog3.chalice new file mode 100644 index 00000000..de5dfad7 --- /dev/null +++ b/Chalice/tests/examples/prog3.chalice @@ -0,0 +1,246 @@ +// 4 errors expected
+
+class Main {
+ method A() {
+ var d := new Data;
+ call d.Init();
+ share d;
+
+ var t0: T := new T; t0.d := d;
+ share t0 between waitlevel and d
+ var t1: T := new T; t1.d := d;
+ share t1 between waitlevel and d
+
+ var t0Token: token<T.run>;
+ fork t0Token := t0.run();
+ var t1Token: token<T.run>;
+ fork t1Token := t1.run();
+
+ join t0Token; acquire t0; unshare t0;
+ join t1Token; acquire t1; unshare t1;
+
+ acquire d; unshare d;
+ assert 0 <= d.x && d.x < 100;
+ }
+
+ method B() returns (r: U)
+ lockchange r;
+ {
+ var u := new U;
+ share u;
+
+ var uToken: token<U.run>;
+ fork uToken := u.run();
+
+ acquire u; // a little unusual to acquire after a fork, but allowed
+ assert waitlevel == u.mu;
+
+ var v := new U;
+ share v; acquire v; // this line has the effect of increasing waitlevel
+
+ assert waitlevel == v.mu;
+ assert waitlevel != u.mu;
+ assert u << v;
+ assert u << waitlevel;
+
+ join uToken; // material for the smoke check
+ release u;
+ r := v;
+ }
+
+ method C()
+ ensures waitlevel == old(waitlevel);
+ {
+ var u := new U;
+ share u;
+ acquire u;
+ release u;
+ }
+
+ method Mx0()
+ {
+ }
+ method Mx1()
+ lockchange this
+ {
+ }
+ method MxCaller0()
+ ensures waitlevel == old(waitlevel);
+ {
+ }
+ method MxCaller1()
+ ensures waitlevel == old(waitlevel);
+ {
+ call Mx0();
+ }
+ method MxCaller2()
+ ensures waitlevel == old(waitlevel); // error
+ {
+ call Mx1();
+ } // error: missing lockchange
+
+ method D(u: U)
+ requires u != null && rd(u.mu) && waitlevel << u;
+ ensures waitlevel == old(waitlevel);
+ {
+ acquire u;
+ release u;
+ }
+}
+
+class Data {
+ var x: int;
+ invariant acc(x) && 0 <= x && x < 100;
+ method Init()
+ requires acc(x);
+ ensures acc(x) && x == 0;
+ {
+ x := 0;
+ }
+}
+
+class T {
+ var d: Data;
+ invariant rd(d) && d != null && rd(d.mu) && rd(this.mu) && this << d;
+ method run()
+ requires rd(mu) && waitlevel << this;
+ ensures rd(mu);
+ {
+ acquire this;
+ acquire d;
+ d.x := d.x + 1;
+ if (d.x == 100) { d.x := 0; }
+ release d;
+ release this;
+ }
+}
+
+class U {
+ method run()
+ requires rd(mu) && waitlevel << this;
+ ensures rd(mu);
+ {
+ }
+}
+
+// Tests that use OLD in postcondition of run:
+
+class X {
+ var k: int
+ var l: int
+
+ method inc()
+ requires acc(k)
+ ensures acc(k) && k == old(k) + 1
+ {
+ k := k + 1
+ }
+ method Client0() returns (y: int)
+ ensures y == 8
+ {
+ var x := new X
+ x.k := 17 x.l := 10
+ call x.inc()
+ assert x.k == 18 && x.l == 10
+ y := x.k - x.l
+ }
+
+ method run()
+ requires acc(k) && 0 <= k
+ ensures acc(k) && k == old(k) + 1
+ {
+ k := k + 1
+ }
+
+ method Client1() returns (y: int)
+ ensures y == 8
+ {
+ var x := new X
+ x.k := 17
+ x.l := 20
+ var xToken: token<X.run>;
+ fork xToken := x.run();
+ x.l := 10
+ join xToken
+ assert x.k == 18 && x.l == 10
+ y := x.k - x.l
+ }
+ method Client2(tk: token<X.run>, x: X) returns (z: int)
+ requires x!=null && tk!=null && acc(tk.joinable) && tk.joinable && eval(tk.fork x.run(), acc(x.k) && 0<=x.k);
+ ensures 1 <= z
+ {
+ join tk
+ z := x.k
+ assert 1<=x.k;
+ }
+}
+
+class ReadSharing {
+ var x: int
+
+ method Consume()
+ requires rd(x,1)
+ {
+ // skip
+ }
+
+ method Divulge() // bad
+ requires rd(x,1)
+ {
+ call Consume()
+ call Consume() // error: cannot share twice (1773)
+ }
+
+ method Communicates() // good
+ requires rd(x,3)
+ ensures rd(x,1)
+ {
+ call Consume()
+ call Consume()
+ }
+
+ method Gossips() // bad
+ requires rd(x,3)
+ ensures rd(x,1)
+ {
+ call Consume()
+ call Consume()
+ call Consume()
+ } // error: does not live up to postcondition (2015)
+
+ method Shares() // good
+ requires rd*(x)
+ ensures rd*(x)
+ {
+ call Consume()
+ call Consume()
+ call Consume()
+ }
+
+ method TeamPlayer(N: int) // good
+ requires 0<N && rd(x,N)
+ {
+ var n := N
+ while (1 < n)
+ invariant 0<n && rd(x,n)
+ {
+ n := n - 1
+ }
+ }
+
+ method Unselfish(N: int) // good
+ requires rd*(x)
+ ensures rd*(x)
+ {
+ var n := N
+ if (N == 173) {
+ call Unselfish(200)
+ }
+ while (0 < n)
+ invariant rd*(x)
+ {
+ call Consume()
+ n := n - 1
+ }
+ }
+}
diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt new file mode 100644 index 00000000..7537f222 --- /dev/null +++ b/Chalice/tests/examples/prog3.output.txt @@ -0,0 +1,8 @@ +Verification of prog3.chalice
+
+ 76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
+ 76.3: Method might lock/unlock more than allowed.
+ 191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x.
+ 202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x.
+
+Boogie program verifier finished with 51 verified, 4 errors
diff --git a/Chalice/tests/examples/prog4.chalice b/Chalice/tests/examples/prog4.chalice new file mode 100644 index 00000000..3c655c71 --- /dev/null +++ b/Chalice/tests/examples/prog4.chalice @@ -0,0 +1,53 @@ +class LoopTargets {
+ method M() returns (y) {
+ y := 0
+ while (y < 100) { y := y + 1 }
+ assert y == 0 // error (139)
+ }
+ method N() returns (t: LoopTargets)
+ lockchange t
+ {
+ t := new LoopTargets
+ share t
+ acquire t
+ var s := true
+ while (s)
+ lockchange t
+ {
+ release t // error: loop invariant does not say holds(t) (252)
+ s := false
+ }
+ }
+ method P() {
+ var t := new LoopTargets
+ share t
+ acquire t
+ var s := true
+ while (s)
+ invariant acc(t.mu) && waitlevel == t.mu
+ lockchange t
+ {
+ release t // error: loop invariant does not say holds(t) (414)
+ acquire t
+ s := false
+ }
+ release t
+ }
+ method Q() {
+ var t := new LoopTargets
+ share t
+ acquire t
+ var s := true
+ while (s)
+ invariant rd(t.mu)
+ invariant holds(t) && waitlevel == t.mu
+ lockchange t
+ {
+ release t
+ acquire t
+ s := false
+ }
+ assert holds(t) // there we are
+ release t
+ }
+}
diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt new file mode 100644 index 00000000..950c2277 --- /dev/null +++ b/Chalice/tests/examples/prog4.output.txt @@ -0,0 +1,11 @@ +Verification of prog4.chalice
+
+ 5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
+ 17.7: The target of the release statement might not be locked by the current thread.
+ 17.7: Release might fail because the current thread might hold the read lock.
+ 30.7: The target of the release statement might not be locked by the current thread.
+ 30.7: Release might fail because the current thread might hold the read lock.
+ 34.5: The target of the release statement might not be locked by the current thread.
+ 34.5: Release might fail because the current thread might hold the read lock.
+
+Boogie program verifier finished with 6 verified, 7 errors
diff --git a/Chalice/tests/examples/quantifiers.chalice b/Chalice/tests/examples/quantifiers.chalice new file mode 100644 index 00000000..7377ca3f --- /dev/null +++ b/Chalice/tests/examples/quantifiers.chalice @@ -0,0 +1,59 @@ +class A { + var f: int; +} + +class Quantifiers { + var bamboo: seq<A>; + + method test1(a: seq<int>, b: int) + requires b in a; + requires b > 0; + { + assert exists j in a :: true && j > 0; + assert exists j:int :: 0 <= j && j < |a| && a[j] > 0; + assert forall j in a :: exists k in a :: k > 0; + } + + method test2(a: seq<A>) + requires rd(a[*].*); + requires |a| > 0; + requires forall i in a :: i != null && i.f > 0; + { + assert a[0].f > 0; + assert forall j: A :: j in a && j != null ==> j.f > 0; + assert exists j: A :: j in a && j != null && j.f > 0; + } + + method test3(a: seq<A>) + requires |a| > 0; + requires acc(a[*].f); + { + var c := new A; + assert c != a[0]; + } +} + +class Functions { + var x: int; + var y: int; + + function test1(): int + requires acc(this.*); + { + x + y + } + + function test2(): int + requires acc(x) && acc(y); + { + x + y + } + + function test3(a: seq<A>): int + requires acc(a[*].f); + requires forall x in a :: x != null; + requires forall i,j in [0..|a|] :: i != j ==> a[i] != a[j]; + { + |a| == 0 ? 0 : a[0].f + test3(a[1..]) + } +} diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt new file mode 100644 index 00000000..20b0af7b --- /dev/null +++ b/Chalice/tests/examples/quantifiers.output.txt @@ -0,0 +1,5 @@ +Verification of quantifiers.chalice
+
+ 57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
+
+Boogie program verifier finished with 11 verified, 1 error
diff --git a/Chalice/tests/examples/reg_test.bat b/Chalice/tests/examples/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/reg_test_all.bat b/Chalice/tests/examples/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/swap.chalice b/Chalice/tests/examples/swap.chalice new file mode 100644 index 00000000..46a6a71a --- /dev/null +++ b/Chalice/tests/examples/swap.chalice @@ -0,0 +1,20 @@ +class C {
+ method m(a, b) returns (x, y)
+ ensures x == a && y == b;
+ {
+ x := a;
+ y := b;
+ }
+
+ var F;
+ var G;
+ method n()
+ requires acc(F) && acc(this.G);
+ ensures acc(F) && acc(G);
+ ensures F == old(G) && G == old(F);
+ {
+ var tmp := F;
+ F := G;
+ G := tmp;
+ }
+}
diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt new file mode 100644 index 00000000..29df3021 --- /dev/null +++ b/Chalice/tests/examples/swap.output.txt @@ -0,0 +1,4 @@ +Verification of swap.chalice
+
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/examples/test.bat b/Chalice/tests/examples/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/examples/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
|