Every optimization is a claim that a rewrite preserves what the program does, and that claim cannot be made by looking at instructions one at a time. Deleting an assignment is safe only if nothing downstream reads it; removing a bounds check is safe only if the index can never leave the array. Each is a statement about every path through a function.

Mica derives those statements first, and the optimizer acts only on what was derived.

First the control flow graph

Basic-block construction follows the leader algorithm for three-address code: the first instruction is a leader, every branch target starts a block, and every instruction after a jump starts a new block. Edges follow the standard model: jumps contribute target edges, conditional jumps add a fallthrough, and epilogues terminate flow.

Loops come next. A depth-first postorder numbers the reachable blocks, a Cooper–Harvey–Kennedy fixpoint builds the immediate-dominator tree, and an interval numbering of that tree makes dominance constant-time: a dominates b exactly when a’s interval encloses b’s. An edge u → h whose target dominates its source is a back edge, h is a loop header, and the backward flood from u that stops at h gathers the natural loop body. Each block’s depth is the number of loop bodies containing it.

Depth is not decoration: register allocation weighs spill costs by it, because a value inside a loop is read as many times as the loop iterates — something its live-range length does not reveal.

Then two analyses, two questions

The liveness analysis runs backward and answers: at this program point, will name X be read before it is overwritten? Per block, Use(B) is the names read before being written in B, and Def(B) the names written anywhere in B.

LiveOut(B) = ∪ LiveIn(succ) over all successors of B
LiveIn(B)  = Use(B) ∪ ( LiveOut(B) \ Def(B) )

Reaching definitions runs forward and answers: at this use of name X, which definitions could have produced the value? Gen(B) is the value id of B’s last definition of each name, Kill(B) every other definition of the names B redefines.

ReachingIn(B)  = ∪ ReachingOut(pred) over all predecessors of B
ReachingOut(B) = Gen(B) ∪ ( ReachingIn(B) \ Kill(B) )

Both are may analyses, so union is the meet operator where control flow joins: a name is live if some future path reads it, a definition reaches a use if some path delivers it. Worklist iteration converges because the per-block transfer functions are monotone over a finite lattice — the powerset of names for liveness, of value ids for reaching definitions. This is the Kleene fixed-point theorem applied to dataflow. Termination is a proof, not a bail-out after a fixed number of rounds.

What the facts buy

Liveness produces gap-aware live ranges as half-open [start, end) intervals. A lifetime with a hole becomes several disjoint runs rather than invented names, so the emitter still sees one name per value and a gap marks a genuinely dead region. Those intervals drive interference, coalescing, and register assignment, with loop depth supplying the spill weights. The same result prunes φ placement, so a φ appears only where the variable is live at the merge.

Downstream of that pruned form, value-range propagation applies the same lattice discipline to intervals rather than sets: each value carries the [lower, upper] range it provably lies in, and a φ takes the hull of its inputs. Where an index provably stays inside a literal array extent, the bounds guard is removed outright.

The corpus draws that line. A counted loop folds to an exact interval and its guard goes:

    { the direct counted-loop shape: the counter itself is the index, the exact interval [0, 4095] }
    total := 0;
    for k := 0 to 4095 do
        total := total + a[k];

A while-loop counter is not the recognised shape, so its guard stays planted:

    total := 0;
    k := 0;
    while k < 64 do
    begin
        total := total + a[k * 64 + k];
        k := k + 1;
    end;

Both live in one corpus program whose totals match in every optimization mode.

These analyses are checked against themselves as well as against expected output: the fast dominator tree against an independent naive dominator-set computation for functions below a size bound, and the freshly constructed SSA form’s liveness against the trusted result, an identity oracle that holds before forwarding rewrites which values are live. A disagreement halts the compiler as an internal fault. The graph and the liveness solution are built on every compile, so they sit under the whole merge-gated corpus: 1,389 test programs and 8,436 declared runs.

See also