Flashcards — Chapter 14¶
80 cards. Review them with spaced repetition in the terminal (./course flash 14) or export them to Anki (./course flash export 14). Here, click a card to reveal its back.
lattice¶
What is a complete lattice?
A partial order in which every subset has a least upper bound (join) and a greatest lower bound (meet). Finite lattices are complete (Lemma 14.1.4).
Heights of the standard constructions?
h(P(S)) = |S|; h(L1 × L2) = h(L1) + h(L2); h(X → L) = |X|·h(L); flat lattice S⊥⊤: 2 (Proposition 14.1.8).
Why does every analysis in Ch 14 terminate (without widening)?
Built from powersets, products, maps and flat lattices over finite index sets → finite height; monotone transfer functions → each value rises at most h times.
Which LLVM type is the lattice of SCCP and LazyValueInfo?
ValueLatticeElement (llvm/Analysis/ValueLattice.h): unknown, undef, constant, notconstant, constantrange, overdefined; mergeIn is the join.
tarski¶
Knaster–Tarski theorem?
A monotone f on a complete lattice has a complete lattice of fixed points; lfp(f) = ⊓{x | f(x) ⊑ x}, gfp(f) = ⊔{x | x ⊑ f(x)}.
Monotone vs distributive?
Monotone: x ⊑ y ⇒ f(x) ⊑ f(y). Distributive: f(x ⊔ y) = f(x) ⊔ f(y). Distributive implies monotone (Lemma 14.1.10), not conversely (constant propagation).
Why do analyses want the least fixed point?
Every fixed point of the equations is sound only if it is above the collecting semantics; the least one is the most precise solution of those equations. Starting from ⊤ converges to a useless one.
kleene¶
Kleene iteration?
x0 = ⊥, x(k+1) = F(xk) until stable. On finite height it stops after ≤ h(L)+1 applications and returns lfp(F) (Theorem 14.1.14).
Key invariant of Kleene iteration?
Every iterate F^k(⊥) is ⊑ lfp(F) and the chain is ascending (Lemma 14.1.16). Stopping early under-approximates: unsound for a may-analysis.
Cost of Kleene (Jacobi) iteration on a dataflow system?
≤ h+1 rounds, each evaluating all 2n components: the running example needs 7 rounds = 42 evaluations vs 18 (round-robin RPO) or 8 (worklist).
framework¶
Monotone framework (Kam–Ullman)?
(L, F): L a complete lattice with ACC, F a set of monotone functions containing id and closed under composition. Instance: (G, f: N → F, boundary value ι).
Kildall's algorithm?
Worklist of nodes; pop m, apply f_m to IN[m], join into each successor's IN; re-add a successor whose IN changed. Terminates with MFP (Theorem 14.2.11).
Cost of Kildall's algorithm?
Each IN rises ≤ h times, each rise re-queues the node's out-edges: O(e·h) transfer/join operations (Proposition 14.2.15).
mop-mfp¶
MOP solution?
MOP(n) = ⊔ over all paths p from r to n of f_p(ι): the most precise answer any flow-sensitive, path-insensitive analysis can give.
MOP vs MFP (this course's orientation)?
MOP ⊑ MFP always (soundness, Theorem 14.2.12); MOP = MFP when all transfer functions are distributive (Theorem 14.2.13). Kam–Ullman write the dual: MFP ≤ MOP.
Is MOP computable?
Not in general: Kam–Ullman reduce Post's correspondence problem to MOP for a monotone (non-distributive) framework (Theorem 14.2.14). MFP always is (finite height).
reaching-definitions¶
Reaching definitions equations?
Forward, may: IN[B] = ∪ OUT[P]; OUT[B] = gen[B] ∪ (IN[B] ∖ kill[B]); gen = last def of each var in B, kill = other defs of vars defined in B.
What do reaching definitions give a compiler?
Use-def chains (which definitions may reach a use); in LLVM: mem2reg's phi placement for memory, ReachingDefAnalysis after register allocation.
Cost of reaching definitions with bit vectors?
≤ d(G)+2 RPO passes, each O(n·⌈D/w⌉) word ops for D definitions (Proposition 14.3.22).
liveness¶
Liveness equations?
Backward, may: OUT[B] = ∪ IN[S]; IN[B] = use[B] ∪ (OUT[B] ∖ def[B]), use = upward-exposed uses.
SSA liveness: where is a phi operand used?
At the end of the incoming predecessor (live-out of that predecessor only); the phi result is defined at the top of its block and is not live-in there (Definition 14.3.9).
Who consumes liveness?
Register allocation (interference), dead-code elimination, pruned SSA construction, stack coloring (LLVM StackLifetime).
available-expressions¶
Available expressions equations?
Forward, must: IN[B] = ∩ OUT[P] (IN[entry] = {}); OUT[B] = e_gen[B] ∪ (IN[B] ∖ e_kill[B]); every non-entry point starts at the universe.
What does an available expression enable?
Global CSE: if ab is available at a computation of ab, reuse the earlier value; the availability half of PRE (LLVM EarlyCSE, GVN).
Why initialize available expressions to the universe?
It is ⊥ of the must order; starting from {} gives a smaller, useless fixed point in which nothing survives a loop's back edge.
very-busy-expressions¶
Very busy (anticipable) expressions?
Backward, must: e is very busy at p if every path from p evaluates e before any operand changes. OUT[B] = ∩ IN[S]; IN[B] = e_use[B] ∪ (OUT[B] ∖ e_kill[B]).
What are very busy expressions used for?
Code hoisting: an expression very busy at a point can be computed once there (LLVM GVNHoist); the anticipability half of PRE / lazy code motion.
Cost of very busy expressions?
Same as the other gen/kill classics: rapid, ≤ d+2 passes on the reverse graph, O(⌈E/w⌉) per transfer.
constant-propagation¶
Constant-propagation lattice?
Vars → Z⊥⊤ pointwise; height 2|Vars| though Z is infinite (Definition 14.3.16).
Why is constant propagation not distributive?
x=2,y=3 on one path and x=3,y=2 on another: z=x+y is 5 on both (MOP) but joining first gives x=y=⊤, z=⊤ (MFP).
What improves on simple constant propagation?
Wegman–Zadeck SCCP: sparse over SSA and tracks executable edges, so it also removes unreachable code and finds more constants (Lesson 14.6).
definite-init¶
Definite initialization?
Forward must-analysis: x is definitely initialized at p if every path from entry to p stores x. IN = ∩ OUT[P], IN[entry] = {}, OUT = IN ∪ stored(B).
is uninitialized vs may be uninitialized?
Warn when not definitely initialized (must); say 'is' when no store reaches the load on any path (reaching stores empty), else 'may be'.
Who implements definite initialization?
Clang -Wuninitialized/-Wsometimes-uninitialized (UninitializedValues.cpp), GCC -Wmaybe-uninitialized, Java definite assignment (JLS ch. 16), rustc MaybeUninitializedPlaces.
round-robin¶
Round-robin iteration?
Sweep all nodes in a fixed order, updating in place, until a whole sweep changes nothing (Algorithm 14.4.1).
Kam–Ullman d+2 bound?
For rapid frameworks (all gen/kill problems), round-robin in RPO needs ≤ d(G)+2 passes, d = max back edges on a cycle-free path (Theorem 14.4.6).
Why not postorder for a forward problem?
Facts then advance one block per pass: a loop chain of n blocks needs n+1 passes (Θ(n²) evaluations) instead of 3 (Proposition 14.4.10).
worklist¶
Worklist algorithm?
Keep only nodes whose inputs may have changed; pop, recompute, push dependents if the output changed (Algorithm 14.4.2).
Does worklist order change the result?
No: every fair order returns MFP (Theorem 14.4.4); order changes only cost. Priority by RPO is near-optimal on reducible CFGs.
Which worklists do production solvers use?
RPO-priority: Clang ForwardDataflowWorklist, rustc (seeded in RPO), GCC df_worklist_dataflow (postorder index); SCCP uses instruction and block worklists.
bit-vector¶
Bit-vector transfer function?
OUT = gen | (IN & ~kill), word by word; join is | (may) or & (must) (Algorithm 14.4.8).
Cost of a bit-vector set operation?
⌈k/w⌉ word operations for k facts on a w-bit machine (Proposition 14.4.9): 300 facts = 5 words on 64-bit.
When do bit vectors apply?
Only to powerset lattices over a finite universe (the classics, stack slots, registers); value lattices like constants or intervals need other representations.
intervals¶
Allen–Cocke interval?
I(h): the maximal single-entry subgraph with header h, grown by adding nodes all of whose predecessors are already in it (Definition 14.5.3).
Interval elimination?
Summarize each interval by a transfer function (compose, join, closure), collapse to the derived graph, repeat until one node, then propagate back down (Algorithm 14.5.6). Reducible CFGs only.
Cost of interval elimination?
O(ℓ(n+e)) algebra operations, ℓ = length of the derived sequence (Proposition 14.5.13); needs a closure operation f*.
structural¶
Structural analysis (Sharir)?
Reduce the CFG bottom-up by matching region schemas (block, if-then(-else), self loop, while, natural loop, improper region) into a control tree; solve by schema formulas.
What does structural analysis do with irreducible regions?
Collapses them into an improper-region node and iterates inside it.
Structural analysis: trade-off?
Near-linear on structured code and yields reusable region summaries, but many schemas to implement; used by decompilers and GPU structurizers.
path-expressions¶
Tarjan's path expressions?
Compute a regular expression P(r, v) over edges denoting all paths to v, then interpret it: ∪ as join, · as composition, * as closure (Theorem 14.5.12).
Gen/kill algebra: composition and closure?
(G2,K2)∘(G1,K1) = (G2 ∪ (G1∖K2), K1 ∪ K2); join (G1∪G2, K1∩K2); (G,K)* = (G, ∅) (Lemma 14.5.2).
Cost of path expressions?
O(e·α(e,n)) on reducible graphs via the dominator tree (Tarjan 1981); O(n³) by simple state elimination.
def-use¶
Def-use chain?
A link from a definition to a use it may reach; the sparse representation of reaching definitions (Definition 14.6.1).
Size of def-use chains without SSA?
Quadratic: d definitions × u uses in the worst case; SSA with phis makes it linear (d + u edges).
Sparse = dense?
For per-value problems, propagating along def-use/SSA edges computes the same fixed point as the dense analysis (Theorem 14.6.3), at cost O(h·uses).
sparse¶
SCCP (Wegman–Zadeck)?
Two worklists: SSA edges and CFG edges. Only executable edges contribute to phis; branches on constants mark one edge executable (Algorithm 14.6.6).
Sparse SSA liveness?
For each use, walk backwards through predecessors marking live-in/out until reaching the definition or an already-marked block (Algorithm 14.6.4); cost ∝ total live-range size.
Where does LLVM use sparse propagation?
SCCPSolver (SCCP, IPSCCP), SparseSolver, DemandedBits (backward), CodeGen LiveVariables; MLIR's sparse dataflow analyses.
seg¶
Sparse evaluation graph (Choi–Cytron–Ferrante)?
Nodes: entry, blocks with non-identity transfer functions, and meet nodes at DF⁺ of them; edges bypass identity regions (Definition 14.6.8).
SEG correctness?
Solving the SEG gives the same MFP as the dense system at every original node (Theorem 14.6.10).
An SEG in LLVM?
MemorySSA: MemoryDefs at stores/calls, MemoryPhis at the iterated dominance frontier, MemoryUses linked to the reaching def.
galois¶
Galois connection?
α: C → A, γ: A → C with α(c) ⊑ a ⇔ c ⊆ γ(a) (Definition 14.7.2): α gives the best abstraction, γ the meaning.
Best abstract transformer?
f♯ = α ∘ f ∘ γ; any sound f♯ satisfies α ∘ f ∘ γ ⊑ f♯ (Lemma 14.7.3). E.g. x*x on [-2,3]: best [0,9], interval product [-6,9].
Fixed-point transfer theorem?
If f♯ soundly abstracts f, then α(lfp f) ⊑ lfp f♯: the abstract analysis over-approximates the collecting semantics (Theorem 14.7.4).
domains¶
Non-relational domains?
One abstract value per variable: signs, constants Z⊥⊤, intervals [a,b], congruences aZ+b. O(1) per operation; cannot express x = y.
Interval domain height?
Infinite (ascending chains [0,0] ⊏ [0,1] ⊏ …): needs widening to terminate.
Congruence join?
(aZ+b) ⊔ (cZ+d) = gcd(a, c, |b−d|)Z + b; e.g. 6Z+1 ⊔ 6Z+4 = 3Z+1.
Machine integers in interval analysis?
A non-nsw add that may overflow wraps, so the result is top; with nsw, overflow is poison and the exact range can be clipped (E6-R2; LLVM ConstantRange::addWithNoWrap).
relational¶
Octagon domain (Miné)?
Constraints ±x ±y ≤ c, stored as a 2v×2v difference-bound matrix; strong closure (Floyd–Warshall-like) O(v³) gives the tightest form (Theorem 14.7.8).
Polyhedra (Cousot–Halbwachs)?
Arbitrary linear inequalities; double description (constraints + generators), join = convex hull; exponential worst case.
What do relational domains buy?
Correlations: i = j or j = 2i survive widening, so a bound on i yields a bound on j (Astrée, IKOS; isl/Polly for polyhedra).
widening¶
Widening ∇?
An upper bound operator (x ⊔ y ⊑ x ∇ y) that makes every ascending chain x0, x1 = x0 ∇ f(x0), … stabilize (Definition 14.7.9). Intervals: unstable bounds jump to ±∞.
Narrowing Δ?
After widening reaches a post-fixed point, iterate x ← x Δ f(x) to recover bounds: intervals refine only infinite bounds; stays sound (Theorem 14.7.10).
Where to widen?
At a set of widening points cutting every cycle — loop heads. E6 widens only the head's phis so outer-loop values keep their bounds; widening with thresholds keeps constants like the loop bound.
datalog¶
Datalog semantics?
Least model of the rules = least fixed point of the immediate-consequence operator T_P (Definition 14.8.2); negation must be stratified.
Semi-naive evaluation?
Each round fires a rule once per recursive body atom restricted to the previous round's delta, so every derivation uses a new tuple (Algorithm 14.8.4). Transitive closure of an n-chain: n(n−1)/2 derivations.
Datalog analyzers?
bddbddb (BDDs), Doop (points-to for Java), Soufflé (compiled to parallel C++), CodeQL (queries).
ifds¶
IFDS?
Interprocedural, finite, distributive, subset problems solved as reachability over realizable paths in the exploded supergraph (Reps–Horwitz–Sagiv 1995).
Cost of IFDS tabulation?
O(E·D³) for E supergraph edges and D facts; path edges and summary edges are memoized per procedure.
IDE?
Extends IFDS with environment transformers (value lattices on each fact), e.g. linear constant propagation (Sagiv–Reps–Horwitz 1996).