|
| 1 | +abstract type AbstractLattice; end |
| 2 | +function widenlattice end |
| 3 | + |
| 4 | +""" |
| 5 | + struct JLTypeLattice |
| 6 | +
|
| 7 | +A singleton type representing the lattice of Julia types, without any inference |
| 8 | +extensions. |
| 9 | +""" |
| 10 | +struct JLTypeLattice <: AbstractLattice; end |
| 11 | +widenlattice(::JLTypeLattice) = error("Type lattice is the least-precise lattice available") |
| 12 | +is_valid_lattice(::JLTypeLattice, @nospecialize(elem)) = isa(elem, Type) |
| 13 | + |
| 14 | +""" |
| 15 | + struct ConstsLattice |
| 16 | +
|
| 17 | +A lattice extending `JLTypeLattice` and adjoining `Const` and `PartialTypeVar`. |
| 18 | +""" |
| 19 | +struct ConstsLattice <: AbstractLattice; end |
| 20 | +widenlattice(::ConstsLattice) = JLTypeLattice() |
| 21 | +is_valid_lattice(lattice::ConstsLattice, @nospecialize(elem)) = |
| 22 | + is_valid_lattice(widenlattice(lattice), elem) || isa(elem, Const) || isa(elem, PartialTypeVar) |
| 23 | + |
| 24 | +""" |
| 25 | + struct PartialsLattice{L} |
| 26 | +
|
| 27 | +A lattice extending lattice `L` and adjoining `PartialStruct` and `PartialOpaque`. |
| 28 | +""" |
| 29 | +struct PartialsLattice{L <: AbstractLattice} <: AbstractLattice |
| 30 | + parent::L |
| 31 | +end |
| 32 | +widenlattice(L::PartialsLattice) = L.parent |
| 33 | +is_valid_lattice(lattice::PartialsLattice, @nospecialize(elem)) = |
| 34 | + is_valid_lattice(widenlattice(lattice), elem) || |
| 35 | + isa(elem, PartialStruct) || isa(elem, PartialOpaque) |
| 36 | + |
| 37 | +""" |
| 38 | + struct ConditionalsLattice{L} |
| 39 | +
|
| 40 | +A lattice extending lattice `L` and adjoining `Conditional`. |
| 41 | +""" |
| 42 | +struct ConditionalsLattice{L <: AbstractLattice} <: AbstractLattice |
| 43 | + parent::L |
| 44 | +end |
| 45 | +widenlattice(L::ConditionalsLattice) = L.parent |
| 46 | +is_valid_lattice(lattice::ConditionalsLattice, @nospecialize(elem)) = |
| 47 | + is_valid_lattice(widenlattice(lattice), elem) || isa(elem, Conditional) |
| 48 | + |
| 49 | +struct InterConditionalsLattice{L <: AbstractLattice} <: AbstractLattice |
| 50 | + parent::L |
| 51 | +end |
| 52 | +widenlattice(L::InterConditionalsLattice) = L.parent |
| 53 | +is_valid_lattice(lattice::InterConditionalsLattice, @nospecialize(elem)) = |
| 54 | + is_valid_lattice(widenlattice(lattice), elem) || isa(elem, InterConditional) |
| 55 | + |
| 56 | +const AnyConditionalsLattice{L} = Union{ConditionalsLattice{L}, InterConditionalsLattice{L}} |
| 57 | +const BaseInferenceLattice = typeof(ConditionalsLattice(PartialsLattice(ConstsLattice()))) |
| 58 | +const IPOResultLattice = typeof(InterConditionalsLattice(PartialsLattice(ConstsLattice()))) |
| 59 | + |
| 60 | +""" |
| 61 | + struct InferenceLattice{L} |
| 62 | +
|
| 63 | +The full lattice used for abstract interpration during inference. Takes |
| 64 | +a base lattice and adjoins `LimitedAccuracy`. |
| 65 | +""" |
| 66 | +struct InferenceLattice{L} <: AbstractLattice |
| 67 | + parent::L |
| 68 | +end |
| 69 | +widenlattice(L::InferenceLattice) = L.parent |
| 70 | +is_valid_lattice(lattice::InferenceLattice, @nospecialize(elem)) = |
| 71 | + is_valid_lattice(widenlattice(lattice), elem) || isa(elem, LimitedAccuracy) |
| 72 | + |
| 73 | +""" |
| 74 | + struct OptimizerLattice |
| 75 | +
|
| 76 | +The lattice used by the optimizer. Extends |
| 77 | +`BaseInferenceLattice` with `MaybeUndef`. |
| 78 | +""" |
| 79 | +struct OptimizerLattice <: AbstractLattice; end |
| 80 | +widenlattice(L::OptimizerLattice) = BaseInferenceLattice.instance |
| 81 | +is_valid_lattice(lattice::OptimizerLattice, @nospecialize(elem)) = |
| 82 | + is_valid_lattice(widenlattice(lattice), elem) || isa(elem, MaybeUndef) |
| 83 | + |
| 84 | +""" |
| 85 | + tmeet(lattice, a, b::Type) |
| 86 | +
|
| 87 | +Compute the lattice meet of lattice elements `a` and `b` over the lattice |
| 88 | +`lattice`. If `lattice` is `JLTypeLattice`, this is equiavalent to type |
| 89 | +intersection. Note that currently `b` is restricted to being a type (interpreted |
| 90 | +as a lattice element in the JLTypeLattice sub-lattice of `lattice`). |
| 91 | +""" |
| 92 | +function tmeet end |
| 93 | + |
| 94 | +function tmeet(::JLTypeLattice, @nospecialize(a::Type), @nospecialize(b::Type)) |
| 95 | + ti = typeintersect(a, b) |
| 96 | + valid_as_lattice(ti) || return Bottom |
| 97 | + return ti |
| 98 | +end |
| 99 | + |
| 100 | +""" |
| 101 | + tmerge(lattice, a, b) |
| 102 | +
|
| 103 | +Compute a lattice join of elements `a` and `b` over the lattice `lattice`. |
| 104 | +Note that the computed element need not be the least upper bound of `a` and |
| 105 | +`b`, but rather, we impose additional limitations on the complexity of the |
| 106 | +joined element, ideally without losing too much precision in common cases and |
| 107 | +remaining mostly associative and commutative. |
| 108 | +""" |
| 109 | +function tmerge end |
| 110 | + |
| 111 | +""" |
| 112 | + ⊑(lattice, a, b) |
| 113 | +
|
| 114 | +Compute the lattice ordering (i.e. less-than-or-equal) relationship between |
| 115 | +lattice elements `a` and `b` over the lattice `lattice`. If `lattice` is |
| 116 | +`JLTypeLattice`, this is equiavalent to subtyping. |
| 117 | +""" |
| 118 | +function ⊑ end |
| 119 | + |
| 120 | +⊑(::JLTypeLattice, @nospecialize(a::Type), @nospecialize(b::Type)) = a <: b |
| 121 | + |
| 122 | +""" |
| 123 | + ⊏(lattice, a, b) -> Bool |
| 124 | +
|
| 125 | +The strict partial order over the type inference lattice. |
| 126 | +This is defined as the irreflexive kernel of `⊑`. |
| 127 | +""" |
| 128 | +⊏(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = ⊑(lattice, a, b) && !⊑(lattice, b, a) |
| 129 | + |
| 130 | +""" |
| 131 | + ⋤(lattice, a, b) -> Bool |
| 132 | +
|
| 133 | +This order could be used as a slightly more efficient version of the strict order `⊏`, |
| 134 | +where we can safely assume `a ⊑ b` holds. |
| 135 | +""" |
| 136 | +⋤(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = !⊑(lattice, b, a) |
| 137 | + |
| 138 | +""" |
| 139 | + is_lattice_equal(lattice, a, b) -> Bool |
| 140 | +
|
| 141 | +Check if two lattice elements are partial order equivalent. |
| 142 | +This is basically `a ⊑ b && b ⊑ a` but (optionally) with extra performance optimizations. |
| 143 | +""" |
| 144 | +function is_lattice_equal(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) |
| 145 | + a === b && return true |
| 146 | + ⊑(lattice, a, b) && ⊑(lattice, b, a) |
| 147 | +end |
| 148 | + |
| 149 | +""" |
| 150 | + has_nontrivial_const_info(lattice, t) -> Bool |
| 151 | +
|
| 152 | +Determine whether the given lattice element `t` of `lattice` has non-trivial |
| 153 | +constant information that would not be available from the type itself. |
| 154 | +""" |
| 155 | +has_nontrivial_const_info(lattice::AbstractLattice, @nospecialize t) = |
| 156 | + has_nontrivial_const_info(widenlattice(lattice), t) |
| 157 | +has_nontrivial_const_info(::JLTypeLattice, @nospecialize(t)) = false |
| 158 | + |
| 159 | +# Curried versions |
| 160 | +⊑(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⊑(lattice, a, b) |
| 161 | +⊏(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⊏(lattice, a, b) |
| 162 | +⋤(lattice::AbstractLattice) = (@nospecialize(a), @nospecialize(b)) -> ⋤(lattice, a, b) |
| 163 | + |
| 164 | +# Fallbacks for external packages using these methods |
| 165 | +const fallback_lattice = InferenceLattice(BaseInferenceLattice.instance) |
| 166 | +const fallback_ipo_lattice = InferenceLattice(IPOResultLattice.instance) |
| 167 | + |
| 168 | +⊑(@nospecialize(a), @nospecialize(b)) = ⊑(fallback_lattice, a, b) |
| 169 | +tmeet(@nospecialize(a), @nospecialize(b)) = tmeet(fallback_lattice, a, b) |
| 170 | +tmerge(@nospecialize(a), @nospecialize(b)) = tmerge(fallback_lattice, a, b) |
| 171 | +⊏(@nospecialize(a), @nospecialize(b)) = ⊏(fallback_lattice, a, b) |
| 172 | +⋤(@nospecialize(a), @nospecialize(b)) = ⋤(fallback_lattice, a, b) |
| 173 | +is_lattice_equal(@nospecialize(a), @nospecialize(b)) = is_lattice_equal(fallback_lattice, a, b) |
0 commit comments