Lesson 14.1 — Lattices and fixed points¶

Techniques: partial orders, lattices and complete lattices with their standard constructions (powerset, product, map, flat); monotone and distributive functions; the Knaster–Tarski fixed-point theorem; Kleene iteration · Pebble implements: the lattice interface of the generic solver (pebble/include/pebble/Analysis/Dataflow.h, exercise E1) · Lab: — (drills lattice-props, widening) · Prerequisites: Ch 8 (CFGs), sets and functions · Time: 4–6 hours

Every analysis in this chapter answers a question like "which variables may be read later?" by solving a system of equations whose unknowns are sets of facts, one per program point. Take the loop

int x = 1;
for (int i = 0; i < n; i++)
  if (x != 1)
    x = 2;
return x;

At the loop head, \(x\) is whatever entered (\(1\)) joined with whatever the body produced. If the body never runs its if, the body produces \(x\) unchanged, so the equation is \(x_{\mathrm{head}} = 1 \sqcup x_{\mathrm{head}}\). Both "\(x\) is always 1" and "\(x\) is unknown" satisfy that equation. Which answer is right, why does a solver find one and not the other, and why does it stop at all? This lesson gives the order-theoretic answers the rest of the chapter uses: facts form a lattice, equations are monotone functions, and the answer we want is a least fixed point, which Kleene iteration computes.

1. Problem and motivation¶

A dataflow analysis assigns to every program point an abstract value that summarizes all executions reaching that point. Two things make this well defined. First, abstract values must be comparable ("this summary is more precise than that one") and combinable where control flow merges ("what is true after either branch?"). Second, the equations relating program points are recursive through loops, so we need a theorem saying they have a solution, and an algorithm computing it.

Complete lattices and constructions¶

