THE REACHING DEFINITIONS which assignment's value is still live here?
A reaching definition is an assignment whose value can still arrive at a program point without being overwritten on the way. Computing the set at every point is the archetypal dataflow analysis: each statement generates its own def and kills all other defs of the same variable, and the sets flow forward — OUT = gen ∪ (IN − kill) — iterated to a fixed point. Kildall's insight was that this, and liveness, and available expressions, are all the same computation over a lattice: monotone functions climbing to the least fixed point.
THE TECHNIQUE OUT = gen ∪ (IN − kill), iterated to a fixpoint
Three statements define variables; each gen-s its def and kills the others of that variable. The demo runs the forward transfer to the exit and shows which defs still reach — as a bitset: live demo
HISTORY & CREDIT Gary Kildall, 1973
“A variable has a value.” — at a given point it may have several possible values, one per definition that reaches it. Reaching definitions is the compiler admitting that uncertainty precisely: here is the exact set of assignments that could be the source. cited
1973 · Gary Kildall — “A Unified Approach to Global Program Optimization” (POPL): dataflow analysis as monotone functions over a lattice, solved by iteration to a least fixed point — reaching definitions, liveness, available expressions, one framework. with · Allen & Cocke — the gen/kill formulation of the transfer functions. now · the fixpoint solver at the heart of every optimizer; Kildall also wrote CP/M.
The lattice climbs and stops: monotone transfer functions guarantee a unique least fixed point. Convergence is not hoped for — it is proved by the algebra. Kildall 1973
RECOMMEND FOR I-13 reaching set at exit as a bitmask, computed
On the canonical compiler, over three statements (def a=0, def b=1, redef a=2), the reaching set at exit is {1,2} = bitmask 6 — b and the newest a survive, the old a is killed:
$ i13 run reaching.i13 # gen/kill forward transfer to exit
r = 6 -- bits {1,2}: def b and the new def of a reach; old def a killed
Recommend: a general reaching-definitions pass is the same fixpoint i13 already runs in miniature — its single-pass validator threads a live flag to prove return-totality (fall-through-without--> is rejected, E0401). That is a one-bit dataflow analysis. The full lattice version is the natural generalization; i13 kept the cheapest slice that serves its honesty goal rather than the whole framework, which is the right call for a verifier.