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

Closed

WojciechMazur wants to merge 93 commits intorelease-3.7.0from

backport-release-3.7.0-22539

Commits on Apr 10, 2025

Elide capabilities implied by Capability subtypes when printing

odersky
authored and
WojciechMazur
committed
Add Mutable classes and ReadOnly capabilities

odersky
authored and
WojciechMazur
committed
Drop special handling of functions with pure arguments in Existential.toCap

odersky
authored and
WojciechMazur
committed
Implement fresh capabilities
WojciechMazur
committed
Separation checking for applications

odersky
authored and
WojciechMazur
committed
Separation checking for blocks

odersky
authored and
WojciechMazur
committed
Address review comments

odersky
authored and
WojciechMazur
committed
Use deep capturesets for separation checking.

odersky
authored and
WojciechMazur
committed
Cache derived reach, readOnly, and maybe capabilities

odersky
authored and
WojciechMazur
committed
Avoid forming intersections of capture sets on refined type lookup

odersky
authored and
WojciechMazur
committed
Check separation of different parts of a declared type.

odersky
authored and
WojciechMazur
committed
Check that hidden parameters are annotated @consume

odersky
authored and
WojciechMazur
committed
Check that only @consume parameters flow to @consume parameters

odersky
authored and
WojciechMazur
committed
Check that SharedCapabilities don't capture `cap`.

odersky
authored and
WojciechMazur
committed
Turn separation checking on by default

odersky
authored and
WojciechMazur
committed
Make sure fresh results of methods only hide local refs

odersky
authored and
WojciechMazur
committed
Make sure parameters are not used again after they are consumed

odersky
authored and
WojciechMazur
committed
Check accesses to non-local this in hidden sets

odersky
authored and
WojciechMazur
committed
Check that @consumed prefix capabilities are not re-used

odersky
authored and
WojciechMazur
committed
Allow SharableCapablity anywhere on a path

odersky
authored and
WojciechMazur
committed
Polishings

odersky
authored and
WojciechMazur
committed
Polish and document separation checker.

odersky
authored and
WojciechMazur
committed
Address review comments

odersky
authored and
WojciechMazur
committed
Fix handling paths extending SharedCapabiolity

odersky
authored and
WojciechMazur
committed
Streamline deepCaptureSet

odersky
authored and
WojciechMazur
committed
Avoid edge case where non-sensical info was printed for selections

odersky
authored and
WojciechMazur
committed
Make printFresh a -Y option

odersky
authored and
WojciechMazur
committed
Charge deep capture set for arguments to @consume parameters

odersky
authored and
WojciechMazur
committed
Don't flag local fresh capabilities as errors in markFree

odersky
authored and
WojciechMazur
committed
Tweak error message in SepCheck

odersky
authored and
WojciechMazur
committed
Add reach capabilities on the fly in getBoxed

odersky
authored and
WojciechMazur
committed
Revise path handling

odersky
authored and
WojciechMazur
committed
Don't avoid elements of hidden sets

odersky
authored and
WojciechMazur
committed
Shorten transitive hidden sets and replace cycles by aliases

odersky
authored and
WojciechMazur
committed
Use peaks-based checking for applications

odersky
authored and
WojciechMazur
committed
Allow more than one existential per binder.

odersky
authored and
WojciechMazur
committed
Use peaks-based checking for types

odersky
authored and
WojciechMazur
committed
Drop transitive hidden set construction

odersky
authored and
WojciechMazur
committed
Peak-based separation checking for def-use

odersky
authored and
WojciechMazur
committed
More tests

odersky
authored and
WojciechMazur
committed
Fix: Don't add implicit Capability captures to result types of constructors

odersky
authored and
WojciechMazur
committed
Dont apply Fresh.FromCap to inferred types

odersky
authored and
WojciechMazur
committed
Also include nested caps when computing hidden members of a capture set

odersky
authored and
WojciechMazur
committed
Fix soundness problem with curried functions

odersky
authored and
WojciechMazur
committed
Use Fresh(...) instead of Fresh.Cap(...)

odersky
authored and
WojciechMazur
committed
Print cc-generated dependent functions as parametric functions

