Skip to content

Commit 67d42bd

Browse files
oderskyodersky
committed
Cache derived reach, readOnly, and maybe capabilities
This is necessary since capability sets are IdentitySets.
1 parent 190aaca commit 67d42bd

File tree

5 files changed

+69
-21
lines changed

5 files changed

+69
-21
lines changed

‎compiler/src/dotty/tools/dotc/cc/CaptureOps.scala‎

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -463,7 +463,10 @@ extension (tp: Type)
463463
def reach(using Context): CaptureRef = tp match
464464
case tp @ AnnotatedType(tp1: CaptureRef, annot)
465465
if annot.symbol == defn.MaybeCapabilityAnnot =>
466-
tp.derivedAnnotatedType(tp1.reach, annot)
466+
tp1.reach.maybe
467+
case tp @ AnnotatedType(tp1: CaptureRef, annot)
468+
if annot.symbol == defn.ReadOnlyCapabilityAnnot =>
469+
tp1.reach.readOnly
467470
case tp @ AnnotatedType(tp1: CaptureRef, annot)
468471
if annot.symbol == defn.ReachCapabilityAnnot =>
469472
tp
@@ -476,9 +479,8 @@ extension (tp: Type)
476479
*/
477480
def readOnly(using Context): CaptureRef = tp match
478481
case tp @ AnnotatedType(tp1: CaptureRef, annot)
479-
if annot.symbol == defn.MaybeCapabilityAnnot
480-
|| annot.symbol == defn.ReachCapabilityAnnot =>
481-
tp.derivedAnnotatedType(tp1.readOnly, annot)
482+
if annot.symbol == defn.MaybeCapabilityAnnot =>
483+
tp1.readOnly.maybe
482484
case tp @ AnnotatedType(tp1: CaptureRef, annot)
483485
if annot.symbol == defn.ReadOnlyCapabilityAnnot =>
484486
tp
@@ -710,17 +712,23 @@ object CapsOfApply:
710712
case TypeApply(capsOf, arg :: Nil) if capsOf.symbol == defn.Caps_capsOf => Some(arg)
711713
case _ => None
712714

713-
abstract class AnnotatedCapability(annot: Context ?=> ClassSymbol):
715+
abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
714716
def apply(tp: Type)(using Context): AnnotatedType =
715717
assert(tp.isTrackableRef)
716718
tp match
717-
case AnnotatedType(_, annot) => assert(!unwrappable.contains(annot.symbol))
719+
case AnnotatedType(_, annot) =>
720+
assert(!unwrappable.contains(annot.symbol), i"illegal combination of derived capabilities: $annotCls over ${annot.symbol}")
718721
case _ =>
719-
AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
722+
tp match
723+
case tp: CaptureRef => tp.derivedRef(annotCls)
724+
case _ => AnnotatedType(tp, Annotation(annotCls, util.Spans.NoSpan))
725+
720726
def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
721-
case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annot) => Some(parent)
727+
case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annotCls) => Some(parent)
722728
case _ => None
729+
723730
protected def unwrappable(using Context): Set[Symbol]
731+
end AnnotatedCapability
724732

725733
/** An extractor for `ref @maybeCapability`, which is used to express
726734
* the maybe capability `ref?` as a type.

‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import Periods.NoRunId
1414
import compiletime.uninitialized
1515
import StdNames.nme
1616
import CaptureSet.VarState
17+
import Annotations.Annotation
1718

1819
/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
1920
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
@@ -24,6 +25,18 @@ trait CaptureRef extends TypeProxy, ValueType:
2425
private var myCaptureSet: CaptureSet | Null = uninitialized
2526
private var myCaptureSetRunId: Int = NoRunId
2627
private var mySingletonCaptureSet: CaptureSet.Const | Null = null
28+
private var myDerivedRefs: List[AnnotatedType] = Nil
29+
30+
/** A derived reach, readOnly or maybe reference. Derived references are cached. */
31+
def derivedRef(annotCls: ClassSymbol)(using Context): AnnotatedType =
32+
def recur(refs: List[AnnotatedType]): AnnotatedType = refs match
33+
case ref :: refs1 =>
34+
if ref.annot.symbol == annotCls then ref else recur(refs1)
35+
case Nil =>
36+
val derived = AnnotatedType(this, Annotation(annotCls, util.Spans.NoSpan))
37+
myDerivedRefs = derived :: myDerivedRefs
38+
derived
39+
recur(myDerivedRefs)
2740

