Skip to content

Commit 83feab2

Browse files
authored
Delay normalization of capture sets of vals and defs (#25640)
Normalization means: Make all LocalCaps of a val or def `sym` have origin InDecl(sym). Previously this was done immediately when an element was included in a set. But that broke transaction semantics since some additions could not be undone by removing the added element from the set. We now do the same transformation as part of interpolation after the definition is rechecked. This is still OK, since the normalization is needed only for separation checking Fixes #25622
2 parents 85f8b6c + ca51c83 commit 83feab2

20 files changed

+143
-93
lines changed

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

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Flags.*
1717
import config.Printers.capt
1818
import annotation.constructorOnly
1919
import ast.tpd
20+
import tpd.*
2021
import printing.{Printer, Showable}
2122
import printing.Texts.Text
2223
import reporting.{Message, trace}
@@ -990,7 +991,7 @@ object Capabilities:
990991
case TypeArg(tp: Type)
991992
case UnsafeAssumePure
992993
case Formal(pref: ParamRef, app: tpd.Apply)
993-
case ResultInstance(methType: Type, meth: Symbol)
994+
case ResultInstance(methType: Type, tree: Tree)
994995
case UnapplyInstance(info: MethodType)
995996
case LocalInstance(restpe: Type)
996997
case NewInstance(tp: Type, fields: List[Symbol])
@@ -1026,15 +1027,24 @@ object Capabilities:
10261027
if meth.exists
10271028
then i" when checking argument to parameter ${pref.paramName} of $meth"
10281029
else ""
1029-
case ResultInstance(mt, meth) =>
1030-
val methDescr = if meth.exists then i"$meth's type " else ""
1031-
i" when instantiating $methDescr$mt"
1030+
case ResultInstance(mt, tree) =>
1031+
def methDescr(tree: Tree): String = tree match
1032+
case app: GenericApply =>
1033+
methDescr(app.fun)
1034+
case Select(qual, nme.apply) if defn.isFunctionType(qual.tpe.widen.stripCapturing) =>
1035+
i"function ${methDescr(qual)}"
1036+
case _ if tree.symbol.exists =>
1037+
i"${tree.symbol}'s type "
1038+
case _ =>
1039+
""
1040+
i" when instantiating ${methDescr(tree)}$mt"
10321041
case UnapplyInstance(info) =>
10331042
i" when instantiating argument of unapply with type $info"
10341043
case LocalInstance(restpe) =>
10351044
i" when instantiating expected result type $restpe of function literal"
10361045
case NewInstance(tp, fields) =>
1037-
i" when constructing instance $tp$contributingStr"
1046+
if tp.typeSymbol.is(Module) then contributingStr
1047+
else i" when constructing instance $tp$contributingStr"
10381048
case LambdaExpected(respt) =>
10391049
i" when instantiating expected result type $respt of lambda"
10401050
case LambdaActual(restp: Type) =>

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

Lines changed: 53 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -761,7 +761,6 @@ object CaptureSet:
761761

762762
if debugVars && id == debugTarget then
763763
println(i"###INIT ELEMS of $id of class $getClass in $initialOwner, $nestedOK to $initialElems")
764-
assert(false)
765764

766765
def elems: Refs = myElems
767766
def elems_=(refs: Refs): Unit =
@@ -1029,63 +1028,72 @@ object CaptureSet:
10291028
end Var
10301029

10311030
/** Variables created in types of inferred type trees */
1032-
class ProperVar(override val owner: Symbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context)
1033-
extends Var(owner, initialElems, nestedOK):
1031+
class VarInTypeTree(override val owner: Symbol, initialElems: Refs = emptyRefs, val nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context)
1032+
extends Var(owner, initialElems, nestedOK) {
10341033

10351034
/** Make sure that capset variables in types of vals and result types of
10361035
* non-anonymous functions contain only a single LocalCap, and furthermore
10371036
* that that LocalCap has as origin InDecl(owner), where owner is the val
1038-
* or def for which the type is defined.
1037+
* or def for which the type is defined. If the capture set does not satisfy
1038+
* this condition, create a LocalCap with the right origin and move other
1039+
* LocalCaps to its hidden set.
10391040
* Note: This currently does not apply to classified or read-only LocalCaps.
10401041
*/
1041-
override def includeElem(elem: Capability)(using ctx: Context, vs: VarState): Unit = elem match
1042-
case elem: LocalCap
1043-
if !nestedOK
1044-
&& !elems.contains(elem)
1045-
&& !owner.isAnonymousFunction =>
1046-
def fail = i"attempting to add $elem to $this"
1047-
def hideIn(ac: LocalCap): Boolean =
1048-
assert(elem.tryClassifyAs(ac.hiddenSet.classifier), fail)
1049-
if isRefining then
1050-
// If a variable is added by addCaptureRefinements in a synthetic
1051-
// refinement of a class type, don't do level checking. The problem is
1052-
// that the variable might be matched against a type that does not have
1053-
// a refinement, in which case LocalCaps of the class definition would
1054-
// leak out in the corresponding places. This will fail level checking.
1055-
// The disallowBadRoots override below has a similar reason.
1056-
// TODO: We should instead mark the variable as impossible to instantiate
1057-
// and drop the refinement later in the inferred type.
1058-
// Test case is drop-refinement.scala.
1059-
true
1060-
else if ac.acceptsLevelOf(elem) then
1061-
ac.hiddenSet.add(elem)
1062-
true
1063-
else
1064-
capt.println(i"level failure when subsuming in a LocalCap, cannot add $elem with ${elem.levelOwner} to $owner / $fail")
1065-
false
1066-
val isSubsumed = (false /: elems): (isSubsumed, prev) =>
1067-
prev match
1068-
case prev: LocalCap => hideIn(prev)
1069-
case _ => isSubsumed
1070-
if !isSubsumed then
1071-
if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then
1072-
val fc = LocalCap(owner, Origin.InDecl(owner, elem.origin.contributingFields))
1073-
assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail)
1074-
hideIn(fc)
1075-
super.includeElem(fc)
1076-
else
1077-
super.includeElem(elem)
1078-
case _ =>
1079-
super.includeElem(elem)
1042+
def normalizeLocalCaps()(using ctx: Context): Unit =
1043+
if !nestedOK && !owner.isAnonymousFunction then
1044+
var inDeclRoots = elems.filter:
1045+
case elem: LocalCap => elem.origin == Origin.InDecl(owner)
1046+
case _ => false
1047+
val oldElems = elems
1048+
elems = inDeclRoots
1049+
given VarState = VarState.Closed()
1050+
for elem <- oldElems do {
1051+
def fail = i"attempting to add $elem to $this"
1052+
1053+
def hideIn(ac: LocalCap): Boolean =
1054+
assert(elem.tryClassifyAs(ac.hiddenSet.classifier), fail)
1055+
if isRefining then
1056+
// If a variable is added by addCaptureRefinements in a synthetic
1057+
// refinement of a class type, don't do level checking. The problem is
1058+
// that the variable might be matched against a type that does not have
1059+
// a refinement, in which case LocalCaps of the class definition would
1060+
// leak out in the corresponding places. This will fail level checking.
1061+
// The disallowBadRoots override below has a similar reason.
1062+
// TODO: We should instead mark the variable as impossible to instantiate
1063+
// and drop the refinement later in the inferred type.
1064+
// Test case is drop-refinement.scala.
1065+
true
1066+
else if ac.acceptsLevelOf(elem) then
1067+
ac.hiddenSet.add(elem)
1068+
true
1069+
else
1070+
capt.println(i"level failure when subsuming in a LocalCap, cannot add $elem with ${elem.levelOwner} to $owner / $fail")
1071+
false
1072+
1073+
elem match
1074+
case elem: LocalCap =>
1075+
if elem.origin != Origin.InDecl(owner) then
1076+
val isSubsumed = (false /: inDeclRoots): (isSubsumed, root) =>
1077+
hideIn(root.asInstanceOf[LocalCap])
1078+
if !isSubsumed then
1079+
val fc = LocalCap(owner, Origin.InDecl(owner, elem.origin.contributingFields))
1080+
assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail)
1081+
if hideIn(fc) then
1082+
inDeclRoots += fc
1083+
elems += fc
1084+
else
1085+
elems += elem
1086+
case _ =>
1087+
elems += elem
1088+
}
10801089

