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/permission-model | |
| 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/permission-model')
31 files changed, 1170 insertions, 0 deletions
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" %*
|