Skip to content

Commit dfcca31

Browse files
oderskyodersky
committed
Let FreshCaps in field types contribute to class captures
A fresh in the capture set of a class field now causes a fresh to be added to the capture set of every instance of that class.
1 parent ecc8ba3 commit dfcca31

File tree

15 files changed

+223
-34
lines changed

15 files changed

+223
-34
lines changed

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

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -896,18 +896,26 @@ object Capabilities:
896896
else if cls2.isSubClass(cls1) then cls2
897897
else defn.NothingClass
898898

899-
def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers =
899+
/** The smallest list D of class symbols in cs1 and cs2 such that
900+
* every class symbol in cs1 and cs2 is a subclass of a class symbol in D
901+
*/
902+
def dominators(cs1: List[ClassSymbol], cs2: List[ClassSymbol])(using Context): List[ClassSymbol] =
900903
// Drop classes that subclass classes of the other set
901904
// @param proper If true, only drop proper subclasses of a class of the other set
902905
def filterSub(cs1: List[ClassSymbol], cs2: List[ClassSymbol], proper: Boolean) =
903906
cs1.filter: cls1 =>
904907
!cs2.exists: cls2 =>
905908
cls1.isSubClass(cls2) && (!proper || cls1 != cls2)
909+
filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false)
910+
911+
def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers =
906912
(cs1, cs2) match
907-
case (Unclassified, _) | (_, Unclassified) => Unclassified
908-
case (UnknownClassifier, _) | (_, UnknownClassifier) => UnknownClassifier
913+
case (Unclassified, _) | (_, Unclassified) =>
914+
Unclassified
915+
case (UnknownClassifier, _) | (_, UnknownClassifier) =>
916+
UnknownClassifier
909917
case (ClassifiedAs(cs1), ClassifiedAs(cs2)) =>
910-
ClassifiedAs(filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false))
918+
ClassifiedAs(dominators(cs1, cs2))
911919

912920
/** The place of - and cause for - creating a fresh capability. Used for
913921
* error diagnostics
@@ -920,7 +928,7 @@ object Capabilities:
920928
case ResultInstance(methType: Type, meth: Symbol)
921929
case UnapplyInstance(info: MethodType)
922930
case LocalInstance(restpe: Type)
923-
case NewMutable(tp: Type)
931+
case NewInstance(tp: Type)
924932
case NewCapability(tp: Type)
925933
case LambdaExpected(respt: Type)
926934
case LambdaActual(restp: Type)
@@ -950,6 +958,8 @@ object Capabilities:
950958
i" when instantiating argument of unapply with type $info"
951959
case LocalInstance(restpe) =>
952960
i" when instantiating expected result type $restpe of function literal"
961+
case NewInstance(tp) =>
962+
i" when constructing instance $tp"
953963
case NewCapability(tp) =>
954964
val kind = if tp.derivesFromMutable then "mutable" else "Capability instance"
955965
i" when constructing $kind $tp"

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

Lines changed: 55 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import typer.Checking.{checkBounds, checkAppliedTypesIn}
1717
import typer.ErrorReporting.{Addenda, NothingToAdd, err}
1818
import typer.ProtoTypes.{LhsProto, WildcardSelectionProto, SelectionProto}
1919
import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
20+
import util.chaining.tap
2021
import transform.{Recheck, PreRecheck, CapturedVars}
2122
import Recheck.*
2223
import scala.collection.mutable
@@ -247,6 +248,11 @@ class CheckCaptures extends Recheck, SymTransformer:
247248

248249
val ccState1 = new CCState // Dotty problem: Rename to ccState ==> Crash in ExplicitOuter
249250

251+
/** A cache that stores for each class the classifiers of all fresh instances
252+
* in the types of its fields.
253+
*/
254+
val knownFresh = new util.EqHashMap[Symbol, List[ClassSymbol]]
255+
250256
class CaptureChecker(ictx: Context) extends Rechecker(ictx), CheckerAPI:
251257

