Skip to content

Commit d40f1f9

Browse files
committed
Also drop read-only versions of shared capabilities from separation checking
We do get sometimes capabilities like `async.rd` where `async` is shared. It does not look straightforward to prevent that, so instead we count async.rd as shared if async is.
1 parent 9f0adf6 commit d40f1f9

File tree

2 files changed

+24
-2
lines changed

2 files changed

+24
-2
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -638,7 +638,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
638638
val badParams = mutable.ListBuffer[Symbol]()
639639
def currentOwner = role.dclSym.orElse(ctx.owner)
640640
for hiddenRef <- refsToCheck.deduct(explicitRefs(tpe)) do
641-
if !hiddenRef.isKnownClassifiedAs(defn.Caps_SharedCapability) then
641+
if !hiddenRef.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then
642642
hiddenRef.pathRoot match
643643
case ref: TermRef if ref.symbol != role.dclSym =>
644644
val refSym = ref.symbol
@@ -675,7 +675,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
675675
role match
676676
case _: TypeRole.Argument | _: TypeRole.Qualifier =>
677677
for ref <- refsToCheck do
678-
if !ref.isKnownClassifiedAs(defn.Caps_SharedCapability) then
678+
if !ref.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then
679679
consumed.put(ref, pos)
680680
case _ =>
681681
end checkConsumedRefs
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
import caps.*
2+
object Test
3+
4+
class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Mutable:
5+
private val arr: Array[T] = new Array[T](len)
6+
def get(i: Int): T = arr(i)
7+
update def set(i: Int, x: T): Unit = arr(i) = x
8+
9+
class Async extends SharedCapability
10+
11+
def f[T](x: T): T & Pure = x.asInstanceOf[T & Pure]
12+
13+
def test =
14+
def x(async: Async): Arr[String]^{cap.rd} =
15+
val y = Arr[String](async, 10)
16+
for i <- 0 to 10 do
17+
y.set(i, "A")
18+
val z = f(y)
19+
y
20+
21+
22+

0 commit comments

Comments
 (0)