Skip to content
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

Separation checking for product types #22539

Merged
merged 93 commits into from
Mar 14, 2025
Merged
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
103ef96
Elide capabilities implied by Capability subtypes when printing
odersky Dec 6, 2024
748f4a6
Add Mutable classes and ReadOnly capabilities
odersky Jan 10, 2025
e4cc265
Drop special handling of functions with pure arguments in Existential…
odersky Dec 15, 2024
ad11819
Implement fresh capabilities
odersky Jan 11, 2025
4c8a50f
Separation checking for applications
odersky Jan 11, 2025
b0c9b3d
Separation checking for blocks
odersky Jan 12, 2025
70074c4
Address review comments
odersky Jan 19, 2025
190aaca
Use deep capturesets for separation checking.
odersky Jan 20, 2025
67d42bd
Cache derived reach, readOnly, and maybe capabilities
odersky Jan 20, 2025
b1da91a
Avoid forming intersections of capture sets on refined type lookup
odersky Jan 21, 2025
131f070
Check separation of different parts of a declared type.
odersky Jan 24, 2025
3adf4b0
Check that hidden parameters are annotated @consume
odersky Jan 25, 2025
ee23239
Check that only @consume parameters flow to @consume parameters
odersky Jan 26, 2025
a4df033
Check that SharedCapabilities don't capture `cap`.
odersky Jan 26, 2025
52dc9b4
Turn separation checking on by default
odersky Jan 26, 2025
824dd83
Make sure fresh results of methods only hide local refs
odersky Jan 27, 2025
7b0b80b
Make sure parameters are not used again after they are consumed
odersky Jan 28, 2025
66fc880
Check accesses to non-local this in hidden sets
odersky Jan 28, 2025
821e17a
Check that @consumed prefix capabilities are not re-used
odersky Jan 29, 2025
3ed82a3
Allow SharableCapablity anywhere on a path
odersky Jan 30, 2025
2d37938
Polishings
odersky Jan 31, 2025
d661678
Polish and document separation checker.
odersky Feb 1, 2025
9710872
Address review comments
odersky Feb 5, 2025
367f66c
Fix handling paths extending SharedCapabiolity
odersky Feb 9, 2025
51050f9
Streamline deepCaptureSet
odersky Feb 9, 2025
f0e0117
Avoid edge case where non-sensical info was printed for selections
odersky Feb 2, 2025
8d15e88
Make printFresh a -Y option
odersky Feb 3, 2025
5132d55
Charge deep capture set for arguments to @consume parameters
odersky Feb 3, 2025
21a5399
Don't flag local fresh capabilities as errors in markFree
odersky Feb 3, 2025
91eef32
Tweak error message in SepCheck
odersky Feb 4, 2025
cf48a6c
Add reach capabilities on the fly in getBoxed
odersky Feb 4, 2025
b4ff2fa
Revise path handling
odersky Feb 4, 2025
e2f44e4
Don't avoid elements of hidden sets
odersky Feb 6, 2025
4d04d35
Shorten transitive hidden sets and replace cycles by aliases
odersky Feb 7, 2025
f761183
Use peaks-based checking for applications
odersky Feb 11, 2025
20df57b
Allow more than one existential per binder.
odersky Feb 13, 2025
b115ff6
Use peaks-based checking for types
odersky Feb 13, 2025
c049774
Drop transitive hidden set construction
odersky Feb 13, 2025
81491f0
Peak-based separation checking for def-use
odersky Feb 14, 2025
6bb7cdc
More tests
odersky Feb 16, 2025
a870eff
Fix: Don't add implicit Capability captures to result types of constr…
odersky Feb 19, 2025
117d5e3
Dont apply Fresh.FromCap to inferred types
odersky Feb 19, 2025
72bf9c6
Also include nested caps when computing hidden members of a capture set
odersky Feb 19, 2025
1430a20
Fix soundness problem with curried functions
odersky Feb 20, 2025
e943c1c
Use Fresh(...) instead of Fresh.Cap(...)
odersky Feb 22, 2025
38d5177
Print cc-generated dependent functions as parametric functions
odersky Feb 23, 2025
2c07372
Fix resultDependent computation for MethodTypes
odersky Feb 23, 2025
263f1ba
Adopt declared parameter names in comparison
odersky Feb 23, 2025
4f348a7
Make mapping to dependent functions more uniform
odersky Feb 24, 2025
5b6533f
Refactoring: Move normalizeCaptures to SetupTypeMap
odersky Feb 24, 2025
8f07594
Fix: Avoid double refinements
odersky Feb 24, 2025
64d99c5
Simplify Existential.mapCapInResults
odersky Feb 24, 2025
3bd4bda
Some infrastructure for making existentials Fresh instances
odersky Feb 24, 2025
ea5a9d5
Switch to new scheme for bound caps
odersky Feb 27, 2025
449d409
Improve printing of existential Fresh instances
odersky Feb 27, 2025
2b264cf
Improve printing of Fresh in parts of types
odersky Feb 27, 2025
a10ce6f
Drop old existential handling
odersky Feb 27, 2025
fc8425b
Drop deep toCap when checking closures
odersky Feb 27, 2025
0e0388e
Drop followResult = true in CaptureSet.ofInfo
odersky Feb 27, 2025
60eb732
Make `inOpenedFreshBinder` work also if there is no capture checking …
odersky Feb 27, 2025
3c9545f
Update check files
odersky Feb 27, 2025
8e67d6c
Refactoring: Separate addOwnerAsHidden from Fresh creation
odersky Feb 28, 2025
aa06e07
Expand cap arguments of function aliases before de-aliasing
odersky Mar 1, 2025
4e6b82e
Always use the sealed policy
odersky Mar 1, 2025
0f0a5b3
Refactoring: Move Fresh.fromCap into transformExplicitType
odersky Mar 1, 2025
30971b5
Open existential scopes only for `(x: T) => U` functions
odersky Mar 3, 2025
b17ef26
Tighten subsume rules for existentials
odersky Mar 4, 2025
d2d529e
Tighten existential subsume rules further:
odersky Mar 4, 2025
f3ef42b
chore: double the heap size and the stack size
hamzaremmal Mar 4, 2025
4c53fd1
Allow whitespace between -> and following capture set
odersky Mar 5, 2025
641dffa
Make CanThrow a SharedCapability
odersky Mar 5, 2025
58baf53
Let existential variables only subsume shared capabilities
odersky Mar 5, 2025
33ef293
Classify existential variables as root capabilities
odersky Mar 6, 2025
12047d8
Classify existential variables as root capabilities
odersky Mar 6, 2025
399b220
Merge `Existential` and `Fresh` into `root` module
odersky Mar 6, 2025
6093dab
Drop Caps_Exists handling and deprecate caps.Exists
odersky Mar 6, 2025
f7484ce
Small tweaks
odersky Mar 7, 2025
d27f2bb
Make `cap` not subsume anything by default.
odersky Mar 7, 2025
ec8d119
Turn off withCapAsRoot exception for box adaptation
odersky Mar 7, 2025
731c9aa
Test case showing that second soundness hole is filled
odersky Mar 7, 2025
d89138a
Tighten consume checks
odersky Mar 8, 2025
a6f1ab2
Split posCC from pos tests
odersky Mar 9, 2025
d2e276c
Fine-tune pruning for consume checks of arguments
odersky Mar 9, 2025
f547582
Refactor
odersky Mar 9, 2025
ee60b21
Fix compute overlap logic for consumes
odersky Mar 9, 2025
c790007
Remove unused files and document root.scala
odersky Mar 10, 2025
9a49c52
Add `mut` modifier to Parser doc comment
odersky Mar 11, 2025
d781b3e
Rename -Ycc-print-fresh to -Ycc-verbose
odersky Mar 11, 2025
dc0dd7f
Refactor addenda generation
odersky Mar 12, 2025
fbe37b8
More refactoring, avoid globally accessible variable
odersky Mar 12, 2025
ac84d13
Fix typo in error message
odersky Mar 13, 2025
23cb1f3
Change rules for tracked refinments and tighten intersections
odersky Mar 13, 2025
48a52a2
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