Skip to content

Exclusive capabilities #22218

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 23 commits into from
Feb 5, 2025
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
22cb87b
Elide capabilities implied by Capability subtypes when printing
odersky Dec 6, 2024
216973e
Add Mutable classes and ReadOnly capabilities
odersky Jan 10, 2025
234d0dc
Drop special handling of functions with pure arguments in Existential…
odersky Dec 15, 2024
a239bfa
Implement fresh capabilities
odersky Jan 11, 2025
d211bf9
Separation checking for applications
odersky Jan 11, 2025
fd327e3
Separation checking for blocks
odersky Jan 12, 2025
b0be75b
Address review comments
odersky Jan 19, 2025
c377f49
Use deep capturesets for separation checking.
odersky Jan 20, 2025
1cdb21b
Cache derived reach, readOnly, and maybe capabilities
odersky Jan 20, 2025
937b8af
Avoid forming intersections of capture sets on refined type lookup
odersky Jan 21, 2025
438ea60
Check separation of different parts of a declared type.
odersky Jan 24, 2025
c1f2542
Check that hidden parameters are annotated @consume
odersky Jan 25, 2025
9ca1776
Check that only @consume parameters flow to @consume parameters
odersky Jan 26, 2025
564c847
Check that SharedCapabilities don't capture `cap`.
odersky Jan 26, 2025
94fcabc
Turn separation checking on by default
odersky Jan 26, 2025
e229807
Make sure fresh results of methods only hide local refs
odersky Jan 27, 2025
84b5bff
Make sure parameters are not used again after they are consumed
odersky Jan 28, 2025
c1ad0c1
Check accesses to non-local this in hidden sets
odersky Jan 28, 2025
65a1301
Check that @consumed prefix capabilities are not re-used
odersky Jan 29, 2025
9f40649
Allow SharableCapablity anywhere on a path
odersky Jan 30, 2025
b0628d1
Polishings
odersky Jan 31, 2025
813c585
Polish and document separation checker.
odersky Feb 1, 2025
a41c10f
Address review comments
odersky Feb 5, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Cache derived reach, readOnly, and maybe capabilities
This is necessary since capability sets are IdentitySets.
  • Loading branch information
odersky committed Jan 29, 2025
commit 1cdb21b3a1d23ccd1da75d09cba55ad9030729e4
24 changes: 16 additions & 8 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,10 @@ extension (tp: Type)
def reach(using Context): CaptureRef = tp match
case tp @ AnnotatedType(tp1: CaptureRef, annot)
if annot.symbol == defn.MaybeCapabilityAnnot =>
tp.derivedAnnotatedType(tp1.reach, annot)
tp1.reach.maybe
case tp @ AnnotatedType(tp1: CaptureRef, annot)
if annot.symbol == defn.ReadOnlyCapabilityAnnot =>
tp1.reach.readOnly
case tp @ AnnotatedType(tp1: CaptureRef, annot)
if annot.symbol == defn.ReachCapabilityAnnot =>
tp
Expand All @@ -476,9 +479,8 @@ extension (tp: Type)
*/
def readOnly(using Context): CaptureRef = tp match
case tp @ AnnotatedType(tp1: CaptureRef, annot)
if annot.symbol == defn.MaybeCapabilityAnnot
|| annot.symbol == defn.ReachCapabilityAnnot =>
tp.derivedAnnotatedType(tp1.readOnly, annot)
if annot.symbol == defn.MaybeCapabilityAnnot =>
tp1.readOnly.maybe
case tp @ AnnotatedType(tp1: CaptureRef, annot)
if annot.symbol == defn.ReadOnlyCapabilityAnnot =>
tp
Expand Down Expand Up @@ -710,17 +712,23 @@ object CapsOfApply:
case TypeApply(capsOf, arg :: Nil) if capsOf.symbol == defn.Caps_capsOf => Some(arg)
case _ => None

abstract class AnnotatedCapability(annot: Context ?=> ClassSymbol):
abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
def apply(tp: Type)(using Context): AnnotatedType =
assert(tp.isTrackableRef)
tp match
case AnnotatedType(_, annot) => assert(!unwrappable.contains(annot.symbol))
case AnnotatedType(_, annot) =>
assert(!unwrappable.contains(annot.symbol), i"illegal combination of derived capabilities: $annotCls over ${annot.symbol}")
case _ =>
AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
tp match
case tp: CaptureRef => tp.derivedRef(annotCls)
case _ => AnnotatedType(tp, Annotation(annotCls, util.Spans.NoSpan))

