Monotone Dataflow: Lattices, Transfer Functions, and Fixpoints

A linter that asks “is this variable read after it is written here” is doing dataflow analysis, whether or not it uses that name. So is a check for a use of an uninitialised variable, a null dereference along some path, or a lock released on one branch but not another. The questions differ in direction and in what counts as a fact, but the machinery is shared: a lattice of facts, transfer functions for statements, and a fixpoint over the control-flow graph.

Four choices define an analysis

Every classic dataflow analysis is specified by four decisions.

The first is direction. A forward analysis computes facts about the program state before each statement from facts about its predecessors. A backward analysis computes facts about what will happen after a statement from its successors. Reaching definitions, available expressions, and constant propagation are forward. Liveness and very busy expressions are backward. Direction is a property of the question, not a matter of taste: “which definitions can reach this use” flows with execution, while “will this value be needed later” flows against it.

The second is the lattice. The analysis assigns each program point an element of a partially ordered set, with a join or meet operation that combines facts from multiple paths. The order encodes precision: smaller elements are more precise in a may analysis, larger ones more precise in a must analysis, and the top and bottom elements represent “no information” and “contradiction” in a way that depends on the direction of the order. Confusing which end is which is the most common source of analyses that report everything or nothing.

The third is the transfer function. Each statement maps an input fact to an output fact. For reaching definitions, a statement that assigns to x kills the definitions of x that reach it and generates a new definition. For liveness, a statement generates the variables it reads and kills the variables it writes. The function must be monotone with respect to the lattice order: a more precise input may not produce a less precise output. Monotonicity is what makes the fixpoint iteration converge to a unique least fixpoint.

The fourth is the merge policy. At a join point, a may analysis takes the union of incoming facts, because a fact that holds on any path is possible. A must analysis takes the intersection, because a fact that holds only on some paths is not guaranteed. This is where the may/must distinction becomes operational, and it is also where precision is lost: merging paths discards the correlation between facts that held on each one.

The worklist, and why it terminates

The naive algorithm initialises every program point to the bottom (or top) element and repeatedly applies transfer functions to every node until nothing changes. The worklist version is the same computation with an efficiency trick: when a node’s output changes, only its successors need to be re-examined, so they are pushed onto a queue.

Termination follows from two properties. The lattice must have finite height, meaning there is no infinite strictly ascending chain, and the transfer functions must be monotone. Each update moves a node’s fact strictly upward in the lattice, and the height bounds the number of times any node can change. For a lattice of sets over a finite universe, the height is the size of the universe, so the worst case is proportional to the number of nodes times the number of facts, though real programs converge far faster because most updates propagate a small distance.

Ordering the worklist matters in practice. Processing nodes in reverse postorder tends to visit definitions before their uses, so forward analyses reach a fixpoint in few passes. A queue that processes in arbitrary order still terminates but may do substantially more work. The same reverse-postorder idea underlies the dominance algorithm in Control-Flow Graphs and Dominance.

def liveness(cfg, use, defs):
    live_in = {n: set() for n in cfg.nodes}
    live_out = {n: set() for n in cfg.nodes}
    work = list(cfg.nodes)
    while work:
        n = work.pop()
        out = set().union(*(live_in[s] for s in cfg.succ[n])) if cfg.succ[n] else set()
        inn = use[n] | (out - defs[n])
        if out != live_out[n] or inn != live_in[n]:
            live_out[n], live_in[n] = out, inn
            work.extend(cfg.pred[n])
    return live_in, live_out

A variable is live at a point if some path from that point reads it before writing it. The analysis is backward, the merge is union, and the transfer function removes definitions and adds uses. The result answers “is this assignment dead” by checking whether the assigned variable is live immediately after the assignment, which is the basis for the dead-store rule in most linters.

May and must are not the same lattice

Reaching definitions is a may analysis: a definition reaches a point if there exists a path from the definition to the point with no intervening kill. The lattice is the powerset of definitions, ordered by subset, and the merge is union. Its complement, “every path from this point to exit is preceded by a definition”, is a must property and needs intersection and a reversed order.

Available expressions is the standard must example. An expression is available at a point if every path to that point evaluates it and no operand is redefined afterwards. The merge is intersection, and the initial value at entry is the empty set for a forward may analysis but the full set for a forward must analysis. Mixing these up produces an analysis that claims availability after a branch that skips the computation, which is exactly the kind of false negative that makes a linter untrustworthy.

The naming of top and bottom is a perennial trap. In the subset order, bottom is the empty set and top is the universe. For a may analysis, bottom means “nothing is possible” and is the optimistic starting point; for a must analysis, top means “everything is guaranteed” and is the optimistic starting point. Implementations that share a lattice library across both often encode the starting value as a flag rather than relying on the name, because the same lattice element plays opposite roles.

Precision is lost at merges and at calls

The framework is sound but not precise, and the imprecision has identifiable sources. The first is path merging. At a join, the analysis keeps one fact per program point, so it cannot represent “x is 1 on this path and 2 on that one”. It represents the join, which is “x is 1 or 2”. Any later question that depends on the correlation between x and another variable is unanswerable. This is the core of the path-sensitivity trade-off examined in Path Sensitivity and Branch Correlation.

The second is the treatment of calls. A call is often modelled as a transfer function that kills everything the callee might modify, or as a summary computed once per function. The first is sound and imprecise; the second is precise only if the summary is context-independent, which it usually is not. Interprocedural analyses extend the lattice to include call strings or summaries, at a cost that grows quickly.

The third is the heap. A local variable’s definition is easy to track because the variable is a syntactic object. An object field is not: two expressions may refer to the same object, and a write through one aliases the other. Without alias information, a field write must kill every fact about every field of the same type, which is why alias analysis and dataflow precision are linked. The may-alias relation is covered in May-Alias Analysis and Points-To Sets.

A fourth source is non-distributivity. Constant propagation over a lattice of values is not distributive: merging two paths first and then evaluating a condition can lose a fact that evaluating on each path separately would preserve. The analysis remains sound, but it will fail to prove that a branch is dead when each path individually would prove it. This is a fundamental limit of the bit-vector framework, not an implementation bug, and it is why more precise analyses move to disjunctive or path-based representations.

Choosing the abstraction is the design act

The framework does not dictate what a fact is. That choice determines both cost and usefulness. Tracking a boolean per variable is cheap and answers definite-assignment questions. Tracking a small set of constants answers branch feasibility and dead-code questions. Tracking a full interval or a points-to set answers more, and costs more in both time and memory.

The practical discipline is to pick the weakest abstraction that answers the question being asked, and to document what it cannot answer. An analysis that reports “this may be null” from a lattice that cannot distinguish “definitely null” from “unknown” will produce a stream of findings that are technically true and operationally useless. The fix is not a bigger lattice by default; it is a lattice whose elements correspond to distinctions the rule actually uses.