Skip to content

Commit 87012a8

Browse files
committed
Fix consumedByPath to handle reach capabilities
1 parent b7f4d72 commit 87012a8

File tree

2 files changed

+84
-8
lines changed

2 files changed

+84
-8
lines changed

compiler/src/dotty/tools/dotc/cc/SepCheck.scala

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -570,6 +570,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
570570
* @return The set of actual consumed capabilities from all consume fields along the path
571571
*/
572572
def consumedByPath(cap: Capability)(using Context): Refs = cap match
573+
case Reach(underlying) => consumedByPath(underlying)
573574
case ref: TermRef =>
574575
def recur(tp: Type, acc: Refs): Refs = tp match
575576
case ref: TermRef =>
@@ -606,7 +607,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
606607
// Return both the capabilities in the capture set AND what they transitively consume
607608
var result = emptyRefs
608609
for cap <- captureSet do
609-
// Stop at cap - don't include fresh root capabilities
610610
cap match
611611
case _: RootCapability => // Skip
612612
case _ =>
@@ -667,13 +667,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
667667

668668
// Check if any capability consumed by the path was consumed at position `pos`.
669669
// We need to check both the capability and its reach, since consumed might store the reach version.
670-
val shouldExempt = pathConsumed.exists { cap =>
671-
if consumed.get(cap) == pos then
672-
true
673-
else cap match
674-
case _: RootCapability => false // RootCapability.reach is unsupported
675-
case _ => consumed.get(cap.reach) == pos
676-
}
670+
val shouldExempt = pathConsumed.exists:
671+
case _: RootCapability => false
672+
case cap => consumed.get(cap) == pos || consumed.get(cap.reach) == pos
677673

678674
if !shouldExempt then
679675
consumeError(ref, pos, tree.srcPos)
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

0 commit comments

Comments
 (0)