252258
// println(i"checking ${ictx.source}"(using ictx))
@@ -620,9 +626,7 @@ class CheckCaptures extends Recheck, SymTransformer:
620626
fn.tpe.widenDealias match
621627
case tl: TypeLambda => tl.paramNames
622628
case ref: AppliedType if ref.typeSymbol.isClass => ref.typeSymbol.typeParams.map(_.name)
623-
case t =>
624-
println(i"parent type: $t")
625-
args.map(_ => EmptyTypeName)
629+
case t => args.map(_ => EmptyTypeName)
626630

627631
for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do
628632
def where = if sym.exists then i" in an argument of $sym" else ""
@@ -870,7 +874,7 @@ class CheckCaptures extends Recheck, SymTransformer:
870874
var allCaptures: CaptureSet =
871875
if core.derivesFromCapability
872876
then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet
873-
else initCs
877+
else initCs ++ impliedByFields(core)
874878
for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
875879
val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
876880
if !getter.is(Private) && getter.hasTrackedParts then
@@ -894,20 +898,53 @@ class CheckCaptures extends Recheck, SymTransformer:
894898
val (refined, cs) = addParamArgRefinements(core, initCs)
895899
refined.capturing(cs)
896900

897-
/*
898-
def impliedFresh: CaptureSet =
899-
cls.info.fields.foldLeft(CaptureSet.empty: CaptureSet): (cs, field) =>
900-
if !cs.isAlwaysEmpty || field.symbol.is(ParamAccessor) then
901-
cs
902-
else
903-
val fieldFreshCaps = field.info.spanCaptureSet.elems.filter(_.isTerminalCapability)
904-
if fieldFreshCaps.isEmpty then cs
905-
else
906-
val classFresh = FreshCap(ctx.owner, NoPrefix, )
907-
if fieldFreshCaps.forall(_.isReadOnly)
908-
then cs + classFresh.readOnly
909-
else cs + classFresh
910-
*/
901+
/** The additional capture set implied by the capture sets of its fields. This
902+
* is either empty or, if some fields have a terminal capability in their span
903+
* capture sets, it consists of a single fresh cap that subsumes all these terminal
904+
* capabiltities. Class parameters are not counted.
905+
*/
906+
def impliedByFields(core: Type): CaptureSet =
907+
var infos: List[String] = Nil
908+
def pushInfo(msg: => String) =
909+
if ctx.settings.YccVerbose.value then infos = msg :: infos
910+
911+
/** The classifiers of the fresh caps in the span capture sets of all fields
912+
* in the given class `cls`.
913+
*/
914+
def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match
915+
case cls: ClassSymbol =>
916+
val fieldClassifiers =
917+
for
918+
sym <- cls.info.decls.toList
919+
if sym.isField && !sym.isOneOf(DeferredOrTermParamOrAccessor)
920+
&& !sym.hasAnnotation(defn.UntrackedCapturesAnnot)
921+
case fresh: FreshCap <- sym.info.spanCaptureSet.elems
922+
.filter(_.isTerminalCapability)
923+
.map(_.stripReadOnly)
924+
.toList
925+
_ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh")
926+
yield fresh.hiddenSet.classifier
927+
val parentClassifiers =
928+
cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty)
929+
if fieldClassifiers.isEmpty && parentClassifiers.isEmpty
930+
then Nil
931+
else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators)
932+
case _ => Nil
933+
934+
def fresh =
935+
FreshCap(Origin.NewInstance(core)).tap: fresh =>
936+
if ctx.settings.YccVerbose.value then
937+
pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field")
938+
report.echo(infos.mkString("\n"), ctx.owner.srcPos)
939+
940+
knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match
941+
case Nil => CaptureSet.empty
942+
case cl :: Nil =>
943+
val result = fresh
944+
result.hiddenSet.adoptClassifier(cl)
945+
result.singletonCaptureSet
946+
case _ => fresh.singletonCaptureSet
947+
end impliedByFields
911948

912949
augmentConstructorType(resType, capturedVars(cls))
913950
.showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt)

‎library/src/scala/caps/package.scala‎

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -173,10 +173,23 @@ end internal
173173