def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annot) => Some(parent)
case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annotCls) => Some(parent)
case _ => None

protected def unwrappable(using Context): Set[Symbol]
end AnnotatedCapability

/** An extractor for `ref @maybeCapability`, which is used to express
* the maybe capability `ref?` as a type.
Expand Down
13 changes: 13 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ import Periods.NoRunId
import compiletime.uninitialized
import StdNames.nme
import CaptureSet.VarState
import Annotations.Annotation

/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
Expand All @@ -24,6 +25,18 @@ trait CaptureRef extends TypeProxy, ValueType:
private var myCaptureSet: CaptureSet | Null = uninitialized
private var myCaptureSetRunId: Int = NoRunId
private var mySingletonCaptureSet: CaptureSet.Const | Null = null
private var myDerivedRefs: List[AnnotatedType] = Nil

/** A derived reach, readOnly or maybe reference. Derived references are cached. */
def derivedRef(annotCls: ClassSymbol)(using Context): AnnotatedType =
def recur(refs: List[AnnotatedType]): AnnotatedType = refs match
case ref :: refs1 =>
if ref.annot.symbol == annotCls then ref else recur(refs1)
case Nil =>
val derived = AnnotatedType(this, Annotation(annotCls, util.Spans.NoSpan))
myDerivedRefs = derived :: myDerivedRefs
derived
recur(myDerivedRefs)

/** Is the reference tracked? This is true if it can be tracked and the capture
* set of the underlying type is not always empty.
Expand Down
15 changes: 6 additions & 9 deletions tests/neg-custom-args/captures/i21614.check
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 ---------------------------------------
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
12 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
| ^^^^^^^^^^^^^^^^^^^^^^^
| Found: (f: F) ->{files.rd*} box Logger{val f²: File^?}^?
| Required: (f: box F^{files.rd*}) ->{fresh} box Logger{val f²: File^?}^?
|
| where: f is a reference to a value parameter
| f² is a value in class Logger
| ^
| Found: (f : F)
| Required: File^
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
Expand All @@ -14,7 +11,7 @@
|Found: (_$1: box File^{files*}) ->{files*} (ex$16: caps.Exists) -> box Logger{val f: File^{_$1}}^{ex$16.rd, _$1}
|Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^?
|
|Note that reference ex$16.rd
|cannot be included in outer capture set ?
|Note that the universal capability `cap.rd`
|cannot be included in capture set ?
|
| longer explanation available when compiling with `-explain`
34 changes: 32 additions & 2 deletions tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -56,15 +56,45 @@
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/reaches.scala:79:10 -----------------------------------------------------------
79 | ps.map((x, y) => compose1(x, y)) // error // error
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
| ^
| 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/reaches.scala:79:13 -----------------------------------------------------------
79 | ps.map((x, y) => compose1(x, y)) // error // error
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
| ^
| 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/reaches.scala:79:31 -----------------------------------------------------------
79 | ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
| ^
| Separation failure: argument of type (x$0: A) ->{y} box A^?
| to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
| corresponds to capture-polymorphic formal parameter g of type box A^? => box A^?
| and captures {ps*}, but this capability is also passed separately
| in the first argument with type (x$0: A) ->{x} box A^?.
|
| Capture set of first argument : {x}
| Hidden set of current argument : {y}
| Footprint of first argument : {x, ps*}
| Hidden footprint of current argument : {y, ps*}
| Declared footprint of current argument: {}
| Undeclared overlap of footprints : {ps*}
-- Error: tests/neg-custom-args/captures/reaches.scala:82:31 -----------------------------------------------------------
82 | ps.map((x, y) => compose1(x, y)) // error sepcheck
| ^
| Separation failure: argument of type (x$0: A) ->{y} box A^?
| to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
| corresponds to capture-polymorphic formal parameter g of type box A^? => box A^?
| and captures {ps*}, but this capability is also passed separately
| in the first argument with type (x$0: A) ->{x} box A^?.
|
| Capture set of first argument : {x}
| Hidden set of current argument : {y}
| Footprint of first argument : {x, ps*}
| Hidden footprint of current argument : {y, ps*}
| Declared footprint of current argument: {}
| Undeclared overlap of footprints : {ps*}
-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
61 | val leaked = usingFile[File^{id*}]: f => // error
| ^^^
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ 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
ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck

def mapCompose2[A](@use ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
ps.map((x, y) => compose1(x, y))
ps.map((x, y) => compose1(x, y)) // error sepcheck