-
-
Notifications
You must be signed in to change notification settings - Fork 5.5k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Refactor lattice code to expose layering and enable easy extension
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
- Loading branch information
Showing
13 changed files
with
374 additions
and
158 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,160 @@ | ||
| abstract type AbstractLattice; end | ||
| function widen end | ||
|
|
||
| """ | ||
| struct JLTypeLattice | ||
| A singleton type representing the lattice of Julia types, without any inference | ||
| extensions. | ||
| """ | ||
| struct JLTypeLattice <: AbstractLattice; end | ||
| widen(::JLTypeLattice) = error("Type lattice is the least-precise lattice available") | ||
| is_valid_lattice(::JLTypeLattice, @nospecialize(elem)) = isa(elem, Type) | ||
|
|
||
| """ | ||
| struct ConstsLattice | ||
| A lattice extending `JLTypeLattice` and adjoining `Const` and `PartialTypeVar`. | ||
| """ | ||
| struct ConstsLattice <: AbstractLattice; end | ||
| widen(::ConstsLattice) = JLTypeLattice() | ||
| is_valid_lattice(lattice::ConstsLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || isa(elem, Const) || isa(elem, PartialTypeVar) | ||
|
|
||
| """ | ||
| struct PartialsLattice{L} | ||
| A lattice extending lattice `L` and adjoining `PartialStruct` and `PartialOpaque`. | ||
| """ | ||
| struct PartialsLattice{L <: AbstractLattice} <: AbstractLattice | ||
| parent::L | ||
| end | ||
| widen(L::PartialsLattice) = L.parent | ||
| is_valid_lattice(lattice::PartialsLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || | ||
| isa(elem, PartialStruct) || isa(elem, PartialOpaque) | ||
|
|
||
| """ | ||
| struct ConditionalsLattice{L} | ||
| A lattice extending lattice `L` and adjoining `Conditional`. | ||
| """ | ||
| struct ConditionalsLattice{L <: AbstractLattice} <: AbstractLattice | ||
| parent::L | ||
| end | ||
| widen(L::ConditionalsLattice) = L.parent | ||
| is_valid_lattice(lattice::ConditionalsLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || isa(elem, Conditional) | ||
|
|
||
| struct InterConditionalsLattice{L <: AbstractLattice} <: AbstractLattice | ||
| parent::L | ||
| end | ||
| widen(L::InterConditionalsLattice) = L.parent | ||
| is_valid_lattice(lattice::InterConditionalsLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || isa(elem, InterConditional) | ||
|
|
||
| const AnyConditionalsLattice{L} = Union{ConditionalsLattice{L}, InterConditionalsLattice{L}} | ||
| const BaseInferenceLattice = typeof(ConditionalsLattice(PartialsLattice(ConstsLattice()))) | ||
| const IPOResultLattice = typeof(InterConditionalsLattice(PartialsLattice(ConstsLattice()))) | ||
|
|
||
| """ | ||
| struct OptimizerLattice | ||
| The lattice used by the optimizer. Extends | ||
| `BaseInferenceLattice` with `MaybeUndef`. | ||
| """ | ||
| struct OptimizerLattice <: AbstractLattice; end | ||
| widen(L::OptimizerLattice) = BaseInferenceLattice.instance | ||
| is_valid_lattice(lattice::OptimizerLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || isa(elem, MaybeUndef) | ||
|
|
||
| """ | ||
| struct InferenceLattice{L} | ||
| The full lattice used for abstract interpration during inference. Takes | ||
| a base lattice and adjoins `LimitedAccuracy`. | ||
| """ | ||
| struct InferenceLattice{L} <: AbstractLattice | ||
| parent::L | ||
| end | ||
| widen(L::InferenceLattice) = L.parent | ||
| is_valid_lattice(lattice::InferenceLattice, @nospecialize(elem)) = | ||
| is_valid_lattice(widen(lattice), elem) || isa(elem, LimitedAccuracy) | ||
|
|
||
| """ | ||
| tmeet(lattice, a, b::Type) | ||
| Compute the lattice meet of lattice elements `a` and `b` over the lattice | ||
| `lattice`. If `lattice` is `JLTypeLattice`, this is equiavalent to type | ||
| intersection. Note that currently `b` is restricted to being a type (interpreted | ||
| as a lattice element in the JLTypeLattice sub-lattice of `lattice`). | ||
| """ | ||
| function tmeet end | ||
|
|
||
| """ | ||
| tmerge(lattice, a, b) | ||
| Compute a lattice join of elements `a` and `b` over the lattice `lattice`. | ||
| Note that the computed element need not be the least upper bound of `a` and | ||
| `b`, but rather, we impose some heuristic limits on the complexity of the | ||
| joined element, ideally without losing too much precision in common cases and | ||
| remaining mostly associative and commutative. | ||
| """ | ||
| function tmerge end | ||
|
|
||
| """ | ||
| ⊑(lattice, a, b) | ||
| Compute the lattice ordering (i.e. less-than-or-equal) relationship between | ||
| lattice elements `a` and `b` over the lattice `lattice`. If `lattice` is | ||
| `JLTypeLattice`, this is equiavalent to subtyping. | ||
| """ | ||
| function ⊑ end | ||
|
|
||
| function ⊑(::JLTypeLattice, @nospecialize(a::Type), @nospecialize(b::Type)) | ||
| a <: b | ||
| end | ||
|
|
||
|
|
||
| """ | ||
| ⊏(lattice, a, b) -> Bool | ||
| The strict partial order over the type inference lattice. | ||
| This is defined as the irreflexive kernel of `⊑`. | ||
| """ | ||
| ⊏(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = ⊑(lattice, a, b) && !⊑(lattice, b, a) | ||
|
|
||
| """ | ||
| ⋤(lattice, a, b) -> Bool | ||
| This order could be used as a slightly more efficient version of the strict order `⊏`, | ||
| where we can safely assume `a ⊑ b` holds. | ||
| """ | ||
| ⋤(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = !⊑(lattice, b, a) | ||
|
|
||
| """ | ||
| is_lattice_equal(a, b) -> Bool | ||
| Check if two lattice elements are partial order equivalent. | ||
| This is basically `a ⊑ b && b ⊑ a` but (optionally) with extra performance optimizations. | ||
| """ | ||
| function is_lattice_equal(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) | ||
| a === b && return true | ||
| ⊑(lattice, a, b) && ⊑(lattice, b, a) | ||
| end | ||
|
|
||
| # Curried versions | ||
| ⊑(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⊑(lattice, a, b) | ||
| ⊏(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⊏(lattice, a, b) | ||
| ⋤(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⋤(lattice, a, b) | ||
|
|
||
| # Fallbacks for external packages using these methods | ||
| const fallback_lattice = InferenceLattice(BaseInferenceLattice.instance) | ||
| const fallback_ipo_lattice = InferenceLattice(IPOResultLattice.instance) | ||
|
|
||
| ⊑(@nospecialize(a), @nospecialize(b)) = ⊑(fallback_lattice, a, b) | ||
| tmeet(@nospecialize(a), @nospecialize(b)) = tmeet(fallback_lattice, a, b) | ||
| tmerge(@nospecialize(a), @nospecialize(b)) = tmerge(fallback_lattice, a, b) | ||
| ⊏(@nospecialize(a), @nospecialize(b)) = ⊏(fallback_lattice, a, b) | ||
| ⋤(@nospecialize(a), @nospecialize(b)) = ⋤(fallback_lattice, a, b) | ||
| is_lattice_equal(@nospecialize(a), @nospecialize(b)) = is_lattice_equal(fallback_lattice, a, b) |
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
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
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
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
Oops, something went wrong.