Skip to content

Chapter 14 · Dataflow Analysis & Abstract Interpretation

Part 3 · Analysis Foundations & SSA · about 3 weeks · Previous: Ch 13 · Next: Ch 15

The problem

You are given a function as a control-flow graph \(G = (N, E, r)\) and a question about its runs that must hold at every program point: which variables may still be read later (liveness), which stores may reach this load (reaching definitions), is a*b already computed on every path here (available expressions), is this variable surely initialized, what range can i take at the loop head? The exact answer — the join over all executions — is undecidable, so an analysis picks an abstraction: a lattice \(L\) of facts, a monotone transfer function \(f_n : L \to L\) per node, and a boundary value \(\iota\). The output is one fact \(\mathrm{IN}[n]\), \(\mathrm{OUT}[n]\) per block (or per SSA value, for sparse analyses) that is sound — it over-approximates every run — and as precise as the abstraction allows: the least fixed point of the dataflow equations (MFP), ideally equal to the meet over all paths (MOP). This chapter surveys how to state such analyses (lattices, monotone frameworks, Galois connections, Datalog), how to solve them (round-robin, worklists, bit vectors, elimination, sparse SSA propagation, widening) and the classic instances. In LLVM these are SparseSolver, SCCP, LazyValueInfo/ConstantRange, KnownBits, DemandedBits, MemorySSA, StackLifetime and codegen LiveVariables; in pebblec your framework runs as opt passes on the LLVM IR the front end emits, and its liveness, ranges and definite-initialization facts feed the pebble-uninit warning, the optimizations of Ch 17 and register allocation (Ch 22).

What you will be able to do

  • Decide whether a poset is a (complete) lattice, compute its height, and check monotonicity and distributivity of a transfer function; prove Knaster–Tarski and Kleene's theorem and use them to say which solution an analysis computes.
  • Formulate any analysis as a monotone-framework instance and fill in IN/OUT tables by hand for reaching definitions, liveness (also on SSA), available and very busy expressions, constant propagation and definite initialization.
  • Prove MOP ⊑ MFP, MFP = MOP for distributive frameworks, and the Kam–Ullman \(d(G) + 2\) bound; explain why MOP is undecidable in general.
  • Trace round-robin and worklist solvers (FIFO, LIFO, priority by RPO) step by step and predict their evaluation counts; implement them once, generically, behind pebble/include/pebble/Analysis/Dataflow.h.
  • Solve a gen/kill problem by elimination (Allen–Cocke intervals, structural analysis, path expressions) and a value problem sparsely on SSA (SCCP, sparse liveness, SEGs).
  • Design an abstract domain with a Galois connection, run intervals with widening and narrowing to a sound post-fixed point, and implement it for LLVM IR (print<pebble-intervals>).
  • Write an analysis as Datalog rules, evaluate them semi-naively, and explain how IFDS turns interprocedural distributive problems into graph reachability.
  • Find where LLVM 23, GCC, Clang, MLIR and rustc implement each of these, and reproduce their behaviour with opt, clang-23 and GCC dumps.

Prerequisites: Ch 8 (CFGs, basic blocks, DFS orders), Ch 9 (LLVM IR, alloca/load/store, phis), Ch 12 (new-pass-manager passes and analyses, lit + FileCheck). Lesson 14.6 uses dominance frontiers from Ch 15, Lesson 15.3; read that section first or take the frontier as a black box.

Notation

Shared notation follows the house notation: §1 (sets, functions, logic), §2 (orders and lattices), §3 (graphs and CFGs) and §7 (dataflow, SSA, IR). Orientation: facts grow up: the join \(\sqcup\) merges paths, \(\bot\) is "no information yet", and every analysis computes a least fixed point. Must-analyses (available expressions, very busy expressions, definite initialization) are the same theory on the dual of the subset order, so their \(\bot\) is the universe and their join is \(\cap\). Kam–Ullman and the Dragon book write the dual (meets, "MFP ≤ MOP"); Definition 14.2.3 translates. In this chapter:

