From 5d1a3128b23517dd649bdaac4f9d8aab8656d2c1 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 3 Jun 2026 23:50:06 +0200 Subject: [PATCH] Check anonymous functions with fresh results for consume conditions Previously, anonymous functions were excluded. lambda-fresh-2.scala shows why this is unsound. We now drop the special treatment of anonymous functions, and at the same time exclude LocalCaps that come from outside the function from checking. --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 23 ++++++----- .../src/dotty/tools/dotc/cc/ccConfig.scala | 2 +- .../captures/lambda-fresh-2.check | 36 ++++++++++++++++++ .../captures/lambda-fresh-2.scala | 38 +++++++++++++++++++ tests/neg-custom-args/captures/reaches.check | 10 +++++ tests/neg-custom-args/captures/reaches.scala | 4 +- .../captures/scoped-caps-global.scala | 2 +- .../captures/scoped-caps.check | 4 ++ .../captures/scoped-caps.scala | 2 +- 9 files changed, 106 insertions(+), 15 deletions(-) create mode 100644 tests/neg-custom-args/captures/lambda-fresh-2.check create mode 100644 tests/neg-custom-args/captures/lambda-fresh-2.scala diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 64e327187567..4871ecf4de9d 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -863,20 +863,23 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case _ => /** If `tpe` appears as a (result-) type of a definition, treat its - * hidden set minus its explicitly declared footprint as consumed. - * If `tpe` appears as an argument to a consume parameter, treat + * hidden set of locally owned LocalCaps minus its explicitly declared footprint + * as consumed. If `tpe` appears as an argument to a consume parameter, treat * its footprint as consumed. */ def checkLegalRefs() = role match case TypeRole.Result(sym, _) => - if !sym.isAnonymousFunction // we don't check return types of anonymous functions - && !sym.is(Case) // We don't check so far binders in patterns since they - // have inferred universal types. TODO come back to this; - // either infer more precise types for such binders or - // "see through them" when we look at hidden sets. + if !sym.is(Case) // We don't check so far binders in patterns since they + // have inferred universal types. TODO come back to this; + // either infer more precise types for such binders or + // "see through them" when we look at hidden sets. then - val refs = tpe.deepCaptureSet.elems - val refsStar = refs.transHiddenSet + var refs = tpe.deepCaptureSet.elems + val refsCaps = refs.filter: elem => + elem.core match + case core: LocalCap => core.ccOwner.isContainedIn(sym) + case _ => false + val refsStar = refsCaps.transHiddenSet val toCheck = refsStar.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks) def descr = i"${role.description} $tpe hides" checkConsumedRefs(toCheck, tpe, role, descr, pos) @@ -1015,8 +1018,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: && !isUnsafeAssumeSeparate(tree.rhs) && !isCoverageLiftedTemp(tree) then + capt.println(i"sep check def $sym: ${tree.tpt.nuType} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}") checkType(tree.tpt, sym) - capt.println(i"sep check def $sym: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}") pushDef(tree, spanCaptures(tree.tpt).transHiddenSet.deductSymRefs(sym)) def inSection[T](op: => T)(using Context): T = diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala index 090fa38043da..f88b4df234e0 100644 --- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala +++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala @@ -54,7 +54,7 @@ object ccConfig: /** Not used currently. Handy for trying out new features */ def newScheme(using ctx: Context): Boolean = - Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.9`) + Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.10`) /** Allow @use annotations */ def allowUse(using Context): Boolean = diff --git a/tests/neg-custom-args/captures/lambda-fresh-2.check b/tests/neg-custom-args/captures/lambda-fresh-2.check new file mode 100644 index 000000000000..1a7cfae9af00 --- /dev/null +++ b/tests/neg-custom-args/captures/lambda-fresh-2.check @@ -0,0 +1,36 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:20:29 ------------------------------- +20 | val a: () => Ref^{fresh} = () => f1 // error + | ^^^^^^^^ + |Found: () ->{f1.rd} Ref^{any} + |Required: () => Ref^{fresh} + | + |Note that capability `any` cannot flow into capture set {fresh²} + |because `fresh²`, which is existentially bound in Ref^{fresh³}, cannot subsume `any`. + | + |where: => refers to a root capability in the type of value a + | any is a root capability classified as Unscoped created in anonymous function of type (): Ref^{any} when instantiating expected result type Ref^{fresh} of function literal + | fresh is a root capability associated with the result type of (): Ref^{fresh} + | fresh² is a root capability associated with the result type of (): Ref^{any} + | fresh³ is the root capability caps.fresh + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:12:36 ---------------------------------------------------- +12 | val a: () => File^{fresh} = () => f1 // error + | ^ + |Separation failure: anonymous function of type (): File^{fresh}'s inferred result type File^ hides non-local value f1 +-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:14:11 ---------------------------------------------------- +14 | def g(): File^ = f3 // error + | ^^^^^ + | Separation failure: method g's result type File^ hides non-local value f3 +-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:22:11 ---------------------------------------------------- +22 | def g(): Ref^ = f3 // error + | ^^^^ + | Separation failure: method g's result type Ref^ hides non-local value f3 +-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:28:35 ---------------------------------------------------- +28 | val a: () => One^{fresh} = () => f1 // error + | ^ + |Separation failure: anonymous function of type (): One^{fresh}'s inferred result type One^ hides non-local value f1 +-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:30:11 ---------------------------------------------------- +30 | def g(): One^ = f3 // error + | ^^^^ + | Separation failure: method g's result type One^ hides non-local value f3 diff --git a/tests/neg-custom-args/captures/lambda-fresh-2.scala b/tests/neg-custom-args/captures/lambda-fresh-2.scala new file mode 100644 index 000000000000..c66df47d4295 --- /dev/null +++ b/tests/neg-custom-args/captures/lambda-fresh-2.scala @@ -0,0 +1,38 @@ +import caps.* + +class Ref extends Mutable +class One extends ExclusiveCapability +class Sha extends SharedCapability +class File + +def test() = + val f1: File^ = File() + val f2: File^ = File() + val f3: File^ = File() + val a: () => File^{fresh} = () => f1 // error + val b: () => File^ = () => f2 // ok + def g(): File^ = f3 // error + +def test1() = + val f1 = Ref() + val f2 = Ref() + val f3 = Ref() + val a: () => Ref^{fresh} = () => f1 // error + val b: () => Ref^ = () => f2 // ok + def g(): Ref^ = f3 // error + +def test2() = + val f1 = One() + val f2 = One() + val f3 = One() + val a: () => One^{fresh} = () => f1 // error + val b: () => One^ = () => f2 // ok + def g(): One^ = f3 // error + +def test3() = + val f1 = Sha() + val f2 = Sha() + val f3 = Sha() + val a: () => Sha^{fresh} = () => f1 // ok, SharedCapabilities are excluded from frhsness checking + val b: () => Sha^ = () => f2 // ok + def g(): Sha^ = f3 // ok, SharedCapabilities are excluded from frhsness checking diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index a474dee39396..0ed28baaeb61 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -84,6 +84,16 @@ | ^^^^^^^^^^ | Separation failure: value next's type () => Unit hides parameter xs. | The parameter needs to be annotated with consume to allow this. +-- Error: tests/neg-custom-args/captures/reaches.scala:67:40 ----------------------------------------------------------- +67 | val id: (x: File^) -> File^{fresh} = x => x // error + | ^ + |Separation failure: anonymous function of type (x: File^): File^{fresh}'s inferred result type File^ hides parameter x. + |The parameter needs to be annotated with consume to allow this. +-- Error: tests/neg-custom-args/captures/reaches.scala:68:36 ----------------------------------------------------------- +68 | val id2: File^ -> File^{fresh} = x => x // error + | ^ + |Separation failure: anonymous function of type (x: File^): File^{fresh}'s inferred result type File^ hides parameter x. + |The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/reaches.scala:88:28 ----------------------------------------------------------- 88 | ps.map((x, y) => compose1(x, y)) // error // error // error | ^ diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index 26e9652587df..e893228fc731 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -64,8 +64,8 @@ def attack2 = f1 def attack3 = - val id: (x: File^) -> File^{fresh} = x => x // was error, now OK - val id2: File^ -> File^{fresh} = x => x // now also OK + val id: (x: File^) -> File^{fresh} = x => x // error + val id2: File^ -> File^{fresh} = x => x // error val leaked = usingFile[File^{id*}]: f => val f1: File^{id*} = id(f) // error diff --git a/tests/neg-custom-args/captures/scoped-caps-global.scala b/tests/neg-custom-args/captures/scoped-caps-global.scala index 4c07322e7250..c5bbb39c115b 100644 --- a/tests/neg-custom-args/captures/scoped-caps-global.scala +++ b/tests/neg-custom-args/captures/scoped-caps-global.scala @@ -19,7 +19,7 @@ def test(io: Object^): Unit = val h: S -> B^ = ??? val _: (x: S) -> B^{fresh} = h // error: direct conversion fails - val _: (x: S) -> B^{fresh} = (x: S) => h(x) // eta expansion is ok + val _: (x: S) -> B^{fresh} = (x: S) => h(x) // error: eta expansion also fails since `h` is non-local val h2: S -> S = ??? val _: (x: S) -> S^{fresh} = h2 // direct conversion OK for shared S diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check index 76383ae0ab40..6b3156ef0470 100644 --- a/tests/neg-custom-args/captures/scoped-caps.check +++ b/tests/neg-custom-args/captures/scoped-caps.check @@ -94,3 +94,7 @@ | any² is a root capability in the type of value _$16 | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/scoped-caps.scala:20:36 ------------------------------------------------------- +20 | val _: (x: S) -> B^{fresh} = (x: S) => h(x) // error: eta expansion also fails since `h` is non-local + | ^ + |Separation failure: anonymous function of type (x: S^): B^{fresh}'s inferred result type B^ hides non-local value h diff --git a/tests/neg-custom-args/captures/scoped-caps.scala b/tests/neg-custom-args/captures/scoped-caps.scala index 7e380f9fb092..d7e0f9c41da2 100644 --- a/tests/neg-custom-args/captures/scoped-caps.scala +++ b/tests/neg-custom-args/captures/scoped-caps.scala @@ -17,7 +17,7 @@ def test(io: Object^): Unit = val h: S -> B^ = ??? val _: (x: S) -> B^{fresh} = h // error: direct conversion fails - val _: (x: S) -> B^{fresh} = (x: S) => h(x) // eta expansion is ok + val _: (x: S) -> B^{fresh} = (x: S) => h(x) // error: eta expansion also fails since `h` is non-local val h2: S -> S = ??? val _: (x: S) -> S^{fresh} = h2 // direct conversion OK for shared S