Skip to content

Commit 2c883ca

Browse files
committed
Fix exemption logic for all DerivedCapabilities
1 parent a539295 commit 2c883ca

File tree

2 files changed

+52
-2
lines changed

2 files changed

+52
-2
lines changed

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -570,7 +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)
573+
case d: DerivedCapability => consumedByPath(d.underlying)
574574
case ref: TermRef =>
575575
def recur(tp: Type, acc: Refs): Refs = tp match
576576
case ref: TermRef =>
@@ -669,7 +669,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
669669
// We need to check both the capability and its reach, since consumed might store the reach version.
670670
val shouldExempt = pathConsumed.exists:
671671
case _: RootCapability => false
672-
case cap => consumed.get(cap) == pos || consumed.get(cap.reach) == pos
672+
case c: DerivedCapability => consumed.get(c.underlying) == pos
673+
case c => consumed.get(c) == pos
673674

674675
if !shouldExempt then
675676
consumeError(ref, pos, tree.srcPos)
Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
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.b) // ok
42+
println(a5.b) // ok
43+
44+
println(b) // error
45+
println(b2) // error
46+
println(b3) // error
47+
println(b4) // error
48+
println(b5) // error (currently accepted!!!)
49+
println(b6) // error (currently accepted!!!)

0 commit comments

Comments
 (0)