code wiki / _hdl_build / nx_codegen_diff_gate.nx
nx_codegen_diff_gate.nx source
↩ module page · 50 lines · 2559 B
1// nx_codegen_diff_gate.nx -- DIFFERENTIAL codegen verifier: the safety gate that
2// lets the Nishi team improve register allocation (nx_x86_regalloc) WITHOUT a g1
3// repeat. Compiles a corpus of self-verifying programs with TWO compilers (the
4// pinned known-good and a candidate), links + runs both, asserts IDENTICAL runtime
5// behaviour. A correct codegen change emits different asm but the SAME result; a
6// g1-style high-pressure miscompile DIVERGES and is CAUGHT before promotion.
7// Build pipeline = nx_codegen_exec (shared). Known answer: all agree -> exit 0.
8
9import "nx_codegen_exec.nx"
10
11func main() -> i64 {
12 gd_puts("=== DIFFERENTIAL codegen gate: known-good vs candidate, 1:1 behaviour ===\n" as *u8)
13 let kg: *u8 = "_offc/nx_cc_known_good.elf" as *u8
14 let cand: *u8 = "_offc/nx_compile_x86_native.elf" as *u8
15
16 let corpus: *i64 = sys_mmap(8 * 8) as *i64
17 var nc: i64 = 0
18 corpus[nc] = ("runtime/_hdl_build/nx_u128_test.nx" as *u8) as i64; nc = nc + 1
19 corpus[nc] = ("runtime/_hdl_build/nx_regalloc_linscan_test.nx" as *u8) as i64; nc = nc + 1
20
21 var diverge: i64 = 0
22 var pipefail: i64 = 0
23 var i: i64 = 0
24 while i < nc {
25 let src: *u8 = corpus[i] as *u8
26 let ka: i64 = gd_build_run(kg, src, "/tmp/gd_k.s" as *u8, "/tmp/gd_k.elf" as *u8)
27 let ca: i64 = gd_build_run(cand, src, "/tmp/gd_c.s" as *u8, "/tmp/gd_c.elf" as *u8)
28 gd_puts(" prog: " as *u8); gd_puts(src); gd_puts("\n" as *u8)
29 if ka < 0 { gd_emit(" known-good pipeline FAILED (rc) : " as *u8, ka); pipefail = pipefail + 1 }
30 if ca < 0 { gd_emit(" candidate pipeline FAILED (rc) : " as *u8, ca); pipefail = pipefail + 1 }
31 if ka >= 0 { if ca >= 0 {
32 gd_emit(" known-good exit : " as *u8, ka)
33 gd_emit(" candidate exit : " as *u8, ca)
34 if ka != ca { gd_puts(" *** DIVERGE -- a compiler miscompiles this program ***\n" as *u8); diverge = diverge + 1 }
35 else { gd_puts(" agree (identical behaviour)\n" as *u8) }
36 } }
37 i = i + 1
38 }
39
40 gd_puts("----------------------------------------------------------------\n" as *u8)
41 gd_emit(" programs : " as *u8, nc)
42 gd_emit(" divergences (miscompiles): " as *u8, diverge)
43 gd_emit(" pipeline failures : " as *u8, pipefail)
44 gd_puts(" -> a divergence blocks promotion (no g1 ships); agreement clears the candidate.\n" as *u8)
45
46 if pipefail != 0 { sys_exit(1); return 1 }
47 if diverge != 0 { sys_exit(2); return 2 }
48 sys_exit(0)
49 return 0
50}