nx_regalloc_exec_test.nx source

1// nx_regalloc_exec_test.nx -- PROVE register-allocated execution is 1:1 with the 2// reference, on the race kernel's real arithmetic, over many inputs -- AND prove 3// the check CATCHES a corrupted allocation. This is the gate that makes absorbing 4// the allocator into codegen safe: any g1-style miscompile diverges here and fails. 5// 6// v0=INPUT c, v1=INPUT acc, v2=INPUT i 7// v3=c*K, v4=v3+A, v5=v4>>31, v6=v4^v5(c2,live-out), 8// v7=v6&M, v8=acc+v7(acc1,live-out), v9=i+1(i1,live-out), v10=v9<KK 9// 10// Known answer: allocation sound + 0 spills; ref==alloc for ALL random inputs; a 11// corrupted allocation (two overlapping vregs aliased to one register) DIVERGES 12// (the verifier catches the miscompile). exit 0. 13 14import "nx_regalloc_interp.nx" 15 16func re_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 17func re_emit(name: *u8, v: i64) -> i64 { 18 re_puts(name) 19 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 20 let t: *u8 = sys_mmap(28); var k: i64 = 0 21 if m == 0 { t[0] = 48; k = 1 } 22 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 23 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 24 b[k] = 10; sys_write(1, b, k + 1); return 0 25} 26 27const RE_N: i64 = 11 28const RE_NREG: i64 = 8 29const RE_TRIALS: i64 = 256 30const RE_K: i64 = 6364136223846793005 31const RE_A: i64 = 1442695040888963407 32const RE_M: i64 = 65535 33const RE_KK: i64 = 1000000 34 35func re_rng(s: i64) -> i64 { return s * 6364136223846793005 + 1442695040888963407 } 36 37func main() -> i64 { 38 re_puts("=== register-allocated execution == reference (1:1), race kernel ===\n" as *u8) 39 40 let op: *i64 = sys_mmap(8 * RE_N) 41 let u0: *i64 = sys_mmap(8 * RE_N) 42 let u1: *i64 = sys_mmap(8 * RE_N) 43 let imm: *i64 = sys_mmap(8 * RE_N) 44 // v0..v2 inputs 45 op[0] = ROP_INPUT; u0[0] = 0 - 1; u1[0] = 0 - 1; imm[0] = 0 46 op[1] = ROP_INPUT; u0[1] = 0 - 1; u1[1] = 0 - 1; imm[1] = 1 47 op[2] = ROP_INPUT; u0[2] = 0 - 1; u1[2] = 0 - 1; imm[2] = 2 48 op[3] = ROP_MUL_IMM; u0[3] = 0; u1[3] = 0 - 1; imm[3] = RE_K 49 op[4] = ROP_ADD_IMM; u0[4] = 3; u1[4] = 0 - 1; imm[4] = RE_A 50 op[5] = ROP_SHR_IMM; u0[5] = 4; u1[5] = 0 - 1; imm[5] = 31 51 op[6] = ROP_XOR; u0[6] = 4; u1[6] = 5; imm[6] = 0 52 op[7] = ROP_AND_IMM; u0[7] = 6; u1[7] = 0 - 1; imm[7] = RE_M 53 op[8] = ROP_ADD; u0[8] = 1; u1[8] = 7; imm[8] = 0 54 op[9] = ROP_ADD_IMM; u0[9] = 2; u1[9] = 0 - 1; imm[9] = 1 55 op[10] = ROP_LT_IMM; u0[10] = 9; u1[10] = 0 - 1; imm[10] = RE_KK 56 57 let loa: i64 = 6 // c2 (live-out) 58 let lob: i64 = 8 // acc1 (live-out) 59 let loc: i64 = 9 // i1 (live-out) 60 61 // intervals; live-outs kept live to the block end (loop-carried). 62 let last_use: *i64 = sys_mmap(8 * RE_N) 63 let alloc: *i64 = sys_mmap(8 * RE_N) 64 ra_compute_last_use(RE_N, u0, u1, last_use) 65 last_use[loa] = RE_N; last_use[lob] = RE_N; last_use[loc] = RE_N 66 let spills: i64 = ra_linscan(RE_N, RE_NREG, last_use, alloc) 67 let valid: i64 = ra_validate(RE_N, last_use, alloc, RE_NREG) 68 re_emit(" spills (0 = fits) : " as *u8, spills) 69 re_emit(" sound (0 = valid) : " as *u8, valid) 70 71 // 1:1 over random inputs: reference vs allocated execution. 72 let inputs: *i64 = sys_mmap(8 * 4) 73 var mism: i64 = 0 74 var s: i64 = 11400714819323198485 75 var tr: i64 = 0 76 while tr < RE_TRIALS { 77 s = re_rng(s); inputs[0] = s 78 s = re_rng(s); inputs[1] = s 79 s = re_rng(s); inputs[2] = s 80 let rref: i64 = ri_interp_ref(RE_N, op, u0, u1, imm, inputs, loa, lob, loc) 81 let ralc: i64 = ri_interp_alloc(RE_N, RE_NREG, op, u0, u1, imm, alloc, inputs, loa, lob, loc) 82 if rref != ralc { mism = mism + 1 } 83 tr = tr + 1 84 } 85 re_emit(" trials : " as *u8, RE_TRIALS) 86 re_emit(" ref != alloc mismatches : " as *u8, mism) 87 88 // NEGATIVE CONTROL: corrupt the allocation -- alias acc_in(v1) onto t0(v3)'s 89 // register (they overlap), then the verifier MUST catch the divergence. 90 let bad: *i64 = sys_mmap(8 * RE_N) 91 var c: i64 = 0 92 while c < RE_N { bad[c] = alloc[c]; c = c + 1 } 93 bad[1] = alloc[3] // force a real collision 94 inputs[0] = 123456789; inputs[1] = 987654321; inputs[2] = 42 95 let g_ref: i64 = ri_interp_ref(RE_N, op, u0, u1, imm, inputs, loa, lob, loc) 96 let g_bad: i64 = ri_interp_alloc(RE_N, RE_NREG, op, u0, u1, imm, bad, inputs, loa, lob, loc) 97 var caught: i64 = 0 98 if g_ref != g_bad { caught = 1 } 99 re_emit(" corrupted alloc caught : " as *u8, caught) 100 101 re_puts("----------------------------------------------------------------\n" as *u8) 102 re_puts(" allocated code computes IDENTICALLY to the reference, and a corrupted\n" as *u8) 103 re_puts(" allocation is CAUGHT -> the gate that makes codegen absorption safe.\n" as *u8) 104 105 // GATE 106 if valid != 0 { sys_exit(1); return 1 } 107 if spills != 0 { sys_exit(2); return 2 } // race body fits in registers 108 if mism != 0 { sys_exit(3); return 3 } // execution equivalence must be exact 109 if caught != 1 { sys_exit(4); return 4 } // verifier must catch a miscompile 110 sys_exit(0) 111 return 0 112}