Skip to content

Commit d43dfe3

Browse files
committed
Add tests for consume in constructor parameters
1 parent 4636639 commit d43dfe3

File tree

5 files changed

+227
-0
lines changed

5 files changed

+227
-0
lines changed
Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
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^)
15+
class A3(consume var b: B^)
16+
class A4(consume val b: A2^{cap.only[Foo]})
17+
18+
// Test: Access nested fields (suffix paths) after consume
19+
def testSuffixPaths =
20+
val d: D = D()
21+
val c: C = C(d)
22+
val b: B^ = B(c)
23+
val a1 = A(b)
24+
val b2: B^ = B(c)
25+
val a2 = A2(b2) // the difference is that we pass b2.rd
26+
val b3: B^ = B(c)
27+
val a3 = A3(b3)
28+
val b4: B^ = B(c)
29+
val a22 = A2(b4)
30+
val a4 = A4(a22)
31+
val b5: B^{cap.only[Foo]} = B(c)
32+
val a5 = A(b5)
33+
val b6: B^{cap.only[Foo]} = B(c)
34+
val a222 = A2(b6)
35+
val a6 = A4(a222)
36+
37+
38+
println(a1.b) // ok
39+
println(a2.b) // ok
40+
println(a3.b) // ok
41+
println(a4.b) // ok
42+
println(a4.b.b) // ok
43+
println(a5.b) // ok
44+
println(a6.b) // ok
45+
println(a6.b.b) // ok
46+
47+
println(b) // error
48+
println(b2) // error
49+
println(b3) // error
50+
println(b4) // error
51+
//println(b5) // should error (currently accepted!!!)
52+
//println(b6) // should error (currently accepted!!!)
53+
//println(a222) // should error (currently accepted!!!)
Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
// Create a deeper nesting structure
6+
class D()
7+
class C(val d: D^)
8+
class B(val c: C^)
9+
class A(consume val b: B^)
10+
11+
// Test 1: Accessing nested fields through a consumed path
12+
def testNestedFieldsAfterConsume =
13+
val d: D^ = D()
14+
val c: C^ = C(d)
15+
val b: B^ = B(c)
16+
val a = A(b)
17+
18+
// After a consumed b, we should be able to access:
19+
println(a.b) // OK - a owns b
20+
println(a.b.c) // OK - accessing field of consumed b through a
21+
println(a.b.c.d) // OK - deeper nesting through consumed path
22+
23+
// Test 2: Non-trivial prefix accessing a consumed field
24+
class Container(consume val a: A^):
25+
val other: A^ = A(B(C(D())))
26+
27+
class Outer(consume val container: Container^)
28+
29+
def testComplexPrefix =
30+
val d1: D^ = D()
31+
val c1: C^ = C(d1)
32+
val b1: B^ = B(c1)
33+
val a1 = A(b1)
34+
val container1 = Container(a1)
35+
val outer = Outer(container1)
36+
37+
// Non-trivial prefix: outer.container.a (where 'a' was consumed by container)
38+
println(outer.container) // OK - outer consumed container
39+
println(outer.container.a) // OK - accessing consumed field through prefix
40+
println(outer.container.a.b) // OK - and then its nested fields
41+
println(outer.container.a.b.c) // OK - even deeper
42+
println(outer.container.a.b.c.d) // OK - deepest level
43+
44+
// Test 3: Multiple consume parameters with nested access
45+
class Multi(consume val b1: B^, consume val b2: B^):
46+
val b3: B^ = B(C(D()))
47+
48+
def testMultipleConsume =
49+
val b1: B^ = B(C(D()))
50+
val b2: B^ = B(C(D()))
51+
val multi = Multi(b1, b2)
52+
53+
// All of these should work:
54+
println(multi.b1) // OK
55+
println(multi.b1.c) // OK - nested field of consumed b1
56+
println(multi.b1.c.d) // OK - deeper nesting
57+
println(multi.b2) // OK
58+
println(multi.b2.c) // OK - nested field of consumed b2
59+
println(multi.b2.c.d) // OK - deeper nesting
60+
println(multi.b3.c.d) // OK - non-consumed field
61+
62+
// Test 4: Consume at multiple levels with complex paths
63+
class Top(consume val outer: Outer^)
64+
65+
def testMultiLevelConsume =
66+
val d2: D^ = D()
67+
val c2: C^ = C(d2)
68+
val b2: B^ = B(c2)
69+
val a2 = A(b2)
70+
val container2 = Container(a2)
71+
val outer2 = Outer(container2)
72+
val top = Top(outer2)
73+
74+
// Very deep path through multiple consume levels:
75+
println(top.outer) // OK - top consumed outer
76+
println(top.outer.container) // OK - continue through path
77+
println(top.outer.container.a) // OK - container consumed a
78+
println(top.outer.container.a.b) // OK - a consumed b
79+
println(top.outer.container.a.b.c) // OK - nested field
80+
println(top.outer.container.a.b.c.d) // OK - deepest field
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
class B
6+
7+
class A(consume val b: B^):
8+
val bb: B^ = B()
9+
10+
class C(consume val a: A^):
11+
val aa: A^ = A(B())
12+
13+
// Test deep nested access paths
14+
def testDeepPaths =
15+
val b: B^ = B()
16+
val a = A(b)
17+
val c = C(a)
18+
19+
// All these should work - accessing through ownership chain
20+
println(c.a) // c owns a
21+
println(c.a.b) // c owns a, a owns b
22+
println(c.a.bb) // c owns a, accessing other field
23+
println(c.aa) // accessing other field of c
24+
println(c.aa.b) // accessing nested field through c.aa
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
class B
6+
7+
class A(consume val b: B^):
8+
val bb: B^ = B()
9+
10+
class C(consume val a: A^):
11+
val aa: A^ = A(B())
12+
13+
// Test: After consuming b into a, then consuming a into c,
14+
// we should be able to access c.a.b (nested field selection)
15+
def testNestedAccess =
16+
val b: B^ = B()
17+
val a = A(b)
18+
println(a.b) // OK - a consumed b, accessing through a
19+
val c = C(a)
20+
println(c.a) // Should be OK - c consumed a, accessing through c
21+
println(c.a.b) // Should be OK - accessing b through c.a, where c owns a and a owns b
22+
23+
// Test: The deeper path c.a.b should work even though a was consumed
24+
def testDeepPath =
25+
val b: B^ = B()
26+
val a = A(b)
27+
val c = C(a)
28+
// At this point:
29+
// - b was consumed by a (so we can't use b directly)
30+
// - a was consumed by c (so we can't use a directly)
31+
// But we should be able to access:
32+
println(c.a.b) // OK - full path through ownership chain
33+
println(c.a.bb) // OK - other field of c.a
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
// Create a deep nesting structure for testing suffix paths
6+
class D
7+
class C(val d: D^)
8+
class B(val c: C^)
9+
class A(consume val b: B^)
10+
11+
// Test 1: Simple suffix paths after consume
12+
def test1 =
13+
val d: D^ = D()
14+
val c: C^ = C(d)
15+
val b: B^ = B(c)
16+
val a = A(b)
17+
18+
// After 'a' consumes 'b', access nested fields:
19+
println(a.b) // OK - consumed field
20+
println(a.b.c) // OK - suffix: .c after consumed field
21+
println(a.b.c.d) // OK - suffix: .c.d after consumed field
22+
23+
// Test 2: Non-consume wrapper with consumed inner field
24+
class Holder(val a: A^) // Note: NOT consume
25+
26+
def test2 =
27+
val d: D^ = D()
28+
val c: C^ = C(d)
29+
val b: B^ = B(c)
30+
val a = A(b)
31+
val holder = Holder(a)
32+
33+
// Access through holder.a.b where b was consumed by a:
34+
println(holder.a) // OK - not consumed
35+
println(holder.a.b) // OK - accessing consumed field through prefix
36+
println(holder.a.b.c) // OK - suffix .c
37+
println(holder.a.b.c.d) // OK - suffix .c.d

0 commit comments

Comments
 (0)