2841
/** Is the reference tracked? This is true if it can be tracked and the capture
2942
* set of the underlying type is not always empty.

‎tests/neg-custom-args/captures/i21614.check‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,8 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 ---------------------------------------
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
22
12 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
3-
| ^^^^^^^^^^^^^^^^^^^^^^^
4-
| Found: (f: F) ->{files.rd*} box Logger{val f²: File^?}^?
5-
| Required: (f: box F^{files.rd*}) ->{fresh} box Logger{val f²: File^?}^?
6-
|
7-
| where: f is a reference to a value parameter
8-
| f² is a value in class Logger
3+
| ^
4+
| Found: (f : F)
5+
| Required: File^
96
|
107
| longer explanation available when compiling with `-explain`
118
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
@@ -14,7 +11,7 @@
1411
|Found: (_$1: box File^{files*}) ->{files*} (ex$16: caps.Exists) -> box Logger{val f: File^{_$1}}^{ex$16.rd, _$1}
1512
|Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^?
1613
|
17-
|Note that reference ex$16.rd
18-
|cannot be included in outer capture set ?
14+
|Note that the universal capability `cap.rd`
15+
|cannot be included in capture set ?
1916
|
2017
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/reaches.check‎

Lines changed: 32 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,15 +56,45 @@
5656
|
5757
| longer explanation available when compiling with `-explain`
5858
-- Error: tests/neg-custom-args/captures/reaches.scala:79:10 -----------------------------------------------------------
59-
79 | ps.map((x, y) => compose1(x, y)) // error // error
59+
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
6060
| ^
6161
| Local reach capability ps* leaks into capture scope of method mapCompose.
6262
| To allow this, the parameter ps should be declared with a @use annotation
6363
-- Error: tests/neg-custom-args/captures/reaches.scala:79:13 -----------------------------------------------------------
64-
79 | ps.map((x, y) => compose1(x, y)) // error // error
64+
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
6565
| ^
6666
| Local reach capability ps* leaks into capture scope of method mapCompose.
6767
| To allow this, the parameter ps should be declared with a @use annotation
68+
-- Error: tests/neg-custom-args/captures/reaches.scala:79:31 -----------------------------------------------------------
69+
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
70+
| ^
71+
| Separation failure: argument of type (x$0: A) ->{y} box A^?
72+
| to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
73+
| corresponds to capture-polymorphic formal parameter g of type box A^? => box A^?
74+
| and captures {ps*}, but this capability is also passed separately
75+
| in the first argument with type (x$0: A) ->{x} box A^?.
76+
|
77+
| Capture set of first argument : {x}
78+
| Hidden set of current argument : {y}
79+
| Footprint of first argument : {x, ps*}
80+
| Hidden footprint of current argument : {y, ps*}
81+
| Declared footprint of current argument: {}
82+
| Undeclared overlap of footprints : {ps*}
83+
-- Error: tests/neg-custom-args/captures/reaches.scala:82:31 -----------------------------------------------------------
84+
82 | ps.map((x, y) => compose1(x, y)) // error sepcheck
85+
| ^
86+
| Separation failure: argument of type (x$0: A) ->{y} box A^?
87+
| to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
88+
| corresponds to capture-polymorphic formal parameter g of type box A^? => box A^?
89+
| and captures {ps*}, but this capability is also passed separately
90+
| in the first argument with type (x$0: A) ->{x} box A^?.
91+
|
92+
| Capture set of first argument : {x}
93+
| Hidden set of current argument : {y}
94+
| Footprint of first argument : {x, ps*}
95+
| Hidden footprint of current argument : {y, ps*}
96+
| Declared footprint of current argument: {}
97+
| Undeclared overlap of footprints : {ps*}
6898
-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
6999
61 | val leaked = usingFile[File^{id*}]: f => // error
70100
| ^^^

‎tests/neg-custom-args/captures/reaches.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
7676
z => g(f(z))
7777

7878
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
79-
ps.map((x, y) => compose1(x, y)) // error // error
79+
ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
8080

8181
def mapCompose2[A](@use ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
82-
ps.map((x, y) => compose1(x, y))
82+
ps.map((x, y) => compose1(x, y)) // error sepcheck

0 commit comments

Comments
 (0)