10811090
/** Variables that represent refinements of class parameters can have the universal
10821091
* capture set, since they represent only what is the result of the constructor.
10831092
* Test case: Without that tweak, logger.scala would not compile.
10841093
*/
10851094
override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) =
10861095
if !isRefining then super.disallowBadRoots(upto)(handler)
1087-
1088-
end ProperVar
1096+
}
10891097

10901098
/** A variable that is derived from some other variable via a map or filter. */
10911099
abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)

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

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -374,6 +374,10 @@ class CheckCaptures extends Recheck, SymTransformer:
374374
if variance > 0 then
375375
t match
376376
case t @ CapturingType(parent, refs) =>
377+
refs match
378+
case refs: CaptureSet.VarInTypeTree if refs.owner == sym =>
379+
refs.normalizeLocalCaps()
380+
case _ =>
377381
for ref <- refs.elems do
378382
ref match
379383
case ref: LocalCap if !ref.hiddenSet.givenOwner.exists =>
@@ -718,10 +722,10 @@ class CheckCaptures extends Recheck, SymTransformer:
718722
/** If `tp` (possibly after widening singletons) is an ExprType
719723
* of a parameterless method, map ResultCap instances in it to LocalCap instances
720724
*/
721-
def mapResultRoots(tp: Type, sym: Symbol)(using Context): Type =
725+
def mapResultRoots(tp: Type, tree: Tree)(using Context): Type =
722726
tp.widenSingleton match
723-
case tp: ExprType if sym.is(Method) =>
724-
resultToAny(tp, Origin.ResultInstance(tp, sym))
727+
case tp: ExprType if tree.symbol.is(Method) =>
728+
resultToAny(tp, Origin.ResultInstance(tp, tree))
725729
case _ =>
726730
tp
727731