Symbol Meaning
\((L, \sqsubseteq)\), \(\sqcup\), \(\sqcap\), \(\bot\), \(\top\) a lattice, its order, join, meet, least and greatest elements (Definitions 14.1.1–14.1.3)
\(h(L)\) height: the most strict steps on a chain (Definition 14.1.6)
\(\mathcal{P}(S)\), \(L_1 \times L_2\), \(X \to L\), \(S_\bot^\top\) powerset, product, map and flat lattices (Definition 14.1.7)
\(\mathrm{lfp}(F)\), \(\mathrm{gfp}(F)\), \(F^{k}(\bot)\) least and greatest fixed points, Kleene iterates (Definitions 14.1.11, Theorem 14.1.14)
\(G = (N, E, r)\), \(G^{R}\) flowgraph with entry \(r\); the reverse graph for backward problems (Definition 14.2.1)
\(n = \lvert N \rvert\), \(e = \lvert E \rvert\) numbers of nodes and edges
\((L, \mathcal{F})\) a monotone framework: lattice and a set of monotone functions closed under composition (Definition 14.2.2)
\((G, f, \iota)\), \(f_n\), \(f_{u \to v}\) a framework instance: transfer function per node (and optional per edge), boundary value (Definition 14.2.4)
\(f_p\), \(\mathrm{Paths}(n)\) path transfer function; paths from \(r\) to \(n\) (Definition 14.2.5)
\(\mathrm{IN}[n]\), \(\mathrm{OUT}[n]\) facts before and after node \(n\) (CFG orientation, also for backward problems)
\(\mathrm{MOP}\), \(\mathrm{MFP}\) meet-over-all-paths and maximal-fixed-point solutions (Definitions 14.2.6, 14.2.9)
\(\mathrm{gen}_n\), \(\mathrm{kill}_n\), \((G, K)\) gen and kill sets; the gen/kill function \(X \mapsto G \cup (X \setminus K)\)
\(\mathrm{use}(n)\), \(\mathrm{def}(n)\), \(\mathit{Vars}\), \(\mathit{Exprs}\) variables read before written / written in \(n\); universes (Definition 14.3.1)
\(d(G)\) loop connectedness: the most retreating edges on a cycle-free path (Definition 14.4.5)
\(w\), \(k\) machine word size; number of facts in a bit-vector universe
\(f^{*}\), \(I(h)\) closure \(\bigsqcup_{i \ge 0} f^{i}\) (Definition 14.5.1); Allen–Cocke interval with header \(h\) (Definition 14.5.3)
\(P(s, t)\), \(\cdot\), \(+\), \({}^{*}\) path expression and its operators (Definition 14.5.10)
\(\mathrm{DF}^{+}(S)\) iterated dominance frontier (as in Ch 15), used by SEGs (Definition 14.6.8)
\(\alpha\), \(\gamma\), \(\wp(\Sigma)\) abstraction and concretization of a Galois connection over sets of states (Definitions 14.7.1–14.7.2)
\(f^{\sharp}\), \(\alpha \circ f \circ \gamma\) abstract transformer; the best one (Lemma 14.7.3)
\([a, b]\), \(a + m\mathbb{Z}\) an interval; a congruence class (Definition 14.7.5)
\(\nabla\), \(\Delta\) widening and narrowing (Definition 14.7.9)
\(T_P\), \(\Delta R\) immediate-consequence operator of a Datalog program; the delta of relation \(R\) in semi-naive evaluation (Definition 14.8.2, Algorithm 14.8.4)
\(G^{\#}\), \(D\) exploded supergraph and the IFDS fact domain (Definitions 14.8.6–14.8.7)

Numbered statements are N.k.m (chapter, lesson, counter), as in NOTATION.md §9. The chapter's running example is one six-block loop (blocks A–F, variables a b i n s t u x) used in every lesson; its C version is tests/ch14/Inputs/c/running.c.

Technique map

Family Techniques (origin) Lesson
Lattice theory Partial orders, lattices, complete lattices and their constructions (Birkhoff; Tarski 1955 [Tar55]); monotone and distributive functions; Knaster–Tarski fixed-point theorem (Knaster 1928, Tarski 1955); Kleene iteration and its constructive versions (Kleene 1952; Cousot & Cousot 1979 [CC79b]) 14.1
Monotone frameworks Kildall's framework and iterative algorithm (Kildall 1973 [Kil73]); monotone frameworks, MOP vs MFP, soundness, distributivity, undecidability of MOP (Kam & Ullman 1976, 1977 [KU76, KU77]) 14.2
The classic analyses Reaching definitions and live variables (Allen 1970 [All70]; Allen & Cocke 1976 [AC76]); available expressions (Cocke 1970 [Coc70]; Ullman 1973 [Ull73]); very busy expressions / anticipability (Morel & Renvoise 1979 [MR79]); constant propagation (Kildall 1973); definite initialization (Java definite assignment [JLS]; Clang -Wuninitialized) 14.3
Iterative solvers Round-robin in RPO and postorder (Hecht & Ullman 1975 [HU75]; Kam & Ullman 1976); worklists: FIFO, LIFO, priority by RPO, SCC order (Kildall 1973; Cooper, Harvey & Kennedy 2004 [CHK04]; Bourdoncle 1993 [Bou93]); bit-vector implementations (Khedker & Dhamdhere 1994 [KD94]) 14.4
Elimination methods Allen–Cocke interval analysis (Allen & Cocke 1976 [AC76]; Graham–Wegman 1976 [GW76]); structural analysis (Sharir 1980 [Sha80]); path expressions (Tarjan 1981 [Tar81a, Tar81b]); survey (Ryder & Paull 1986 [RP86]) 14.5
Sparse analysis Def-use chains; SSA-based sparse propagation: sparse constant propagation and SCCP (Wegman & Zadeck 1991 [WZ91]), sparse SSA liveness (Brandner et al. 2011 [BBD+11]); sparse evaluation graphs (Choi, Cytron & Ferrante 1991 [CCF91]) 14.6
Abstract interpretation Galois connections and sound transformers (Cousot & Cousot 1977, 1979 [CC77, CC79]); signs, constants, intervals (Cousot & Cousot 1976 [CC76]), congruences (Granger 1989 [Gra89]); octagons (Miné 2006 [Min06]), polyhedra (Cousot & Halbwachs 1978 [CH78]); widening and narrowing (Cousot & Cousot 1976, 1992 [CC92]) 14.7
Declarative analysis Datalog: least models, naive and semi-naive evaluation, stratified negation (Bancilhon & Ramakrishnan 1986 [BR86]; Abiteboul, Hull & Vianu 1995 [AHV95]); bddbddb (Whaley & Lam 2004 [WL04]), Doop (Bravenboer & Smaragdakis 2009 [BS09]), Soufflé (Jordan, Scholz & Subotić 2016 [JSS16]) 14.8
Interprocedural preview IFDS (Reps, Horwitz & Sagiv 1995 [RHS95]); IDE (Sagiv, Reps & Horwitz 1996 [SRH96]) — continued in Ch 20 14.8 
flowchart LR
  T[Knaster–Tarski 1955<br/>Kleene iteration] --> K[Kildall 1973<br/>iterative framework]
  K -->|monotone, MOP vs MFP| KU[Kam–Ullman 1976/77]
  KU -->|visiting order, d+2| RR[Round-robin RPO<br/>Hecht–Ullman 1975]
  RR -->|visit only changed nodes| WL[Worklists: FIFO / LIFO /<br/>priority RPO / SCC]
  RR -->|word-parallel sets| BV[Bit vectors]
  K -->|solve by graph reduction| AC[Allen–Cocke intervals 1976]
  AC -->|more schemas, control tree| SA[Structural analysis<br/>Sharir 1980]
  AC -->|regular expressions over paths| PE[Path expressions<br/>Tarjan 1981]
  K -->|facts on values, not points| DU[Def-use chains]
  DU -->|SSA edges| SSA[SCCP 1991<br/>sparse SSA liveness]
  DU -->|per-problem sparse graph| SEG[SEGs<br/>Choi–Cytron–Ferrante 1991]
  T -->|abstraction α/γ| AI[Abstract interpretation<br/>Cousot–Cousot 1977]
  AI --> NR[Signs, constants,<br/>intervals, congruences]
  AI --> RD[Octagons 2006<br/>polyhedra 1978]
  NR -->|infinite height| WN[Widening / narrowing]
  K -->|facts as relations| DL[Datalog: semi-naive<br/>Doop, Soufflé]
  K -->|interprocedural, distributive| IF[IFDS 1995 / IDE 1996]
  IF -.->|same fixpoint as| DL

Who uses what

System Technique Notes
LLVM 23 SSA-based sparse propagation (SCCP/IPSCCP over ValueLatticeElement), SparseSolver; intervals as ConstantRange in SCCP and LazyValueInfo; congruences as KnownBits; backward def-use propagation in DemandedBits; a sparse evaluation graph for memory (MemorySSA) Lessons 14.1, 14.6, 14.7
LLVM 23 CodeGen Round-robin over bit vectors (StackLifetime), sparse SSA liveness of virtual registers (LiveVariables), reaching definitions after register allocation (ReachingDefAnalysis) Lessons 14.3, 14.4, 14.6
GCC 15 RTL dataflow framework (df-core.cc): bit-vector problems (DF_LR, DF_RD, …) on a worklist in postorder; Wegman–Zadeck CCP on GIMPLE SSA; on-demand ranges (Ranger); -Wmaybe-uninitialized Lessons 14.3, 14.4, 14.6, 14.7
Clang 23 -Wuninitialized / -Wsometimes-uninitialized (definite initialization on a worklist over packed 2-bit values); the FlowSensitive dataflow framework used by clang-tidy checks; static analyzer: path-sensitive symbolic execution, live variables, range constraints and loop widening Lessons 14.1, 14.3, 14.7
MLIR DataFlowSolver with sparse (constant propagation, integer ranges, dead code) and dense analyses, liveness Lessons 14.2, 14.6, 14.7
rustc MIR dataflow framework: JoinSemiLattice domains, RPO-seeded worklist; maybe-uninitialized places and liveness for the borrow checker Lessons 14.1, 14.3, 14.4
Soufflé, Doop, CodeQL Datalog-based analysis with semi-naive evaluation; points-to analysis (Doop), security queries (CodeQL) Lesson 14.8
Astrée, isl / Polly Relational domains: octagons in Astrée; polyhedra (Presburger sets) in isl, which Polly uses Lesson 14.7

Comparison

One row per technique, the same rows as the lessons' §8 tables (the lesson has the "Choose it when…" paragraphs).

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)
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*)
Reaching definitions Exact (distributive): MFP = MOP \(\le d + 2\) bit-vector passes Use-def chains; quadratic sets without SSA Low (gen/kill) Memory SSA construction, post-RA register reasoning
Live variables Exact (distributive) \(\le d + 2\) passes on \(G^{R}\) Live sets per block; SSA version needs phi conventions Low Register allocation, DCE, pruned SSA
Available expressions Exact (distributive), must \(\le d + 2\) passes Redundant expressions to delete Low Global CSE; availability half of PRE
Very busy expressions Exact (distributive), must, backward \(\le d + 2\) passes Hoisting points Low Code hoisting; anticipability half of PRE
Constant propagation Sound, below MOP (not distributive) \(\le 2\lvert \mathit{Vars} \rvert\) height; 2–3 passes Constants per point Low–medium (lattice of maps) Folding; superseded by SCCP
Definite initialization Exact for its definition; path-insensitive as available expressions Warnings with "is/may" Low -Wuninitialized, Java/C# definite assignment
Round-robin iteration Exact MFP (Theorem 14.4.4) \(\le d + 2\) passes in RPO for rapid problems; \(\Theta(n)\) passes in postorder on a loop chain Pass count is a simple progress measure Lowest Small analyses; bit-vector problems with small \(d\) (LLVM StackLifetime)
Worklist algorithms Exact MFP Visits only nodes with changed inputs; priority-by-RPO is near-optimal on reducible CFGs Evaluation count per node Low–medium (a queue + membership bits) Production solvers (GCC df, Clang, rustc, SCCP)
Bit-vector implementations Same fixed point; only for powerset lattices \(\lceil k / w \rceil\) word operations per set operation — Low Classic analyses; any finite-universe powerset lattice
Allen–Cocke interval analysis MOP for distributive frameworks with closure; reducible CFGs only (or node splitting) \(O(\ell (n + e))\) algebra operations Loop summaries reusable after edits Medium: interval partition + function algebra Historical (IBM compilers); the definition of reducibility
Structural analysis Same, plus precise schemas; improper regions iterate near-linear on structured code A control tree mirroring the source High: many schemas Region-based optimization, decompilers, GPU structurizers
Tarjan's path expressions MOP for any problem with a closed semiring of functions \(O(e\,\alpha(e,n))\) on reducible CFGs Symbolic path summaries, reusable across problems High Algebraic program analysis; theory; closed-form loop summaries (SCEV)
Def-use chains Same as dense for per-value problems (Theorem 14.6.3) \(O(h \cdot U)\); skips irrelevant blocks Facts per value, not per point Low on SSA; quadratic chains without it DemandedBits, value-lattice analyses
SSA-based sparse propagation SCCP: strictly more than CP + UCE; sparse liveness = dense liveness Linear (SCCP); proportional to live ranges (liveness) Per-value lattice, executable edges Medium (two worklists) SCCP/CCP in every compiler; codegen liveness
Sparse evaluation graphs Same as dense MFP for any monotone problem (Theorem 14.6.10) Near-linear per problem after DF+ A per-problem sparse graph High (per-problem construction) MemorySSA; sparse memory analyses
Galois connections Defines the best transformer; soundness by construction — Proof obligations per operation Conceptual Designing and proving analyses
Non-relational domains (signs, constants, intervals, congruences) One property per variable; no correlations \(O(1)\) per operation Ranges, constants, parities per value Low Compilers: LVI, ConstantRange, KnownBits, Ranger, E6
Relational domains (octagons, polyhedra) Linear relations (\(\pm x \pm y \le c\); any linear) Octagons \(O(v^3)\); polyhedra exponential Invariants such as \(i = j\), \(j = 2i\) High (DBMs, double description) Verifiers (Astrée, IKOS, EVA); polyhedral loop optimization (Polly)
Widening and narrowing Sound post-fixed point; narrowing recovers bounds \(\le 2\) jumps per bound Loss of bounds that only a later test restores Low Every analysis over an infinite-height domain
Datalog-based analysis Least model = MFP for set-based (finite, monotone) analyses; any relation-valued analysis Semi-naive: each derivation once per new tuple; Soufflé-compiled near hand-written speed Relations queryable afterwards; derivations explainable (provenance) Very low per analysis (rules), high for the engine Points-to (Doop), security queries (CodeQL), rapid prototyping
IFDS/IDE Exact over realizable paths for distributive problems (MVP) \(O(E D^{3})\) Context-sensitive facts per node Medium (tabulation + flow functions) Interprocedural taint, uninitialized variables, typestate, linear constants

