nx_opt_eqsat_pass.nx source
↩ module page · 127 lines · 7450 B
1// nx_opt_eqsat_pass.nx -- EQUALITY SATURATION AS AN ACTUAL IR REWRITE PASS.
2//
3// This is the first thing in the estate that makes nx_eqsat CHANGE A PROGRAM rather than merely judge
4// one. Everything before it -- seven gates, 93 teeth, and nx_opt_eqsat_oracle_gate -- proved the engine
5// sound and used it to CHECK the shipping optimizer. This consumes it.
6//
7// WHAT IT DOES: for each two-operand integer instruction, build a small e-graph of that expression
8// (constants as constants, non-constant operands as e-graph VARIABLES KEYED ON THEIR IR VALUE ID, so
9// the same SSA value becomes the same e-class), saturate it under the data-driven rule table plus the
10// const-fold analysis, extract the cost-minimal representative, and if that representative is a
11// CONSTANT, fold the instruction's result to it. The rewrite mechanism is the incumbent one, copied
12// deliberately from opt_const_fold: set the result Value's kind to CONST and its const_int. No new way
13// to mutate IR is introduced by this file.
14//
15// WHY IT IS NOT A DUPLICATE OF opt_const_fold: that pass requires BOTH operands to be constants. This
16// one folds through ALGEBRAIC IDENTITIES, so it reaches expressions the shipping pipeline cannot --
17// `x ^ x` and `x - x` with x a runtime value fold to 0 here and are left untouched there. That gap is
18// real and currently unmitigated, because opt_simplify (the peephole that would catch some of these)
19// is BISECT-DISABLED in opt_run and has been since a self-host miscompile.
20//
21// DELIBERATELY NOT IMPORTED BY nx_opt.nx YET, and the lang_opt_eqsat_pass watch contract stays OPEN
22// because of it. Adding `import nx_eqsat.nx` to nx_opt pulls the whole engine into every nx_cc build,
23// changing the compiler's closure and its bytes. That is a compiler change and it belongs behind the
24// equivalence net (nx_cc_equiv_gate 10/10 + selfhost) as a deliberate act, not as a side effect of
25// landing a pass. Shipping the pass first, wired to nothing, is the sequencing that keeps the
26// shipping compiler byte-identical while the capability becomes real and provable.
27//
28// TYPE NARROWNESS, STATED: i32-typed instructions are SKIPPED. opt_const_fold wraps folded constants
29// mod 2^32 to match the backend's masking behaviour, and a fold that ignored that would produce a
30// silently wrong value -- exactly the class this estate tracks hardest. Rather than duplicate that
31// wrapping logic (a second ruler), this pass declines i32 and says so.
32// license_tier: ORIGINAL expect_exit: 0
33
34import "nx_syscalls.nx"
35import "nx_types.nx"
36import "nx_ir.nx"
37import "nx_eqsat.nx"
38
39const OEP_CAP_NODES: i64 = 64
40const OEP_CAP_CLS: i64 = 64
41const OEP_SAT_ITERS: i64 = 8
42const OEP_DSL_ROWS: i64 = 16
43
44// Map an IR opcode to the e-graph operator with the SAME semantics, or -1 to decline.
45// Declining is the safe direction: an unmapped op is simply not considered for rewriting.
46// DIV/REM/SHR are absent ON PURPOSE -- nx_eqsat_op_to_gate_kind refuses them too, because the gate
47// simulator has no faithful cell for them, and a fold without a faithful oracle is a guess.
48func oep_ir_op_to_eq(op: i64) -> i64 {
49 if op == OP_ADD { return NX_EQ_OP_ADD }
50 if op == OP_SUB { return NX_EQ_OP_SUB }
51 if op == OP_MUL { return NX_EQ_OP_MUL }
52 if op == OP_AND { return NX_EQ_OP_AND }
53 if op == OP_OR { return NX_EQ_OP_OR }
54 if op == OP_XOR { return NX_EQ_OP_XOR }
55 if op == OP_SHL { return NX_EQ_OP_SHL }
56 return 0 - 1
57}
58
59func opt_eqsat_pass(f: *Function) -> i64 {
60 // BUFFERS HOISTED OUT OF BOTH LOOPS. A per-instruction sys_mmap is a syscall per instruction and
61 // would dominate the pass; nx_eqsat_init resets the graph in place, so one allocation serves every
62 // expression. This is the same lesson the engine's own cf_scratch field records.
63 let nodes: *NxENode = sys_mmap(OEP_CAP_NODES * 64) as *NxENode
64 let classes: *NxEClass = sys_mmap(OEP_CAP_CLS * 32) as *NxEClass
65 let g: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
66 let table: *NxDslRule = sys_mmap(OEP_DSL_ROWS * 96) as *NxDslRule
67 if (nodes as i64) == 0 { return 0 }
68 if (classes as i64) == 0 { return 0 }
69 if (g as i64) == 0 { return 0 }
70 if (table as i64) == 0 { return 0 }
71
72 var folded: i64 = 0
73 var bi: i64 = 0
74 while bi < f.n_blocks {
75 let b: *BasicBlock = block_at(f, bi)
76 var inst: *Instr = b.head
77 while inst != (0 as *Instr) {
78 if inst.n_operands == 2 {
79 let eop: i64 = oep_ir_op_to_eq(inst.op)
80 if eop >= 0 {
81 var skip: i64 = 0
82 // i32 results need the backend's mod-2^32 wrap; decline rather than duplicate it.
83 if inst.ty != (0 as *Type) { if inst.ty.kind == TY_I32 { skip = 1 } }
84 if skip == 0 {
85 if nx_eqsat_init(g, nodes, OEP_CAP_NODES, classes, OEP_CAP_CLS) == NX_EQSAT_OK {
86 nx_eqsat_enable_constfold(g)
87 let nrules: i64 = nx_eqsat_builtin_dsl_table(table)
88 // Append the proven xor-self rule; it is the identity that reaches
89 // expressions opt_const_fold structurally cannot see.
90 nx_eqsat_dsl_set_row(table, nrules, NX_EQSAT_RULE_XOR_SELF, NX_EQ_OP_XOR,
91 DSL_VAR, 0, DSL_SAME_AS_A, 0,
92 RHS_CONST, 0, SC_NONE, CNT_REAL_MERGE, 0)
93 nx_eqsat_enable_dsl(g, table, nrules + 1, OEP_DSL_ROWS)
94 let av: *Value = val_at(f, inst.op0)
95 let bv: *Value = val_at(f, inst.op1)
96 // KEYING VARIABLES ON THE IR VALUE ID is what makes `x ^ x` recognisable:
97 // both operands resolve to the same e-class, so the rule can match.
98 var ea: i64 = 0
99 var eb: i64 = 0
100 if av.kind == 0 { ea = nx_eqsat_add_const(g, av.const_int) } else { ea = nx_eqsat_add_var(g, inst.op0) }
101 if bv.kind == 0 { eb = nx_eqsat_add_const(g, bv.const_int) } else { eb = nx_eqsat_add_var(g, inst.op1) }
102 if ea >= 0 { if eb >= 0 {
103 let top: i64 = nx_eqsat_add_binary(g, eop, ea, eb)
104 if top >= 0 {
105 nx_eqsat_saturate(g, OEP_SAT_ITERS)
106 nx_eqsat_recompute_best(g)
107 let canon: i64 = nx_eqsat_find(g, top)
108 let bn: i64 = g.classes[canon].best_node
109 if g.nodes[bn].op == NX_EQ_OP_CONST {
110 // SAME REWRITE MECHANISM AS opt_const_fold -- no new mutation path.
111 let res: *Value = val_at(f, inst.result)
112 res.kind = 0
113 res.const_int = g.nodes[bn].payload
114 folded = folded + 1
115 }
116 }
117 } }
118 }
119 }
120 }
121 }
122 inst = inst.next
123 }
124 bi = bi + 1
125 }
126 return folded
127}