@@ -756,7 +760,7 @@ class CheckCaptures extends Recheck, SymTransformer:
756760
markFree(sym.info.captureSet, tree)
757761

758762
SafeRefs.checkSafe(tree, pt)
759-
mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
763+
mapResultRoots(super.recheckIdent(tree, pt), tree)
760764
}
761765

762766
override def recheckThis(tree: This, pt: Type)(using Context): Type =
@@ -822,7 +826,7 @@ class CheckCaptures extends Recheck, SymTransformer:
822826
i"Cannot call update ${tree.symbol} of ${qualType.showRef}"
823827

824828
val origSelType = recheckSelection(tree, qualType, name, disambiguate)
825-
val selType = mapResultRoots(origSelType, tree.symbol)
829+
val selType = mapResultRoots(origSelType, tree)
826830
val selWiden = selType.widen
827831

828832
def capturesResult = origSelType.widenSingleton match
@@ -933,7 +937,7 @@ class CheckCaptures extends Recheck, SymTransformer:
933937
protected override
934938
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
935939
val resultType = super.recheckApplication(tree, qualType, funType, argTypes)
936-
val appType = resultToAny(resultType, Origin.ResultInstance(funType, tree.symbol))
940+
val appType = resultToAny(resultType, Origin.ResultInstance(funType, tree))
937941
val qualCaptures = qualType.captureSet
938942
val argCaptures =
939943
for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
@@ -1048,7 +1052,7 @@ class CheckCaptures extends Recheck, SymTransformer:
10481052
markFreeTypeArgs(tree.fun, meth, tree.args)
10491053

10501054
val funType = super.recheckTypeApply(tree, pt)
1051-
val res = resultToAny(funType, Origin.ResultInstance(funType, meth))
1055+
val res = resultToAny(funType, Origin.ResultInstance(funType, tree))
10521056
includeCallCaptures(tree.symbol, res, tree)
10531057
checkContains(tree)
10541058
res
@@ -1481,7 +1485,7 @@ class CheckCaptures extends Recheck, SymTransformer:
14811485
else i"classified as ${cl.typeRef}"
14821486
report.error(
14831487
em"""$cls is classied as ${cls.classifier.typeRef} but has a field ${fld.name}
1484-
|$fldClassifier
1488+
|$fldClassifier.
14851489
|Field classifiers have to conform to the classifier of the containing class.""",
14861490
cls.srcPos)
14871491
// (2)

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -322,7 +322,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
322322
mapInferred(inCaptureRefinement = true)(tp.memberInfo(getter)).strippedDealias
323323
RefinedType.precise(core, getter.name,
324324
CapturingType(getterType,
325-
CaptureSet.ProperVar(ctx.owner, isRefining = true)))
325+
CaptureSet.VarInTypeTree(ctx.owner, isRefining = true)))
326326
.showing(i"add capture refinement $tp --> $result", capt)
327327
else
328328
core
@@ -779,7 +779,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
779779
// Infer the self type for the rest, which is all classes without explicit
780780
// self types (to which we also add nested module classes), provided they are
781781
// neither pure, nor are publicily extensible with an unconstrained self type.
782-
val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false, isRefining = false)
782+
val cs = CaptureSet.VarInTypeTree(cls, CaptureSet.emptyRefs, nestedOK = false, isRefining = false)
783783