Comparison-lab results (reference solution in the course's Linux container; evaluation and derivation counts are deterministic, the millisecond timings are machine- and run-dependent — a second run measured 30, 158 and 20 ms for Part 1 and 272 / 17.6 ms for Part 3; reproduce with build/<preset>/bin/ch14-solverbench after E1, E2 and L1, and uv run python labs/ch14-dataflow/datalog/compare.py --chain 60 after L3):

  • Solver orders (Part 1, random CFGs with 10 000 blocks, 256 facts): RPO round-robin 6 passes (60 000 evaluations, 16 ms), postorder round-robin 69 passes (690 000, 149 ms), FIFO worklist 46 448 evaluations (18 ms). On a 1024-block loop chain postorder needs 1 049 600 evaluations, RPO 3 072 (Part 2).
  • Dense vs sparse liveness (Part 3, 5 000 blocks, 15 019 SSA values): dense bit-vector liveness 228 ms, sparse path exploration 14.6 ms.
  • Naive vs semi-naive Datalog (transitive closure of a 60-node chain): 71 980 vs 1 770 derivations, 2 094 ms vs 54 ms.

Route through this chapter

Step What Techniques How it is exercised
1 Lesson 14.1 lattices, Knaster–Tarski, Kleene drills lattice-props, widening; quiz; flashcards
2 Lesson 14.2 Kildall, monotone frameworks, MOP/MFP quiz; MFP = MOP property tests in E1
3 Lesson 14.3 reaching definitions, liveness, available / very busy expressions, constant propagation, definite initialization drill dataflow-table; Pebble implements liveness (E2), reaching stores (E3), definite initialization (E4), pebble-uninit (E5)
4 Lesson 14.4 round-robin, worklists, bit vectors drill worklist-trace; Pebble implements all five solver strategies (E1); lab ch14-solverbench Parts 1–2
5 Lesson 14.5 Allen–Cocke, structural analysis, path expressions theory + drill dataflow-table (the same fixed point) + quiz
6 Lesson 14.6 def-use chains, SCCP, sparse liveness, SEGs lab L1 (sparse liveness) vs E2 (dense), ch14-solverbench Part 3
7 Lesson 14.7 Galois connections, non-relational and relational domains, widening/narrowing drill widening; Pebble implements intervals with widening and narrowing (E6), soundness against concrete runs
8 Lesson 14.8 Datalog, IFDS/IDE lab L3 (semi-naive engine), L4 (liveness rules) checked against E2
9 Exercises Pebble uses a generic worklist solver (priority by RPO) with dense bit-vector instances and an interval analysis ./course test 14
10 Comparison lab labs/ch14-dataflow/ round-robin vs worklist orders vs sparse; C++ vs Datalog lab tests + measurements
11 Theory test all ./course quiz 14 (≥ 80 % to finish)

Practice and check

./course drill dataflow-table --difficulty easy   # IN/OUT tables for the four classics
./course drill worklist-trace                     # predict every pop of a worklist
./course drill lattice-props                      # lattice? height? monotone? distributive?
./course drill widening                           # interval iterates with widening and narrowing
./course flash 14                                 # daily, a few minutes
./course quiz 14                                  # after the lessons
./course test 14                                  # after the exercises
./course status                                   # done = quiz ≥ 80 % and tests pass

References

The chapter's annotated bibliography — papers, textbook sections, pinned source files and docs — is in references.md. Start with: [Kil73] (where iterative dataflow analysis begins), [KU77] (MOP, MFP and why they differ), [SPA] (a free, modern textbook covering Lessons 14.1–14.4 and 14.7), [CC77] (abstract interpretation), and [WZ91] (SCCP, the sparse analysis every compiler runs).