nx_bck_elide.nx

nx_bck_elide.nx -- LN7 SOUND BOUNDS-CHECK ELISION (bck_elide_dominated). WHAT THIS IS. The consumer nx_opt.nx's own VRA header has NAMED and never built since v0.0.1: "opt_bounds_check_elim: drop array bounds checks when index is provably within range". This is that pass, and it is deliberately NOT the range-based version that comment imagines -- it is the DOMINANCE version, which needs no range lattice and whose soundness argument is short enough to be checked by eye. THE THEOREM. emit_bounds_check_v (nx_parse.nx) emits, for one access: b: c1 = idx >=s 0 ; br_cond c1 -> lo, fail lo: c2 = idx <s len ; br_cond c2 -> ok, fail fail: write(2,msg) ; exit_group(71) ; br ok ok: <the access> If a site S1 and a site S2 carry the SAME (idx value id, len constant) and S1's `ok` block DOMINATES S2's entry block, then S2's comparisons can only ever answer true, so making S2's two branches unconditional changes no observable behaviour. Why the facts still hold at S2: values here are SSA, so an id names one immutable quantity for the whole function; dominance says EVERY path from entry to S2 runs through S1's ok; and S1's ok is only entered with the facts established (see the four structural preconditions below). Nothing about the distance between the two sites, or what sits between them, can weaken that -- there is no store that can retarget an SSA id. WRONG IN THE DIRECTION OF KEEPING THE CHECK, BY CONSTRUCTION. Every predicate below is a REASON TO ELIDE; the default is to keep. An unrecognised shape, an unreadable value, a truncated CFG, a length that is not a constant -- all fall through to "keep the check". An unsound elision is a silent memory-safety hole: it deletes the check that would have caught a real overrun, and nothing anywhere reports it. So this file has no "probably" cases. THE FOUR STRUCTURAL PRECONDITIONS a site must meet before it may JUSTIFY an elision -- each one closes a way for `ok` to be entered WITHOUT the facts: (1) `lo` has exactly ONE predecessor, and it is `b`. Otherwise control could enter lo from elsewhere and take the true edge to ok having proven `idx < len` but never `idx >= 0`. (2) every predecessor of `ok` is `lo` or `fail`. Any third edge into ok reaches it with no facts at all. A pred count above the pred slots the struct actually has means the edge list is TRUNCATED and cannot be enumerated -- that is a refusal, not a pass. (3) `fail` provably does not return: it must contain a syscall whose number operand is the exit_group constant. This is the precondition it would be easiest to assume instead of