784784
if cls.derivesFrom(defn.Caps_Capability) then
785785
// If cls is a capability class, we need to add a LocalCap capability to ensure
@@ -939,7 +939,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
939939

940940
/** Add a capture set variable to `tp` if necessary. */
941941
private def addVar(tp: Type, owner: Symbol, isRefining: Boolean, typeArgFormal: Type = NoType)(using Context): Type =
942-
decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner), isRefining), typeArgFormal)
942+
decorate(tp, CaptureSet.VarInTypeTree(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner), isRefining), typeArgFormal)
943943

944944
/** A map that adds <fluid> capture sets at all contra- and invariant positions
945945
* in a type where a capture set would be needed. This is used to make types

tests/neg-custom-args/captures/cc-this5.check

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1+
-- [E223] CaptureChecking Error: tests/neg-custom-args/captures/cc-this5.scala:16:20 -----------------------------------
2+
16 | def f = println(c) // error
3+
| ^
4+
| Reference `c` is not included in the allowed capture set 's1
5+
| of the enclosing class A.
16
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:21:15 -------------------------------------
27
21 | val x: A = this // error
38
| ^^^^

tests/neg-custom-args/captures/cc-this5.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ def foo(c: Cap) =
1313
def test(c: Cap) =
1414
class A:
1515
val x: A = this
16-
def f = println(c)
16+
def f = println(c) // error
1717

1818
def test2(c: Cap) =
1919
class A:

tests/neg-custom-args/captures/check-inferred.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
39 |class B extends caps.Control: // error
77
| ^
88
| class B is classied as scala.caps.Control but has a field x
9-
| of unclassified type test.A^
9+
| of unclassified type test.A^.
1010
| Field classifiers have to conform to the classifier of the containing class.
1111
-- Error: tests/neg-custom-args/captures/check-inferred.scala:43:6 -----------------------------------------------------
1212
43 |class C: // error

tests/neg-custom-args/captures/global-mutables.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
| Note that capability `Test33` cannot flow into capture set {}.
1515
| Note that object Test33 is a capability because it uses capabilities {any}
1616
|
17-
| where: any is a root capability classified as Unscoped in the type of object Test33
17+
| where: any is a root capability classified as Unscoped created in object Test33
1818
|
1919
| longer explanation available when compiling with `-explain`
2020
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/global-mutables.scala:11:22 ------------------------------
@@ -28,7 +28,7 @@
2828
| Note that capability `Test33` cannot flow into capture set {}.
2929
| Note that object Test33 is a capability because it uses capabilities {any}
3030
|
31-
| where: any is a root capability classified as Unscoped in the type of object Test33
31+
| where: any is a root capability classified as Unscoped created in object Test33
3232
|
3333
| longer explanation available when compiling with `-explain`
3434
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/global-mutables.scala:16:22 ------------------------------

tests/neg-custom-args/captures/i20481.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i20481.scala:4:13 ----------------------------------------
22
4 | val b: A = this // error
33
| ^^^^
4-
| Found: (A.this : A^{any})
5-
| Required: A
4+
| Found: (A.this : A^{any})
5+
| Required: A
66
|
7-
| Note that capability `any` cannot flow into capture set {}.
7+
| Note that capability `any` cannot flow into capture set {}.
88
|
9-
| where: any is a root capability in the type of class A with contributing field val f
9+
| where: any is a root capability created in class A when constructing instance A with contributing field val f
1010
|
1111
| longer explanation available when compiling with `-explain`
1212
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i20481.scala:8:14 ----------------------------------------

tests/neg-custom-args/captures/i23850.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
|Note that capability `test` cannot flow into capture set {}.
1010
|Note that object test is a capability because it contains fields given instance given_Console
1111
|
12-
|where: any is a root capability classified as SharedCapability in the type of object test with contributing field val given_Console
12+
|where: any is a root capability classified as SharedCapability created in object test with contributing field val given_Console
1313
|
1414
16 | log(s"adding a ($a) to b ($b)")
1515
17 | a + b

0 commit comments

Comments
 (0)