From 97a2ef2e0da2643de909d2b9f90bcc6a32e417c9 Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 25 Oct 2025 15:38:30 +0300 Subject: [PATCH] Implement inheritance condition for Mutable types --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 147 +++++++++------ .../capture-checking/mutability.md | 173 +----------------- .../captures/mutable-inheritance.check | 16 ++ .../captures/mutable-inheritance.scala | 20 ++ 4 files changed, 131 insertions(+), 225 deletions(-) create mode 100644 tests/neg-custom-args/captures/mutable-inheritance.check create mode 100644 tests/neg-custom-args/captures/mutable-inheritance.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 3e00907332f2..cca9814c00b1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -886,7 +886,7 @@ class CheckCaptures extends Recheck, SymTransformer: */ def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = var refined: Type = core - var allCaptures: CaptureSet = initCs ++ impliedByFields(core) + var allCaptures: CaptureSet = initCs ++ captureSetImpliedByFields(cls, core) for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then @@ -910,62 +910,61 @@ class CheckCaptures extends Recheck, SymTransformer: val (refined, cs) = addParamArgRefinements(core, initCs) refined.capturing(cs) - /** The additional capture set implied by the capture sets of its fields. This - * is either empty or, if some fields have a terminal capability in their span - * capture sets, it consists of a single fresh cap that subsumes all these terminal - * capabiltities. Class parameters are not counted. If the type is a mutable type, - * we add a fresh cap in any case -- this is because we can currently hide - * mutability in array vals, an example is neg-customargs/captures/matrix.scala. - */ - def impliedByFields(core: Type): CaptureSet = - var infos: List[String] = Nil - def pushInfo(msg: => String) = - if ctx.settings.YccVerbose.value then infos = msg :: infos - - /** The classifiers of the fresh caps in the span capture sets of all fields - * in the given class `cls`. Mutable types get at least a fresh classified - * as mutable. - */ - def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match - case cls: ClassSymbol => - val fields = cls.info.decls.toList - var fieldClassifiers = - for - sym <- fields if contributesFreshToClass(sym) - case fresh: FreshCap <- sym.info.spanCaptureSet.elems - .filter(_.isTerminalCapability) - .map(_.stripReadOnly) - .toList - _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh") - yield fresh.hiddenSet.classifier - if cls.typeRef.isMutableType then - fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers - val parentClassifiers = - cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) - if fieldClassifiers.isEmpty && parentClassifiers.isEmpty - then Nil - else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators) - case _ => Nil - - def fresh = - FreshCap(Origin.NewInstance(core)).tap: fresh => - if ctx.settings.YccVerbose.value then - pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field") - report.echo(infos.mkString("\n"), ctx.owner.srcPos) - - knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match - case Nil => CaptureSet.empty - case cl :: Nil => - val result = fresh - result.hiddenSet.adoptClassifier(cl) - result.singletonCaptureSet - case _ => fresh.singletonCaptureSet - end impliedByFields - augmentConstructorType(resType, capturedVars(cls)) .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt) end refineConstructorInstance + /** The additional capture set implied by the capture sets of its fields. This + * is either empty or, if some fields have a terminal capability in their span + * capture sets, it consists of a single fresh cap that subsumes all these terminal + * capabiltities. Class parameters are not counted. If the type is a mutable type, + * we add a fresh cap in any case -- this is because we can currently hide + * mutability in array vals, an example is neg-customargs/captures/matrix.scala. + */ + def captureSetImpliedByFields(cls: ClassSymbol, core: Type)(using Context): CaptureSet = + var infos: List[String] = Nil + def pushInfo(msg: => String) = + if ctx.settings.YccVerbose.value then infos = msg :: infos + + /** The classifiers of the fresh caps in the span capture sets of all fields + * in the given class `cls`. + */ + def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match + case cls: ClassSymbol => + var fieldClassifiers = + for + sym <- cls.info.decls.toList + if contributesFreshToClass(sym) + case fresh: FreshCap <- sym.info.spanCaptureSet.elems + .filter(_.isTerminalCapability) + .map(_.stripReadOnly) + .toList + _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh") + yield fresh.hiddenSet.classifier + if cls.typeRef.isMutableType then + fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers + val parentClassifiers = + cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) + if fieldClassifiers.isEmpty && parentClassifiers.isEmpty + then Nil + else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators) + case _ => Nil + + def fresh = + FreshCap(Origin.NewInstance(core)).tap: fresh => + if ctx.settings.YccVerbose.value then + pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field") + report.echo(infos.mkString("\n"), ctx.owner.srcPos) + + knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match + case Nil => CaptureSet.empty + case cl :: Nil => + val result = fresh + result.hiddenSet.adoptClassifier(cl) + result.singletonCaptureSet + case _ => fresh.singletonCaptureSet + end captureSetImpliedByFields + /** Recheck type applications: * - Map existential captures in result to `cap` * - include captures of called methods in environment @@ -2139,7 +2138,38 @@ class CheckCaptures extends Recheck, SymTransformer: end for end checkEscapingUses - /** Check that arguments of TypeApplys and AppliedTypes conform to their bounds. + /** Check all parent class constructors of classes extending Mutable + * either also extend Mutable or are read-only. + * + * A parent class constructor is _read-only_ if the following conditions are met + * 1. The class does not retain any exclusive capabilities from its environment. + * 2. The constructor does not take arguments that retain exclusive capabilities. + * 3. The class does not does not have fields that retain exclusive universal capabilities. + */ + def checkMutableInheritance(cls: ClassSymbol, parents: List[Tree])(using Context): Unit = + if cls.derivesFrom(defn.Caps_Mutable) then + for parent <- parents do + if !parent.tpe.derivesFromMutable then + val pcls = parent.nuType.classSymbol + val parentIsExclusive = + if parent.isType then + capturedVars(pcls).isExclusive + || captureSetImpliedByFields(pcls.asClass, parent.nuType).isExclusive + + else parent.nuType.captureSet.isExclusive + if parentIsExclusive then + report.error( + em"""illegal inheritance: $cls which extends `Mutable` is not allowed to also extend $pcls + |since $pcls retains exclusive capabilities but does not extend `Mutable`.""", + parent.srcPos) + + /** Checks to run after the rechecking pass: + * - Check that arguments of TypeApplys and AppliedTypes conform to their bounds. + * - Check that no uses refer to reach capabilities of parameters of enclosing + * methods or classes. + * - Run the separation checker under language.experimental.separationChecking + * - Check that classes extending Mutable do not extend other classes that do + * not extend Mutable yet retain exclusive capabilities */ def postCheck(unit: tpd.Tree)(using Context): Unit = val checker = new TreeTraverser: @@ -2150,6 +2180,7 @@ class CheckCaptures extends Recheck, SymTransformer: trace(i"post check $tree"): traverseChildren(tree)(using lctx) check(tree) + def check(tree: Tree)(using Context) = tree match case TypeApply(fun, args) => fun.nuType.widen match @@ -2162,8 +2193,9 @@ class CheckCaptures extends Recheck, SymTransformer: if ccConfig.postCheckCapturesets then args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol)) case _ => + case TypeDef(_, impl: Template) => + checkMutableInheritance(tree.symbol.asClass, impl.parents) case _ => - end check end checker checker.traverse(unit)(using ctx.withOwner(defn.RootClass)) @@ -2173,11 +2205,12 @@ class CheckCaptures extends Recheck, SymTransformer: usedSet(tree) = tree.markedFree ++ cs ccState.inSepCheck: SepCheck(this).traverse(unit) + if !ctx.reporter.errorsReported then // We dont report errors here if previous errors were reported, because other // errors often result in bad applied types, but flagging these bad types gives // often worse error messages than the original errors. - val checkApplied = new TreeTraverser: + val checkAppliedTypes = new TreeTraverser: def traverse(t: Tree)(using Context) = t match case tree: InferredTypeTree => case tree: New => @@ -2185,7 +2218,7 @@ class CheckCaptures extends Recheck, SymTransformer: withCollapsedFresh: checkAppliedTypesIn(tree.withType(tree.nuType)) case _ => traverseChildren(t) - checkApplied.traverse(unit) + checkAppliedTypes.traverse(unit) end postCheck /** Perform the following kinds of checks: diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 793597a45284..58f9a53d3895 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -75,13 +75,13 @@ an update method or an update class as non-private member or constructor. When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`. -**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. +**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced) -**Definition:** A class is _read_only_ if the following conditions are met: +**Definition:** A parent class constructor is _read-only_ if the following conditions are met: - 1. It does not extend any exclusive capabilities from its environment. - 2. It does not take parameters with exclusive capabilities. - 3. It does not contain mutable fields, or fields that take exclusive capabilities. + 1. The class does not retain any exclusive capabilities from its environment. + 2. The constructor does not take arguments that retain exclusive capabilities. + 3. The class does not does not have fields that retain exclusive universal capabilities. **Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only. @@ -293,166 +293,3 @@ The subcapturing theory for sets is then as before, with the following additiona - `{x, ...}.RD = {x.rd, ...}.RD` - `{x.rd, ...} <: {x, ...}` -## Separation Checking - -The idea behind separation checking is simple: We now interpret each occurrence of `cap` as a separate top capability. This includes derived syntaxes like `A^` and `B => C`. We further keep track during capture checking which capabilities are subsumed by each `cap`. If capture checking widens a capability `x` to a top capability `capᵢ`, we say `x` is _hidden_ by `capᵢ`. The rule then is that any capability hidden by a top capability `capᵢ` cannot be referenced independently or hidden in another `capⱼ` in code that can see `capᵢ`. - -Here's an example: -```scala -val x: C^ = y - ... x ... // ok - ... y ... // error -``` -This principle ensures that capabilities such as `x` that have `cap` as underlying capture set are un-aliased or "fresh". Any previously existing aliases such as `y` in the code above are inaccessible as long as `x` is also visible. - -Separation checking applies only to exclusive capabilities and their read-only versions. Any capability extending `SharedCapability` in its type is exempted; the following definitions and rules do not apply to them. - -**Definitions:** - - - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`. - - - The _transitive capture set_ `tcs(C)` of a capture set C is the union - of `tcs(c)` for all elements `c` of `C`. - - - Two capture sets _interfere_ if one contains an exclusive capability `x` and the other also contains `x` or contains the read-only capability `x.rd`. Conversely, two capture sets are _separated_ if their transitive capture sets don't interfere. - -Separation checks are applied in the following scenarios: - -### Checking Applications - -When checking a function application `f(e_1, ..., e_n)`, we instantiate each `cap` in a formal parameter of `f` to a fresh top capability and compare the argument types with these instantiated parameter types. We then check that the hidden set of each instantiated top capability for an argument `eᵢ` is separated from the capture sets of all the other arguments as well as from the capture sets of the function prefix and the function result. For instance a -call to -```scala -multiply(a, b, a) -``` -would be rejected since `a` appears in the hidden set of the last parameter of multiply, which has type `Matrix^` and also appears in the capture set of the -first parameter. - -We do not report a separation error between two sets if a formal parameter's capture set explicitly names a conflicting parameter. For instance, consider a method `seq` to apply two effectful function arguments in sequence. It can be declared as follows: -```scala -def seq(f: () => Unit; g: () ->{cap, f} Unit): Unit = - f(); g() -``` -Here, the `g` parameter explicitly mentions `f` in its potential capture set. This means that the `cap` in the same capture set would not need to hide the first argument, since it already appears explicitly in the same set. Consequently, we can pass the same function twice to `compose` without violating the separation criteria: -```scala -val r = Ref(1) -val plusOne = r.set(r.get + 1) -seq(plusOne, plusOne) -``` -Without the explicit mention of parameter `f` in the capture set of parameter `g` of `seq` we'd get a separation error, since the transitive capture sets of both arguments contain `r` and are therefore not separated. - -### Checking Statement Sequences - -When a capability `x` is used at some point in a statement sequence, we check that `{x}` is separated from the hidden sets of all previous definitions. - -Example: -```scala -val a: Ref^ = Ref(1) -val b: Ref^ = a -val x = a.get // error -``` -Here, the last line violates the separation criterion since it uses in `a.get` the capability `a`, which is hidden by the definition of `b`. -Note that this check only applies when there are explicit top capabilities in play. One could very well write -```scala -val a: Ref^ = Ref(1) -val b: Ref^{a} = a -val x = a.get // ok -``` -One can also drop the explicit type of `b` and leave it to be inferred. That would -not cause a separation error either. -```scala -val a: Ref^ = Ref(0 -val b = a -val x = a.get // ok -``` - -### Checking Types - -When a type contains top capabilities we check that their hidden sets don't interfere with other parts of the same type. - -Example: -```scala -val b: (Ref^, Ref^) = (a, a) // error -val c: (Ref^, Ref^{a}) = (a, a) // error -val d: (Ref^{a}, Ref^{a}) = (a, a) // ok -``` -Here, the definition of `b` is in error since the hidden sets of the two `^`s in its type both contain `a`. Likewise, the definition of `c` is in error since the hidden set of the `^` in its type contains `a`, which is also part of a capture set somewhere else in the type. On the other hand, the definition of `d` is legal since there are no hidden sets to check. - -### Checking Return Types - -When a `cap` appears in the return type of a function it means a "fresh" top capability, different from what is known at the call site. Separation checking makes sure this is the case. For instance, the following is OK: -```scala -def newRef(): Ref^ = Ref(1) -``` -And so is this: -```scala -def newRef(): Ref^ = - val a = Ref(1) - a -``` -But the next definitions would cause a separation error: -```scala -val a = Ref(1) -def newRef(): Ref^ = a // error -``` -The rule is that the hidden set of a fresh cap in a return type cannot reference exclusive or read-only capabilities defined outside of the function. What about parameters? Here's another illegal version: -```scala -def incr(a: Ref^): Ref^ = - a.set(a.get + 1) - a -``` -These needs to be rejected because otherwise we could have set up the following bad example: -```scala -val a = Ref(1) -val b: Ref^ = incr(a) -``` -Here, `b` aliases `a` but does not hide it. If we referred to `a` afterwards we would be surprised to see that the reference has now a value of 2. -Therefore, parameters cannot appear in the hidden sets of fresh result caps either, at least not in general. An exception to this rule is described in the next section. - -### Consume Parameters - -Returning parameters in fresh result caps is safe if the actual argument to the parameter is not used afterwards. We can signal and enforce this pattern by adding a `consume` modifier to a parameter. With that new soft modifier, the following variant of `incr` is legal: -```scala -def incr(consume a: Ref^): Ref^ = - a.set(a.get + 1) - a -``` -Here, we increment the value of a reference and then return the same reference while enforcing the condition that the original reference cannot be used afterwards. Then the following is legal: -```scala -val a1 = Ref(1) -val a2 = incr(a1) -val a3 = incr(a2) -println(a3) -``` -Each reference `aᵢ` is unused after it is passed to `incr`. But the following continuation of that sequence would be in error: -```scala -val a4 = println(a2) // error -val a5 = incr(a1) // error -``` -In both of these assignments we use a capability that was consumed in an argument -of a previous application. - -Consume parameters enforce linear access to resources. This can be very useful. As an example, consider Scala's buffers such as `ListBuffer` or `ArrayBuffer`. We can treat these buffers as if they were purely functional, if we can enforce linear access. - -For instance, we can define a function `linearAdd` that adds elements to buffers in-place without violating referential transparency: -```scala -def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ = - buf += elem -``` -`linearAdd` returns a fresh buffer resulting from appending `elem` to `buf`. It overwrites `buf`, but that's OK since the `consume` modifier on `buf` ensures that the argument is not used after the call. - -### Consume Methods - -Buffers in Scala's standard library use a single-argument method `+=` instead of a two argument global function like `linearAdd`. We can enforce linearity in this case by adding the `consume` modifier to the method itself. -```scala -class Buffer[T] extends Mutable: - consume def +=(x: T): Buffer[T]^ = this // ok -``` -`consume` on a method implies `update`, so there's no need to label `+=` separately as an update method. Then we can write -```scala -val b = Buffer[Int]() += 1 += 2 -val c = b += 3 -// b cannot be used from here -``` -This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer. - diff --git a/tests/neg-custom-args/captures/mutable-inheritance.check b/tests/neg-custom-args/captures/mutable-inheritance.check new file mode 100644 index 000000000000..013a1e09926d --- /dev/null +++ b/tests/neg-custom-args/captures/mutable-inheritance.check @@ -0,0 +1,16 @@ +-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:4:8 ------------------------------------------------- +4 | class A extends E, caps.Mutable // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | reference (c : Object^) is not included in the allowed capture set {cap} of the self type of class A + | + | where: cap is a fresh root capability classified as Mutable in the type of class A +-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:7:16 ------------------------------------------------ +7 |class C extends B(??? : Int => Int), caps.Mutable // error + | ^^^^^^^^^^^^^^^^^^^ + | illegal inheritance: class C which extends `Mutable` is not allowed to also extend class B + | since class B retains exclusive capabilities but does not extend `Mutable`. +-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:18:16 ----------------------------------------------- +18 |class H extends G, caps.Mutable // error + | ^ + | illegal inheritance: class H which extends `Mutable` is not allowed to also extend class G + | since class G retains exclusive capabilities but does not extend `Mutable`. diff --git a/tests/neg-custom-args/captures/mutable-inheritance.scala b/tests/neg-custom-args/captures/mutable-inheritance.scala new file mode 100644 index 000000000000..6637fbb0ea7b --- /dev/null +++ b/tests/neg-custom-args/captures/mutable-inheritance.scala @@ -0,0 +1,20 @@ +def test(c: Object^) = + class E: + def f = println(c) + class A extends E, caps.Mutable // error + +class B(x: Int => Int) +class C extends B(??? : Int => Int), caps.Mutable // error + +class D extends caps.Mutable: + var x: Int = 0 + +class F extends D, caps.Mutable // ok + +class Ref extends caps.Mutable + +class G: + val r: Ref^ = Ref() +class H extends G, caps.Mutable // error + +