Partial orders and lattices come from algebra (Birkhoff's Lattice Theory, 1940). Kildall's 1973 paper that founded iterative dataflow analysis [Kil73] already used a meet semilattice of "pools" of facts; Kam and Ullman made the lattice conditions precise [KU77], and the Cousots made complete lattices the universal setting for static analysis [CC77]. In LLVM the lattices are concrete C++ types: ValueLatticeElement (unknown, undef, constant, constant range, overdefined) in llvm/include/llvm/Analysis/ValueLattice.h [LLVM-VL], used by SCCP and LazyValueInfo; Pebble's solver treats a lattice element as an opaque vector of words the client interprets (Dataflow.h).

Knaster–Tarski fixed points¶

Knaster (1928) and Tarski (1955) proved that every monotone function on a complete lattice has a least fixed point [Tar55]. For dataflow this means the equations always have a best solution, even through loops, independent of any algorithm. It also explains the two answers for the loop above: fixed points form a lattice, and "optimistic" analyses such as SCCP find the least one while "pessimistic" ones stop at a larger one.

Kleene iteration¶

Existence is not enough: we need to compute the fixed point. The constructive answer, usually credited to Kleene, is to start at \(\bot\) and apply the function until nothing changes; the Cousots gave the constructive versions of Tarski's theorem that static analysis uses [CC79b]. On lattices of finite height this terminates, and every solver in Lesson 14.4 is Kleene iteration with a clever schedule. Where the lattice has infinite height (intervals, Lesson 14.7), Kleene iteration may not stop and we will need widening.

2. Definitions and algorithms¶

Definition 14.1.1 (Partial order)

A partial order on a set \(L\) is a relation \(\sqsubseteq\ \subseteq L \times L\) that is reflexive (\(x \sqsubseteq x\)), antisymmetric (\(x \sqsubseteq y \land y \sqsubseteq x \Rightarrow x = y\)) and transitive (\(x \sqsubseteq y \land y \sqsubseteq z \Rightarrow x \sqsubseteq z\)). \((L, \sqsubseteq)\) is a poset. We write \(x \sqsubset y\) for \(x \sqsubseteq y \land x \neq y\). In this chapter \(x \sqsubseteq y\) reads "\(x\) is at least as precise as \(y\)": facts grow up the order (NOTATION.md §2).

Definition 14.1.2 (Bounds, join, meet)

Let \((L, \sqsubseteq)\) be a poset and \(X \subseteq L\). An upper bound of \(X\) is a \(u \in L\) with \(x \sqsubseteq u\) for all \(x \in X\). A least upper bound (join) \(\bigsqcup X\) is an upper bound below every other upper bound; it is unique when it exists (antisymmetry). Dually, a lower bound, the greatest lower bound (meet) \(\mathop{\Large\sqcap} X\). For two elements we write \(x \sqcup y = \bigsqcup \{x, y\}\) and \(x \sqcap y = \mathop{\Large\sqcap} \{x, y\}\).

Definition 14.1.3 (Lattice, complete lattice)

A poset is a lattice if every pair \(x, y\) has a join \(x \sqcup y\) and a meet \(x \sqcap y\). It is a complete lattice if every subset \(X \subseteq L\) (including \(\emptyset\) and infinite ones) has a join and a meet. A complete lattice has a least element \(\bot = \bigsqcup \emptyset = \mathop{\Large\sqcap} L\) and a greatest element \(\top = \mathop{\Large\sqcap} \emptyset = \bigsqcup L\). A join semilattice only requires binary joins.

Lattices and non-lattices

The four subsets of \(\{x, y\}\) ordered by \(\subseteq\) form a lattice: \(\{x\} \sqcup \{y\} = \{x, y\}\), \(\{x\} \sqcap \{y\} = \emptyset\). The "bowtie" \(\{\bot, a, b, c, d, \top\}\) with \(a, b \sqsubset c, d\) is not: \(a\) and \(b\) have two minimal upper bounds \(c\) and \(d\), hence no least one. The drill ./course drill lattice-props asks exactly this question on random posets.

Lemma 14.1.4 (Finite lattices are complete)

Every nonempty finite lattice is a complete lattice.

Proof

Let \(L\) be a nonempty finite lattice and \(X = \{x_1, \dots, x_k\} \subseteq L\). If \(k \ge 1\), \(u = x_1 \sqcup (x_2 \sqcup (\cdots \sqcup x_k))\) exists by repeated binary joins; it is an upper bound of \(X\), and by induction on \(k\) it lies below every upper bound of \(X\) (an upper bound \(v\) of \(X\) is an upper bound of \(\{x_2, \dots, x_k\}\), so it is above their join by the induction hypothesis, and above \(x_1\), hence above the binary join). So \(\bigsqcup X = u\). For \(X = \emptyset\) we need a least element: \(\mathop{\Large\sqcap} L\), the meet of the finitely many elements of \(L\), exists by the dual argument and lies below everything, so it is \(\bigsqcup \emptyset\). Meets are dual. \(\square\)

Definition 14.1.5 (Chains, ascending chain condition)

A chain is a subset \(C \subseteq L\) totally ordered by \(\sqsubseteq\). An ascending chain is a sequence \(x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq \cdots\). \(L\) satisfies the ascending chain condition (ACC) if every ascending chain is eventually constant.

Definition 14.1.6 (Height)

The height \(h(L)\) is the supremum of the lengths (number of strict steps) of the chains of \(L\): \(h(L) = \sup \{\, k \mid x_0 \sqsubset x_1 \sqsubset \cdots \sqsubset x_k \text{ in } L \,\}\). A lattice of finite height satisfies ACC; the converse fails (the lattice of natural numbers under \(\ge\) with a bottom added has infinite height and still satisfies ACC).

Definition 14.1.7 (Standard constructions)

Let \(L, L_1, L_2\) be complete lattices, \(S\) a finite set, \(V\) a finite set of variables, \(C\) any set.

Powerset \((\mathcal{P}(S), \subseteq)\): join \(\cup\), meet \(\cap\), \(\bot = \emptyset\), \(\top = S\). Its dual \((\mathcal{P}(S), \supseteq)\) has join \(\cap\) and \(\bot = S\).
Product \(L_1 \times L_2\) ordered componentwise: \((a_1, a_2) \sqsubseteq (b_1, b_2)\) iff \(a_1 \sqsubseteq_1 b_1\) and \(a_2 \sqsubseteq_2 b_2\); joins are componentwise.
Map lattice \(V \to L\) ordered pointwise: \(f \sqsubseteq g\) iff \(f(v) \sqsubseteq g(v)\) for all \(v\); \((f \sqcup g)(v) = f(v) \sqcup g(v)\).
Flat lattice \(C_\bot^\top = C \cup \{\bot, \top\}\) with \(\bot \sqsubset c \sqsubset \top\) for every \(c \in C\) and distinct elements of \(C\) incomparable.

Proposition 14.1.8 (Heights of the constructions)

With the notation of Definition 14.1.7: \(h(\mathcal{P}(S)) = \lvert S \rvert\); \(h(L_1 \times L_2) = h(L_1) + h(L_2)\); \(h(V \to L) = \lvert V \rvert \cdot h(L)\); and \(h(C_\bot^\top) = 2\) for nonempty \(C\) (even when \(C = \mathbb{Z}\)). Each construction is a complete lattice.

Proof

Powerset: a strict chain \(X_0 \subsetneq \cdots \subsetneq X_k\) adds at least one element per step, so \(k \le \lvert S \rvert\); \(\emptyset \subsetneq \{s_1\} \subsetneq \{s_1, s_2\} \subsetneq \cdots\) attains it. Product: in a strict chain of pairs every step strictly increases at least one component, and each component can strictly increase at most \(h(L_i)\) times along a chain, so \(k \le h(L_1) + h(L_2)\); raising the first component through a maximal chain and then the second attains the bound. Map lattice: \(V \to L\) is the product of \(\lvert V \rvert\) copies of \(L\). Flat: the longest chains are \(\bot \sqsubset c \sqsubset \top\). Completeness is componentwise (products, maps), by \(\bigcup\)/\(\bigcap\) (powersets), and immediate for flat lattices (any set with two distinct constants has join \(\top\)). \(\square\)

The lattices of this chapter

Liveness on the running example of Lesson 14.3 uses \(N \to \mathcal{P}(\mathit{Vars})\) with 6 blocks and 8 variables: height \(6 \cdot 8 = 48\). Constant propagation uses \(\mathit{Vars} \to \mathbb{Z}_\bot^\top\): height \(2\lvert \mathit{Vars} \rvert\) although \(\mathbb{Z}\) is infinite. The interval lattice of Lesson 14.7 has infinite height: \([0,0] \sqsubset [0,1] \sqsubset [0,2] \sqsubset \cdots\).

Definition 14.1.9 (Monotone, distributive)

A function \(f : L \to L\) is monotone if \(x \sqsubseteq y \Rightarrow f(x) \sqsubseteq f(y)\), and distributive (a join homomorphism) if \(f(x \sqcup y) = f(x) \sqcup f(y)\) for all \(x, y\).

Lemma 14.1.10 (Distributive implies monotone)

Every distributive function is monotone. Every gen/kill function \(f(X) = G \cup (X \setminus K)\) on \(\mathcal{P}(S)\) is distributive, and so is every composition and every pointwise union of distributive functions.

Proof

If \(x \sqsubseteq y\) then \(x \sqcup y = y\), so \(f(y) = f(x \sqcup y) = f(x) \sqcup f(y)\), which means \(f(x) \sqsubseteq f(y)\). For gen/kill: \(G \cup ((X \cup Y) \setminus K) = (G \cup (X \setminus K)) \cup (G \cup (Y \setminus K))\) because set difference distributes over union. If \(f, g\) are distributive, \(f(g(x \sqcup y)) = f(g(x) \sqcup g(y)) = f(g(x)) \sqcup f(g(y))\), and \((f \sqcup g)(x \sqcup y) = f(x) \sqcup f(y) \sqcup g(x) \sqcup g(y) = (f \sqcup g)(x) \sqcup (f \sqcup g)(y)\) by associativity and commutativity of \(\sqcup\). \(\square\)

Monotone but not distributive

Constant propagation's transfer function for z = x + y on \(\{x, y, z\} \to \mathbb{Z}_\bot^\top\) is monotone but not distributive: with \(e_1 = [x \mapsto 2, y \mapsto 3]\) and \(e_2 = [x \mapsto 3, y \mapsto 2]\), \(f(e_1) \sqcup f(e_2)\) has \(z = 5\), but \(f(e_1 \sqcup e_2)\) has \(x = y = \top\) and so \(z = \top\). Lesson 14.2 shows what this costs.

Definition 14.1.11 (Fixed points)

For \(F : L \to L\), \(x\) is a fixed point if \(F(x) = x\), a pre-fixed point if \(F(x) \sqsubseteq x\) and a post-fixed point if \(x \sqsubseteq F(x)\). \(\mathrm{lfp}(F)\) and \(\mathrm{gfp}(F)\) denote the least and greatest fixed points when they exist.

Complete lattices and constructions¶

The operations the solver needs are exactly those of Definitions 14.1.3 and 14.1.7: a join to combine facts at control-flow merges, equality to detect convergence, and the least element \(\bot\) to start from. Dataflow.h asks the client for Join, Init (\(\bot\) of the join order) and BoundaryFact; a must-analysis over \((\mathcal{P}(S), \supseteq)\) passes \(\cap\) as Join and \(S\) as Init, which is the dual lattice of Definition 14.1.7, not a different algorithm.

LazyValueInfo's lattice elements in LLVM

Reproduce (opt 23.1.2):

cat > lvi.ll <<'EOF'
define i32 @f(i32 %x) {
entry:
  %c = icmp ult i32 %x, 10
  br i1 %c, label %then, label %else
then:
  %a = add i32 %x, 5
  br label %join
else:
  br label %join
join:
  %p = phi i32 [ %a, %then ], [ 0, %else ]
  %r = mul i32 %p, 2
  ret i32 %r
}
EOF
opt -passes='jump-threading,print<lazy-value-info>' -disable-output lvi.ll

Output (complete; jump threading has already merged the empty %else into the edge %entry → %join):

LVI for function 'f':
define i32 @f(i32 %x) {
entry:
; LatticeVal for: 'i32 %x' is: overdefined
; LatticeVal for: '  %c = icmp ult i32 %x, 10' in BB: '%entry' is: overdefined
; LatticeVal for: '  %c = icmp ult i32 %x, 10' in BB: '%then' is: constantrange<-1, 0>
; LatticeVal for: '  %c = icmp ult i32 %x, 10' in BB: '%join' is: overdefined
  %c = icmp ult i32 %x, 10
; LatticeVal for: '  br i1 %c, label %then, label %join' in BB: '%entry' is: overdefined
; LatticeVal for: '  br i1 %c, label %then, label %join' in BB: '%then' is: overdefined
; LatticeVal for: '  br i1 %c, label %then, label %join' in BB: '%join' is: overdefined
  br i1 %c, label %then, label %join

then:                                             ; preds = %entry
; LatticeVal for: 'i32 %x' is: constantrange<0, 10>
; LatticeVal for: '  %a = add i32 %x, 5' in BB: '%then' is: constantrange<5, 15>
  %a = add i32 %x, 5
; LatticeVal for: '  br label %join' in BB: '%then' is: overdefined
  br label %join

join:                                             ; preds = %entry, %then
; LatticeVal for: 'i32 %x' is: overdefined
; LatticeVal for: '  %p = phi i32 [ %a, %then ], [ 0, %entry ]' in BB: '%join' is: constantrange<0, 15>
  %p = phi i32 [ %a, %then ], [ 0, %entry ]
; LatticeVal for: '  %r = mul i32 %p, 2' in BB: '%join' is: constantrange<0, 29>
  %r = mul i32 %p, 2
; LatticeVal for: '  ret i32 %r' in BB: '%join' is: overdefined
  ret i32 %r
}

What to notice: every value gets an element of one lattice, ValueLatticeElement: overdefined is \(\top\) ("could be anything"), constantrange<lo, hi> is the half-open interval \([lo, hi)\), and the unprinted unknown is \(\bot\). The phi's range \([0, 15)\) is the join of \(\{0\}\) and \([5, 15)\) (Definition 14.1.2): the smallest range containing both, which also contains the impossible values \(1..4\) — a join over-approximates. The same value %x has different lattice elements in different blocks: LVI's lattice is a map from (value, block) pairs to ranges (Definition 14.1.7).

Knaster–Tarski fixed points¶

Theorem 14.1.12 (Knaster–Tarski)

Let \((L, \sqsubseteq)\) be a complete lattice and \(F : L \to L\) monotone. Then \(\mathrm{lfp}(F) = \mathop{\Large\sqcap} \{\, x \mid F(x) \sqsubseteq x \,\}\) exists, and dually \(\mathrm{gfp}(F) = \bigsqcup \{\, x \mid x \sqsubseteq F(x) \,\}\). Moreover the set of fixed points of \(F\) is itself a complete lattice.

Proof sketch (least fixed point in full; the greatest is dual; the lattice of fixed points: [Tar55, Theorem 1])

Let \(P = \{\, x \mid F(x) \sqsubseteq x \,\}\) be the pre-fixed points (\(\top \in P\), so \(P \neq \emptyset\)) and \(m = \mathop{\Large\sqcap} P\), which exists because \(L\) is complete.

\(m\) is a pre-fixed point. For every \(x \in P\): \(m \sqsubseteq x\), so by monotonicity \(F(m) \sqsubseteq F(x) \sqsubseteq x\). Hence \(F(m)\) is a lower bound of \(P\), and since \(m\) is the greatest lower bound, \(F(m) \sqsubseteq m\).
\(m\) is a fixed point. From step 1 and monotonicity, \(F(F(m)) \sqsubseteq F(m)\), so \(F(m) \in P\) and therefore \(m \sqsubseteq F(m)\). With step 1 and antisymmetry, \(F(m) = m\).
\(m\) is the least fixed point. Every fixed point \(y\) satisfies \(F(y) = y \sqsubseteq y\), so \(y \in P\) and \(m \sqsubseteq y\).

The lattice structure of the set of fixed points is the second half of Tarski's theorem; we do not use it beyond the observation that there can be many fixed points between \(\mathrm{lfp}\) and \(\mathrm{gfp}\). \(\square\)

Two fixed points for the introductory loop

In SSA form the loop of the introduction has \(x_0 = \phi(1, x_1)\) at the head and \(x_1 = \phi(2, x_0)\) after the if, where the \(2\) arrives only along the edge from x = 2. Take the flat lattice \(\mathbb{Z}_\bot^\top\) for each \(x_j\) and let the if's edge be executable only if \(x_0 \neq 1\) is possibly true. With \(x_0 = x_1 = 1\) the condition is false, the edge carries \(\bot\), and \(x_1 = \bot \sqcup 1 = 1\), \(x_0 = 1 \sqcup 1 = 1\): a fixed point. With \(x_0 = x_1 = \top\) the edge is executable and \(x_1 = 2 \sqcup \top = \top\), \(x_0 = 1 \sqcup \top = \top\): also a fixed point. Theorem 14.1.12 says the least one, \(1\), is canonical; an analysis that starts from \(\bot\) finds it.

The least fixed point in LLVM: SCCP proves x == 1, instsimplify cannot

Reproduce (clang 23.1.2, opt 23.1.2):

cat > opt.c <<'EOF'
int f(int n) {
  int x = 1;
  for (int i = 0; i < n; i++)
    if (x != 1)
      x = 2;
  return x;
}
EOF
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm opt.c -o opt.ll
opt -passes=mem2reg -S opt.ll -o opt.ssa.ll
opt -passes=sccp -S opt.ssa.ll | grep -E 'phi|ret'
opt -passes=instsimplify -S opt.ssa.ll | grep -E 'phi|ret'

Output:

  %i.0 = phi i32 [ 0, %entry ], [ %inc, %for.inc ]
  ret i32 1
  %x.0 = phi i32 [ 1, %entry ], [ %x.1, %for.inc ]
  %i.0 = phi i32 [ 0, %entry ], [ %inc, %for.inc ]
  %x.1 = phi i32 [ 2, %if.then ], [ %x.0, %for.body ]
  ret i32 %x.0

What to notice: SCCP starts every value at \(\bot\) ("unknown") and every edge as non-executable, and only raises them when forced, so it lands on the least fixed point \(x = 1\) and returns the constant. InstSimplify looks at each instruction with its operands assumed arbitrary — a larger fixed point where \(x_0 = \top\) — and cannot remove the cycle of phis. Both answers satisfy the equations; Theorem 14.1.12 is why "least" is the one worth computing.

Kleene iteration¶

Definition 14.1.13 (Continuity)

\(F : L \to L\) is (Scott-)continuous if for every ascending chain \(x_0 \sqsubseteq x_1 \sqsubseteq \cdots\), \(F(\bigsqcup_i x_i) = \bigsqcup_i F(x_i)\). Continuous functions are monotone. On a lattice that satisfies ACC every monotone function is continuous, because every ascending chain is eventually constant and its join is its last element.

Theorem 14.1.14 (Kleene)

Let \(L\) be a complete lattice and \(F\) continuous. Then \(\mathrm{lfp}(F) = \bigsqcup_{i \ge 0} F^{i}(\bot)\). If \(L\) has finite height \(h\), then \(F^{k}(\bot) = F^{k+1}(\bot) = \mathrm{lfp}(F)\) for some \(k \le h\).

Proof

The iterates form a chain. \(F^{0}(\bot) = \bot \sqsubseteq F(\bot)\); if \(F^{i}(\bot) \sqsubseteq F^{i+1}(\bot)\) then monotonicity gives \(F^{i+1}(\bot) \sqsubseteq F^{i+2}(\bot)\) (induction on \(i\)). They stay below every pre-fixed point \(p\). \(\bot \sqsubseteq p\); if \(F^{i}(\bot) \sqsubseteq p\) then \(F^{i+1}(\bot) \sqsubseteq F(p) \sqsubseteq p\). The limit is a fixed point. Let \(u = \bigsqcup_i F^{i}(\bot)\). By continuity \(F(u) = \bigsqcup_i F^{i+1}(\bot) = u\) (dropping the first element \(\bot\) of a chain does not change its join). Since every fixed point is a pre-fixed point, \(u\) is below all of them: \(u = \mathrm{lfp}(F)\). Finite height. A strictly increasing prefix \(F^{0}(\bot) \sqsubset \cdots \sqsubset F^{k}(\bot)\) is a chain of length \(k\), so \(k \le h\); the first \(k\) with \(F^{k}(\bot) = F^{k+1}(\bot)\) therefore exists, and from then on the sequence is constant, so \(F^{k}(\bot) = u\). \(\square\)

Algorithm 14.1.15 (Kleene iteration)

Input: a complete lattice \(L\) of finite height with \(\bot\), equality and \(\sqcup\); a monotone \(F : L \to L\).
Output: \(\mathrm{lfp}(F)\) and the number \(k\) of applications of \(F\).
Precondition: \(F\) monotone; \(h(L) < \infty\) (or: \(L\) satisfies ACC).
Postcondition: \(x = F(x)\) and \(x \sqsubseteq y\) for every fixed point \(y\).
Invariant: \(x = F^{k}(\bot)\), \(x \sqsubseteq F(x)\) and \(x \sqsubseteq \mathrm{lfp}(F)\) (Lemma 14.1.16).

function Kleene(L, F):
    x ← ⊥
    k ← 0
    loop:
        y ← F(x)                  # one application of F
        k ← k + 1
        if y = x:
            return (x, k)
        x ← y

Lemma 14.1.16 (Invariant of Algorithm 14.1.15)

At the start of every iteration of the loop, \(x = F^{k}(\bot)\), \(x \sqsubseteq F(x)\) and \(x \sqsubseteq \mathrm{lfp}(F)\).

Proof

Initialization: \(x = \bot = F^{0}(\bot)\), and \(\bot\) is below everything. Maintenance: if the loop does not return, the new \(x\) is \(y = F(x) = F^{k+1}(\bot)\) and \(k\) has been incremented; the other two facts are the chain and pre-fixed-point parts of the proof of Theorem 14.1.14. Exit: the loop returns when \(F(x) = x\), a fixed point below \(\mathrm{lfp}(F)\), hence equal to it. \(\square\)

Kleene iteration inside Clang's dataflow framework (clang-tidy)

Reproduce (clang-tidy 18.1.3, the version in the course container; the framework is the same design in Clang 23.1.2, clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h [CLANG-DFA]):

cat > opt.cpp <<'EOF'
#include <optional>
int f(std::optional<int> o, int n) {
  int s = 0;
  for (int i = 0; i < n; i++) {
    if (o.has_value())
      s += *o;
    s += *o;
  }
  return s;
}
EOF
clang-tidy --checks='-*,bugprone-unchecked-optional-access' opt.cpp -- -std=c++17 2>/dev/null

Output (clang-tidy prints the file name as an absolute path; shortened here to opt.cpp):

opt.cpp:7:11: warning: unchecked access to optional value [bugprone-unchecked-optional-access]
    7 |     s += *o;
      |           ^

What to notice: the check is a forward dataflow analysis on the Clang CFG whose lattice element records, per optional, whether has_value() is known true. The loop makes the equations recursive; runDataflowAnalysis iterates the transfer functions from the initial state until the block states stop changing — Theorem 14.1.14 on a lattice of finite height — and only then reports. The dereference on line 6 is guarded on every path, the one on line 7 is not.

3. Worked example¶

Running example (the program of Lesson 14.3, blocks \(A\)–\(F\), entry \(A\), exit \(F\)):

flowchart TD
  A(["A: x = a * b<br/>i = 0<br/>s = 0"]) --> B["B: if i < n"]
  B --> C["C: t = a * b<br/>if t < s"]
  B --> F["F: ret s"]
  C --> D["D: s = s + t<br/>a = t - 1"]
  C --> E["E: u = a * b<br/>i = i + 1"]
  D --> E
  E --> B

Complete lattices and constructions on the running example¶

Liveness asks, for every block, which variables may be read later. Its lattice is the map lattice \(L = \{A, \dots, F\} \times \{\mathrm{in}, \mathrm{out}\} \to \mathcal{P}(\{a, b, i, n, s, t, u, x\})\): height \(12 \cdot 8 = 96\) by Proposition 14.1.8. The equations of Lesson 14.3 define one monotone \(F : L \to L\) whose components are \(\mathrm{IN}[B] = \mathrm{UEVar}(B) \cup (\mathrm{OUT}[B] \setminus \mathrm{VarKill}(B))\) and \(\mathrm{OUT}[B] = \bigcup_{S \in \mathrm{succs}(B)} \mathrm{IN}[S]\), with the local sets

block	UEVar	VarKill
A	{a,b}	{i,s,x}
B	{i,n}	{}
C	{a,b,s}	{t}
D	{s,t}	{a,s}
E	{a,b,i}	{i,u}
F	{s}	{}

Knaster–Tarski on the running example¶

\(F\) is monotone (unions and gen/kill functions, Lemma 14.1.10) on a complete lattice (Proposition 14.1.8), so \(\mathrm{lfp}(F)\) exists. It is not the only fixed point: setting every IN and OUT except \(\mathrm{OUT}[F]\) to all eight variables also satisfies the equations — for instance \(\mathrm{IN}[B] = \{i, n\} \cup (\mathit{Vars} \setminus \emptyset) = \mathit{Vars}\) — but it claims that the dead \(x\) and \(u\) are live, which is sound for register allocation and useless for dead-code elimination. The least fixed point is the precise one.

Kleene iteration on the running example¶

Algorithm 14.1.15 applies \(F\) to all components at once (every new value computed from the previous iterate; this is "Jacobi" iteration). Each cell is \(\mathrm{IN} / \mathrm{OUT}\); bold marks a change:

block	\(F^{1}(\bot)\)	\(F^{2}(\bot)\)	\(F^{3}(\bot)\)	\(F^{4}(\bot)\)	\(F^{5}(\bot)\)	\(F^{6}(\bot)\)	\(F^{7}(\bot)\)
A	{a,b} / {}	{a,b} / {i,n}	{a,b,n} /	{a,b,n} / {a,b,i,n,s}	{a,b,n} /	{a,b,n} /	{a,b,n} /
B	{i,n} / {}	{i,n} / {a,b,s}	{a,b,i,n,s} /	{a,b,i,n,s} / {a,b,i,s}	{a,b,i,n,s} /	{a,b,i,n,s} / {a,b,i,n,s}	{a,b,i,n,s} /
C	{a,b,s} / {}	{a,b,s} / {a,b,i,s,t}	{a,b,i,s} /	{a,b,i,s} / {a,b,i,n,s,t}	{a,b,i,n,s} /	{a,b,i,n,s} /	{a,b,i,n,s} /
D	{s,t} / {}	{s,t} / {a,b,i}	{b,i,s,t} /	{b,i,s,t} / {a,b,i,n}	{b,i,n,s,t} /	{b,i,n,s,t} / {a,b,i,n,s}	{b,i,n,s,t} /
E	{a,b,i} / {}	{a,b,i} / {i,n}	{a,b,i,n} /	{a,b,i,n} / {a,b,i,n,s}	{a,b,i,n,s} /	{a,b,i,n,s} /	{a,b,i,n,s} /
F	{s} / {}	{s} / {}	{s} / {}	{s} / {}	{s} / {}	{s} / {}	{s} / {}

\(F^{1}\): every IN becomes its UEVar (all OUTs were \(\emptyset\)).
\(F^{2}\)–\(F^{6}\): facts travel one block per iteration against the edges; \(n\) needs the longest trip, from B's test around the loop to D and back to B's OUT.
\(F^{7} = F^{6}\): the fixed point, after 7 applications of \(F\) (6 changing and 1 confirming), each evaluating all 12 components — 42 block transfer evaluations. Lesson 14.4 reaches the same fixed point with 18 (round-robin in the right order) or 8 (a worklist).

Try it

./course drill lattice-props --seed 3 --difficulty medium asks whether a random poset is a lattice, its height, and whether a map on it is monotone or distributive; --solution prints every join and meet. ./course drill dataflow-table --seed 2 --difficulty easy --solution shows round-robin iteration on a random program.

4. Invariants and correctness¶

Complete lattices and constructions¶

The correctness facts are Lemma 14.1.4 (finite lattices are complete), Proposition 14.1.8 (constructions preserve completeness and add heights) and Lemma 14.1.10 (distributivity is preserved by composition and join). Together they give the one property every later termination proof uses: an analysis built from powersets, products, maps and flat lattices over finite index sets has finite height, and its transfer functions are monotone if each component is.

When it breaks: the interval lattice is complete but has infinite height, so Theorem 14.1.14 gives the least fixed point only as the join of an infinite chain (the loop for (i = 0; ; i++) produces \([0,0] \sqsubset [0,1] \sqsubset \cdots\)). That is why Lesson 14.7 needs widening.

Knaster–Tarski fixed points¶

Theorem 14.1.12 needs completeness and monotonicity. Without monotonicity a fixed point need not exist: on the two-element lattice \(\{0 \sqsubset 1\}\), \(F(0) = 1, F(1) = 0\) has none. Without completeness it may not either: \(x \mapsto x + 1\) on \((\mathbb{Z}, \le)\) is monotone and fixed-point free. A dataflow framework with a non-monotone transfer function (for example one that removes a fact when an input fact appears) can make a solver oscillate forever.

Kleene iteration¶

Lemma 14.1.16 is the invariant; Theorem 14.1.14 is correctness and termination: the measure is the length of the strictly increasing prefix of iterates, bounded by \(h(L)\). The iteration never overshoots: \(F^{i}(\bot) \sqsubseteq \mathrm{lfp}(F)\) at every step, so stopping early (for instance after a timeout) yields an unsound under-approximation for a may-analysis — never stop Kleene iteration early and use the result as if it were the fixed point.

5. Complexity¶

Let \(h = h(L)\), and let \(c_F\) be the cost of one application of \(F\) and \(c_{=}\) of one equality test.

Technique	Time (worst)	Time (typical)	Space	Variables
Join / meet in \(\mathcal{P}(S)\) as bit vectors	\(O(\lvert S \rvert / w)\)	same	\(\lvert S \rvert / w\) words	\(w\) = machine word bits
Knaster–Tarski	— (existence only)	—	—	—
Kleene iteration (Algorithm 14.1.15)	\(O(h \cdot (c_F + c_{=}))\)	far fewer than \(h\) rounds	two elements of \(L\)	\(h = h(L)\)

Proposition 14.1.17 (Cost of Kleene iteration)

Algorithm 14.1.15 applies \(F\) at most \(h(L) + 1\) times.

Proof

By Theorem 14.1.14 the iterates strictly increase until the first repetition, so at most \(h(L)\) applications produce a strictly larger element, and one more observes \(F(x) = x\). \(\square\)

Pathological input. Liveness on a chain \(B_1 \to B_2 \to \cdots \to B_n\) where only \(B_n\) reads \(v\) and nothing defines it: Jacobi iteration moves the fact \(v\) one component per application (\(\mathrm{IN}[B_n]\), then \(\mathrm{OUT}[B_{n-1}]\), then \(\mathrm{IN}[B_{n-1}]\), …), so it needs \(2n\) applications of \(F\) (\(2n - 1\) changing, one confirming), each of cost \(\Theta(n)\) block transfers: \(\Theta(n^2)\) transfer evaluations, whereas visiting blocks in the right order (Lesson 14.4) needs \(2n\). The height bound \(h = 2n \cdot \lvert \mathit{Vars} \rvert\) is far larger than the actual number of rounds; bounds by height are worst-case guarantees, not predictions.

At scale: the height of the liveness lattice of a 5 000-block function with 20 000 SSA values is \(10^{4} \cdot 2 \cdot 10^{4} = 2 \cdot 10^{8}\), yet the solvers of Lesson 14.4 converge in a handful of passes on real code; Kam and Ullman's \(d(G) + 2\) bound explains why [KU76].

Complete lattices and constructions¶

Semilattices instead of lattices [Kil73, KU77]: only \(\sqcup\) is needed by the solvers — trade-off: fewer axioms to check, but no meet for combining analyses (reduced products need both).
Reduced product [CC79]: the product of two domains followed by mutual refinement (for example signs × parity) — trade-off: more precise than the plain product of Definition 14.1.7, more expensive operations.
Lattices of infinite height with ACC-free chains need widening [CC77], cross-linked in Lesson 14.7.

Knaster–Tarski fixed points¶

Greatest fixed points for must-analyses: the least fixed point in the dual order, which is why Dataflow.h has one algorithm and lets Init be \(\top\) of the subset order — trade-off: none, but the orientation must be stated (NOTATION.md §2).
Post-fixed points as sound results [CC77]: any \(x\) with \(F(x) \sqsubseteq x\) over-approximates \(\mathrm{lfp}(F)\) (Theorem 14.1.12, step 3) — the justification for widening, which computes such an \(x\) cheaply at the price of precision.

Kleene iteration¶

Chaotic iteration [NNH, Ch. 6]: apply the components of \(F\) in any fair order and in place; still converges to \(\mathrm{lfp}(F)\) — trade-off: faster (round-robin, worklists, Lesson 14.4) but the order now matters for cost.
Kleene iteration with widening [CC77]: replace \(x_{k+1} = F(x_k)\) by \(x_{k+1} = x_k \nabla F(x_k)\) — trade-off: terminates on infinite-height lattices, but only reaches a post-fixed point.

7. In real compilers¶

Complete lattices and constructions¶

LLVM

llvm/include/llvm/Analysis/ValueLattice.h — ValueLatticeElement with the tags unknown, undef, constant, notconstant, constantrange and overdefined, and mergeIn, the join (LLVM 23.1.2) [LLVM-VL]. llvm/include/llvm/IR/ConstantRange.h supplies the interval join unionWith [LLVM-CR].

GCC gcc/tree-ssa-ccp.cc — ccp_lattice_t with UNINITIALIZED, UNDEFINED, CONSTANT, VARYING (GCC 15) [GCC-CCP].
rustc compiler/rustc_mir_dataflow/src/framework/lattice.rs — trait JoinSemiLattice (rustc 1.90.0) [RUSTC-DF].
MLIR mlir/include/mlir/Analysis/DataFlowFramework.h — AnalysisState; lattices such as IntegerValueRangeLattice in IntegerRangeAnalysis.h (LLVM 23.1.2) [MLIR-DF].

Find where LLVM does it. Open llvm/include/llvm/Analysis/ValueLattice.h and read ValueLatticeElement::mergeIn. Question: which tag does merging two different constants produce when range merging is allowed? (Quiz llvm-where-lattice-merge.)

Knaster–Tarski fixed points¶

LLVM

llvm/lib/Transforms/Utils/SCCPSolver.cpp — SCCPInstVisitor::solve computes the least fixed point optimistically: values start unknown, blocks start non-executable (LLVM 23.1.2) [LLVM-SCCP]. Pessimistic simplifiers such as llvm/lib/Analysis/InstructionSimplify.cpp stop at larger fixed points.

GCC gcc/tree-ssa-ccp.cc — the same optimistic least fixed point ("UNDEFINED ... we don't yet know if its value is a constant", file comment) (GCC 15) [GCC-CCP].
Clang clang/docs/DataFlowAnalysisIntro.md states the termination condition in these terms: "If the lattice has a finite height and transfer functions are monotonic the algorithm is guaranteed to terminate" (LLVM 23.1.2) [CLANG-DFDOC].

Kleene iteration¶

Clang

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h — runDataflowAnalysis iterates the transfer functions over the CFG until the block states are stable (LLVM 23.1.2) [CLANG-DFA].

rustc compiler/rustc_mir_dataflow/src/framework/mod.rs — Analysis::iterate_to_fixpoint (rustc 1.90.0) [RUSTC-DF].
MLIR mlir/include/mlir/Analysis/DataFlowFramework.h — DataFlowSolver::initializeAndRun drives every analysis to a joint fixed point (LLVM 23.1.2) [MLIR-DF].

8. Comparison¶

Technique	Power / precision	Speed	Output / error quality	Implementation effort	Typical use
Complete lattices and constructions	Expresses every analysis in this chapter; precision is decided by the chosen lattice	join \(O(\lvert S \rvert / w)\) on bit vectors	Facts are human-readable sets, maps, ranges	Low: a type with join, equality and \(\bot\)	The value type of every dataflow solver (LLVM `ValueLatticeElement`)
Knaster–Tarski	Guarantees a best (least) solution exists	— (not an algorithm)	Tells you which solution a solver must return	None	Specifying analyses; justifying optimistic analyses such as SCCP
Kleene iteration	Computes exactly \(\mathrm{lfp}(F)\)	\(\le h(L) + 1\) applications of \(F\); Jacobi is the slowest schedule	Exact least fixed point	Lowest: one loop	Reference oracle; the basis of chaotic iteration (Lesson 14.4)

Choose a richer lattice when a coarser one loses the fact you need (sets of constants instead of one constant, ranges instead of signs). Invoke Knaster–Tarski when you design an analysis: prove monotonicity and completeness, then you only need an algorithm. Use plain Kleene iteration when you need an obviously correct reference implementation (the course's Python oracles in tools/course/lib/dataflow.py are exactly this); use the ordered strategies of Lesson 14.4 in production.

9. Assessment¶

Technique	Quiz ids (`solutions/quizzes/ch14.yaml`)	Drill	Flashcard tag	Exercises
Complete lattices and constructions	`lattice-height-map`, `lattice-is-lattice`, `llvm-where-lattice-merge`	`./course drill lattice-props`	`lattice`	E1 (the `Join`/`Init` contract)
Knaster–Tarski fixed points	`tarski-least-fixpoint`, `monotone-distributive`	`./course drill lattice-props --difficulty medium`	`tarski`	—
Kleene iteration	`kleene-iterations-interval`, `kleene-stop-early`	`./course drill widening --difficulty hard` (Kleene count)	`kleene`	E1

Pitfall

"The solver found a fixed point, so the answer is right." Every monotone system can have many fixed points (Theorem 14.1.12); a solver that starts from the wrong end (⊤ instead of ⊥ for a may-analysis) converges immediately to a sound but useless one. The starting point is part of the specification.

References¶

See the chapter references.

Lesson 14.1 — Lattices and fixed points¶

1. Problem and motivation¶

Complete lattices and constructions¶

Knaster–Tarski fixed points¶

Kleene iteration¶

2. Definitions and algorithms¶

Complete lattices and constructions¶

Knaster–Tarski fixed points¶

Kleene iteration¶

3. Worked example¶

Complete lattices and constructions on the running example¶

Knaster–Tarski on the running example¶

Kleene iteration on the running example¶

4. Invariants and correctness¶

Complete lattices and constructions¶

Knaster–Tarski fixed points¶

Kleene iteration¶

5. Complexity¶

6. Variants and refinements¶

Complete lattices and constructions¶

Knaster–Tarski fixed points¶

Kleene iteration¶

7. In real compilers¶

Complete lattices and constructions¶

Knaster–Tarski fixed points¶

Kleene iteration¶

8. Comparison¶

9. Assessment¶

References¶