From af36d6e62a6a615ccb26310a9f4df1de66cc7d0f Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 20 Jul 2025 21:29:06 +0200 Subject: [PATCH 1/2] Drop isOfNestedMethod exception in normal mode It's hard to generalie this to late use checking. And it does not add anything fundamental. --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 8 +++++--- tests/neg-custom-args/captures/method-uses.scala | 6 +++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ab40a3faaa36..04683afa44c4 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -427,11 +427,13 @@ class CheckCaptures extends Recheck, SymTransformer: else i"\nof the enclosing ${owner.showLocated}" - /** Does the given environment belong to a method that is (a) nested in a term + /** Under deferredReaches: + * Does the given environment belong to a method that is (a) nested in a term * and (b) not the method of an anonymous function? */ def isOfNestedMethod(env: Env | Null)(using Context) = - env != null + ccConfig.deferredReaches + && env != null && env.owner.is(Method) && env.owner.owner.isTerm && !env.owner.isAnonymousFunction @@ -540,7 +542,7 @@ class CheckCaptures extends Recheck, SymTransformer: isVisible checkSubset(included, env.captured, tree.srcPos, provenance(env)) capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") - if !isOfNestedMethod(env) then + if !isOfNestedMethod(env) || true then recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner), env) // Don't propagate out of methods inside terms. The use set of these methods // will be charged when that method is called. diff --git a/tests/neg-custom-args/captures/method-uses.scala b/tests/neg-custom-args/captures/method-uses.scala index 69acef6a99a8..da8f226685c0 100644 --- a/tests/neg-custom-args/captures/method-uses.scala +++ b/tests/neg-custom-args/captures/method-uses.scala @@ -2,9 +2,9 @@ def test(xs: List[() => Unit]) = xs.head // error def foo = - xs.head // ok + xs.head // error, ok under deferredReaches def bar() = - xs.head // ok + xs.head // error, ok under deferredReaches class Foo: println(xs.head) // error, but could be OK @@ -14,7 +14,7 @@ def test(xs: List[() => Unit]) = Foo() // OK, but could be error def test2(xs: List[() => Unit]) = - def foo = xs.head // ok + def foo = xs.head // error, ok under deferredReaches () def test3(xs: List[() => Unit]): () ->{xs*} Unit = () => From 2c44028381afdbab9c0dde252ec0b4246dab909b Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 21 Jul 2025 12:06:11 +0200 Subject: [PATCH 2/2] Rely on hidden sets for use checking Two changes: 1. We don't distinguish anymore according to separation checking in markFree. We use the same logic regardless of this option. This improves expressiveness because we now admit local reach capabilities that do not refer to parameters. Previously, these were only admitted under separation checking, which is a severe loss of expressiveness. 2. We do trace hidden sets to check that a local reach capability does not refer indirectly through a fresh to a parameter reach. This has to be done after regular capture checking, since hidden sets need to be completely known. This fixes a soundness hole that would have opened once we add `cap.only[Sharable]` capabilities which escape separation checking. Fixes #23579 --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 141 ++++++++++++------ tests/neg-custom-args/captures/dcs-tvar.check | 20 ++- .../captures/delayedRunops.check | 29 +++- .../captures/delayedRunops.scala | 10 +- tests/neg-custom-args/captures/i21442.check | 5 + tests/neg-custom-args/captures/i21442.scala | 2 +- .../captures/localReaches.check | 20 +++ .../captures/localReaches.scala | 28 ++++ tests/neg-custom-args/captures/reaches.check | 18 ++- tests/neg-custom-args/captures/reaches.scala | 2 +- tests/neg-custom-args/captures/reaches2.check | 31 +--- tests/neg-custom-args/captures/reaches2.scala | 2 +- .../captures/unsound-reach-6.check | 20 +-- .../neg-custom-args/captures/use-capset.check | 10 +- .../captures/widen-reach.check | 21 ++- tests/neg/localReaches.check | 10 ++ tests/neg/localReaches.scala | 28 ++++ .../captures/use-alternatives.scala | 25 ++++ 18 files changed, 299 insertions(+), 123 deletions(-) create mode 100644 tests/neg-custom-args/captures/localReaches.check create mode 100644 tests/neg-custom-args/captures/localReaches.scala create mode 100644 tests/neg/localReaches.check create mode 100644 tests/neg/localReaches.scala create mode 100644 tests/pos-custom-args/captures/use-alternatives.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 04683afa44c4..7c2d39f5819d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -26,6 +26,7 @@ import reporting.{trace, Message, OverrideError} import Annotations.Annotation import Capabilities.* import dotty.tools.dotc.cc.CaptureSet.MutAdaptFailure +import dotty.tools.dotc.util.common.alwaysTrue /** The capture checker */ object CheckCaptures: @@ -253,8 +254,12 @@ class CheckCaptures extends Recheck, SymTransformer: */ private val sepCheckFormals = util.EqHashMap[Tree, Type]() - /** The references used at identifier or application trees */ - private val usedSet = util.EqHashMap[Tree, CaptureSet]() + /** The references used at identifier or application trees, including the + * environment at the reference point. + */ + private val useInfos = mutable.ArrayBuffer[(Tree, CaptureSet, Env)]() + + private var usedSet = util.EqHashMap[Tree, CaptureSet]() /** The set of symbols that were rechecked via a completer */ private val completed = new mutable.HashSet[Symbol] @@ -273,7 +278,7 @@ class CheckCaptures extends Recheck, SymTransformer: extension [T <: Tree](tree: T) def needsSepCheck: Boolean = sepCheckFormals.contains(tree) def formalType: Type = sepCheckFormals.getOrElse(tree, NoType) - def markedFree = usedSet.getOrElse(tree, CaptureSet.empty) + def markedFree: CaptureSet = usedSet.getOrElse(tree, CaptureSet.empty) /** Instantiate capture set variables appearing contra-variantly to their * upper approximation. @@ -462,20 +467,6 @@ class CheckCaptures extends Recheck, SymTransformer: !sym.isContainedIn(env.owner) } - /** If capability `c` refers to a parameter that is not @use declared, report an error. - * Exception under deferredReaches: If use comes from a nested closure, accept it. - */ - def checkUseDeclared(c: Capability, env: Env, lastEnv: Env | Null) = - if lastEnv != null && env.nestedClosure.exists && env.nestedClosure == lastEnv.owner then - assert(ccConfig.deferredReaches) // access is from a nested closure under deferredReaches, so it's OK - else c.paramPathRoot match - case ref: NamedType if !ref.symbol.isUseParam => - val what = if ref.isType then "Capture set parameter" else "Local reach capability" - report.error( - em"""$what $c leaks into capture scope of ${env.ownerString}. - |To allow this, the ${ref.symbol} should be declared with a @use annotation""", tree.srcPos) - case _ => - /** Avoid locally defined capability by charging the underlying type * (which may not be cap). This scheme applies only under the deferredReaches setting. */ @@ -483,7 +474,10 @@ class CheckCaptures extends Recheck, SymTransformer: if c.isParamPath then c match case Reach(_) | _: TypeRef => - checkUseDeclared(c, env, lastEnv) + val accessFromNestedClosure = + lastEnv != null && env.nestedClosure.exists && env.nestedClosure == lastEnv.owner + if !accessFromNestedClosure then + checkUseDeclared(c, tree.srcPos) case _ => else val underlying = c match @@ -501,32 +495,22 @@ class CheckCaptures extends Recheck, SymTransformer: * parameter. This is the default. */ def avoidLocalReachCapability(c: Capability, env: Env): Unit = c match - case Reach(c1) => - if c1.isParamPath then - checkUseDeclared(c, env, null) - else - // When a reach capabilty x* where `x` is not a parameter goes out - // of scope, we need to continue with `x`'s underlying deep capture set. - // It is an error if that set contains cap. - // The same is not an issue for normal capabilities since in a local - // definition `val x = e`, the capabilities of `e` have already been charged. - // Note: It's not true that the underlying capture set of a reach capability - // is always cap. Reach capabilities over paths depend on the prefix, which - // might turn a cap into something else. - // The path-use.scala neg test contains an example. - val underlying = CaptureSet.ofTypeDeeply(c1.widen) - capt.println(i"Widen reach $c to $underlying in ${env.owner}") - if sepChecksEnabled then - recur(underlying.filter(!_.isTerminalCapability), env, null) - // we don't want to disallow underlying Fresh instances, since these are typically locally created - // fresh capabilities. We don't need to also follow the hidden set since separation - // checking makes ure that locally hidden references need to go to @consume parameters. - else - underlying.disallowRootCapability(ctx.owner): () => - report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos) - recur(underlying, env, null) - case c: TypeRef if c.isParamPath => - checkUseDeclared(c, env, null) + case Reach(c1) if !c1.isParamPath => + // Parameter reaches are rejected in checkEscapingUses. + // When a reach capabilty x* where `x` is not a parameter goes out + // of scope, we need to continue with `x`'s underlying deep capture set. + // It is an error if that set contains cap. + // The same is not an issue for normal capabilities since in a local + // definition `val x = e`, the capabilities of `e` have already been charged. + // Note: It's not true that the underlying capture set of a reach capability + // is always cap. Reach capabilities over paths depend on the prefix, which + // might turn a cap into something else. + // The path-use.scala neg test contains an example. + val underlying = CaptureSet.ofTypeDeeply(c1.widen) + capt.println(i"Widen reach $c to $underlying in ${env.owner}") + recur(underlying.filter(!_.isTerminalCapability), env, null) + // we don't want to disallow underlying Fresh instances, since these are typically locally created + // fresh capabilities. We do check that they hide no parameter reach caps in checkEscapingUses case _ => def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit = @@ -542,15 +526,28 @@ class CheckCaptures extends Recheck, SymTransformer: isVisible checkSubset(included, env.captured, tree.srcPos, provenance(env)) capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") - if !isOfNestedMethod(env) || true then + if !isOfNestedMethod(env) then recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner), env) - // Don't propagate out of methods inside terms. The use set of these methods - // will be charged when that method is called. + // Under deferredReaches, don't propagate out of methods inside terms. + // The use set of these methods will be charged when that method is called. recur(cs, curEnv, null) - usedSet(tree) = tree.markedFree ++ cs + useInfos += ((tree, cs, curEnv)) end markFree + /** If capability `c` refers to a parameter that is not @use declared, report an error. + */ + def checkUseDeclared(c: Capability, pos: SrcPos)(using Context): Unit = + c.paramPathRoot match + case ref: NamedType if !ref.symbol.isUseParam => + val what = if ref.isType then "Capture set parameter" else "Local reach capability" + val owner = ref.symbol.owner + val ownerStr = if owner.isAnonymousFunction then "enclosing function" else owner.show + report.error( + em"""$what $c leaks into capture scope of $ownerStr. + |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos) + case _ => + /** Include references captured by the called method in the current environment stack */ def includeCallCaptures(sym: Symbol, resType: Type, tree: Tree)(using Context): Unit = resType match case _: MethodOrPoly => // wait until method is fully applied @@ -1992,6 +1989,48 @@ class CheckCaptures extends Recheck, SymTransformer: traverseChildren(t) check.traverse(tp) + /** Check that no uses refer to reach capabilities of parameters of enclosing + * methods or classes. + */ + def checkEscapingUses()(using Context) = + for (tree, uses, env) <- useInfos do + val seen = util.EqHashSet[Capability]() + + // The owner of the innermost environment of kind Boxed + def boxedOwner(env: Env): Symbol = + if env.kind == EnvKind.Boxed then env.owner + else if isOfNestedMethod(env) then env.owner.owner + else if env.owner.isStaticOwner then NoSymbol + else boxedOwner(nextEnvToCharge(env, alwaysTrue)) + + def checkUseUnlessBoxed(c: Capability, croot: NamedType) = + if !boxedOwner(env).isContainedIn(croot.symbol.owner) then + checkUseDeclared(c, tree.srcPos) + + def check(cs: CaptureSet): Unit = cs.elems.foreach(checkElem) + + def checkElem(c: Capability): Unit = + if !seen.contains(c) then + seen += c + c match + case Reach(c1) => + c1.paramPathRoot match + case croot: NamedType => checkUseUnlessBoxed(c, croot) + case _ => check(CaptureSet.ofTypeDeeply(c1.widen)) + case c: TypeRef => + c.paramPathRoot match + case croot: NamedType => checkUseUnlessBoxed(c, croot) + case _ => + case c: DerivedCapability => + checkElem(c.underlying) + case c: FreshCap => + check(c.hiddenSet) + case _ => + + check(uses) + end for + end checkEscapingUses + /** Check that arguments of TypeApplys and AppliedTypes conform to their bounds. */ def postCheck(unit: tpd.Tree)(using Context): Unit = @@ -2020,7 +2059,11 @@ class CheckCaptures extends Recheck, SymTransformer: end checker checker.traverse(unit)(using ctx.withOwner(defn.RootClass)) - if sepChecksEnabled then SepCheck(this).traverse(unit) + checkEscapingUses() + if sepChecksEnabled then + for (tree, cs, env) <- useInfos do + usedSet(tree) = tree.markedFree ++ cs + SepCheck(this).traverse(unit) if !ctx.reporter.errorsReported then // We dont report errors here if previous errors were reported, because other // errors often result in bad applied types, but flagging these bad types gives diff --git a/tests/neg-custom-args/captures/dcs-tvar.check b/tests/neg-custom-args/captures/dcs-tvar.check index 76b4036a8821..65fc12f82ba0 100644 --- a/tests/neg-custom-args/captures/dcs-tvar.check +++ b/tests/neg-custom-args/captures/dcs-tvar.check @@ -1,10 +1,14 @@ --- Error: tests/neg-custom-args/captures/dcs-tvar.scala:6:15 ----------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:6:2 --------------------------------------- 6 | () => runOps(xs) // error - | ^^ - | Local reach capability xs* leaks into capture scope of method f. - | To allow this, the parameter xs should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:15 ----------------------------------------------------------- + | ^^^^^^^^^^^^^^^^ + | Found: () ->{xs*} Unit + | Required: () -> Unit + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:2 --------------------------------------- 9 | () => runOps(xs) // error - | ^^ - | Local reach capability xs* leaks into capture scope of method g. - | To allow this, the parameter xs should be declared with a @use annotation + | ^^^^^^^^^^^^^^^^ + | Found: () ->{xs*} Unit + | Required: () -> Unit + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check index c4e5f7ab7a8a..5554a32bc10e 100644 --- a/tests/neg-custom-args/captures/delayedRunops.check +++ b/tests/neg-custom-args/captures/delayedRunops.check @@ -1,12 +1,25 @@ --- Error: tests/neg-custom-args/captures/delayedRunops.scala:17:13 ----------------------------------------------------- -17 | runOps(ops1) // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:15:4 --------------------------------- +15 | () => // error + | ^ + | Found: () ->{ops*} Unit + | Required: () -> Unit +16 | val ops1 = ops +17 | runOps(ops1) + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:27:4 --------------------------------- +27 | () => // error + | ^ + | Found: () ->{ops*} Unit + | Required: () -> Unit +28 | val ops1: List[() ->{ops*} Unit] = ops +29 | runOps(ops1) + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/delayedRunops.scala:23:13 ----------------------------------------------------- +23 | runOps(ops1) // error | ^^^^ - | Local reach capability ops* leaks into capture scope of method delayedRunOps1. - | To allow this, the parameter ops should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/delayedRunops.scala:29:13 ----------------------------------------------------- -29 | runOps(ops1) // error - | ^^^^ - | Local reach capability ops* leaks into capture scope of method delayedRunOps3. + | Local reach capability ops* leaks into capture scope of method delayedRunOps2. | To allow this, the parameter ops should be declared with a @use annotation -- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:16 ----------------------------------------------------- 22 | val ops1: List[() => Unit] = ops // error diff --git a/tests/neg-custom-args/captures/delayedRunops.scala b/tests/neg-custom-args/captures/delayedRunops.scala index 946d4324ddeb..a4cb0129d912 100644 --- a/tests/neg-custom-args/captures/delayedRunops.scala +++ b/tests/neg-custom-args/captures/delayedRunops.scala @@ -12,18 +12,18 @@ import caps.{use, consume} // unsound: impure operation pretended pure def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit = - () => + () => // error val ops1 = ops - runOps(ops1) // error + runOps(ops1) // unsound: impure operation pretended pure def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit = () => val ops1: List[() => Unit] = ops // error - runOps(ops1) // was error + runOps(ops1) // error // unsound: impure operation pretended pure def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit = - () => + () => // error val ops1: List[() ->{ops*} Unit] = ops - runOps(ops1) // error + runOps(ops1) diff --git a/tests/neg-custom-args/captures/i21442.check b/tests/neg-custom-args/captures/i21442.check index 6bf6cf2191ab..330c88d393dd 100644 --- a/tests/neg-custom-args/captures/i21442.check +++ b/tests/neg-custom-args/captures/i21442.check @@ -3,6 +3,11 @@ | ^^^^^^^ | Local reach capability x.unbox* leaks into capture scope of method foo. | To allow this, the parameter x should be declared with a @use annotation +-- Error: tests/neg-custom-args/captures/i21442.scala:18:14 ------------------------------------------------------------ +18 | val io = x1.unbox // error + | ^^^^^^^^ + | Local reach capability x* leaks into capture scope of method bar. + | To allow this, the parameter x should be declared with a @use annotation -- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------ 17 | val x1: Boxed[IO^] = x // error | ^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/i21442.scala b/tests/neg-custom-args/captures/i21442.scala index 16d32c5218cb..3541bd89789a 100644 --- a/tests/neg-custom-args/captures/i21442.scala +++ b/tests/neg-custom-args/captures/i21442.scala @@ -15,5 +15,5 @@ def foo(x: Boxed[IO^]): Unit = // But, no type error reported. def bar(x: Boxed[IO^]): Unit = val x1: Boxed[IO^] = x // error - val io = x1.unbox // was error + val io = x1.unbox // error io.use() diff --git a/tests/neg-custom-args/captures/localReaches.check b/tests/neg-custom-args/captures/localReaches.check new file mode 100644 index 000000000000..886fbbf7c3e9 --- /dev/null +++ b/tests/neg-custom-args/captures/localReaches.check @@ -0,0 +1,20 @@ +-- Error: tests/neg-custom-args/captures/localReaches.scala:24:30 ------------------------------------------------------ +24 | var x: () ->{xs*} Unit = ys.head // error + | ^^^^^^^ + | Local reach capability ops* leaks into capture scope of method localReach3. + | To allow this, the parameter ops should be declared with a @use annotation +-- Error: tests/neg-custom-args/captures/localReaches.scala:27:11 ------------------------------------------------------ +27 | x = ys.head // error + | ^^^^^^^ + | Local reach capability ops* leaks into capture scope of method localReach3. + | To allow this, the parameter ops should be declared with a @use annotation +-- Error: tests/neg-custom-args/captures/localReaches.scala:14:10 ------------------------------------------------------ +14 | val xs: List[() => Unit] = op :: Nil // error + | ^^^^^^^^^^^^^^^^ + | Separation failure: value xs's type List[() => Unit] hides parameter op. + | The parameter needs to be annotated with @consume to allow this. +-- Error: tests/neg-custom-args/captures/localReaches.scala:22:10 ------------------------------------------------------ +22 | val xs: List[() => Unit] = ops // error + | ^^^^^^^^^^^^^^^^ + | Separation failure: value xs's type List[() => Unit] hides parameter ops. + | The parameter needs to be annotated with @consume to allow this. diff --git a/tests/neg-custom-args/captures/localReaches.scala b/tests/neg-custom-args/captures/localReaches.scala new file mode 100644 index 000000000000..9795a6dd099c --- /dev/null +++ b/tests/neg-custom-args/captures/localReaches.scala @@ -0,0 +1,28 @@ +import language.experimental.captureChecking +// no separation checking +import caps.consume + +def localReach() = + val xs: List[() => Unit] = ??? + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head + while ys.nonEmpty do + ys = ys.tail + x = ys.head + +def localReach2(op: () => Unit) = + val xs: List[() => Unit] = op :: Nil // error + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head + while ys.nonEmpty do + ys = ys.tail + x = ys.head + +def localReach3(ops: List[() => Unit]) = + val xs: List[() => Unit] = ops // error + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head // error + while ys.nonEmpty do + ys = ys.tail + x = ys.head // error + diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index 0d683cbaf1ca..11681df3ac6a 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -90,11 +90,16 @@ 72 | f1 | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:88:10 ----------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 -------------------------------------- 88 | ps.map((x, y) => compose1(x, y)) // error - | ^ - | Local reach capability ps* leaks into capture scope of method mapCompose. - | To allow this, the parameter ps should be declared with a @use annotation + | ^^^^^^^^^^^^^^^^^^^^^^^ + |Found: (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^? + |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^? ->? A^? + | + |where: => refers to a fresh root capability created in method mapCompose when checking argument to parameter f of method map + | ^ refers to the universal root capability + | + | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:91:10 -------------------------------------- 91 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ @@ -105,3 +110,8 @@ | ^ refers to the universal root capability | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/reaches.scala:39:31 ----------------------------------------------------------- +39 | val next: () => Unit = cur.head // error + | ^^^^^^^^ + | Local reach capability xs* leaks into capture scope of method runAll2. + | To allow this, the parameter xs should be declared with a @use annotation diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index b98ca4814e95..b811b1405590 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -36,7 +36,7 @@ def runAll1(@use xs: List[Proc]): Unit = def runAll2(@consume xs: List[Proc]): Unit = var cur: List[Proc] = xs while cur.nonEmpty do - val next: () => Unit = cur.head // was error, now OK + val next: () => Unit = cur.head // error next() cur = cur.tail diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check index 8391836d611e..3ad78fd49eed 100644 --- a/tests/neg-custom-args/captures/reaches2.check +++ b/tests/neg-custom-args/captures/reaches2.check @@ -1,26 +1,7 @@ --- Error: tests/neg-custom-args/captures/reaches2.scala:10:10 ---------------------------------------------------------- -10 | ps.map((x, y) => compose1(x, y)) // error // error // error - | ^ - | Local reach capability ps* leaks into capture scope of method mapCompose. - | To allow this, the parameter ps should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/reaches2.scala:10:13 ---------------------------------------------------------- -10 | ps.map((x, y) => compose1(x, y)) // error // error // error - | ^ - | Local reach capability ps* leaks into capture scope of method mapCompose. - | To allow this, the parameter ps should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/reaches2.scala:10:28 ---------------------------------------------------------- -10 | ps.map((x, y) => compose1(x, y)) // error // error // error - | ^ - |Separation failure: argument of type A ->{x} A - |to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C - |corresponds to capture-polymorphic formal parameter f of type A^? => A^? - |and hides capabilities {x}. - |Some of these overlap with the captures of the second argument with type A ->{y} A. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:10:10 ------------------------------------- +10 | ps.map((x, y) => compose1(x, y)) // error + | ^^^^^^^^^^^^^^^^^^^^^^^ + | Found: (x$1: (A^? ->{ps*} A^?, A^? ->{ps*} A^?)^?) ->{ps*} A^? ->{ps*} A^? + | Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^? ->? A^? | - | Hidden set of current argument : {x} - | Hidden footprint of current argument : {x, ps*} - | Capture set of second argument : {y} - | Footprint set of second argument : {y, ps*} - | The two sets overlap at : {ps*} - | - |where: => refers to a fresh root capability created in anonymous function of type (x$1: (A^? ->{ps*} A^?, A^? ->{ps*} A^?)^?): A^? ->{ps*} A^? when checking argument to parameter f of method compose1 + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/reaches2.scala b/tests/neg-custom-args/captures/reaches2.scala index 69ee3472cf86..1ba3dff04ba1 100644 --- a/tests/neg-custom-args/captures/reaches2.scala +++ b/tests/neg-custom-args/captures/reaches2.scala @@ -7,5 +7,5 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C = z => g(f(z)) def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] = - ps.map((x, y) => compose1(x, y)) // error // error // error + ps.map((x, y) => compose1(x, y)) // error diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check index a6a6c69f93bc..8308e2336d7c 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.check +++ b/tests/neg-custom-args/captures/unsound-reach-6.check @@ -1,13 +1,3 @@ --- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:7:13 ---------------------------------------------------- -7 | println(xs.head) // error - | ^^^^^^^ - | Local reach capability xs* leaks into capture scope of method f. - | To allow this, the parameter xs should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 --------------------------------------------------- -11 | val z = f(ys) // error @consume failure - | ^^ - | Local reach capability ys* leaks into capture scope of method test. - | To allow this, the parameter ys should be declared with a @use annotation -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-6.scala:13:22 ------------------------------ 13 | val _: () -> Unit = x // error | ^ @@ -22,6 +12,16 @@ | Required: () -> Unit | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:7:13 ---------------------------------------------------- +7 | println(xs.head) // error + | ^^^^^^^ + | Local reach capability xs* leaks into capture scope of method f. + | To allow this, the parameter xs should be declared with a @use annotation +-- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 --------------------------------------------------- +11 | val z = f(ys) // error @consume failure + | ^^ + | Local reach capability ys* leaks into capture scope of method test. + | To allow this, the parameter ys should be declared with a @use annotation -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 --------------------------------------------------- 19 | val z = f(ys) // error @consume failure | ^^ diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check index 082ad2860425..fc65636b1302 100644 --- a/tests/neg-custom-args/captures/use-capset.check +++ b/tests/neg-custom-args/captures/use-capset.check @@ -1,8 +1,3 @@ --- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 --------------------------------------------------------- -5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error - | ^^^^^^^ - | Capture set parameter C leaks into capture scope of method g. - | To allow this, the type C should be declared with a @use annotation -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 ----------------------------------- 11 | val _: () -> Unit = h // error: should be ->{io} | ^ @@ -17,3 +12,8 @@ | Required: () -> List[Object^{io}] -> Object^{io} | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 --------------------------------------------------------- +5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error + | ^^^^^^^ + | Capture set parameter C leaks into capture scope of method g. + | To allow this, the type C should be declared with a @use annotation diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check index 5e83c94880dc..9d0ecceb1808 100644 --- a/tests/neg-custom-args/captures/widen-reach.check +++ b/tests/neg-custom-args/captures/widen-reach.check @@ -15,13 +15,22 @@ | ^² refers to a fresh root capability in the type of value foo | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ---------------------------------- 13 | val y2: IO^ -> IO^ = y1.foo // error | ^^^^^^ - | Local reach capability x* leaks into capture scope of method test. - | To allow this, the parameter x should be declared with a @use annotation --- Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ------------------------------------------------------- + | Found: IO^ ->{x*} IO^{x*} + | Required: IO^ -> IO^² + | + | where: ^ refers to the universal root capability + | ^² refers to a fresh root capability in the type of value y2 + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ---------------------------------- 14 | val y3: IO^ -> IO^{x*} = y1.foo // error | ^^^^^^ - | Local reach capability x* leaks into capture scope of method test. - | To allow this, the parameter x should be declared with a @use annotation + | Found: IO^ ->{x*} IO^{x*} + | Required: IO^ -> IO^{x*} + | + | where: ^ refers to the universal root capability + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/localReaches.check b/tests/neg/localReaches.check new file mode 100644 index 000000000000..18510e3a3616 --- /dev/null +++ b/tests/neg/localReaches.check @@ -0,0 +1,10 @@ +-- Error: tests/neg/localReaches.scala:24:30 --------------------------------------------------------------------------- +24 | var x: () ->{xs*} Unit = ys.head // error + | ^^^^^^^ + | Local reach capability ops* leaks into capture scope of method localReach3. + | To allow this, the parameter ops should be declared with a @use annotation +-- Error: tests/neg/localReaches.scala:27:11 --------------------------------------------------------------------------- +27 | x = ys.head // error + | ^^^^^^^ + | Local reach capability ops* leaks into capture scope of method localReach3. + | To allow this, the parameter ops should be declared with a @use annotation diff --git a/tests/neg/localReaches.scala b/tests/neg/localReaches.scala new file mode 100644 index 000000000000..d0935e2d491f --- /dev/null +++ b/tests/neg/localReaches.scala @@ -0,0 +1,28 @@ +import language.experimental.captureChecking +// no separation checking +import caps.consume + +def localReach() = + val xs: List[() => Unit] = ??? + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head + while ys.nonEmpty do + ys = ys.tail + x = ys.head + +def localReach2(op: () => Unit) = + val xs: List[() => Unit] = op :: Nil + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head + while ys.nonEmpty do + ys = ys.tail + x = ys.head + +def localReach3(ops: List[() => Unit]) = + val xs: List[() => Unit] = ops + var ys: List[() ->{xs*} Unit] = xs + var x: () ->{xs*} Unit = ys.head // error + while ys.nonEmpty do + ys = ys.tail + x = ys.head // error + diff --git a/tests/pos-custom-args/captures/use-alternatives.scala b/tests/pos-custom-args/captures/use-alternatives.scala new file mode 100644 index 000000000000..b4fd896210d4 --- /dev/null +++ b/tests/pos-custom-args/captures/use-alternatives.scala @@ -0,0 +1,25 @@ +import language.experimental.captureChecking +import caps.{cap, use} + +def foo1(@use xs: List[() => Unit]): Unit = + var x: () ->{xs*} Unit = xs.head + var ys = xs + while ys.nonEmpty do + ys = ys.tail + x = ys.head + +def foo2(@use xs: List[() => Unit]): Unit = + def inner[@use C^](xs: List[() ->{C} Unit]): Unit = + var x: () ->{C} Unit = xs.head + var ys = xs + while ys.nonEmpty do + ys = ys.tail + x = ys.head + inner(xs) + +def foo3[@use C^](xs: List[() ->{C} Unit]): Unit = + var x: () ->{C} Unit = xs.head + var ys = xs + while ys.nonEmpty do + ys = ys.tail + x = ys.head