Home › Wiki › computer_science › programming_language_theory › optimisations › data_flow_analysis Data Flow Analysis Basic idea
Compute, for every program point, a conservative summary of all execution paths that could reach it. Framed as a fixpoint over a lattice: each instruction has a transfer function, joins use the lattice meet/join.
Forward: O U T [ B ] = f B ( I N [ B ] ) \mathrm{OUT}[B] = f_B(\mathrm{IN}[B]) OUT [ B ] = f B ( IN [ B ]) , I N [ B ] = ⨆ P ∈ p r e d ( B ) O U T [ P ] \mathrm{IN}[B] = \bigsqcup_{P \in \mathrm{pred}(B)} \mathrm{OUT}[P] IN [ B ] = ⨆ P ∈ pred ( B ) OUT [ P ]
Backward: I N [ B ] = f B ( O U T [ B ] ) \mathrm{IN}[B] = f_B(\mathrm{OUT}[B]) IN [ B ] = f B ( OUT [ B ]) , O U T [ B ] = ⨆ S ∈ s u c c ( B ) I N [ S ] \mathrm{OUT}[B] = \bigsqcup_{S \in \mathrm{succ}(B)} \mathrm{IN}[S] OUT [ B ] = ⨆ S ∈ succ ( B ) IN [ S ]
Termination guaranteed for monotone f f f on a finite-height lattice (Tarski).
Examples: reaching definitions, live variables, available expressions, very-busy expressions.