174174
@experimental
175175
object unsafe:
176-
/**
177-
* Marks the constructor parameter as untracked.
178-
* The capture set of this parameter will not be included in
179-
* the capture set of the constructed object.
176+
/** Two usages:
177+
*
178+
* 1. Marks the constructor parameter as untracked.
179+
* The capture set of this parameter will not be included in
180+
* the capture set of the constructed object.
181+
*
182+
* 2. Marks a class field that has a cap in its capture set, so that
183+
* the cap is not contributed to the class instance.
184+
* Exampple:
185+
*
186+
* class A { val b B^ = ... }; new A()
187+
*
188+
* has type A^ since b contributes a cap. But
189+
*
190+
* class A { @untrackedCaptures val b: B^ = ... }; new A()
191+
*
192+
* has type A. The `b` field does not contribute its cap.
180193
*
181194
* @note This should go into annotations. For now it is here, so that we
182195
* can experiment with it quickly between minor releases

‎library/src/scala/collection/Iterator.scala‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import scala.collection.mutable.{ArrayBuffer, ArrayBuilder, Builder, ImmutableBu
1818
import scala.annotation.tailrec
1919
import scala.annotation.unchecked.uncheckedVariance
2020
import scala.runtime.Statics
21+
import caps.unsafe.untrackedCaptures
2122

2223
/** Iterators are data structures that allow to iterate over a sequence
2324
* of elements. They have a `hasNext` method for checking
@@ -917,7 +918,12 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
917918
*/
918919
def patch[B >: A](from: Int, patchElems: Iterator[B]^, replaced: Int): Iterator[B]^{this, patchElems} =
919920
new AbstractIterator[B] {
920-
private[this] var origElems: Iterator[B]^ = self
921+
// TODO We should be able to prove that origElems is safe even though it is
922+
// declared as Iterator[B]^. We could show that origElems is never assigned a
923+
// freh cap. Maybe we can invent another annotation that is checked and that
924+
// shows that the `^` is just used as an upper bound for concete non-fresh
925+
// capabilities.
926+
@untrackedCaptures private[this] var origElems: Iterator[B]^ = self
921927
// > 0 => that many more elems from `origElems` before switching to `patchElems`
922928
// 0 => need to drop elems from `origElems` and start using `patchElems`
923929
// -1 => have dropped elems from `origElems`, will be using `patchElems` until it's empty

‎library/src/scala/collection/generic/IsIterable.scala‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ package generic
1515

1616
import scala.language.`2.13`
1717
import language.experimental.captureChecking
18+
import caps.unsafe.untrackedCaptures
1819

1920
/** A trait which can be used to avoid code duplication when defining extension
2021
* methods that should be applicable both to existing Scala collections (i.e.,
@@ -123,6 +124,7 @@ transparent trait IsIterable[Repr] extends IsIterableOnce[Repr] {
123124
type C
124125

125126
@deprecated("'conversion' is now a method named 'apply'", "2.13.0")
127+
@untrackedCaptures
126128
override val conversion: Repr => IterableOps[A, Iterable, C] = apply(_)
127129

128130
/** A conversion from the type `Repr` to `IterableOps[A, Iterable, C]` */

‎library/src/scala/collection/generic/IsIterableOnce.scala‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ package generic
1616

1717
import scala.language.`2.13`
1818
import language.experimental.captureChecking
19+
import caps.unsafe.untrackedCaptures
1920

2021
/** Type class witnessing that a collection representation type `Repr` has
2122
* elements of type `A` and has a conversion to `IterableOnce[A]`.
@@ -46,6 +47,7 @@ transparent trait IsIterableOnce[Repr] {
4647
type A
4748

4849
@deprecated("'conversion' is now a method named 'apply'", "2.13.0")
50+
@untrackedCaptures
4951
val conversion: Repr => IterableOnce[A] = apply(_)
5052

5153
/** A conversion from the representation type `Repr` to a `IterableOnce[A]`. */

‎library/src/scala/collection/generic/IsSeq.scala‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ package generic
1515

1616
import scala.language.`2.13`
1717
import language.experimental.captureChecking
18+
import caps.unsafe.untrackedCaptures
1819

1920
import scala.reflect.ClassTag
2021

@@ -31,6 +32,7 @@ import scala.reflect.ClassTag
3132
transparent trait IsSeq[Repr] extends IsIterable[Repr] {
3233

3334
@deprecated("'conversion' is now a method named 'apply'", "2.13.0")
35+
@untrackedCaptures
3436
override val conversion: Repr => SeqOps[A, Iterable, C] = apply(_)
3537

3638
/** A conversion from the type `Repr` to `SeqOps[A, Iterable, C]`

‎library/src/scala/collection/immutable/LazyListIterable.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ import scala.collection.generic.SerializeEnd
2525
import scala.collection.mutable.{Builder, ReusableBuilder, StringBuilder}
2626
import scala.language.implicitConversions
2727
import scala.runtime.Statics
28+
import caps.unsafe.untrackedCaptures
2829

2930
/** This class implements an immutable linked list. We call it "lazy"
3031
* because it computes its elements only when they are needed.
@@ -1374,7 +1375,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
13741375

13751376
private final class WithFilter[A] private[LazyListIterable](lazyList: LazyListIterable[A]^, p: A => Boolean)
13761377
extends collection.WithFilter[A, LazyListIterable] {
1377-
private[this] val filtered = lazyList.filter(p)
1378+
@untrackedCaptures private[this] val filtered = lazyList.filter(p)
13781379
def map[B](f: A => B): LazyListIterable[B]^{this, f} = filtered.map(f)
13791380
def flatMap[B](f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f)
13801381
def foreach[U](f: A => U): Unit = filtered.foreach(f)

‎tests/neg-custom-args/captures/cc-this.check‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,4 +18,4 @@
1818
-- Error: tests/neg-custom-args/captures/cc-this.scala:33:8 ------------------------------------------------------------
1919
33 | def c3 = c2.y // error
2020
| ^
21-
| Separation failure: method c3's inferred result type C{val x: () => Int}^{cc} hides non-local parameter cc
21+
| Separation failure: method c3's inferred result type C{val x: () => Int}^ hides non-local parameter cc

‎tests/neg-custom-args/captures/fresh-fields.check‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:25:13 ---------------------------------
2+
25 | val _: B = b // error
3+
| ^
4+
| Found: (b : B^)
5+
| Required: B
6+
|
7+
| Note that capability cap is not included in capture set {}.
8+
|
9+
| where: ^ refers to a fresh root capability in the type of value b
10+
| cap is a fresh root capability in the type of value b
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:27:13 ---------------------------------
14+
27 | val _: C = c // error
15+
| ^
16+
| Found: (c : C^)
17+
| Required: C
18+
|
19+
| Note that capability cap is not included in capture set {}.
20+
|
21+
| where: ^ refers to a fresh root capability in the type of value c
22+
| cap is a fresh root capability in the type of value c
23+
|
24+
| longer explanation available when compiling with `-explain`
25+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:29:13 ---------------------------------
26+
29 | val _: D = d // error
27+
| ^
28+
| Found: (d : D^)
29+
| Required: D
30+
|
31+
| Note that capability cap is not included in capture set {}.
32+
|
33+
| where: ^ refers to a fresh root capability in the type of value d
34+
| cap is a fresh root capability in the type of value d
35+
|
36+
| longer explanation available when compiling with `-explain`
37+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:31:13 ---------------------------------
38+
31 | val _: E = e // error
39+
| ^
40+
| Found: (e : E^)
41+
| Required: E
42+
|
43+
| Note that capability cap is not included in capture set {}.
44+
|
45+
| where: ^ refers to a fresh root capability classified as SharedCapability in the type of value e
46+
| cap is a fresh root capability classified as SharedCapability in the type of value e
47+
|
48+
| longer explanation available when compiling with `-explain`
49+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:33:13 ---------------------------------
50+
33 | val _: F = f // error
51+
| ^
52+
| Found: (f : F^)
53+
| Required: F
54+
|
55+
| Note that capability cap is not included in capture set {}.
56+
|
57+
| where: ^ refers to a fresh root capability in the type of value f
58+
| cap is a fresh root capability in the type of value f
59+
|
60+
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)