rocq/backend/Regs.v
# Whole-function register allocation and selection
A simple, loop-weighted interval register allocator and direct register emitter for the Gallina backend (M7 of docs/gallina-backend.md). It takes the func and plan that Validate.v and Abi.v produce, numbers the temporaries into nat identifiers so inner loops avoid term and string comparisons, assigns integer (w, l) temporaries and pointer (p) address words to the seven allocatable general registers (%r10, %r11, %rbx, %r12–%r15), checks the assignment with an executable validator (valid_alloc, proved sound in RegsProof.v), resolves phi edges by parallel moves without shadow slots, and selects scalar and address operations straight into their assigned registers.
Pointer lowers stay in their lowers[ ] frame roots so the collector scans every live capability at every safepoint, and temporaries live across any returning call take only callee-saved registers (%rbx, %r12–%r15), saved after the stack check and restored before every leave.
Allocatable registers
The seven general registers available for register homes: two caller-saved (%r10, %r11) and five callee-saved (%rbx, %r12–%r15), all disjoint from the emitter's scratch registers (%rax, %rcx, %rdx, %rsi, %rdi, %r8, %r9).
| | | HR10 | ||
| | | HR11 | ||
| | | HRbx | ||
| | | HR12 | ||
| | | HR13 | ||
| | | HR14 | ||
| | | HR15 |
Equality of hregs.
Whether r is preserved across SysV / Fil-C calls.
The five callee-saved registers, in prologue save order.
The caller-saved registers, tried first for non-call-crossing temporaries so callee-saved registers remain free across calls.
All seven allocatable registers.
64-bit AT&T name of r.
32-bit AT&T name of r.
16-bit AT&T name of r.
8-bit AT&T name of r.
Name of r at 32 bits (half = true) or 64 bits (half = false).
Name of r at store width w.
Tail-recursive nat sets and intervals
Fast nat comparisons through Nat.compare, avoiding Peano subtraction in extracted code.
Membership in a sorted listnat.
Equality of two sorted listnat ordsets.
Tail-recursive union accumulator for sorted listnats.
Tail-recursive difference accumulator for sorted listnats.
Sort and deduplicate a listnat.
Insert one nat into a sorted listnat.
A closed live interval [lo, hi] with lo ≤ hi.
Whether two sorted lists of disjoint closed intervals have no point in common.
Tail-recursive merge and coalescing of two sorted interval lists.
Whether any point in sorted pts lies inside sorted intervals ivs.
ZMap keyed by nat via Z.of_nat.
Plan uses, defs, calls and adjacent elisions
How an instruction invokes helper or target calls.
| | | RCallNone | ||
| | | RCallAfterReads | ||
| | | RCallDuringReads |
Temporary reads in a fast-call word.
Temporary reads in a generic cell.
Temporary definitions in call result channels.
Uses, definitions and call kind of one action.
Count every read of a temporary across all blocks of a plan.
| | | EPlain | idx : Z pi : pinst | |
| | | EFlightFused |
| | | EJumpPlain | j : pjump | |
| | | EJumpCmp | ||
| | | EJumpLetCmp |
Non-place uses of an access (its stored value, if any).
Whether o at integer class k computes directly into %rax without calls or float state.
Numbered CFG representation
| rb_idx | : nat | |
| rb_succs | : listnat × bool | |
| rb_phis | : listnat × listnat × optionnat | |
| rb_insts | : listrinst | |
| rb_jump_uses | : listnat |
Class table and numbering of temporaries defined in f.
Liveness over numbered blocks
Keep only temporaries belonging to keep (None keeps all).
Phi sources read on the edge pred_bi → rb.
Gen and Kill of one rblock.
LiveOut and LiveAcross of block bi given live_in.
Compute live_in, live_out, live_across over rbs.
Executable allocation validator
Check that no two temporaries in ts are assigned the same hreg in rm.
Check that every mapped temporary in ts holds a callee-saved register.
Backward check over the reversed instructions of one rblock.
Linear-time check that rm assigns only w, l or p-address temporaries, has no live register collision at any instruction, jump, phi header or entry, and assigns only callee-saved registers across calls and poll edges.
Loop depths, weights, exact intervals and priority coloring
Natural loop spans [sj, max_bi], one per loop header sj with a backward edge sj ≤ bi, so multiple continue edges to one header count as one loop rather than nested loops.
Phi partner edges so loop induction variables coalesce with their step temporaries.
Cap candidate set to the top 512 weighted eligible temporaries so pathological multi-thousand-temporary functions stay fast.
Sort weight, tid descending by weight, ties broken by smaller tid.
Build per-block [lo, hi] live sub-intervals and call-crossing flags over keep.
Priority coloring state: per-register union of assigned intervals.
Allocate registers for numbered blocks rbs, returning Somerm only when valid_alloc accepts rm.
Parallel moves for phi edges
A parallel-move location: an allocated hreg, a stack slot at -off(%rbp), or the cycle-breaking scratch register %rcx.
Whether m is a true no-op: identical source and destination, and either 64-bit or an already zero-extended 32-bit source.
Find a move in prefix_rev + rest whose destination is read by no other remaining move.
Load integer constant n at width half into dst64, dst32 without touching EFLAGS.
Function context and register-aware selection
Build the frame layout and rctx for p, adding save slots for the callee-saved registers that rm uses.
Load v at class k into the scratch short register r.
Load v at integer width half into dst64, dst32.
Store 64-bit register src64 into k (register home or frame slot).
Prologue, epilogue and phi edges
Exception exit with callee-saved registers restored.
Parallel-move construction for phis on edge from from.
Direct integer, comparison, flight and access selection
Source operand for a binary integer op (imm32, hreg, or frame slot) when available without a scratch register.
Compare x and y at integer class ck, setting EFLAGS for c.
Narrow source register of hr for ext_op.
Direct two-operand commutative ALU (and, or, xor) into dst64, dst32, where dst_hr is Somehr when targeting an allocatable register.
Direct integer Add with 3-address lea when operands live in registers distinct from the destination.
Direct integer Sub with lea on constant subtrahends.
Direct integer Mul, using 3-operand imul $imm, src, dst when multiplying by a 32-bit immediate.
Direct shift into dst64, dst32.
Division, float and x87 operations through %rax, reading and writing register homes via rload and rstore_key.
Emit integer operation o at class k into dst64, dst32.
Flight address calculation into dst64 (%rax or an hreg).
Raw loads and stores with direct register destinations/sources.
Calls and ABI actions
Emitting instructions, returns, branches and blocks
Top-level function and module emission
Compile f and its ABI plan p with register allocation, returning None if valid_alloc rejects the assignment.
Lines of one module item under register allocation.
Pieces of a module compiled with register allocation.