Lesson 14.2 — Monotone frameworks: MOP and MFP¶
Techniques: Kildall's framework and iterative algorithm; Kam–Ullman monotone frameworks; the meet-over-all-paths (MOP) and maximal-fixed-point (MFP) solutions, soundness, equality for distributive frameworks, undecidability of MOP · Pebble implements: the framework instance of
Dataflow.h(exercise E1) · Lab: the MFP = MOP property tests (ch14.DataflowSolver.*) · Prerequisites: Lesson 14.1 · Time: 4–6 hours
Which constant does z hold at the end of this program?
Along each of the two paths, z is 5. But an analysis that first merges what it knows at the join (\(x \in \{2, 3\}\), \(y \in \{2, 3\}\)) and then evaluates x + y has lost the correlation and can only say "not a constant". The first answer is the meet over all paths (MOP), the ideal; the second is the maximal fixed point (MFP), what every iterative solver computes. This lesson defines both, proves that MFP is always a sound approximation of MOP, that they coincide for distributive problems, and that in general MOP cannot be computed at all.
1. Problem and motivation¶
Before 1973 every global optimization came with its own ad hoc propagation algorithm: available expressions in one pass, live variables in another [Ull73, AC76]. Kildall observed that they all have the same shape — a lattice of facts, a function per node, a merge at joins — and gave one algorithm for all of them [Kil73]. Kam and Ullman then separated the specification (what answer is correct) from the algorithm (what the solver returns) and proved when they agree [KU76, KU77]. Pebble's Dataflow.h is exactly their interface: a lattice, a direction, a transfer function per node, a boundary value; one solver serves liveness (E2), reaching stores (E3), definite initialization (E4) and intervals (E6).
Monotone frameworks (Kildall)¶
Kildall's "pools" of facts propagate along edges; at a node with several predecessors the pools are combined with a meet; the process repeats until nothing changes [Kil73]. He proved termination for finite semilattices and correctness for distributive functions. The generalization to monotone functions, and the name "monotone framework", are Kam and Ullman's [KU77].
MOP and MFP (Kam–Ullman)¶
The semantics of a program point is the set of all executions reaching it. The best abstraction that ignores which branches are feasible is the join over all paths: MOP. Kam and Ullman showed that MOP is not computable for monotone frameworks in general, that the iterative algorithm computes the MFP solution, that MFP is always sound with respect to MOP, and that MFP = MOP when the framework is distributive [KU77]. Constant propagation is the standard non-distributive example; bit-vector problems are distributive, so for them the iterative algorithm is exact.
2. Definitions and algorithms¶
Definition 14.2.1 (Flowgraph, paths)
A flowgraph \(G = (N, E, r)\) is a finite directed graph with an entry node \(r\). A path \(p = \langle n_0, n_1, \dots, n_k \rangle\) has \((n_{i}, n_{i+1}) \in E\); \(\mathrm{Paths}(n)\) is the set of paths from \(r\) to \(n\). For a backward analysis we use the reverse graph \(G^{R}\) with the exits as entries; everything below is stated for forward problems.
Definition 14.2.2 (Monotone framework)
A monotone framework is a pair \((L, \mathcal{F})\) where \(L\) is a complete lattice (join \(\sqcup\), least element \(\bot\)) satisfying ACC, and \(\mathcal{F}\) is a set of monotone functions \(L \to L\) that contains the identity and is closed under composition. It is distributive if every \(f \in \mathcal{F}\) is distributive (Definition 14.1.9).
Definition 14.2.3 (Kam–Ullman orientation)
Kam and Ullman write the same theory in the dual order: facts go down, merges are meets \(\wedge\), and the lattice top means "no information yet" [KU77]. Every statement of this lesson translates by swapping \(\sqcup \leftrightarrow \sqcap\) and \(\sqsubseteq \leftrightarrow \sqsupseteq\). In particular their soundness theorem "\(\mathrm{MFP} \le \mathrm{MOP}\)" is our \(\mathrm{MOP} \sqsubseteq \mathrm{MFP}\): in both, MFP is the less precise one.
Definition 14.2.4 (Framework instance)
An instance of \((L, \mathcal{F})\) is a tuple \((G, f, \iota)\): a flowgraph \(G\), a map
\(f : N \to \mathcal{F}\) assigning a transfer function \(f_n\) to each node, and a boundary value
\(\iota \in L\) for the entry. (Pebble's Dataflow.h also allows edge functions \(f_{u \to v}\); they
compose with the node functions and change nothing below.)
Liveness and constant propagation as instances
Liveness: \(L = \mathcal{P}(\mathit{Vars})\) with \(\cup\), \(\mathcal{F}\) = all gen/kill functions \(X \mapsto G \cup (X \setminus K)\), on \(G^{R}\), \(\iota = \emptyset\) at the exits — distributive by Lemma 14.1.10. Constant propagation: \(L = \mathit{Vars} \to \mathbb{Z}_\bot^\top\), \(\mathcal{F}\) generated by the assignment transfer functions — monotone, not distributive (the example after Lemma 14.1.10).
Definition 14.2.5 (Path transfer function)
For \(p = \langle n_0, \dots, n_k \rangle\) let \(f_p = f_{n_{k-1}} \circ \cdots \circ f_{n_0}\) (the effect of executing \(n_0, \dots, n_{k-1}\); the empty composition is the identity). \(f_p(\iota)\) is the fact holding on entry to \(n_k\) after path \(p\).
Definition 14.2.6 (Meet-over-all-paths solution)
\(\mathrm{MOP}(n) = \bigsqcup_{p \in \mathrm{Paths}(n)} f_p(\iota)\) for every \(n\); nodes unreachable from \(r\) get \(\bot\). (Kam and Ullman's name keeps "meet" from their orientation.)
Definition 14.2.7 (Dataflow equations)
The equations of the instance are, for every \(n \in N\),
Equivalently \(\vec{\mathrm{IN}} = \mathcal{E}(\vec{\mathrm{IN}})\) for the function \(\mathcal{E} : (N \to L) \to (N \to L)\) defined by the right-hand sides.
Lemma 14.2.8 (The equation function is monotone)
\(\mathcal{E}\) is monotone on the map lattice \(N \to L\), which is complete and satisfies ACC.
Proof
Each component of \(\mathcal{E}(\vec{X})\) is a join of a constant and of \(f_m(X_m)\); the \(f_m\) are monotone and \(\sqcup\) is monotone in each argument, so \(\vec{X} \sqsubseteq \vec{Y}\) pointwise implies \(\mathcal{E}(\vec{X}) \sqsubseteq \mathcal{E}(\vec{Y})\) pointwise. \(N \to L\) is complete and satisfies ACC by Proposition 14.1.8 (a finite product of lattices with ACC). \(\square\)
Definition 14.2.9 (Maximal-fixed-point solution)
\(\mathrm{MFP} = \mathrm{lfp}(\mathcal{E})\), which exists by Lemma 14.2.8 and Theorem 14.1.12. It is called maximal in Kam and Ullman's orientation (Definition 14.2.3) and is the least solution of the equations in ours.
Monotone frameworks (Kildall)¶
Algorithm 14.2.10 (Kildall's iterative algorithm)
- Input: an instance \((G, f, \iota)\) of a monotone framework.
- Output: \(\mathrm{IN}[n]\) for every node.
- Precondition: \(L\) satisfies ACC; every \(f_n\) is monotone.
- Postcondition: \(\vec{\mathrm{IN}} = \mathrm{MFP}\) (Theorem 14.2.11).
- Invariant: \(\vec{\mathrm{IN}} \sqsubseteq \mathrm{MFP}\) pointwise, and every edge \(m \to n\) whose constraint \(f_m(\mathrm{IN}[m]) \sqsubseteq \mathrm{IN}[n]\) may be violated has its source \(m\) in \(W\).
Theorem 14.2.11 (Kildall's algorithm computes MFP)
Under its precondition, Algorithm 14.2.10 terminates, whatever order it removes nodes from \(W\) in, and returns \(\mathrm{MFP}\).
Proof
Invariant \(\vec{\mathrm{IN}} \sqsubseteq \mathrm{MFP}\): initially \(\mathrm{IN}[r] = \iota \sqsubseteq \mathrm{MFP}(r)\) (the equation for \(r\) contains \(\iota\)) and all else is \(\bot\). An update sets \(\mathrm{IN}[n] \leftarrow \mathrm{IN}[n] \sqcup f_m(\mathrm{IN}[m])\) with \(m \in \mathrm{preds}(n)\); by the invariant and monotonicity \(f_m(\mathrm{IN}[m]) \sqsubseteq f_m(\mathrm{MFP}(m)) \sqsubseteq \mathrm{MFP}(n)\), the last step because MFP satisfies \(n\)'s equation. So the join stays below \(\mathrm{MFP}(n)\). Invariant on \(W\): call an edge \(m \to n\) satisfied if \(f_m(\mathrm{IN}[m]) \sqsubseteq \mathrm{IN}[n]\). Initially every source is in \(W\). Processing \(m\) joins \(f_m(\mathrm{IN}[m])\) into every successor, so all edges out of \(m\) are satisfied when \(m\) leaves \(W\). An edge \(m' \to n'\) can become unsatisfied only when \(\mathrm{IN}[m']\) grows (growing \(\mathrm{IN}[n']\) keeps edges into \(n'\) satisfied), and every growth of \(\mathrm{IN}[n]\) adds \(n\) to \(W\). \(\mathrm{IN}[r] \sqsupseteq \iota\) holds from the start and values only grow. Termination: every iteration either empties an element of \(W\) without growing anything, or grows some \(\mathrm{IN}[n]\) strictly; by ACC each \(\mathrm{IN}[n]\) grows finitely often, and each growth adds one node to \(W\), so the loop ends. Result: at the end \(W = \emptyset\), so every constraint holds: \(\vec{\mathrm{IN}}\) is a pre-fixed point of \(\mathcal{E}\), hence \(\mathrm{MFP} \sqsubseteq \vec{\mathrm{IN}}\) (Theorem 14.1.12); with the first invariant, \(\vec{\mathrm{IN}} = \mathrm{MFP}\). \(\square\)
Kildall's framework as a C++ template: LLVM's SparseSolver
Reproduce (opt 23.1.2):
cat > cvp.ll <<'EOF'
define internal i32 @inc(i32 %x) {
%r = add i32 %x, 1
ret i32 %r
}
define internal i32 @dec(i32 %x) {
%r = sub i32 %x, 1
ret i32 %r
}
define i32 @apply(i1 %c, i32 %v) {
entry:
%fp = select i1 %c, ptr @inc, ptr @dec
%r = call i32 %fp(i32 %v)
ret i32 %r
}
EOF
opt -passes=called-value-propagation -S cvp.ll | grep -E 'call|^!0'
Output:
What to notice: CalledValuePropagation instantiates the generic SparseSolver<LatticeKey,
LatticeVal> of llvm/include/llvm/Analysis/SparsePropagation.h [LLVM-SPARSE] with a lattice of
sets of functions (with a ⊤ for "too many"), supplies the transfer functions through
AbstractLatticeFunction::ComputeInstructionState, and lets the solver iterate to the least fixed
point; the select joins \(\{\texttt{@inc}\}\) and \(\{\texttt{@dec}\}\) — Definition 14.2.2 with a
different lattice and no other change.
MOP and MFP (Kam–Ullman)¶
Theorem 14.2.12 (Soundness of MFP)
For every instance of a monotone framework and every node \(n\): \(\mathrm{MOP}(n) \sqsubseteq \mathrm{MFP}(n)\) (in Kam and Ullman's orientation, \(\mathrm{MFP} \le \mathrm{MOP}\)).
Proof
It suffices to show \(f_p(\iota) \sqsubseteq \mathrm{MFP}(n)\) for every path \(p \in \mathrm{Paths}(n)\), because MOP is the least upper bound of those values. Induction on the length \(k\) of \(p\). \(k = 0\): \(p = \langle r \rangle\), \(f_p = \mathrm{id}\) and \(\iota \sqsubseteq \mathrm{MFP}(r)\) because \(\iota\) is a joinand of \(r\)'s equation. Step: \(p = p' \cdot \langle n \rangle\) with \(p'\) ending in \(m \in \mathrm{preds}(n)\). By the induction hypothesis \(f_{p'}(\iota) \sqsubseteq \mathrm{MFP}(m)\), so by monotonicity \(f_p(\iota) = f_m(f_{p'}(\iota)) \sqsubseteq f_m(\mathrm{MFP}(m))\), which is a joinand of \(n\)'s equation, which \(\mathrm{MFP}\) satisfies: \(f_m(\mathrm{MFP}(m)) \sqsubseteq \mathrm{MFP}(n)\). \(\square\)
Theorem 14.2.13 (Distributive frameworks: MFP = MOP)
If the framework is distributive and every node is reachable from \(r\), then \(\mathrm{MFP}(n) = \mathrm{MOP}(n)\) for every \(n\).
Proof
By Theorem 14.2.12 it remains to show \(\mathrm{MFP} \sqsubseteq \mathrm{MOP}\), and since MFP is the least pre-fixed point it suffices that \(\vec{\mathrm{MOP}}\) satisfies every equation's constraint \(\iota_n \sqcup \bigsqcup_{m} f_m(\mathrm{MOP}(m)) \sqsubseteq \mathrm{MOP}(n)\). For \(n = r\): \(\iota = f_{\langle r \rangle}(\iota) \sqsubseteq \mathrm{MOP}(r)\). For an edge \(m \to n\):
The second equality is distributivity. It is stated for binary joins; \(\mathrm{Paths}(m)\) can be infinite, but the join is attained by a finite subset (ACC: the ascending chain of joins of the first \(k\) paths, enumerated by length, stabilizes), and distributivity extends to finite joins by induction. The last step holds because each \(p \cdot \langle n \rangle\) is in \(\mathrm{Paths}(n)\). \(\mathrm{Paths}(m) \neq \emptyset\) because \(m\) is reachable. \(\square\)
Theorem 14.2.14 (Kam–Ullman: MOP is undecidable)
There is no algorithm that computes \(\mathrm{MOP}\) for every instance of every monotone framework. Already for constant propagation (\(L = \mathit{Vars} \to \mathbb{Z}_\bot^\top\): infinite, but of finite height, with computable transfer functions) no algorithm decides, given an instance and a node \(n\), whether a variable is a constant in \(\mathrm{MOP}(n)\). (The infinite value set is essential: over a finite lattice, MOP is computable by reachability in the product of \(G\) and \(L\).)
Proof sketch (full proof: [KU77])
Kam and Ullman reduce the (modified) Post correspondence problem to MOP for a monotone but non-distributive framework built from constant propagation: each path through a loop spells a candidate sequence of dominoes, integer variables encode the two strings built so far, and whether a variable's value at the exit is the same constant on every path depends on whether some path spells a solution. MOP is the join over all such paths, so computing it decides the instance — undecidable. (A finite lattice cannot encode unboundedly long strings, which is why the reduction needs \(\mathbb{Z}\).) MFP merges before evaluating and is therefore always computable. Distributivity is exactly what the reduction must violate, because by Theorem 14.2.13 MOP = MFP is computable for distributive frameworks.
MFP loses what MOP keeps: SCCP versus InstCombine
Reproduce (clang 23.1.2, opt 23.1.2, x86-64 Linux; other targets print other function attributes):
cat > mop.c <<'EOF'
int g(int c) {
int x, y;
if (c) { x = 2; y = 3; }
else { x = 3; y = 2; }
return x + y;
}
EOF
clang-23 -O0 -Xclang -disable-O0-optnone -fno-discard-value-names -S -emit-llvm mop.c -o - \
| opt -passes=mem2reg,sccp -S | grep -E '^define|phi|= add|^ ret'
clang-23 -O2 -fno-discard-value-names -S -emit-llvm mop.c -o - | grep -E '^define|^ ret'
Output:
define dso_local range(i32 4, 7) i32 @g(i32 noundef %c) #0 {
%x.0 = phi i32 [ 2, %if.then ], [ 3, %if.else ]
%y.0 = phi i32 [ 3, %if.then ], [ 2, %if.else ]
%add = add nuw nsw i32 %x.0, %y.0
ret i32 %add
define dso_local noundef range(i32 4, 7) i32 @g(i32 noundef %c) local_unnamed_addr #0 {
ret i32 5
What to notice: SCCP is an MFP analysis over constant ranges: it joins at the merge (\(x, y \in [2, 4)\))
and then adds, so the best it can say is \(z \in [4, 7)\) — the range(i32 4, 7) return attribute.
That is Theorem 14.2.12: sound, above MOP. At -O2, InstCombine's foldBinopWithPhiOperands
evaluates add separately per incoming edge of the phis — per path — and gets \(5\) on both,
which is the MOP answer. Programs can be transformed so that MOP becomes computable (here by
duplicating the addition into the predecessors); no analysis over the original merged CFG can.
3. Worked example¶
The instance of the introduction as a program in the notation of Lesson 14.3:
flowchart TD
A(["A: if c < d"]) --> B["B: x = 2<br/>y = 3"]
A --> C["C: x = 3<br/>y = 2"]
B --> D["D: z = x + y"]
C --> D
D --> E["E: ret z"]The lattice is \(\{x, y, z\} \to \mathbb{Z}_\bot^\top\); an environment is written as the list of non-\(\bot\) entries.
Monotone frameworks (Kildall) on the example¶
Algorithm 14.2.10 with \(W\) a FIFO queue initialized in the order \(A, B, C, D, E\); \(f_m\) is applied to \(\mathrm{IN}[m]\) and joined into each successor:
| step | remove | \(f_m(\mathrm{IN}[m])\) | successors updated | \(W\) after |
|---|---|---|---|---|
| 0 | — | — | \(\mathrm{IN}[A] = \iota = []\), others \(\bot\) | A B C D E |
| 1 | A | \([]\) | B: \(\bot \sqcup [] = []\) (unchanged: both "no constants"); C: same | B C D E |
| 2 | B | \([x{=}2, y{=}3]\) | D: \([x{=}2, y{=}3]\) | C D E |
| 3 | C | \([x{=}3, y{=}2]\) | D: \([x{=}\top, y{=}\top]\) | D E |
| 4 | D | \([x{=}\top, y{=}\top, z{=}\top]\) | E: \([x{=}\top, y{=}\top, z{=}\top]\) | E |
| 5 | E | — (no successors) | — | (empty) |
(Step 1 changes nothing because the empty environment \([]\) and \(\bot\) coincide in this encoding: every variable is \(\bot\).) MFP at \(E\): \(z = \top\).
MOP and MFP (Kam–Ullman) on the example¶
\(\mathrm{Paths}(E) = \{\langle A, B, D, E\rangle, \langle A, C, D, E\rangle\}\):
| path | \(f_p(\iota)\) on entry to \(E\) |
|---|---|
| A B D E | \([x{=}2, y{=}3, z{=}5]\) |
| A C D E | \([x{=}3, y{=}2, z{=}5]\) |
| join = \(\mathrm{MOP}(E)\) | \([x{=}\top, y{=}\top, z{=}5]\) |
So \(\mathrm{MOP}(E) \sqsubset \mathrm{MFP}(E)\) strictly: the framework is not distributive (Theorem 14.2.13 does not apply) and the soundness inequality of Theorem 14.2.12 is strict. The C++ test ch14.DataflowSolver.ConstantPropagationIsNotDistributive encodes this instance for your solver; MFPEqualsMOPOnAcyclicDistributiveInstances checks Theorem 14.2.13 on 300 random acyclic gen/kill instances, computing MOP by enumerating paths.
Try it
./course drill dataflow-table --seed 5 --difficulty medium gives a random gen/kill instance; since
it is distributive, its MFP table is also its MOP. ./course drill lattice-props --seed 9 --difficulty medium
checks distributivity of a map by finding the witness pair.
4. Invariants and correctness¶
Monotone frameworks (Kildall)¶
The invariants are stated in Algorithm 14.2.10 and proved in Theorem 14.2.11: the current solution never exceeds MFP, and the worklist contains every node that could violate a constraint. Termination is by ACC on the finite product \(N \to L\).
When it breaks: if some \(f_n\) is not monotone, the first invariant fails — a larger input may produce a smaller output, a successor's fact can later need to shrink, and the join-only update never shrinks anything. The algorithm then returns a result that is not a fixed point, or loops (for example \(f(0) = 1\), \(f(1) = 0\) on a self-loop never stabilizes if updates overwrite instead of join).
MOP and MFP (Kam–Ullman)¶
Theorems 14.2.12–14.2.14. Two preconditions matter:
- Distributivity (Theorem 14.2.13): the constant-propagation instance above is the counterexample without it.
- Reachability (Theorem 14.2.13): for an unreachable node \(n\), \(\mathrm{MOP}(n) = \bot\) by definition, but MFP can be larger, because an unreachable predecessor \(m\) still contributes \(f_m(\mathrm{IN}[m]) \sqsupseteq f_m(\bot)\), which is not \(\bot\) when \(m\) generates facts: a definition in an unreachable block "reaches" its unreachable successors in MFP but not in MOP. Soundness (Theorem 14.2.12) is unaffected. For a must-analysis \(\bot\) is the universe, so an unreachable block that keeps the universe (definite initialization, E4) agrees with MOP.
5. Complexity¶
Let \(n = \lvert N \rvert\), \(e = \lvert E \rvert\), \(h = h(L)\), \(c_f\) the cost of a transfer function and \(c_\sqcup\) of a join.
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Kildall (Algorithm 14.2.10) | \(O(e \cdot h \cdot (c_f + c_\sqcup))\) | a few visits per node (Lesson 14.4) | \(O(n)\) lattice elements + \(W\) | \(n, e, h\) |
| MOP by path enumeration (acyclic \(G\)) | \(O(\lvert \mathrm{Paths} \rvert \cdot n \cdot c_f)\), exponential in \(n\) | — | \(O(n)\) | \(n\) |
| MOP, general monotone framework | undecidable (Theorem 14.2.14) | — | — | — |
Proposition 14.2.15 (Cost of Kildall's algorithm)
Algorithm 14.2.10 removes nodes from \(W\) at most \(n (h + 1)\) times and evaluates at most \(e (h + 1)\) joins.
Proof
Initially \(W\) holds \(n\) nodes. A node \(v\) is added to \(W\) only when \(\mathrm{IN}[v]\) strictly grows, which happens at most \(h\) times per node (a strictly increasing chain in \(L\)), so additions total at most \(n h\) and removals at most \(n + n h\). A node \(m\) is therefore removed at most \(h + 1\) times, and each removal performs one transfer evaluation and one join per out-edge: at most \(\sum_m (h + 1)\,\mathrm{outdeg}(m) = e (h + 1)\) joins overall. \(\square\)
Pathological input. MOP enumeration on the "diamond chain" of \(k\) consecutive if-then-else diamonds: \(2^{k}\) paths reach the last node, so enumerating them costs \(\Theta(2^{k} k)\) transfer evaluations while MFP costs \(\Theta(k)\) with a good order. For \(k = 30\), a billion paths.
At scale: Kildall's own paper already iterated over a worklist of nodes and pools [Kil73]; the bound \(e \cdot h\) is pessimistic by orders of magnitude, and Lesson 14.4 shows the \(d(G) + 2\) pass bound that explains practice.
6. Variants and refinements¶
Monotone frameworks (Kildall)¶
- Edge-based transfer functions: attach functions to edges (branch refinement, phi copies), as IDE does with its edge functions [SRH96] — trade-off: more precision for conditions, one more function per edge. Pebble's
Problem::EdgeTransfer. - Bidirectional frameworks (Morel–Renvoise PRE [MR79]) [KD94]: IN depends on both predecessors and successors — trade-off: expresses PRE directly, but the solvers of Lesson 14.4 lose their order guarantees; later PRE formulations (lazy code motion) decompose it into unidirectional problems.
- Sparse frameworks [CCF91]: solve on a smaller graph than the CFG (Lesson 14.6).
MOP and MFP (Kam–Ullman)¶
- Path-sensitive analysis (e.g. the clang static analyzer's symbolic execution) [CLANG-SA]: approximates MOP by exploring paths up to a budget — trade-off: more precise than MFP, exponential, incomplete (it gives up after a loop bound).
- Trace partitioning / relational domains [CC79, MR05]: keep the correlation between \(x\) and \(y\) at the merge (\(x + y = 5\) is a relation) — trade-off: relational lattices such as octagons (Lesson 14.7) recover the example above at polynomial cost.
- IFDS [RHS95]: for distributive problems with finite fact sets, MOP over interprocedurally valid paths is computable in polynomial time (Lesson 14.8).
7. In real compilers¶
Monotone frameworks (Kildall)¶
LLVM
llvm/include/llvm/Analysis/SparsePropagation.h — AbstractLatticeFunction (the framework:
lattice values, MergeValues = join, ComputeInstructionState = transfer) and SparseSolver::Solve
(the algorithm) (LLVM 23.1.2) [LLVM-SPARSE]. Its client is
llvm/lib/Transforms/IPO/CalledValuePropagation.cpp.
- Clang
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h—DataflowAnalysis<Derived, LatticeT>withtransferand a lattice type providingjoin(LLVM 23.1.2) [CLANG-DFA]. - MLIR
mlir/include/mlir/Analysis/DataFlowFramework.h—DataFlowAnalysis,DataFlowSolver(LLVM 23.1.2) [MLIR-DF]. - GCC
gcc/df-core.cc—df_analyze_problemruns anystruct dataflowproblem (confluence and transfer callbacks) (GCC 15) [GCC-DF]. - rustc
compiler/rustc_mir_dataflow/src/framework/mod.rs— traitAnalysiswithDomain: JoinSemiLattice(rustc 1.90.0) [RUSTC-DF].
Find where LLVM does it. Open llvm/include/llvm/Analysis/SparsePropagation.h. Question: what is the name of the class whose Solve method runs the propagation? (Quiz llvm-where-sparse-solver.)
MOP and MFP (Kam–Ullman)¶
LLVM
llvm/lib/Transforms/InstCombine/InstructionCombining.cpp — InstCombinerImpl::foldBinopWithPhiOperands
and foldOpIntoPhi evaluate an operation per incoming edge of a phi, recovering path-wise
(MOP-like) results after the fact (LLVM 23.1.2) [LLVM-IC].
- Clang the static analyzer (
clang --analyze) is path-sensitive: it explores paths separately up to a loop bound, approximating MOP where the flow-sensitive-Wuninitializedcomputes MFP [CLANG-SA]. - GCC
gcc/tree-ssa-ccp.cc— Wegman–Zadeck CCP, an MFP analysis (GCC 15) [GCC-CCP].
8. Comparison¶
| Technique | Power / precision | Speed | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Monotone framework + Kildall's algorithm (MFP) | Sound; exact for distributive frameworks (Theorem 14.2.13), above MOP otherwise | \(O(e \cdot h)\) updates worst case; near-linear in practice | One fact per program point; merges lose path correlations | Low: one generic solver, one instance per analysis | Every production dataflow framework (LLVM, GCC, Clang, MLIR, rustc) |
| MOP (Kam–Ullman) | The most precise path-insensitive-to-feasibility answer | Exponential by enumeration; undecidable in general (Theorem 14.2.14) | Ideal reference; per-path results | Only for acyclic graphs or distributive problems | Specification; property tests (ch14.DataflowSolver.MFPEqualsMOP*) |
Choose MFP via a generic framework when you build any analysis you want to terminate. Reason in terms of MOP when you judge precision: if your framework is distributive, MFP is optimal and you should not look for a better algorithm, only a better lattice.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Monotone frameworks (Kildall) | framework-instance, kildall-updates, llvm-where-sparse-solver |
./course drill dataflow-table |
framework |
E1 |
| MOP and MFP (Kam–Ullman) | mop-vs-mfp-const, distributive-exact, mop-undecidable |
./course drill lattice-props --difficulty medium (distributivity) |
mop-mfp |
E1 (MFP = MOP tests) |
Pitfall
"MFP ⊑ MOP means MFP is more precise." It depends on the orientation. Kam and Ullman order facts downward, so their "\(\mathrm{MFP} \le \mathrm{MOP}\)" says MFP is lower, i.e. less informative. In this course facts grow upward and the same theorem reads \(\mathrm{MOP} \sqsubseteq \mathrm{MFP}\). Always check which way a paper's lattice points (Definition 14.2.3).
References¶
See the chapter references.