Skip to content

Commit f7db3fd

Browse files
committed
Add more tests for consume constructor parameters
1 parent d54f0fc commit f7db3fd

File tree

2 files changed

+153
-0
lines changed

2 files changed

+153
-0
lines changed
Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
import scala.caps.Mutable
5+
6+
// Create a deeper nesting structure
7+
class D()
8+
class C(val d: D^)
9+
class B(val c: C^)
10+
class A(consume val b: B^) extends Mutable:
11+
update def use() = println("Using A")
12+
13+
// Test 1: Accessing nested fields through a consumed path
14+
def testNestedFieldsAfterConsume =
15+
val d: D^ = D()
16+
val c: C^ = C(d)
17+
val b: B^ = B(c)
18+
val a = A(b)
19+
20+
// After a consumed b, we should be able to access:
21+
println(a.b) // OK - a owns b
22+
println(a.b.c) // OK - accessing field of consumed b through a
23+
println(a.b.c.d) // OK - deeper nesting through consumed path
24+
25+
// Test 2: Non-trivial prefix accessing a consumed field
26+
class Container(consume val a: A^) extends Mutable:
27+
val other: A^ = A(B(C(D())))
28+
update def operate() = other.use()
29+
30+
class Outer(consume val container: Container^) extends Mutable:
31+
update def execute() = container.operate()
32+
33+
def testComplexPrefix =
34+
val d1: D^ = D()
35+
val c1: C^ = C(d1)
36+
val b1: B^ = B(c1)
37+
val a1 = A(b1)
38+
val container1 = Container(a1)
39+
val outer = Outer(container1)
40+
41+
// Non-trivial prefix: outer.container.a (where 'a' was consumed by container)
42+
println(outer.container) // OK - outer consumed container
43+
println(outer.container.a) // OK - accessing consumed field through prefix
44+
println(outer.container.a.b) // OK - and then its nested fields
45+
println(outer.container.a.b.c) // OK - even deeper
46+
println(outer.container.a.b.c.d) // OK - deepest level
47+
48+
println(container1) // error
49+
println(a1) // error
50+
51+
// Test 3: Multiple consume parameters with nested access
52+
class Multi(consume val b1: B^, consume val b2: B^) extends Mutable:
53+
val b3: B^ = B(C(D()))
54+
update def combine() = ()
55+
56+
def testMultipleConsume =
57+
val b1: B^ = B(C(D()))
58+
val b2: B^ = B(C(D()))
59+
val multi = Multi(b1, b2)
60+
61+
// All of these should work:
62+
println(multi.b1) // OK
63+
println(multi.b1.c) // OK - nested field of consumed b1
64+
println(multi.b1.c.d) // OK - deeper nesting
65+
println(multi.b2) // OK
66+
println(multi.b2.c) // OK - nested field of consumed b2
67+
println(multi.b2.c.d) // OK - deeper nesting
68+
println(multi.b3.c.d) // OK - non-consumed field
69+
70+
println(b1) // error
71+
println(b2) // error
72+
73+
// Test 4: Consume at multiple levels with complex paths
74+
class Top(consume val outer: Outer^) extends Mutable:
75+
update def topAction() = outer.execute()
76+
77+
def testMultiLevelConsume =
78+
val d2: D^ = D()
79+
val c2: C^ = C(d2)
80+
val b2: B^ = B(c2)
81+
val a2 = A(b2)
82+
val container2 = Container(a2)
83+
val outer2 = Outer(container2)
84+
val top = Top(outer2)
85+
86+
// Very deep path through multiple consume levels:
87+
println(top.outer) // OK - top consumed outer
88+
println(top.outer.container) // OK - continue through path
89+
println(top.outer.container.a) // OK - container consumed a
90+
println(top.outer.container.a.b) // OK - a consumed b
91+
println(top.outer.container.a.b.c) // OK - nested field
92+
println(top.outer.container.a.b.c.d) // OK - deepest field
93+
94+
println(a2) // error
95+
println(container2) // error
96+
println(outer2) // error
97+
println(top) // ok
Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.*
4+
5+
class Foo extends ExclusiveCapability, Classifier
6+
7+
// Testing with various DerivedCapabilities
8+
class D
9+
class C(val d: D)
10+
class B(val c: C) extends Foo, Mutable:
11+
update def foo() = println("foo")
12+
class A(consume val b: B^) extends Mutable:
13+
update def bar() = b.foo()
14+
class A2(consume val b: B^) extends Mutable:
15+
update def bar() = b.foo()
16+
class A3(consume var b: B^) extends Mutable:
17+
update def bar() = b.foo()
18+
class A4(consume val b: A2^{cap.only[Foo]}) extends Mutable: // FIXME needs to be classified as Foo, too
19+
update def bar() = b.b.foo()
20+
21+
// Test: Access nested fields (suffix paths) after consume
22+
def testSuffixPaths =
23+
val d: D = D()
24+
val c: C = C(d)
25+
val b: B^ = B(c)
26+
val a1 = A(b)
27+
val b2: B^ = B(c)
28+
val a2 = A2(b2)
29+
val b3: B^ = B(c)
30+
val a3 = A3(b3)
31+
val b4: B^ = B(c)
32+
val a22 = A2(b4)
33+
//val a4 = A4(a22) // FIXME should work?
34+
val b5: B^{cap.only[Foo]} = B(c)
35+
val a5 = A(b5)
36+
val b6: B^{cap.only[Foo]} = B(c)
37+
val a222 = A2(b6)
38+
//val a6 = A4(a222) // FIXME should work?
39+
40+
41+
println(a1.b) // ok
42+
println(a2.b) // ok
43+
println(a3.b) // ok
44+
//println(a4.b) // ok needs fixing
45+
//println(a4.b.b) // ok needs fixing
46+
println(a5.b) // ok
47+
// println(a6.b) // ok needs fixing
48+
// println(a6.b.b) // ok needs fixing
49+
50+
println(b) // error
51+
println(b2) // error
52+
println(b3) // error
53+
println(b4) // error
54+
println(b5) // error
55+
println(b6) // error
56+
//println(a222) // should error, but doesn't work yet

0 commit comments

Comments
 (0)