Module rustc_mir_dataflow::lattice
source · Expand description
Traits used to represent lattices for use as the domain of a dataflow analysis.
Overview
The most common lattice is a powerset of some set S
, ordered by set inclusion. The Hasse
diagram for the powerset of a set with two elements (X
and Y
) is shown below. Note that
distinct elements at the same height in a Hasse diagram (e.g. {X}
and {Y}
) are
incomparable, not equal.
{X, Y} <- top
/ \
{X} {Y}
\ /
{} <- bottom
The defining characteristic of a lattice—the one that differentiates it from a partially
ordered set—is the existence of a unique least upper and greatest lower bound for
every pair of elements. The lattice join operator (∨
) returns the least upper bound, and the
lattice meet operator (∧
) returns the greatest lower bound. Types that implement one operator
but not the other are known as semilattices. Dataflow analysis only uses the join operator and
will work with any join-semilattice, but both should be specified when possible.
PartialOrd
Given that they represent partially ordered sets, you may be surprised that JoinSemiLattice
and MeetSemiLattice
do not have PartialOrd
as a supertrait. This
is because most standard library types use lexicographic ordering instead of set inclusion for
their PartialOrd
impl. Since we do not actually need to compare lattice elements to run a
dataflow analysis, there’s no need for a newtype wrapper with a custom PartialOrd
impl. The
only benefit would be the ability to check that the least upper (or greatest lower) bound
returned by the lattice join (or meet) operator was in fact greater (or lower) than the inputs.
Structs
- The counterpart of a given semilattice
T
using the inverse order.
Enums
- Extends a type
T
with top and bottom elements to make it a partially ordered set in which no value ofT
is comparable with any other. - Extend a lattice with a bottom value to represent an unreachable execution.
Traits
- A set that has a “bottom” element, which is less than or equal to any other element.
- A set that has a “top” element, which is greater than or equal to any other element.
- A partially ordered set that has a least upper bound for any pair of elements in the set.
- A partially ordered set that has a greatest lower bound for any pair of elements in the set.