nx_regalloc_calls_test.nx source

1// nx_regalloc_calls_test.nx -- PROVE the G1 allocator's live-across-call capability, with 2// the bug reproduced under control. One kernel where v0,v1,v2 are all live across a call: 3// CALL-UNAWARE alloc (base ra_linscan): places a spanning vreg in a caller-saved reg 4// -> ra_validate_calls flags it (STATIC) AND the execution model diverges (DYNAMIC). 5// CALL-AWARE alloc (ra_linscan_calls): spanning vregs are callee-saved or spilled 6// -> validate passes AND execution matches the reference on every input. 7// Known answer: fixed sound + naive unsound + fixed==ref for all inputs -> exit 0. 8 9import "nx_regalloc_calls.nx" 10 11func rt_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 12func rt_num(v: i64) -> i64 { 13 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 14 let t: *u8 = sys_mmap(28); var k: i64 = 0 15 if m == 0 { t[0] = 48; k = 1 } 16 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 17 if v < 0 { rt_puts("-" as *u8) } 18 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 19 sys_write(1, b, k); return 0 20} 21func rt_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 22func tally(r: *i64, n: i64) -> i64 { 23 var ec: i64 = 0; var i: i64 = 0 24 while i < n { if r[i] != 1 { if ec == 0 { ec = i + 1 } } i = i + 1 } 25 return ec 26} 27 28// build the kernel: v0,v1 inputs; v2=3*v0; v3=CALL; v4=v2+v3; v5=v0+v4; v6=v1^v5. 29// v0,v1,v2 are defined before the call (i3) and used after -> they SPAN it. 30func build_kernel(op: *i64, u0: *i64, u1: *i64, imm: *i64, isc: *i64) -> i64 { 31 op[0]=ROP_INPUT; u0[0]=0-1; u1[0]=0-1; imm[0]=0; isc[0]=0 32 op[1]=ROP_INPUT; u0[1]=0-1; u1[1]=0-1; imm[1]=1; isc[1]=0 33 op[2]=ROP_MUL_IMM; u0[2]=0; u1[2]=0-1; imm[2]=3; isc[2]=0 34 op[3]=ROP_CALL; u0[3]=0-1; u1[3]=0-1; imm[3]=100; isc[3]=1 35 op[4]=ROP_ADD; u0[4]=2; u1[4]=3; imm[4]=0; isc[4]=0 36 op[5]=ROP_ADD; u0[5]=0; u1[5]=4; imm[5]=0; isc[5]=0 37 op[6]=ROP_XOR; u0[6]=1; u1[6]=5; imm[6]=0; isc[6]=0 38 return 7 39} 40 41// run T trials over varying inputs; counts[0]=fixed mismatches, counts[1]=naive mismatches. 42func run_trials(n: i64, nreg: i64, ncaller: i64, op: *i64, u0: *i64, u1: *i64, imm: *i64, isc: *i64, 43 a_fix: *i64, a_naive: *i64, counts: *i64) -> i64 { 44 counts[0] = 0; counts[1] = 0 45 let inp: *i64 = sys_mmap(8 * 4) as *i64 46 var t: i64 = 0 47 while t < 24 { 48 inp[0] = t * 7 + 1 49 inp[1] = t * 5 + 3 50 let ref: i64 = rc_interp_ref(n, op, u0, u1, imm, isc, inp, 4, 5, 6) 51 let fix: i64 = rc_interp_alloc(n, nreg, ncaller, op, u0, u1, imm, isc, a_fix, inp, 4, 5, 6) 52 let naive: i64 = rc_interp_alloc(n, nreg, ncaller, op, u0, u1, imm, isc, a_naive, inp, 4, 5, 6) 53 if fix != ref { counts[0] = counts[0] + 1 } 54 if naive != ref { counts[1] = counts[1] + 1 } 55 t = t + 1 56 } 57 return 0 58} 59 60func main() -> i64 { 61 rt_puts("=== G1 register allocator: LIVE-ACROSS-CALL capability, proven by execution ===\n" as *u8) 62 let op: *i64 = sys_mmap(8 * 16) as *i64 63 let u0: *i64 = sys_mmap(8 * 16) as *i64 64 let u1: *i64 = sys_mmap(8 * 16) as *i64 65 let imm: *i64 = sys_mmap(8 * 16) as *i64 66 let isc: *i64 = sys_mmap(8 * 16) as *i64 67 let lu: *i64 = sys_mmap(8 * 16) as *i64 68 let a_fix: *i64 = sys_mmap(8 * 16) as *i64 69 let a_naive: *i64 = sys_mmap(8 * 16) as *i64 70 let counts: *i64 = sys_mmap(8 * 4) as *i64 71 let r: *i64 = sys_mmap(8 * 8) as *i64 72 73 let n: i64 = build_kernel(op, u0, u1, imm, isc) 74 ra_compute_last_use(n, u0, u1, lu) 75 lu[4] = n - 1; lu[5] = n - 1; lu[6] = n - 1 // live-outs stay live to block end (read by the checksum) 76 let nreg: i64 = 3 77 let ncaller: i64 = 2 // regs 0,1 caller-saved; reg 2 callee-saved 78 79 // allocate both ways 80 ra_linscan(n, nreg, lu, a_naive) // call-UNAWARE (the base allocator = the gap) 81 ra_linscan_calls(n, nreg, ncaller, lu, isc, a_fix) // call-AWARE (the fix) 82 83 // static soundness 84 let vn: i64 = ra_validate_calls(n, lu, isc, a_naive, ncaller) 85 let vf: i64 = ra_validate_calls(n, lu, isc, a_fix, ncaller) 86 rt_puts(" static : call-unaware sound? " as *u8); if vn == 0 { rt_puts("yes (missed it!)" as *u8) } else { rt_puts("NO -- caller-saved reg held live across a call at v" as *u8); rt_num((0 - vn) - 1) } 87 rt_puts("\n static : call-aware sound? " as *u8); if vf == 0 { rt_puts("YES" as *u8) } else { rt_puts("no (violation v" as *u8); rt_num((0 - vf) - 1); rt_puts(")" as *u8) }; rt_puts("\n" as *u8) 88 89 // dynamic differential 90 run_trials(n, nreg, ncaller, op, u0, u1, imm, isc, a_fix, a_naive, counts) 91 rt_puts(" exec : over 24 inputs -- call-aware mismatches=" as *u8); rt_num(counts[0]) 92 rt_puts(" call-unaware mismatches=" as *u8); rt_num(counts[1]); rt_puts("\n" as *u8) 93 94 // verdicts (memory-backed) 95 r[0] = rt_eq(vf, 0) // fix is statically sound 96 r[1] = 0; if vn != 0 { r[1] = 1 } // base allocator is statically UNSOUND for calls 97 r[2] = rt_eq(counts[0], 0) // fix matches reference on every input 98 r[3] = 0; if counts[1] > 0 { r[3] = 1 } // base allocator DIVERGES -- bug reproduced 99 100 rt_puts("----------------------------------------------------------------\n" as *u8) 101 rt_puts(" The G1 allocator spills/callee-saves anything that spans a call -- the live-across-call\n" as *u8) 102 rt_puts(" miscompile is fixed at the SOURCE (allocation policy) and proven by execution.\n" as *u8) 103 104 rt_puts(" verdicts: r0(fix-sound)=" as *u8); rt_num(r[0]); rt_puts(" r1(naive-unsound)=" as *u8); rt_num(r[1]) 105 rt_puts(" r2(fix-matches)=" as *u8); rt_num(r[2]); rt_puts(" r3(naive-diverges)=" as *u8); rt_num(r[3]); rt_puts("\n" as *u8) 106 let ec: i64 = tally(r, 4) 107 rt_puts(" gate ec : " as *u8); rt_num(ec); rt_puts("\n" as *u8) 108 sys_exit(ec) 109 return ec 110}