Skip to content

Commit 8b66711

Browse files
committed
Add advanced test case for classifier capabilities
1 parent 11e901f commit 8b66711

File tree

1 file changed

+67
-0
lines changed

1 file changed

+67
-0
lines changed
Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.*
4+
5+
// Test inspired by the "Gentrification Gone too Far?" paper
6+
object Levels:
7+
8+
trait Read extends Classifier, Capability
9+
trait ReadWrite extends Classifier, Capability
10+
11+
trait File(val name: String):
12+
val r: Read^
13+
val rw: ReadWrite^
14+
// operations guarded by boxed capability members
15+
val read: () ->{r} Int
16+
val write: Int ->{rw} Unit
17+
18+
object File:
19+
def apply(s: String): File^ = new File(s) {
20+
val r = new Read {}
21+
val rw = new ReadWrite {}
22+
val read = () =>
23+
println(s"Reading from $name with capability $r")
24+
42
25+
val write = (i: Int) =>
26+
println(s"Writing $i to $name with capability $rw")
27+
}
28+
29+
// Unfortunately, we do not have @use lambdas yet
30+
trait UseFunction[U]:
31+
def apply(@use f: File^): U
32+
33+
def withFile[U](name: String)(block: UseFunction[U]): U = block(File(name)) // unrestricted use of files & other capabilities
34+
def parReduce[U](xs: Seq[U])(op: (U, U) ->{cap.only[Read]} U): U = xs.reduce(op) // only Read-classified allowed
35+
36+
@main def test =
37+
withFile("foo.txt"):
38+
new UseFunction[Unit]:
39+
def apply(@use f: File^): Unit =
40+
f.read() // ok
41+
parReduce(1 to 1000): (a, b) =>
42+
a * b * f.read() // ok
43+
parReduce(1 to 1000): (a, b) => // error
44+
f.write(42) // the error stems from here
45+
a + b + f.read() // ok
46+
f.write(42) // ok, unrestricted access to file
47+
48+
def testMulti =
49+
withFile("foo.txt"):
50+
new UseFunction[Unit]:
51+
def apply(@use f: File^): Unit =
52+
withFile("bar.txt"):
53+
new UseFunction[Unit]:
54+
def apply(@use g: File^): Unit =
55+
f.read() // ok
56+
g.read() // ok
57+
parReduce(1 to 1000): (a, b) =>
58+
a * b * f.read() + g.read() // ok
59+
parReduce(1 to 1000): (a, b) => // error
60+
f.write(42) // the error stems from here
61+
a + b + f.read() + g.read() // ok
62+
parReduce(1 to 1000): (a, b) => // error
63+
g.write(42) // the error stems from here
64+
0
65+
f.write(42) // ok, unrestricted access to file
66+
g.write(42) // ok, unrestricted access to file
67+

0 commit comments

Comments
 (0)