From 74b6bf610e32370b70ee9d5383e304961129990b Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Wed, 18 Sep 2024 15:33:16 +0200 Subject: [PATCH 1/8] Add path support for cc --- compiler/src/dotty/tools/dotc/ast/untpd.scala | 4 +- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 3 +- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 84 +++++++++----- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 8 +- .../dotty/tools/dotc/cc/CheckCaptures.scala | 106 ++++++++++-------- .../dotty/tools/dotc/parsing/Parsers.scala | 28 ++--- .../captures/class-contra.check | 13 +-- .../captures/class-contra.scala | 3 +- .../captures/explain-under-approx.check | 14 +-- .../captures/filevar-multi-ios.scala | 41 +++++++ tests/neg-custom-args/captures/i15116.check | 16 ++- tests/neg-custom-args/captures/path-box.scala | 20 ++++ .../captures/path-connection.scala | 46 ++++++++ .../captures/path-illigal.scala | 7 ++ .../captures/path-simple.scala | 27 +++++ .../neg-custom-args/captures/singletons.scala | 8 +- .../captures/filevar-expanded.scala | 3 +- tests/pos-custom-args/captures/filevar.scala | 3 +- 18 files changed, 314 insertions(+), 120 deletions(-) create mode 100644 tests/neg-custom-args/captures/filevar-multi-ios.scala create mode 100644 tests/neg-custom-args/captures/path-box.scala create mode 100644 tests/neg-custom-args/captures/path-connection.scala create mode 100644 tests/neg-custom-args/captures/path-illigal.scala create mode 100644 tests/neg-custom-args/captures/path-simple.scala diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala index 60309d4d83bd..b86734afcc0a 100644 --- a/compiler/src/dotty/tools/dotc/ast/untpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala @@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo { def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated = Annotated(parent, New(scalaAnnotationDot(annotName), List(refs))) - def makeCapsOf(id: Ident)(using Context): Tree = - TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil) + def makeCapsOf(tp: Tree)(using Context): Tree = + TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil) def makeCapsBound()(using Context): Tree = makeRetaining( diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 29c6528e36de..79cc7d136e45 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -194,7 +194,8 @@ extension (tp: Type) true case tp: TermRef => ((tp.prefix eq NoPrefix) - || tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner) + || tp.symbol.isField && !tp.symbol.isStatic && ( + tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef) || tp.isRootCapability ) && !tp.symbol.isOneOf(UnstableValueFlags) case tp: TypeRef => diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index f00c6869cd80..05162907b608 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType: case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists) case _ => false - /** Normalize reference so that it can be compared with `eq` for equality */ - final def normalizedRef(using Context): CaptureRef = this match - case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef => - tp.derivedAnnotatedType(parent.normalizedRef, annot) - case tp: TermRef if tp.isTrackableRef => - tp.symbol.termRef - case _ => this + // With the support of pathes, we don't need to normalize the `TermRef`s anymore. + // /** Normalize reference so that it can be compared with `eq` for equality */ + // final def normalizedRef(using Context): CaptureRef = this match + // case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef => + // tp.derivedAnnotatedType(parent.normalizedRef, annot) + // case tp: TermRef if tp.isTrackableRef => + // tp.symbol.termRef + // case _ => this /** The capture set consisting of exactly this reference */ final def singletonCaptureSet(using Context): CaptureSet.Const = if mySingletonCaptureSet == null then - mySingletonCaptureSet = CaptureSet(this.normalizedRef) + mySingletonCaptureSet = CaptureSet(this) mySingletonCaptureSet.uncheckedNN /** The capture set of the type underlying this reference */ @@ -99,25 +100,56 @@ trait CaptureRef extends TypeProxy, ValueType: * x: x1.type /\ x1 subsumes y ==> x subsumes y */ final def subsumes(y: CaptureRef)(using Context): Boolean = - (this eq y) - || this.isRootCapability - || y.match - case y: TermRef => - (y.prefix eq this) - || y.info.match - case y1: SingletonCaptureRef => this.subsumes(y1) - case _ => false - case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) - case _ => false - || this.match - case ReachCapability(x1) => x1.subsumes(y.stripReach) - case x: TermRef => - x.info match - case x1: SingletonCaptureRef => x1.subsumes(y) + def compareCaptureRefs(x: Type, y: Type): Boolean = + (x eq y) + || y.match + case y: CaptureRef => x.match + case x: CaptureRef => x.subsumes(y) case _ => false - case x: TermParamRef => subsumesExistentially(x, y) - case x: TypeRef => assumedContainsOf(x).contains(y) - case _ => false + case _ => false + + def compareUndelying(x: Type): Boolean = x match + case x: SingletonCaptureRef => x.subsumes(y) + case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) + case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) + case _ => false + + if (this eq y) || this.isRootCapability then return true + + // similar to compareNamed in TypeComparer + y match + case y: TermRef => + this match + case x: TermRef => + val xSym = x.symbol + val ySym = y.symbol + + // check x.f and y.f + if (xSym ne NoSymbol) + && (xSym eq ySym) + && compareCaptureRefs(x.prefix, y.prefix) + || (x.name eq y.name) + && x.isPrefixDependentMemberRef + && compareCaptureRefs(x.prefix, y.prefix) + && x.signature == y.signature + && !(xSym.isClass && ySym.isClass) + then return true + case _ => + + // shorten + if compareCaptureRefs(this, y.prefix) then return true + // underlying + if compareCaptureRefs(this, y.info) then return true + case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1) + case _ => + + return this.match + case ReachCapability(x1) => x1.subsumes(y.stripReach) + case x: TermRef => compareUndelying(x.info) + case CapturingType(x1, _) => compareUndelying(x1) + case x: TermParamRef => subsumesExistentially(x, y) + case x: TypeRef => assumedContainsOf(x).contains(y) + case _ => false def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 44d5e2cf4b88..81b4287961ba 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -374,7 +374,7 @@ object CaptureSet: def apply(elems: CaptureRef*)(using Context): CaptureSet.Const = if elems.isEmpty then empty - else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*)) + else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*)) def apply(elems: Refs)(using Context): CaptureSet.Const = if elems.isEmpty then empty else Const(elems) @@ -508,7 +508,11 @@ object CaptureSet: !noUniversal else elem match case elem: TermRef if level.isDefined => - elem.symbol.ccLevel <= level + elem.prefix match + case prefix: CaptureRef => + levelOK(prefix) + case _ => + elem.symbol.ccLevel <= level case elem: ThisType if level.isDefined => elem.cls.ccLevel.nextInner <= level case ReachCapability(elem1) => diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index b05ab8542137..ec1e63137311 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -122,10 +122,6 @@ object CheckCaptures: * This check is performed at Typer. */ def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit = - parent.tpe match - case _: SingletonType => - report.error(em"Singleton type $parent cannot have capture set", parent.srcPos) - case _ => def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match case ref: CaptureRef => if !ref.isTrackableRef then @@ -373,45 +369,54 @@ class CheckCaptures extends Recheck, SymTransformer: * the environment's owner */ def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit = + // A captured reference with the symbol `sym` is visible from the environment + // if `sym` is not defined inside the owner of the environment. + inline def isVisibleFromEnv(sym: Symbol, env: Env) = + if env.kind == EnvKind.NestedInOwner then + !sym.isProperlyContainedIn(env.owner) + else + !sym.isContainedIn(env.owner) + + def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit = + // Only captured references that are visible from the environment + // should be included. + val included = cs.filter: c => + c.stripReach match + case ref: NamedType => + val refSym = ref.symbol + val refOwner = refSym.owner + val isVisible = isVisibleFromEnv(refOwner, env) + if isVisible && !ref.isRootCapability then + ref match + case ref: TermRef if ref.prefix `ne` NoPrefix => + // If c is a path of a class defined outside the environment, + // we check the capture set of its info. + checkSubsetEnv(ref.captureSetOfInfo, env) + case _ => + if !isVisible + && (c.isReach || ref.isType) + && (!ccConfig.useSealed || refSym.is(Param)) + && refOwner == env.owner + then + if refSym.hasAnnotation(defn.UnboxAnnot) then + capt.println(i"exempt: $ref in $refOwner") + else + // Reach capabilities that go out of scope have to be approximated + // by their underlying capture set, which cannot be universal. + // Reach capabilities of @unboxed parameters are exempted. + val cs = CaptureSet.ofInfo(c) + cs.disallowRootCapability: () => + report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) + checkSubset(cs, env.captured, pos, provenance(env)) + isVisible + case ref: ThisType => isVisibleFromEnv(ref.cls, env) + case _ => false + checkSubset(included, env.captured, pos, provenance(env)) + capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") + if !cs.isAlwaysEmpty then forallOuterEnvsUpTo(ctx.owner.topLevelClass): env => - // Whether a symbol is defined inside the owner of the environment? - inline def isContainedInEnv(sym: Symbol) = - if env.kind == EnvKind.NestedInOwner then - sym.isProperlyContainedIn(env.owner) - else - sym.isContainedIn(env.owner) - // A captured reference with the symbol `sym` is visible from the environment - // if `sym` is not defined inside the owner of the environment - inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym) - // Only captured references that are visible from the environment - // should be included. - val included = cs.filter: c => - c.stripReach match - case ref: NamedType => - val refSym = ref.symbol - val refOwner = refSym.owner - val isVisible = isVisibleFromEnv(refOwner) - if !isVisible - && (c.isReach || ref.isType) - && (!ccConfig.useSealed || refSym.is(Param)) - && refOwner == env.owner - then - if refSym.hasAnnotation(defn.UnboxAnnot) then - capt.println(i"exempt: $ref in $refOwner") - else - // Reach capabilities that go out of scope have to be approximated - // by their underlying capture set, which cannot be universal. - // Reach capabilities of @unboxed parameters are exempted. - val cs = CaptureSet.ofInfo(c) - cs.disallowRootCapability: () => - report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) - checkSubset(cs, env.captured, pos, provenance(env)) - isVisible - case ref: ThisType => isVisibleFromEnv(ref.cls) - case _ => false - checkSubset(included, env.captured, pos, provenance(env)) - capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") + checkSubsetEnv(cs, env) end markFree /** Include references captured by the called method in the current environment stack */ @@ -488,21 +493,28 @@ class CheckCaptures extends Recheck, SymTransformer: case _ => denot val selType = recheckSelection(tree, qualType, name, disambiguate) - val selCs = selType.widen.captureSet - if selCs.isAlwaysEmpty - || selType.widen.isBoxedCapturing + val selWiden = selType.widen + def isStableSel = selType match + case selType: NamedType => selType.symbol.isStableMember + case _ => false + + if pt == LhsProto || qualType.isBoxedCapturing - || pt == LhsProto + || selType.isTrackableRef + || selWiden.isBoxedCapturing + || selWiden.captureSet.isAlwaysEmpty then selType else val qualCs = qualType.captureSet - capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree") + val selCs = selType.captureSet + capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree") + if qualCs.mightSubcapture(selCs) && !selCs.mightSubcapture(qualCs) && !pt.stripCapturing.isInstanceOf[SingletonType] then - selType.widen.stripCapturing.capturing(qualCs) + selWiden.stripCapturing.capturing(qualCs) .showing(i"alternate type for select $tree: $selType --> $result, $qualCs / $selCs", capt) else selType diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index 8a173faa3cec..96f09a0d6214 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -1548,21 +1548,23 @@ object Parsers { case _ => None } - /** CaptureRef ::= ident [`*` | `^`] | `this` + /** CaptureRef ::= (ident | `this`) [`*` | `^`] */ def captureRef(): Tree = - if in.token == THIS then simpleRef() - else - val id = termIdent() - if isIdent(nme.raw.STAR) then - in.nextToken() - atSpan(startOffset(id)): - PostfixOp(id, Ident(nme.CC_REACH)) - else if isIdent(nme.UPARROW) then - in.nextToken() - atSpan(startOffset(id)): - makeCapsOf(cpy.Ident(id)(id.name.toTypeName)) - else id + val ref = singleton() + if isIdent(nme.raw.STAR) then + in.nextToken() + atSpan(startOffset(ref)): + PostfixOp(ref, Ident(nme.CC_REACH)) + else if isIdent(nme.UPARROW) then + in.nextToken() + def toTypeSel(r: Tree): Tree = r match + case id: Ident => cpy.Ident(id)(id.name.toTypeName) + case Select(qual, id) => Select(qual, id.toTypeName) + case _ => r + atSpan(startOffset(ref)): + makeCapsOf(toTypeSel(ref)) + else ref /** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking */ diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check index 9fc009ac3d48..808118bd1795 100644 --- a/tests/neg-custom-args/captures/class-contra.check +++ b/tests/neg-custom-args/captures/class-contra.check @@ -1,10 +1,7 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 --------------------------------- -12 | def fun(x: K{val f: T^{a}}) = x.setf(a) // error - | ^ - | Found: (a : T^{x, y}) - | Required: T^{} - | - | Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position - | was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:40 --------------------------------- +12 | def fun1(k: K{val f: T^{a}}) = k.setf(a) // error + | ^ + | Found: (a : T^{x, y}) + | Required: T^{k.f} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/class-contra.scala b/tests/neg-custom-args/captures/class-contra.scala index 210fd4e331f1..8ef8e7485a18 100644 --- a/tests/neg-custom-args/captures/class-contra.scala +++ b/tests/neg-custom-args/captures/class-contra.scala @@ -9,5 +9,6 @@ class T def test(x: Cap, y: Cap) = val a: T^{x, y} = ??? - def fun(x: K{val f: T^{a}}) = x.setf(a) // error + def fun1(k: K{val f: T^{a}}) = k.setf(a) // error + def fun2(k: K{val f: a.type}) = k.setf(a) () \ No newline at end of file diff --git a/tests/neg-custom-args/captures/explain-under-approx.check b/tests/neg-custom-args/captures/explain-under-approx.check index 2d2b05b4b95a..c186fc6adb11 100644 --- a/tests/neg-custom-args/captures/explain-under-approx.check +++ b/tests/neg-custom-args/captures/explain-under-approx.check @@ -1,20 +1,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 ------------------------- 12 | col.add(Future(() => 25)) // error | ^^^^^^^^^^^^^^^^ - | Found: Future[Int]{val a: (async : Async^)}^{async} - | Required: Future[Int]^{} - | - | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position - | was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{col.futs*} | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 ------------------------- 15 | col1.add(Future(() => 25)) // error | ^^^^^^^^^^^^^^^^ - | Found: Future[Int]{val a: (async : Async^)}^{async} - | Required: Future[Int]^{} - | - | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position - | was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{col1.futs*} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/filevar-multi-ios.scala b/tests/neg-custom-args/captures/filevar-multi-ios.scala new file mode 100644 index 000000000000..8ffc8d8e299c --- /dev/null +++ b/tests/neg-custom-args/captures/filevar-multi-ios.scala @@ -0,0 +1,41 @@ +import language.experimental.modularity +import compiletime.uninitialized + +class IO extends caps.Capability + +class File: + def write(x: String): Unit = ??? + +object test1: + + class Service(val io: IO, val io2: IO): + var file: File^{io} = uninitialized + var file2: File^{io2} = uninitialized + def log = file.write("log") + + def withFile[T](io: IO)(op: File^{io} => T): T = + op(new File) + + def test(io3: IO, io4: IO) = + withFile(io3): f => + val o = Service(io3, io4) + o.file = f // error + o.file2 = f // error + o.log + +object test2: + + class Service(tracked val io: IO, tracked val io2: IO): + var file: File^{io} = uninitialized + var file2: File^{io2} = uninitialized + def log = file.write("log") + + def withFile[T](io: IO)(op: File^{io} => T): T = + op(new File) + + def test(io3: IO, io4: IO) = + withFile(io3): f => + val o = Service(io3, io4) + o.file = f + o.file2 = f // error + o.log diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check index df05324866e1..0a16af9f6704 100644 --- a/tests/neg-custom-args/captures/i15116.check +++ b/tests/neg-custom-args/captures/i15116.check @@ -18,13 +18,17 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ---------------------------------------- 5 | val x = Foo(m) // error | ^^^^^^ - | Found: Foo{val m: String^{Baz.this}}^{Baz.this} + | Found: Foo{val m²: (Baz.this.m : String^)}^{Baz.this.m} | Required: Foo | + | where: m is a value in trait Baz + | m² is a value in class Foo + | + | | Note that the expected type Foo | is the previously inferred type of value x | which is also the type seen in separately compiled sources. - | The new inferred type Foo{val m: String^{Baz.this}}^{Baz.this} + | The new inferred type Foo{val m: (Baz.this.m : String^)}^{Baz.this.m} | must conform to this type. | | longer explanation available when compiling with `-explain` @@ -48,13 +52,17 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ---------------------------------------- 9 | val x = Foo(m) // error | ^^^^^^ - | Found: Foo{val m: String^{Baz2.this}}^{Baz2.this} + | Found: Foo{val m²: (Baz2.this.m : String^)}^{Baz2.this.m} | Required: Foo | + | where: m is a value in trait Baz2 + | m² is a value in class Foo + | + | | Note that the expected type Foo | is the previously inferred type of value x | which is also the type seen in separately compiled sources. - | The new inferred type Foo{val m: String^{Baz2.this}}^{Baz2.this} + | The new inferred type Foo{val m: (Baz2.this.m : String^)}^{Baz2.this.m} | must conform to this type. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/path-box.scala b/tests/neg-custom-args/captures/path-box.scala new file mode 100644 index 000000000000..3213c236aaf5 --- /dev/null +++ b/tests/neg-custom-args/captures/path-box.scala @@ -0,0 +1,20 @@ +class A: + val m: A^ = ??? + val self: this.type = this + +case class Box[+T](value: T) + +def testBox1(a: A^): Box[A^{a}] = + Box(a.m) + +def testBox2(a: A^): Box[A^{a.m}] = + Box(a.m) + +def testBox3(a: A^): Box[A^{a.m}] = + Box(a) // error + +def testBox4(a: A^): Box[A^{a.m}] = + Box(a.m.m.m) + +def testBox5(a: A^): Box[A^{a.m}] = + Box(a.m.m.self) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-connection.scala b/tests/neg-custom-args/captures/path-connection.scala new file mode 100644 index 000000000000..3b3820488c8d --- /dev/null +++ b/tests/neg-custom-args/captures/path-connection.scala @@ -0,0 +1,46 @@ +import language.experimental.modularity + +trait Reader: + def read(): String + +trait Sender: + def send(msg: String): Unit + +class Connection extends Reader, Sender: + def read() = "hello" + def send(msg: String) = () + + val readOnly: Reader^ = new Reader: + def read() = Connection.this.read() + +class ReaderProxy(tracked val r: Reader^) extends Reader: + def read() = "(Proxy)" + r.read() + +class SenderProxy(tracked val s: Sender^) extends Sender: + def send(msg: String) = s.send("(Proxy) " + msg) + +def testConnection(c: Connection^)( + handle1: Reader^{c.readOnly} => String, + handle2: Sender^{c} => Unit, + handle3: Reader^{c} => String, + ) = + val m1 = c.read() + c.send("hello") + + val m2 = c.readOnly.read() + + val m3a = handle1(c.readOnly) + val m3b = handle3(c.readOnly) + + val m4a = handle1(c) // error + val m4b = handle3(c) + + val m5a = handle1(new ReaderProxy(c.readOnly)) + val m5b = handle3(new ReaderProxy(c.readOnly)) + + val m6a = handle1(new ReaderProxy(c)) // error + val m6b = handle3(new ReaderProxy(c)) + + handle2(c) + + handle2(new SenderProxy(c)) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-illigal.scala b/tests/neg-custom-args/captures/path-illigal.scala new file mode 100644 index 000000000000..f09db0087ef7 --- /dev/null +++ b/tests/neg-custom-args/captures/path-illigal.scala @@ -0,0 +1,7 @@ +class A: + val m: A^ = ??? + var n: A^ = ??? + +def test1(a: A^) = + val c1: A^{a.m} = a.m + val f1: A^{a.n} = a.n // error \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-simple.scala b/tests/neg-custom-args/captures/path-simple.scala new file mode 100644 index 000000000000..93b6dacebe74 --- /dev/null +++ b/tests/neg-custom-args/captures/path-simple.scala @@ -0,0 +1,27 @@ + +class A: + val m: A^ = ??? + val self: this.type = this + +case class C(ca: A^) + +def test1(a: A^, b: A^) = + val c1: A^{a} = a.m + val c2: A^{a.m} = a.m + val c3: A^{b} = a.m // error + + val d1: A^{a} = a.self + val d2: A^{a.self} = a.self + val d3: A^{a.self} = a + + val e1: A^{a.m} = a.self.m + val e2: A^{a.self.m} = a.self.m + val e3: A^{a.self.m} = a.m + +def test2(a: A^) = + val b: a.type = a + val c1: C^{a} = new C(a) + val c2: C^{a} = new C(a.m) + val c3: C^{a.m} = new C(a.m) + val c4: C^{b} = new C(a) + val c5: C^{a} = new C(b) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/singletons.scala b/tests/neg-custom-args/captures/singletons.scala index 194e6e850dcd..be0ee67ab1bc 100644 --- a/tests/neg-custom-args/captures/singletons.scala +++ b/tests/neg-custom-args/captures/singletons.scala @@ -1,6 +1,6 @@ val x = () => () -val y1: x.type = x // ok -val y2: x.type^{} = x // error: singleton type cannot have capture set -val y3: x.type^{x} = x // error: singleton type cannot have capture set // error -val y4: x.type^ = x // error: singleton type cannot have capture set +val y1: x.type = x +val y2: x.type^{} = x +val y3: x.type^{x} = x // error +val y4: x.type^ = x diff --git a/tests/pos-custom-args/captures/filevar-expanded.scala b/tests/pos-custom-args/captures/filevar-expanded.scala index a883471e8d2e..58e7a0e67e0a 100644 --- a/tests/pos-custom-args/captures/filevar-expanded.scala +++ b/tests/pos-custom-args/captures/filevar-expanded.scala @@ -1,4 +1,5 @@ import language.experimental.captureChecking +import language.experimental.modularity import compiletime.uninitialized object test1: @@ -22,7 +23,7 @@ object test2: class File: def write(x: String): Unit = ??? - class Service(io: IO^): + class Service(tracked val io: IO^): var file: File^{io} = uninitialized def log = file.write("log") diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala index 9ab34fe617b5..dc8d0b18908b 100644 --- a/tests/pos-custom-args/captures/filevar.scala +++ b/tests/pos-custom-args/captures/filevar.scala @@ -1,4 +1,5 @@ import language.experimental.captureChecking +import language.experimental.modularity import compiletime.uninitialized object test1: @@ -22,7 +23,7 @@ object test2: class File: def write(x: String): Unit = ??? - class Service(io: IO): + class Service(tracked val io: IO): var file: File^{io} = uninitialized def log = file.write("log") From ddba6082ba08487d528f773232ad3094e055a874 Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Thu, 19 Sep 2024 15:30:57 +0200 Subject: [PATCH 2/8] Add comment for path-dependent limitation --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 5 +---- compiler/src/dotty/tools/dotc/cc/Setup.scala | 5 +++++ tests/neg-custom-args/captures/path-connection.scala | 2 ++ 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ec1e63137311..b3a1ab44d6cd 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -494,10 +494,7 @@ class CheckCaptures extends Recheck, SymTransformer: val selType = recheckSelection(tree, qualType, name, disambiguate) val selWiden = selType.widen - def isStableSel = selType match - case selType: NamedType => selType.symbol.isStableMember - case _ => false - + if pt == LhsProto || qualType.isBoxedCapturing || selType.isTrackableRef diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 22e7899eeea1..76ae41649517 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -518,6 +518,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: info match case mt: MethodOrPoly => val psyms = psymss.head + // TODO: the substitution does not work for param-dependent method types. + // For example, `(x: T, y: x.f.type) => Unit`. In this case, when we + // substitute `x.f.type`, `x` becomes a `TermParamRef`. But the new method + // type is still under initialization and `paramInfos` is still `null`, + // so the new `NamedType` will not have a denoation. mt.companion(mt.paramNames)( mt1 => if !paramSignatureChanges && !mt.isParamDependent && prevLambdas.isEmpty then diff --git a/tests/neg-custom-args/captures/path-connection.scala b/tests/neg-custom-args/captures/path-connection.scala index 3b3820488c8d..c65aa75b1ed2 100644 --- a/tests/neg-custom-args/captures/path-connection.scala +++ b/tests/neg-custom-args/captures/path-connection.scala @@ -19,6 +19,8 @@ class ReaderProxy(tracked val r: Reader^) extends Reader: class SenderProxy(tracked val s: Sender^) extends Sender: def send(msg: String) = s.send("(Proxy) " + msg) +// TODO: We have to put `c` in the different argument list to make it work. +// See the comments in `integrateRT`. def testConnection(c: Connection^)( handle1: Reader^{c.readOnly} => String, handle2: Sender^{c} => Unit, From 440c053213ae75f6fb68581cf9a3ecb4e30785e7 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 24 Sep 2024 18:05:57 +0200 Subject: [PATCH 3/8] Add alternative subsumes implementations This is done for comparing old with new --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 46 +++++++++++++++++-- 1 file changed, 41 insertions(+), 5 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 05162907b608..107b1a178069 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -93,23 +93,59 @@ trait CaptureRef extends TypeProxy, ValueType: final def invalidateCaches() = myCaptureSetRunId = NoRunId + final def subsumes(y: CaptureRef)(using Context): Boolean = + val was = subsumesOld(y) + val now = subsumesNew(y) + if was != now then + println(i"diff for $this subsumes $y, now: $now, ${this.getClass}, ${y.getClass}") + was + + final def subsumesOld(y: CaptureRef)(using Context): Boolean = + (this eq y) + || this.isRootCapability + || y.match + case y: TermRef => + y.prefix.match + case ypre: CaptureRef => + this.subsumesOld(ypre) + || this.match + case x @ TermRef(xpre: CaptureRef, _) => + x.symbol == y.symbol && xpre =:= ypre + case _ => + false + case _ => false + || y.info.match + case y1: SingletonCaptureRef => this.subsumesOld(y1) + case _ => false + case MaybeCapability(y1) => this.stripMaybe.subsumesOld(y1) + case _ => false + || this.match + case ReachCapability(x1) => x1.subsumesOld(y.stripReach) + case x: TermRef => + x.info match + case x1: SingletonCaptureRef => x1.subsumesOld(y) + case _ => false + case x: TermParamRef => subsumesExistentially(x, y) + case x: TypeRef => assumedContainsOf(x).contains(y) + case _ => false + /** x subsumes x * this subsumes this.f * x subsumes y ==> x* subsumes y, x subsumes y? * x subsumes y ==> x* subsumes y*, x? subsumes y? * x: x1.type /\ x1 subsumes y ==> x subsumes y */ - final def subsumes(y: CaptureRef)(using Context): Boolean = + final def subsumesNew(y: CaptureRef)(using Context): Boolean = def compareCaptureRefs(x: Type, y: Type): Boolean = (x eq y) || y.match case y: CaptureRef => x.match - case x: CaptureRef => x.subsumes(y) + case x: CaptureRef => x.subsumesNew(y) case _ => false case _ => false def compareUndelying(x: Type): Boolean = x match - case x: SingletonCaptureRef => x.subsumes(y) + case x: SingletonCaptureRef => x.subsumesNew(y) case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) case _ => false @@ -140,11 +176,11 @@ trait CaptureRef extends TypeProxy, ValueType: if compareCaptureRefs(this, y.prefix) then return true // underlying if compareCaptureRefs(this, y.info) then return true - case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1) + case MaybeCapability(y1) => return this.stripMaybe.subsumesNew(y1) case _ => return this.match - case ReachCapability(x1) => x1.subsumes(y.stripReach) + case ReachCapability(x1) => x1.subsumesNew(y.stripReach) case x: TermRef => compareUndelying(x.info) case CapturingType(x1, _) => compareUndelying(x1) case x: TermParamRef => subsumesExistentially(x, y) From 45df15269d9c237e78a4f4322a7b8e52bfec02e0 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 24 Sep 2024 18:07:50 +0200 Subject: [PATCH 4/8] Revert to previous subsumes scheme Add the path cases without changing the whole logic --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 82 +++---------------- 1 file changed, 12 insertions(+), 70 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 107b1a178069..195f07f778eb 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -93,21 +93,21 @@ trait CaptureRef extends TypeProxy, ValueType: final def invalidateCaches() = myCaptureSetRunId = NoRunId + /** x subsumes x + * this subsumes this.f + * x subsumes y ==> x* subsumes y, x subsumes y? + * x subsumes y ==> x* subsumes y*, x? subsumes y? + * x: x1.type /\ x1 subsumes y ==> x subsumes y + * TODO: Document path cases + */ final def subsumes(y: CaptureRef)(using Context): Boolean = - val was = subsumesOld(y) - val now = subsumesNew(y) - if was != now then - println(i"diff for $this subsumes $y, now: $now, ${this.getClass}, ${y.getClass}") - was - - final def subsumesOld(y: CaptureRef)(using Context): Boolean = (this eq y) || this.isRootCapability || y.match case y: TermRef => y.prefix.match case ypre: CaptureRef => - this.subsumesOld(ypre) + this.subsumes(ypre) || this.match case x @ TermRef(xpre: CaptureRef, _) => x.symbol == y.symbol && xpre =:= ypre @@ -115,78 +115,20 @@ trait CaptureRef extends TypeProxy, ValueType: false case _ => false || y.info.match - case y1: SingletonCaptureRef => this.subsumesOld(y1) + case y1: SingletonCaptureRef => this.subsumes(y1) case _ => false - case MaybeCapability(y1) => this.stripMaybe.subsumesOld(y1) + case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) case _ => false || this.match - case ReachCapability(x1) => x1.subsumesOld(y.stripReach) + case ReachCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => x.info match - case x1: SingletonCaptureRef => x1.subsumesOld(y) + case x1: SingletonCaptureRef => x1.subsumes(y) case _ => false case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) case _ => false - /** x subsumes x - * this subsumes this.f - * x subsumes y ==> x* subsumes y, x subsumes y? - * x subsumes y ==> x* subsumes y*, x? subsumes y? - * x: x1.type /\ x1 subsumes y ==> x subsumes y - */ - final def subsumesNew(y: CaptureRef)(using Context): Boolean = - def compareCaptureRefs(x: Type, y: Type): Boolean = - (x eq y) - || y.match - case y: CaptureRef => x.match - case x: CaptureRef => x.subsumesNew(y) - case _ => false - case _ => false - - def compareUndelying(x: Type): Boolean = x match - case x: SingletonCaptureRef => x.subsumesNew(y) - case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) - case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) - case _ => false - - if (this eq y) || this.isRootCapability then return true - - // similar to compareNamed in TypeComparer - y match - case y: TermRef => - this match - case x: TermRef => - val xSym = x.symbol - val ySym = y.symbol - - // check x.f and y.f - if (xSym ne NoSymbol) - && (xSym eq ySym) - && compareCaptureRefs(x.prefix, y.prefix) - || (x.name eq y.name) - && x.isPrefixDependentMemberRef - && compareCaptureRefs(x.prefix, y.prefix) - && x.signature == y.signature - && !(xSym.isClass && ySym.isClass) - then return true - case _ => - - // shorten - if compareCaptureRefs(this, y.prefix) then return true - // underlying - if compareCaptureRefs(this, y.info) then return true - case MaybeCapability(y1) => return this.stripMaybe.subsumesNew(y1) - case _ => - - return this.match - case ReachCapability(x1) => x1.subsumesNew(y.stripReach) - case x: TermRef => compareUndelying(x.info) - case CapturingType(x1, _) => compareUndelying(x1) - case x: TermParamRef => subsumesExistentially(x, y) - case x: TypeRef => assumedContainsOf(x).contains(y) - case _ => false - def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) From 263d6eb9337f6849ee8aa77941a017d500af68ff Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Sep 2024 11:57:39 +0200 Subject: [PATCH 5/8] Add logic to mark paths as used If we refer to a path `a.b`, we should mark `a.b` as used, which is better than marking `a`. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 27 +++++++++++++------ .../dotty/tools/dotc/transform/Recheck.scala | 15 +++++------ .../dotty/tools/dotc/typer/ProtoTypes.scala | 6 +++-- tests/pos-custom-args/captures/path-use.scala | 19 +++++++++++++ 4 files changed, 49 insertions(+), 18 deletions(-) create mode 100644 tests/pos-custom-args/captures/path-use.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index b3a1ab44d6cd..05bcecf86067 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -13,7 +13,7 @@ import Trees.* import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker} import typer.Checking.{checkBounds, checkAppliedTypesIn} import typer.ErrorReporting.{Addenda, NothingToAdd, err} -import typer.ProtoTypes.{AnySelectionProto, LhsProto} +import typer.ProtoTypes.{LhsProto, WildcardSelectionProto} import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* @@ -183,6 +183,9 @@ object CheckCaptures: /** Attachment key for bodies of closures, provided they are values */ val ClosureBodyValue = Property.Key[Unit] + /** A prototype that indicates selection with an immutable value */ + class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto + class CheckCaptures extends Recheck, SymTransformer: thisPhase => @@ -357,12 +360,13 @@ class CheckCaptures extends Recheck, SymTransformer: * the environment in which `sym` is defined. */ def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit = - if sym.exists then - val ref = sym.termRef - if ref.isTracked then - forallOuterEnvsUpTo(sym.enclosure): env => - capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}") - checkElem(ref, env.captured, pos, provenance(env)) + markFree(sym, sym.termRef, pos) + + def markFree(sym: Symbol, ref: TermRef, pos: SrcPos)(using Context): Unit = + if sym.exists && ref.isTracked then + forallOuterEnvsUpTo(sym.enclosure): env => + capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}") + checkElem(ref, env.captured, pos, provenance(env)) /** Make sure (projected) `cs` is a subset of the capture sets of all enclosing * environments. At each stage, only include references from `cs` that are outside @@ -464,9 +468,16 @@ class CheckCaptures extends Recheck, SymTransformer: includeCallCaptures(tree.symbol, tree.srcPos) else //debugShowEnvs() - markFree(tree.symbol, tree.srcPos) + def addSelects(ref: TermRef, pt: Type): TermRef = pt match + case pt: PathSelectionProto => addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) + case _ => ref + markFree(tree.symbol, addSelects(tree.symbol.termRef, pt), tree.srcPos) super.recheckIdent(tree, pt) + override def selectionProto(tree: Select, pt: Type)(using Context): Type = + if !tree.symbol.isOneOf(UnstableValueFlags) then PathSelectionProto(tree.symbol, pt) + else super.selectionProto(tree, pt) + /** A specialized implementation of the selection rule. * * E |- f: T{ m: R^Cr }^{f} diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala index 03f0001110d3..26a75215bab1 100644 --- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala +++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala @@ -12,7 +12,7 @@ import DenotTransformers.{DenotTransformer, IdentityDenotTransformer, SymTransfo import NamerOps.linkConstructorParams import NullOpsDecorator.stripNull import typer.ErrorReporting.err -import typer.ProtoTypes.* +import typer.ProtoTypes.{AnySelectionProto, LhsProto} import typer.TypeAssigner.seqLitType import typer.ConstFold import typer.ErrorReporting.{Addenda, NothingToAdd} @@ -203,13 +203,12 @@ abstract class Recheck extends Phase, SymTransformer: tree.tpe def recheckSelect(tree: Select, pt: Type)(using Context): Type = - recheckSelection(tree, recheckSelectQualifier(tree), tree.name, pt) + recheckSelection(tree, + recheck(tree.qualifier, selectionProto(tree, pt)).widenIfUnstable, + tree.name, pt) - def recheckSelectQualifier(tree: Select)(using Context): Type = - val proto = - if tree.symbol == defn.Any_asInstanceOf then WildcardType - else AnySelectionProto - recheck(tree.qualifier, proto).widenIfUnstable + def selectionProto(tree: Select, pt: Type)(using Context): Type = + if tree.symbol == defn.Any_asInstanceOf then WildcardType else AnySelectionProto def recheckSelection(tree: Select, qualType: Type, name: Name, sharpen: Denotation => Denotation)(using Context): Type = @@ -308,7 +307,7 @@ abstract class Recheck extends Phase, SymTransformer: def recheckApply(tree: Apply, pt: Type)(using Context): Type = val (funtpe0, qualType) = tree.fun match case fun: Select => - val qualType = recheckSelectQualifier(fun) + val qualType = recheck(fun.qualifier, selectionProto(fun, WildcardType)).widenIfUnstable (recheckSelection(fun, qualType, fun.name, WildcardType), qualType) case _ => (recheck(tree.fun), NoType) diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala index a69a63d1ceef..53e0b456ed9a 100644 --- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala +++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala @@ -324,6 +324,8 @@ object ProtoTypes { case tp: UnapplyFunProto => new UnapplySelectionProto(name, nameSpan) case tp => SelectionProto(name, IgnoredProto(tp), typer, privateOK = true, nameSpan) + class WildcardSelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + /** A prototype for expressions [] that are in some unspecified selection operation * * [].?: ? @@ -332,9 +334,9 @@ object ProtoTypes { * operation is further selection. In this case, the expression need not be a value. * @see checkValue */ - @sharable object AnySelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + @sharable object AnySelectionProto extends WildcardSelectionProto - @sharable object SingletonTypeProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + @sharable object SingletonTypeProto extends WildcardSelectionProto /** A prototype for selections in pattern constructors */ class UnapplySelectionProto(name: Name, nameSpan: Span) extends SelectionProto(name, WildcardType, NoViewsAllowed, true, nameSpan) diff --git a/tests/pos-custom-args/captures/path-use.scala b/tests/pos-custom-args/captures/path-use.scala new file mode 100644 index 000000000000..5eb2b60fd218 --- /dev/null +++ b/tests/pos-custom-args/captures/path-use.scala @@ -0,0 +1,19 @@ +import language.experimental.namedTuples + +class IO + +class C(val f: IO^): + val procs: List[Proc] = ??? + +type Proc = () => Unit + +def test(io: IO^) = + val c = C(io) + val f = () => println(c.f) + val _: () ->{c.f} Unit = f + + val x = c.procs + val _: List[() ->{c.procs*} Unit] = x + + val g = () => println(c.procs.head) + val _: () ->{c.procs*} Unit = g From 152710b04a7f14a5aba57a3d828865b58bbb5855 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Sep 2024 21:01:05 +0200 Subject: [PATCH 6/8] Tweaks to path checking and massage tests Needed to make stdlib2-cc go through. There were two errors. One in LayListIterable required a type annotation and a tweak to markFree. The other in Vieew.scala required a cast, but this could be fixed with better handling of pattern matching. path-patmat-should-be-pos.scala is a minimization. --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 27 ++++++++++++------- .../dotty/tools/dotc/cc/CheckCaptures.scala | 25 ++++++++++++----- .../src/scala/collection/View.scala | 5 +++- .../immutable/LazyListIterable.scala | 4 ++- .../captures/path-patmat-should-be-pos.scala | 26 ++++++++++++++++++ 5 files changed, 69 insertions(+), 18 deletions(-) create mode 100644 tests/neg-custom-args/captures/path-patmat-should-be-pos.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 195f07f778eb..bbaf0c7d2fa0 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -101,6 +101,19 @@ trait CaptureRef extends TypeProxy, ValueType: * TODO: Document path cases */ final def subsumes(y: CaptureRef)(using Context): Boolean = + + def subsumingRefs(x: Type, y: Type): Boolean = x match + case x: CaptureRef => y match + case y: CaptureRef => x.subsumes(y) + case _ => false + case _ => false + + def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match + case info: SingletonCaptureRef => test(info) + case info: AndType => test(info.tp1) || test(info.tp2) + case info: OrType => test(info.tp1) && test(info.tp2) + case _ => false + (this eq y) || this.isRootCapability || y.match @@ -109,25 +122,21 @@ trait CaptureRef extends TypeProxy, ValueType: case ypre: CaptureRef => this.subsumes(ypre) || this.match - case x @ TermRef(xpre: CaptureRef, _) => - x.symbol == y.symbol && xpre =:= ypre + case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol => + subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre) case _ => false case _ => false - || y.info.match - case y1: SingletonCaptureRef => this.subsumes(y1) - case _ => false + || viaInfo(y.info)(subsumingRefs(this, _)) case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) case _ => false || this.match case ReachCapability(x1) => x1.subsumes(y.stripReach) - case x: TermRef => - x.info match - case x1: SingletonCaptureRef => x1.subsumes(y) - case _ => false + case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) case _ => false + end subsumes def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 05bcecf86067..19acebde8651 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -466,16 +466,24 @@ class CheckCaptures extends Recheck, SymTransformer: if tree.symbol.info.isParameterless then // there won't be an apply; need to include call captures now includeCallCaptures(tree.symbol, tree.srcPos) - else + else if !tree.symbol.isStatic then //debugShowEnvs() def addSelects(ref: TermRef, pt: Type): TermRef = pt match - case pt: PathSelectionProto => addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) + 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. + addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) case _ => ref - markFree(tree.symbol, addSelects(tree.symbol.termRef, pt), tree.srcPos) + val ref = tree.symbol.termRef + val pathRef = addSelects(ref, pt) + //if pathRef ne ref then + // println(i"add selects $ref --> $pathRef") + markFree(tree.symbol, if false then ref else pathRef, tree.srcPos) super.recheckIdent(tree, pt) override def selectionProto(tree: Select, pt: Type)(using Context): Type = - if !tree.symbol.isOneOf(UnstableValueFlags) then PathSelectionProto(tree.symbol, pt) + val sym = tree.symbol + if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic then PathSelectionProto(sym, pt) else super.selectionProto(tree, pt) /** A specialized implementation of the selection rule. @@ -1141,11 +1149,14 @@ class CheckCaptures extends Recheck, SymTransformer: (erefs /: erefs.elems): (erefs, eref) => eref match case eref: ThisType if isPureContext(ctx.owner, eref.cls) => - erefs ++ arefs.filter { - case aref: TermRef => eref.cls.isProperlyContainedIn(aref.symbol.owner) + def isOuterRef(aref: Type): Boolean = aref match + case aref: TermRef => + val owner = aref.symbol.owner + if owner.isClass then isOuterRef(aref.prefix) + else eref.cls.isProperlyContainedIn(owner) case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls) case _ => false - } + erefs ++ arefs.filter(isOuterRef) case _ => erefs diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala index 31c544a46beb..132934dbe3bd 100644 --- a/scala2-library-cc/src/scala/collection/View.scala +++ b/scala2-library-cc/src/scala/collection/View.scala @@ -150,7 +150,10 @@ object View extends IterableFactory[View] { object Filter { def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} = underlying match { - case filter: Filter[A] if filter.isFlipped == isFlipped => new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) + case filter: Filter[A] if filter.isFlipped == isFlipped => + new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) + .asInstanceOf[Filter[A]^{underlying, p}] + // !!! asInstanceOf needed once paths were added, see path-patmat-should-be-pos.scala for minimization case _ => new Filter(underlying, p, isFlipped) } } diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala index 2f7b017a6729..28ce8da104aa 100644 --- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala +++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala @@ -1366,7 +1366,9 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { case SerializeEnd => initRead = true case a => init += a.asInstanceOf[A] } - val tail = in.readObject().asInstanceOf[LazyListIterable[A]] + val tail: LazyListIterable[A] = in.readObject().asInstanceOf[LazyListIterable[A]] + // Explicit type annotation needed so that tail.state below is dropped from capture set. + // Before paths were added, it was tail that was added, and the `asSeenFrom` to a pure type made it work. // scala/scala#10118: caution that no code path can evaluate `tail.state` // before the resulting LazyListIterable is returned val it = init.toList.iterator diff --git a/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala new file mode 100644 index 000000000000..aca6102204a3 --- /dev/null +++ b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala @@ -0,0 +1,26 @@ +class It[A] + +class Filter[A](val underlying: It[A]^, val p: A => Boolean) extends It[A] +object Filter: + def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{underlying, p} = + underlying match + case filter: Filter[A]^ => + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} // error + // !!! should work, it seems to be the case that the system does not recognize that + // underlying and filter are aliases. + + // On the other hand, the following works: + locally: + val filter: underlying.type & Filter[A] = ??? + val a: It[A]^{filter.underlying} = ??? + val b: It[A]^{underlying} = a + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} + + locally: + val filter: underlying.type & Filter[A]^ = ??? + val a: It[A]^{filter.underlying} = ??? + val b: It[A]^{underlying} = a + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} From cfb8314296572d669d573bc9fb5935ae14c4e6e6 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 27 Sep 2024 13:53:34 +0200 Subject: [PATCH 7/8] Drop special handling in recheckApplication In recheckApplication we implemented a rule that computed the capture set of an application `f(a)` by being the "better" of either the capture set of `f` union capture set of `a` or the capture set of the result type of `f(a)`. This relies on capture monotinicity, which we try to get away from. Also, it's semantically dubious if the type of the argument `a` is a type variable that can be instantiated to a capturing type as in the following example: ```scala trait Iterator[+A] ... def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} ``` Here, we account for every capability in `IterableOnce[B]^` already in `f`. But those capabilities could also come from `A` if `A` is instantiated in the actual function argument to a capturing type. There was extensive breakage once the special handling was dropped. One example is the `flatMap` definition above. We leave that as a potential soundness hold for now, but the right way to fix `flatMap` would be by adding a capture set variable: ```scala def flatMap[B, C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^} ``` The problem is that this currently cannot be done in a way that allows flatMap to be called as before, passing a single type argument for `B`. We'd have to change the system to either allow curried type parameters or optional type parameters for capture sets. Another issue is that now more reach capabilities are registered as used by the enclosing method. An example is lazylist-exceptions.scala, which has been moved to pending. Here, the use is spurious because it happens inside an anonymous class creation on the right hand side of the method. With refined use checking, the use would not propagate to the method, so the reach capability should not be leaking. But to get there we need to implement refined use checking first. --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 4 ++-- .../dotty/tools/dotc/cc/CheckCaptures.scala | 9 ++++++--- .../src/scala/collection/Iterator.scala | 6 ++++-- .../src/scala/collection/View.scala | 2 +- .../immutable/LazyListIterable.scala | 4 ++-- .../src/scala/collection/mutable/Buffer.scala | 4 +++- tests/neg-custom-args/captures/i21646.scala | 13 ++++++++++++ .../captures/inner-classes.scala | 2 +- tests/neg-custom-args/captures/lazylist.check | 2 +- .../captures/leaking-iterators.scala | 4 ++-- tests/neg-custom-args/captures/reaches.check | 2 +- .../captures/refine-withFile.scala | 2 +- tests/neg-custom-args/captures/uses.scala | 20 +++++++++++++++++++ tests/neg/i19470.check | 2 +- .../captures/lazylists-exceptions.check | 0 .../captures/lazylists-exceptions.scala | 1 + .../captures/lazylists-exceptions.scala | 4 ++-- .../pos-custom-args/captures/iterators.scala | 4 ++-- .../pos-custom-args/captures/lazylists1.scala | 6 +++--- .../captures/logger-tracked.scala | 12 +++++------ tests/pos-custom-args/captures/logger.scala | 12 +++++------ .../captures/nested-classes-2.scala | 2 +- .../colltest5/CollectionStrawManCC5_1.scala | 14 ++++++++++--- 23 files changed, 90 insertions(+), 41 deletions(-) create mode 100644 tests/neg-custom-args/captures/i21646.scala create mode 100644 tests/neg-custom-args/captures/uses.scala rename tests/{neg-custom-args => pending/neg-customargs}/captures/lazylists-exceptions.check (100%) rename tests/{neg-custom-args => pending/neg-customargs}/captures/lazylists-exceptions.scala (96%) rename tests/{ => pending}/pos-custom-args/captures/lazylists-exceptions.scala (92%) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 79cc7d136e45..db17022efe92 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -640,8 +640,8 @@ object CapsOfApply: class AnnotatedCapability(annot: Context ?=> ClassSymbol): def apply(tp: Type)(using Context) = AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan)) - def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match - case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent) + def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match + case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent) case _ => None /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 19acebde8651..59b78e6428ae 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -581,7 +581,8 @@ class CheckCaptures extends Recheck, SymTransformer: markFree(argType.deepCaptureSet, arg.srcPos) argType - /** A specialized implementation of the apply rule. + /** CURRENTLY DISABLED: + * A specialized implementation of the apply rule. * * E |- q: Tq^Cq * E |- q.f: Ta^Ca ->Cf Tr^Cr @@ -604,6 +605,7 @@ class CheckCaptures extends Recheck, SymTransformer: protected override def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type = val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes)) + return appType val qualCaptures = qualType.captureSet val argCaptures = for (arg, argType) <- tree.args.lazyZip(argTypes) yield @@ -1150,10 +1152,11 @@ class CheckCaptures extends Recheck, SymTransformer: eref match case eref: ThisType if isPureContext(ctx.owner, eref.cls) => def isOuterRef(aref: Type): Boolean = aref match - case aref: TermRef => + case aref: NamedType => val owner = aref.symbol.owner if owner.isClass then isOuterRef(aref.prefix) - else eref.cls.isProperlyContainedIn(owner) + else + eref.cls.isProperlyContainedIn(owner) case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls) case _ => false erefs ++ arefs.filter(isOuterRef) diff --git a/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala index 4d1b0ed4ff95..368f13fb4b76 100644 --- a/scala2-library-cc/src/scala/collection/Iterator.scala +++ b/scala2-library-cc/src/scala/collection/Iterator.scala @@ -588,6 +588,8 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite def next() = f(self.next()) } + // CC TODO This is unsafe. We will need to use a capture set variable: + // def flatMap[B][C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^} def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new AbstractIterator[B] { private[this] var cur: Iterator[B]^{f} = Iterator.empty /** Trillium logic boolean: -1 = unknown, 0 = false, 1 = true */ @@ -595,7 +597,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite private[this] def nextCur(): Unit = { cur = null - cur = f(self.next()).iterator + cur = f(self.next()).iterator.asInstanceOf // CC cast needed once apply special handling is dropped _hasNext = -1 } @@ -1215,7 +1217,7 @@ object Iterator extends IterableFactory[Iterator] { } private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]) { - def headIterator: Iterator[A]^{this} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference" + def headIterator: Iterator[A]^{this.head*} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference" } /** Creates a delegating iterator capped by a limit count. Negative limit means unbounded. diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala index 132934dbe3bd..3545a3e1b72b 100644 --- a/scala2-library-cc/src/scala/collection/View.scala +++ b/scala2-library-cc/src/scala/collection/View.scala @@ -57,7 +57,7 @@ object View extends IterableFactory[View] { * @tparam A View element type */ def fromIteratorProvider[A](it: () => Iterator[A]^): View[A]^{it} = new AbstractView[A] { - def iterator: Iterator[A]^{it} = it() + def iterator: Iterator[A]^{it} = it().asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply } /** diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala index 28ce8da104aa..2291a4d89eb3 100644 --- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala +++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala @@ -1041,7 +1041,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { var itHasNext = false var rest = restRef // var rest = restRef.elem while (!itHasNext && !rest.isEmpty) { - it = f(rest.head).iterator + it = f(rest.head).iterator.asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply itHasNext = it.hasNext if (!itHasNext) { // wait to advance `rest` because `it.next()` can throw rest = rest.tail @@ -1155,7 +1155,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { /** Creates a State from an Iterator, with another State appended after the Iterator * is empty. */ - private def stateFromIteratorConcatSuffix[A](it: Iterator[A]^)(suffix: => State[A]^): State[A]^{it, suffix} = + private def stateFromIteratorConcatSuffix[A, C^](it: Iterator[A]^)(suffix: => State[A]^{C^}): State[A]^{it, suffix, C^} = if (it.hasNext) sCons(it.next(), newLL(stateFromIteratorConcatSuffix(it)(suffix))) else suffix diff --git a/scala2-library-cc/src/scala/collection/mutable/Buffer.scala b/scala2-library-cc/src/scala/collection/mutable/Buffer.scala index 27e5a8997d48..591583ae90d4 100644 --- a/scala2-library-cc/src/scala/collection/mutable/Buffer.scala +++ b/scala2-library-cc/src/scala/collection/mutable/Buffer.scala @@ -184,7 +184,9 @@ trait IndexedBuffer[A] extends IndexedSeq[A] var i = 0 val s = size val newElems = new Array[(IterableOnce[A]^{f})](s) - while (i < s) { newElems(i) = f(this(i)); i += 1 } + while i < s do + newElems(i) = f(this(i)).asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply + i += 1 clear() i = 0 while (i < s) { ++=(newElems(i)); i += 1 } diff --git a/tests/neg-custom-args/captures/i21646.scala b/tests/neg-custom-args/captures/i21646.scala new file mode 100644 index 000000000000..42c493a9ea80 --- /dev/null +++ b/tests/neg-custom-args/captures/i21646.scala @@ -0,0 +1,13 @@ +import language.experimental.captureChecking +import caps.Capability + +trait File extends Capability + +class Resource[T <: Capability](gen: T): + def use[U](f: T => U): U = + f(gen) // error + +@main def run = + val myFile: File = ??? + val r = Resource(myFile) // error + () diff --git a/tests/neg-custom-args/captures/inner-classes.scala b/tests/neg-custom-args/captures/inner-classes.scala index fd500e607970..0f509faa3e31 100644 --- a/tests/neg-custom-args/captures/inner-classes.scala +++ b/tests/neg-custom-args/captures/inner-classes.scala @@ -19,7 +19,7 @@ object test: final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: // error def isEmpty = false def head = x - def tail: LazyList[T]^{this} = xs() + def tail: LazyList[T]^{this} = xs().asInstanceOf end LazyCons new LazyCons(1, () => LazyNil) diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check index f0fbd1a025b5..5853c0bad1c2 100644 --- a/tests/neg-custom-args/captures/lazylist.check +++ b/tests/neg-custom-args/captures/lazylist.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 ------------------------------------- 17 | def tail = xs() // error | ^^^^ - | Found: lazylists.LazyList[T]^{LazyCons.this.xs} + | Found: lazylists.LazyList[T]^{LazyCons.this.xs*} | Required: lazylists.LazyList[T] | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/leaking-iterators.scala b/tests/neg-custom-args/captures/leaking-iterators.scala index ad5958e91e5b..40c551cc075e 100644 --- a/tests/neg-custom-args/captures/leaking-iterators.scala +++ b/tests/neg-custom-args/captures/leaking-iterators.scala @@ -36,8 +36,8 @@ trait Iterator[+A] extends IterableOnce[A]: def ++[B >: A](xs: IterableOnce[B]^): Iterator[B]^{this, xs} end Iterator -private final class ConcatIteratorCell[A](head: => IterableOnce[A]^): - def headIterator: Iterator[A]^{this} = head.iterator +private final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}): + def headIterator: Iterator[A]^{this, C^} = head.iterator def usingLogFile[R](op: FileOutputStream^ => R): R = val logFile = FileOutputStream("log") diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index f00fea09ed8c..62ebeeb529a2 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -32,7 +32,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 -------------------------------------- 62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ | ^^^^^ - | Found: File^{f} + | Found: File^ | Required: File^{id*} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/refine-withFile.scala b/tests/neg-custom-args/captures/refine-withFile.scala index 823b62711d05..6cb1431f79d6 100644 --- a/tests/neg-custom-args/captures/refine-withFile.scala +++ b/tests/neg-custom-args/captures/refine-withFile.scala @@ -5,4 +5,4 @@ val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ??? def main(): Unit = val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error - val leaked = g[File^{f*}]("test")(f => f) // boom + val leaked = g[File^{f*}]("test")(f => f) // error diff --git a/tests/neg-custom-args/captures/uses.scala b/tests/neg-custom-args/captures/uses.scala new file mode 100644 index 000000000000..b872c7b03ec7 --- /dev/null +++ b/tests/neg-custom-args/captures/uses.scala @@ -0,0 +1,20 @@ +class C +def test(x: C^, y: C^) = + class D { + println(x) + def foo() = println(y) + } + val d = D() + val _: D^{y} = d // error, should be ok + val _: D = d // error + + val f = () => println(D()) + val _: () ->{x} Unit = f // ok + val _: () -> Unit = f // should be error + + def g = () => + println(x) + () => println(y) + val _: () ->{x} () ->{y} Unit = g // error, should be ok + val _: () -> () -> Unit = g // error + diff --git a/tests/neg/i19470.check b/tests/neg/i19470.check index fdb336bef7e5..ed9d795b0957 100644 --- a/tests/neg/i19470.check +++ b/tests/neg/i19470.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg/i19470.scala:9:12 ------------------------------------------------------------- 9 | List(foo(f())) // error | ^^^^^^^^ - | Found: Inv[box IO^{f?}] + | Found: Inv[box IO^{f*?}] | Required: box Inv[box IO^?]^? | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/pending/neg-customargs/captures/lazylists-exceptions.check similarity index 100% rename from tests/neg-custom-args/captures/lazylists-exceptions.check rename to tests/pending/neg-customargs/captures/lazylists-exceptions.check diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.scala b/tests/pending/neg-customargs/captures/lazylists-exceptions.scala similarity index 96% rename from tests/neg-custom-args/captures/lazylists-exceptions.scala rename to tests/pending/neg-customargs/captures/lazylists-exceptions.scala index 295147f7f3c5..937d562f3324 100644 --- a/tests/neg-custom-args/captures/lazylists-exceptions.scala +++ b/tests/pending/neg-customargs/captures/lazylists-exceptions.scala @@ -1,3 +1,4 @@ +// Needs better use handling import language.experimental.saferExceptions trait LazyList[+A]: diff --git a/tests/pos-custom-args/captures/lazylists-exceptions.scala b/tests/pending/pos-custom-args/captures/lazylists-exceptions.scala similarity index 92% rename from tests/pos-custom-args/captures/lazylists-exceptions.scala rename to tests/pending/pos-custom-args/captures/lazylists-exceptions.scala index afc6616108bc..7da43a485a85 100644 --- a/tests/pos-custom-args/captures/lazylists-exceptions.scala +++ b/tests/pending/pos-custom-args/captures/lazylists-exceptions.scala @@ -12,9 +12,9 @@ object LzyNil extends LzyList[Nothing]: def head = ??? def tail = ??? -final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: +def LzyCons[A, C^](hd: A, tl: () => LzyList[A]^{C^}): LzyList[A]^{tl, C^} = new LzyList[A]: private var forced = false - private var cache: LzyList[A @uncheckedCaptures]^{this} = uninitialized + private var cache: LzyList[A @uncheckedCaptures]^{this, C^} = uninitialized private def force = if !forced then { cache = tl(); forced = true } cache diff --git a/tests/pos-custom-args/captures/iterators.scala b/tests/pos-custom-args/captures/iterators.scala index 89e1eb91b4f4..8db6702e8a26 100644 --- a/tests/pos-custom-args/captures/iterators.scala +++ b/tests/pos-custom-args/captures/iterators.scala @@ -13,8 +13,8 @@ abstract class Iterator[T]: def next = f(thisIterator.next) end Iterator -private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^): - def headIterator: Iterator[A]^{this} = head.iterator +private[this] final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}): + def headIterator: Iterator[A]^{this, C^} = head.iterator class C type Cap = C^ diff --git a/tests/pos-custom-args/captures/lazylists1.scala b/tests/pos-custom-args/captures/lazylists1.scala index 62b34f442221..2afc6d2a41cc 100644 --- a/tests/pos-custom-args/captures/lazylists1.scala +++ b/tests/pos-custom-args/captures/lazylists1.scala @@ -14,7 +14,7 @@ object LazyNil extends LazyList[Nothing]: def tail = ??? def concat[B](other: LazyList[B]^): LazyList[B]^{other} = other -final class LazyCons[+A](x: A)(xs: () => LazyList[A]^) extends LazyList[A]: +def LazyCons[A, C^](x: A)(xs: () => LazyList[A]^{C^}): LazyList[A]^{xs, C^} = new LazyList[A]: def isEmpty = false def head = x def tail: LazyList[A]^{this} = xs() @@ -30,10 +30,10 @@ def test(cap1: Cap, cap2: Cap) = def f(x: String): String = if cap1 == cap1 then "" else "a" def g(x: String): String = if cap2 == cap2 then "" else "a" - val xs = new LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil) + val xs = LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil) val xsc: LazyList[String]^{cap1} = xs val ys = xs.map(g) val ysc: LazyList[String]^{cap1, cap2} = ys - val zs = new LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil) + val zs = LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil) val as = xs.concat(zs) val asc: LazyList[String]^{xs, zs} = as diff --git a/tests/pos-custom-args/captures/logger-tracked.scala b/tests/pos-custom-args/captures/logger-tracked.scala index 053731de444d..88f79f5b5066 100644 --- a/tests/pos-custom-args/captures/logger-tracked.scala +++ b/tests/pos-custom-args/captures/logger-tracked.scala @@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]: def head = ??? def tail = ??? -final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: - def isEmpty = false - def head = x - def tail: LazyList[T]^{this} = xs() -end LazyCons +def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} = + new LazyList[T]: + def isEmpty = false + def head = x + def tail: LazyList[T]^{this} = xs() extension [A](x: A) - def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} = + def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} = LazyCons(x, () => xs1) extension [A](xs: LazyList[A]^) diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala index 81eeb521fee5..7150655f2daf 100644 --- a/tests/pos-custom-args/captures/logger.scala +++ b/tests/pos-custom-args/captures/logger.scala @@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]: def head = ??? def tail = ??? -final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: - def isEmpty = false - def head = x - def tail: LazyList[T]^{this} = xs() -end LazyCons +def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} = + new LazyList[T]: + def isEmpty = false + def head = x + def tail: LazyList[T]^{this} = xs() extension [A](x: A) - def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} = + def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} = LazyCons(x, () => xs1) extension [A](xs: LazyList[A]^) diff --git a/tests/pos-custom-args/captures/nested-classes-2.scala b/tests/pos-custom-args/captures/nested-classes-2.scala index 744635ee949b..fb44a8d394fa 100644 --- a/tests/pos-custom-args/captures/nested-classes-2.scala +++ b/tests/pos-custom-args/captures/nested-classes-2.scala @@ -11,7 +11,7 @@ def test1(x: (() => Unit)): Unit = def test2(x1: (() => Unit), x2: (() => Unit) => Unit) = class C1(x1: (() => Unit), xx2: (() => Unit) => Unit): - def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^ = C2(y1, y2) + def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^{y1, y2} = C2(y1, y2) class C2(y1: (() => Unit), y2: (() => Unit) => Unit): val a: (() => Unit) => (() => Unit) = f(y1) a(x1) //OK, but should be error diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala index 5443758afa72..99a4452ad23e 100644 --- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala +++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala @@ -433,8 +433,8 @@ object CollectionStrawMan5 { } object View { - def fromIterator[A](it: => Iterator[A]^): View[A]^{it} = new View[A]: - def iterator: Iterator[A]^{this} = it + def fromIterator[A, CI^](it: => Iterator[A]^{CI^}): View[A]^{it, CI^} = new View[A]: + def iterator: Iterator[A]^{this, CI^} = it case object Empty extends View[Nothing] { def iterator: Iterator[Nothing] = Iterator.empty @@ -555,7 +555,15 @@ object CollectionStrawMan5 { private var myCurrent: Iterator[B]^{this, f} = Iterator.empty private def current = { while (!myCurrent.hasNext && self.hasNext) - myCurrent = f(self.next()).iterator + myCurrent = f(self.next()).iterator.asInstanceOf + // TODO: This is actually unsafe, we need to use a capture set variable for `flatMap`, like this: + // def flatMap[B, C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^} + // but if we do this we get: + // Local reach capability C leaks into capture scope of method flatMap + // The problem is we can do this only if we upgrade use reasoning. The C capability + // is not used at the call of flatMap. It's used later in the iterator. + // So the correct type of `flatMap` that expresses this should be: + // def flatMap[B, C^](deferred f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^} myCurrent } def hasNext = current.hasNext From 03b444d5e6ff71772907051c28f0dc0f0d16de79 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 27 Sep 2024 19:04:45 +0200 Subject: [PATCH 8/8] Account for added outer refs in the capture sets of classes --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 46 ++++++++++++++----- .../captures/outerRefsUses.scala | 10 ++++ 2 files changed, 45 insertions(+), 11 deletions(-) create mode 100644 tests/neg-custom-args/captures/outerRefsUses.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 59b78e6428ae..738150691807 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1091,7 +1091,7 @@ class CheckCaptures extends Recheck, SymTransformer: if actualBoxed eq actual then // Only `addOuterRefs` when there is no box adaptation - expected1 = addOuterRefs(expected1, actual) + expected1 = addOuterRefs(expected1, actual, tree.srcPos) if isCompatible(actualBoxed, expected1) then if debugSuccesses then tree match case Ident(_) => @@ -1132,8 +1132,12 @@ class CheckCaptures extends Recheck, SymTransformer: * that are outside `Cls`. These are all accessed through `Cls.this`, * so we can assume they are already accounted for by `Ce` and adding * them explicitly to `Ce` changes nothing. + * - To make up for this, we also add these variables to the capture set of `Cls`, + * so that all instances of `Cls` will capture these outer references. + * So in a sense we use `{Cls.this}` as a placeholder for certain outer captures. + * that we needed to be subsumed by `Cls.this`. */ - private def addOuterRefs(expected: Type, actual: Type)(using Context): Type = + private def addOuterRefs(expected: Type, actual: Type, pos: SrcPos)(using Context): Type = def isPure(info: Type): Boolean = info match case info: PolyType => isPure(info.resType) @@ -1146,20 +1150,40 @@ class CheckCaptures extends Recheck, SymTransformer: else isPure(owner.info) && isPureContext(owner.owner, limit) // Augment expeced capture set `erefs` by all references in actual capture - // set `arefs` that are outside some `this.type` reference in `erefs` + // set `arefs` that are outside some `C.this.type` reference in `erefs` for an enclosing + // class `C`. If an added reference is not a ThisType itself, add it to the capture set + // (i.e. use set) of the `C`. This makes sure that any outer reference implicitly subsumed + // by `C.this` becomes a capture reference of every instance of `C`. def augment(erefs: CaptureSet, arefs: CaptureSet): CaptureSet = (erefs /: erefs.elems): (erefs, eref) => eref match case eref: ThisType if isPureContext(ctx.owner, eref.cls) => - def isOuterRef(aref: Type): Boolean = aref match - case aref: NamedType => - val owner = aref.symbol.owner - if owner.isClass then isOuterRef(aref.prefix) - else - eref.cls.isProperlyContainedIn(owner) + + def pathRoot(aref: Type): Type = aref match + case aref: NamedType if aref.symbol.owner.isClass => pathRoot(aref.prefix) + case _ => aref + + def isOuterRef(aref: Type): Boolean = pathRoot(aref) match + case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner) case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls) case _ => false - erefs ++ arefs.filter(isOuterRef) + + val outerRefs = arefs.filter(isOuterRef) + + // Include implicitly added outer references in the capture set of the class of `eref`. + for outerRef <- outerRefs.elems do + if !erefs.elems.contains(outerRef) + && !pathRoot(outerRef).isInstanceOf[ThisType] + // we don't need to add outer ThisTypes as these are anyway added as path + // prefixes at the use site. And this exemption is required since capture sets + // of non-local classes are always empty, so we can't add an outer this to them. + then + def provenance = + i""" of the enclosing class ${eref.cls}. + |The reference was included since we tried to establish that $arefs <: $erefs""" + checkElem(outerRef, capturedVars(eref.cls), pos, provenance) + + erefs ++ outerRefs case _ => erefs @@ -1344,7 +1368,7 @@ class CheckCaptures extends Recheck, SymTransformer: * @param sym symbol of the field definition that is being checked */ override def checkSubType(actual: Type, expected: Type)(using Context): Boolean = - val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing) + val expected1 = alignDependentFunction(addOuterRefs(expected, actual, srcPos), actual.stripCapturing) val actual1 = val saved = curEnv try diff --git a/tests/neg-custom-args/captures/outerRefsUses.scala b/tests/neg-custom-args/captures/outerRefsUses.scala new file mode 100644 index 000000000000..cd03c8c41efd --- /dev/null +++ b/tests/neg-custom-args/captures/outerRefsUses.scala @@ -0,0 +1,10 @@ +class IO +def test(io: IO^) = + class C: + def foo() = () => + val x: IO^{this} = io + () + val c = new C + val _: C^{io} = c // ok + val _: C = c // error + ()