diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index ca55fef08758..45177b8c45ba 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -15,7 +15,8 @@ import CaptureSet.VarState import Capabilities.* import StdNames.nme import config.Feature -import dotty.tools.dotc.core.NameKinds.TryOwnerName +import NameKinds.TryOwnerName +import typer.ProtoTypes.WildcardSelectionProto /** Attachment key for capturing type trees */ private val Captures: Key[CaptureSet] = Key() @@ -639,6 +640,10 @@ extension (tp: AnnotatedType) case ann: CaptureAnnotation => ann.boxed case _ => false +/** A prototype that indicates selection */ +class PathSelectionProto(val select: Select, val pt: Type) extends typer.ProtoTypes.WildcardSelectionProto: + def selector(using Context): Symbol = select.symbol + /** Drop retains annotations in the inferred type if CC is not enabled * or transform them into RetainingTypes if CC is enabled. */ diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 92fa632f5166..ec7fb036729d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -103,9 +103,6 @@ object CheckCaptures: override def toString = "SubstParamsMap" end SubstParamsMap - /** A prototype that indicates selection with an immutable value */ - class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto - /** Check that a @retains annotation only mentions references that can be tracked. * This check is performed at Typer. */ @@ -573,12 +570,12 @@ class CheckCaptures extends Recheck, SymTransformer: // fresh capabilities. We do check that they hide no parameter reach caps in checkEscapingUses case _ => - def checkReadOnlyMethod(included: CaptureSet, env: Env): Unit = + def checkReadOnlyMethod(included: CaptureSet, meth: Symbol): Unit = included.checkAddedElems: elem => if elem.isExclusive then report.error( - em"""Read-only ${env.owner} accesses exclusive capability $elem; - |${env.owner} should be declared an update method to allow this.""", + em"""Read-only $meth accesses exclusive capability $elem; + |$meth should be declared an update method to allow this.""", tree.srcPos) def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit = @@ -598,8 +595,11 @@ class CheckCaptures extends Recheck, SymTransformer: if !isOfNestedMethod(env) then val nextEnv = nextEnvToCharge(env) if nextEnv != null && !nextEnv.owner.isStaticOwner then - if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then - checkReadOnlyMethod(included, env) + if nextEnv.owner != env.owner + && env.owner.isReadOnlyMember + && env.owner.owner.derivesFrom(defn.Caps_Mutable) + then + checkReadOnlyMethod(included, env.owner) recur(included, nextEnv, env) // Under deferredReaches, don't propagate out of methods inside terms. // The use set of these methods will be charged when that method is called. @@ -705,29 +705,23 @@ class CheckCaptures extends Recheck, SymTransformer: * where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b` * instead of just charging `x`. */ - private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = - pt match - case pt: PathSelectionProto if ref.isTracked => - // if `ref` is not tracked then the selection could not give anything new - // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. - if pt.select.symbol.isReadOnlyMethodOrLazyVal then - markFree(ref.readOnly, tree) - else - val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef] - markPathFree(sel, pt.pt, pt.select) - case _ => - markFree(ref.adjustReadOnly(pt), tree) + private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = pt match + case pt: PathSelectionProto + if ref.isTracked && !pt.selector.isOneOf(MethodOrLazyOrMutable) => + // if `ref` is not tracked then the selection could not give anything new + // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. + val sel = ref.select(pt.selector).asInstanceOf[TermRef] + markPathFree(sel, pt.pt, pt.select) + case _ => + markFree(ref.adjustReadOnly(pt), 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 * a PathSelectionProto. */ override def selectionProto(tree: Select, pt: Type)(using Context): Type = - val sym = tree.symbol - if !sym.isOneOf(MethodOrLazyOrMutable) && !sym.isStatic - || sym.isReadOnlyMethodOrLazyVal - then PathSelectionProto(tree, pt) - else super.selectionProto(tree, pt) + if tree.symbol.isStatic then super.selectionProto(tree, pt) + else PathSelectionProto(tree, pt) /** A specialized implementation of the selection rule. * @@ -1039,7 +1033,7 @@ class CheckCaptures extends Recheck, SymTransformer: recheck(tree.rhs, lhsType.widen) lhsType match case lhsType @ TermRef(qualType, _) - if (qualType ne NoPrefix) && !lhsType.symbol.is(Transparent) => + if (qualType ne NoPrefix) && !lhsType.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) => checkUpdate(qualType, tree.srcPos)(i"Cannot assign to field ${lhsType.name} of ${qualType.showRef}") case _ => defn.UnitType @@ -1131,21 +1125,30 @@ class CheckCaptures extends Recheck, SymTransformer: try if sym.is(Module) then sym.info // Modules are checked by checking the module class else - if sym.is(Mutable) && !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then - val addendum = setup.capturedBy.get(sym) match - case Some(encl) => - val enclStr = - if encl.isAnonymousFunction then - val location = setup.anonFunCallee.get(encl) match - case Some(meth) if meth.exists => i" argument in a call to $meth" - case _ => "" - s"an anonymous function$location" - else encl.show - i"\n\nNote that $sym does not count as local since it is captured by $enclStr" - case _ => - "" - disallowBadRootsIn( - tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) + if sym.is(Mutable) then + if !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then + val addendum = setup.capturedBy.get(sym) match + case Some(encl) => + val enclStr = + if encl.isAnonymousFunction then + val location = setup.anonFunCallee.get(encl) match + case Some(meth) if meth.exists => i" argument in a call to $meth" + case _ => "" + s"an anonymous function$location" + else encl.show + i"\n\nNote that $sym does not count as local since it is captured by $enclStr" + case _ => + "" + disallowBadRootsIn( + tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) + if sepChecksEnabled && false + && sym.owner.isClass + && !sym.owner.derivesFrom(defn.Caps_Mutable) + && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then + report.error( + em"""Mutable $sym is defined in a class that does not extend `Mutable`. + |The variable needs to be annotated with `untrackedCaptures` to allow this.""", + tree.namePos) // Lazy vals need their own environment to track captures from their RHS, // similar to how methods work @@ -1793,7 +1796,10 @@ class CheckCaptures extends Recheck, SymTransformer: if needsAdaptation && !insertBox then // we are unboxing val criticalSet = // the set with which we unbox - if covariant then captures // covariant: we box with captures of actual type plus captures leaked by inner adapation + if covariant then + if expected.expectsReadOnly && actual.derivesFromMutable + then captures.readOnly + else captures else expected.captureSet // contravarant: we unbox with captures of epected type //debugShowEnvs() markFree(criticalSet, tree) diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 57bbd9e8be44..3d1a9e75b3fd 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -8,6 +8,7 @@ import Capabilities.* import util.SrcPos import config.Printers.capt import ast.tpd.Tree +import typer.ProtoTypes.LhsProto /** Handling mutability and read-only access */ @@ -46,25 +47,28 @@ object Mutability: end Exclusivity extension (sym: Symbol) - /** An update method is either a method marked with `update` or - * a setter of a non-transparent var. + /** An update method is either a method marked with `update` or a setter + * of a field of a Mutable class that's not annotated with @uncheckedCaptures. + * `update` is implicit for `consume` methods of Mutable classes. */ def isUpdateMethod(using Context): Boolean = sym.isAllOf(Mutable | Method) - && (!sym.isSetter || sym.field.is(Transparent)) + && (if sym.isSetter then + sym.owner.derivesFrom(defn.Caps_Mutable) + && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot) + else true + ) - /** A read-only method is a real method (not an accessor) in a type extending - * Mutable that is not an update method. Included are also lazy vals in such types. - */ - def isReadOnlyMethodOrLazyVal(using Context): Boolean = - sym.isOneOf(MethodOrLazy, butNot = Mutable | Accessor) - && sym.owner.derivesFrom(defn.Caps_Mutable) + /** A read-only member is a lazy val or a method that is not an update method. */ + def isReadOnlyMember(using Context): Boolean = + sym.isOneOf(MethodOrLazy) && !sym.isUpdateMethod private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity = import Exclusivity.* if sym == cls then OK // we are directly in `cls` or in one of its constructors + else if sym.isUpdateMethod then OK else if sym.owner == cls then - if sym.isUpdateMethod || sym.isConstructor then OK + if sym.isConstructor then OK else NotInUpdateMethod(sym, cls) else if sym.isStatic then OutsideClass(cls) else sym.owner.inExclusivePartOf(cls) @@ -77,7 +81,7 @@ object Mutability: tp.derivesFrom(defn.Caps_Mutable) && tp.membersBasedOnFlags(Mutable, EmptyFlags).exists: mbr => if mbr.symbol.is(Method) then mbr.symbol.isUpdateMethod - else !mbr.symbol.is(Transparent) + else !mbr.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) /** OK, except if `tp` extends `Mutable` but `tp`'s capture set is non-exclusive */ private def exclusivity(using Context): Exclusivity = @@ -98,19 +102,25 @@ object Mutability: case _ => tp.exclusivity + def expectsReadOnly(using Context): Boolean = tp match + case tp: PathSelectionProto => + tp.selector.isReadOnlyMember || tp.selector.isMutableVar && tp.pt != LhsProto + case _ => tp.isValueType && !tp.isMutableType + extension (cs: CaptureSet) private def exclusivity(tp: Type)(using Context): Exclusivity = if cs.isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp) extension (ref: TermRef | ThisType) /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the - * following is true: it appears in a non-exclusive context, or the expected - * type is a value type that is not a mutable type. + * following is true: + * - it appears in a non-exclusive context, + * - the expected type is a value type that is not a mutable type, + * - the expected type is a read-only selection */ def adjustReadOnly(pt: Type)(using Context): Capability = if ref.derivesFromMutable - && (pt.isValueType && !pt.isMutableType - || ref.exclusivityInContext != Exclusivity.OK) + && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK) then ref.readOnly else ref @@ -142,7 +152,6 @@ object Mutability: && expected.isValueType && (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly) && !expected.isSingleton - && actual.isBoxedCapturing == expected.isBoxedCapturing then refs.readOnly else refs actual.derivedCapturingType(parent1, refs1) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index b98f07080181..a40e7699c953 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -638,7 +638,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val badParams = mutable.ListBuffer[Symbol]() def currentOwner = role.dclSym.orElse(ctx.owner) for hiddenRef <- refsToCheck.deduct(explicitRefs(tpe)) do - if !hiddenRef.isKnownClassifiedAs(defn.Caps_SharedCapability) then + if !hiddenRef.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then hiddenRef.pathRoot match case ref: TermRef if ref.symbol != role.dclSym => val refSym = ref.symbol @@ -675,7 +675,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: role match case _: TypeRole.Argument | _: TypeRole.Qualifier => for ref <- refsToCheck do - if !ref.isKnownClassifiedAs(defn.Caps_SharedCapability) then + if !ref.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then consumed.put(ref, pos) case _ => end checkConsumedRefs diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index b8de2c7a9115..44aa7c19b6d5 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -333,6 +333,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { case tp: LazyRef if !printDebug => try toText(tp.ref) catch case ex: Throwable => "..." + case sel: cc.PathSelectionProto => + "?.{ " ~ toText(sel.select.symbol) ~ "}" case AnySelectionProto => "a type that can be selected or applied" case tp: SelectionProto => diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala index 02a55be9ea5a..2e8c435e2c38 100644 --- a/compiler/src/dotty/tools/dotc/typer/Namer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala @@ -995,8 +995,12 @@ class Namer { typer: Typer => end if } + /** Add an implicit Mutable flag to consume methods in Mutable classes. This + * turns the method into an update method. + */ private def normalizeFlags(denot: SymDenotation)(using Context): Unit = - if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) then + if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) + && denot.owner.derivesFrom(defn.Caps_Mutable) then denot.setFlag(Mutable) /** Intentionally left without `using Context` parameter. We need diff --git a/docs/_docs/reference/experimental/capture-checking/classifiers.md b/docs/_docs/reference/experimental/capture-checking/classifiers.md index bbba42c37da9..0890725b83e0 100644 --- a/docs/_docs/reference/experimental/capture-checking/classifiers.md +++ b/docs/_docs/reference/experimental/capture-checking/classifiers.md @@ -45,10 +45,10 @@ sealed trait Capability trait SharedCapability extends Capability Classifier trait Control extends SharedCapability, Classifier -trait ExclusiveCapability extends Capability, Classifier -trait Mutable extends ExclusiveCapability, Classifier +trait ExclusiveCapability extends Capability +trait Read extends ExclusiveCapability, Classifier ``` -Here is a graph showing the hierarchy of predefined classifier traits: +Here is a graph showing the hierarchy of predefined capability traits. Classifier traits are underlined. ``` Capability / \ @@ -56,14 +56,17 @@ Here is a graph showing the hierarchy of predefined classifier traits: / \ / \ SharedCapability ExclusiveCapability + ---------------- | | | | | | | | - Control Mutable + Control Read + ------- ---- ``` -At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two classifier traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. -`ExclusiveCapability` is a base trait for capabilities that allow only un-aliased access to the data they represent, with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. +At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. +`ExclusiveCapability` is a base trait for capabilities that +are checked for anti-aliasing restrictions with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. `Control` capabilities are shared. This means they cannot directly or indirectly capture exclusive capabilities such as capabilities that control access to mutable state. Typical `Control` capabilities are: diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 65b29bb2c4ce..177dc7e18a23 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -31,9 +31,9 @@ A capability is called We introduce a new trait ```scala -trait Mutable extends ExclusiveCapability, Classifier +trait Mutable ``` -It is used as a [classifier](classifiers.md) trait for types that define mutable variables and/or _update methods_. +It is used as a marker trait for types that define mutable variables and/or _update methods_. ## Update Methods @@ -134,10 +134,9 @@ a method that accesses exclusive 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.) +A read-only capability can be seen as a [classified](classifiers.md) capability +using a classifier trait `Read`. I.e. +`x.rd` is a shorthand for `x.only[Read]`. **Implicitly added capture sets** @@ -283,31 +282,34 @@ ro.set(22) // disallowed, since `ro` is read-only access ``` -## Transparent Vars +## Untracked Vars Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance: ```scala +import caps.unsafe.untrackedCaptures + class Cache[T](eval: () -> T): - private transparent var x: T = compiletime.uninitialized - private transparent var known = false + @untrackedCaptures private var x: T = compiletime.uninitialized + @untrackedCaptures private 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`. +Note that, even though `Cache` has mutable variables, it is not declared as a `Mutable` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. 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 annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable field are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer +to use `@untrackedCaptures` responsibly so that it does not hide visible side effects on mutable state. -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 at the moment 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. So the `Cache` class above would in fact +currently compile without the addition of `@untrackedCaptures`. -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. +But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` 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 `@untrackedCapture`s would become essential as an escape hatch. -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 `@untrackedCaptures` is disallowed for such local variables. -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. +The `untrackedCaptures` annotation can also be used in some other contexts unrelated to mutable variables. These are described in its [doc comment](https://www.scala-lang.org/api/current/scala/caps/unsafe$$untrackedCaptures.html). ## Read-Only Capsets diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 0527c3e149d6..6fbb0a9a0f93 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -63,7 +63,7 @@ type Shared = SharedCapability * During separation checking, exclusive usage of marked capabilities will be enforced. */ @experimental -trait ExclusiveCapability extends Capability, Classifier +trait ExclusiveCapability extends Capability @experimental type Exclusive = ExclusiveCapability @@ -80,7 +80,7 @@ trait Control extends SharedCapability, Classifier /** Marker trait for classes with methods that require an exclusive reference. */ @experimental -trait Mutable extends ExclusiveCapability, Classifier +trait Mutable extends ExclusiveCapability /** Marker trait for classes with reader methods, typically extended by Mutable classes */ @experimental diff --git a/tests/neg-custom-args/captures/classified-inheritance.check b/tests/neg-custom-args/captures/classified-inheritance.check index 629f815c4b06..6f34d52a4b7a 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.check +++ b/tests/neg-custom-args/captures/classified-inheritance.check @@ -1,8 +1,8 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:5:6 ---------------------------------------------- -5 |class C2 extends caps.Control, caps.Mutable // error +5 |class C2 extends caps.Control, caps.Read // error | ^ - | class C2 inherits two unrelated classifier traits: trait Mutable and trait Control + | class C2 inherits two unrelated classifier traits: trait Read and trait Control -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:10:6 --------------------------------------------- 10 |class C3 extends Matrix, Async // error | ^ - | class C3 inherits two unrelated classifier traits: trait Control and trait Mutable + | class C3 inherits two unrelated classifier traits: trait Control and trait Read diff --git a/tests/neg-custom-args/captures/classified-inheritance.scala b/tests/neg-custom-args/captures/classified-inheritance.scala index 3aef8bd5e35d..78ac5c779271 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.scala +++ b/tests/neg-custom-args/captures/classified-inheritance.scala @@ -2,9 +2,9 @@ import language.experimental.captureChecking class C1 extends caps.Control, caps.SharedCapability // OK -class C2 extends caps.Control, caps.Mutable // error +class C2 extends caps.Control, caps.Read // error trait Async extends caps.Control -class Matrix extends caps.Mutable +class Matrix extends caps.Read class C3 extends Matrix, Async // error diff --git a/tests/neg-custom-args/captures/classifiers-1.scala b/tests/neg-custom-args/captures/classifiers-1.scala index ee49330ec801..ce0ca8890923 100644 --- a/tests/neg-custom-args/captures/classifiers-1.scala +++ b/tests/neg-custom-args/captures/classifiers-1.scala @@ -1,4 +1,4 @@ -class M extends caps.Mutable +class M extends caps.Read class M1(x: Int => Int) extends M // error diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check index 452de9d23b4f..61f4c66d12a9 100644 --- a/tests/neg-custom-args/captures/i23726.check +++ b/tests/neg-custom-args/captures/i23726.check @@ -14,7 +14,7 @@ | The two sets overlap at : {a} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:16:5 ------------------------------------------------------------- 16 | f3(b) // error | ^ @@ -31,7 +31,7 @@ | The two sets overlap at : {b} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value b - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:24:5 ------------------------------------------------------------- 24 | f7(a) // error | ^ @@ -48,4 +48,4 @@ | The two sets overlap at : {a} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply diff --git a/tests/neg-custom-args/captures/i24310.scala b/tests/neg-custom-args/captures/i24310.scala index ca390f715ae5..741ce05b8e5c 100644 --- a/tests/neg-custom-args/captures/i24310.scala +++ b/tests/neg-custom-args/captures/i24310.scala @@ -11,11 +11,12 @@ class Matrix(val f: () => Int) extends Mutable: update def add(): Unit = () -@main def test = +def test(consume proc: () => Int) = val r: Ref^ = Ref() val m: Matrix^ = Matrix(() => 42) val m2: Matrix^ = Matrix(() => m.run()) val m3: Matrix^ = Matrix(() => r.get()) + val m4: Matrix^ = Matrix(proc) def par(f1: () => Int, f2: () => Int): Unit = println(s"par results: ${f1()} and ${f2()}") diff --git a/tests/neg-custom-args/captures/lazyvals-sep.check b/tests/neg-custom-args/captures/lazyvals-sep.check index 0b9e9b969a27..0d01da2c2f30 100644 --- a/tests/neg-custom-args/captures/lazyvals-sep.check +++ b/tests/neg-custom-args/captures/lazyvals-sep.check @@ -34,7 +34,7 @@ |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 Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 --------------------------------- @@ -48,7 +48,7 @@ |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 Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 ------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 700c37ee2302..63cb8472fc05 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -5,7 +5,7 @@ | consume parameter or was used as a prefix to a consume method on line 11 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- 20 | val buf3 = buf1.append(4) // error | ^^^^ @@ -13,7 +13,7 @@ | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- 28 | val buf3 = buf1.append(4) // error | ^^^^ @@ -21,7 +21,7 @@ | consume parameter or was used as a prefix to a consume method on line 25 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- 38 | val buf3 = buf1.append(4) // error | ^^^^ @@ -29,11 +29,11 @@ | consume parameter or was used as a prefix to a consume method on line 33 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(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. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 4d13f9916fef..549adb55a351 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -1,15 +1,15 @@ -- [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]^ + | Found: BadBuffer[T]^{BadBuffer.this.rd} + | Required: BadBuffer[T]^ | - | Note that capability BadBuffer.this.rd is not included in capture set {}. + | 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}. + | 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 + | where: ^ and cap refer to a fresh root capability 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 ------------------------------------------------------ @@ -20,11 +20,11 @@ -- 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} + | 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 + | where: ^ refers to a fresh root capability 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 | ^^^^^^^^^^^^^ @@ -33,11 +33,11 @@ -- 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 20 - | and therefore is no longer available. + | 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 20 + | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:29:17 ----------------------------------------------------- 29 | val buf3 = app(buf1, 4) // error | ^^^^ @@ -45,7 +45,7 @@ | 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 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:37:17 ----------------------------------------------------- 37 | val buf3 = app(buf1, 4) // error | ^^^^ @@ -53,7 +53,7 @@ | 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 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:47:17 ----------------------------------------------------- 47 | val buf3 = app(buf1, 4) // error | ^^^^ @@ -61,11 +61,11 @@ | 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 + | where: ^ refers to a fresh root capability in the type of value buf1 -- 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. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf diff --git a/tests/neg-custom-args/captures/matrix.check b/tests/neg-custom-args/captures/matrix.check index f6d1cf6634bc..6a58b62dc2a3 100644 --- a/tests/neg-custom-args/captures/matrix.check +++ b/tests/neg-custom-args/captures/matrix.check @@ -13,7 +13,7 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul + |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul -- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------ 30 | mul1(m1, m2, m2) // error: will fail separation checking | ^^ @@ -29,4 +29,4 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul1 + |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1 diff --git a/tests/neg-custom-args/captures/mut-iterator.check b/tests/neg-custom-args/captures/mut-iterator.check new file mode 100644 index 000000000000..22c1c425cd7b --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator.check @@ -0,0 +1,29 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:9:17 ------------------------------------------------------- +9 | def next() = f(Iterator.this.next()) // error + | ^ + | Read-only method next accesses exclusive capability (f : T => U); + | method next should be declared an update method to allow this. + | + | where: => refers to a fresh root capability in the type of parameter f +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:17:14 ------------------------------------------------------ +17 | current = xs1 // error + | ^^^^^^^^^^^^^ + | Cannot assign to field current of $anon.this + | since the access is in method next, which is not an update method. +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:22:15 ------------------------------------------------------ +22 | def next() = f(it.next()) // error + | ^ + | Read-only method next accesses exclusive capability (f : T => U); + | method next should be declared an update method to allow this. + | + | where: => refers to a fresh root capability in the type of parameter f +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:7:25 ------------------------------------------------------- +7 | def map[U](f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method map's result type Iterator[U]^{cap.rd} hides non-local this of class trait Iterator. + | The access must be in a consume method to allow this. +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:20:55 ------------------------------------------------------ +20 |def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method mappedIterator's result type Iterator[U]^{cap.rd} hides parameters it and f. + | The parameters need to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/mut-iterator.scala b/tests/neg-custom-args/captures/mut-iterator.scala new file mode 100644 index 000000000000..a6e022ead7fe --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator.scala @@ -0,0 +1,32 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: // error + def hasNext = Iterator.this.hasNext + def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 // error + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + def hasNext = it.hasNext + def next() = f(it.next()) // error + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + val proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) + mapped.next() diff --git a/tests/neg-custom-args/captures/mut-iterator1.check b/tests/neg-custom-args/captures/mut-iterator1.check new file mode 100644 index 000000000000..2a167a752e41 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator1.check @@ -0,0 +1,5 @@ +-- [E164] Declaration Error: tests/neg-custom-args/captures/mut-iterator1.scala:9:15 ----------------------------------- +9 | update def next() = f(Iterator.this.next()) // error + | ^ + | error overriding method next in trait Iterator of type (): U; + | method next of type (): U is an update method, cannot override a read-only method diff --git a/tests/neg-custom-args/captures/mut-iterator1.scala b/tests/neg-custom-args/captures/mut-iterator1.scala new file mode 100644 index 000000000000..c51575c4b2f7 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator1.scala @@ -0,0 +1,30 @@ +import caps.{Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/neg-custom-args/captures/mut-iterator2.check b/tests/neg-custom-args/captures/mut-iterator2.check new file mode 100644 index 000000000000..4e4febb46ff3 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator2.check @@ -0,0 +1,17 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:9:26 ------------------------------------------------------ +9 | update def next() = f(Iterator.this.next()) // error + | ^^^^^^^^^^^^^ + | Read-only method map accesses exclusive capability (Iterator.this : Iterator[T]^); + | method map should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:7:25 ------------------------------------------------------ +7 | def map[U](f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method map's result type Iterator[U]^{cap.rd} hides non-local this of class trait Iterator. + | The access must be in a consume method to allow this. +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:20:55 ----------------------------------------------------- +20 |def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method mappedIterator's result type Iterator[U]^{cap.rd} hides parameters it and f. + | The parameters need to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/mut-iterator2.scala b/tests/neg-custom-args/captures/mut-iterator2.scala new file mode 100644 index 000000000000..9a2b76018dba --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator2.scala @@ -0,0 +1,30 @@ +import caps.{Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: // error + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/neg-custom-args/captures/mut-iterator3.check b/tests/neg-custom-args/captures/mut-iterator3.check new file mode 100644 index 000000000000..e80d8bd541d6 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator3.check @@ -0,0 +1,10 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator3.scala:31:20 ----------------------------------------------------- +31 | val mapped = roit.map(proc) // error + | ^^^^^^^^ + | Cannot call update method map of roit + | since its capture set {roit} is read-only. +-- Error: tests/neg-custom-args/captures/mut-iterator3.scala:32:9 ------------------------------------------------------ +32 | mapped.next() // error + | ^^^^^^^^^^^ + | Cannot call update method next of mapped + | since its capture set {mapped} is read-only. diff --git a/tests/neg-custom-args/captures/mut-iterator3.scala b/tests/neg-custom-args/captures/mut-iterator3.scala new file mode 100644 index 000000000000..5170cebe6f03 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator3.scala @@ -0,0 +1,32 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + consume def map[U](consume f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](consume it: Iterator[T]^, consume f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) // error + mapped.next() // error diff --git a/tests/neg-custom-args/captures/mut-iterator4.check b/tests/neg-custom-args/captures/mut-iterator4.check new file mode 100644 index 000000000000..9400c630406f --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator4.check @@ -0,0 +1,29 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:26 ------------------------------------------------------ +9 | update def next() = f(Iterator.this.next()) // error // error + | ^^^^^^^^^^^^^ + | Read-only method map accesses exclusive capability (Iterator.this : Iterator[T]^); + | method map should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:47 --------------------------------- +9 | update def next() = f(Iterator.this.next()) // error // error + | ^ + |Found: Iterator[U^'s1]^{Iterator.this.rd, f, Iterator.this, cap} + |Required: Iterator[U]^{Iterator.this, f} + | + |Note that capability cap is not included in capture set {Iterator.this, f}. + | + |where: cap is a fresh root capability classified as Mutable created in method map when constructing instance Object with (Iterator[U]^{cap².rd}) {...} + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:23:34 -------------------------------- +23 | update def next() = f(it.next()) // error + | ^ + |Found: Iterator[U^'s2]^{it.rd, f, it, cap} + |Required: Iterator[U]^{it, f} + | + |Note that capability cap is not included in capture set {it, f}. + | + |where: cap is a fresh root capability classified as Mutable created in method mappedIterator when constructing instance Object with (Iterator[U]^{cap².rd}) {...} + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-iterator4.scala b/tests/neg-custom-args/captures/mut-iterator4.scala new file mode 100644 index 000000000000..114c08af2001 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator4.scala @@ -0,0 +1,33 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + def map[U](f: T => U): Iterator[U]^{Iterator.this, f} = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error // error + +end Iterator + +def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U]^{it, f} = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) // error + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) + mapped.next() diff --git a/tests/neg-custom-args/captures/mut-iterator5.check b/tests/neg-custom-args/captures/mut-iterator5.check new file mode 100644 index 000000000000..f9aa93e489e2 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator5.check @@ -0,0 +1,12 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator5.scala:11:23 ----------------------------------------------------- +11 | while hasNext do f(next()) // error + | ^^^^ + | Cannot call update method next of Iterator.this + | since the access is in method stupidForeach, which is not an update method. +-- Error: tests/neg-custom-args/captures/mut-iterator5.scala:16:26 ----------------------------------------------------- +16 | update def next() = Iterator.this.next() // error + | ^^^^^^^^^^^^^ + | Read-only method sneakyForeach accesses exclusive capability (Iterator.this : Iterator[T]^); + | method sneakyForeach should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/mut-iterator5.scala b/tests/neg-custom-args/captures/mut-iterator5.scala new file mode 100644 index 000000000000..a2af33c2e1f4 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator5.scala @@ -0,0 +1,33 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + update def foreach[U](f: T => Unit): Unit = + while hasNext do f(next()) + + def stupidForeach[U](f: T => Unit): Unit = + while hasNext do f(next()) // error + + def sneakyForeach(f: T => Unit): Unit = + val it = new Iterator[T]: + def hasNext = Iterator.this.hasNext + update def next() = Iterator.this.next() // error + while it.hasNext do f(it.next()) +end Iterator + +def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Unit = i => io.write(i) + val f = () => listIterator(List(1, 2, 3)).sneakyForeach(proc) diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check index 90abebcbcb15..c4da68169ce8 100644 --- a/tests/neg-custom-args/captures/mutability.check +++ b/tests/neg-custom-args/captures/mutability.check @@ -11,15 +11,15 @@ -- [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]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | 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}. + | 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 + | where: ^ and cap refer to a fresh root capability in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:11:13 -------------------------------------------------------- @@ -28,7 +28,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:14:12 -------------------------------------------------------- 14 | self3().set(x) // error | ^^^^^^^^^^^ @@ -37,16 +37,16 @@ -- [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]^ + | 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 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}. + | 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 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:16:15 -------------------------------------------------------- @@ -55,7 +55,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:19:12 -------------------------------------------------------- 19 | self5().set(x) // error | ^^^^^^^^^^^ @@ -64,15 +64,15 @@ -- [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]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | 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}. + | 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 + | where: ^ and cap refer to a fresh root capability in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:21:15 -------------------------------------------------------- @@ -81,7 +81,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:25:25 -------------------------------------------------------- 25 | def set(x: T) = this.x.set(x) // error | ^^^^^^^^^^ @@ -100,16 +100,16 @@ -- [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]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. + | 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}. + | 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 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability in the type of value r5 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:45:9 --------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/mutable-inheritance.check b/tests/neg-custom-args/captures/mutable-inheritance.check index 013a1e09926d..84d69eb2824c 100644 --- a/tests/neg-custom-args/captures/mutable-inheritance.check +++ b/tests/neg-custom-args/captures/mutable-inheritance.check @@ -1,9 +1,3 @@ --- 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 | ^^^^^^^^^^^^^^^^^^^ @@ -14,3 +8,8 @@ | ^ | 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`. +-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:4:18 ------------------------------------------------ +4 | class A extends E, caps.Mutable // error + | ^ + | illegal inheritance: class A which extends `Mutable` is not allowed to also extend class E + | since class E retains exclusive capabilities but does not extend `Mutable`. diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check index f5c83dbbb333..76cf79f25987 100644 --- a/tests/neg-custom-args/captures/mutvars.check +++ b/tests/neg-custom-args/captures/mutvars.check @@ -11,15 +11,15 @@ -- [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]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | 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}. + | 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 + | where: ^ and cap refer to a fresh root capability in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:13:16 ----------------------------------------------------------- @@ -30,16 +30,16 @@ -- [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]^ + | 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 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}. + | 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 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:18:16 ----------------------------------------------------------- @@ -50,15 +50,15 @@ -- [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]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | 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}. + | 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 + | where: ^ and cap refer to a fresh root capability in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:24:29 ----------------------------------------------------------- @@ -79,16 +79,16 @@ -- [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]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. + | 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}. + | 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 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability in the type of value r5 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 ----------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 079862ca9df6..153fd5458ba6 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -6,14 +6,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- 12 | val t: Ref^{cap} = a // error | ^ - | Found: (a : Ref) - | Required: Ref^ + | Found: (a : Ref) + | Required: Ref^ | - | Note that capability a is not included in capture set {}. + | 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). + | 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). | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value t + | where: ^ and cap refer to a fresh root capability in the type of value t | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check index 905becd123e4..535cbed775cf 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -8,6 +8,6 @@ | because (a1 : A^) in method b is not visible from cap in variable a. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value a1 - | ^² and cap refer to a fresh root capability classified as Mutable in the type of variable a + | ^² and cap refer to a fresh root capability in the type of variable a | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check index 590c0b01c757..54ab518926cc 100644 --- a/tests/neg-custom-args/captures/sep-box.check +++ b/tests/neg-custom-args/captures/sep-box.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 5967947783ae..0d1a4df1e98e 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -5,7 +5,7 @@ | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x + | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- 21 | par(rx, () => x.put(42)) // error | ^ @@ -13,7 +13,7 @@ | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x + | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index 2676f3f62362..39b657a201f1 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -6,7 +6,7 @@ |Another part, Ref^², captures capabilities {c}. |The two sets overlap at {c}. | - |where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter - | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter + |where: ^ refers to a fresh root capability in the result type of method mkCounter + | ^² refers to a fresh root capability in the result type of method mkCounter | cap is a fresh root capability classified as Mutable in the type of value c | cap² is a fresh root capability classified as Mutable created in value c when constructing instance Ref diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index a2b576de8c3a..ea32ef208b88 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -24,8 +24,8 @@ | Footprint set of second argument : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test0 when checking argument to parameter x of method foo + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test0 when checking argument to parameter x of method foo -- Error: tests/neg-custom-args/captures/sep-curried.scala:22:44 ------------------------------------------------------- 22 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error | ^ @@ -41,8 +41,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in value f when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in value f when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:29:6 -------------------------------------------------------- 29 | foo(a)(a) // error | ^ @@ -58,8 +58,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test2 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test2 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:35:9 -------------------------------------------------------- 35 | foo(a)(a) // error | ^ @@ -75,8 +75,8 @@ | Footprint set of function prefix : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test3 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test3 when checking argument to parameter y of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:42:4 -------------------------------------------------------- 42 | f(a) // error | ^ @@ -92,5 +92,5 @@ | Footprint set of function prefix : {f, a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test4 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test4 when checking argument to parameter y of method apply diff --git a/tests/neg-custom-args/captures/sep-list.check b/tests/neg-custom-args/captures/sep-list.check index 43ac04df02b0..5ecde5d6d2bd 100644 --- a/tests/neg-custom-args/captures/sep-list.check +++ b/tests/neg-custom-args/captures/sep-list.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {h2, xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check index 5baf11b03ec4..ff0d2237dd2d 100644 --- a/tests/neg-custom-args/captures/sep-pairs-unboxed.check +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -13,8 +13,8 @@ | Footprint set of second argument : {x} | The two sets overlap at : {x} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x - | ^² refers to a fresh root capability classified as Mutable created in method mkPair when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability in the type of parameter x + | ^² refers to a fresh root capability created in method mkPair when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 ------------------------------------------------- 35 | val twoCopy = Pair(two.fst, two.fst) // error | ^^^^^^^ @@ -30,8 +30,8 @@ | Footprint set of second argument : {two.fst} | The two sets overlap at : {two.fst} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst - | ^² refers to a fresh root capability classified as Mutable created in value twoCopy when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability in the type of value fst + | ^² refers to a fresh root capability created in value twoCopy when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 ------------------------------------------------- 41 | val twisted = PairPair(two.fst, two) // error | ^^^^^^^ @@ -39,7 +39,7 @@ |to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair |corresponds to capture-polymorphic formal parameter fst of type Ref^² |and hides capabilities {two.fst}. - |Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + |Some of these overlap with the captures of the second argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. | | Hidden set of current argument : {two.fst} | Hidden footprint of current argument : {two.fst} @@ -47,8 +47,8 @@ | Footprint set of second argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst - | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair + |where: ^ refers to a fresh root capability in the type of value fst + | ^² refers to a fresh root capability created in value twisted when checking argument to parameter fst of constructor PairPair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:33 ------------------------------------------------- 47 | val twisted = swapped(two, two.snd) // error | ^^^^^^^ @@ -56,7 +56,7 @@ |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^ |corresponds to capture-polymorphic formal parameter y of type Ref^² |and hides capabilities {two.snd}. - |Some of these overlap with the captures of the first argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + |Some of these overlap with the captures of the first argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. | | Hidden set of current argument : {two.snd} | Hidden footprint of current argument : {two.snd} @@ -64,8 +64,8 @@ | Footprint set of first argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value snd - | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter y of method swapped + |where: ^ refers to a fresh root capability in the type of value snd + | ^² refers to a fresh root capability created in value twisted when checking argument to parameter y of method swapped -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 ------------------------------------------------- 58 | val twoOther = Pair(two.fst, two.snd) // error // error | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index d51870f3eedf..6005eb1a49e6 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -6,8 +6,8 @@ | Another part, Ref^², captures capabilities {r0}. | The two sets overlap at {r0}. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value r1 - | ^² refers to a fresh root capability classified as Mutable in the type of value r1 + | where: ^ refers to a fresh root capability in the type of value r1 + | ^² refers to a fresh root capability in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:13:9 ---------------------------------------------------------- 13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0 | ^^^^^^^^^^^^^^^^ @@ -16,17 +16,17 @@ | Another part, Ref^², captures capabilities {r1*, r0}. | The two sets overlap at {r1*, r0}. | - | where: ^ refers to a fresh root capability classified as Mutable in the result type of method bad - | ^² refers to a fresh root capability classified as Mutable in the result type of method bad - | cap is a fresh root capability classified as Mutable in the type of value r1 - | cap² is a fresh root capability classified as Mutable in the type of value r1 + | where: ^ refers to a fresh root capability in the result type of method bad + | ^² refers to a fresh root capability in the result type of method bad + | cap is a fresh root capability in the type of value r1 + | cap² is a fresh root capability in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:43:18 --------------------------------------------------------- 43 | val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error | ^^^^^^^^^^^^^^^^ - | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {fstSame}. - | Another part, Ref^², captures capabilities {sndSame, same.snd*}. - | The two sets overlap at {cap of value same}. + | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. + | One part, Ref^, hides capabilities {fstSame}. + | Another part, Ref^², captures capabilities {sndSame, same.snd*}. + | The two sets overlap at {cap of value same}. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair - | ^² refers to a fresh root capability classified as Mutable in the type of value sameToPair + | where: ^ refers to a fresh root capability in the type of value sameToPair + | ^² refers to a fresh root capability in the type of value sameToPair diff --git a/tests/neg-custom-args/captures/var-access.check b/tests/neg-custom-args/captures/var-access.check new file mode 100644 index 000000000000..63028ba807cc --- /dev/null +++ b/tests/neg-custom-args/captures/var-access.check @@ -0,0 +1,18 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:9:21 ------------------------------------ +9 | val _: () -> Int = f // error + | ^ + | Found: (f : () ->{a.rd} Int) + | Required: () -> Int + | + | Note that capability a.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:12:22 ----------------------------------- +12 | val _: () -> Unit = g // error + | ^ + | Found: (g : () ->{a} Unit) + | Required: () -> Unit + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/var-access.scala b/tests/neg-custom-args/captures/var-access.scala new file mode 100644 index 000000000000..c3d5a2cab50c --- /dev/null +++ b/tests/neg-custom-args/captures/var-access.scala @@ -0,0 +1,18 @@ +import caps.* +class A extends Mutable: + var x: Int = 0 + +def test = + val a = A() + val f = () => a.x + val _: () ->{a.rd} Int = f + val _: () -> Int = f // error + val g = () => a.x += 1 + val _: () ->{a} Unit = g + val _: () -> Unit = g // error + + + + + + diff --git a/tests/pos-custom-args/captures/lazyref-mutvar.scala b/tests/pos-custom-args/captures/lazyref-mutvar.scala index 541f8da94595..e071ad4ef0b0 100644 --- a/tests/pos-custom-args/captures/lazyref-mutvar.scala +++ b/tests/pos-custom-args/captures/lazyref-mutvar.scala @@ -1,7 +1,9 @@ import compiletime.uninitialized +import caps.unsafe.untrackedCaptures + class LazyRef[T](val mkElem: () => T): - transparent var elem: T = uninitialized - transparent var evaluated = false + @untrackedCaptures var elem: T = uninitialized + @untrackedCaptures var evaluated = false def get: T = if !evaluated then elem = mkElem() diff --git a/tests/pos-custom-args/captures/mark-free-ro.scala b/tests/pos-custom-args/captures/mark-free-ro.scala new file mode 100644 index 000000000000..625b6ba7813c --- /dev/null +++ b/tests/pos-custom-args/captures/mark-free-ro.scala @@ -0,0 +1,13 @@ +import caps.{cap, Mutable} +import caps.unsafe.untrackedCaptures + +class Test extends Mutable: + var ctxStack: Array[FreshCtx^] = new Array(10) + + class FreshCtx(level: Int) extends Mutable: + this: FreshCtx^ => + def detached: Boolean = + val c: FreshCtx^{cap.rd} = ctxStack(level) + (c eq this) + def detached2 = + ctxStack(level) eq this diff --git a/tests/pos-custom-args/captures/mut-iterator.scala b/tests/pos-custom-args/captures/mut-iterator.scala new file mode 100644 index 000000000000..c019f0cc95ff --- /dev/null +++ b/tests/pos-custom-args/captures/mut-iterator.scala @@ -0,0 +1,30 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + consume def map[U](consume f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](consume it: Iterator[T]^, consume f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/pos-custom-args/captures/restrict-try.scala b/tests/pos-custom-args/captures/restrict-try.scala index fc2a09ecb535..b6be00f69fd7 100644 --- a/tests/pos-custom-args/captures/restrict-try.scala +++ b/tests/pos-custom-args/captures/restrict-try.scala @@ -1,11 +1,11 @@ -import caps.{SharedCapability, Control, Mutable} +import caps.{SharedCapability, Control, Read} class Try[+T] case class Ok[T](x: T) extends Try[T] case class Fail(ex: Exception) extends Try[Nothing] -trait Matrix extends Mutable: - update def update(): Unit +trait Matrix extends Read: + def get(): Unit trait Label extends Control: def break(): Unit @@ -19,7 +19,7 @@ def Test(m: Matrix^, l: Label) = val x = Try: val b = () => - m.update() + m.get() l.break() val _: () ->{m, l} Unit = b b diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala new file mode 100644 index 000000000000..002410e2afd4 --- /dev/null +++ b/tests/pos-custom-args/captures/ro-array.scala @@ -0,0 +1,22 @@ +import caps.* +object Test + +class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Mutable: + private val arr: Array[T] = new Array[T](len) + def get(i: Int): T = arr(i) + update def set(i: Int, x: T): Unit = arr(i) = x + +class Async extends SharedCapability + +def f[T](x: T): T & Pure = x.asInstanceOf[T & Pure] + +def test = + def x(async: Async): Arr[String]^{cap.rd} = + val y = Arr[String](async, 10) + for i <- 0 to 10 do + y.set(i, "A") + val z = f(y) + y + + + diff --git a/tests/pos-custom-args/captures/transparent-mutvars.scala b/tests/pos-custom-args/captures/untracked-mutvars.scala similarity index 91% rename from tests/pos-custom-args/captures/transparent-mutvars.scala rename to tests/pos-custom-args/captures/untracked-mutvars.scala index 6ccc3517fe85..3810217eac67 100644 --- a/tests/pos-custom-args/captures/transparent-mutvars.scala +++ b/tests/pos-custom-args/captures/untracked-mutvars.scala @@ -1,5 +1,6 @@ +import caps.unsafe.untrackedCaptures class Ref[T](init: T) extends caps.Mutable: - transparent var fld: T = init + @untrackedCaptures var fld: T = init def hide(x: T) = this.fld = x // ok update def hide2(x: T) = this.fld = x // ok