diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 92fa632f5166..c6c442a953d9 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -917,12 +917,26 @@ class CheckCaptures extends Recheck, SymTransformer: */ def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = var refined: Type = core - var allCaptures: CaptureSet = initCs ++ captureSetImpliedByFields(cls, core) + val implied = captureSetImpliedByFields(cls, core) + var allCaptures: CaptureSet = initCs ++ implied for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this - allCaptures ++= argType.captureSet + if getter.hasAnnotation(defn.ConsumeAnnot) + && !implied.isAlwaysEmpty + && argType.captureSet.subCaptures(allCaptures) + // A consume parameter of a constructor will be hidden in the implied fresh of the + // class if there is one. Example: + // + // class A(consume val x: B^) { val c: C^ = ... } + // val a = A(b) // a: A{...}^{cap hiding b} + // But + // class A1(val x: B^) { val c: C^ = ... } + // val a1 = A1(b) // a1: A{...}^{cap, b} + // See consume-in-constructor.scala. + then () // force the fresh in implied to hide argType.captureSet + else allCaptures ++= argType.captureSet (refined, allCaptures) /** Augment result type of constructor with refinements and captures. diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index b98f07080181..7fff46ca9c7e 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -7,6 +7,7 @@ import collection.mutable import core.* import Symbols.*, Types.*, Flags.*, Contexts.*, Names.*, Decorators.* import CaptureSet.{Refs, emptyRefs, HiddenSet} +import NameKinds.WildcardParamName import config.Printers.capt import StdNames.nme import util.{SimpleIdentitySet, EqHashMap, SrcPos} @@ -558,6 +559,69 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: sepApplyError(fn, parts, arg, app) end checkApply + /** Compute the set of capabilities that are consumed along a selection path. + * For example, if we have the path `a.b` where `b` is a consume field with type `B^{x}`, + * this returns the actual consumed capabilities `{x}` from the type's capture set. + * + * This walks the path and for each consume field encountered, collects the capabilities + * from that field's widened type's capture set. + * + * @param cap The capability to analyze (e.g., `a.b`) + * @return The set of actual consumed capabilities from all consume fields along the path + */ + def consumedByPath(cap: Capability)(using Context): Refs = cap match + case Reach(underlying) => consumedByPath(underlying) + case ref: TermRef => + def recur(tp: Type, acc: Refs): Refs = tp match + case ref: TermRef => + // This is a selection like a.b, or just a reference like a + val fieldSym = ref.symbol + val accWithCurrent = + if fieldSym.exists && fieldSym.isConsumeParam then + // This field is a consume parameter. Collect capabilities from its type's capture set. + acc ++ ref.widen.captureSet.elems + else + acc + // Also check if the current reference's type has consume fields + val accWithConsumeFields = accWithCurrent ++ capsFromConsumeFields(ref) + // Recurse on the prefix if it's a selection + if ref.prefix ne NoPrefix then + recur(ref.prefix, accWithConsumeFields) + else + accWithConsumeFields + case _ => + acc + + def capsFromConsumeFields(ref: TermRef): Refs = + // For types with consume fields, use the capture set of the reference itself + // and recursively check what those capabilities consume + val tpe = ref.widen.dealias + val cls = tpe.classSymbol + if cls.exists then + // Check if this class has any consume fields + val hasConsumeFields = cls.info.decls.exists(m => m.isConsumeParam && m.isTerm) + if hasConsumeFields then + // Use the capture set of the widened type + val captureSet = ref.widen.captureSet.elems + // Use the capture set of the reference itself (e.g., {a} for holder.a : A^{a}) + // Return both the capabilities in the capture set AND what they transitively consume + var result = emptyRefs + for cap <- captureSet do + cap match + case _: RootCapability => // Skip + case _ => + result = result + cap + result = result ++ consumedByPath(cap) + result + else + emptyRefs + else + emptyRefs + + recur(ref, emptyRefs) + case _ => + emptyRefs + /** 1. Check that the capabilities used at `tree` don't overlap with * capabilities hidden by a previous definition. * 2. Also check that none of the used capabilities was consumed before. @@ -597,8 +661,18 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for ref <- used do val pos = consumed.clashing(ref) if pos != null then - // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }") - consumeError(ref, pos, tree.srcPos) + // Check if this reference should be exempted because consume fields along + // the path own the consumed capabilities. + val pathConsumed = consumedByPath(ref) + + // Check if any capability consumed by the path was consumed at position `pos`. + // We need to check both the capability and its reach, since consumed might store the reach version. + val shouldExempt = pathConsumed.exists: + case _: RootCapability => false + case cap => consumed.get(cap) == pos || consumed.get(cap.reach) == pos + + if !shouldExempt then + consumeError(ref, pos, tree.srcPos) end checkUse /** If `tp` denotes some version of a singleton capability `x.type` the set `{x, x*}` @@ -986,7 +1060,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: traverseSection(tree) case tree: ValDef => traverseChildren(tree) - checkValOrDefDef(tree) + if !tree.name.is(WildcardParamName) then + checkValOrDefDef(tree) case tree: DefDef => if skippable(tree.symbol) then capt.println(i"skipping sep check of ${tree.symbol}") diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check new file mode 100644 index 000000000000..d6d3fad2e89e --- /dev/null +++ b/tests/neg-custom-args/captures/consume-in-constructor.check @@ -0,0 +1,31 @@ +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 -------------------------------------------- +20 | println(b) // error + | ^ + | Separation failure: Illegal access to {b} which is hidden by the previous definition + | of value a2 with type A2{val b: B^{b²}}^. + | This type hides capabilities {cap, b²} + | + | where: ^ refers to a fresh root capability in the type of value a2 + | b is a value in class A2 + | b² is a value in method Test + | cap is a fresh root capability created in value a2 when constructing instance A2 +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 -------------------------------------------- +21 | println(a1) // error, since `b` was consumed before + | ^^ + | Separation failure: Illegal access to {b} which is hidden by the previous definition + | of value a2 with type A2{val b: B^{b²}}^. + | This type hides capabilities {cap, b²} + | + | where: ^ refers to a fresh root capability in the type of value a2 + | b is a value in class A2 + | b² is a value in method Test + | cap is a fresh root capability created in value a2 when constructing instance A2 +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:28:10 -------------------------------------------- +28 | println(b) // error, b is hidden in the type of a1 + | ^ + | Separation failure: Illegal access to {b} which is hidden by the previous definition + | of value a1 with type A1^. + | This type hides capabilities {cap, b} + | + | where: ^ refers to a fresh root capability in the type of value a1 + | cap is a fresh root capability created in value a1 when constructing instance A1 diff --git a/tests/neg-custom-args/captures/consume-in-constructor.scala b/tests/neg-custom-args/captures/consume-in-constructor.scala new file mode 100644 index 000000000000..eec43073ab68 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-in-constructor.scala @@ -0,0 +1,33 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +class B + +class A1(val b: B^): + val bb: B^ = B() + +class A2(consume val b: B^): + val bb: B^ = B() + +def Test = + val b: B^ = B() + val a1 = A1(b) + val _: A1^{cap, b} = a1 + println(b) // OK since a1's type mentions `b` explicitly + val a2 = A2(b) + val _: A2^{cap, b} = a2 + println(b) // error + println(a1) // error, since `b` was consumed before + println(a2) // OK since b belongs to a2 + println(a2.b) // OK since b belongs to a2 + +def Test2 = + val b: B^ = B() + val a1: A1^ = A1(b) + println(b) // error, b is hidden in the type of a1 + + + + + diff --git a/tests/pos-custom-args/captures/paths-complex-consume.scala b/tests/pos-custom-args/captures/paths-complex-consume.scala new file mode 100644 index 000000000000..f4fbc0ca7c11 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-complex-consume.scala @@ -0,0 +1,80 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +// Create a deeper nesting structure +class D() +class C(val d: D^) +class B(val c: C^) +class A(consume val b: B^) + +// Test 1: Accessing nested fields through a consumed path +def testNestedFieldsAfterConsume = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + + // After a consumed b, we should be able to access: + println(a.b) // OK - a owns b + println(a.b.c) // OK - accessing field of consumed b through a + println(a.b.c.d) // OK - deeper nesting through consumed path + +// Test 2: Non-trivial prefix accessing a consumed field +class Container(consume val a: A^): + val other: A^ = A(B(C(D()))) + +class Outer(consume val container: Container^) + +def testComplexPrefix = + val d1: D^ = D() + val c1: C^ = C(d1) + val b1: B^ = B(c1) + val a1 = A(b1) + val container1 = Container(a1) + val outer = Outer(container1) + + // Non-trivial prefix: outer.container.a (where 'a' was consumed by container) + println(outer.container) // OK - outer consumed container + println(outer.container.a) // OK - accessing consumed field through prefix + println(outer.container.a.b) // OK - and then its nested fields + println(outer.container.a.b.c) // OK - even deeper + println(outer.container.a.b.c.d) // OK - deepest level + +// Test 3: Multiple consume parameters with nested access +class Multi(consume val b1: B^, consume val b2: B^): + val b3: B^ = B(C(D())) + +def testMultipleConsume = + val b1: B^ = B(C(D())) + val b2: B^ = B(C(D())) + val multi = Multi(b1, b2) + + // All of these should work: + println(multi.b1) // OK + println(multi.b1.c) // OK - nested field of consumed b1 + println(multi.b1.c.d) // OK - deeper nesting + println(multi.b2) // OK + println(multi.b2.c) // OK - nested field of consumed b2 + println(multi.b2.c.d) // OK - deeper nesting + println(multi.b3.c.d) // OK - non-consumed field + +// Test 4: Consume at multiple levels with complex paths +class Top(consume val outer: Outer^) + +def testMultiLevelConsume = + val d2: D^ = D() + val c2: C^ = C(d2) + val b2: B^ = B(c2) + val a2 = A(b2) + val container2 = Container(a2) + val outer2 = Outer(container2) + val top = Top(outer2) + + // Very deep path through multiple consume levels: + println(top.outer) // OK - top consumed outer + println(top.outer.container) // OK - continue through path + println(top.outer.container.a) // OK - container consumed a + println(top.outer.container.a.b) // OK - a consumed b + println(top.outer.container.a.b.c) // OK - nested field + println(top.outer.container.a.b.c.d) // OK - deepest field diff --git a/tests/pos-custom-args/captures/paths-deep-consume.scala b/tests/pos-custom-args/captures/paths-deep-consume.scala new file mode 100644 index 000000000000..6a890b934ec4 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-deep-consume.scala @@ -0,0 +1,24 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +class B + +class A(consume val b: B^): + val bb: B^ = B() + +class C(consume val a: A^): + val aa: A^ = A(B()) + +// Test deep nested access paths +def testDeepPaths = + val b: B^ = B() + val a = A(b) + val c = C(a) + + // All these should work - accessing through ownership chain + println(c.a) // c owns a + println(c.a.b) // c owns a, a owns b + println(c.a.bb) // c owns a, accessing other field + println(c.aa) // accessing other field of c + println(c.aa.b) // accessing nested field through c.aa diff --git a/tests/pos-custom-args/captures/paths-nested-consume.scala b/tests/pos-custom-args/captures/paths-nested-consume.scala new file mode 100644 index 000000000000..7caa46a28426 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-nested-consume.scala @@ -0,0 +1,33 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +class B + +class A(consume val b: B^): + val bb: B^ = B() + +class C(consume val a: A^): + val aa: A^ = A(B()) + +// Test: After consuming b into a, then consuming a into c, +// we should be able to access c.a.b (nested field selection) +def testNestedAccess = + val b: B^ = B() + val a = A(b) + println(a.b) // OK - a consumed b, accessing through a + val c = C(a) + println(c.a) // Should be OK - c consumed a, accessing through c + println(c.a.b) // Should be OK - accessing b through c.a, where c owns a and a owns b + +// Test: The deeper path c.a.b should work even though a was consumed +def testDeepPath = + val b: B^ = B() + val a = A(b) + val c = C(a) + // At this point: + // - b was consumed by a (so we can't use b directly) + // - a was consumed by c (so we can't use a directly) + // But we should be able to access: + println(c.a.b) // OK - full path through ownership chain + println(c.a.bb) // OK - other field of c.a diff --git a/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala new file mode 100644 index 000000000000..02b8e78197be --- /dev/null +++ b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala @@ -0,0 +1,37 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +// Create a deep nesting structure for testing suffix paths +class D +class C(val d: D^) +class B(val c: C^) +class A(consume val b: B^) + +// Test 1: Simple suffix paths after consume +def test1 = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + + // After 'a' consumes 'b', access nested fields: + println(a.b) // OK - consumed field + println(a.b.c) // OK - suffix: .c after consumed field + println(a.b.c.d) // OK - suffix: .c.d after consumed field + +// Test 2: Non-consume wrapper with consumed inner field +class Holder(val a: A^) // Note: NOT consume + +def test2 = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + val holder = Holder(a) + + // Access through holder.a.b where b was consumed by a: + println(holder.a) // OK - not consumed + println(holder.a.b) // OK - accessing consumed field through prefix + println(holder.a.b.c) // OK - suffix .c + println(holder.a.b.c.d) // OK - suffix .c.d