Skip to content

Commit 04278ba

Browse files
oderskyodersky
committed
Make Arrays mutable types under separation checking
1 parent 8cb4bd4 commit 04278ba

File tree

21 files changed

+328
-82
lines changed

21 files changed

+328
-82
lines changed

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

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -553,10 +553,13 @@ extension (sym: Symbol)
553553
* - or it is a value class
554554
* - or it is an exception
555555
* - or it is one of Nothing, Null, or String
556+
* Arrays are not pure under strict mutability even though their self type is declared pure
557+
* in Arrays.scala.
556558
*/
557559
def isPureClass(using Context): Boolean = sym match
558560
case cls: ClassSymbol =>
559-
cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)
561+
(cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls))
562+
&& !(cls == defn.ArrayClass && ccConfig.strictMutability)
560563
case _ =>
561564
false
562565

@@ -588,8 +591,8 @@ extension (sym: Symbol)
588591
&& !defn.isPolymorphicAfterErasure(sym)
589592
&& !defn.isTypeTestOrCast(sym)
590593

591-
/** It's a parameter accessor that is not annotated @constructorOnly or @uncheckedCaptures
592-
* and that is not a consume accessor.
594+
/** It's a parameter accessor for a parameter that that is not annotated
595+
* @constructorOnly or @uncheckedCaptures and that is not a consume parameter.
593596
*/
594597
def isRefiningParamAccessor(using Context): Boolean =
595598
sym.is(ParamAccessor)
@@ -600,6 +603,17 @@ extension (sym: Symbol)
600603
&& !param.hasAnnotation(defn.ConsumeAnnot)
601604
}
602605

606+
/** It's a parameter accessor that is tracked for capture checking. Excluded are
607+
* accessors for parameters annotated with constructorOnly or @uncheckedCaptures.
608+
*/
609+
def isTrackedParamAccessor(using Context): Boolean =
610+
sym.is(ParamAccessor)
611+
&& {
612+
val param = sym.owner.primaryConstructor.paramNamed(sym.name)
613+
!param.hasAnnotation(defn.ConstructorOnlyAnnot)
614+
&& !param.hasAnnotation(defn.UntrackedCapturesAnnot)
615+
}
616+
603617
def hasTrackedParts(using Context): Boolean =
604618
!CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
605619

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

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -666,13 +666,33 @@ object CaptureSet:
666666
then i" under-approximating the result of mapping $ref to $mapped"
667667
else ""
668668

669-
private def capImpliedByCapability(parent: Type)(using Context): Capability =
670-
if parent.derivesFromStateful then GlobalCap.readOnly else GlobalCap
669+
private def capImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using Context): Capability =
670+
// Since standard library classes are not compiled with separation checking,
671+
// they treat Array as a Pure class. That means, no effort is made to distinguish
672+
// between exclusive and read-only arrays. To compensate in code compiled under
673+
// strict mutability, we treat contravariant arrays in signatures of stdlib
674+
// members as read-only (so all arrays may be passed to them), and co- and
675+
// invariant arrays as exclusive.
676+
// TODO This scheme should also apply whenever code under strict mutability interfaces
677+
// with code compiled without. To do that we will need to store in the Tasty format
678+
// a flag whether code was compiled with separation checking on. This will have
679+
// to wait until 3.10.
680+
def isArrayFromScalaPackage =
681+
parent.classSymbol == defn.ArrayClass
682+
&& ccConfig.strictMutability
683+
&& variance >= 0
684+
&& sym.isContainedIn(defn.ScalaPackageClass)
685+
if parent.derivesFromStateful && !isArrayFromScalaPackage
686+
then GlobalCap.readOnly
687+
else GlobalCap
671688

672689
/* The same as {cap} but generated implicitly for references of Capability subtypes.
690+
* @param parent the type to which the capture set will be attached
691+
* @param sym the symbol carrying that type
692+
* @param variance the variance in which `parent` appears in the type of `sym`
673693
*/
674-
class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context)
675-
extends Const(SimpleIdentitySet(capImpliedByCapability(parent)))
694+
class CSImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using @constructorOnly ctx: Context)
695+
extends Const(SimpleIdentitySet(capImpliedByCapability(parent, sym, variance)))
676696

