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 | |
| 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')
135 files changed, 7187 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" %*
diff --git a/Chalice/tests/permission-model/basic.chalice b/Chalice/tests/permission-model/basic.chalice new file mode 100644 index 00000000..53443a49 --- /dev/null +++ b/Chalice/tests/permission-model/basic.chalice @@ -0,0 +1,232 @@ +class Cell {
+ var x: int;
+
+ // dispose a read permission to x
+ method dispose_rd()
+ requires rd(x);
+ ensures true;
+ {
+ }
+
+ // return read permission
+ method void()
+ requires rd(x);
+ ensures rd(x);
+ {
+ }
+
+ // multiple calls to method that destroys rd(x)
+ method a1()
+ requires rd(x);
+ ensures true;
+ {
+ call dispose_rd();
+ call dispose_rd();
+ }
+
+ // call to method that destroys rd(x) really removes permission
+ method a2()
+ requires rd(x);
+ ensures rd(x);
+ {
+ call dispose_rd();
+ // ERROR: should fail to verify postcondition
+ }
+
+ // forking and method calls of dispose_rd
+ method a3()
+ requires rd(x);
+ ensures true;
+ {
+ fork dispose_rd();
+ call dispose_rd();
+ fork dispose_rd();
+ call dispose_rd();
+ }
+
+ // forking and method calls of dispose_rd
+ method a4()
+ requires rd(x);
+ ensures rd(x);
+ {
+ fork dispose_rd();
+ // ERROR: should fail to verify postcondition
+ }
+
+ // forking and method calls of dispose_rd
+ method a5()
+ requires rd(x);
+ ensures rd(x,1);
+ {
+ fork dispose_rd();
+ // OK: giving away an epsilon permission however should work
+ }
+
+ // forking and method calls of dispose_rd
+ method a6()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ fork dispose_rd();
+ // OK: giving away a 'undefined' read permission however should work
+ }
+
+ // multiple forks of dispose_rd
+ method a7()
+ requires rd(x);
+ ensures true;
+ {
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ fork dispose_rd();
+ }
+
+ // joining to regain permission
+ method a8(a: int)
+ requires rd(x);
+ ensures rd(x)
+ {
+ fork tk := void();
+ join tk;
+ }
+
+ // joining to regain permission
+ method a9(a: int)
+ requires rd(x);
+ ensures rd(x)
+ {
+ fork tk := dispose_rd();
+ join tk;
+ // ERROR: should fail to verify postcondition
+ }
+
+ // joining to regain permission
+ method a10(a: int)
+ requires rd(x);
+ ensures a == 3 ==> rd(x)
+ {
+ fork tk := void();
+ if (3 == a) {
+ join tk;
+ }
+ }
+
+ // finite loop of method calls, preserving rd(x)
+ method a11()
+ requires rd(x);
+ ensures rd(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant rd(x);
+ {
+ call void();
+ i := i+1;
+ }
+ }
+
+ // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a12(a: int)
+ requires rd(x);
+ ensures rd*(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < a)
+ invariant rd*(x);
+ {
+ fork dispose_rd();
+ i := i+1;
+ }
+ }
+
+ // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a13(a: int)
+ requires rd(x);
+ ensures rd(x);
+ {
+ var i: int;
+ i := 0;
+ while (i < a)
+ invariant rd*(x);
+ {
+ fork dispose_rd();
+ i := i+1;
+ }
+ // ERROR: should fail to verify postcondition
+ }
+
+ // calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+ method a14()
+ requires rd(x);
+ ensures true;
+ {
+ call dispose_rd();
+
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant rd*(x);
+ {
+ call dispose_rd();
+ i := i+1;
+ }
+ }
+
+ // return unknown permission
+ method a15()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ call dispose_rd();
+ }
+
+ // rd in loop invariant
+ method a16()
+ requires rd(x);
+ ensures rd*(x);
+ {
+ call dispose_rd();
+
+ var i: int;
+ i := 0;
+ while (i < 1000)
+ invariant acc(x,rd);
+ {
+ call void();
+ i := i+1;
+ }
+ }
+
+ // rd in method contracts
+ method a17()
+ requires acc(x,rd);
+ {
+ call dispose_rd();
+ call a17();
+ }
+
+ // multiple rd in method contracts
+ method a18()
+ requires rd(x);
+ ensures rd(x)
+ {
+ call a18a()
+ call a18b()
+ }
+ method a18a()
+ requires acc(x,2*rd);
+ ensures acc(x,rd+rd);
+ {
+ }
+ method a18b()
+ requires acc(x,rd+rd);
+ ensures acc(x,rd*2);
+ {
+ }
+
+}
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt new file mode 100644 index 00000000..510ae7f5 --- /dev/null +++ b/Chalice/tests/permission-model/basic.output.txt @@ -0,0 +1,8 @@ +Verification of basic.chalice
+
+ 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
+ 48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
+ 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
+ 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.
+
+Boogie program verifier finished with 41 verified, 4 errors
diff --git a/Chalice/tests/permission-model/channels.chalice b/Chalice/tests/permission-model/channels.chalice new file mode 100644 index 00000000..6a4961cd --- /dev/null +++ b/Chalice/tests/permission-model/channels.chalice @@ -0,0 +1,45 @@ +class C {
+ var f: int;
+
+ method t1(ch: C1)
+ requires ch != null && rd(f);
+ ensures true;
+ {
+ send ch(this) // ERROR
+ }
+
+ method t2(ch: C1)
+ requires ch != null && acc(f);
+ ensures true;
+ {
+ send ch(this)
+ }
+
+ method t3(ch: C2)
+ requires ch != null && rd(f);
+ ensures rd(f);
+ {
+ send ch(this)
+ // ERROR: should fail to verify postcondition
+ }
+
+ method t4(ch: C1, a: C) returns (b: C)
+ requires ch != null && credit(ch, 1) && rd(ch.mu) && waitlevel << ch;
+ ensures rd*(b.f);
+ {
+ receive b := ch
+ }
+
+ method t5(ch: C1)
+ requires ch != null && acc(f,1);
+ ensures true;
+ {
+ send ch(this)
+ send ch(this)
+ send ch(this)
+ }
+
+}
+
+channel C1(x: C) where rd(x.f);
+channel C2(x: C) where rd*(x.f);
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt new file mode 100644 index 00000000..11543925 --- /dev/null +++ b/Chalice/tests/permission-model/channels.output.txt @@ -0,0 +1,6 @@ +Verification of channels.chalice
+
+ 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.
+ 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.
+
+Boogie program verifier finished with 11 verified, 2 errors
diff --git a/Chalice/tests/permission-model/generate_reference.bat b/Chalice/tests/permission-model/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/generate_reference_all.bat b/Chalice/tests/permission-model/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/locks.chalice b/Chalice/tests/permission-model/locks.chalice new file mode 100644 index 00000000..5107fd38 --- /dev/null +++ b/Chalice/tests/permission-model/locks.chalice @@ -0,0 +1,146 @@ +class Cell {
+ var x: int;
+
+ // use starred read permission
+ invariant rd*(x);
+
+ method a1(c: Cell)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd*(c.x));
+
+ release c;
+ assert(rd*(c.x));
+ }
+
+ method a2(c: Cell)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd(c.x)); // ERROR: should fail
+
+ release c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a3()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ assert(rd*(c.x));
+
+ acquire c;
+ unshare c;
+ assert(rd*(c.x));
+ }
+
+ method a4()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a5()
+ {
+ var c: Cell := new Cell;
+
+ share c;
+ acquire c;
+ unshare c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+}
+
+
+class Cell2 {
+ var x: int;
+
+ // use normal fractional permission
+ invariant rd(x);
+
+ method a1(c: Cell2)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd*(c.x));
+
+ release c;
+ assert(rd*(c.x)); // ERROR: we gave away all permission
+ }
+
+ method a2(c: Cell2)
+ requires c != null && rd(c.mu) && waitlevel << c;
+ {
+ acquire c;
+ assert(rd(c.x)); // ERROR: should fail
+
+ release c;
+ assert(rd(c.x)); // ERROR: should fail
+ }
+
+ method a3()
+ {
+ var c: Cell2 := new Cell2;
+
+ share c;
+ assert(rd*(c.x));
+
+ call void(c);
+ assert(rd*(c.x));
+
+ call dispose(c);
+ assert(rd*(c.x));
+
+ acquire c;
+ unshare c;
+ assert(rd*(c.x));
+
+ assert(acc(c.x)); // ERROR: should fail
+ }
+
+ method a4(c: Cell2)
+ requires c != null && acc(c.mu) && holds(c);
+ requires rd(c.x);
+ lockchange c
+ {
+ release c; // ERROR: should fail, we don't have enough permission
+ }
+
+ method a5()
+ {
+ var c: Cell2 := new Cell2;
+
+ share c;
+ acquire c;
+ assert(acc(c.x));
+
+ unshare c;
+ assert(acc(c.x));
+ }
+
+ method a6(c: Cell2)
+ requires acc(c.x,rd(c)) && acc(c.mu) && c.mu == lockbottom
+ {
+ var n: int;
+
+ share c;
+ rd acquire c;
+ n := c.x
+ rd release c;
+
+ n := c.x // ERROR: no read access possible
+
+ acquire c;
+ unshare c;
+ }
+
+ method void(c: Cell2) requires rd(c.x); ensures rd(c.x); {}
+
+ method dispose(c: Cell2) requires rd(c.x); {}
+
+}
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt new file mode 100644 index 00000000..c1167c3b --- /dev/null +++ b/Chalice/tests/permission-model/locks.output.txt @@ -0,0 +1,14 @@ +Verification of locks.chalice
+
+ 21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
+ 24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
+ 44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x.
+ 54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x.
+ 73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x.
+ 80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x.
+ 83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x.
+ 103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x.
+ 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x.
+ 136.10: Location might not be readable.
+
+Boogie program verifier finished with 20 verified, 10 errors
diff --git a/Chalice/tests/permission-model/peculiar.chalice b/Chalice/tests/permission-model/peculiar.chalice new file mode 100644 index 00000000..31c4d259 --- /dev/null +++ b/Chalice/tests/permission-model/peculiar.chalice @@ -0,0 +1,55 @@ +class Cell {
+ var x: int;
+
+ invariant rd(x);
+
+ method t1()
+ requires acc(x);
+ ensures rd(x) && rd(x);
+ {
+ }
+
+ method t2()
+ requires acc(x,1);
+ ensures rd(x);
+ {
+ call void();
+ }
+
+ method t3()
+ requires rd(x);
+ {
+ call t3helper();
+ }
+
+ method t3helper()
+ requires rd(x) && rd(x);
+ ensures rd(x) && rd(x);
+ {}
+
+ method t4()
+ requires rd(x);
+ {
+ call dispose();
+ call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
+ assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
+ }
+
+ method t5(n: int)
+ requires acc(x);
+ {
+ var i: int := 0;
+ call req99();
+ while (i < n)
+ invariant rd*(x);
+ {
+ call dispose();
+ i := i+1
+ }
+ }
+
+ method dispose() requires rd(x); {}
+ method void() requires rd(x); ensures rd(x); {}
+ method req99() requires acc(x,99); {}
+
+}
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt new file mode 100644 index 00000000..fd3c0a76 --- /dev/null +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -0,0 +1,5 @@ +Verification of peculiar.chalice
+
+ 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x.
+
+Boogie program verifier finished with 18 verified, 1 error
diff --git a/Chalice/tests/permission-model/permarith_parser.chalice b/Chalice/tests/permission-model/permarith_parser.chalice new file mode 100644 index 00000000..5b011d79 --- /dev/null +++ b/Chalice/tests/permission-model/permarith_parser.chalice @@ -0,0 +1,37 @@ +class Cell {
+ var x: int;
+ var y: Cell;
+
+ method a1()
+ requires acc(x,y); // ERROR: amount is not integer
+ {
+ }
+
+ method a2()
+ requires acc(x,n); // ERROR: unknown variable
+ {
+ }
+
+ method a3()
+ requires acc(x,rd(rd(1))); // ERROR: invalid permission expression
+ {
+ }
+
+ method a4()
+ requires acc(x,rd*(y)); // ERROR: invalid permission expression
+ {
+ }
+
+ method a5()
+ requires acc(x,rd(this.mu)); // ERROR: invalid type inside rd
+ requires acc(x,rd(null)); // ERROR: invalid type inside rd
+ requires acc(x,rd(true)); // ERROR: invalid type inside rd
+ {
+ }
+
+ method a6()
+ requires acc(x,rd(x)*rd(x)); // ERROR: permission multiplication not allowed
+ {
+ }
+
+}
diff --git a/Chalice/tests/permission-model/permarith_parser.output.txt b/Chalice/tests/permission-model/permarith_parser.output.txt new file mode 100644 index 00000000..f124b714 --- /dev/null +++ b/Chalice/tests/permission-model/permarith_parser.output.txt @@ -0,0 +1,13 @@ +Verification of permarith_parser.chalice
+
+The program did not typecheck.
+6.14: fraction in permission must be of type integer
+11.20: undeclared member n in class Cell
+16.26: permission not expected here.
+16.26: type $Permission is not supported inside a rd expression.
+21.20: rd expression is allowed only in positive predicate contexts
+21.14: expression of type bool invalid in permission
+26.20: type $Mu of variable mu is not supported inside a rd expression.
+27.23: type null is not supported inside a rd expression.
+28.23: type bool is not supported inside a rd expression.
+33.14: multiplication of permission amounts not supported
diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice new file mode 100644 index 00000000..94cf30a3 --- /dev/null +++ b/Chalice/tests/permission-model/permission_arithmetic.chalice @@ -0,0 +1,193 @@ +class Cell {
+ var x: int;
+ var i: int;
+ var y: Cell;
+
+ invariant rd(x);
+
+ predicate valid { rd(x) }
+
+ method a1(n: int) // test various arithmetic operations on permissions
+ requires acc(x,1+1) && acc(x,1) && acc(x,3) && acc(x,1-rd(5-7)+rd(3)) && rd(x) && rd(this.y);
+ ensures acc(x,100-97);
+ {
+ }
+
+ method a2(n: int)
+ requires acc(x,1-rd(1)-2);
+ {
+ assert false; // this should verify, as the precondition contains an invalid permission
+ }
+
+ method a3(n: int)
+ {
+ assert acc(x,1-rd(1)-2); // ERROR: invalid (negative) permission
+ }
+
+ method a4(n: int)
+ requires acc(x,rd(n));
+ {
+ }
+
+ method a5(n: int)
+ requires acc(x,rd(n)-rd(2));
+ {
+ }
+
+ method a6()
+ requires acc(x);
+ {
+ call a5(1); // ERROR: n=1 makes the permission in the precondition negative
+ }
+
+ method a7(c: Cell)
+ requires acc(c.x,100-rd(c));
+ requires c != null && acc(c.mu) && waitlevel << c;
+ ensures acc(c.x);
+ {
+ acquire(c);
+ unshare(c);
+ }
+
+ method a8()
+ requires acc(x,100-rd(valid)) && valid;
+ ensures acc(x);
+ {
+ unfold valid;
+ }
+
+ method a9()
+ requires acc(x,rd(valid));
+ ensures valid;
+ {
+ fold valid;
+ }
+
+ method a10()
+ requires valid;
+ ensures acc(x,rd(valid));
+ {
+ unfold valid;
+ }
+
+ method a11() // ERROR: postcondition does not hold (not enough permission)
+ requires valid;
+ ensures acc(x);
+ {
+ unfold valid;
+ }
+
+ method a12()
+ requires rd(this.i) && this.i > 0 && acc(x,rd(this.i));
+ ensures rd(this.i) && this.i > 0 && acc(x,rd(i));
+ {
+ }
+
+ method a13(i: int) // ERROR: postcondition does not hold
+ requires rd(this.i) && this.i > 0 && i > 0 && acc(x,rd(this.i));
+ ensures i > 0 && acc(x,rd(i));
+ {
+ }
+
+ method a14()
+ requires acc(y) && this.y == this; // test aliasing
+ requires acc(x,100-rd(y));
+ requires y != null && acc(this.mu) && waitlevel << this;
+ ensures acc(x);
+ lockchange this;
+ {
+ acquire this;
+ }
+
+ method a15()
+ requires acc(x,rd(this.i)); // ERROR: this.i is not readable
+ ensures acc(x,rd(this.i));
+ {
+ }
+
+ method a16()
+ requires acc(x,rd(this.y)); // ERROR: this.y is not readable
+ ensures acc(x,rd(this.y));
+ {
+ }
+
+ method a17(tk: token<Cell.void>)
+ requires acc(x,100-rd(tk)) && acc(tk.joinable) && tk.joinable;
+ requires eval(tk.fork this.void(),true);
+ ensures acc(x);
+ {
+ join tk;
+ }
+
+ method a18()
+ requires acc(x,rd+rd-rd+10*rd-rd*(5+5))
+ ensures rd(x)
+ {
+ call void();
+ }
+
+ method a19()
+ requires acc(x)
+ requires acc(this.mu) && lockbottom == this.mu
+ ensures acc(x)
+ lockchange this;
+ {
+ share this;
+ acquire this;
+ unshare this;
+ }
+
+ method a20()
+ requires rd(x)
+ requires acc(this.mu) && lockbottom == this.mu
+ lockchange this;
+ {
+ share this; // ERROR: not enough permission
+ }
+
+ method a21()
+ requires acc(x,rd*2)
+ ensures rd(x) && rd(x)
+ {
+ assert acc(x,rd+rd)
+ assert acc(x,(1+1)*rd)
+ }
+
+ method a22()
+ requires acc(x,1*2*5)
+ ensures acc(x,10)
+ {
+ }
+
+ method a23(c: Cell) // ERROR: permission in postcondition not positive
+ requires acc(x,rd-rd(c))
+ ensures acc(x,rd(c)-rd)
+ {
+ }
+
+ method a24()
+ requires rd*(x)
+ requires rd*(x)
+ {
+ }
+
+ method a25() // ERROR: postcondition does not hold, possibly not enough permission
+ requires rd*(x)
+ ensures acc(x,rd)
+ {
+ }
+
+ // interaction of monitors and predicates
+ method a26()
+ requires acc(x,rd(this))
+ requires acc(mu) && lockbottom == this.mu
+ ensures valid
+ lockchange this
+ {
+ share this
+ acquire this
+ fold valid
+ }
+
+ method void() requires rd(x); ensures rd(x); {}
+}
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt new file mode 100644 index 00000000..f735cf85 --- /dev/null +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -0,0 +1,13 @@ +Verification of permission_arithmetic.chalice
+
+ 24.5: Assertion might not hold. The permission at 24.18 might not be positive.
+ 40.5: The precondition at 33.14 might not hold. The permission at 33.20 might not be positive.
+ 73.3: The postcondition at 75.13 might not hold. Insufficient fraction at 75.13 for Cell.x.
+ 86.3: The postcondition at 88.13 might not hold. Insufficient epsilons at 88.22 for Cell.x.
+ 103.20: Location might not be readable.
+ 109.20: Location might not be readable.
+ 145.5: Monitor invariant might not hold. Insufficient fraction at 6.13 for Cell.x.
+ 162.3: The postcondition at 164.13 might not hold. The permission at 164.19 might not be positive.
+ 174.3: The postcondition at 176.13 might not hold. Insufficient fraction at 176.13 for Cell.x.
+
+Boogie program verifier finished with 47 verified, 9 errors
diff --git a/Chalice/tests/permission-model/predicate_error1.chalice b/Chalice/tests/permission-model/predicate_error1.chalice new file mode 100644 index 00000000..0726e349 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error1.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3);
+ {
+ unfold rd(read3); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error1.output.txt b/Chalice/tests/permission-model/predicate_error1.output.txt new file mode 100644 index 00000000..d7964c29 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error1.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error1.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error2.chalice b/Chalice/tests/permission-model/predicate_error2.chalice new file mode 100644 index 00000000..cc8d7d28 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error2.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read1,1);
+ {
+ unfold rd(read1,1); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error2.output.txt b/Chalice/tests/permission-model/predicate_error2.output.txt new file mode 100644 index 00000000..cc580b7b --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error2.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error2.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error3.chalice b/Chalice/tests/permission-model/predicate_error3.chalice new file mode 100644 index 00000000..eb1d8777 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error3.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3,1);
+ {
+ unfold rd(read3,1); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error3.output.txt b/Chalice/tests/permission-model/predicate_error3.output.txt new file mode 100644 index 00000000..3e325f1b --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error3.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error3.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error4.chalice b/Chalice/tests/permission-model/predicate_error4.chalice new file mode 100644 index 00000000..0726e349 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error4.chalice @@ -0,0 +1,20 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- invalid permission scaling ---
+
+ method error()
+ requires rd(read3);
+ {
+ unfold rd(read3); // ERROR: scaling epsilons is not possible
+ }
+
+}
diff --git a/Chalice/tests/permission-model/predicate_error4.output.txt b/Chalice/tests/permission-model/predicate_error4.output.txt new file mode 100644 index 00000000..8cd03821 --- /dev/null +++ b/Chalice/tests/permission-model/predicate_error4.output.txt @@ -0,0 +1,3 @@ +Verification of predicate_error4.chalice
+
+Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicates.chalice b/Chalice/tests/permission-model/predicates.chalice new file mode 100644 index 00000000..1f752fda --- /dev/null +++ b/Chalice/tests/permission-model/predicates.chalice @@ -0,0 +1,103 @@ +class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // fractional read permission
+ predicate read2 { rd*(x) } // starred fractional read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- basic tests ---
+
+ method b1()
+ requires write1 && write2 && read1 && read2 && read3;
+ ensures write1 && write2 && read1 && read2 && read3;
+ {
+ }
+
+ method b2()
+ requires write1;
+ ensures read1;
+ {
+ unfold write1;
+ fold read1;
+ }
+
+ method b3()
+ requires read1;
+ ensures read3;
+ {
+ unfold read1;
+ fold read3;
+ fold read2;
+ fold read3;
+ fold read2;
+ fold write1; // ERROR: should fail
+ }
+
+ method b4()
+ requires read2;
+ ensures read2;
+ {
+ unfold read2;
+ call dispose();
+ fold read2;
+ }
+
+ method b5()
+ requires read1;
+ ensures read1;
+ {
+ unfold read1;
+ call dispose();
+ fold read1; // ERROR: should fail
+ }
+
+ method b6()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read1;
+ unfold read1;
+ }
+
+ method b7() // ERROR: precondition does not hold
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read2;
+ unfold read2;
+ }
+
+ method b8()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold read3;
+ unfold read3;
+ }
+
+ method b9()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold write1;
+ unfold write1;
+ }
+
+ method b10()
+ requires acc(x);
+ ensures acc(x);
+ {
+ fold write2;
+ unfold write2;
+ }
+
+ // --- helper functions ---
+
+ method void() requires rd(x); ensures rd(x); {}
+ method dispose() requires rd(x); {}
+
+}
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt new file mode 100644 index 00000000..be87e044 --- /dev/null +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -0,0 +1,7 @@ +Verification of predicates.chalice
+
+ 37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.
+ 55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.
+ 66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x.
+
+Boogie program verifier finished with 27 verified, 3 errors
diff --git a/Chalice/tests/permission-model/reg_test.bat b/Chalice/tests/permission-model/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/reg_test_all.bat b/Chalice/tests/permission-model/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice new file mode 100644 index 00000000..29930346 --- /dev/null +++ b/Chalice/tests/permission-model/scaling.chalice @@ -0,0 +1,89 @@ +/*
+
+Note: At the moment, there is a performance problem if permissions are scaled.
+If a predicate (such as read1 below) contains a read permission, and one takes
+read access to that predicate (as in method s1; rd(read1)), then this
+effectively means that the fractions corresponding to the two read permissions
+are multiplied. This introduces non-linear arithmetic in Boogie, which can be
+very hard and unpredicable for the theorem prover. For this reason, this test is
+taking a very long time to complete.
+
+-- Stefan Heule, June 2011
+
+*/
+
+class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // abstract read permission
+ predicate read2 { rd*(x) } // starred read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- permission scaling ---
+
+ method s1()
+ requires rd(read1);
+ {
+ unfold rd(read1);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
+ requires rd(read1);
+ ensures rd(read1);
+ {
+ unfold rd(read1);
+ fold rd(read1);
+ }
+
+ method s3()
+ requires acc(x);
+ ensures rd(read1);
+ {
+ fold rd(read1);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s4() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read1;
+ {
+ fold rd(read1);
+ }
+
+ method s5()
+ requires rd(read2);
+ {
+ unfold rd(read2);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s6()
+ requires acc(x);
+ ensures rd(read2);
+ {
+ fold rd(read2);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s7() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read2;
+ {
+ fold rd(read2);
+ }
+
+ // --- helper functions ---
+
+ method void() requires rd(x); ensures rd(x); {}
+ method dispose() requires rd(x); {}
+
+}
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt new file mode 100644 index 00000000..1ff1d596 --- /dev/null +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -0,0 +1,11 @@ +Verification of scaling.chalice
+
+ 33.5: Assertion might not hold. Insufficient fraction at 33.12 for Cell.x.
+ 36.3: The postcondition at 38.13 might not hold. Insufficient fraction at 38.13 for Cell.read1.
+ 50.5: Assertion might not hold. Insufficient fraction at 50.12 for Cell.x.
+ 53.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Cell.read1.
+ 65.5: Assertion might not hold. Insufficient fraction at 65.12 for Cell.x.
+ 74.5: Assertion might not hold. Insufficient fraction at 74.12 for Cell.x.
+ 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Cell.read2.
+
+Boogie program verifier finished with 17 verified, 7 errors
diff --git a/Chalice/tests/permission-model/sequences.chalice b/Chalice/tests/permission-model/sequences.chalice new file mode 100644 index 00000000..0560945d --- /dev/null +++ b/Chalice/tests/permission-model/sequences.chalice @@ -0,0 +1,85 @@ +class Program {
+ var x: int;
+
+ method a(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ assert rd(a[*].f);
+ call b(a);
+ }
+
+ method b(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ assert rd(a[*].f);
+ }
+
+ method c(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ call void(a[1]);
+ call void(a[0]);
+ }
+
+ method c1(a: seq<A>) // ERROR: should fail to verify postcondition
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd(a[*].f);
+ {
+ call dispose(a[1]);
+ }
+
+ method d(a: seq<A>)
+ requires |a| > 2;
+ requires rd(a[*].f);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd*(a[*].f);
+ {
+ call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
+
+ var x: int;
+ call x := some_number();
+ call dispose(a[x]); // slighly more interesting, but still clearly ok
+ }
+
+ method e(a: seq<A>) // ERROR: should fail to verify postcondition
+ requires |a| > 2;
+ requires acc(a[*].f,10);
+ requires forall i in [0..|a|-1] :: a[i] != null;
+ requires a[0].f == 1;
+ ensures rd*(a[*].f);
+ {
+ var x: int;
+ call x := some_number();
+ call dispose2(a[x]);
+ }
+
+ method some_number() returns (a: int)
+ ensures 0 <= a && a < 3;
+ {
+ a := 1;
+ }
+
+ method dispose(a: A) requires rd(a.f); {}
+ method dispose2(a: A) requires acc(a.f,10); {}
+ method void(a: A) requires rd(a.f); ensures rd(a.f); {}
+}
+
+class A {
+ var f: int;
+}
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt new file mode 100644 index 00000000..16dd9137 --- /dev/null +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -0,0 +1,6 @@ +Verification of sequences.chalice
+
+ 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
+ 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
+
+Boogie program verifier finished with 20 verified, 2 errors
diff --git a/Chalice/tests/permission-model/test.bat b/Chalice/tests/permission-model/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/permission-model/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt new file mode 100644 index 00000000..0e09fb57 --- /dev/null +++ b/Chalice/tests/readme.txt @@ -0,0 +1,39 @@ +
+Chalice Test Suite
+==================
+
+Contents
+--------
+- examples: Various examples how Chalice can be used to verify concurrent
+ programs.
+- permission-model: Regression tests for the permission model of Chalice.
+- refinements: Regression tests for the refinement extension.
+- test-scripts: Some batch scripts that can be used to execute the tests in an
+ easy and automated way. More information below.
+
+
+Test Scripts
+------------
+In the directory test-scripts are various scripts to allow the execution of the
+tests in different ways. There are launchers in the test directories (e.g. in
+examples or permission-model) to access them.
+
+Commands (sorted by relevance):
+- test.bat <file> [-params]: Execute a test and output the result of the
+ verification. Note: <file> must not include the file extension.
+- reg_test.bat <file> [-params]: Execute a tests as a regression test, i.e., run
+ the test and compare the verification result with the reference output stored
+ in <file.output.txt>. Also shows the differences if any.
+- reg_test_all.bat: Execute all tests as regression tests in the current
+ directory.
+- generete_reference.bat <file> [-params]: Generate the reference output.
+- generate_reference_all.bat: Generate reference files for all tests in the
+ current directory.
+- getboogieoutput.bat: File used internally by generete_reference.bat.
+
+
+Note: There is also an alternative way to execute the tests in example, namely
+to use the script test.bat. The scripts in test-scripts allow more fine-grained
+testing, but they do not allow to use special parameters for certain tests
+(e.g. -autoMagic).
+For the refinement tests, there is a bash script test.sh, similar to test.bat.
diff --git a/Chalice/tests/refinements/AngelicExec.chalice b/Chalice/tests/refinements/AngelicExec.chalice new file mode 100644 index 00000000..06ab9c83 --- /dev/null +++ b/Chalice/tests/refinements/AngelicExec.chalice @@ -0,0 +1,34 @@ +class A0 {
+ method m(b: bool) {
+ var x;
+ if (b) {
+ var x [0 <= x && x < 3];
+ } else {
+ x := 1;
+ }
+ }
+}
+
+class B0 refines A0 {
+ refines m(b: bool) {
+ var x := 1;
+ }
+}
+
+class A1 refines A0 {
+ transforms m(b: bool) {
+ _
+ if {
+ replaces * by {x := 1;}
+ } else {
+ *
+ }
+ _
+ }
+}
+
+class A2 refines A1 {
+ refines m(b: bool) {
+ var x := 1;
+ }
+}
diff --git a/Chalice/tests/refinements/Answer b/Chalice/tests/refinements/Answer new file mode 100644 index 00000000..8bd8a24b --- /dev/null +++ b/Chalice/tests/refinements/Answer @@ -0,0 +1,45 @@ +Processing LoopSqRoot.chalice + +Boogie program verifier finished with 9 verified, 0 errors +Processing RecSqRoot.chalice + +Boogie program verifier finished with 11 verified, 0 errors +Processing SpecStmt.chalice + 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true. + 25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true. + 33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true. + +Boogie program verifier finished with 4 verified, 3 errors +Processing SumCubes.chalice + +Boogie program verifier finished with 6 verified, 0 errors +Processing TestTransform.chalice + +Boogie program verifier finished with 10 verified, 0 errors +Processing TestRefines.chalice + 28.5: Refinement may produce different value for pre-state local variable: c + +Boogie program verifier finished with 14 verified, 1 error +Processing RecFiniteDiff.chalice + +Boogie program verifier finished with 9 verified, 0 errors +Processing LoopFiniteDiff.chalice + +Boogie program verifier finished with 12 verified, 0 errors +Processing Pick.chalice + 26.25: Sequence index might be larger than or equal to the length of the sequence. + +Boogie program verifier finished with 11 verified, 1 error +Processing TestCoupling.chalice + 35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y. + 62.38: Location might not be readable. + 66.5: Location might not be writable + +Boogie program verifier finished with 17 verified, 3 errors +Processing Calculator.chalice + +Boogie program verifier finished with 15 verified, 0 errors +Processing AngelicExec.chalice + 14.5: Refinement may produce different value for a declared local variable: x + +Boogie program verifier finished with 11 verified, 1 error diff --git a/Chalice/tests/refinements/Calculator.chalice b/Chalice/tests/refinements/Calculator.chalice new file mode 100644 index 00000000..57c4c87d --- /dev/null +++ b/Chalice/tests/refinements/Calculator.chalice @@ -0,0 +1,69 @@ +/* + Carrol Morgan's calculator + 7/2/2010 Kuat Dafny version + 8/22/2010 translated into Chalice +*/ + +class Calc0 { + var vals: seq<int>; + + method reset() + requires acc(vals); + ensures acc(vals); + { + vals := []; + } + + method add(x: int) + requires acc(vals); + ensures acc(vals); + { + vals := [x] ++ vals; + } + + method mean() returns (m: int) + requires acc(vals) && |vals| > 0; + ensures acc(vals); + { + m := total(vals)/|vals|; + } + + unlimited function total(s: seq<int>): int + { + |s| == 0 ? 0 : s[0] + total(s[1..]) + } +} + + + +class Calc1 refines Calc0 { + var sum: int; + var num: int; + replaces vals by acc(sum) && acc(num) && sum == total(vals) && num == |vals|; + + refines reset() + { + sum := 0; + num := 0; + } + + refines add(x: int) + { + sum := sum + x; + num := num + 1; + } + + refines mean() returns (m: int) + { + m := sum/num; + } +} + + + + + + + + + diff --git a/Chalice/tests/refinements/Celebrity.chalice b/Chalice/tests/refinements/Celebrity.chalice new file mode 100644 index 00000000..b0d398e0 --- /dev/null +++ b/Chalice/tests/refinements/Celebrity.chalice @@ -0,0 +1,48 @@ +// Celebrity example, inspired by the Rodin tutorial
+class Person {
+ function knows(other: Person): bool
+ requires this != other;
+}
+
+class Celebrity0 {
+ function IsCelebrity(c: Person, people: seq<Person>): bool
+ requires null !in people;
+ {
+ c in people && forall p in people :: p != c ==> (p.knows(c)) && (! c.knows(p))
+ }
+
+ method Find(people: seq<Person>, /*ghost*/ c: Person) returns (r: Person)
+ requires null !in people && IsCelebrity(c, people);
+ {
+ var r [r == c];
+ }
+}
+
+/** Without theory of sets, hard to describe: "remove an element from a sequence" */
+class Celebrity1 refines Celebrity0 {
+ refines Find(people: seq<Person>, c: Person) returns (r: Person)
+ {
+ var q:seq<Person> := people;
+
+ // pick and remove a
+ var a:Person := q[0]; q := q[1..]; assert people == [a] ++ q;
+
+ while (|q| > 0)
+ invariant forall p in q :: p in people;
+ invariant a in people;
+ invariant IsCelebrity(c,[a] ++ q);
+ {
+ // pick and remove b
+ var oldq:seq<Person> := q;
+ var b:Person := q[0]; q := q[1..];
+ assert oldq == [b] ++ q;
+
+ if (a != b && a.knows(b)) {
+ a := b;
+ }
+ }
+
+ r := a;
+ }
+}
+
diff --git a/Chalice/tests/refinements/Counter.chalice b/Chalice/tests/refinements/Counter.chalice new file mode 100644 index 00000000..d1efae76 --- /dev/null +++ b/Chalice/tests/refinements/Counter.chalice @@ -0,0 +1,112 @@ +class Counter0 { + var x: int; + + method init() + requires acc(x); + ensures acc(x) && x == 0; + { + x := 0; + } + + method inc() + requires acc(x); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + } + + method dec() + requires acc(x); + ensures acc(x) && x == old(x) - 1; + { + x := x - 1; + } + + method magic() returns (c: Cell) + requires acc(x); + ensures acc(x) && acc(c.n) && x == old(x); + { + var c [acc(c.n)] + } +} + +class Counter1 refines Counter0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + refines init() + { + this.y := 0; + this.z := 0; + } + + refines inc() + { + this.y := this.y + 1; + } + + refines dec() + { + this.z := this.z + 1; + } + + refines magic() returns (c: Cell) + { + c := new Cell; + } +} + +class Cell {var n: int} + +/** TODO: +Two-step data refinement doesn't work for the following reason: +the spec of Counter1 uses the abstract field x which disappears at the concrete method body level. +I'm not sure what a good solution to this problem... +*/ + +class Counter2 refines Counter0 { + var a: Cell; + var b: Cell; + replaces x by acc(a) && acc(b) && acc(a.n) && acc(b.n) && x == a.n - b.n; + + refines init() + { + this.a := new Cell; + this.b := new Cell; + this.a.n := 0; + this.b.n := 0; + } + + refines inc() + { + this.a.n := this.a.n + 1; + } + + refines dec() + { + var i := this.b.n + 1; + this.b := new Cell; + this.b.n := i; + } + + refines magic() returns (c: Cell) + { + c := a; + } +} + +class Client { + method main() + { + var c := new Counter0; + call c.init(); + call c.inc(); + call c.inc(); + call c.dec(); + call d := c.magic(); + d.n := 100; + assert c.x == 1; + } +} + diff --git a/Chalice/tests/refinements/CounterReverse.chalice b/Chalice/tests/refinements/CounterReverse.chalice new file mode 100644 index 00000000..57d87803 --- /dev/null +++ b/Chalice/tests/refinements/CounterReverse.chalice @@ -0,0 +1,21 @@ +class Counter1 { + var y: int; + var z: int; + method inc() + requires acc(y) && acc(z); + requires y >= 0 && z >= 0; + ensures acc(y) && acc(z); + ensures y >= 0 && z >= 0; + { + y := y + 1; + } +} + +class Counter0 refines Counter1 { + var x: int; + replaces y,z by acc(x) && x == y - z; + refines inc() + { + this.x := this.x + 1; + } +} diff --git a/Chalice/tests/refinements/DSW.chalice b/Chalice/tests/refinements/DSW.chalice new file mode 100644 index 00000000..1737df85 --- /dev/null +++ b/Chalice/tests/refinements/DSW.chalice @@ -0,0 +1,119 @@ +// Schorr-Waite algorithm in Chalice
+// (see Test/dafny1/SchorrWaite.dfy)
+
+class Node {
+ var children: seq<Node>;
+ var marked: bool;
+ ghost var path: seq<Node>;
+
+ var parent: Node;
+}
+
+class DSW0 {
+ var stack: seq<Node>;
+ var S: seq<Node>;
+ var root: Node;
+
+ function Reachable(to: Node, p:seq<Node>, from: Node): bool
+ requires acc(p[*].children);
+ {
+ |p| == 0 ? to == from :
+ (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from))
+ }
+
+ method IterativeMark()
+ requires acc(this.*) && acc(S[*].children) && acc(S[*].marked) && acc(S[*].path);
+ requires root in S;
+ requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S);
+ requires forall n in S :: ! n.marked;
+ ensures acc(this.*) && acc(S[*].children) && acc(S[*].marked) && acc(S[*].path);
+ // graph structure is the same
+ ensures S == old(S) && root == old(root);
+ ensures forall n in S :: n.children == old(n.children);
+ // all nodes reachable from root are marked
+ ensures root.marked;
+ ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked);
+ // all marked nodes are reachable from root
+ ensures forall n in S :: n.marked ==>
+ (forall m in n.path :: m in S) && Reachable(n, n.path, root);
+ {
+ var t:Node := root;
+ t.marked := true;
+ stack := nil<Node>;
+ t.path := stack;
+
+ // no termination check
+ var stop := false;
+ while(!stop)
+ invariant acc(this.*) && acc(S[*].children) && acc(S[*].marked) && acc(S[*].path);
+ invariant root == old(root);
+ invariant S == old(S);
+ invariant root.marked;
+ invariant t in S && t.marked && t !in stack;
+ // stack well-formed
+ invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j];
+ invariant forall n in stack :: n in S && n.marked;
+ invariant forall i in [1..|stack|] :: stack[i-1] in stack[i].children;
+ invariant 0 < |stack| ==> t in stack[0].children;
+ // goal
+ invariant forall n in S :: n.marked && n !in stack && n != t ==>
+ (forall ch in n.children :: ch in S && ch.marked);
+ invariant forall n in S :: n.marked ==>
+ (forall m in n.path :: m in S) && Reachable(n, n.path, root);
+ // preservation
+ invariant forall n in S :: n.children == old(n.children);
+ // termination
+ invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked);
+ {
+ call n := PickUnmarked(t.children);
+ if (n != null) {
+ // push
+ stack := [t] ++ stack;
+ n.path := [t] ++ t.path;
+ t := n;
+ t.marked := true;
+ assert Reachable(t.path[0], t.path[1..], root); // needed for limited function
+ } else {
+ // pop
+ if (|stack| == 0) {
+ stop := true;
+ } else {
+ t := stack[0];
+ stack := stack[1..];
+ }
+ }
+ }
+ }
+
+ method PickUnmarked(p: seq<Node>) returns (x: Node)
+ requires rd(p[*].marked);
+ requires forall n in p :: n != null;
+ ensures rd(p[*].marked);
+ ensures x != null ==> x in p && ! x.marked;
+ ensures x == null ==> (forall n in p :: n.marked);
+ {
+ var x [(exists n in p :: !n.marked) ? (x in p && !x.marked) : (x == null)]
+ }
+}
+
+class DSW1 refines DSW0 {
+ replaces stack by acc(S[*].parent);
+
+ transforms IterativeMark()
+ {
+ *
+ }
+
+ transforms PickUnmarked(p: seq<Node>) returns (x: Node)
+ {
+ replaces x by {
+ if (|p| == 0) {
+ x := null;
+ } else if (! p[0].marked) {
+ x := p[0];
+ } else {
+ call x := PickUnmarked(p[1..]);
+ }
+ }
+ }
+}
diff --git a/Chalice/tests/refinements/Duplicates.chalice b/Chalice/tests/refinements/Duplicates.chalice new file mode 100644 index 00000000..52cdc3c3 --- /dev/null +++ b/Chalice/tests/refinements/Duplicates.chalice @@ -0,0 +1,115 @@ +class Duplicates0 {
+ // 3. we can do fast set checks if we know the bounds on the elements
+ method find(s: seq<int>) returns (b:bool)
+ requires forall i in s :: 0 <= i && i < 100;
+ {
+ var b [b == (exists i in [0..|s|] :: s[i] in s[..i]) ];
+ }
+}
+
+class Duplicates1 refines Duplicates0 {
+ refines find(s: seq<int>) returns (b: bool)
+ {
+ b := false;
+ // 0. need a loop
+ // 1. need a set data structure
+ var i := 0;
+ var d := new Set0;
+ call d.init();
+
+ // 6. use a witness from the loop
+ ghost var w;
+
+ while (i < |s|)
+ invariant 0 <= i && i <= |s|;
+ // 5. add loop invariants using value of Set.add: equivalence as a set
+ invariant acc(d.rep);
+ // 6. assert equivalent as sets of d.rep and s[..i]
+ invariant forall n in d.rep :: n in s[..i];
+ invariant forall n in [0..i] :: s[n] in d.rep;
+ // 7. devise termination conditions to satisfy the spec
+ invariant b ==> 0 <= w && w < |s| && s[w] in s[..w];
+ invariant !b ==> (forall j,k in [0..i] :: j != k ==> s[j] != s[k]);
+ {
+ call r := d.add(s[i]);
+ assert r ==> d.rep[0] == s[i]; // help out sequence axioms
+
+ if (! r) {
+ b := true;
+ w := i;
+ }
+
+ i := i + 1;
+ }
+ }
+}
+
+class Set0 {
+ var rep: seq<int>;
+
+ method init()
+ requires acc(rep);
+ ensures acc(rep) && |rep| == 0;
+ {
+ rep := nil<int>;
+ }
+
+ method add(i) returns (b:bool)
+ requires acc(rep);
+ requires 0 <= i && i < 100;
+ ensures acc(rep);
+ ensures (i in old(rep)) ==> !b && rep == old(rep);
+ ensures (i !in old(rep)) ==> b && rep == [i] ++ old(rep);
+ {
+ // 2. need a way to compute whether element is in the set
+ var c:bool [c <==> i in old(rep)];
+ if (c) {
+ b := false;
+ } else {
+ b := true;
+ rep := [i] ++ rep;
+ assert rep[0] == i;
+ }
+ }
+}
+
+class Set1 refines Set0 {
+ var bitset: seq<bool>;
+
+ // 4. represent a set as a bitset (provided representation invariant of the uppermost class)
+ replaces rep by acc(bitset) &&
+ /** representation invariant */ (forall i in rep :: 0 <= i && i < 100) && |bitset| == 100 &&
+ /** coupling invariant */ (forall j in [0..100] :: bitset[j] <==> (j in rep))
+
+
+ refines init()
+ {
+ var i := 0;
+ bitset := nil<bool>;
+ while (i < 100)
+ invariant i <= 100 && acc(bitset);
+ invariant |bitset| == i;
+ invariant forall b in bitset :: ! b;
+ {
+ bitset := [false] ++ bitset;
+ i := i + 1;
+ }
+ }
+
+ transforms add(i) returns (b: bool)
+ {
+ replaces c by {var c:bool := this.bitset[i]}
+ if {
+ *
+ } else {
+ replaces * by {
+ b := true;
+ var s:seq<bool> := [true] ++ this.bitset[i+1..];
+ assert s[0] == true; // help out sequence axioms
+ s := this.bitset[..i] ++ s;
+
+ this.bitset := s;
+ }
+ }
+ }
+}
diff --git a/Chalice/tests/refinements/DuplicatesLight.chalice b/Chalice/tests/refinements/DuplicatesLight.chalice new file mode 100644 index 00000000..5fbe0735 --- /dev/null +++ b/Chalice/tests/refinements/DuplicatesLight.chalice @@ -0,0 +1,42 @@ +class Duplicates0 {
+ method find(s: seq<int>) returns (b: bool)
+ requires forall i in s :: i in [0..100];
+ {
+ spec b [ b <==> (exists i in [0..|s|] :: s[i] in s[..i]) ];
+ }
+}
+
+class Duplicates1 refines Duplicates0 {
+ refines find(s: seq<int>) returns (b: bool)
+ {
+ var n := 0;
+ b := false;
+ while (n < |s|)
+ invariant 0 <= n && n <= |s|;
+ invariant b <==> (exists i in [0..n] :: s[i] in s[..i]);
+ {
+ spec c: bool [ c <==> s[n] in s[..n] ];
+ b := b || c;
+ n := n + 1;
+ }
+ }
+}
+
+class Duplicates2 refines Duplicates1 {
+ transforms find(s: seq<int>) returns (b: bool)
+ {
+ _
+ var bitset:seq<bool> [ |bitset| == 100 && true !in bitset ];
+ while
+ invariant |bitset| == 100;
+ invariant forall i in [0..100] :: bitset[i] <==> i in s[..n];
+ {
+ replaces c by {
+ var c: bool := bitset[ s[n] ];
+ }
+ bitset := bitset[ .. s[n] ] ++ [true] ++ bitset[ s[n] + 1 ..];
+ _
+ }
+ _
+ }
+}
diff --git a/Chalice/tests/refinements/DuplicatesVideo.chalice b/Chalice/tests/refinements/DuplicatesVideo.chalice new file mode 100644 index 00000000..3886cb78 --- /dev/null +++ b/Chalice/tests/refinements/DuplicatesVideo.chalice @@ -0,0 +1,43 @@ +class Duplicates0 {
+ method Find(s: seq<int>) returns (b: bool)
+ requires forall i in s :: i in [0..100];
+ {
+ b := exists i in [0..|s|] :: s[i] in s[..i];
+ }
+}
+
+class Duplicates1 refines Duplicates0 {
+ refines Find(s: seq<int>) returns (b: bool)
+ {
+ var n := 0;
+ b := false;
+ while (n < |s|)
+ invariant 0 <= n && n <= |s|;
+ invariant b <==> exists i in [0..n] :: s[i] in s[..i];
+ {
+ var c := s[n] in s[..n];
+ b := b || c;
+ n := n + 1;
+ }
+ }
+}
+
+class Duplicates2 refines Duplicates1 {
+ transforms Find(s: seq<int>) returns (b: bool)
+ {
+ _;
+ // bitset has length 100, initially all false
+ var bitset:seq<bool> [|bitset| == 100 && true !in bitset ];
+ while
+ invariant |bitset| == 100;
+ invariant forall i in [0..n] :: bitset[ s[i] ];
+ invariant forall j in [0..100] :: bitset[j] ==> j in s[..n];
+ {
+ replaces c by {
+ var c: bool := bitset[ s[n] ];
+ }
+ bitset := bitset[..s[n] ] ++ [true] ++ bitset[ s[n] + 1 ..];
+ _;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/refinements/List.chalice b/Chalice/tests/refinements/List.chalice new file mode 100644 index 00000000..b13f6ee3 --- /dev/null +++ b/Chalice/tests/refinements/List.chalice @@ -0,0 +1,47 @@ +class List0 {
+ var rep: seq<int>;
+
+ method init()
+ requires acc(rep);
+ ensures acc(rep);
+ {
+ rep := [0];
+ }
+
+ method get(i) returns (v)
+ requires acc(rep);
+ requires 0 <= i && i < |rep|;
+ ensures acc(rep);
+ {
+ v := rep[i];
+ }
+}
+
+class List1 refines List0 {
+ var sub: seq<List1>;
+ var data: int;
+
+ replaces rep by acc(sub) && acc(data) && acc(sub[*].sub) && acc(sub[*].data) &&
+ /** valid */ |sub| >= 0 &&
+ (forall i in [0..|sub|] :: sub[i] != null && sub[i].sub == sub[i+1..]) &&
+ /** coupling */ |sub| + 1 == |rep| &&
+ (forall i in [0..|sub|] :: sub[i].data == rep[i+1]) &&
+ data == rep[0]
+
+ refines init()
+ {
+ data := 0;
+ sub := nil<List1>;
+ }
+
+ refines get(i) returns (v)
+ {
+ if (i == 0) {
+ v := data;
+ } else {
+ var next:List1 := sub[0];
+ call v := next.get(i-1);
+ //v := sub[i-1].data;
+ }
+ }
+}
diff --git a/Chalice/tests/refinements/LoopFiniteDiff.chalice b/Chalice/tests/refinements/LoopFiniteDiff.chalice new file mode 100644 index 00000000..bd744c89 --- /dev/null +++ b/Chalice/tests/refinements/LoopFiniteDiff.chalice @@ -0,0 +1,61 @@ +class Cube0 { + method compute(n) + requires n >= 0; + { + var v [v == n*n*n]; + } +} + +class Cube1 refines Cube0 { + transforms compute(n) + { + replaces v by { + var i := 0; + var v := 0; + while (i < n) + invariant i <= n + invariant v == i * i * i + { + i := i + 1; + var v [v == i * i * i]; + } + } + } +} + +class Cube2 refines Cube1 { + transforms compute(n) + { + _ + var w := 1; + while + invariant w == (i+1)*(i+1)*(i+1) - i*i*i + { + _ + replaces v by { + v := v + w; + var w [w == (i+1)*(i+1)*(i+1) - i*i*i]; + } + } + _ + } +} + +class Cube3 refines Cube2 { + transforms compute(n) + { + _ + var x := 0; + while + invariant x == i*i + { + _ + replaces w by { + x := x + 2*i - 1; + w := 3*x + 3*i + 1; + } + } + _ + } +} + diff --git a/Chalice/tests/refinements/LoopSqRoot.chalice b/Chalice/tests/refinements/LoopSqRoot.chalice new file mode 100644 index 00000000..4ea9434d --- /dev/null +++ b/Chalice/tests/refinements/LoopSqRoot.chalice @@ -0,0 +1,43 @@ +class A0 { + method sqroot(n) returns (x) + requires n >= 0; + { + var x [x*x <= n && n < (x+1)*(x+1) && x >=0]; + } +} + +class A1 refines A0 { + transforms sqroot(n) returns (x) + { + replaces x by { + var l := 0; + var r := n + 1; + while (l + 1 != r) + invariant l >= 0 && r > l; + invariant l*l <= n && n < r*r; + { + var k [l < k && k < r]; + if (k*k <= n) { + l := k; + } else { + r := k; + } + } + x := l; + } + } +} + +class A2 refines A1 { + transforms sqroot(n) returns (x) + { + _ + while { + replaces k by { + var k [2*k <= l+r && l+r < 2*(k+1)] + } + * + } + _ + } +} diff --git a/Chalice/tests/refinements/Pick.chalice b/Chalice/tests/refinements/Pick.chalice new file mode 100644 index 00000000..7df2f90d --- /dev/null +++ b/Chalice/tests/refinements/Pick.chalice @@ -0,0 +1,28 @@ +class Pick0 { + method pick(s: seq<int>) returns (x) + requires |s| > 0; + { + var x [x in s] + } +} + +class Pick1 refines Pick0 { + transforms pick(s: seq<int>) returns (x) + { + replaces x by {x := s[0]} + } +} + +class Pick2 refines Pick0 { + transforms pick(s: seq<int>) returns (x) + { + replaces * by {x := s[|s|-1]} + } +} + +class Pick3 refines Pick0 { + transforms pick(s: seq<int>) returns (x) + { + replaces x by {x := s[1]} + } +} diff --git a/Chalice/tests/refinements/RecFiniteDiff.chalice b/Chalice/tests/refinements/RecFiniteDiff.chalice new file mode 100644 index 00000000..1a971aed --- /dev/null +++ b/Chalice/tests/refinements/RecFiniteDiff.chalice @@ -0,0 +1,51 @@ +// Example of a program computing cube using only addition. +// Step-wise refinement using specification statement. +// Chalice does not have termination metric for recursive methods. + +class Cube0 { + method compute(n) returns (v) + requires n >= 0; + ensures v == n*n*n; + { + var v [v == n*n*n] + } +} + +class Cube1 refines Cube0 { + transforms compute(n) returns (v, w) + // strengthen post-condition based on new output variables + ensures w == (n+1)*(n+1)*(n+1)-n*n*n; + { + replaces v by { + if (n == 0) { + v := 0; + w := 1; + } else { + call v1,w1 := compute(n-1); // rely on stronger post-condition + v := v1 + w1; + // simplified form: aha! we need n*n to compute with addition + var w [w == 3*n*n + 3*n + 1]; + } + } + } +} + +class Cube2 refines Cube1 { + transforms compute(n) returns (v, w, x) + ensures x == (n+1)*(n+1); + { + if { + _ + x := 1; + } else { + replaces v1, w1 by { + call v1,w1,x1 := compute(n-1); + } + _ + replaces w by { + w := 3*x1 + 3*n + 1; + x := x1 + 2*n + 1; + } + } + } +} diff --git a/Chalice/tests/refinements/RecSqRoot.chalice b/Chalice/tests/refinements/RecSqRoot.chalice new file mode 100644 index 00000000..a10c1b55 --- /dev/null +++ b/Chalice/tests/refinements/RecSqRoot.chalice @@ -0,0 +1,46 @@ +class A0 { + method sqroot(n) returns (x) + requires n >= 0; + { + var x [x*x <= n && n < (x+1)*(x+1)]; + } +} + +class A1 refines A0 { + transforms sqroot(n) returns (x) + { + replaces x by {call x := rec(n,0,n+1)} + } + + method rec(n, l, r) returns (x) + requires l*l <= n && n < r*r; + requires l >= 0 && r >= 0; + ensures x*x <= n && n < (x+1)*(x+1); + { + if (l+1 == r) { + x := l; + } else { + var k [l < k && k < r]; + if (n < k*k) { + call x := rec(n,l,k); + } else { + call x := rec(n,k,r); + } + } + } +} + +class A2 refines A1 { + transforms rec(n, l, r) returns (x) + { + if { + * + } else { + replaces k by { + assert l < r; + var k := l+1; + } + * + } + } +} diff --git a/Chalice/tests/refinements/SpecStmt.chalice b/Chalice/tests/refinements/SpecStmt.chalice new file mode 100644 index 00000000..15072d41 --- /dev/null +++ b/Chalice/tests/refinements/SpecStmt.chalice @@ -0,0 +1,35 @@ +class Test { + var x: int; + method m(a:int) returns (b:int) + { + var c := 0; + ghost const d,c [d == c]; + var b [b == 0]; + var e [e == a]; + assert d == c; + assert e == a; + assert b == 0; + assert c == 0; // error + } + + method n() + requires acc(x); + { + x := 0; + const y [acc(x), rd(x) && x == old(x) + 1 && y == x]; + assert y == 1; + const v [rd(x), rd(x) && v == old(x) + 1]; + assert v == 2; + const z [z == 1]; + ghost var t [z == 1, true]; + assert false; // reachable + } + + method o() + { + var z [acc(x) && z == 0]; // unimplementable + x := z; + assert x == 0; + assert false; // reachable + } +} diff --git a/Chalice/tests/refinements/SumCubes.chalice b/Chalice/tests/refinements/SumCubes.chalice new file mode 100644 index 00000000..a24a0f37 --- /dev/null +++ b/Chalice/tests/refinements/SumCubes.chalice @@ -0,0 +1,29 @@ +class SumCubes0 { + method compute(n) + requires n >= 0; + { + var i := 0; + var s := 0; + while (i < n) + invariant i <= n; + { + i := i + 1; + s := s + i*i*i; + } + } +} + +class SumCubes1 refines SumCubes0 { + transforms compute(n) + { + _ + var t := 0; + while + invariant s == t*t; + invariant 2*t == i*(i+1); + { + _ + t := t + i; + } + } +} diff --git a/Chalice/tests/refinements/TestCoupling.chalice b/Chalice/tests/refinements/TestCoupling.chalice new file mode 100644 index 00000000..a178c9b4 --- /dev/null +++ b/Chalice/tests/refinements/TestCoupling.chalice @@ -0,0 +1,74 @@ +class A0 { + var x: int; + var n: int; + var k: int; + + method inc() + requires acc(x) && acc(n); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + n := n + 1; + } + + method error() + requires acc(x) + ensures acc(x) + { + x := x + 1; + } +} + +class A1 refines A0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + refines inc() + ensures y == old(y) + 1 + { + this.y := 1 + this.y; + this.n := this.n + 1; + } + + refines error() + ensures acc(y) + { + this.y := 1 + this.y; + } +} + +class B0 { + var x: int; + var y: int; + + method error() + requires acc(x); + ensures acc(x); + { + x := x + 1; + } + + method inc() + requires acc(x) && acc(y); + ensures acc(x) && acc(y); + { + x := x + 1; + } +} + +class B1 refines B0 { + var z: int; + replaces x,y by acc(z) && z == x + y; + + refines error() + { + this.z := this.z + 1; + } + + refines inc() + { + this.z := this.z + 1; + } +} + diff --git a/Chalice/tests/refinements/TestRefines.chalice b/Chalice/tests/refinements/TestRefines.chalice new file mode 100644 index 00000000..3081eb90 --- /dev/null +++ b/Chalice/tests/refinements/TestRefines.chalice @@ -0,0 +1,30 @@ +class A { + var x:int; + function f():int {1} + method m(i:int) returns (j:int) { + var j [j > 0]; + } +} + +class B refines C {} +class C refines D {} +class D refines A { + transforms m(i:int) returns (j:int, k:int) + { + * + } +} + +class X { + method m() returns (c: bool) + { + c := true; + } +} + +class Y refines X { + refines m() returns (c: bool, d: bool) + { + c := false; + } +} diff --git a/Chalice/tests/refinements/TestTransform.chalice b/Chalice/tests/refinements/TestTransform.chalice new file mode 100644 index 00000000..2c18907f --- /dev/null +++ b/Chalice/tests/refinements/TestTransform.chalice @@ -0,0 +1,38 @@ +class A { + method m(i: int) returns (x: int) + ensures x == i; + { + var j := 0; + var v [v == i + j]; + x := v; + } + + method n() { + var x := 0; + var y := 1; + var z := 2; + } +} + +class B refines A { + transforms m(i: int) returns (x: int, y: int) + ensures y == 0; + { + var t := 0; + _ + replaces v by { + var v := i + j; + call t, j := m(0); + y := j; + } + _ + } + + transforms n() { + replaces * by { + var x := 0; + var y := x + 1; + var z := 2*y; + } + } +} diff --git a/Chalice/tests/refinements/original/CounterPredicate.chalice b/Chalice/tests/refinements/original/CounterPredicate.chalice new file mode 100644 index 00000000..fd35c18c --- /dev/null +++ b/Chalice/tests/refinements/original/CounterPredicate.chalice @@ -0,0 +1,136 @@ +class Cell { + var n : int; +} + +class A { + var x : int; + + predicate valid { + acc(x) && x >= 0 + } + + function getX(): int requires valid + { + unfolding valid in x + } + + method init() + requires acc(this.*); + ensures valid; + { + x := 0; + fold valid; + } + + method inc() + requires valid; + ensures valid && getX() == old(getX()) + 1; + { + unfold valid; + x := x + 1; + fold valid; + } + + method dec() + requires valid && getX() > 0; + ensures valid; + { + unfold valid; + x := x - 1; + fold valid; + } + + method magic() returns (c: Cell) + requires valid; + ensures valid; + { + } +} + +class C { + ghost var x : int; + var y : Cell; + var z : Cell; + + function getX() : int + requires valid; + { + unfolding valid in y.n - z.n + } + + predicate valid { + acc(x) && acc(y) && acc(z) && acc(y.n) && acc(z.n) && + y != null && z != null && + y.n >= 0 && z.n >= 0 && + y.n - z.n == x && + x >= 0 + } + + method init() + requires acc(this.*); + ensures valid; + { + x := 0; + // + y := new Cell; + z := new Cell; + y.n := 0; + z.n := 0; + fold valid; + } + + method inc() + requires valid; + ensures valid && getX() == old(getX()) + 1; + { + unfold valid; + x := x + 1; + // + y.n := y.n + 1; + fold valid; + } + + method dec() + requires valid && getX() > 0; + ensures valid; + { + unfold valid; + x := x - 1; + // + z.n := z.n + 1; + fold valid; + } + + method magic() returns (c: Cell) + requires valid; + ensures valid; + { + unfold valid; + c := y; + fold valid; + } +} + +class Client { + method main() + { + // Abstract program + var a := new A; + call a.init(); + call a.inc(); // problem is here + call a.inc(); + call a.dec(); + call ac := a.magic(); + ac.n := 0; + + // Concrete program + var c := new C; + call c.init(); + call c.inc(); + call c.inc(); + call c.dec(); + call cc := c.magic(); + cc.n := 0; + } +} + diff --git a/Chalice/tests/refinements/original/DSW0.chalice b/Chalice/tests/refinements/original/DSW0.chalice new file mode 100644 index 00000000..d83c5438 --- /dev/null +++ b/Chalice/tests/refinements/original/DSW0.chalice @@ -0,0 +1,145 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// (incomplete version) Two children instead of a sequence of an array +class Node { + var left: Node; + var right: Node; + var marked: bool; + var l: bool; + var r: bool; +} + +class Main { + method RecursiveMark(root: Node, S: seq<Node>) + requires acc(S[*].marked, 50) && acc(S[*].*, 50); + requires root != null && root in S; + // S is closed under 'left' and 'right': + requires forall n in S :: n != null && + ((n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S)); + requires forall n in S :: ! n.marked; + ensures acc(S[*].marked, 50) && acc(S[*].*, 50); + ensures root.marked; + // nodes reachable from 'root' are marked: + ensures forall n in S :: n.marked ==> + ((n.left != null ==> n.left in S && n.left.marked) && + (n.right != null ==> n.right in S && n.right.marked)); + { + var stack: seq<Node> := []; + call RecursiveMarkWorker(root, S, stack); + } + + method RecursiveMarkWorker(root: Node, S: seq<Node>, stack: seq<Node>) + requires acc(S[*].marked, 50) && acc(S[*].*, 50); + requires root != null && root in S; + requires forall n in S :: n != null && + ((n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S)) + requires forall n in S :: n.marked ==> + (n in stack || + ((n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked))); + requires forall n in stack :: n != null && n in S && n.marked; + ensures acc(S[*].marked, 50) && acc(S[*].*, 50); + ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right); + ensures forall n in S :: n.marked ==> + (n in stack || + ((n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked))); + ensures forall n in S :: old(n.marked) ==> n.marked; + ensures root.marked; + { + if (! root.marked) { + root.marked := true; + var next:seq<Node> := [root] ++ stack; + assert next[0] == root; + if (root.left != null) { + call RecursiveMarkWorker(root.left, S, next); + } + + if (root.right != null) { + call RecursiveMarkWorker(root.right, S, next); + } + } + } + + method IterativeMark(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && + (n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S); + requires forall n in S :: ! n.marked; + requires forall n in S :: ! n.l && ! n.r; + ensures acc(S[*].*); + ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right); + ensures root.marked; + ensures forall n in S :: n.marked ==> + (n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked); + ensures forall n in S :: ! n.l && ! n.r; + { + var t:Node := root; + t.marked := true; + var stack: seq<Node> := []; + + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked && t in S && t !in stack; + invariant forall n in stack :: n in S; + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + invariant forall n in S :: (n in stack || n == t) ==> + n.marked && + (n.r ==> n.l) && + (n.l && n.left != null ==> n.left in S && n.left.marked) && + (n.r && n.right != null ==> n.right in S && n.right.marked) + // stack is linked + invariant forall i in [1..|stack|] :: stack[i-1] == (stack[i].l ? stack[i].right : stack[i].left); + invariant 0 < |stack| ==> t == (stack[0].l ? stack[0].right : stack[0].left); + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (n.left != null ==> n.left in S && n.left.marked) && + (n.right != null ==> n.right in S && n.right.marked); + // preservation + invariant forall n in S :: n !in stack && n != t ==> ! n.l && ! n.r; + invariant forall n in S :: n.left == old(n.left) && n.right == old(n.right); + invariant stop ==> |stack| == 0 && ! t.l && ! t.r && + (t.left != null ==> t.left.marked) && + (t.right != null ==> t.right.marked); + { + if (! t.l && (t.left == null || t.left.marked)) { + // advance + t.l := true; + } else if (t.l && ! t.r && (t.right == null || t.right.marked)) { + // advance + t.r := true; + } else if (t.r) { + // pop + t.l := false; + t.r := false; + if (|stack| == 0) { + stop := true; + } else { + t := stack[0]; + stack := stack[1..]; + if (t.l) {t.r := true} else {t.l := true} + } + } else if (!t.l) { + // push + stack := [t] ++ stack; + assert stack[0] == t; + t := t.left; + t.marked := true; + } else if (!t.r) { + // push + assert t.l; + stack := [t] ++ stack; + assert stack[0] == t; + t := t.right; + t.marked := true; + } + } + } +} diff --git a/Chalice/tests/refinements/original/DSW1.chalice b/Chalice/tests/refinements/original/DSW1.chalice new file mode 100644 index 00000000..612f21ac --- /dev/null +++ b/Chalice/tests/refinements/original/DSW1.chalice @@ -0,0 +1,91 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// Arbitrary number of children +// No counter for visited nodes; next node is selected non-deterministically +class Node { + var children: seq<Node>; + var marked: bool; + ghost var path: seq<Node>; +} + +class Main { + function Reachable(to: Node, p:seq<Node>, from: Node): bool + requires acc(p[*].children); + { + |p| == 0 ? to == from : + (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from)) + } + + method IterativeMark(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); + requires forall n in S :: ! n.marked; + ensures acc(S[*].*); + // graph structure is the same + ensures forall n in S :: n.children == old(n.children); + // all nodes reachable from root are marked + ensures root.marked; + ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked); + // all marked nodes are reachable from root + ensures forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && Reachable(n, n.path, root); + { + var t:Node := root; + t.marked := true; + var stack: seq<Node> := []; + t.path := stack; + + // no termination check + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked; + invariant t in S && t.marked && t !in stack; + // stack well-formed + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + invariant forall n in stack :: n in S && n.marked; + invariant forall i in [1..|stack|] :: stack[i-1] in stack[i].children; + invariant 0 < |stack| ==> t in stack[0].children; + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (forall ch in n.children :: ch in S && ch.marked); + invariant forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && Reachable(n, n.path, root); + // preservation + invariant forall n in S :: n.children == old(n.children); + // termination + invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked); + { + call n := PickUnmarked(t.children); + + if (n != null) { + // push + stack := [t] ++ stack; + n.path := [t] ++ t.path; + t := n; + t.marked := true; + assert Reachable(t.path[0], t.path[1..], root); // needed for limited function + } else { + // pop + if (|stack| == 0) { + stop := true; + } else { + t := stack[0]; + stack := stack[1..]; + } + } + } + } + + method PickUnmarked(p: seq<Node>) returns (x: Node) + requires rd(p[*].marked); + requires forall n in p :: n != null; + ensures rd(p[*].marked); + ensures x != null ==> x in p && ! x.marked; + ensures x == null ==> (forall n in p :: n.marked); + { + assume false; // magic! + } +} diff --git a/Chalice/tests/refinements/original/DSW10.chalice b/Chalice/tests/refinements/original/DSW10.chalice new file mode 100644 index 00000000..3bf70eeb --- /dev/null +++ b/Chalice/tests/refinements/original/DSW10.chalice @@ -0,0 +1,120 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// Arbitrary number of children +// Added visited field to refine non-det choice with a conditional +// Added a client +class Node { + var children: seq<Node>; + var marked: bool; + var visited: int; + ghost var path: seq<Node>; +} + +class Main { + method Test() + { + var a := new Node {marked := false, visited := 0}; + var b := new Node {marked := false, visited := 0}; + var c := new Node {marked := false, visited := 0}; + var d := new Node {marked := false, visited := 0}; + a.children := [b]; + b.children := [c,a]; + c.children := [b]; + d.children := [a,b,c]; + // a <-> b <-> c + // ^ \ ^ / ^ + // d + assert [a,b,c,d][0] == a; // root is in sequence + call IterativeMark(a, [a,b,c,d]); + assert a.marked; + assert a.children[0] == b; // b should be marked + assert b.marked; + assert b.children[0] == c; // c should be marked + assert c.marked; + assert !d.marked; + } + + function Reachable(to: Node, p:seq<Node>, from: Node): bool + requires acc(p[*].children); + { + |p| == 0 ? to == from : + (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from)) + } + + method IterativeMark(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); + requires forall n in S :: ! n.marked; + requires forall n in S :: n.visited == 0; + ensures acc(S[*].*); + // graph structure is the same + ensures forall n in S :: n.children == old(n.children); + ensures forall n in S :: n.visited == 0; + // all nodes reachable from root are marked + ensures root.marked; + ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked); + // all marked nodes are reachable from root + ensures forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && + Reachable(n, n.path, root); + { + var t:Node := root; + t.marked := true; + var stack: seq<Node> := []; + t.path := stack; + + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked && t in S && t.marked && t !in stack; + // no duplicates in the stack + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + // stack well-formed + invariant forall n in stack :: n in S; + invariant forall n in S :: n in stack || n == t ==> + n.marked && + 0 <= n.visited && n.visited <= |n.children| && + (forall i in [0..n.visited] :: n.children[i] in S && n.children[i].marked); + invariant forall n in stack :: n.visited < |n.children|; + // stack is linked + invariant forall i in [1..|stack|] :: stack[i-1] == stack[i].children[stack[i].visited]; + invariant 0 < |stack| ==> t == stack[0].children[stack[0].visited]; + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (forall ch in n.children :: ch in S && ch.marked); + invariant forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && + Reachable(n, n.path, root); + // preservation + invariant forall n in S :: n !in stack && n != t ==> n.visited == old(n.visited); + invariant forall n in S :: n.children == old(n.children); + // termination + invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked) && t.visited == 0; + { + if (t.visited == |t.children|) { + // pop + t.visited := 0; + if (|stack| == 0) { + stop := true; + } else { + t := stack[0]; + stack := stack[1..]; + t.visited := t.visited + 1; + } + } else if (t.children[t.visited].marked) { + // skip + t.visited := t.visited + 1; + } else { + // push + ghost var oldt:Node := t; + stack := [t] ++ stack; + t := t.children[t.visited]; + t.path := [oldt] ++ oldt.path; // TODO: in fact, this is stack + t.marked := true; + assert Reachable(oldt, oldt.path, root); // needed for limited function + } + } + } +} diff --git a/Chalice/tests/refinements/original/DSW2.chalice b/Chalice/tests/refinements/original/DSW2.chalice new file mode 100644 index 00000000..7438c688 --- /dev/null +++ b/Chalice/tests/refinements/original/DSW2.chalice @@ -0,0 +1,95 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// Add arbitrary number of children, not just two. +// Remove visited field for visited nodes; next node is selected non-deterministically (verification time 30s) +// Added parent pointer p (stack remains) (verification time 8s, limited functions) +class Node { + var children: seq<Node>; + var marked: bool; + ghost var path: seq<Node>; +} + +class Main { + function Reachable(to: Node, p:seq<Node>, from: Node): bool + requires acc(p[*].children); + { + |p| == 0 ? to == from : + (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from)) + } + + method SchorrWaite(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); + requires forall n in S :: ! n.marked; + ensures acc(S[*].*); + // graph structure is the same + ensures forall n in S :: n.children == old(n.children); + // all nodes reachable from root are marked + ensures root.marked; + ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked); + // all marked nodes are reachable from root + ensures forall n in S :: n.marked ==> (forall m in n.path :: m in S) && Reachable(n, n.path, root); + { + var p:Node := null; + var t:Node := root; + t.marked := true; + var stack: seq<Node> := []; + t.path := stack; + + // no termination check + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked; + invariant t in S && t.marked && t !in stack; + // stack well-formed + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + invariant forall n in stack :: n in S && n.marked; + invariant forall i in [1..|stack|] :: stack[i-1] in stack[i].children; + invariant 0 < |stack| ==> p == stack[0] && t in p.children; + invariant 0 == |stack| ==> p == null; + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (forall ch in n.children :: ch in S && ch.marked); + invariant forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && Reachable(n, n.path, root); + // preservation + invariant forall n in S :: n.children == old(n.children); + // termination + invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked); + { + call n := PickUnmarked(t.children); + + if (n != null) { + // push + p := t; + stack := [t] ++ stack; + n.path := [t] ++ t.path; + t := n; + t.marked := true; + assert Reachable(t.path[0], t.path[1..], root); // limited function + } else { + // pop + if (p == null) { + stop := true; + } else { + t := p; + stack := stack[1..]; + p := |stack| > 0 ? stack[0] : null; + } + } + } + } + + method PickUnmarked(p: seq<Node>) returns (x: Node) + requires rd(p[*].marked); + requires forall n in p :: n != null; + ensures rd(p[*].marked); + ensures x != null ==> x in p && ! x.marked; + ensures x == null ==> (forall n in p :: n.marked); + { + assume false; // magic! + } +} diff --git a/Chalice/tests/refinements/original/DSW3.chalice b/Chalice/tests/refinements/original/DSW3.chalice new file mode 100644 index 00000000..dbf161cd --- /dev/null +++ b/Chalice/tests/refinements/original/DSW3.chalice @@ -0,0 +1,106 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// Add arbitrary number of children, not just two. +// Remove visited field for visited nodes; next node is selected non-deterministically +// Added parent pointer p (stack remains) +// Note: the challenge is to update children field of nodes on stack so that we can recover +// parent pointer in pop operation +// Add parent field to Node and made stack ghost (verification time 80s, limited functions) +class Node { + var children: seq<Node>; + var marked: bool; + var parent: Node; + ghost var path: seq<Node>; +} + +class Main { + function Reachable(to: Node, p:seq<Node>, from: Node): bool + requires acc(p[*].children); + { + |p| == 0 ? to == from : + (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from)) + } + + method SchorrWaite(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); + requires forall n in S :: ! n.marked && n.parent == null; + ensures acc(S[*].*); + // graph structure is the same + ensures forall n in S :: n.children == old(n.children); + ensures forall n in S :: n.parent == null; + // all nodes reachable from root are marked + ensures root.marked; + ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked); + // all marked nodes are reachable from root + ensures forall n in S :: n.marked ==> (forall m in n.path :: m in S) && Reachable(n, n.path, root); + { + var p:Node := null; + var t:Node := root; + t.marked := true; + ghost var stack: seq<Node> := []; + t.path := stack; + + // no termination check + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked; + invariant t in S && t.marked && t !in stack; + // stack well-formed + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + invariant forall n in stack :: n in S && n.marked; + invariant forall i in [1..|stack|] :: stack[i-1] in stack[i].children; + invariant forall i in [1..|stack|] :: stack[i-1].parent == stack[i]; + invariant 0 < |stack| ==> p == stack[0] && t in p.children && stack[|stack|-1].parent == null; + invariant 0 == |stack| <==> p == null; + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (forall ch in n.children :: ch in S && ch.marked); + invariant forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && Reachable(n, n.path, root); + invariant forall n in S :: n !in stack ==> n.parent == null; + // preservation + invariant forall n in S :: n.children == old(n.children); + // termination + invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked); + { + call n := PickUnmarked(t.children); + + if (n != null) { + // push + t.parent := p; + p := t; + stack := [t] ++ stack; + n.path := [t] ++ t.path; + t := n; + t.marked := true; + assert Reachable(t.path[0], t.path[1..], root); // limited function + assert forall x in S :: x.marked ==> Reachable(x, x.path, root); + assume forall x in S :: x.marked ==> Reachable(x, x.path, root); + } else { + // pop + if (p == null) { + stop := true; + } else { + t := p; + p := t.parent; + t.parent := null; + stack := stack[1..]; + } + } + } + } + + method PickUnmarked(p: seq<Node>) returns (x: Node) + requires rd(p[*].marked); + requires forall n in p :: n != null; + ensures rd(p[*].marked); + ensures x != null ==> x in p && ! x.marked; + ensures x == null ==> (forall n in p :: n.marked); + { + assume false; + } +} diff --git a/Chalice/tests/refinements/original/DSW4.chalice b/Chalice/tests/refinements/original/DSW4.chalice new file mode 100644 index 00000000..f594595a --- /dev/null +++ b/Chalice/tests/refinements/original/DSW4.chalice @@ -0,0 +1,117 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +// Add arbitrary number of children, not just two. +// Remove visited field for visited nodes; next node is selected non-deterministically +// Added parent pointer p (stack remains) +// Note: the challenge is to update children field of nodes on stack so that we can recover +// parent pointer in pop operation +// Add parent field to Node and made stack ghost (verification time 80s, limited functions) +// Add Reachable that existentially quantifies over paths (verification time 23s, limited functions) +class Node { + var children: seq<Node>; + var marked: bool; + var parent: Node; + var visited: int; + ghost var path: seq<Node>; +} + +class Main { + function Reachable(to: Node, from: Node, S: seq<Node>): bool + requires acc(S[*].children); + { + exists p:seq<Node> :: (forall n in p :: n in S) && Via(to, p, from) + } + + function Via(to: Node, p:seq<Node>, from: Node): bool + requires acc(p[*].children); + { + |p| == 0 ? to == from : + (p[0] != null && to in p[0].children && Via(p[0], p[1..], from)) + } + + method SchorrWaite(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); + requires forall n in S :: ! n.marked && n.parent == null && n.visited == 0; + ensures acc(S[*].*); + // graph structure is the same + ensures forall n in S :: n.children == old(n.children); + ensures forall n in S :: n.parent == null && n.visited == 0; + // all nodes reachable from root are marked + ensures root.marked; + ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked); + // all marked nodes are reachable from root + ensures forall n in S :: n.marked ==> (forall m in n.path :: m in S) && Reachable(n, root, S); + { + var p:Node := null; + var t:Node := root; + t.marked := true; + ghost var stack: seq<Node> := []; + t.path := stack; + + // no termination check + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked; + invariant t in S && t.marked && t !in stack; + // stack well-formed + invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j]; + invariant forall n in stack :: n in S && n.marked; + invariant forall i in [1..|stack|] :: stack[i-1] in stack[i].children; + invariant forall i in [1..|stack|] :: stack[i-1].parent == stack[i]; + invariant 0 < |stack| ==> p == stack[0] && t in p.children && stack[|stack|-1].parent == null; + invariant 0 == |stack| <==> p == null; + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (forall ch in n.children :: ch in S && ch.marked); + invariant forall n in S :: n.marked ==> + (forall m in n.path :: m in S) && Via(n, n.path, root); + invariant forall n in S :: n !in stack ==> n.parent == null; + // preservation + invariant forall n in S :: n.children == old(n.children) && n.visited == 0; + // termination + invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked); + { + call n := PickUnmarked(t, t.children); + + if (n != null) { + // push + t.parent := p; + p := t; + stack := [t] ++ stack; + n.path := [t] ++ t.path; + t := n; + t.marked := true; + assert Via(t.path[0], t.path[1..], root); // limited function + assert forall x in S :: x.marked ==> Via(x, x.path, root); + assume forall x in S :: x.marked ==> Via(x, x.path, root); + } else { + // pop + if (p == null) { + stop := true; + } else { + t := p; + p := t.parent; + t.parent := null; + stack := stack[1..]; + } + } + } + } + + method PickUnmarked(n: Node, p: seq<Node>) returns (x: Node) + requires rd(p[*].marked, 50); + requires rd(n.*, 50); + requires forall q in p :: q != null; + requires p == n.children; + ensures rd(p[*].marked, 50); + ensures rd(n.*, 50); + ensures x != null ==> x in p && ! x.marked; + ensures x == null ==> (forall q in p :: q.marked); + { + assume false; + } +} diff --git a/Chalice/tests/refinements/original/List.chalice b/Chalice/tests/refinements/original/List.chalice new file mode 100644 index 00000000..efcec2c8 --- /dev/null +++ b/Chalice/tests/refinements/original/List.chalice @@ -0,0 +1,159 @@ +/**
+Interesting issues:
+ * using functions in refinement to write getters
+ * using functions to write coupling invariant
+ * refining to a recursive implementation
+ * restricting refinement (List1 must have at least one item)
+ * refining a method with an output variable
+
+Do we shadows the abstract variables in the later concrete programs?
+
+How do we handle generic sequence in List2
+*/
+
+class List0 {
+ var rep: seq<int>;
+
+ method init()
+ requires acc(this.*);
+ ensures acc(rep);
+ {
+ rep := [0];
+ }
+
+ function length(): int
+ requires acc(rep);
+ {
+ |rep|
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(rep);
+ requires 0 <= i && i < length();
+ ensures acc(rep);
+ {
+ v := rep[i];
+ }
+
+ method pick() returns (v: int)
+ requires acc(rep);
+ ensures acc(rep);
+ {
+ var i: int;
+ assume 0 <= i && i < length();
+ v := rep[i];
+ }
+}
+
+class List1 {
+ ghost var rep: seq<int>;
+
+ var data: int;
+ var l: seq<List1>;
+
+ function inv(): bool
+ requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l);
+ {
+ /** valid */ |l| >= 0 &&
+ (forall i in [0..|l|] :: l[i] != null && l[i].l == l[i+1..]) &&
+ /** coupling */ |l| + 1 == |rep| &&
+ (forall i in [0..|l|] :: l[i].data == rep[i+1]) &&
+ data == rep[0]
+ }
+
+ method init()
+ requires acc(this.*);
+ ensures acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
+ {
+ rep := [0];
+ data := 0;
+ l := nil<List1>;
+ }
+
+ function length(): int
+ requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
+ {
+ |l| + 1
+ }
+
+ method checkLength()
+ requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
+ {
+ assert |l| + 1 == |rep|;
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
+ requires 0 <= i && i < length();
+ ensures acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
+ {
+ if (i == 0) {
+ v := data;
+ } else {
+ v := l[i-1].data;
+ }
+ assert v == rep[i];
+ }
+}
+
+class List2 {
+ // ghost var rep: seq<int>;
+ ghost var l: seq<List2>;
+
+ var data: int;
+ var next: List2;
+ var size: int;
+
+ function inv(): bool
+ requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next);
+ {
+ /** valid */ |l| >= 0 &&
+ (forall i in [0..|l|] :: l[i] != null && l[i].l == l[i+1..]) &&
+ /** new coupling */ size == |l| + 1 &&
+ (next == null ==> |l| == 0) &&
+ (next != null ==> |l| > 0 && next == l[0] && l[|l|-1].next == null) &&
+ (forall i in [0..|l|] :: l[i].size == size - i - 1) &&
+ (forall i in [0..|l|-1] :: l[i].next == l[i+1])
+ }
+
+ method init()
+ requires acc(this.*);
+ ensures acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
+ {
+ data := 0;
+ l := nil<List2>;
+ next := null;
+ size := 1;
+ }
+
+ function length(): int
+ requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
+ {
+ size
+ }
+
+ method checkLength()
+ requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
+ {
+ assert size == |l| + 1;
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
+ requires 0 <= i && i < length();
+ ensures acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
+ /** loop invariant: assertion on coupling of abstract and concrete outputs */
+ ensures i == 0 ==> v == data;
+ ensures i > 0 ==> i-1 < |l| && l[i-1] != null && v == l[i-1].data;
+ {
+ if (i == 0) {
+ v := data;
+ } else {
+ assert next != null;
+ assert l == [next] ++ next.l;
+ call w := next.get(i-1);
+ v := w;
+ }
+ }
+}
+
diff --git a/Chalice/tests/refinements/original/ListNode.chalice b/Chalice/tests/refinements/original/ListNode.chalice new file mode 100644 index 00000000..ae72fe67 --- /dev/null +++ b/Chalice/tests/refinements/original/ListNode.chalice @@ -0,0 +1,163 @@ +/**
+Interesting issues:
+ * recursive functions should either use read accesses or provide frame conditions of operating on the same state
+ * carrying super-abstract state might be beneficial for the proof in the concrete program
+ * proofs of function refinement might be needed as lemmas in places where they are used
+*/
+
+class List0 {
+ var rep: seq<int>;
+
+ method init()
+ requires acc(this.*);
+ ensures acc(rep);
+ {
+ rep := [0];
+ }
+
+ function length(): int
+ requires acc(rep);
+ {
+ |rep|
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(rep);
+ requires 0 <= i && i < length();
+ ensures acc(rep);
+ {
+ v := rep[i];
+ }
+
+ method pick() returns (v: int)
+ requires acc(rep);
+ ensures acc(rep);
+ {
+ var i: int;
+ assume 0 <= i && i < length();
+ v := rep[i];
+ }
+}
+
+class Node1 {
+ var data;
+}
+
+class List1 {
+ ghost var rep: seq<int>;
+ var l: seq<Node1>;
+
+ function inv(): bool
+ requires acc(rep) && acc(l) && acc(l[*].data);
+ {
+ /** valid */ (forall i in [0..|l|] :: l[i] != null) &&
+ /** coupling */ |l| == |rep| && (forall i in [0..|l|] :: l[i].data == rep[i])
+ }
+
+ method init()
+ requires acc(this.*);
+ ensures acc(rep) && acc(l) && acc(l[*].data) && inv();
+ {
+ rep := nil<int>;
+ l := nil<Node1>;
+ }
+
+ function length(): int
+ requires acc(rep) && acc(l) && acc(l[*].data) && inv();
+ {
+ |l|
+ }
+
+ method checkLength()
+ requires acc(rep) && acc(l) && acc(l[*].data) && inv();
+ {
+ assert length() == |rep|;
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(rep) && acc(l) && acc(l[*].data) && inv();
+ requires 0 <= i && i < length();
+ ensures acc(rep) && acc(l) && acc(l[*].data) && inv();
+ {
+ v := l[i].data;
+ assert v == rep[i];
+ }
+}
+
+class Node2 {
+ var data;
+ var next: Node2;
+}
+
+class List2 {
+ ghost var rep: seq<int>;
+ ghost var l: seq<Node2>;
+
+ var head: Node2;
+ var size: int;
+
+ function inv(): bool
+ requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size)
+ {
+ /** valid */ (forall i in [0..|l|] :: l[i] != null) &&
+ /** coupling */ |l| == |rep| && (forall i in [0..|l|] :: l[i].data == rep[i]) &&
+ /** new coupling */ size == |l| &&
+ (head == null ==> |l| == 0) &&
+ (head != null ==> |l| > 0 && head == l[0] && l[|l|-1].next == null) &&
+ (forall i in [0..|l|-1] :: l[i].next == l[i+1])
+ }
+
+ method init()
+ requires acc(this.*);
+ ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ {
+ rep := nil<int>;
+ l := nil<Node2>;
+ head := null;
+ size := 0;
+ }
+
+ function length(): int
+ requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ {
+ size
+ }
+
+ method checkLength()
+ requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ {
+ assert length() == |l|;
+ }
+
+ method get(i: int) returns (v: int)
+ requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ requires 0 <= i && i < length();
+ ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ {
+ call v := getrec(i, head, 0);
+ assert v == l[i].data;
+ }
+
+ method getrec(i: int, n: Node2, /* ghost */ j: int) returns (v: int)
+ requires acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ requires length() == |l|;
+ requires 0 <= i && i < length();
+ requires 0 <= j && j <= i;
+ requires l[j] == n;
+ ensures acc(rep) && acc(l) && acc(l[*].data) && acc(l[*].next) && acc(head) && acc(size) && inv();
+ // frame
+ ensures l == old(l);
+ ensures forall x in l :: x != null && x.data == old(x.data) && x.next == old(x.next);
+ ensures size == old(size);
+ ensures head == old(head);
+ ensures rep == old(rep);
+ ensures v == l[i].data;
+ ensures l == old(l);
+ {
+ if (i == j) {
+ v := n.data;
+ } else {
+ call v := getrec(i, n.next, j+1);
+ }
+ }
+}
diff --git a/Chalice/tests/refinements/original/ListPredicate.chalice b/Chalice/tests/refinements/original/ListPredicate.chalice new file mode 100644 index 00000000..af334093 --- /dev/null +++ b/Chalice/tests/refinements/original/ListPredicate.chalice @@ -0,0 +1,109 @@ +/* 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 append(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.append(x);
+ }
+ fold this.valid;
+ }
+
+ method prepend(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)
+ }
+
+ 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)
+ }
+}
+
+// abstract sequence of integers
+class LinkedList {
+ ghost var rep: seq<int>;
+
+ var first: Node;
+
+ method init()
+ requires acc(this.*);
+ ensures valid;
+ {
+ first := null;
+ assert coupling(rep, first);
+ fold valid;
+ }
+
+ method append(x: int)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ rep := rep ++ [x];
+ fold valid;
+ }
+
+ method prepend(x: int)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ rep := [x] ++ rep;
+ fold valid;
+ }
+
+ predicate valid {
+ acc(rep) && acc(first) && (first != null ==> first.valid)
+ }
+
+ function coupling(a: seq<int>, c: Node) : bool
+ requires c != null ==> c.valid;
+ {
+ c == null ? a == nil<int> :
+ (|a| > 0 && a[0] == c.value && coupling(a[1..], c.next))
+ }
+
+
+}
diff --git a/Chalice/tests/refinements/original/StringBuilder.chalice b/Chalice/tests/refinements/original/StringBuilder.chalice new file mode 100644 index 00000000..d73f8373 --- /dev/null +++ b/Chalice/tests/refinements/original/StringBuilder.chalice @@ -0,0 +1,67 @@ +class Char {} +class StringBuilder0 { + var rep: seq<Char>; + method Init() + requires acc(rep); + ensures acc(rep); + { rep := nil<Char>; } + function ToString(): seq<Char> + requires rd(rep); + { rep } + method Append(chars: seq<Char>) + requires acc(rep); + ensures acc(rep); + ensures ToString() == old(ToString()) ++ chars; + { rep := rep ++ chars; } +} + +class Chunk0 { + var rep: seq<Char>; + ghost var start; +} + + +class StringBuilder1 refines StringBuilder0 { + var chunks: seq<Chunk0>; + + replaces rep by acc(chunks) && acc(chunks[*].rep) && acc(chunks[*].start) && + /** representation invariant */ null !in chunks && |chunks| > 0 && + chunks[0].start == 0 && + (forall i in [0..|chunks|-1] :: chunks[i+1].start == chunks[i].start + |chunks[i].rep|) && + /** coupling invariant */ (forall c in chunks :: c.rep == rep[c.start..c.start + |c.rep|]) + + refines Init() + { + var c := new Chunk0; + c.rep := nil<Char>; + c.start := 0; + chunks := [c]; + rep := nil<Char>; + } + + + refines Append(chars: seq<Char>) + { + rep := rep ++ chars; + var i; assume 0 <= i && i < |chars|; + if (i > 0) { + call AppendChunk(chunks[|chunks|-1], chars[..i]); + } + if (i < |chars| - 1) { + call ExpandByABlock(); + call AppendChunk(chunks[|chunks|-1], chars[i..]); + } + } + + method AppendChunk(ch: Chunk0, chars: seq<Char>) + { + ch.rep := ch.rep ++ chars; + } + + method ExpandByABlock() + { + var c := new Chunk0; + c.rep := nil<Char>; + chunks := chunks ++ [c]; + } +}
\ No newline at end of file diff --git a/Chalice/tests/refinements/test.sh b/Chalice/tests/refinements/test.sh new file mode 100644 index 00000000..8ebef27a --- /dev/null +++ b/Chalice/tests/refinements/test.sh @@ -0,0 +1,52 @@ +#!/usr/bin/bash + +# Regression tests for refinement extension +# Author: Kuat Yessenov + +TESTS=" + LoopSqRoot.chalice + RecSqRoot.chalice + SpecStmt.chalice + SumCubes.chalice + TestTransform.chalice + TestRefines.chalice + RecFiniteDiff.chalice + LoopFiniteDiff.chalice + Pick.chalice + TestCoupling.chalice + Calculator.chalice + AngelicExec.chalice +" + +# Switch to test directory +CURRENT=`pwd` +cd `dirname $0` + +# Remove stale output file +if [ -f Output ] +then + rm -f Output +fi + +# Process tests +START=`date +%s` +for f in ${TESTS} +do + echo "Processing $f" | tee -a Output + scala -cp ../bin chalice.Chalice -nologo -noTermination $f >> Output 2>&1 +done +END=`date +%s` +echo "Time: $(( $END - $START )) seconds" + +# Compare with answer +if diff Output Answer +then + rm Output + rm out.bpl + echo Success +else + echo Failure +fi + +# Switch back to current directory +cd ${CURRENT} diff --git a/Chalice/tests/test-scripts/diff.bat b/Chalice/tests/test-scripts/diff.bat new file mode 100644 index 00000000..87fa935f --- /dev/null +++ b/Chalice/tests/test-scripts/diff.bat @@ -0,0 +1,21 @@ +@echo off
+
+set differ="C:\Program Files\TortoiseSVN\bin\TortoiseMerge.exe"
+if exist %differ% goto :diff
+if not exist %differ% goto :txtdiff
+
+:txtdiff
+echo ====================================
+echo Reference output: %1
+echo ------------------------------------
+type "%1"
+echo ====================================
+echo Currenct output: %2
+echo ------------------------------------
+type "%2"
+echo ====================================
+goto :eof
+
+:diff
+%differ% "%1" "%2"
+goto :eof
diff --git a/Chalice/tests/test-scripts/generate_reference.bat b/Chalice/tests/test-scripts/generate_reference.bat new file mode 100644 index 00000000..a2e9c443 --- /dev/null +++ b/Chalice/tests/test-scripts/generate_reference.bat @@ -0,0 +1,8 @@ +@echo off
+
+set getboogieoutput="%~dp0\getboogieoutput.bat"
+
+echo Generating reference for %1.chalice ...
+call %getboogieoutput% %1 %2 %3 %4 %5 %6 %7
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/generate_reference_all.bat b/Chalice/tests/test-scripts/generate_reference_all.bat new file mode 100644 index 00000000..83b04700 --- /dev/null +++ b/Chalice/tests/test-scripts/generate_reference_all.bat @@ -0,0 +1,10 @@ +@echo off
+
+set getboogieoutput="%~dp0\getboogieoutput.bat"
+
+for /F %%f in ('dir *.chalice /b') do (
+ echo Generating reference for %%~nf.chalice ...
+ call %getboogieoutput% %%~nf %1 %2 %3 %4 %5 %6 %7
+)
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/getboogieoutput.bat b/Chalice/tests/test-scripts/getboogieoutput.bat new file mode 100644 index 00000000..eb7d99a4 --- /dev/null +++ b/Chalice/tests/test-scripts/getboogieoutput.bat @@ -0,0 +1,13 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+
+set output="%1.output.txt"
+
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 >> %output% 2>&1
+
+set o=%~dp1%out.bpl
+if exist "%o%" copy "%o%" "%1.bpl">nul
+if exist "%o%" del "%~dp1%out.bpl"
diff --git a/Chalice/tests/test-scripts/reg_test.bat b/Chalice/tests/test-scripts/reg_test.bat new file mode 100644 index 00000000..d31773da --- /dev/null +++ b/Chalice/tests/test-scripts/reg_test.bat @@ -0,0 +1,43 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+set diff="%~dp0\diff.bat"
+
+if not exist "%1.chalice" goto errorNotFound
+if not exist "%1.output.txt" goto errorNoRef
+
+set output=output.txt
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+
+fc "%1.output.txt" output.txt > nul
+if not errorlevel 1 goto passTest
+goto failTest
+
+:passTest
+echo OK: %1.chalice
+goto end
+
+:failTest
+echo FAIL: %1.chalice
+call %diff% "%1.output.txt" output.txt
+goto errorEnd
+
+:errorEnd
+if exist out.bpl del out.bpl
+if exist output.txt del output.txt
+exit /b 1
+
+:end
+if exist out.bpl del out.bpl
+if exist output.txt del output.txt
+exit /b 0
+
+:errorNotFound
+echo ERROR: %1.chalice not found.
+goto errorEnd
+
+:errorNoRef
+echo ERROR: %1.output.txt (reference output) not found.
+goto errorEnd
diff --git a/Chalice/tests/test-scripts/reg_test_all.bat b/Chalice/tests/test-scripts/reg_test_all.bat new file mode 100644 index 00000000..6bbac775 --- /dev/null +++ b/Chalice/tests/test-scripts/reg_test_all.bat @@ -0,0 +1,9 @@ +@echo off
+
+set regtest="%~dp0\reg_test.bat"
+
+for /F %%f in ('dir *.chalice /b') do (
+ call %regtest% %%~nf %1 %2 %3 %4 %5 %6 %7 %8
+)
+
+exit /b 0
diff --git a/Chalice/tests/test-scripts/test.bat b/Chalice/tests/test-scripts/test.bat new file mode 100644 index 00000000..321fdcef --- /dev/null +++ b/Chalice/tests/test-scripts/test.bat @@ -0,0 +1,17 @@ +@echo off
+
+set chalice="%~dp0\..\..\chalice.bat"
+
+if not exist "%1.chalice" goto errorNotFound
+
+set output=output.txt
+echo Verification of %1.chalice > %output%
+echo.>> %output%
+call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+type %output%
+
+exit /B 0
+
+:errorNotFound
+echo ERROR: %1.chalice not found.
+exit /B 1
|