nx_regalloc_soundness_test.nx source
↩ module page · 164 lines · 6176 B
1// nx_regalloc_soundness_test.nx -- BITS-UP soundness proof for the allocator
2// running on compute_liveness' (correct) intervals. Builds a loop where K
3// values are all live across the body (defined in entry, used in the header
4// each iteration -> live across the back-edge), runs the FULL allocator flow
5// WITH compute_liveness enabled, then checks the interference invariant:
6// for every pair of values that are BOTH register-homed and whose
7// (post-liveness) intervals OVERLAP, their registers MUST differ.
8// A violation = linear-scan handed two simultaneously-live values the same
9// register = a real miscompile source. Zero blast radius (executes the
10// allocator, not the built IR).
11// exit 0 = sound. 50 = an interference violation (prints the pair). other =
12// setup divergence.
13// license_tier: ORIGINAL
14
15import "nx_syscalls.nx"
16import "nx_types.nx"
17import "nx_ir.nx"
18import "nx_regalloc.nx"
19
20const K: i64 = 24 // values live across the loop body (>16 GPRs -> forces spills)
21
22func main() -> i64 {
23 let m_raw: *u8 = sys_mmap(256)
24 let m: *Module = m_raw as *Module
25 m.name = "soundness" as *u8
26 m.functions = 0 as *Function
27 m.n_functions = 0
28
29 let f: *Function = ir_function_new(m, "main" as *u8, 4, ir_type_i64())
30 let entry: *BasicBlock = ir_block_new(f) // 0
31 let header: *BasicBlock = ir_block_new(f) // 1
32 let body: *BasicBlock = ir_block_new(f) // 2
33 let exit: *BasicBlock = ir_block_new(f) // 3
34
35 // entry: define K live-across-body values vN = N+1 + 0
36 let ids_raw: *u8 = sys_mmap(K * 8 + 16)
37 let ids: *i64 = ids_raw as *i64
38 var i: i64 = 0
39 while i < K {
40 ids[i] = ir_emit_binop(entry, OP_ADD, ir_const_i64(f, i + 1), ir_const_i64(f, 0), ir_type_i64())
41 i = i + 1
42 }
43 ir_emit_br(entry, header)
44
45 // header: cond = sum of all K values (USES each -> all live into header
46 // every iteration) ; br_cond cond -> body, exit
47 var acc: i64 = ids[0]
48 i = 1
49 while i < K {
50 acc = ir_emit_binop(header, OP_ADD, acc, ids[i], ir_type_i64())
51 i = i + 1
52 }
53 ir_emit_br_cond(header, acc, body, exit)
54
55 // body: a throwaway value ; br header (BACK-EDGE)
56 let tmp: i64 = ir_emit_binop(body, OP_ADD, ir_const_i64(f, 2), ir_const_i64(f, 3), ir_type_i64())
57 ir_emit_br(body, header)
58
59 // exit: return 0
60 ir_emit_return(exit, ir_const_i64(f, 0))
61
62 // ---- full allocator flow WITH compute_liveness enabled ----
63 let n: i64 = f.n_values
64 let intv_raw: *u8 = sys_mmap(n * 48 + 16)
65 let intv: *Interval = intv_raw as *Interval
66 let calls_raw: *u8 = sys_mmap(4096)
67 let calls: *i64 = calls_raw as *i64
68 let nc_raw: *u8 = sys_mmap(16)
69 let nc: *i64 = nc_raw as *i64
70 *nc = 0
71 let bs_raw: *u8 = sys_mmap(f.n_blocks * 8 + 16)
72 let bb_start: *i64 = bs_raw as *i64
73 let be_raw: *u8 = sys_mmap(f.n_blocks * 8 + 16)
74 let bb_end: *i64 = be_raw as *i64
75
76 build_intervals(f, intv, calls, nc, bb_start, bb_end)
77 compute_liveness(f, intv, bb_start, bb_end) // the corrected intervals
78 mark_crosses_call(intv, n, calls, *nc)
79
80 // Partition GPR, non-rematerialisable values; sort by start; linear-scan.
81 let gpr_raw: *u8 = sys_mmap(n * 8 + 16)
82 let gpr_ids: *i64 = gpr_raw as *i64
83 var n_gpr: i64 = 0
84 var v: i64 = 0
85 while v < n {
86 let iv: *Interval = intv_at(intv, v)
87 if iv.start >= 0 {
88 if is_rematerialisable(f, v) == 0 {
89 if is_float_value(f, v) == 0 {
90 gpr_ids[n_gpr] = v
91 n_gpr = n_gpr + 1
92 }
93 }
94 }
95 v = v + 1
96 }
97 sort_by_start(gpr_ids, n_gpr, intv)
98 let mask_raw: *u8 = sys_mmap(16)
99 let mask: *i64 = mask_raw as *i64
100 *mask = 0
101 linear_scan(intv, gpr_ids, n_gpr, mask)
102
103 // Confirm spilling actually happened (the path the historical bug hides in).
104 var n_reg: i64 = 0
105 var n_spill: i64 = 0
106 var sv: i64 = 0
107 while sv < n {
108 let iv: *Interval = intv_at(intv, sv)
109 if iv.start >= 0 {
110 if is_rematerialisable(f, sv) == 0 {
111 if is_float_value(f, sv) == 0 {
112 if iv.reg >= 0 { n_reg = n_reg + 1 }
113 if iv.reg < 0 { n_spill = n_spill + 1 }
114 }
115 }
116 }
117 sv = sv + 1
118 }
119 nx_puts_err("allocator: " as *u8)
120 nx_puti_err(n_reg)
121 nx_puts_err(" in-register, " as *u8)
122 nx_puti_err(n_spill)
123 nx_puts_err(" spilled\n" as *u8)
124 if n_spill == 0 { return 60 } // K too small -> spill path not exercised
125
126 // ---- INTERFERENCE CHECK ----
127 // For every pair of register-homed values whose intervals overlap, regs
128 // must differ. Overlap(a,b) = NOT (a.end < b.start OR b.end < a.start).
129 var a: i64 = 0
130 while a < n {
131 let ia: *Interval = intv_at(intv, a)
132 if ia.start >= 0 {
133 if ia.reg >= 0 {
134 var b: i64 = a + 1
135 while b < n {
136 let ib: *Interval = intv_at(intv, b)
137 if ib.start >= 0 {
138 if ib.reg >= 0 {
139 var disjoint: i64 = 0
140 if ia.end < ib.start { disjoint = 1 }
141 if ib.end < ia.start { disjoint = 1 }
142 if disjoint == 0 {
143 if ia.reg == ib.reg {
144 // overlapping live ranges sharing a register
145 nx_puts_err("INTERFERENCE: values " as *u8)
146 nx_puti_err(a)
147 nx_puts_err(" and " as *u8)
148 nx_puti_err(b)
149 nx_puts_err(" share reg " as *u8)
150 nx_puti_err(ia.reg)
151 nx_puts_err("\n" as *u8)
152 return 50
153 }
154 }
155 }
156 }
157 b = b + 1
158 }
159 }
160 }
161 a = a + 1
162 }
163 return 0
164}