nx_regalloc_interp.nx source

1// nx_regalloc_interp.nx -- EXECUTION-equivalence verifier for register allocation. 2// 3// The static soundness checker (nx_regalloc_linscan: no two live vregs share a 4// register) is necessary but the absorption gate wants more: PROVE that code run 5// THROUGH the allocation (values living in physical registers + spill slots) 6// computes the IDENTICAL result to the reference (one slot per value). Two 7// interpreters, compared 1:1 over many inputs -- if they ever diverge, the 8// allocation miscompiled (the g1 failure, caught before it can ship). 9// 10// The IR carries real opcodes so the interpretation is meaningful (it computes the 11// race kernel's actual arithmetic). live-out values (loop-carried) are kept live to 12// the block end so they remain readable -- exactly how a real backend treats them. 13 14import "nx_regalloc_linscan.nx" // chains in nx_syscalls + the allocator (single import path) 15 16const ROP_INPUT: i64 = 0 // imm = input index 17const ROP_MUL_IMM: i64 = 1 18const ROP_ADD_IMM: i64 = 2 19const ROP_SHR_IMM: i64 = 3 20const ROP_XOR: i64 = 4 21const ROP_AND_IMM: i64 = 5 22const ROP_ADD: i64 = 6 23const ROP_LT_IMM: i64 = 7 24 25const RI_SPILL: i64 = 0 - 1 26 27func ri_op_eval(op: i64, a: i64, b: i64, imm: i64) -> i64 { 28 if op == ROP_MUL_IMM { return a * imm } 29 if op == ROP_ADD_IMM { return a + imm } 30 if op == ROP_SHR_IMM { return a >> imm } 31 if op == ROP_XOR { return a ^ b } 32 if op == ROP_AND_IMM { return a & imm } 33 if op == ROP_ADD { return a + b } 34 if op == ROP_LT_IMM { if a < imm { return 1 } return 0 } 35 return 0 36} 37 38// where vreg v lives under this allocation (a register, or its spill slot). 39func ri_get(v: i64, alloc: *i64, regf: *i64, spill: *i64) -> i64 { 40 if alloc[v] >= 0 { return regf[alloc[v]] } 41 return spill[v] 42} 43 44// REFERENCE: one slot per vreg (always correct). Returns a checksum of the three 45// live-outs. 46func ri_interp_ref(n: i64, op: *i64, u0: *i64, u1: *i64, imm: *i64, inputs: *i64, 47 loa: i64, lob: i64, loc: i64) -> i64 { 48 let val: *i64 = sys_mmap(8 * n) 49 var i: i64 = 0 50 while i < n { 51 if op[i] == ROP_INPUT { val[i] = inputs[imm[i]] } 52 else { 53 var a: i64 = 0 54 var b: i64 = 0 55 if u0[i] >= 0 { a = val[u0[i]] } 56 if u1[i] >= 0 { b = val[u1[i]] } 57 val[i] = ri_op_eval(op[i], a, b, imm[i]) 58 } 59 i = i + 1 60 } 61 return val[loa] * 31 + val[lob] * 7 + val[loc] 62} 63 64// ALLOCATED: values live in regf[alloc[v]] or spill[v]. Same checksum -- must match 65// the reference iff the allocation is execution-correct. 66func ri_interp_alloc(n: i64, nreg: i64, op: *i64, u0: *i64, u1: *i64, imm: *i64, 67 alloc: *i64, inputs: *i64, loa: i64, lob: i64, loc: i64) -> i64 { 68 let regf: *i64 = sys_mmap(8 * nreg) 69 let spill: *i64 = sys_mmap(8 * n) 70 var i: i64 = 0 71 while i < n { 72 var v: i64 = 0 73 if op[i] == ROP_INPUT { v = inputs[imm[i]] } 74 else { 75 var a: i64 = 0 76 var b: i64 = 0 77 if u0[i] >= 0 { a = ri_get(u0[i], alloc, regf, spill) } 78 if u1[i] >= 0 { b = ri_get(u1[i], alloc, regf, spill) } 79 v = ri_op_eval(op[i], a, b, imm[i]) 80 } 81 if alloc[i] >= 0 { regf[alloc[i]] = v } else { spill[i] = v } 82 i = i + 1 83 } 84 return ri_get(loa, alloc, regf, spill) * 31 + ri_get(lob, alloc, regf, spill) * 7 + ri_get(loc, alloc, regf, spill) 85}