odersky
authored and
WojciechMazur
committed
Fix resultDependent computation for MethodTypes

odersky
authored and
WojciechMazur
committed
Adopt declared parameter names in comparison

odersky
authored and
WojciechMazur
committed
Make mapping to dependent functions more uniform

odersky
authored and
WojciechMazur
committed
Refactoring: Move normalizeCaptures to SetupTypeMap

odersky
authored and
WojciechMazur
committed
Fix: Avoid double refinements

odersky
authored and
WojciechMazur
committed
Simplify Existential.mapCapInResults

odersky
authored and
WojciechMazur
committed
Some infrastructure for making existentials Fresh instances

odersky
authored and
WojciechMazur
committed
Switch to new scheme for bound caps

odersky
authored and
WojciechMazur
committed
Improve printing of existential Fresh instances

odersky
authored and
WojciechMazur
committed
Improve printing of Fresh in parts of types

odersky
authored and
WojciechMazur
committed
Drop old existential handling

odersky
authored and
WojciechMazur
committed
Drop deep toCap when checking closures

odersky
authored and
WojciechMazur
committed
Drop followResult = true in CaptureSet.ofInfo

odersky
authored and
WojciechMazur
committed
Make `inOpenedFreshBinder` work also if there is no capture checking phase

odersky
authored and
WojciechMazur
committed
Update check files

odersky
authored and
WojciechMazur
committed
Refactoring: Separate addOwnerAsHidden from Fresh creation

odersky
authored and
WojciechMazur
committed
Expand cap arguments of function aliases before de-aliasing

odersky
authored and
WojciechMazur
committed
Always use the sealed policy

odersky
authored and
WojciechMazur
committed
Refactoring: Move Fresh.fromCap into transformExplicitType

odersky
authored and
WojciechMazur
committed
Open existential scopes only for `(x: T) => U` functions

odersky
authored and
WojciechMazur
committed
Tighten subsume rules for existentials

odersky
authored and
WojciechMazur
committed
Tighten existential subsume rules further:

odersky
authored and
WojciechMazur
committed
chore: double the heap size and the stack size

hamzaremmal
authored and
WojciechMazur
committed
Allow whitespace between -> and following capture set

odersky
authored and
WojciechMazur
committed
Make CanThrow a SharedCapability

odersky
authored and
WojciechMazur
committed
Let existential variables only subsume shared capabilities

odersky
authored and
WojciechMazur
committed
Classify existential variables as root capabilities

odersky
authored and
WojciechMazur
committed
Classify existential variables as root capabilities

odersky
authored and
WojciechMazur
committed
Merge `Existential` and `Fresh` into `root` module

odersky
authored and
WojciechMazur
committed
Drop Caps_Exists handling and deprecate caps.Exists

odersky
authored and
WojciechMazur
committed
Small tweaks

odersky
authored and
WojciechMazur
committed
Make `cap` not subsume anything by default.

odersky
authored and
WojciechMazur
committed
Turn off withCapAsRoot exception for box adaptation

odersky
authored and
WojciechMazur
committed
Test case showing that second soundness hole is filled

odersky
authored and
WojciechMazur
committed
Tighten consume checks

odersky
authored and
WojciechMazur
committed
Split posCC from pos tests

odersky
authored and
WojciechMazur
committed
Fine-tune pruning for consume checks of arguments

odersky
authored and
WojciechMazur
committed
Refactor

odersky
authored and
WojciechMazur
committed
Fix compute overlap logic for consumes

odersky
authored and
WojciechMazur
committed
Remove unused files and document root.scala

odersky
authored and
WojciechMazur
committed
Add `mut` modifier to Parser doc comment

odersky
authored and
WojciechMazur
committed
Rename -Ycc-print-fresh to -Ycc-verbose

odersky
authored and
WojciechMazur
committed
Refactor addenda generation

odersky
authored and
WojciechMazur
committed
More refactoring, avoid globally accessible variable

odersky
authored and
WojciechMazur
committed
Fix typo in error message

odersky
authored and
WojciechMazur
committed
Change rules for tracked refinments and tighten intersections

odersky
authored and
WojciechMazur
committed
Fix MimaFilters

odersky
authored and
WojciechMazur
committed