From af9ecad2c79b1c70386a5e4623ec6db88eee2cae Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 15 Oct 2024 18:24:44 +0200 Subject: [PATCH] Allow only reach capabilities of parameters in deep capture sets --- compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 14 +++++++++----- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 8 +++++++- compiler/src/dotty/tools/dotc/cc/Setup.scala | 3 ++- tests/neg-custom-args/captures/delayedRunops.check | 10 ++++++++++ tests/neg-custom-args/captures/delayedRunops.scala | 12 ++++++++++++ .../neg-custom-args/captures/delayedRunops2.scala | 12 ++++++++++++ tests/neg-custom-args/captures/reaches.check | 4 ++-- tests/neg-custom-args/captures/wf-reach-1.check | 4 ++++ tests/neg-custom-args/captures/wf-reach-1.scala | 2 ++ tests/neg/leak-problem.scala | 7 +++---- .../captures/gears-problem.scala} | 0 11 files changed, 63 insertions(+), 13 deletions(-) create mode 100644 tests/neg-custom-args/captures/wf-reach-1.check create mode 100644 tests/neg-custom-args/captures/wf-reach-1.scala rename tests/{pos/gears-probem.scala => pos-custom-args/captures/gears-problem.scala} (100%) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 37be4c76c8d1..3170a1b1b2d2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -232,14 +232,11 @@ extension (tp: Type) */ def deepCaptureSet(using Context): CaptureSet = val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing) - def reachCanSubsumDcs = - dcs.isUniversal - || dcs.elems.forall(c => c.pathOwner.isContainedIn(tp.pathOwner)) if dcs.isAlwaysEmpty then tp.captureSet else tp match - case tp @ ReachCapability(_) if reachCanSubsumDcs => + case tp @ ReachCapability(_) if tp.isParamPath => tp.singletonCaptureSet - case tp: SingletonCaptureRef if tp.isTrackableRef && reachCanSubsumDcs => + case tp: SingletonCaptureRef if tp.isTrackableRef && tp.isParamPath => tp.reach.singletonCaptureSet case _ => tp.captureSet ++ dcs @@ -297,6 +294,13 @@ extension (tp: Type) case tp1: ThisType => tp1.cls case _ => NoSymbol + final def isParamPath(using Context): Boolean = tp.dealias match + case tp1: NamedType => + tp1.prefix match + case _: ThisType | NoPrefix => tp1.symbol.isOneOf(Param | ParamAccessor) + case prefix => prefix.isParamPath + case _ => false + /** If this is a unboxed capturing type with nonempty capture set, its boxed version. * Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed. * The identity for all other types. diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 835e413463bd..426e7e0b23b2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -1119,12 +1119,18 @@ object CaptureSet: * replaces caps with reach capabilties. */ def ofTypeDeeply(tp: Type)(using Context): CaptureSet = + object ReachesMap extends IdempotentCaptRefMap: + def apply(t: Type): Type = t match + case ReachCapability(ref) if !ref.isParamPath => + defn.Caps_CapSet.typeRef.capturing(ref.deepCaptureSet) + case _ => + t val collect = new TypeAccumulator[CaptureSet]: def apply(cs: CaptureSet, t: Type) = if variance <= 0 then cs else t.dealias match case t @ CapturingType(p, cs1) => - this(cs, p) ++ cs1 + this(cs, p) ++ cs1.map(ReachesMap) case t @ AnnotatedType(parent, ann) => this(cs, parent) case t @ FunctionOrMethod(args, res @ Existential(_, _)) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 76ae41649517..ddd9e240be5d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -751,7 +751,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: report.warning(em"redundant capture: $dom already accounts for $ref", pos) if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then - report.error(em"$ref cannot be tracked since its capture set is empty", pos) + val deepStr = if ref.isReach then " deep" else "" + report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos) check(parent.captureSet, parent) val others = diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check index 625f17663a4a..179d4e62a0e4 100644 --- a/tests/neg-custom-args/captures/delayedRunops.check +++ b/tests/neg-custom-args/captures/delayedRunops.check @@ -3,3 +3,13 @@ | ^^^^ | reference ops* is not included in the allowed capture set {} | of an enclosing function literal with expected type () -> Unit +-- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:13 ----------------------------------------------------- +21 | runOps(ops1) // error + | ^^^^ + | reference (caps.cap : caps.Capability) is not included in the allowed capture set {} + | of an enclosing function literal with expected type () -> Unit +-- Error: tests/neg-custom-args/captures/delayedRunops.scala:27:13 ----------------------------------------------------- +27 | runOps(ops1) // error + | ^^^^ + | reference ops* is not included in the allowed capture set {} + | of an enclosing function literal with expected type () -> Unit diff --git a/tests/neg-custom-args/captures/delayedRunops.scala b/tests/neg-custom-args/captures/delayedRunops.scala index 1d1475806c52..8fcaf87b3b53 100644 --- a/tests/neg-custom-args/captures/delayedRunops.scala +++ b/tests/neg-custom-args/captures/delayedRunops.scala @@ -13,3 +13,15 @@ import language.experimental.captureChecking () => val ops1 = ops runOps(ops1) // error + + // unsound: impure operation pretended pure + def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit = + () => + val ops1: List[() => Unit] = ops + runOps(ops1) // error + + // unsound: impure operation pretended pure + def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit = + () => + val ops1: List[() ->{ops*} Unit] = ops + runOps(ops1) // error diff --git a/tests/neg-custom-args/captures/delayedRunops2.scala b/tests/neg-custom-args/captures/delayedRunops2.scala index 0c9aec20aaa3..ada95065764f 100644 --- a/tests/neg-custom-args/captures/delayedRunops2.scala +++ b/tests/neg-custom-args/captures/delayedRunops2.scala @@ -8,3 +8,15 @@ def app[T, U](x: T, op: T => U): () ->{op} U = def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit = app[List[() ->{ops*} Unit], Unit](ops, runOps) // error + +def app2[T, U](x: T, op: T => U): () ->{op} U = + () => + def y: T = x + op(y) + +def unsafeRunOps2(ops: List[() => Unit]): () -> Unit = + app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error + + + + diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index d5facb0f8529..d9a6e58b9938 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -47,8 +47,8 @@ -- Error: tests/neg-custom-args/captures/reaches.scala:60:31 ----------------------------------------------------------- 60 | val leaked = usingFile[File^{id*}]: f => // error | ^^^ - | id* cannot be tracked since its capture set is empty + | id* cannot be tracked since its deep capture set is empty -- Error: tests/neg-custom-args/captures/reaches.scala:61:18 ----------------------------------------------------------- 61 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error | ^^^ - | id* cannot be tracked since its capture set is empty + | id* cannot be tracked since its deep capture set is empty diff --git a/tests/neg-custom-args/captures/wf-reach-1.check b/tests/neg-custom-args/captures/wf-reach-1.check new file mode 100644 index 000000000000..6a3ac9771a11 --- /dev/null +++ b/tests/neg-custom-args/captures/wf-reach-1.check @@ -0,0 +1,4 @@ +-- Error: tests/neg-custom-args/captures/wf-reach-1.scala:2:17 --------------------------------------------------------- +2 | val y: Object^{x*} = ??? // error + | ^^ + | x* cannot be tracked since its deep capture set is empty diff --git a/tests/neg-custom-args/captures/wf-reach-1.scala b/tests/neg-custom-args/captures/wf-reach-1.scala new file mode 100644 index 000000000000..c8901c7ae4a8 --- /dev/null +++ b/tests/neg-custom-args/captures/wf-reach-1.scala @@ -0,0 +1,2 @@ +def test(x: List[() -> Unit]) = + val y: Object^{x*} = ??? // error diff --git a/tests/neg/leak-problem.scala b/tests/neg/leak-problem.scala index c271e5d02560..d597ee6caa8f 100644 --- a/tests/neg/leak-problem.scala +++ b/tests/neg/leak-problem.scala @@ -15,8 +15,7 @@ def useBoxedAsync(x: Box[Async^]): Unit = def useBoxedAsync1(x: Box[Async^]): Unit = x.get.read() // now ok -def test(): Unit = - val xs: Box[Async^] = ??? +def test(xs: Box[Async^]): Unit = val xsLambda = () => useBoxedAsync(xs) val _: () ->{xs*} Unit = xsLambda val _: () -> Unit = xsLambda // error @@ -27,8 +26,8 @@ def test(): Unit = t1.read() val xsLambda2 = () => useBoxedAsync2(xs) - val _: () ->{xs*} Unit = xsLambda - val _: () -> Unit = xsLambda // error + val _: () ->{xs*} Unit = xsLambda2 + val _: () -> Unit = xsLambda2 // error val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x) diff --git a/tests/pos/gears-probem.scala b/tests/pos-custom-args/captures/gears-problem.scala similarity index 100% rename from tests/pos/gears-probem.scala rename to tests/pos-custom-args/captures/gears-problem.scala