677697
/** A special capture set that gets added to the types of symbols that were not
678698
* themselves capture checked, in order to admit arbitrary corresponding capture

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

Lines changed: 1 addition & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1410,9 +1410,7 @@ class CheckCaptures extends Recheck, SymTransformer:
14101410

14111411
// (3) Capture set of self type includes capture sets of parameters
14121412
for param <- cls.paramGetters do
1413-
if !param.hasAnnotation(defn.ConstructorOnlyAnnot)
1414-
&& !param.hasAnnotation(defn.UntrackedCapturesAnnot)
1415-
then
1413+
if param.isTrackedParamAccessor then
14161414
withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
14171415
checkSubset(param.termRef.captureSet, thisSet, param.srcPos)
14181416

@@ -2148,26 +2146,6 @@ class CheckCaptures extends Recheck, SymTransformer:
21482146
checker.traverse(tree.nuType)
21492147
end checkTypeParam
21502148

2151-
/** Under the unsealed policy: Arrays are like vars, check that their element types
2152-
* do not contains `cap` (in fact it would work also to check on array creation
2153-
* like we do under sealed).
2154-
*/
2155-
def checkArraysAreSealedIn(tp: Type, pos: SrcPos)(using Context): Unit =
2156-
val check = new TypeTraverser:
2157-
def traverse(t: Type): Unit =
2158-
t match
2159-
case AppliedType(tycon, arg :: Nil) if tycon.typeSymbol == defn.ArrayClass =>
2160-
if !(pos.span.isSynthetic && ctx.reporter.errorsReported)
2161-
&& !arg.typeSymbol.name.is(WildcardParamName)
2162-
then
2163-
disallowBadRootsIn(arg, NoSymbol, "Array", "have element type", "", pos)
2164-
traverseChildren(t)
2165-
case defn.RefinedFunctionOf(rinfo: MethodType) =>
2166-
traverse(rinfo)
2167-
case _ =>
2168-
traverseChildren(t)
2169-
check.traverse(tp)
2170-
21712149
/** Check that no uses refer to reach capabilities of parameters of enclosing
21722150
* methods or classes.
21732151
*/

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import config.Printers.capt
1010
import config.Feature
1111
import ast.tpd.Tree
1212
import typer.ProtoTypes.LhsProto
13+
import StdNames.nme
1314

1415
/** Handling mutability and read-only access
1516
*/
@@ -59,6 +60,7 @@ object Mutability:
5960
&& !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot)
6061
else true
6162
)
63+
|| ccConfig.strictMutability && sym.name == nme.update && sym == defn.Array_update
6264

6365
/** A read-only member is a lazy val or a method that is not an update method. */
6466
def isReadOnlyMember(using Context): Boolean =

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

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,16 @@ object Setup:
8484
case _ => false
8585
case _ => None
8686

87+
def patchArrayClass()(using Context): Unit =
88+
if ccConfig.strictMutability then
89+
val arrayCls = defn.ArrayClass.asClass
90+
arrayCls.info match
91+
case oldInfo: ClassInfo if !arrayCls.derivesFrom(defn.Caps_Mutable) =>
92+
arrayCls.info = oldInfo.derivedClassInfo(
93+
declaredParents = oldInfo.declaredParents :+ defn.Caps_Mutable.typeRef)
94+
arrayCls.invalidateBaseDataCache()
95+
case _ =>
96+
8797
end Setup
8898
import Setup.*
8999

@@ -425,7 +435,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
425435
then
426436
normalizeCaptures(mapOver(t)) match
427437
case t1 @ CapturingType(_, _) => t1
428-
case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false)
438+
case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1, sym, variance), boxed = false)
429439
else normalizeCaptures(mapFollowingAliases(t))
430440

431441
def innerApply(t: Type) =

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,9 +61,12 @@ object ccConfig:
6161
def newScheme(using ctx: Context): Boolean =
6262
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
6363

64+
/** Allow @use annotations */
6465
def allowUse(using Context): Boolean =
6566
Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
6667

67-
68+
/** Treat arrays as mutable types. Enabled under separation checking */
69+
def strictMutability(using Context): Boolean =
70+
Feature.enabled(Feature.separationChecking)
6871

6972
end ccConfig

‎compiler/src/dotty/tools/dotc/core/SymDenotations.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1886,7 +1886,7 @@ object SymDenotations {
18861886
myBaseTypeCache.nn
18871887
}
18881888

1889-
private def invalidateBaseDataCache() = {
1889+
def invalidateBaseDataCache() = {
18901890
baseDataCache.invalidate()
18911891
baseDataCache = BaseData.None
18921892
}

‎compiler/src/dotty/tools/dotc/typer/TyperPhase.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ class TyperPhase(addRootImports: Boolean = true) extends Phase {
4444
val unit = ctx.compilationUnit
4545
try
4646
if !unit.suspended then ctx.profiler.onUnit(ctx.phase, unit):
47+
if ctx.run.nn.ccEnabledSomewhere then cc.Setup.patchArrayClass()
4748
unit.tpdTree = ctx.typer.typedExpr(unit.untpdTree)
4849
typr.println("typed: " + unit.source)
4950
record("retained untyped trees", unit.untpdTree.treeSize)

‎tests/neg-custom-args/captures/existential-mapping.check‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
-- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 -----------------------------------------------
22
46 | val z2: (x: A^) => Array[C^] = ??? // error
33
| ^^^^^^^^^^^^^^^^^^^^
4-
| Array[C^] captures the root capability `cap` in invariant position.
4+
| Array[C^]^{cap.rd} captures the root capability `cap` in invariant position.
55
| This capability cannot be converted to an existential in the result type of a function.
66
|
7-
| where: ^ refers to the universal root capability
7+
| where: ^ and cap refer to the universal root capability
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
99
9 | val _: (x: C^) -> C = x1 // error
1010
| ^^

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import caps.*
22

33
class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
4-
private val arr: Array[T] = new Array[T](len)
4+
private val arr: Array[T]^ = new Array[T](len)
55
def get(i: Int): T = arr(i)
66
update def update(i: Int, x: T): Unit = arr(i) = x
77

0 commit comments

Comments
 (0)