Skip to content

Backport "Separation checking for product types" to 3.7.0 #22964

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

Closed
wants to merge 93 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
93 commits
Select commit Hold shift + click to select a range
e29c8d9
Elide capabilities implied by Capability subtypes when printing
odersky Dec 6, 2024
63de12d
Add Mutable classes and ReadOnly capabilities
odersky Jan 10, 2025
8e37a5c
Drop special handling of functions with pure arguments in Existential…
odersky Dec 15, 2024
094a99b
Implement fresh capabilities
WojciechMazur Apr 10, 2025
d218cc4
Separation checking for applications
odersky Jan 11, 2025
8939a08
Separation checking for blocks
odersky Jan 12, 2025
7a714d2
Address review comments
odersky Jan 19, 2025
6b2c624
Use deep capturesets for separation checking.
odersky Jan 20, 2025
ec0bafd
Cache derived reach, readOnly, and maybe capabilities
odersky Jan 20, 2025
e265377
Avoid forming intersections of capture sets on refined type lookup
odersky Jan 21, 2025
485a534
Check separation of different parts of a declared type.
odersky Jan 24, 2025
b106107
Check that hidden parameters are annotated @consume
odersky Jan 25, 2025
83c864c
Check that only @consume parameters flow to @consume parameters
odersky Jan 26, 2025
b83d97a
Check that SharedCapabilities don't capture `cap`.
odersky Jan 26, 2025
654415c
Turn separation checking on by default
odersky Jan 26, 2025
ac1ba8a
Make sure fresh results of methods only hide local refs
odersky Jan 27, 2025
246c27e
Make sure parameters are not used again after they are consumed
odersky Jan 28, 2025
00c94c3
Check accesses to non-local this in hidden sets
odersky Jan 28, 2025
2d2271a
Check that @consumed prefix capabilities are not re-used
odersky Jan 29, 2025
0b67cf8
Allow SharableCapablity anywhere on a path
odersky Jan 30, 2025
0b3187e
Polishings
odersky Jan 31, 2025
ce1477f
Polish and document separation checker.
odersky Feb 1, 2025
04be85a
Address review comments
odersky Feb 5, 2025
fb00530
Fix handling paths extending SharedCapabiolity
odersky Feb 9, 2025
e3b8034
Streamline deepCaptureSet
odersky Feb 9, 2025
9918cf5
Avoid edge case where non-sensical info was printed for selections
odersky Feb 2, 2025
bf10f66
Make printFresh a -Y option
odersky Feb 3, 2025
5c636ae
Charge deep capture set for arguments to @consume parameters
odersky Feb 3, 2025
938afc5
Don't flag local fresh capabilities as errors in markFree
odersky Feb 3, 2025
852a710
Tweak error message in SepCheck
odersky Feb 4, 2025
ddec1ec
Add reach capabilities on the fly in getBoxed
odersky Feb 4, 2025
00e5c64
Revise path handling
odersky Feb 4, 2025
0e6c4b0
Don't avoid elements of hidden sets
odersky Feb 6, 2025
72cdafa
Shorten transitive hidden sets and replace cycles by aliases
odersky Feb 7, 2025
82f25c4
Use peaks-based checking for applications
odersky Feb 11, 2025
73fe2f5
Allow more than one existential per binder.
odersky Feb 13, 2025
b67fc44
Use peaks-based checking for types
odersky Feb 13, 2025
35d4b1f
Drop transitive hidden set construction
odersky Feb 13, 2025
f8271b7
Peak-based separation checking for def-use
odersky Feb 14, 2025
03d1c99
More tests
odersky Feb 16, 2025
9b3e5c3
Fix: Don't add implicit Capability captures to result types of constr…
odersky Feb 19, 2025
8c5311c
Dont apply Fresh.FromCap to inferred types
odersky Feb 19, 2025
2f2ef87
Also include nested caps when computing hidden members of a capture set
odersky Feb 19, 2025
2cdd242
Fix soundness problem with curried functions
odersky Feb 20, 2025
569e8de
Use Fresh(...) instead of Fresh.Cap(...)
odersky Feb 22, 2025
84960c0
Print cc-generated dependent functions as parametric functions
odersky Feb 23, 2025
8e20f6d
Fix resultDependent computation for MethodTypes
odersky Feb 23, 2025
b0bc2c8
Adopt declared parameter names in comparison
odersky Feb 23, 2025
6d19ee0
Make mapping to dependent functions more uniform
odersky Feb 24, 2025
1d74752
Refactoring: Move normalizeCaptures to SetupTypeMap
odersky Feb 24, 2025
adbea87
Fix: Avoid double refinements
odersky Feb 24, 2025
73164e3
Simplify Existential.mapCapInResults
odersky Feb 24, 2025
98494e4
Some infrastructure for making existentials Fresh instances
odersky Feb 24, 2025
1718f85
Switch to new scheme for bound caps
odersky Feb 27, 2025
bc69162
Improve printing of existential Fresh instances
odersky Feb 27, 2025
e86bb06
Improve printing of Fresh in parts of types
odersky Feb 27, 2025
7a52405
Drop old existential handling
odersky Feb 27, 2025
5e0cf9c
Drop deep toCap when checking closures
odersky Feb 27, 2025
f0dc51e
Drop followResult = true in CaptureSet.ofInfo
odersky Feb 27, 2025
fab8e42
Make `inOpenedFreshBinder` work also if there is no capture checking …
odersky Feb 27, 2025
32a8da7
Update check files
odersky Feb 27, 2025
36927c6
Refactoring: Separate addOwnerAsHidden from Fresh creation
odersky Feb 28, 2025
43d832e
Expand cap arguments of function aliases before de-aliasing
odersky Mar 1, 2025
bfce102
Always use the sealed policy
odersky Mar 1, 2025
52cb990
Refactoring: Move Fresh.fromCap into transformExplicitType
odersky Mar 1, 2025
a64dfe9
Open existential scopes only for `(x: T) => U` functions
odersky Mar 3, 2025
dea2b25
Tighten subsume rules for existentials
odersky Mar 4, 2025
f942b69
Tighten existential subsume rules further:
odersky Mar 4, 2025
3fe1c8c
chore: double the heap size and the stack size
hamzaremmal Mar 4, 2025
4be9f6f
Allow whitespace between -> and following capture set
odersky Mar 5, 2025
ab3c8e9
Make CanThrow a SharedCapability
odersky Mar 5, 2025
e472bc9
Let existential variables only subsume shared capabilities
odersky Mar 5, 2025
e09162c
Classify existential variables as root capabilities
odersky Mar 6, 2025
5256587
Classify existential variables as root capabilities
odersky Mar 6, 2025
aeb5b28
Merge `Existential` and `Fresh` into `root` module
odersky Mar 6, 2025
9cfc405
Drop Caps_Exists handling and deprecate caps.Exists
odersky Mar 6, 2025
e0b3711
Small tweaks
odersky Mar 7, 2025
2d3016f
Make `cap` not subsume anything by default.
odersky Mar 7, 2025
a527629
Turn off withCapAsRoot exception for box adaptation
odersky Mar 7, 2025
4d097ac
Test case showing that second soundness hole is filled
odersky Mar 7, 2025
b7c6b35
Tighten consume checks
odersky Mar 8, 2025
c37499e
Split posCC from pos tests
odersky Mar 9, 2025
6e6dfb8
Fine-tune pruning for consume checks of arguments
odersky Mar 9, 2025
462bb0e
Refactor
odersky Mar 9, 2025
22c70e1
Fix compute overlap logic for consumes
odersky Mar 9, 2025
b4fe06f
Remove unused files and document root.scala
odersky Mar 10, 2025
31a539a
Add `mut` modifier to Parser doc comment
odersky Mar 11, 2025
c53b88a
Rename -Ycc-print-fresh to -Ycc-verbose
odersky Mar 11, 2025
990d286
Refactor addenda generation
odersky Mar 12, 2025
312b330
More refactoring, avoid globally accessible variable
odersky Mar 12, 2025
98d1ab0
Fix typo in error message
odersky Mar 13, 2025
b789c22
Change rules for tracked refinments and tighten intersections
odersky Mar 13, 2025
cffd1a2
Fix MimaFilters
odersky Mar 14, 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
4 changes: 2 additions & 2 deletions .jvmopts
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
-Xss1m
-Xms512m
-Xmx4096m
-Xms1024m
-Xmx8192m
-XX:MaxInlineLevel=35
-XX:ReservedCodeCacheSize=512m
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,7 @@ class BTypesFromSymbols[I <: DottyBackendInterface](val int: I, val frontendAcce
// tests/run/serialize.scala and https://github.com/typelevel/cats-effect/pull/2360).
val privateFlag = !sym.isClass && (sym.is(Private) || (sym.isPrimaryConstructor && sym.owner.isTopLevelModuleClass))

val finalFlag = sym.is(Final) && !toDenot(sym).isClassConstructor && !sym.is(Mutable, butNot = Accessor) && !sym.enclosingClass.is(Trait)
val finalFlag = sym.is(Final) && !toDenot(sym).isClassConstructor && !sym.isMutableVar && !sym.enclosingClass.is(Trait)

import asm.Opcodes.*
import GenBCodeOps.addFlagIf
Expand Down
2 changes: 2 additions & 0 deletions compiler/src/dotty/tools/dotc/ast/Desugar.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2262,6 +2262,8 @@ object desugar {
New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
else if op.name == nme.CC_REACH then
Apply(ref(defn.Caps_reachCapability), t :: Nil)
else if op.name == nme.CC_READONLY then
Apply(ref(defn.Caps_readOnlyCapability), t :: Nil)
else
assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
Select(t, op.name)
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
Original file line number Diff line number Diff line change
Expand Up @@ -759,7 +759,7 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
*/
def isVariableOrGetter(tree: Tree)(using Context): Boolean = {
def sym = tree.symbol
def isVar = sym.is(Mutable)
def isVar = sym.isMutableVarOrAccessor
def isGetter =
mayBeVarGetter(sym) && sym.owner.info.member(sym.name.asTermName.setterName).exists

Expand Down
3 changes: 3 additions & 0 deletions compiler/src/dotty/tools/dotc/ast/untpd.scala
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {

case class Var()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Mutable)

case class Mut()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Mutable)

case class Implicit()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Implicit)

case class Given()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Given)
Expand Down Expand Up @@ -332,6 +334,7 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {

def isEnumCase: Boolean = isEnum && is(Case)
def isEnumClass: Boolean = isEnum && !is(Case)
def isMutableVar: Boolean = is(Mutable) && mods.exists(_.isInstanceOf[Mod.Var])
}

@sharable val EmptyModifiers: Modifiers = Modifiers()
Expand Down
3 changes: 2 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
case cr: TermRef => ref(cr)
case cr: TermParamRef => untpd.Ident(cr.paramName).withType(cr)
case cr: ThisType => This(cr.cls)
// TODO: Will crash if the type is an annotated type, for example `cap?`
case root(_) => ref(root.cap)
// TODO: Will crash if the type is an annotated type, for example `cap.rd`
}
val arg = repeated(elems, TypeTree(defn.AnyType))
New(symbol.typeRef, arg :: Nil)
Expand Down
Loading
Loading