From e98b50341ec09627a507f26ca01c3d2819e4cf5d Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 30 Jul 2024 19:16:48 +0200 Subject: [PATCH 1/3] Fix setup of CapSet arguments. These arguments tell the whole truth; they cannot possibly be decorated with another capture set. So we should not add a capture set variable. --- compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 4 +++- .../src/dotty/tools/dotc/cc/CapturingType.scala | 1 + compiler/src/dotty/tools/dotc/cc/Setup.scala | 11 +++++++---- tests/pos/polycap.scala | 14 ++++++++++++++ 4 files changed, 25 insertions(+), 5 deletions(-) create mode 100644 tests/pos/polycap.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 5680df476f8d..a2d2d2cf358c 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -264,7 +264,9 @@ extension (tp: Type) def boxed(using Context): Type = tp.dealias match case tp @ CapturingType(parent, refs) if !tp.isBoxed && !refs.isAlwaysEmpty => tp.annot match - case ann: CaptureAnnotation => AnnotatedType(parent, ann.boxedAnnot) + case ann: CaptureAnnotation => + assert(!parent.derivesFrom(defn.Caps_CapSet)) + AnnotatedType(parent, ann.boxedAnnot) case ann => tp case tp: RealTypeBounds => tp.derivedTypeBounds(tp.lo.boxed, tp.hi.boxed) diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index bb79e52f1060..9f9b923b2c88 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -33,6 +33,7 @@ object CapturingType: * boxing status is the same or if A is boxed. */ def apply(parent: Type, refs: CaptureSet, boxed: Boolean = false)(using Context): Type = + assert(!boxed || !parent.derivesFrom(defn.Caps_CapSet)) if refs.isAlwaysEmpty && !refs.keepAlways then parent else parent match case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed => diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index c048edfb2102..25d50052f107 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -134,9 +134,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: private def box(tp: Type)(using Context): Type = def recur(tp: Type): Type = tp.dealiasKeepAnnotsAndOpaques match case tp @ CapturingType(parent, refs) => - if tp.isBoxed then tp else tp.boxed + if tp.isBoxed || parent.derivesFrom(defn.Caps_CapSet) then tp + else tp.boxed case tp @ AnnotatedType(parent, ann) => - if ann.symbol.isRetains + if ann.symbol.isRetains && !parent.derivesFrom(defn.Caps_CapSet) then CapturingType(parent, ann.tree.toCaptureSet, boxed = true) else tp.derivedAnnotatedType(box(parent), ann) case tp1 @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp1) => @@ -605,8 +606,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: !refs.isEmpty case tp: (TypeRef | AppliedType) => val sym = tp.typeSymbol - if sym.isClass then !sym.isPureClass - else instanceCanBeImpure(tp.superType) + if sym.isClass + then !sym.isPureClass + else !tp.derivesFrom(defn.Caps_CapSet) // CapSet arguments don't get other capture set variables added + && instanceCanBeImpure(tp.superType) case tp: (RefinedOrRecType | MatchType) => instanceCanBeImpure(tp.underlying) case tp: AndType => diff --git a/tests/pos/polycap.scala b/tests/pos/polycap.scala new file mode 100644 index 000000000000..684f46454595 --- /dev/null +++ b/tests/pos/polycap.scala @@ -0,0 +1,14 @@ +import language.experimental.captureChecking + +class Source[+T, Cap^] + +def completed[T, Cap^](result: T): Source[T, Cap] = + //val fut = new Source[T, Cap]() + val fut2 = new Source[T, Cap]() + fut2: Source[T, Cap] + + + + + + From 02b1b6d3481342d753b0f678e5383d81faba2c8d Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 4 Aug 2024 11:16:58 +0200 Subject: [PATCH 2/3] Implement caps.Contains --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 24 ++++++++++++++++++- .../dotty/tools/dotc/core/Definitions.scala | 6 +++-- library/src/scala/caps.scala | 12 +++++++++- tests/neg-custom-args/captures/i21313.check | 11 +++++++++ tests/neg-custom-args/captures/i21313.scala | 15 ++++++++++++ tests/pos-custom-args/captures/i21313.scala | 11 +++++++++ 6 files changed, 75 insertions(+), 4 deletions(-) create mode 100644 tests/neg-custom-args/captures/i21313.check create mode 100644 tests/neg-custom-args/captures/i21313.scala create mode 100644 tests/pos-custom-args/captures/i21313.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 6fa63c21edaa..5af57c31e05f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -674,7 +674,29 @@ class CheckCaptures extends Recheck, SymTransformer: i"Sealed type variable $pname", "be instantiated to", i"This is often caused by a local capability$where\nleaking as part of its result.", tree.srcPos) - handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt))) + val res = handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt))) + if meth == defn.Caps_containsImpl then checkContains(tree) + res + end recheckTypeApply + + /** Faced with a tree of form `caps.contansImpl[CS, r.type]`, check that `R` is a tracked + * capability and assert that `{r} <:CS`. + */ + def checkContains(tree: TypeApply)(using Context): Unit = + tree.fun.knownType.widen match + case fntpe: PolyType => + tree.args match + case csArg :: refArg :: Nil => + val cs = csArg.knownType.captureSet + val ref = refArg.knownType + capt.println(i"check contains $cs , $ref") + ref match + case ref: CaptureRef if ref.isTracked => + checkElem(ref, cs, tree.srcPos) + case _ => + report.error(em"$refArg is not a tracked capability", refArg.srcPos) + case _ => + case _ => override def recheckBlock(tree: Block, pt: Type)(using Context): Type = inNestedLevel(super.recheckBlock(tree, pt)) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index fda12a5488ce..1d2f2b05feb4 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -993,15 +993,17 @@ class Definitions { @tu lazy val CapsModule: Symbol = requiredModule("scala.caps") @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap") @tu lazy val Caps_Capability: TypeSymbol = CapsModule.requiredType("Capability") - @tu lazy val Caps_CapSet = requiredClass("scala.caps.CapSet") + @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet") @tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability") @tu lazy val Caps_capsOf: TermSymbol = CapsModule.requiredMethod("capsOf") - @tu lazy val Caps_Exists = requiredClass("scala.caps.Exists") + @tu lazy val Caps_Exists: ClassSymbol = requiredClass("scala.caps.Exists") @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe") @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure") @tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox") @tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox") @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg") + @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Capability") + @tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl") @tu lazy val PureClass: Symbol = requiredClass("scala.Pure") diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala index 1416a7b35f83..9700ed62738d 100644 --- a/library/src/scala/caps.scala +++ b/library/src/scala/caps.scala @@ -1,6 +1,6 @@ package scala -import annotation.{experimental, compileTimeOnly} +import annotation.{experimental, compileTimeOnly, retainsCap} @experimental object caps: @@ -19,6 +19,16 @@ import annotation.{experimental, compileTimeOnly} /** Carrier trait for capture set type parameters */ trait CapSet extends Any + /** A type constraint expressing that the capture set `C` needs to contain + * the capability `R` + */ + sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton] + + /** The only implementation of `Contains`. The constraint that `{R} <: C` is + * added separately by the capture checker. + */ + given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]() + @compileTimeOnly("Should be be used only internally by the Scala compiler") def capsOf[CS]: Any = ??? diff --git a/tests/neg-custom-args/captures/i21313.check b/tests/neg-custom-args/captures/i21313.check new file mode 100644 index 000000000000..37b944a97d68 --- /dev/null +++ b/tests/neg-custom-args/captures/i21313.check @@ -0,0 +1,11 @@ +-- Error: tests/neg-custom-args/captures/i21313.scala:6:27 ------------------------------------------------------------- +6 |def foo(x: Async) = x.await(???) // error + | ^ + | (x : Async) is not a tracked capability +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 --------------------------------------- +15 | ac1.await(src2) // error + | ^^^^ + | Found: (src2 : Source[Int, caps.CapSet^{ac2}]^?) + | Required: Source[Int, caps.CapSet^{ac1}]^ + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21313.scala b/tests/neg-custom-args/captures/i21313.scala new file mode 100644 index 000000000000..01bedb10aefd --- /dev/null +++ b/tests/neg-custom-args/captures/i21313.scala @@ -0,0 +1,15 @@ +import caps.CapSet + +trait Async: + def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T + +def foo(x: Async) = x.await(???) // error + +trait Source[+T, Cap^]: + final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap. + +def test(using ac1: Async^, ac2: Async^, x: String) = + val src1 = new Source[Int, CapSet^{ac1}] {} + ac1.await(src1) // ok + val src2 = new Source[Int, CapSet^{ac2}] {} + ac1.await(src2) // error diff --git a/tests/pos-custom-args/captures/i21313.scala b/tests/pos-custom-args/captures/i21313.scala new file mode 100644 index 000000000000..2fda6c0c0e45 --- /dev/null +++ b/tests/pos-custom-args/captures/i21313.scala @@ -0,0 +1,11 @@ +import caps.CapSet + +trait Async: + def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T + +trait Source[+T, Cap^]: + final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap. + +def test(using ac1: Async^, ac2: Async^, x: String) = + val src1 = new Source[Int, CapSet^{ac1}] {} + ac1.await(src1) From 618bbc52bf2a3407a2e0ff2788a9df1265df035d Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 7 Aug 2024 19:25:06 +0200 Subject: [PATCH 3/3] Handle local type parameters in markFree These need to be handled like reach capabilities. Fixes #21347 --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 30 ++++++++++--------- tests/neg-custom-args/captures/i21347.check | 15 ++++++++++ tests/neg-custom-args/captures/i21347.scala | 12 ++++++++ 3 files changed, 43 insertions(+), 14 deletions(-) create mode 100644 tests/neg-custom-args/captures/i21347.check create mode 100644 tests/neg-custom-args/captures/i21347.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 5af57c31e05f..dbf01915122d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -388,23 +388,25 @@ class CheckCaptures extends Recheck, SymTransformer: // should be included. val included = cs.filter: c => c.stripReach match - case ref: TermRef => - //if c.isReach then println(i"REACH $c in ${env.owner}") - //assert(!env.owner.isAnonymousFunction) + case ref: NamedType => val refSym = ref.symbol val refOwner = refSym.owner val isVisible = isVisibleFromEnv(refOwner) - if !isVisible && c.isReach && refSym.is(Param) && refOwner == env.owner then - if refSym.hasAnnotation(defn.UnboxAnnot) then - capt.println(i"exempt: $ref in $refOwner") - else - // Reach capabilities that go out of scope have to be approximated - // by their underlying capture set, which cannot be universal. - // Reach capabilities of @unboxed parameters are exempted. - val cs = CaptureSet.ofInfo(c) - cs.disallowRootCapability: () => - report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) - checkSubset(cs, env.captured, pos, provenance(env)) + if !isVisible + && (c.isReach || ref.isType) + && refSym.is(Param) + && refOwner == env.owner + then + if refSym.hasAnnotation(defn.UnboxAnnot) then + capt.println(i"exempt: $ref in $refOwner") + else + // Reach capabilities that go out of scope have to be approximated + // by their underlying capture set, which cannot be universal. + // Reach capabilities of @unboxed parameters are exempted. + val cs = CaptureSet.ofInfo(c) + cs.disallowRootCapability: () => + report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) + checkSubset(cs, env.captured, pos, provenance(env)) isVisible case ref: ThisType => isVisibleFromEnv(ref.cls) case _ => false diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check new file mode 100644 index 000000000000..c680a54d3efc --- /dev/null +++ b/tests/neg-custom-args/captures/i21347.check @@ -0,0 +1,15 @@ +-- Error: tests/neg-custom-args/captures/i21347.scala:4:15 ------------------------------------------------------------- +4 | ops.foreach: op => // error + | ^ + | Local reach capability C leaks into capture scope of method runOps +5 | op() +-- Error: tests/neg-custom-args/captures/i21347.scala:8:14 ------------------------------------------------------------- +8 | () => runOps(f :: Nil) // error + | ^^^^^^^^^^^^^^^^ + | reference (caps.cap : caps.Capability) is not included in the allowed capture set {} + | of an enclosing function literal with expected type () -> Unit +-- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------ +11 | ops.foreach: op => // error + | ^ + | Local reach capability ops* leaks into capture scope of method runOpsAlt +12 | op() diff --git a/tests/neg-custom-args/captures/i21347.scala b/tests/neg-custom-args/captures/i21347.scala new file mode 100644 index 000000000000..41887be6a78a --- /dev/null +++ b/tests/neg-custom-args/captures/i21347.scala @@ -0,0 +1,12 @@ +import language.experimental.captureChecking + +def runOps[C^](ops: List[() ->{C^} Unit]): Unit = + ops.foreach: op => // error + op() + +def boom(f: () => Unit): () -> Unit = + () => runOps(f :: Nil) // error + +def runOpsAlt(ops: List[() => Unit]): Unit = + ops.foreach: op => // error + op() \ No newline at end of file