> For the complete documentation index, see [llms.txt](https://isubasinghe.gitbook.io/isithas-wiki/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://isubasinghe.gitbook.io/isithas-wiki/computer_science/programming_language_theory/optimisations/data_flow_analysis.md).

# 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.

## Key formulas

* Forward: $\mathrm{OUT}\[B] = f\_B(\mathrm{IN}\[B])$, $\mathrm{IN}\[B] = \bigsqcup\_{P \in \mathrm{pred}(B)} \mathrm{OUT}\[P]$
* Backward: $\mathrm{IN}\[B] = f\_B(\mathrm{OUT}\[B])$, $\mathrm{OUT}\[B] = \bigsqcup\_{S \in \mathrm{succ}(B)} \mathrm{IN}\[S]$
* Termination guaranteed for monotone $f$ on a finite-height lattice (Tarski).
* Examples: reaching definitions, live variables, available expressions, very-busy expressions.