From ec5062a0ed6a56e2d92245f9188134f3c7e191e9 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:14:44 +0700 Subject: [PATCH] Alignment is a counter, not a property of the prologue Every stack movement now goes through pushv/popv and increments a depth word on the function context. A call pads to 16 from wherever the expression evaluator has left rsp, and asserts the parity before it emits the call. The nested probe passes. The stack-argument path is folded into the same counter rather than keeping its own, because two independent notions of parity is how the bug comes back. --- spike/backend/x86.ml | 76 +++++++++++++++++++++++++++----------------- 1 file changed, 46 insertions(+), 30 deletions(-) diff --git a/spike/backend/x86.ml b/spike/backend/x86.ml index 57a78b6..9f486fe 100644 --- a/spike/backend/x86.ml +++ b/spike/backend/x86.ml @@ -122,6 +122,17 @@ let patch b ~at ~target = type fnctx = { b : buf; nslots : int; + (* How many 8-byte words this expression's evaluation has pushed since the + prologue. rsp is 16-aligned at the end of the prologue, so [depth] even + means rsp is aligned and [depth] odd means it is 8 out. + + This counter is the answer to the one bug the ABI probe found. Alignment + is not a property of the prologue: the evaluator spills the left operand + across the right one's evaluation, so a call written in the right operand + runs with one word outstanding. Deriving it from a count kept here is the + only way that stays correct as the evaluator grows cases, and it is what + clang's [sub rsp, 8] before a call is doing. *) + mutable depth : int; (* A symbol the code calls, resolved to an absolute address by the driver before emission. movabs + call r is what a JIT does anyway: a rel32 call cannot reach an arbitrary mmap, and the 2-byte indirect call is cheaper @@ -131,6 +142,11 @@ type fnctx = { let slot_disp i = -8 * (i + 1) +(* Every stack movement goes through these two, so that nothing can move rsp + without the counter noticing. *) +let pushv f r = push f.b r; f.depth <- f.depth + 1 +let popv f r = pop f.b r; f.depth <- f.depth - 1 + (* Every type this spike handles is one 8-byte integer register. Everything else is the real backend's problem and is enumerated in the verdict rather than guessed at here. *) @@ -234,10 +250,10 @@ and prim f e (p : Flan.Tast.prim) args = and binop f x y = let b = f.b in value f x; - push b rax; + pushv f rax; value f y; mov_rr b ~dst:rcx ~src:rax; - pop b rax + popv f rax and emit_if f c t e = let b = f.b in @@ -267,41 +283,41 @@ and emit_if f c t e = and call f (addr : int64) args ~xfer = let b = f.b in let n = List.length args + (if xfer then 1 else 0) in - if n > 6 then begin - (* The stack half. Evaluate every stacked argument first, right to left, - leaving them pushed, then fill the registers -- otherwise evaluating a - stacked argument would clobber a register already loaded. *) - let stacked = List.filteri (fun i _ -> i >= 6) args in - let nstack = List.length stacked + (if xfer then 1 else 0) in - if nstack land 1 = 1 then sub_imm32 b ~dst:rsp 8; - if xfer then (movabs b ~dst:rax 0L; push b rax); - List.iter (fun a -> value f a; push b rax) (List.rev stacked) - end; - (* The register half, and it needs a spill: rdi..r9 are argument registers + (* Bring rsp to 16 first, so everything below can count in pairs. *) + let pad = f.depth land 1 = 1 in + if pad then (sub_imm32 b ~dst:rsp 8; f.depth <- f.depth + 1); + let stacked = List.filteri (fun i _ -> i >= 6) args in + let nstack = List.length stacked + (if xfer && n > 6 then 1 else 0) in + (* The stack half, evaluated right to left so that the seventh argument ends + up at [rsp] and the eighth above it. The transfer channel is the last + argument of all, so it is pushed first. *) + if nstack land 1 = 1 then (sub_imm32 b ~dst:rsp 8; f.depth <- f.depth + 1); + if xfer && n > 6 then (movabs b ~dst:rax 0L; pushv f rax); + List.iter (fun a -> value f a; pushv f rax) (List.rev stacked); + (* The register half needs a spill of its own: rdi..r9 are argument registers and rax is where every value lands, so an earlier argument would be - clobbered by a later one's evaluation. Push each, then pop them into - their registers in reverse. *) + clobbered by a later one's evaluation. Push each, then pop them into their + registers in reverse. *) let inreg = List.filteri (fun i _ -> i < 6) args in - List.iter (fun a -> value f a; push b rax) inreg; + List.iter (fun a -> value f a; pushv f rax) inreg; let nreg = List.length inreg in - List.iteri (fun i _ -> pop b arg_regs.(nreg - 1 - i)) inreg; + List.iteri (fun i _ -> popv f arg_regs.(nreg - 1 - i)) inreg; if xfer && n <= 6 then movabs b ~dst:arg_regs.(nreg) 0L; - (* al = number of vector registers used. Required only for a variadic - callee, and set unconditionally because it is free and a wrong al on a - printf-shaped raylib entry point (TraceLog is one) is a crash that looks - like anything else. It must be set *after* the argument registers, since - al is rax's low byte. *) + (* al = the number of vector registers used. Required only for a variadic + callee and set unconditionally because it is two bytes: a wrong al on a + printf-shaped entry point -- raylib's TraceLog is one -- is a crash that + looks like anything else. After the argument registers, since al is rax's + low byte. *) u8 b 0xb0; u8 b 0x00; (* mov al, 0 *) (* r11 always, never r9: r11 is the scratch register SysV reserves and is the - one 64-bit register guaranteed not to be carrying an argument. Picking the - target conditionally is how a call with six arguments gets quietly wrong. *) + one register guaranteed not to be carrying an argument. Choosing the + target conditionally is how a six-argument call gets quietly wrong. *) u8 b 0x49; u8 b 0xbb; u64 b addr; (* movabs r11, addr *) + assert (f.depth land 1 = 0); call_r b 11; - if n > 6 then begin - let nstack = List.length args - 6 + (if xfer then 1 else 0) in - let pop_bytes = 8 * (nstack + (nstack land 1)) in - add_imm32 b ~dst:rsp pop_bytes - end + let back = 8 * (nstack + (nstack land 1)) in + if back > 0 then (add_imm32 b ~dst:rsp back; f.depth <- f.depth - (back / 8)); + if pad then (add_imm32 b ~dst:rsp 8; f.depth <- f.depth - 1) and node_name (k : Flan.Tast.expr_kind) = match k with @@ -331,7 +347,7 @@ and node_name (k : Flan.Tast.expr_kind) = let fn ~resolve (fd : Flan.Tast.fn) : string = let b = create () in let nslots = Array.length fd.Flan.Tast.slots in - let f = { b; nslots; resolve } in + let f = { b; nslots; resolve; depth = 0 } in push b rbp; mov_rr b ~dst:rbp ~src:rsp; (* Round the frame to 16 so that rsp is aligned at every call site. One