Exclusive capabilities #22218
Polishings
- Loading branch information
commit b0628d1e7d08b70bc49f6001db41b3d72f2b8338
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -636,7 +636,8 @@ object CaptureSet: | |
| */ | ||
| def solve()(using Context): Unit = | ||
| if !isConst then | ||
| val approx = upperApprox(empty) | ||
| .map(Fresh.FromCap(NoSymbol).inverse) // Fresh.Cap --> cap | ||
| .showing(i"solve $this = $result", capt) | ||
| //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}") | ||
| val newElems = approx.elems -- elems | ||
|
|
@@ -1139,6 +1140,7 @@ object CaptureSet: | |
|
|
||
| /** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */ | ||
|
There was a problem hiding this comment. Should this not be an There was a problem hiding this comment. It's always one or the other. BiTypeMaps are better for type inference. |
||
| private abstract class NarrowingCapabilityMap(using Context) extends BiTypeMap: | ||
|
|
||
| def mapRef(ref: CaptureRef): CaptureRef | ||
|
|
||
| def apply(t: Type) = t match | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -519,8 +519,7 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| def includeCallCaptures(sym: Symbol, resType: Type, tree: Tree)(using Context): Unit = resType match | ||||||
| case _: MethodOrPoly => // wait until method is fully applied | ||||||
| case _ => | ||||||
| if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), tree) | ||||||
|
|
||||||
| /** Under the sealed policy, disallow the root capability in type arguments. | ||||||
| * Type arguments come either from a TypeApply node or from an AppliedType | ||||||
|
|
@@ -556,16 +555,21 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| if param.isUseParam then markFree(arg.nuType.deepCaptureSet, errTree) | ||||||
| end disallowCapInTypeArgs | ||||||
|
|
||||||
| /** Rechecking idents involves: | ||||||
| * - adding call captures for idents referring to methods | ||||||
| * - marking as free the identifier with any selections or .rd | ||||||
| * modifiers implied by the expected type | ||||||
| */ | ||||||
| override def recheckIdent(tree: Ident, pt: Type)(using Context): Type = | ||||||
| val sym = tree.symbol | ||||||
| if sym.is(Method) then | ||||||
| // If ident refers to a parameterless method, charge its cv to the environment | ||||||
| includeCallCaptures(sym, sym.info, tree) | ||||||
| else if !sym.isStatic then | ||||||
| // Otherwise charge its symbol, but add all selections and also any `.rd` | ||||||
| // modifier implied by the expected type `pt`. | ||||||
| // Example: If we have `x` and the expected type says we select that with `.a.b` | ||||||
| // where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`. | ||||||
| def addSelects(ref: TermRef, pt: Type): CaptureRef = pt match | ||||||
| case pt: PathSelectionProto if ref.isTracked => | ||||||
| if pt.sym.isReadOnlyMethod then | ||||||
|
|
@@ -582,7 +586,8 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| super.recheckIdent(tree, pt) | ||||||
|
|
||||||
| /** The expected type for the qualifier of a selection. If the selection | ||||||
| * could be part of a capability path or is a a read-only method, we return | ||||||
| * a PathSelectionProto. | ||||||
| */ | ||||||
| override def selectionProto(tree: Select, pt: Type)(using Context): Type = | ||||||
| val sym = tree.symbol | ||||||
|
|
@@ -616,6 +621,9 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| } | ||||||
| case _ => denot | ||||||
|
|
||||||
| // Don't allow update methods to be called unless the qualifier captures | ||||||
|
There was a problem hiding this comment.
Suggested change
|
||||||
| // contain an exclusive referenece. TODO This should probabkly rolled into | ||||||
|
There was a problem hiding this comment.
Suggested change
|
||||||
| // qualifier logic once we have it. | ||||||
| if tree.symbol.isUpdateMethod && !qualType.captureSet.isExclusive then | ||||||
| report.error( | ||||||
| em"""cannot call update ${tree.symbol} from $qualType, | ||||||
|
|
@@ -651,8 +659,8 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| selType | ||||||
| }//.showing(i"recheck sel $tree, $qualType = $result") | ||||||
|
|
||||||
| /** Hook for massaging a function before it is applied. Copies all @use and @consume | ||||||
| * annotations on method parameter symbols to the corresponding paramInfo types. | ||||||
| */ | ||||||
| override def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType = | ||||||
| val paramInfosWithUses = | ||||||
|
|
@@ -682,7 +690,8 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| includeCallCaptures(meth, res, tree) | ||||||
| res | ||||||
|
|
||||||
| /** Recheck argument against a "freshened" version of `formal` where toplevel `cap` | ||||||
| * occurrences are replaced by `Fresh.Cap`. Also, if formal parameter carries a `@use`, | ||||||
| * charge the deep capture set of the actual argument to the environment. | ||||||
| */ | ||||||
| protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type = | ||||||
|
|
@@ -773,16 +782,21 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
|
|
||||||
| /** First half of result pair: | ||||||
| * Refine the type of a constructor call `new C(t_1, ..., t_n)` | ||||||
| * to C{val x_1: @refineOverride T_1, ..., x_m: @refineOverride T_m} | ||||||
| * where x_1, ..., x_m are the tracked parameters of C and | ||||||
| * T_1, ..., T_m are the types of the corresponding arguments. The @refineOveride | ||||||
| * annotations avoid problematic intersections of capture sets when those | ||||||
| * parameters are selected. | ||||||
| * | ||||||
| * Second half: union of initial capture set and all capture sets of arguments | ||||||
| * to tracked parameters. The initial capture set `initCs` is augmented with | ||||||
| * - Fresh.Cap if `core` extends Mutable | ||||||
| * - Fresh.Cap.rd if `core` extends Capability | ||||||
| */ | ||||||
| def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = | ||||||
| var refined: Type = core | ||||||
| var allCaptures: CaptureSet = | ||||||
| if core.derivesFromMutable then initCs ++ CaptureSet.fresh() | ||||||
| else if core.derivesFromCapability then initCs ++ Fresh.Cap().readOnly.singletonCaptureSet | ||||||
| else initCs | ||||||
| for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do | ||||||
|
|
@@ -1488,7 +1502,7 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| /** If actual is a capturing type T^C extending Mutable, and expected is an | ||||||
| * unboxed non-singleton value type not extending mutable, narrow the capture | ||||||
| * set `C` to `ro(C)`. | ||||||
| * The unboxed condition ensures that the expected type is not a type variable | ||||||
| * that's upper bounded by a read-only type. In this case it would not be sound | ||||||
| * to narrow to the read-only set, since that set can be propagated | ||||||
| * by the type variable instantiation. | ||||||
|
|
@@ -1514,9 +1528,9 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
| actual | ||||||
| else | ||||||
| val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual) | ||||||
| val improved = improveReadOnly(improvedVAR, expected) | ||||||
| val adapted = adaptBoxed( | ||||||
| improved.withReachCaptures(actual), expected, tree, | ||||||
| covariant = true, alwaysConst = false, boxErrors) | ||||||
| if adapted eq improvedVAR // no .rd improvement, no box-adaptation | ||||||
| then actual // might as well use actual instead of improved widened | ||||||
|
|
@@ -1563,17 +1577,19 @@ class CheckCaptures extends Recheck, SymTransformer: | |||||
|
|
||||||
| /** Check that overrides don't change the @use or @consume status of their parameters */ | ||||||
| override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit = | ||||||
| for | ||||||
| (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss) | ||||||
| (param1, param2) <- params1.lazyZip(params2) | ||||||
| do | ||||||
| def checkAnnot(cls: ClassSymbol) = | ||||||
| if param1.hasAnnotation(cls) != param2.hasAnnotation(cls) then | ||||||
| report.error( | ||||||
| OverrideError( | ||||||
| i"has a parameter ${param1.name} with different @${cls.name} status than the corresponding parameter in the overridden definition", | ||||||
| self, member, other, self.memberInfo(member), self.memberInfo(other) | ||||||
| ), | ||||||
| if member.owner == clazz then member.srcPos else clazz.srcPos) | ||||||
|
|
||||||
| checkAnnot(defn.UseAnnot) | ||||||
| checkAnnot(defn.ConsumeAnnot) | ||||||
| end OverridingPairsCheckerCC | ||||||
|
|
||||||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -252,7 +252,7 @@ object Existential: | |
| tp1.derivedAnnotatedType(toCap(parent), ann) | ||
| case _ => tp | ||
|
|
||
| /** Map existentials at the top-level and in all nested result types to `Fresh.Cap` | ||
| */ | ||
| def toCapDeeply(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match | ||
| case Existential(boundVar, unpacked) => | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -16,11 +16,16 @@ import util.SimpleIdentitySet.empty | |
| import CaptureSet.{Refs, emptySet, NarrowingCapabilityMap} | ||
| import dotty.tools.dotc.util.SimpleIdentitySet | ||
|
|
||
| /** A module for handling Fresh types. Fresh.Cap instances are top type that keep | ||
| * track of what they hide when capabilities get widened by subsumption to fresh. | ||
| * The module implements operations to convert between regular caps.cap and | ||
| * Fresh.Cap instances. Fresh.Cap is encoded as `caps.cap @freshCapability(...)` where | ||
| * `freshCapability(...)` is a special kind of annotation of type `Fresh.Annot` | ||
| * that contains a hidden set. | ||
| */ | ||
| object Fresh: | ||
|
|
||
| /** The annotation of a Fresh.Cap instance */ | ||
| case class Annot(hidden: CaptureSet.HiddenSet) extends Annotation: | ||
| override def symbol(using Context) = defn.FreshCapabilityAnnot | ||
| override def tree(using Context) = New(symbol.typeRef, Nil) | ||
|
|
@@ -32,13 +37,17 @@ object Fresh: | |
| case _ => false | ||
| end Annot | ||
|
|
||
| /** The initial elements (either 0 or 1) of a hidden set created for given `owner`. | ||
| * If owner `x` is a trackable this is `x*` if reach` is true, or `x` otherwise. | ||
| */ | ||
| private def ownerToHidden(owner: Symbol, reach: Boolean)(using Context): Refs = | ||
| val ref = owner.termRef | ||
| if reach then | ||
| if ref.isTrackableRef then SimpleIdentitySet(ref.reach) else emptySet | ||
| else | ||
| if ref.isTracked then SimpleIdentitySet(ref) else emptySet | ||
|
|
||
| /** An extractor for "fresh" capabilities */ | ||
| object Cap: | ||
|
|
||
| def apply(initialHidden: Refs = emptySet)(using Context): CaptureRef = | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -411,7 +411,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: | |
| def currentOwner = role.dclSym.orElse(ctx.owner) | ||
| for hiddenRef <- prune(refsToCheck, tpe, role) do | ||
| val proot = hiddenRef.pathRootOrShared | ||
| if !proot.widen.derivesFromSharedCapability then | ||
| proot match | ||
| case ref: TermRef => | ||
| val refSym = ref.symbol | ||
|
|
@@ -448,7 +448,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: | |
| role match | ||
| case _: TypeRole.Argument | _: TypeRole.Qualifier => | ||
| for ref <- refsToCheck do | ||
| if !ref.pathRootOrShared.derivesFromSharedCapability then | ||
| consumed.put(ref, pos) | ||
| case _ => | ||
| end checkConsumedRefs | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -345,10 +345,18 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: | |
| parent | ||
| case _ => tp | ||
|
|
||
| /** Check that types extending SharedCapability don't have a `cap` in their capture set. | ||
| * TODO This is not enough. | ||
| * We need to also track that we cannot get exclusive capabilities in paths | ||
| * where some prefix derives from SharedCapability. Also, can we just | ||
| * exclude `cap`, or do we have to extend this to all exclusive capabilties? | ||
| * The problem is that we know what is exclusive in general only after capture | ||
| * checking, not before. | ||
| */ | ||
| def checkSharedOK(tp: Type): tp.type = | ||
| tp match | ||
| case CapturingType(parent, refs) | ||
| if refs.isUniversal && parent.derivesFromSharedCapability => | ||
| fail(em"$tp extends SharedCapability, so it cannot capture `cap`") | ||
| case _ => | ||
| tp | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -1115,8 +1115,6 @@ class Definitions { | |
| @tu lazy val SilentAnnots: Set[Symbol] = | ||
| Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot) | ||
|
|
||
| // A list of annotations that are commonly used to indicate that a field/method argument or return | ||
| // type is not null. These annotations are used by the nullification logic in JavaNullInterop to | ||
| // improve the precision of type nullification. | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -606,7 +606,7 @@ object Checking { | |
| if sym.isWrappedToplevelDef && !sym.isType && sym.flags.is(Infix, butNot = Extension) then | ||
| fail(ModifierNotAllowedForDefinition(Flags.Infix, s"A top-level ${sym.showKind} cannot be infix.")) | ||
| if sym.isUpdateMethod && !sym.owner.derivesFrom(defn.Caps_Mutable) then | ||
| fail(em"Update methods can only be used as members of classes extending the `Mutable` trait") | ||
| checkApplicable(Erased, | ||
| !sym.is(Lazy, butNot = Given) | ||
| && !sym.isMutableVarOrAccessor | ||
|
|
||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.