New capture escape checking based on levels #18463
Merged
Conversation
This file contains 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
odersky
force-pushed
the
add-root-levels
branch
from
544e0c9 to
5274665
Compare
odersky
force-pushed
the
add-root-levels
branch
from
3b8fe9c to
bd8136d
Compare
This was overlooked before.
There was a corner case in installAfter where
- A denotation valid in a single phase got replaced by another one
- Immediately after, the symbol's denotation would be forced in a previous phase
This somehow landed on a wrong denotation. The problem got apparent when more symbols
underwent a Recheck.updateInfoBetween. The flags field installed by a previous update
somehow was not recognized anymore. Specifically, the following was observed in order:
1. For a parameter getter (xs in LazyList, file pos-custeom-args/captures/lazylists1.scala)
the Private flag was suppressed via transformInfo at phase cc.
2. The denotation of the getter v which was valid in the single phase cc+1 was updated at
at cc by updateInfoInBetween in Recheck so that the Private flag was re-asserted in cc+1.
3. Immediately afterwards, the getter's flags was demanded at phase cc.
4. The Private flag was present, even though it should not be.
The problem was fixed by demanding the denotation of the getter as part of isntallAfter.
Constrain closure parameters and result from expected type before rechecking the closure's body. This gives more precise types and avoids the spurious duplication of some variables. It also avoids the unmotivated special case that we needed before to make tests pass.
Previously, the result of a map could contain duplicates. I verified that with the current code base this could cause problems only for capture checking.
This reduces the chance of information loss in capture set propagation for applications.
Currently not needed (was needed for level checking in other branch), but kept since it is a useful generalization.
These changes were needed if we wanted to map all capability classes C to C^. They are a good idea anyway since they make the mapping more robust.
- Define a notion of ccNestingLevel, which corresponds to the nesting level of so called "level owners" relative to each other. - The outermost level owner is _root_. - Other level owners are classes that are not staticOwners and methods that are not constructors. - The ccNestingLevel of any symbol is the ccNestingLevel of its closest enclosing level owner, or -1 for NoSymbol. - Capture set variables are created with a level owner. - Capture set variables cannot include elements with higher ccNestingLevels than the variable's owner. - If level-incorrect elements are attempted to be added to a capture set variable, they are instead widened to the underlying capture set. - Use addenda mechanism to report level errors
Previously, the ccState property was missing on the context used for printing at phase cc.
Intended as a stop-gap for some (as-seen-from related?) problems when comparing capture refinements of classes.
Replaces previous unsound rule where `cap` subsumes everything.
Linyxus
requested changes
Sep 4, 2023
Comment on lines
466
to
467
| // infos other methods are determined from their definitions which | ||
| // are checked on depand |
There was a problem hiding this comment.
Suggested change
| // infos other methods are determined from their definitions which | |
| // are checked on depand | |
| // infos of other methods are determined from their definitions which | |
| // are checked on demand |
| val y1 = f(x1.asInstanceOf[Elem]) | ||
| val y2 = f(x2.asInstanceOf[Elem]) | ||
| if (y0 ne y1) && (y0 ne y2) && (y1 ne y2) then Set3(y0, y1, y2) | ||
| else super.map(f) |
There was a problem hiding this comment.
This results in computing f again over each element, maybe:
Suggested change
| else super.map(f) | |
| else Set(y0, y1, y2) |
| recur(to, from) | ||
| case _ => | ||
| mapOver(t) | ||
| def inverse = thisMap |
There was a problem hiding this comment.
Is it a typo? It seems that the lazyval inverse should be returned here.
There was a problem hiding this comment.
No, the inverse of the inverse is thisMap .
There was a problem hiding this comment.
Ah, yes, sorry for the false alarm.
| mapOverFollowingAliases(t) | ||
|
|
||
| private def transformExplicitType(tp: Type, boxed: Boolean, mapRoots: Boolean)(using Context): Type = | ||
| val tp1 = expandAliases(if boxed then box(tp) else tp) |
There was a problem hiding this comment.
It seems better to first expandAliases (or, at least, expandCapabilityClass) then box the type. Say, if we are transforming an explicit mention of a capability class (say, IO) in a type application, the correct outcome should be box IO^. The box should be there because the capability class is impure. Right now this isn't happening: the output is simply IO^. This is because we are boxing it before expanding, so the original IO isn't recognized as something to be boxed.
I found an unsound example which hides the usage of a capability:
@capability class CanIO { def use(): Unit = () }
def use[X](x: X): (op: X -> Unit) -> Unit = op => op(x)
def test(io: CanIO): Unit =
val f = use[CanIO](io)
val g: () -> Unit = () => f(x => x.use())
// UNSOUND: g uses the capability io but has an empty capture set| end isEnclosingRoot | ||
| end CaptureRoot | ||
|
|
||
| //class LevelError(val rvar: RootVar, val newBound: Symbol, val isUpper: Boolean) extends Exception |
There was a problem hiding this comment.
LevelError doesn't seem to be used any more. Is the comment intentionally kept?
| else false | ||
|
|
||
| /** The owner of the current level. Qualifying owners are | ||
| * - methods other than constructors and anonymous functions |
There was a problem hiding this comment.
Suggested change
| * - methods other than constructors and anonymous functions | |
| * - methods other than constructors, anonymous functions, and synthetic case class accessors |
Comment on lines
827
to
832
| /** An extractor for eta expanded `mdef` an eta-expansion of a method reference? To recognize this, we use | ||
| * the following criterion: A method definition is an eta expansion, if | ||
| * it contains at least one term paramter, the parameter has a zero extent span, | ||
| * and the right hand side is either an application or a closure with' | ||
| * an anonymous method that's itself characterized as an eta expansion. | ||
| */ |
There was a problem hiding this comment.
Suggested change
| /** An extractor for eta expanded `mdef` an eta-expansion of a method reference? To recognize this, we use | |
| * the following criterion: A method definition is an eta expansion, if | |
| * it contains at least one term paramter, the parameter has a zero extent span, | |
| * and the right hand side is either an application or a closure with' | |
| * an anonymous method that's itself characterized as an eta expansion. | |
| */ | |
| /** An extractor for eta expanded `mdef` or an eta-expansion of a method reference. To recognize this, we use | |
| * the following criterion: A method definition is an eta expansion, if | |
| * it contains at least one term paramter, the parameter has a zero extent span, | |
| * and the right hand side is either an application or a closure with | |
| * an anonymous method that's itself characterized as an eta expansion. | |
| */ |
odersky
force-pushed
the
add-root-levels
branch
from
9ab1a70 to
e8b8491
Compare
Linyxus
approved these changes
Sep 5, 2023
Some refined function types are of the form
(A->B)^{cs} { def apply(x: A): B' = ... }
In this case the capture set `cs` was previously dropped. Now it is printed.
Do it in setup instead of on demand. Advantage: no need to determine level ownership for externally compiled symbols.
WojciechMazur
added a commit
to WojciechMazur/dotty
that referenced
this pull request
May 29, 2024
…from opaque type to class in scala#18463
WojciechMazur
added a commit
to WojciechMazur/dotty
that referenced
this pull request
Jun 14, 2024
…from opaque type to class in scala#18463
WojciechMazur
added a commit
to WojciechMazur/dotty
that referenced
this pull request
Jun 14, 2024
…from opaque type to class in scala#18463
WojciechMazur
added a commit
that referenced
this pull request
Jun 17, 2024
…from opaque type to class in #18463
WojciechMazur
added a commit
to WojciechMazur/dotty
that referenced
this pull request
Jul 10, 2024
…from opaque type to class in scala#18463
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
A new scope restriction scheme for capture checking based on levels.
The idea is to have a stack of capture roots where inner capture roots are super-captures of outer roots.
Refines and supersedes #18348