diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ab40a3faaa36..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. @@ -427,11 +432,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 @@ -460,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. */ @@ -481,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 @@ -499,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,13 +528,26 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") 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 @@ -1990,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 = @@ -2018,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/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 = () => 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