diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala index ba7b9132e88a..d88ac7895093 100644 --- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala +++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala @@ -226,7 +226,7 @@ object desugar { paramss = (setterParam :: Nil) :: Nil, tpt = TypeTree(defn.UnitType), rhs = setterRhs - ).withMods((vdef.mods | Accessor) &~ (CaseAccessor | GivenOrImplicit | Lazy)) + ).withMods((vdef.mods | Accessor) &~ (CaseAccessor | GivenOrImplicit | Lazy | Transparent)) .dropEndMarker() // the end marker should only appear on the getter definition Thicket(vdef1, setter) else vdef1 diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 2ae80192f3e1..f9cedd53c66a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -352,11 +352,14 @@ extension (tp: Type) case _ => false - /** Is this a type extending `Mutable` that has update methods? */ + /** Is this a type extending `Mutable` that has non-private update methods + * or mutable fields? + */ def isMutableType(using Context): Boolean = tp.derivesFrom(defn.Caps_Mutable) - && tp.membersBasedOnFlags(Mutable | Method, EmptyFlags) - .exists(_.hasAltWith(_.symbol.isUpdateMethod)) + && tp.membersBasedOnFlags(Mutable, EmptyFlags).exists: mbr => + if mbr.symbol.is(Method) then mbr.symbol.isUpdateMethod + else !mbr.symbol.is(Transparent) /** Is this a reference to caps.cap? Note this is _not_ the GlobalCap capability. */ def isCapRef(using Context): Boolean = tp match @@ -496,6 +499,23 @@ extension (tp: Type) def classifier(using Context): ClassSymbol = tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier) + def exclusivity(using Context): Exclusivity = + if tp.derivesFrom(defn.Caps_Mutable) then + tp match + case tp: Capability if tp.isExclusive => Exclusivity.OK + case _ => tp.captureSet.exclusivity(tp) + else Exclusivity.OK + + def exclusivityInContext(using Context): Exclusivity = tp match + case tp: ThisType => + if tp.derivesFrom(defn.Caps_Mutable) + then ctx.owner.inExclusivePartOf(tp.cls) + else Exclusivity.OK + case tp @ TermRef(prefix: Capability, _) => + prefix.exclusivityInContext.andAlso(tp.exclusivity) + case _ => + tp.exclusivity + extension (tp: MethodType) /** A method marks an existential scope unless it is the prefix of a curried method */ def marksExistentialScope(using Context): Boolean = @@ -629,8 +649,22 @@ extension (sym: Symbol) sym.hasAnnotation(defn.ConsumeAnnot) || sym.info.hasAnnotation(defn.ConsumeAnnot) + /** An update method is either a method marked with `update` or + * a setter of a non-transparent var. + */ def isUpdateMethod(using Context): Boolean = - sym.isAllOf(Mutable | Method, butNot = Accessor) + sym.isAllOf(Mutable | Method) + && (!sym.isSetter || sym.field.is(Transparent)) + + def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity = + import Exclusivity.* + val encl = sym.enclosingMethodOrClass.skipConstructor + if sym == cls then OK // we are directly in `cls` or in one of its constructors + else if encl.owner == cls then + if encl.isUpdateMethod then OK + else NotInUpdateMethod(encl, cls) + else if encl.isStatic then OutsideClass(cls) + else encl.owner.inExclusivePartOf(cls) def isReadOnlyMethod(using Context): Boolean = sym.is(Method, butNot = Mutable | Accessor) && sym.owner.derivesFrom(defn.Caps_Mutable) @@ -769,3 +803,35 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]: foldOver(acc, t) end DeepTypeAccumulator +/** Either OK, or a reason why capture set cannot be exclusive */ +enum Exclusivity: + case OK + + /** Enclosing symbol `sym` is a method of class `cls`, but not an update method */ + case NotInUpdateMethod(sym: Symbol, cls: Symbol) + + /** Access to `this` from outside its class (not sure this can happen) */ + case OutsideClass(cls: Symbol) + + /** A prefix type `tp` has a read-only capture set */ + case ReadOnly(tp: Type) + + def isOK: Boolean = this == OK + + def andAlso(that: Exclusivity): Exclusivity = + if this == OK then that else this + + /** A textual description why `qualType` is not exclusive */ + def description(qualType: Type)(using Context): String = this.runtimeChecked match + case Exclusivity.ReadOnly(tp) => + if qualType eq tp then + i"its capture set ${qualType.captureSet} is read-only" + else + i"the capture set ${tp.captureSet} of its prefix $tp is read-only" + case Exclusivity.NotInUpdateMethod(sym: Symbol, cls: Symbol) => + i"the access is in $sym, which is not an update method" + case Exclusivity.OutsideClass(cls: Symbol) => + i"the access from is from ouside $cls" + +end Exclusivity + diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 313db27c3e28..1b66bb5dadd2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -60,8 +60,15 @@ sealed abstract class CaptureSet extends Showable: def mutability_=(x: Mutability): Unit = myMut = x - /** Mark this capture set as belonging to a Mutable type. */ - def setMutable()(using Context): Unit + /** Mark this capture set as belonging to a Mutable type. Called when a new + * CapturingType is formed. This is different from the setter `mutability_=` + * in that it be defined with different behaviors: + * + * - set mutability to Mutable (for normal Vars) + * - take mutability from the set's sources (for DerivedVars) + * - compute mutability on demand based on mutability of elements (for Consts) + */ + def associateWithMutable()(using Context): Unit /** Is this capture set constant (i.e. not an unsolved capture variable)? * Solved capture variables count as constant. @@ -145,6 +152,9 @@ sealed abstract class CaptureSet extends Showable: final def isExclusive(using Context): Boolean = elems.exists(_.isExclusive) + def exclusivity(tp: Type)(using Context): Exclusivity = + if isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp) + /** Similar to isExlusive, but also includes capture set variables * with unknown status. */ @@ -610,7 +620,7 @@ object CaptureSet: private var isComplete = true - def setMutable()(using Context): Unit = + def associateWithMutable()(using Context): Unit = if !elems.isEmpty then isComplete = false // delay computation of Mutability status @@ -630,9 +640,9 @@ object CaptureSet: else "" private def capImpliedByCapability(parent: Type)(using Context): Capability = - if parent.derivesFromExclusive then GlobalCap.readOnly else GlobalCap + if parent.derivesFromMutable then GlobalCap.readOnly else GlobalCap - /* The same as {cap.rd} but generated implicitly for references of Capability subtypes. + /* The same as {cap} but generated implicitly for references of Capability subtypes. */ class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context) extends Const(SimpleIdentitySet(capImpliedByCapability(parent))) @@ -705,7 +715,7 @@ object CaptureSet: */ var deps: Deps = SimpleIdentitySet.empty - def setMutable()(using Context): Unit = + def associateWithMutable()(using Context): Unit = mutability = Mutable def isConst(using Context) = solved >= ccState.iterationId @@ -1028,6 +1038,9 @@ object CaptureSet: addAsDependentTo(source) + /** Mutability is same as in source, except for readOnly */ + override def associateWithMutable()(using Context): Unit = () + override def mutableToReader(origin: CaptureSet)(using Context): Boolean = super.mutableToReader(origin) && ((origin eq source) || source.mutableToReader(this)) @@ -1364,7 +1377,7 @@ object CaptureSet: def description(using Context): String = def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type" i"""$cs is an exclusive capture set ${ofType(hi)}, - |it cannot subsume a read-only capture set ${ofType(lo)}.""" + |it cannot subsume a read-only capture set ${ofType(lo)}""" /** A VarState serves as a snapshot mechanism that can undo * additions of elements or super sets if an operation fails diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index b9545bf39b8b..415fc094923f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -39,7 +39,7 @@ object CapturingType: case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed => apply(parent1, refs ++ refs1, boxed) case _ => - if parent.derivesFromMutable then refs.setMutable() + if parent.derivesFromMutable then refs.associateWithMutable() refs.adoptClassifier(parent.classifier) AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot)) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 194d0444d890..7be3235bf758 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -680,12 +680,20 @@ class CheckCaptures extends Recheck, SymTransformer: if pt.select.symbol.isReadOnlyMethod then markFree(ref.readOnly, tree) else - markPathFree(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt, pt.select) + val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef] + sel.recomputeDenot() + // We need to do a recomputeDenot here since we have not yet properly + // computed the type of the full path. This means that we erroneously + // think the denotation is the same as in the previous phase so no + // member computation is performed. A test case where this matters is + // read-only-use.scala, where the error on r3 goes unreported. + markPathFree(sel, pt.pt, pt.select) case _ => - if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType then - markFree(ref.readOnly, tree) - else - markFree(ref, tree) + if ref.derivesFromMutable then + if pt.isValueType && !pt.isMutableType || ref.exclusivityInContext != Exclusivity.OK + then markFree(ref.readOnly, tree) + else markFree(ref, tree) + else markFree(ref, tree) /** The expected type for the qualifier of a selection. If the selection * could be part of a capability path or is a a read-only method, we return @@ -724,13 +732,10 @@ class CheckCaptures extends Recheck, SymTransformer: case _ => denot // Don't allow update methods to be called unless the qualifier captures - // an exclusive reference. TODO This should probably rolled into - // qualifier logic once we have it. - if tree.symbol.isUpdateMethod && !qualType.captureSet.isExclusive then - report.error( - em"""cannot call update ${tree.symbol} from $qualType, - |since its capture set ${qualType.captureSet} is read-only""", - tree.srcPos) + // an exclusive reference. + if tree.symbol.isUpdateMethod then + checkUpdate(qualType, tree.srcPos): + i"Cannot call update ${tree.symbol} of ${qualType.showRef}" val origSelType = recheckSelection(tree, qualType, name, disambiguate) val selType = mapResultRoots(origSelType, tree.symbol) @@ -768,6 +773,12 @@ class CheckCaptures extends Recheck, SymTransformer: selType }//.showing(i"recheck sel $tree, $qualType = $result") + def checkUpdate(qualType: Type, pos: SrcPos)(msg: => String)(using Context): Unit = + qualType.exclusivityInContext match + case Exclusivity.OK => + case err => + report.error(em"$msg\nsince ${err.description(qualType)}.", pos) + /** Recheck applications, with special handling of unsafeAssumePure. * More work is done in `recheckApplication`, `recheckArg` and `instantiate` below. */ @@ -997,6 +1008,16 @@ class CheckCaptures extends Recheck, SymTransformer: report.error(em"$refArg is not a tracked capability", refArg.srcPos) case _ => + override def recheckAssign(tree: Assign)(using Context): Type = + val lhsType = recheck(tree.lhs, LhsProto) + recheck(tree.rhs, lhsType.widen) + lhsType match + case lhsType @ TermRef(qualType, _) + if (qualType ne NoPrefix) && !lhsType.symbol.is(Transparent) => + checkUpdate(qualType, tree.srcPos)(i"Cannot assign to field ${lhsType.name} of ${qualType.showRef}") + case _ => + defn.UnitType + /** Recheck Closure node: add the captured vars of the anonymoys function * to the result type. See also `recheckClosureBlock` which rechecks the * block containing the anonymous function and the Closure node. @@ -1836,6 +1857,17 @@ class CheckCaptures extends Recheck, SymTransformer: actual end improveReadOnly + def adaptReadOnly(improved: Type, original: Type, expected: Type, tree: Tree)(using Context): Type = improved match + case improved @ CapturingType(parent, refs) + if parent.derivesFrom(defn.Caps_Mutable) + && expected.isValueType + && refs.isExclusive + && !original.exclusivityInContext.isOK => + improved.derivedCapturingType(parent, refs.readOnly) + .showing(i"Adapted readonly $improved for $tree with original = $original in ${ctx.owner} --> $result", capt) + case _ => + improved + /* Currently not needed since it forms part of `adapt` private def improve(actual: Type, prefix: Type)(using Context): Type = val widened = actual.widen.dealiasKeepAnnots @@ -1873,10 +1905,11 @@ class CheckCaptures extends Recheck, SymTransformer: val widened = actual.widen.dealiasKeepAnnots.dropUseAndConsumeAnnots val improvedVAR = improveCaptures(widened, actual) val improved = improveReadOnly(improvedVAR, expected) + val adaptedReadOnly = adaptReadOnly(improved, actual, expected, tree) val adapted = adaptBoxed( - improved.withReachCaptures(actual), expected, tree, + adaptedReadOnly.withReachCaptures(actual), expected, tree, covariant = true, alwaysConst = false) - if adapted eq improvedVAR // no .rd improvement, no box-adaptation + if adapted eq improvedVAR // no .rd improvement or adaptation, no box-adaptation then actual // might as well use actual instead of improved widened else adapted.showing(i"adapt $actual vs $expected = $adapted", capt) end adapt diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index efcfea69e49c..edb7ea29fc84 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -689,9 +689,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: // neither pure, nor are publicily extensible with an unconstrained self type. val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false, isRefining = false) if cls.derivesFrom(defn.Caps_Capability) then - // If cls is a capability class, we need to add a fresh readonly capability to - // ensure we cannot treat the class as pure. - CaptureSet.fresh(cls, cls.thisType, Origin.InDecl(cls)).readOnly.subCaptures(cs) + // If cls is a capability class, we need to add a fresh capability to ensure + // we cannot treat the class as pure. + CaptureSet.fresh(cls, cls.thisType, Origin.InDecl(cls)).subCaptures(cs) CapturingType(cinfo.selfType, cs) // Compute new parent types diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala index aa5ac72c2aa5..9d8a30cb8c6d 100644 --- a/compiler/src/dotty/tools/dotc/typer/Checking.scala +++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala @@ -630,8 +630,13 @@ object Checking { if sym.is(Transparent) then if sym.isType then if !sym.isExtensibleClass then fail(em"`transparent` can only be used for extensible classes and traits") + else if sym.isMutableVar && sym.owner.isClass && Feature.ccEnabled + || sym.isInlineMethod + then + () // ok else - if !sym.isInlineMethod then fail(em"`transparent` can only be used for inline methods") + def ccAdd = if Feature.ccEnabled then i" and mutable fields" else "" + fail(em"`transparent` can only be used for inline methods$ccAdd") if (!sym.isClass && sym.is(Abstract)) fail(OnlyClassesCanBeAbstract(sym)) // note: this is not covered by the next test since terms can be abstract (which is a dual-mode flag) @@ -691,7 +696,7 @@ object Checking { if sym.isWrappedToplevelDef && !sym.isType && sym.flags.is(Infix, butNot = Extension) then fail(ModifierNotAllowedForDefinition(Flags.Infix, s"A top-level ${sym.showKind} cannot be infix.")) if sym.isUpdateMethod && !sym.owner.derivesFrom(defn.Caps_Mutable) then - fail(em"Update methods can only be used as members of classes extending the `Mutable` trait") + fail(em"Update method ${sym.name} must be declared in a class extending the `Mutable` trait.") if sym.is(Erased) then checkErasedOK(sym) checkCombination(Final, Open) checkCombination(Sealed, Open) diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md new file mode 100644 index 000000000000..793597a45284 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -0,0 +1,458 @@ +--- +layout: doc-page +title: "Mutability" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/mutability.html +--- + +## Introduction + +An important class of effects represents accesses to mutable variables and mutable data structures. Here we distinguish two kinds of accesses: write access and read-only access. This is reflected by the kinds of capabilities permitting these effects. +A write capability to a mutable data structure `x` is just `x`. The corresponding read-only capability is written `x.rd`. + +Mutable data structures are expressed with the marker trait `caps.Mutable`. +For instance, consider a simple reference cell: +```scala +import caps.Mutable + +class Ref[T](init: T) extends Mutable: + var fld: T + +val r: Ref[Int]^ = Ref(22) +``` +A function `() => r.fld += 1` has type `() ->{r} Unit` since it writes to the field `fld` of `r`. By contrast, a function `() => r.fld` has type `() ->{r.rd} Int` since it only reads the contents of `r` but does not update it. + +## Capability Kinds + +A capability is called + - _shared_ if it is [classified](classifiers.md) as a `SharedCapability` + - _exclusive_ otherwise. + +## The Mutable Trait + +We introduce a new trait +```scala +trait Mutable extends ExclusiveCapability, Classifier +``` +It is used as a [classifier](classifiers.md) trait for types that define mutable variables and/or _update methods_. + +## Update Methods + +Update methods are declared using a new soft modifier `update`. + +**Example:** +```scala +class Ref(init: Int) extends Mutable: + private var current = init + def get: Int = current + update def set(x: Int): Unit = current = x +``` +`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters. + +In class `Ref`, the `set` method should be declared as an update method since it accesses `this` as an exclusive write capability by writing to the variable `this.current` in its environment. + +`update` can also be used on an inner class of a class or object extending `Mutable`. It gives all code in the class the right +to access exclusive capabilities in the class environment. Normal classes +can only access exclusive capabilities defined in the class or passed to it in parameters. + +```scala +object Registry extends Mutable: + var count = 0 + update class Counter: + update def next: Int = + count += 1 + count +``` +Normal method members of `Mutable` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller. + +An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as `toString` or `==` inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method. + +The `apply` method of a function type is also a normal method, hence `Mutable` classes may not implement a function type using an update method as the `apply` method. + +## Mutable Types + +A type is called a _mutable_ if it extends `Mutable` and it has a mutable variable or +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. + +**Definition:** A class 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. + +**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only. + +The idea is that when we upcast a reference to a type extending `Mutable` to a type that does not extend `Mutable`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented +in the class can access exclusive capabilities on its own. And we +also cannot override any of the methods of this class with a method +accessing exclusive capabilities, since such a method would have +to be an update method and update methods are not allowed to override regular methods. + + + +**Example:** + +Consider trait `IterableOnce` from the standard library. + +```scala +trait IterableOnce[+T] extends Mutable: + def iterator: Iterator[T]^{this} + update def foreach(op: T => Unit): Unit + update def exists(op: T => Boolean): Boolean + ... +``` +The trait is a mutable type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`. +```scala +trait Iterator[T] extends IterableOnce[T]: + def iterator = this + def hasNext: Boolean + update def next(): T + update def foreach(op: T => Unit): Unit = ... + update def exists(op; T => Boolean): Boolean = ... + ... +``` +But there are other implementations of `IterableOnce` that are not mutable types (even though they do indirectly extend the `Mutable` trait). Notably, collection classes implement `IterableOnce` by creating a fresh +`iterator` each time one is required. The mutation via `next()` is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each `update` method in `IterableOnce` by a normal method without the `update` modifier. + +```scala +trait Iterable[T] extends IterableOnce[T]: + def iterator = new Iterator[T] { ... } + def foreach(op: T => Unit) = iterator.foreach(op) + def exists(op: T => Boolean) = iterator.exists(op) +``` +Here, `Iterable` is not a mutable type since it has no update method as member. +All inherited update methods are (re-)implemented by normal methods. + +**Note:** One might think that we don't need a base trait `Mutable` since in any case +a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of `Mutable` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Mutable`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Mutable`. But `apply` may well be implemented by +a method that accesses exclusive capabilities. + +## Read-only Capabilities + +If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix. + +A read-only capability can be seen as a classified capability +using a classifier trait `Read` that extends `Mutable`. I.e. +`x.rd` can be seen as being essentially the same as `x.only[Read]`. +(Currently, this precise equivalence is still waiting to be implemented.) + +**Implicitly added capture sets** + +A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from other capability traits which implicitly add `{cap}`. + +For instance, consider: +```scala +def addContents(from: Ref[Int], to: Ref[Int]^): Unit = + to.set(to.get + from.get) +``` +Here, `from` is implicitly read-only, and `to`'s type has capture set `cap`. I.e. with explicit capture sets this would read: +```scala +def addContents(from: Ref[Int]^{cap.rd}, to: Ref[Int]^{cap}): Unit +``` +In other words, the explicit `^` indicates where write effects can happen. + +## Read-Only Accesses + +An access `p.m` to an update method or class `m` in a mutable type is permitted only if the type `M` of the prefix `p` retains exclusive capabilities. If `M` is pure or its capture set has only shared and read-only capabilities then the access is not permitted. + +A _read-only access_ is a reference to a type extending `Mutable` where one of the following conditions holds: + + 1. The reference is `this` and the access is not from an update method of the class of `this`. For instance: + ```scala + class Ref[T] extends Mutable: + var current: T + def get: T = this.current // read-only access to `this` + ``` + 2. The reference is a path where the path itself or a prefix of that path has a read-only capture set. For instance: + ```scala + val r: Ref[Int]^{cap.rd} = new Ref[T](22) + def get = r.get // read-only access to `r` + ``` + Another example: + ```scala + class RefContainer extends Mutable: + val r: Ref[Int]^ = new Ref[Int](22) + val c: RefContainer = RefContainer() + def get = c.r.get // read-only access to `c.r` + ``` + In the last example, `c.r` is a read-only access since the prefix `c` is a read-only reference. Note that `^{cap.rd}` was implicitly added to `c: RefContainer` since `RefContainer` is a `Mutable` class. + 3. The expected type of the reference is a value type that is not a mutable type. For instance: + ```scala + val r: Ref[Int]^ = Ref(22) + val x: Object = r // read-only access to `r` + ``` + 4. The reference is immediately followed by a selection with a member that is a normal method or class (not an update method or class). For instance: + ```scala + val r: Ref[Int]^ = Ref(22) + r.get // read-only access to `r` + ``` + +The first two conditions represent safety conditions: we _must_ declare the access a read-only access since the context of the access does not permit updates. The last two conditions are opportunistic: we _are allowed_ to declare the access a read-only access since the context +of the access does not require write capabilities. + +A read-only access charges the read-only capability `x.rd` to its environment. Other accesses charge the full capability `x`. + +**Example:** + +Consider a reference `x` and two closures `f` and `g`. + +```scala +val x = Ref(1) +val f = () => x.get // f: () ->{x.rd} Unit +val g = () => x.set(1) // g: () ->{x} Unit +``` + +`f` accesses a regular method, so it charges only `x.rd` to its environment which shows up in its capture set. By contrast, `g` +accesses an update method of `x`, so its capture set is `{x}`. + +A reference to a mutable type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK: +```scala +val a: Ref^ = Ref(1) +val b1: Ref^{a.rd} = a +val b2: Ref^{cap.rd} = a +``` + +## Update Restrictions + +If a capability `r` is a read-only access, then one cannot use `r` to call an update method of `r` or to assign to a field of `r`. E.g. `r.set(22)` and `r.current = 22` are both disallowed. + +Example: + +```scala +class Ref[T](init: T) extends Mutable: + var current = init + + update def set(x: T) = + current = x // ok, set is an update method + + def badSet(x: T) = + current = x // disallowed, since `this` is read-only access + +val r: Ref[Int]^ = Ref(0) +r.set(22) // ok, `r` is exclusive capability. + +val ro: Ref[Int] = r +ro.set(22) // disallowed, since `ro` is read-only access +``` + + +## Transparent Vars + +Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance: +```scala +class Cache[T](eval: () -> T): + private transparent var x: T = compiletime.uninitialized + private transparent var known = false + def force: T = + if !known then + x = eval() + known = true + x +``` +Here, the mutable field `x` is used to store the result of a pure function `eval`. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is +evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`. + +We can avoid the need for update methods by declaring mutable fields `transparent`. Assignments to `transparent` mutable field are not checked for read-only restrictions. It is up to the developer +to use `transparent` responsibly so that it does not hide visible side effects on mutable state. + +Note that an assignment to a variable is restricted only if the variable is a field of a `Mutable` class. Fields of other classes and local variables are currently not checked. + +It is planned to tighten the rules in the future so that non-transparent mutable fields can be declared only in classes extending `Mutable`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `transparent` would become essential as +an escape hatch. + +By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `transparent` is disallowed for such local variables. + +## Read-Only Capsets + +If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{cap}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{cap.rd}`, respectively. + +The contradiction can be explained by noting that we use a capture set in two different roles. + +First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it. + +But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref^`, we can access all its methods, but if we have a `Ref^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a mutable type with exclusive capabilities lets you do more than a mutable type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities. + +The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `RD`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source. +We add an implicit read-only qualifier `RD` to all capture sets on mutable types that consist only of shared or read-only capabilities. +So when we write +```scala +val b1: Ref^{a.rd} = a +``` +we really mean +```scala +val b1: Ref^{a.rd}.RD = a +``` + +The subcapturing theory for sets is then as before, with the following additional rules: + + - `C <: C.RD` + - `C₁.RD <: C₂.RD` if `C₍ <: C₂` + - `{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/docs/_docs/reference/experimental/capture-checking/separation-checking.md b/docs/_docs/reference/experimental/capture-checking/separation-checking.md index 44c3e2b49986..7fcb35658679 100644 --- a/docs/_docs/reference/experimental/capture-checking/separation-checking.md +++ b/docs/_docs/reference/experimental/capture-checking/separation-checking.md @@ -40,197 +40,6 @@ In fact, only a single character was added: `c`'s type now carries a universal c So, effectively, anything that can be updated must be unaliased. - - -## Capability Kinds - -A capability is called - - _shared_ if it is [classified](classifiers.md) as a `SharedCapability` - - _exclusive_ otherwise. - -## The Mutable Trait - -We introduce a new trait -```scala -trait Mutable extends ExclusiveCapability, Classifier -``` -It is used as a [classifier](classifiers.md) trait for types that define _update methods_ using -a new soft modifier `update`. - -**Example:** -```scala -class Ref(init: Int) extends Mutable: - private var current = init - def get: Int = current - update def set(x: Int): Unit = current = x -``` -`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters. - -In class `Ref`, the `set` should be declared as an update method since it accesses the exclusive write capability of the variable `current` in its environment. - -`update` can also be used on an inner class of a class or object extending `Mutable`. It gives all code in the class the right -to access exclusive capabilities in the class environment. Normal classes -can only access exclusive capabilities defined in the class or passed to it in parameters. - -```scala -object Registry extends Mutable: - var count = 0 - update class Counter: - update def next: Int = - count += 1 - count -``` -Normal method members of `Mutable` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller. - -An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as `toString` or `==` inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method. - -The `apply` method of a function type is also a normal method, hence `Mutable` classes may not implement a function type using an update method as the `apply` method. - -## Mutable Types - -A type is called a _mutable_ if it extends `Mutable` and it has 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. - -**Definition:** A class 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. - -**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only. - -The idea is that when we upcast a reference to a type extending `Mutable` to a type that does not extend `Mutable`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented -in the class can access exclusive capabilities on its own. And we -also cannot override any of the methods of this class with a method -accessing exclusive capabilities, since such a method would have -to be an update method and update methods are not allowed to override regular methods. - - - -**Example:** - -Consider trait `IterableOnce` from the standard library. - -```scala -trait IterableOnce[+T] extends Mutable: - def iterator: Iterator[T]^{this} - update def foreach(op: T => Unit): Unit - update def exists(op: T => Boolean): Boolean - ... -``` -The trait is a mutable type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`. -```scala -trait Iterator[T] extends IterableOnce[T]: - def iterator = this - def hasNext: Boolean - update def next(): T - update def foreach(op: T => Unit): Unit = ... - update def exists(op; T => Boolean): Boolean = ... - ... -``` -But there are other implementations of `IterableOnce` that are not mutable types (even though they do indirectly extend the `Mutable` trait). Notably, collection classes implement `IterableOnce` by creating a fresh -`iterator` each time one is required. The mutation via `next()` is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each `update` method in `IterableOnce` by a normal method without the `update` modifier. - -```scala -trait Iterable[T] extends IterableOnce[T]: - def iterator = new Iterator[T] { ... } - def foreach(op: T => Unit) = iterator.foreach(op) - def exists(op: T => Boolean) = iterator.exists(op) -``` -Here, `Iterable` is not a mutable type since it has no update method as member. -All inherited update methods are (re-)implemented by normal methods. - -**Note:** One might think that we don't need a base trait `Mutable` since in any case -a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of `Mutable` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Mutable`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Mutable`. But `apply` may well be implemented by -a method that accesses exclusive capabilities. - -## Read-only Capabilities - -If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix. - -A read-only capability can be seen as a classified capability -using a classifier trait `Read` that extends `Mutable`. I.e. -`x.rd` can be seen as being essentially the same as `x.only[Read]`. -(Currently, this precise equivalence is still waiting to be implemented.) - -**Implicitly added capture sets** - -A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from -other capability traits which implicitly add `{cap}`. - -For instance, consider the matrix multiplication method mentioned previously: -```scala -def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit -``` -Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read: -```scala -def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit -``` -Separation checking will then make sure that `a` and `b` must be different from `c`. - -## Accesses to Mutable Types - -An access `p.m` to an update method or class `m` in a mutable type is permitted only if the type `M` of the prefix `p` retains exclusive capabilities. If `M` is pure or its capture set has only shared -capabilities then the access is not permitted. - -A _read-only access_ is a reference `x` to a type extending `Mutable` that is either - - - widened to a value type that is not a mutable type, or - - immediately followed by a selection with a member that is a normal method or class (not an update method or class). - -A read-only access charges the read-only capability `x.rd` to its environment. Other accesses charge the full capability `x`. - -**Example:** - -Consider a reference `x` and two closures `f` and `g`. - -```scala -val x = Ref(1) -val f = () => x.get // f: () ->{x.rd} Unit -val g = () => x.set(1) // g: () ->{x} Unit -``` - -`f` accesses a regular method, so it charges only `x.rd` to its environment which shows up in its capture set. By contrast, `g` -accesses an update method of `x`, so its capture set is `{x}`. - -A reference to a mutable type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK: -```scala -val a: Ref^ = Ref(1) -val b1: Ref^{a.rd} = a -val b2: Ref^{cap.rd} = a -``` - -## Read-Only Capsets - -If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{cap}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{cap.rd}`, respectively. - -The contradiction can be explained by noting that we use a capture set in two different roles. - -First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it. - -But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref^`, we can access all its methods, but if we have a `Ref^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a mutable type with exclusive capabilities lets you do more than a mutable type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities. - -The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `RD`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source. -We add an implicit read-only qualifier `RD` to all capture sets on mutable types that consist only of shared or read-only capabilities. -So when we write -```scala -val b1: Ref^{a.rd} = a -``` -we really mean -```scala -val b1: Ref^{a.rd}.RD = a -``` - -The subcapturing theory for sets is then as before, with the following additional rules: - - - `C <: C.RD` - - `C₁.RD <: C₂.RD` if `C₍ <: C₂` - - `{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ᵢ`. diff --git a/docs/sidebar.yml b/docs/sidebar.yml index 144ad293eaea..276491cfd0a8 100644 --- a/docs/sidebar.yml +++ b/docs/sidebar.yml @@ -173,6 +173,7 @@ subsection: - page: reference/experimental/capture-checking/scoped-caps.md - page: reference/experimental/capture-checking/classifiers.md - page: reference/experimental/capture-checking/checked-exceptions.md + - page: reference/experimental/capture-checking/mutability.md - page: reference/experimental/capture-checking/separation-checking.md - page: reference/experimental/capture-checking/how-to-use.md - page: reference/experimental/capture-checking/internals.md diff --git a/project/resources/referenceReplacements/sidebar.yml b/project/resources/referenceReplacements/sidebar.yml index 2f766e17e715..b343f2644a9b 100644 --- a/project/resources/referenceReplacements/sidebar.yml +++ b/project/resources/referenceReplacements/sidebar.yml @@ -160,6 +160,7 @@ subsection: - page: reference/experimental/capture-checking/scoped-caps.md - page: reference/experimental/capture-checking/classifiers.md - page: reference/experimental/capture-checking/checked-exceptions.md + - page: reference/experimental/capture-checking/mutability.md - page: reference/experimental/capture-checking/separation-checking.md - page: reference/experimental/capture-checking/how-to-use.md - page: reference/experimental/capture-checking/internals.md diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 78ddb54b5535..4d13f9916fef 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -1,47 +1,69 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 --------------------------------- +7 | def bar: BadBuffer[T]^ = this // error + | ^^^^ + | Found: BadBuffer[T]^{BadBuffer.this.rd} + | Required: BadBuffer[T]^ + | + | Note that capability BadBuffer.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^, + | it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method bar + | + | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:27 ------------------------------------------------------ 5 | update def append(x: T): BadBuffer[T]^ = this // error | ^^^^^^^^^^^^^ | Separation failure: method append's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. | The access must be in a consume method to allow this. --- Error: tests/neg-custom-args/captures/linear-buffer.scala:7:13 ------------------------------------------------------ -7 | def bar: BadBuffer[T]^ = this // error - | ^^^^^^^^^^^^^ - | Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. - | The access must be in a consume method to allow this. --- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 ----------------------------------------------------- -19 | val buf3 = app(buf, 3) // error +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:29 ----------------------------------------------------- +10 | def bar: BadBuffer[T]^ = this // error // error + | ^^^^ + | Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition + | of method append with result type BadBuffer[T]^. + | This type hides capabilities {BadBuffer.this} + | + | where: ^ refers to a fresh root capability classified as Mutable in the result type of method append +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:13 ----------------------------------------------------- +10 | def bar: BadBuffer[T]^ = this // error // error + | ^^^^^^^^^^^^^ + | Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. + | The access must be in a consume method to allow this. +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:22:17 ----------------------------------------------------- +22 | val buf3 = app(buf, 3) // error | ^^^ | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 17 + | consume parameter or was used as a prefix to a consume method on line 20 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf --- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 ----------------------------------------------------- -26 | val buf3 = app(buf1, 4) // error +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:29:17 ----------------------------------------------------- +29 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 24 + | consume parameter or was used as a prefix to a consume method on line 27 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 --- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 ----------------------------------------------------- -34 | val buf3 = app(buf1, 4) // error +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:37:17 ----------------------------------------------------- +37 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 31 + | consume parameter or was used as a prefix to a consume method on line 34 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 --- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 ----------------------------------------------------- -44 | val buf3 = app(buf1, 4) // error +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:47:17 ----------------------------------------------------- +47 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 39 + | consume parameter or was used as a prefix to a consume method on line 42 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 --- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------ -48 | app(buf, 1) // error +-- Error: tests/neg-custom-args/captures/linear-buffer.scala:51:8 ------------------------------------------------------ +51 | app(buf, 1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot | be passed to a consume parameter or be used as a prefix of a consume method call. diff --git a/tests/neg-custom-args/captures/linear-buffer.scala b/tests/neg-custom-args/captures/linear-buffer.scala index 27e2efeeed1f..9c2f3075bc12 100644 --- a/tests/neg-custom-args/captures/linear-buffer.scala +++ b/tests/neg-custom-args/captures/linear-buffer.scala @@ -6,6 +6,9 @@ class BadBuffer[T] extends Mutable: def foo = def bar: BadBuffer[T]^ = this // error bar + update def updateFoo = + def bar: BadBuffer[T]^ = this // error // error + bar class Buffer[T] extends Mutable: consume def append(x: T): Buffer[T]^ = this // ok diff --git a/tests/neg-custom-args/captures/mut-outside-mutable.check b/tests/neg-custom-args/captures/mut-outside-mutable.check index d0f61f150565..b0ff82884ebe 100644 --- a/tests/neg-custom-args/captures/mut-outside-mutable.check +++ b/tests/neg-custom-args/captures/mut-outside-mutable.check @@ -1,8 +1,8 @@ -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:5:13 ------------------------------------------------ 5 | update def foreach(op: T => Unit): Unit // error | ^ - | Update methods can only be used as members of classes extending the `Mutable` trait + | Update method foreach must be declared in a class extending the `Mutable` trait. -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:9:15 ------------------------------------------------ 9 | update def baz() = 1 // error | ^ - | Update methods can only be used as members of classes extending the `Mutable` trait + | Update method baz must be declared in a class extending the `Mutable` trait. diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check new file mode 100644 index 000000000000..9e83c07c4642 --- /dev/null +++ b/tests/neg-custom-args/captures/mutability.check @@ -0,0 +1,98 @@ +-- Error: tests/neg-custom-args/captures/mutability.scala:4:24 --------------------------------------------------------- +4 | def hide(x: T) = this.set(x) // error + | ^^^^^^^^ + | Cannot call update method set of Ref.this + | since the access is in method hide, which is not an update method. +-- Error: tests/neg-custom-args/captures/mutability.scala:9:9 ---------------------------------------------------------- +9 | self.set(x) // error + | ^^^^^^^^ + | Cannot call update method set of self + | since its capture set {self} is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:10:25 ----------------------------------- +10 | val self2: Ref[T]^ = this // error + | ^^^^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutability.scala:14:12 -------------------------------------------------------- +14 | self3().set(x) // error + | ^^^^^^^^^^^ + | Cannot call update method set of Ref[T^{}]^{self3} + | since its capture set {self3} is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:15:31 ----------------------------------- +15 | val self4: () => Ref[T]^ = () => this // error + | ^^^^^^^^^^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability classified as Mutable in the type of value self4 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutability.scala:19:12 -------------------------------------------------------- +19 | self5().set(x) // error + | ^^^^^^^^^^^ + | Cannot call update method set of Ref[T^{}]^{Ref.this.rd} + | since its capture set {Ref.this.rd} of method self5 is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:20:27 ----------------------------------- +20 | def self6(): Ref[T]^ = this // error + | ^^^^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method self6 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutability.scala:25:25 -------------------------------------------------------- +25 | def set(x: T) = this.x.set(x) // error + | ^^^^^^^^^^ + | Cannot call update method set of Ref2.this.x + | since the access is in method set, which is not an update method. +-- Error: tests/neg-custom-args/captures/mutability.scala:32:5 --------------------------------------------------------- +32 | r1.set(33) // error + | ^^^^^^ + | Cannot call update method set of r1 + | since its capture set {r1} is read-only. +-- Error: tests/neg-custom-args/captures/mutability.scala:37:7 --------------------------------------------------------- +37 | r3.x.set(33) // error + | ^^^^^^^^ + | Cannot call update method set of r3.x + | since the capture set {r3} of its prefix (r3 : Ref2[Int]) is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:42:29 ----------------------------------- +42 | val r5: () => Ref2[Int]^ = () => ref2 // error + | ^^^^^^^^^^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ + | + | Note that capability ref2 is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, + | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability classified as Mutable in the type of value r5 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutability.scala:45:9 --------------------------------------------------------- +45 | r6().x.set(33) // error + | ^^^^^^^^^^ + | Cannot call update method set of Ref[Int]^{cap.rd} + | since its capture set {cap.rd} is read-only. diff --git a/tests/neg-custom-args/captures/mutability.scala b/tests/neg-custom-args/captures/mutability.scala new file mode 100644 index 000000000000..e551a4337015 --- /dev/null +++ b/tests/neg-custom-args/captures/mutability.scala @@ -0,0 +1,48 @@ +class Ref[T](init: T) extends caps.Mutable: + var x: T = init + update def set(x: T) = this.x = x + def hide(x: T) = this.set(x) // error + update def hide2(x: T) = set(x) // ok + + def sneakyHide(x: T) = + val self = this + self.set(x) // error + val self2: Ref[T]^ = this // error + self2.set(x) + + val self3 = () => this + self3().set(x) // error + val self4: () => Ref[T]^ = () => this // error + self4().set(x) + + def self5() = this + self5().set(x) // error + def self6(): Ref[T]^ = this // error + self6().set(x) + +class Ref2[T](init: T) extends caps.Mutable: + val x = Ref[T](init) + def set(x: T) = this.x.set(x) // error + update def set2(x: T) = this.x.set(x) // ok + +def test = + val r = Ref(22) + r.set(33) // ok + val r1: Ref[Int] = Ref(22) + r1.set(33) // error + + val r2 = Ref2(22) + r2.x.set(33) // ok + val r3: Ref2[Int] = Ref2(22) + r3.x.set(33) // error + + val r4 = () => Ref2(22) + r4().x.set(33) // ok + val ref2: Ref2[Int] = Ref2(22) + val r5: () => Ref2[Int]^ = () => ref2 // error + r5().x.set(33) + val r6: () => Ref2[Int] = () => ref2 + r6().x.set(33) // error + + + diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check new file mode 100644 index 000000000000..76a28c7f1e60 --- /dev/null +++ b/tests/neg-custom-args/captures/mutvars.check @@ -0,0 +1,98 @@ +-- Error: tests/neg-custom-args/captures/mutvars.scala:3:28 ------------------------------------------------------------ +3 | def hide(x: T) = this.fld = x // error + | ^^^^^^^^^^^^ + | Cannot assign to field fld of Ref.this + | since the access is in method hide, which is not an update method. +-- Error: tests/neg-custom-args/captures/mutvars.scala:8:13 ------------------------------------------------------------ +8 | self.fld = x // error + | ^^^^^^^^^^^^ + | Cannot assign to field fld of self + | since its capture set {self} is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:9:25 --------------------------------------- +9 | val self2: Ref[T]^ = this // error + | ^^^^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutvars.scala:13:16 ----------------------------------------------------------- +13 | self3().fld = x // error + | ^^^^^^^^^^^^^^^ + | Cannot assign to field fld of Ref[T^{}]^{self3} + | since its capture set {self3} is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:14:31 -------------------------------------- +14 | val self4: () => Ref[T]^ = () => this // error + | ^^^^^^^^^^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability classified as Mutable in the type of value self4 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutvars.scala:18:16 ----------------------------------------------------------- +18 | self5().fld = x // error + | ^^^^^^^^^^^^^^^ + | Cannot assign to field fld of Ref[T^{}]^{Ref.this.rd} + | since its capture set {Ref.this.rd} of method self5 is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:19:27 -------------------------------------- +19 | def self6(): Ref[T]^ = this // error + | ^^^^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ + | + | Note that capability Ref.this.rd is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method self6 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutvars.scala:24:29 ----------------------------------------------------------- +24 | def set(x: T) = this.x.fld = x // error + | ^^^^^^^^^^^^^^ + | Cannot assign to field fld of Ref2.this.x + | since the access is in method set, which is not an update method. +-- Error: tests/neg-custom-args/captures/mutvars.scala:31:9 ------------------------------------------------------------ +31 | r1.fld = 33 // error + | ^^^^^^^^^^^ + | Cannot assign to field fld of r1 + | since its capture set {r1} is read-only. +-- Error: tests/neg-custom-args/captures/mutvars.scala:36:11 ----------------------------------------------------------- +36 | r3.x.fld = 33 // error + | ^^^^^^^^^^^^^ + | Cannot assign to field fld of r3.x + | since the capture set {r3} of its prefix (r3 : Ref2[Int]) is read-only. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:41:29 -------------------------------------- +41 | val r5: () => Ref2[Int]^ = () => ref2 // error + | ^^^^^^^^^^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ + | + | Note that capability ref2 is not included in capture set {}. + | + | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, + | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability classified as Mutable in the type of value r5 + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 ----------------------------------------------------------- +44 | r6().x.fld = 33 // error + | ^^^^^^^^^^^^^^^ + | Cannot assign to field fld of Ref[Int]^{cap.rd} + | since its capture set {cap.rd} is read-only. diff --git a/tests/neg-custom-args/captures/mutvars.scala b/tests/neg-custom-args/captures/mutvars.scala new file mode 100644 index 000000000000..b670b034e7fa --- /dev/null +++ b/tests/neg-custom-args/captures/mutvars.scala @@ -0,0 +1,44 @@ +class Ref[T](init: T) extends caps.Mutable: + var fld: T = init + def hide(x: T) = this.fld = x // error + update def hide2(x: T) = this.fld = x // ok + + def sneakyHide(x: T) = + val self = this + self.fld = x // error + val self2: Ref[T]^ = this // error + self2.fld = x + + val self3 = () => this + self3().fld = x // error + val self4: () => Ref[T]^ = () => this // error + self4().fld = x + + def self5() = this + self5().fld = x // error + def self6(): Ref[T]^ = this // error + self6().fld = x + +class Ref2[T](init: T) extends caps.Mutable: + val x = Ref[T](init) + def set(x: T) = this.x.fld = x // error + update def set2(x: T) = this.x.fld = x // ok + +def test = + val r = Ref(22) + r.fld = 33 // ok + val r1: Ref[Int] = Ref(22) + r1.fld = 33 // error + + val r2 = Ref2(22) + r2.x.fld = 33 // ok + val r3: Ref2[Int] = Ref2(22) + r3.x.fld = 33 // error + + val r4 = () => Ref2(22) + r4().x.fld = 33 // ok + val ref2: Ref2[Int] = Ref2(22) + val r5: () => Ref2[Int]^ = () => ref2 // error + r5().x.fld = 33 + val r6: () => Ref2[Int] = () => ref2 + r6().x.fld = 33 // error diff --git a/tests/neg-custom-args/captures/read-only-use.check b/tests/neg-custom-args/captures/read-only-use.check new file mode 100644 index 000000000000..9973009e796f --- /dev/null +++ b/tests/neg-custom-args/captures/read-only-use.check @@ -0,0 +1,27 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/read-only-use.scala:21:21 -------------------------------- +21 | val _: () -> Int = f // error + | ^ + | Found: (f : () ->{r.rd} Int) + | Required: () -> Int + | + | Note that capability r.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/read-only-use.scala:26:21 -------------------------------- +26 | val _: () -> Int = g // error + | ^ + | Found: (g : () ->{r2.x.rd} Int) + | Required: () -> Int + | + | Note that capability r2.x.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/read-only-use.scala:31:21 -------------------------------- +31 | val _: () -> Int = h // error + | ^ + | Found: (h : () ->{r3.xx.rd} Int) + | Required: () -> Int + | + | Note that capability r3.xx.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/read-only-use.scala b/tests/neg-custom-args/captures/read-only-use.scala new file mode 100644 index 000000000000..a6fda55829a9 --- /dev/null +++ b/tests/neg-custom-args/captures/read-only-use.scala @@ -0,0 +1,34 @@ +class Ref[T](init: T) extends caps.Mutable: + var fld: T = init + update def set(x: T) = this.fld = x + def f(x: T) = + val self3 = () => this + val _: () ->{this.rd} Ref[T]^{this.rd} = self3 + +class Ref2[T](init: T) extends caps.Mutable: + val x: Ref[T]^ = Ref[T](init) + update def set(x: T) = this.x.set(x) + +class Ref3[T](init: T) extends caps.Mutable: + val xx = Ref[T](init) + update def set(x: T) = this.xx.set(x) + +def test = + val r: Ref[Int] = Ref(22) + val f = () => r.fld + val _: () ->{r.rd} Int = f + val f2: () ->{r.rd} Int = () => r.fld + val _: () -> Int = f // error + + val r2: Ref2[Int] = Ref2(22) + val g = () => r2.x.fld + val _: () ->{r2.x.rd} Int = g + val _: () -> Int = g // error + + val r3: Ref3[Int] = Ref3(22) + val h = () => r3.xx.fld + val _: () ->{r3.xx.rd} Int = h + val _: () -> Int = h // error + + + diff --git a/tests/neg-custom-args/captures/readOnly.check b/tests/neg-custom-args/captures/readOnly.check index 31c66ceabb07..dd6c60c474cd 100644 --- a/tests/neg-custom-args/captures/readOnly.check +++ b/tests/neg-custom-args/captures/readOnly.check @@ -19,5 +19,5 @@ -- Error: tests/neg-custom-args/captures/readOnly.scala:20:23 ---------------------------------------------------------- 20 | val doit = () => z.put(x.get max y.get) // error | ^^^^^ - | cannot call update method put from (z : Ref), - | since its capture set {z} is read-only + | Cannot call update method put of z + | since its capture set {z} is read-only. diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 0fde84ba4a78..079862ca9df6 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -1,8 +1,8 @@ -- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:4 ------------------------------------------------- 10 | a.set(42) // error | ^^^^^ - | cannot call update method set from (a : Ref), - | since its capture set {a} is read-only + | Cannot call update method set of a + | since its capture set {a} is read-only. -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- 12 | val t: Ref^{cap} = a // error | ^ @@ -12,7 +12,7 @@ | Note that capability a is not included in capture set {}. | | Note that {cap} is an exclusive capture set of the mutable type Ref^, - | it cannot subsume a read-only capture set of the mutable type (a : Ref).. + | it cannot subsume a read-only capture set of the mutable type (a : Ref). | | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value t | diff --git a/tests/pos-custom-args/captures/lazyref-mutvar.scala b/tests/pos-custom-args/captures/lazyref-mutvar.scala new file mode 100644 index 000000000000..541f8da94595 --- /dev/null +++ b/tests/pos-custom-args/captures/lazyref-mutvar.scala @@ -0,0 +1,9 @@ +import compiletime.uninitialized +class LazyRef[T](val mkElem: () => T): + transparent var elem: T = uninitialized + transparent var evaluated = false + def get: T = + if !evaluated then + elem = mkElem() + evaluated = true + elem diff --git a/tests/pos-custom-args/captures/transparent-mutvars.scala b/tests/pos-custom-args/captures/transparent-mutvars.scala new file mode 100644 index 000000000000..6ccc3517fe85 --- /dev/null +++ b/tests/pos-custom-args/captures/transparent-mutvars.scala @@ -0,0 +1,36 @@ +class Ref[T](init: T) extends caps.Mutable: + transparent var fld: T = init + def hide(x: T) = this.fld = x // ok + update def hide2(x: T) = this.fld = x // ok + + def sneakyHide(x: T) = + val self = this + self.fld = x // ok + + val self3 = () => this + self3().fld = x // ok + + def self5() = this + self5().fld = x // ok + +class Ref2[T](init: T) extends caps.Mutable: + val x = Ref[T](init) + def set(x: T) = this.x.fld = x // ok + update def set2(x: T) = this.x.fld = x // ok + +def test = + val r = Ref(22) + r.fld = 33 // ok + val r1: Ref[Int] = Ref(22) + r1.fld = 33 // ok + + val r2 = Ref2(22) + r2.x.fld = 33 // ok + val r3: Ref2[Int] = Ref2(22) + r3.x.fld = 33 // ok + + val r4 = () => Ref2(22) + r4().x.fld = 33 // ok + val ref2: Ref2[Int] = Ref2(22) + val r6: () => Ref2[Int] = () => ref2 + r6().x.fld = 33 // ok