Block A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval.
cfg.pl: cfg:reverse_postorder/6cfg.plreverse_postorder+Ns, +Succs, +Seen0, -Seen, +Post0, -PostPost is a reverse postorder, in front of Post0, of the block numbers reachable from Ns (depth first, each of Ns in turn) without passing through the bitset Seen0; Seen is Seen0 with those numbers. Succs is s(Ns1, Ns2, ...), each block's successors' numbers. orders the blocks, cfg:cfg_idoms/2cfg.plcfg_idoms+Cfg, -IdomdetIdom is the assoc Label -> immediate dominator, for the reachable labels other than the entry (Cooper, Harvey and Kennedy, "A Simple, Fast Dominance Algorithm"). finds each block's immediate dominator (idom), its parent in the tree, by Cooper, Harvey and Kennedy's fixpoint, cfg:dom_intervals/3cfg.pldom_intervals+Cfg, +Idom, -IntervalsdetIntervals is the assoc Label -> Pre-Last for every reachable label: Pre is the preorder number of Label in the dominator tree, and Last the last one in its subtree., cfg:dominates_by_interval/3cfg.pldominates_by_interval+Intervals, +A, +BsemidetA dominates B, in constant time, given Intervals from dom_intervals/3.; Cfg.v transcribes them as cfg_idoms, dom_intervals, dominates_by_interval and block_intervals.
Dominance.v proves the computed tree sound: dom_entry and dom_closed (a run enters only blocks with an interval), dom_edge (dominance survives an edge), dom_meet (what dominates every reachable predecessor dominates the block, from idoms_nca), dom_antisym, dominates_trans.
Readers: ir:definitions_dominate/3ir.pldefinitions_dominate+Fn, +Params, +BlocksdetIn every reachable block, each use of a temporary is dominated by one of its definitions: a parameter, an earlier instruction or phi of the same block, or one in a block that strictly dominates it. A phi reads its value at the end of the predecessor, if that is reachable. A temporary may be defined more than once (tests/fixtures/memory.ir); one dominating de… (ssastrict SSA nanofilStrict SSA is the form of a function in which every use of a temporary is dominated by a definition of it. nanofil uses the name in two strengths: the middle end's promote:strict_ssa/3 also asks that each temporary have exactly one definition, while the validator's ir:definitions_dominate/3 allows several and asks only that one dominate each use.), ir:site_dominates/4ir.plsite_dominates+Def, +L, +I, +Intervalsthe definition Def comes before position I of block L on every path from the entry. (sitesite nanofilA site is where a temporary is defined: param for a parameter, or at(L, I) for index I of block L, with phis at index -1. A site dominates a position when it comes before it on every path from the entry: the same block at an earlier index, or a block that strictly dominates it.), repeated gettersrepeated getter nanofilA repeated getter is a call of a getter that another call of the same getter dominates in the same activation: a single-definition let(tmp(D), p, copy, [global(G)]), G defined in this module with local linkage. The first call has returned, so the repeat takes the fast path: no safepoint, no free, no store. The evidence pass lets live facts survive it., and every reuse rule through single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point..
The subtlety: soundness only. The proof never shows the idoms are the true immediate dominators, and Cfg.v's fuel bounds stay unproved; a bound too small makes the validator reject a function, never accept a wrong one. Labels must be unique (no_dups).