rocq/backend/Liveness.v
Liveness of temporaries over fused blocks (cfg.pl's temp_liveness/3): the temporaries live on entry to and on exit from each block, reachable or not, the least solution of
- LiveOut(B) = the union over successors S of LiveIn(S) and the temporaries the phis of S read on the edge from B;
- LiveIn(B) = Gen(B) ∪ (LiveOut(B) − Kill(B)).
The frame layout (FrameSlots.v) reads it. The sets are ordsets of names in the standard order, as the Prolog compiler's are. A least solution is the same in whatever order the blocks are visited, so this visits them in rounds where cfg.pl keeps a worklist.
Sets of names
An ordset of names: sorted in the standard order, each once.
As sort/2 on names: the ordset of the names ns.
As ord_union/3 on names.
As ord_subtract/3 on names.
The ordset the map m has for the label l, empty if it has none.
Gen and Kill
A block's events so far: the names defined, the names read before any definition, and the names defined, in reverse order of event.
The events ev and then a use of n: n is read first if nothing defined it before.
The events ev and then a definition of n.
As block_gen_kill/3: Gen, the temporaries the block b reads before it writes them, and Kill, those it writes. Its events are the phi definitions, then each instruction's uses before its definitions, then the jump's uses.
Edge uses
As phi_edge_uses/2, for one block: each predecessor p of the block mapped to the ordset of the temporaries its phis read on the edge from p.
As phi_edge_uses/2: each block's label mapped to its block_edge_uses, for the blocks with phis.
The fixpoint
As live_out/5: the live-out set of the block l, whose successors are ss, given the live-in sets.
One round: each block of order in turn takes the live-in set its equation gives from the sets so far. The result has the new sets and whether any grew.
Up to 2^k rounds of step from m, stopping at the first that changes nothing; the flag says whether the last round run still changed something. The sets only grow, and there are finitely many names and blocks, so enough rounds reach the least solution.
As temp_liveness/3: the live-in and the live-out set of every block of bs, by label. The blocks are visited in postorder, a block after its successors where there is no cycle, then the unreachable ones; 2^40 rounds are more than any function needs.