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
T using the inverse order.Enums
T with top and bottom elements to make it a partially ordered set in which no
value of T is comparable with any other.