From 0fbca40446bda4b5f13055aee09d227dd94a1eaf Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:12:55 +0700 Subject: [PATCH 1/6] One function goes from Tast to machine code and answers correctly x86.ml is an instruction selector for the part of Tast that fits in one integer register: literals, slots, let, if, arithmetic, comparison, and a call. Everything else raises with the node that defeated it, because an honest refusal is the measurement and a silently wrong answer would waste the exercise. The frontend is the real one -- Reader, Parse, Load, Check -- so what is lowered is the same Tast.fn the LLVM backend gets. Seven arithmetic results are compared against what the language says they should be; the disassembly proves nothing and is not the evidence. Nothing is wired into the build. No dune file under spike/, driven by hand with ocamlfind and clang as spike/embed already does. --- spike/backend/driver.ml | 124 +++++++++++++ spike/backend/jit_stubs.c | 105 +++++++++++ spike/backend/probe.flan | 24 +++ spike/backend/run.sh | 38 ++++ spike/backend/x86.ml | 363 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 654 insertions(+) create mode 100644 spike/backend/driver.ml create mode 100644 spike/backend/jit_stubs.c create mode 100644 spike/backend/probe.flan create mode 100644 spike/backend/run.sh create mode 100644 spike/backend/x86.ml diff --git a/spike/backend/driver.ml b/spike/backend/driver.ml new file mode 100644 index 0000000..355a748 --- /dev/null +++ b/spike/backend/driver.ml @@ -0,0 +1,124 @@ +(* The spike's harness: run the real frontend, lower the functions it produced + with [X86], put the bytes in executable memory, call them, and compare with + what the language says they should answer. + + The comparison is the whole point. Reading the bytes proves nothing -- a + disassembly that looks right and a program that returns the wrong number is + the normal outcome of hand-encoding, which is why the oracle here is the + arithmetic and not objdump. [oracle.sh] disassembles the same buffer, and + that is a debugging aid, not the evidence. *) + +external jit_alloc : int -> nativeint = "spike_jit_alloc" +external jit_write : nativeint -> string -> unit = "spike_jit_write" +external jit_protect : nativeint -> int -> unit = "spike_jit_protect" +external call1 : nativeint -> int64 -> int64 = "spike_call1" +external call2 : nativeint -> int64 -> int64 -> int64 = "spike_call2" +external sym : string -> nativeint = "spike_sym" + +let failures = ref 0 +let checks = ref 0 + +let check name got want = + incr checks; + if got = want then Printf.printf " ok %-28s = %Ld\n" name got + else begin + incr failures; + Printf.printf " FAIL %-28s = %Ld, want %Ld\n" name got want + end + +(* One page per function, so that a function that runs off its own end lands in + an unmapped page and segfaults at the fault rather than in the middle of the + next function. This is the crudest possible version of the code-object + question the whole exercise is really about. *) +let page = 4096 + +let install (code : string) : nativeint = + if String.length code > page then failwith "function exceeds one page"; + let p = jit_alloc page in + jit_write p code; + jit_protect p page; + p + +let run src = + let decls = + Flan.Load.program ~file:src (Flan.Parse.program_all (Flan.Reader.read_file src)) + in + let prog = Flan.Check.program_all decls.Flan.Load.decls in + Printf.printf "frontend: %d fns, %d globals, %d structs, %d externs\n" + (List.length prog.Flan.Tast.fns) (List.length prog.Flan.Tast.globals) + (List.length prog.Flan.Tast.structs) (List.length prog.Flan.Tast.externs); + + (* Two passes, because [spike-calls] calls functions whose addresses are not + known until they are installed. Pass one installs every function at a + fixed page; pass two emits the real code into it. A real backend does this + with relocations; the spike does it by emitting twice, which is the same + answer with none of the machinery. *) + let addrs : (string, nativeint) Hashtbl.t = Hashtbl.create 16 in + let unsupported = ref [] in + let lowerable = + List.filter + (fun (fd : Flan.Tast.fn) -> + try + ignore (X86.fn ~resolve:(fun _ -> 0L) fd); + true + with X86.Unsupported m -> + unsupported := (fd.Flan.Tast.name, m) :: !unsupported; + false) + prog.Flan.Tast.fns + in + List.iter + (fun (fd : Flan.Tast.fn) -> + Hashtbl.replace addrs fd.Flan.Tast.name (jit_alloc page)) + lowerable; + let resolve name = + match Hashtbl.find_opt addrs name with + | Some p -> Int64.of_nativeint p + | None -> + (* Not a Flan function: a runtime entry point, looked up the way a dev + build already reaches the host's symbols -- through the dynamic symbol + table, which --dev links with -rdynamic. *) + Int64.of_nativeint (sym name) + in + let bytes = Hashtbl.create 16 in + List.iter + (fun (fd : Flan.Tast.fn) -> + let code = X86.fn ~resolve fd in + Hashtbl.replace bytes fd.Flan.Tast.name code; + let p = Hashtbl.find addrs fd.Flan.Tast.name in + jit_write p code; + jit_protect p page) + lowerable; + + Printf.printf "lowered: %d of %d functions\n" + (List.length lowerable) (List.length prog.Flan.Tast.fns); + List.iter (fun (n, m) -> Printf.printf " skipped %-20s %s\n" n m) + (List.rev !unsupported); + Hashtbl.iter (fun n c -> Printf.printf " %-20s %4d bytes at %nx\n" + n (String.length c) (Hashtbl.find addrs n)) bytes; + + (* Dumped so oracle.sh can disassemble exactly the bytes that ran. *) + (try + let oc = open_out_bin (Filename.concat (Filename.dirname Sys.argv.(0)) "spike-add.bin") in + output_string oc (Hashtbl.find bytes "spike-add"); + close_out oc + with Not_found -> ()); + + print_endline "results:"; + let at n = Hashtbl.find addrs n in + check "spike-add 3 4" (call2 (at "spike-add") 3L 4L) 7L; + check "spike-add -5 2" (call2 (at "spike-add") (-5L) 2L) (-3L); + check "spike-arith 10 4" (call2 (at "spike-arith") 10L 4L) 19L; + check "spike-let 6" (call1 (at "spike-let") 6L) 1332L; + check "spike-if 1 2" (call2 (at "spike-if") 1L 2L) 1L; + check "spike-if 9 2" (call2 (at "spike-if") 9L 2L) 7L; + check "spike-calls 5" (call1 (at "spike-calls") 5L) 656L; + + Printf.printf "\n%d checks, %d failures\n" !checks !failures; + exit (if !failures = 0 then 0 else 1) + +(* The frontend's diagnostics printed rather than swallowed: a spike that says + [Fatal error: exception Errors(_)] costs an hour. *) +let () = + try run Sys.argv.(1) with + | Flan.Loc.Error d -> prerr_endline (Flan.Loc.report d); exit 2 + | Flan.Loc.Errors ds -> prerr_endline (Flan.Loc.report_all ds); exit 2 diff --git a/spike/backend/jit_stubs.c b/spike/backend/jit_stubs.c new file mode 100644 index 0000000..76395b0 --- /dev/null +++ b/spike/backend/jit_stubs.c @@ -0,0 +1,105 @@ +/* The three things OCaml cannot do for itself: get executable memory, put + * bytes in it, and jump to them. Everything interesting is in x86.ml; this + * file is deliberately dumb. + * + * Shaped after lib/dynload_stubs.c's rule, which spike/embed took verbatim for + * the same reason: the boundary passes pointers and scalars, never an OCaml + * [value] into foreign storage. Nothing here keeps anything. + * + * RW then mprotect to R+X, never RWX in one mmap: a hardened kernel may refuse + * a writable-executable anonymous mapping outright, and a policy denial that + * comes back as a null pointer reads exactly like an encoding bug. */ + +#include +#include +#include +#include + +#include +#include +#include +#include +#include + +value spike_jit_alloc(value vlen) { + size_t len = (size_t)Long_val(vlen); + void *p = mmap(NULL, len, PROT_READ | PROT_WRITE, + MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + if (p == MAP_FAILED) caml_failwith("spike_jit_alloc: mmap failed"); + return caml_copy_nativeint((intnat)p); +} + +value spike_jit_write(value vp, value vbytes) { + char *p = (char *)Nativeint_val(vp); + memcpy(p, String_val(vbytes), caml_string_length(vbytes)); + return Val_unit; +} + +value spike_jit_protect(value vp, value vlen) { + void *p = (void *)Nativeint_val(vp); + if (mprotect(p, (size_t)Long_val(vlen), PROT_READ | PROT_EXEC) != 0) + caml_failwith("spike_jit_protect: mprotect failed"); + return Val_unit; +} + +/* Every Flan function's emitted signature is its parameters followed by the + * transfer channel (emit.ml, [signature]), so the trampolines below all pass a + * trailing pointer. Nothing in the spike transfers, so it is NULL. */ +typedef int64_t (*fn0)(void *); +typedef int64_t (*fn1)(int64_t, void *); +typedef int64_t (*fn2)(int64_t, int64_t, void *); + +value spike_call0(value vp) { + return caml_copy_int64(((fn0)Nativeint_val(vp))(NULL)); +} +value spike_call1(value vp, value a) { + return caml_copy_int64(((fn1)Nativeint_val(vp))(Int64_val(a), NULL)); +} +value spike_call2(value vp, value a, value b) { + return caml_copy_int64(((fn2)Nativeint_val(vp))(Int64_val(a), Int64_val(b), NULL)); +} + +value spike_sym(value vname) { + void *h = dlsym(RTLD_DEFAULT, String_val(vname)); + if (h == NULL) caml_failwith("spike_sym: not found"); + return caml_copy_nativeint((intnat)h); +} + +/* ── The C side of the ABI probes ──────────────────────────────────── */ + +/* Eight integers: six in registers, two on the stack, which is the case a + * register-only convention silently gets wrong. The answer is positional so a + * swapped pair cannot pass. */ +int64_t spike_probe8(int64_t a, int64_t b, int64_t c, int64_t d, + int64_t e, int64_t f, int64_t g, int64_t h) { + return a * 1 + b * 10 + c * 100 + d * 1000 + e * 10000 + f * 100000 + + g * 1000000 + h * 10000000; +} + +/* The alignment check, and it has to be done with an aligned load rather than + * by reading rsp, because that is how raylib finds out: the SysV ABI promises + * rsp % 16 == 0 at the call instruction, so on entry rsp+8 is aligned, and a + * callee that spills an __m128 to its frame faults when it is not. -O2 is what + * turns this into an actual movaps; without it the bug hides. */ +__attribute__((noinline)) +int64_t spike_probe_align(int64_t x) { + volatile double v[2] __attribute__((aligned(16))) = { 1.0, 2.0 }; + /* Reading rsp as well, so a failure says which of the two it was. */ + uintptr_t sp; + __asm__ volatile ("mov %%rsp, %0" : "=r"(sp)); + if ((sp % 16) != 8) return -1; /* entry rsp is call-site rsp minus 8 */ + return x + (int64_t)(v[0] + v[1]); +} + +/* A double in xmm0 alongside integers, and al = number of vector registers + * used is *not* required here because this is not variadic -- which is itself + * the thing to record. */ +double spike_probe_f(int64_t a, double x, int64_t b, double y) { + return (double)a + x * 2.0 + (double)b * 100.0 + y * 200.0; +} + +/* A small struct by value. BUILT.md's "Why the FFI goes through a C shim" + * says Flan never emits one of these -- the shim flattens it. This is here to + * measure what the shim is saving us from, not because the backend needs it. */ +typedef struct { float x, y; } spike_vec2; +float spike_probe_struct(spike_vec2 v, float s) { return v.x * s + v.y; } diff --git a/spike/backend/probe.flan b/spike/backend/probe.flan new file mode 100644 index 0000000..0fab0e6 --- /dev/null +++ b/spike/backend/probe.flan @@ -0,0 +1,24 @@ +;; The spike's input. Ordinary Flan, run through the ordinary frontend -- +;; Reader, Parse, Load, Check -- so that what the emitter below lowers is the +;; same Tast.fn the LLVM backend gets and not a literal someone typed to make +;; the exercise come out. + +(defn spike-add [a i64 b i64] i64 + (+ a b)) + +(defn spike-arith [a i64 b i64] i64 + (- (* a 3) (+ b 7))) + +(defn spike-let [a i64] i64 + (let [x (* a a) + y (+ x 1)] + (* x y))) + +(defn spike-if [a i64 b i64] i64 + (if (< a b) (- b a) (- a b))) + +(defn spike-calls [a i64] i64 + (spike-add (spike-arith a 2) (spike-let a))) + +(defn main [] i32 + 0) diff --git a/spike/backend/run.sh b/spike/backend/run.sh new file mode 100644 index 0000000..1ed4a01 --- /dev/null +++ b/spike/backend/run.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +# The spike, end to end: the real frontend produces a Tast, x86.ml turns it +# into bytes, the bytes go into an mmap, and the mmap gets called. +# +# Driven by hand with ocamlfind and clang against the flan.cmxa dune already +# builds, exactly as spike/embed does and for the same reason: nothing under +# spike/ is wired into the build, so there is no dune file here and `dune test` +# cannot see any of it. +set -u +here=$(cd "$(dirname "$0")" && pwd) +root=$(cd "$here/../.." && pwd) +cd "$root" || exit 1 + +dune build --root . lib/flan.cmxa 2>&1 | head -20 + +out=$(mktemp -d); trap 'rm -rf "$out"' EXIT + +# The C stubs. -O2 on purpose: spike_probe_align's aligned load only becomes a +# real movaps with optimisation on, and an alignment bug that only shows up in +# a release build is the one this is looking for. +clang -O2 -c -I"$(ocamlopt -where)" "$here/jit_stubs.c" -o "$out/jit_stubs.o" || exit 1 + +ocamlfind ocamlopt -thread -package unix,threads.posix -linkpkg \ + -I "$root/_build/default/lib/.flan.objs/byte" \ + -I "$root/_build/default/lib/.flan.objs/native" \ + -I "$out" -I "$here" \ + -o "$out/spike" \ + "$root/_build/default/lib/flan.cmxa" \ + -cclib -rdynamic -ccopt -L"$root/_build/default/lib" \ + "$out/jit_stubs.o" \ + "$here/x86.ml" "$here/driver.ml" 2>&1 | head -40 + +test -x "$out/spike" || { echo "build failed"; exit 1; } + +"$out/spike" "$here/probe.flan" +rc=$? +echo "exit: $rc" +exit $rc diff --git a/spike/backend/x86.ml b/spike/backend/x86.ml new file mode 100644 index 0000000..57a78b6 --- /dev/null +++ b/spike/backend/x86.ml @@ -0,0 +1,363 @@ +(* A spike: Tast -> x86-64 machine code, in memory, called. Not a backend. + The point is to find out what breaks, so the subset is deliberately tiny + and every case it cannot do raises with the node that defeated it -- an + honest [Unsupported] is the measurement, and a silently wrong answer is + the one outcome that would waste the exercise. + + Register allocation is the trivial one the brief allows: every slot is a + stack slot at [rbp - 8*(i+1)], every value is computed into rax, and a + binary operator pushes its left operand. Two registers are enough for + everything below and nothing is kept live across a statement. That is what + makes an instruction selector tractable in an afternoon; it is also why the + code it produces is four times the size of clang -O0's. + + Conventions, all of them SysV's, because raylib is called from this code: + - integer arguments in rdi rsi rdx rcx r8 r9, then right-to-left on the + stack; integer result in rax. + - rsp % 16 == 0 at the [call] instruction. raylib spills xmm registers + with movaps and faults far from the cause when this is wrong. + - rbx rbp r12-r15 are callee-saved. This emitter touches none of them + except rbp, which it saves. + - every Flan function takes the transfer channel as a trailing ptr + (emit.ml, [signature]), so a Flan function of n parameters is an n+1 + argument C function. *) + +exception Unsupported of string + +let unsupported fmt = Printf.ksprintf (fun s -> raise (Unsupported s)) fmt + +(* ── Bytes ───────────────────────────────────────────────────────────── *) + +type buf = { mutable bytes : Buffer.t } + +let create () = { bytes = Buffer.create 256 } +let len b = Buffer.length b.bytes +let contents b = Buffer.contents b.bytes +let u8 b n = Buffer.add_char b.bytes (Char.chr (n land 0xff)) + +let u32 b n = + for i = 0 to 3 do u8 b ((n asr (i * 8)) land 0xff) done + +let i32 b (n : int) = + if n < -0x80000000 || n > 0x7fffffff then unsupported "displacement %d" n; + u32 b n + +let u64 b (n : int64) = + for i = 0 to 7 do + u8 b (Int64.to_int (Int64.logand (Int64.shift_right_logical n (i * 8)) 0xffL)) + done + +(* ── Registers and modrm ─────────────────────────────────────────────── *) + +(* The encoding order, not the ABI order: this numbering *is* the three bits + the modrm byte wants, which is why rsp is 4 and rbp is 5 rather than + anything more memorable. *) +let rax = 0 and rcx = 1 and rdx = 2 and _rbx = 3 +let rsp = 4 and rbp = 5 and rsi = 6 and rdi = 7 +let r8 = 8 and r9 = 9 + +(* REX.W is always set: everything here is 64-bit. R extends the reg field and + B the r/m field, which is the whole of what r8-r15 need. *) +let rex b ~r ~m = u8 b (0x48 lor (if r >= 8 then 4 else 0) lor (if m >= 8 then 1 else 0)) +let modrm b ~md ~r ~m = u8 b ((md lsl 6) lor ((r land 7) lsl 3) lor (m land 7)) + +(* reg, reg *) +let rr b op ~r ~m = rex b ~r ~m; u8 b op; modrm b ~md:3 ~r ~m + +(* reg, [rbp + disp32]. Always disp32 rather than the shorter disp8 form: a + frame can outgrow 128 bytes and a one-byte displacement that silently wraps + is exactly the bug this spike would not find. *) +let rm_rbp b op ~r ~disp = + rex b ~r ~m:rbp; u8 b op; modrm b ~md:2 ~r ~m:rbp; i32 b disp + +let mov_rr b ~dst ~src = rr b 0x89 ~r:src ~m:dst (* mov dst, src *) +let mov_load b ~dst ~disp = rm_rbp b 0x8b ~r:dst ~disp (* mov dst, [rbp+d] *) +let mov_store b ~src ~disp = rm_rbp b 0x89 ~r:src ~disp (* mov [rbp+d], src *) + +let movabs b ~dst (n : int64) = + rex b ~r:0 ~m:dst; u8 b (0xb8 lor (dst land 7)); u64 b n + +let push b r = if r >= 8 then u8 b 0x41; u8 b (0x50 lor (r land 7)) +let pop b r = if r >= 8 then u8 b 0x41; u8 b (0x58 lor (r land 7)) + +let add_rr b ~dst ~src = rr b 0x01 ~r:src ~m:dst +let sub_rr b ~dst ~src = rr b 0x29 ~r:src ~m:dst +let and_rr b ~dst ~src = rr b 0x21 ~r:src ~m:dst +let or_rr b ~dst ~src = rr b 0x09 ~r:src ~m:dst +let xor_rr b ~dst ~src = rr b 0x31 ~r:src ~m:dst +let imul_rr b ~dst ~src = (* 0f af /r *) + rex b ~r:dst ~m:src; u8 b 0x0f; u8 b 0xaf; modrm b ~md:3 ~r:dst ~m:src +let cmp_rr b ~a ~bb = rr b 0x39 ~r:bb ~m:a (* cmp a, b *) + +let add_imm32 b ~dst n = rex b ~r:0 ~m:dst; u8 b 0x81; modrm b ~md:3 ~r:0 ~m:dst; i32 b n +let sub_imm32 b ~dst n = rex b ~r:0 ~m:dst; u8 b 0x81; modrm b ~md:3 ~r:5 ~m:dst; i32 b n + +let call_r b r = if r >= 8 then u8 b 0x41; u8 b 0xff; modrm b ~md:3 ~r:2 ~m:r +let leave b = u8 b 0xc9 +let ret b = u8 b 0xc3 +let ud2 b = u8 b 0x0f; u8 b 0x0b + +(* setcc al, then movzx rax, al -- a compare's result is a bool, which is one + byte in Flan's layout (i1 in LLVM, and the ABI zero-extends it). *) +let setcc b cc = u8 b 0x0f; u8 b (0x90 lor cc); modrm b ~md:3 ~r:0 ~m:rax +let movzx_al b = u8 b 0x48; u8 b 0x0f; u8 b 0xb6; modrm b ~md:3 ~r:rax ~m:rax + +(* jcc rel32 and jmp rel32, patched once the target is known. *) +let jcc b cc = u8 b 0x0f; u8 b (0x80 lor cc); let at = len b in u32 b 0; at +let jmp b = u8 b 0xe9; let at = len b in u32 b 0; at + +let patch b ~at ~target = + let rel = target - (at + 4) in + let s = Buffer.contents b.bytes in + let s = Bytes.of_string s in + for i = 0 to 3 do + Bytes.set s (at + i) (Char.chr ((rel asr (i * 8)) land 0xff)) + done; + let nb = Buffer.create (Bytes.length s) in + Buffer.add_bytes nb s; + b.bytes <- nb + +(* ── Lowering ────────────────────────────────────────────────────────── *) + +type fnctx = { + b : buf; + nslots : 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 + than the relocation machinery a real backend would grow here. *) + resolve : string -> int64; +} + +let slot_disp i = -8 * (i + 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. *) +let word_ty (t : Flan.Types.t) = + match t with + | Flan.Types.Int _ | Flan.Types.Bool | Flan.Types.Ptr _ -> true + | _ -> false + +let check_word what (t : Flan.Types.t) = + if not (word_ty t) then + unsupported "%s of type %s: not a single integer register" what + (Flan.Types.to_string t) + +let cc_of signed (p : Flan.Tast.prim) = + match p, signed with + | Flan.Tast.Eq, _ -> 0x4 | Flan.Tast.Ne, _ -> 0x5 + | Flan.Tast.Lt, true -> 0xc | Flan.Tast.Lt, false -> 0x2 + | Flan.Tast.Le, true -> 0xe | Flan.Tast.Le, false -> 0x6 + | Flan.Tast.Gt, true -> 0xf | Flan.Tast.Gt, false -> 0x7 + | Flan.Tast.Ge, true -> 0xd | Flan.Tast.Ge, false -> 0x3 + | _ -> assert false + +let arg_regs = [| rdi; rsi; rdx; rcx; r8; r9 |] + +(* Value into rax. Everything is a subexpression of something that will + immediately consume rax, so nothing is kept live and no allocator is + needed. *) +let rec value f (e : Flan.Tast.expr) : unit = + let b = f.b in + match e.Flan.Tast.e with + | Flan.Tast.Int (n, _) -> movabs b ~dst:rax n + | Flan.Tast.Bool v -> movabs b ~dst:rax (if v then 1L else 0L) + | Flan.Tast.Local i -> + check_word "local" e.Flan.Tast.ty; + if i >= f.nslots then unsupported "slot %d out of range" i; + mov_load b ~dst:rax ~disp:(slot_disp i) + | Flan.Tast.Do body -> block f body + | Flan.Tast.Let (binds, body) -> + List.iter + (fun (i, e) -> + value f e; + check_word "binding" e.Flan.Tast.ty; + mov_store b ~src:rax ~disp:(slot_disp i)) + binds; + block f body + | Flan.Tast.Set (Flan.Tast.Plocal i, rhs) -> + value f rhs; + check_word "assignment" rhs.Flan.Tast.ty; + mov_store b ~src:rax ~disp:(slot_disp i) + | Flan.Tast.If (c, t, e') -> emit_if f c t e' + | Flan.Tast.Return (Some x) -> + value f x; + leave b; ret b + | Flan.Tast.Return None -> leave b; ret b + | Flan.Tast.Prim (p, args) -> prim f e p args + | Flan.Tast.Call (name, args) -> call f (f.resolve name) args ~xfer:true + | Flan.Tast.Unit -> () + | k -> unsupported "expression: %s" (node_name k) + +and block f body = + match body with + | [] -> () + | [ last ] -> value f last + | x :: rest -> value f x; block f rest + +and prim f e (p : Flan.Tast.prim) args = + let b = f.b in + match p, args with + | (Flan.Tast.Add | Flan.Tast.Sub | Flan.Tast.Mul + | Flan.Tast.BitAnd | Flan.Tast.BitOr | Flan.Tast.BitXor), [ x; y ] -> + check_word "arithmetic" x.Flan.Tast.ty; + binop f x y; + (* left in rax, right in rcx *) + (match p with + | Flan.Tast.Add -> add_rr b ~dst:rax ~src:rcx + | Flan.Tast.Sub -> sub_rr b ~dst:rax ~src:rcx + | Flan.Tast.Mul -> imul_rr b ~dst:rax ~src:rcx + | Flan.Tast.BitAnd -> and_rr b ~dst:rax ~src:rcx + | Flan.Tast.BitOr -> or_rr b ~dst:rax ~src:rcx + | _ -> xor_rr b ~dst:rax ~src:rcx) + | (Flan.Tast.Eq | Flan.Tast.Ne | Flan.Tast.Lt | Flan.Tast.Le + | Flan.Tast.Gt | Flan.Tast.Ge), [ x; y ] -> + let signed = + match x.Flan.Tast.ty with + | Flan.Types.Int k -> Flan.Types.signed k + | Flan.Types.Bool -> false + | t -> unsupported "comparison on %s" (Flan.Types.to_string t) + in + binop f x y; + cmp_rr b ~a:rax ~bb:rcx; + setcc b (cc_of signed p); + movzx_al b + | Flan.Tast.Rt sym, args -> call f (f.resolve sym) args ~xfer:false + | _ -> unsupported "primitive in %s" (Flan.Types.to_string e.Flan.Tast.ty) + +(* Left into rax, right into rcx, with the left spilled across the right's + evaluation. Left-to-right, which emit.ml's [map_lr] is explicit about being + required rather than a preference -- a call in either operand has effects. + The push/pop pair keeps rsp 16-aligned in pairs, which matters only because + [call] below re-derives alignment from a counter rather than tracking rsp. *) +and binop f x y = + let b = f.b in + value f x; + push b rax; + value f y; + mov_rr b ~dst:rcx ~src:rax; + pop b rax + +and emit_if f c t e = + let b = f.b in + value f c; + (* cmp rax, 0: 48 83 f8 00 -- written out because the helper above takes + registers only and a zero-compare is the one immediate form worth having. *) + u8 b 0x48; u8 b 0x83; modrm b ~md:3 ~r:7 ~m:rax; u8 b 0x00; + let to_else = jcc b 0x4 in (* je *) + value f t; + let to_end = jmp b in + patch b ~at:to_else ~target:(len b); + value f e; + patch b ~at:to_end ~target:(len b) + +(* A call, and this is the part that has to be exactly right. + + [xfer] appends the transfer channel, which every Flan function's signature + carries and a C entry point does not. The spike passes NULL: nothing here + signals, and a real backend would pass the caller's own channel pointer. + + Alignment: rsp is 16-aligned at function entry minus the 8 the [call] + pushed, so after [push rbp] it is aligned again, and the frame is rounded to + a multiple of 16. Every push here is paired with a pop before the next call + can happen, so rsp is aligned at every call site by construction. Stack + arguments are pushed in pairs to keep it that way -- an odd count gets a + dummy push, which is what clang's [sub rsp, 8] is doing when you see it. *) +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 + 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. *) + let inreg = List.filteri (fun i _ -> i < 6) args in + List.iter (fun a -> value f a; push b rax) inreg; + let nreg = List.length inreg in + List.iteri (fun i _ -> pop b 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. *) + 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. *) + u8 b 0x49; u8 b 0xbb; u64 b addr; (* movabs r11, addr *) + 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 + +and node_name (k : Flan.Tast.expr_kind) = + match k with + | Flan.Tast.Int _ -> "Int" | Flan.Tast.Float _ -> "Float" + | Flan.Tast.Bool _ -> "Bool" | Flan.Tast.Str _ -> "Str" + | Flan.Tast.Unit -> "Unit" | Flan.Tast.Zero _ -> "Zero" + | Flan.Tast.Uninit _ -> "Uninit" | Flan.Tast.Local _ -> "Local" + | Flan.Tast.Global _ -> "Global" | Flan.Tast.Prim _ -> "Prim" + | Flan.Tast.Call _ -> "Call" | Flan.Tast.FnAddr _ -> "FnAddr" + | Flan.Tast.CallPtr _ -> "CallPtr" | Flan.Tast.Do _ -> "Do" + | Flan.Tast.Let _ -> "Let" | Flan.Tast.If _ -> "If" + | Flan.Tast.While _ -> "While" | Flan.Tast.Return _ -> "Return" + | Flan.Tast.Break _ -> "Break" | Flan.Tast.Continue _ -> "Continue" + | Flan.Tast.Set _ -> "Set" | Flan.Tast.Field _ -> "Field" + | Flan.Tast.Addr _ -> "Addr" | Flan.Tast.Deref _ -> "Deref" + | Flan.Tast.Make _ -> "Make" | Flan.Tast.MakeCase _ -> "MakeCase" + | Flan.Tast.CaseField _ -> "CaseField" | Flan.Tast.Arr _ -> "Arr" + | Flan.Tast.Some_ _ -> "Some" | Flan.Tast.None_ -> "None" + | Flan.Tast.Match _ -> "Match" | Flan.Tast.UnwrapSome _ -> "UnwrapSome" + | Flan.Tast.Signal _ -> "Signal" | Flan.Tast.Handled _ -> "Handled" + | Flan.Tast.RestartCase _ -> "RestartCase" + | Flan.Tast.WithAlloc _ -> "WithAlloc" + | Flan.Tast.InvokeRestart _ -> "InvokeRestart" + +(* ── A whole function ────────────────────────────────────────────────── *) + +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 + 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 + extra word for the transfer channel's slot, which is not a Flan slot and + has no index -- the spike never reads it, but a real backend must, and + leaving no room for it is the kind of thing that is cheap now and + expensive later. *) + let frame = (nslots + 1) * 8 in + let frame = (frame + 15) land lnot 15 in + if frame > 0 then sub_imm32 b ~dst:rsp frame; + (* Parameters arrive in registers and are stored into their slots at once, + which is also emit.ml's rule: slots 0..n-1 are the parameters, in order. *) + let np = List.length fd.Flan.Tast.params in + if np > 6 then unsupported "more than six parameters"; + List.iteri + (fun i ty -> + check_word "parameter" ty; + mov_store b ~src:arg_regs.(i) ~disp:(slot_disp i)) + fd.Flan.Tast.params; + (* The transfer channel is the last argument and goes just past the slots. *) + if np < 6 then mov_store b ~src:arg_regs.(np) ~disp:(slot_disp nslots); + block f fd.Flan.Tast.body; + leave b; ret b; + (* Anything that falls off the end of a Never-returning body lands here and + traps rather than running into the next function. LLVM's [unreachable] is + undefined behaviour; ud2 is a defined SIGILL, and the difference is one of + the audit's findings. *) + ud2 b; + contents b From faba8a49f8a8dc7a6f7ad61b25423ddda1dbc2c4 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:14:09 +0700 Subject: [PATCH 2/6] The ABI probe catches a real misalignment, which is why it exists Three synthetic Tast functions calling C: eight integers so two go on the stack, and a callee that does a 16-byte aligned spill and answers -1 if it was entered with rsp misaligned. The third calls it from inside a binary operator. The third fails. Alignment at a call site is not a property of the prologue -- it is a property of how much the expression evaluator has pushed, and the evaluator spills the left operand across the right one's evaluation. A call in that right operand runs 8 bytes off. Nothing in the arithmetic tests could see it, because they call nothing that spills a vector register. This is the raylib failure mode exactly, and it is left red for one commit so the record shows the probe found it rather than agreeing with the code. --- spike/backend/driver.ml | 46 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/spike/backend/driver.ml b/spike/backend/driver.ml index 355a748..99deda9 100644 --- a/spike/backend/driver.ml +++ b/spike/backend/driver.ml @@ -103,6 +103,49 @@ let run src = close_out oc with Not_found -> ()); + (* ── The SysV boundary ────────────────────────────────────────────── + Three synthetic functions, built as Tast by hand rather than written in + Flan, because the surface language has no way to spell a call to an + arbitrary C symbol with eight arguments. [Tast.Rt] is the node a runtime + call already uses and the one a [declare-c] shim lands on, so this is the + real path with a made-up callee. *) + let loc = Flan.Loc.unknown in + let i64 = Flan.Types.Int Flan.Types.I64 in + let ex e = { Flan.Tast.e; ty = i64; loc } in + let lit n = ex (Flan.Tast.Int (Int64.of_int n, Flan.Types.I64)) in + let probe name params body = + { Flan.Tast.name; params; slots = Array.make (List.length params) i64; + snames = Array.make (List.length params) None; ret = i64; + body = [ body ]; fdefers = []; fparent = None; floc = loc } + in + let arg0 = ex (Flan.Tast.Local 0) in + let probes = [ + (* Eight integers: six in registers and two on the stack, which is the case + a register-only convention gets silently wrong. *) + probe "abi-8" [ i64 ] + (ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe8", + [ arg0; lit 2; lit 3; lit 4; lit 5; lit 6; lit 7; lit 8 ]))); + (* rsp % 16 == 0 at the call. The callee does an aligned 16-byte spill and + answers -1 if it was entered misaligned. *) + probe "abi-align" [ i64 ] + (ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe_align", [ arg0 ]))); + (* The same call, but underneath a binary operator -- so it is evaluated + with the left operand spilled on the stack. This is the one that matters: + alignment at a call site is not a property of the prologue, it is a + property of how much the expression evaluator has pushed. *) + probe "abi-align-nested" [ i64 ] + (ex (Flan.Tast.Prim (Flan.Tast.Add, + [ lit 0; + ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe_align", [ arg0 ])) ]))); + ] in + List.iter + (fun (fd : Flan.Tast.fn) -> + let code = X86.fn ~resolve fd in + let p = jit_alloc page in + jit_write p code; jit_protect p page; + Hashtbl.replace addrs fd.Flan.Tast.name p) + probes; + print_endline "results:"; let at n = Hashtbl.find addrs n in check "spike-add 3 4" (call2 (at "spike-add") 3L 4L) 7L; @@ -112,6 +155,9 @@ let run src = check "spike-if 1 2" (call2 (at "spike-if") 1L 2L) 1L; check "spike-if 9 2" (call2 (at "spike-if") 9L 2L) 7L; check "spike-calls 5" (call1 (at "spike-calls") 5L) 656L; + check "abi-8 1" (call1 (at "abi-8") 1L) 87654321L; + check "abi-align 10" (call1 (at "abi-align") 10L) 13L; + check "abi-align-nested 10" (call1 (at "abi-align-nested") 10L) 13L; Printf.printf "\n%d checks, %d failures\n" !checks !failures; exit (if !failures = 0 then 0 else 1) From ec5062a0ed6a56e2d92245f9188134f3c7e191e9 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:14:44 +0700 Subject: [PATCH 3/6] 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 From c73f05b0521b06171617e90960cc95006723652e Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:15:50 +0700 Subject: [PATCH 4/6] Disassembly on request, and it is a debugging aid rather than evidence SPIKE_DISASM=1 objdumps the exact buffers that ran. Kept behind a flag and kept out of the pass/fail path: a disassembly that reads correctly beside a function answering the wrong number is the normal outcome of hand-encoding. --- spike/backend/driver.ml | 19 +++++++++++++------ spike/backend/run.sh | 12 +++++++++++- 2 files changed, 24 insertions(+), 7 deletions(-) diff --git a/spike/backend/driver.ml b/spike/backend/driver.ml index 99deda9..fde8ce4 100644 --- a/spike/backend/driver.ml +++ b/spike/backend/driver.ml @@ -96,12 +96,19 @@ let run src = Hashtbl.iter (fun n c -> Printf.printf " %-20s %4d bytes at %nx\n" n (String.length c) (Hashtbl.find addrs n)) bytes; - (* Dumped so oracle.sh can disassemble exactly the bytes that ran. *) - (try - let oc = open_out_bin (Filename.concat (Filename.dirname Sys.argv.(0)) "spike-add.bin") in - output_string oc (Hashtbl.find bytes "spike-add"); - close_out oc - with Not_found -> ()); + (* The bytes that actually ran, dumped where run.sh can objdump them. + A debugging aid and not the evidence: a disassembly that reads correctly + next to a function that answers 656 when it should answer 650 is the + normal outcome of hand-encoding, which is why the checks below compare + numbers. *) + (match Sys.getenv_opt "SPIKE_DUMP" with + | None -> () + | Some dir -> + Hashtbl.iter + (fun n c -> + let oc = open_out_bin (Filename.concat dir (n ^ ".bin")) in + output_string oc c; close_out oc) + bytes); (* ── The SysV boundary ────────────────────────────────────────────── Three synthetic functions, built as Tast by hand rather than written in diff --git a/spike/backend/run.sh b/spike/backend/run.sh index 1ed4a01..bdef39b 100644 --- a/spike/backend/run.sh +++ b/spike/backend/run.sh @@ -32,7 +32,17 @@ ocamlfind ocamlopt -thread -package unix,threads.posix -linkpkg \ test -x "$out/spike" || { echo "build failed"; exit 1; } -"$out/spike" "$here/probe.flan" +SPIKE_DUMP=$out "$out/spike" "$here/probe.flan" rc=$? + +# Disassembly on request. objdump over the raw buffer, which is what to reach +# for when a function answers the wrong number -- not what proves it answers +# the right one. +if [ "${SPIKE_DISASM:-}" = 1 ]; then + for f in "$out"/*.bin; do + echo; echo "== $(basename "$f" .bin)" + objdump -D -b binary -m i386:x86-64 -M intel "$f" | tail -n +7 + done +fi echo "exit: $rc" exit $rc From e403e74b90274107c3f12f2e0ab9d5166f1bfdc5 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:22:04 +0700 Subject: [PATCH 5/6] Feasible, unforgiving, and not the next thing to do The verdict, as DISCUSS.md item 15. One function goes from Tast to machine code and answers correctly, so the question is not whether it can be done. Three findings decide the shape. Layout is already owned -- emit.ml computes C struct layout for DWARF and is tested against LLVM's own answer -- so the silent-drift risk item 10 feared most does not arise. The C boundary is the easy half, because check.ml already rejects aggregates in a declare and the shim flattens them. And the hard half was not on anyone's list: Flan calling Flan passes aggregates by value, and LLVM's lowering of a first-class struct is per-field rather than the C psABI -- { i8, float } comes back in al and xmm0 where C would pack it into rax, and a %vec return takes a hidden sret pointer that does not appear in the define line. The internal convention is an implementation, not a document. The audit stands on its own: overflow, shifts and evaluation order are defined; division by zero, INT64_MIN/-1, the float cast, Uninit and unreachable are not. Uninit is the one that bites, because poison is where the two backends are supposed to differ. Unloading: the shadow stack answers the running half and every dev-build function is on it -- only the slot table is gated, not the frame. It cannot answer the pointed-into half, which BUILT.md says is the actual reason nothing is dlclose'd. Escaped function values need a rule the language does not have. --- DISCUSS.md | 198 ++++++++++++++++++++++++++++++++++++++ spike/backend/jit_stubs.c | 21 ++-- 2 files changed, 207 insertions(+), 12 deletions(-) diff --git a/DISCUSS.md b/DISCUSS.md index 854460a..a2cd5f0 100644 --- a/DISCUSS.md +++ b/DISCUSS.md @@ -704,3 +704,201 @@ measurement. and the render-thunk-per-inspection all get deleted. It is the bulk of the work and the whole of the prize. 5. **Keep `llc` + `ld` + `dlopen` exactly as they are.** Item 13's third option. Nothing here argues against it. 6. **Measure what is left.** Then, and only then, item 13 step 4. + +## 15. The backend spike, answered: feasible, and the obstacle is not the one anyone expected + +Item 13's step 4, run early and deliberately out of order, as a spike rather than as a decision. **Feasible.** A +function written in Flan goes through the ordinary frontend, is lowered to x86-64 by hand, is written into an `mmap` +and is called, and it answers correctly. That took an afternoon and no reference material beyond `objdump`. + +The apparatus is `spike/backend/`: `x86.ml` (an instruction selector), `jit_stubs.c` (three calls OCaml cannot make +for itself, plus the C side of the ABI probes), `probe.flan`, `driver.ml` and `run.sh`. `bash spike/backend/run.sh` +reproduces everything below. There is no dune file under `spike/`, nothing is wired into the build, and +`dune test --root . -j 1` is green either side of it. + +**The headline is not the arithmetic.** Ten checks pass, and one of them failed first and mattered: a C callee that +does a 16-byte aligned spill and reports whether it was entered aligned. Called plainly it passed; called from inside +a binary operator it returned `-1`. The evaluator spills its left operand across the right operand's evaluation, so a +call written in the right operand runs with `rsp` 8 bytes out. **That is the raylib crash, reproduced on day one of a +backend that does almost nothing.** It is fixed with a depth counter and an assertion, and it is the clearest single +argument that this work is *tractable but unforgiving*: nothing about the wrong version looked wrong, and only a probe +built to catch it caught it. + +### Question 1 — does one function work end to end + +Yes. The frontend is the real one — `Reader`, `Parse`, `Load`, `Check` — so what is lowered is the same `Tast.fn` +`emit.ml` gets, not a literal typed to make the exercise come out. Eleven of the 83 functions in a trivial program +(the prelude is most of them) lower with no special handling, including `space?`, `digit?` and `upper-ascii`, which +nobody wrote for this. + +The emitter is the trivial one the brief allows: every slot is a stack slot at `rbp - 8(i+1)`, every value is computed +into `rax`, a binary operator spills its left operand. Two registers, no allocator, no liveness. `spike-add` is 58 +bytes where clang `-O0` would spend about 20, and that is the correct trade for a debug build. + +Proved by comparing numbers, not by reading bytes. `SPIKE_DISASM=1` disassembles the buffers that ran, and that is a +debugging aid kept out of the pass/fail path on purpose: a disassembly that reads correctly beside a function +answering 656 when it should answer 650 is the normal outcome of hand-encoding. + +### Question 2 — the real shape of the work + +**Layout is already owned, and this is the best news in the report.** `emit.ml`'s `lay` / `lay_fields` / +`payload_lay` compute C struct layout — offsets, padding, tail padding, the union payload blob — because DWARF needs +member offsets as integer literals and `getelementptr` cannot supply one. They are acceptance-tested against LLVM's +own answer for the same struct type. So the drift risk item 10 fears most, *two backends disagreeing silently about +where a field is*, does not arise: there is one layout calculator and a new backend calls it. + +Against `tast.ml`'s `expr_kind`, in four buckets: + +| | nodes | +|---|---| +| **Done in the spike** | `Int` `Bool` `Local` `Do` `Let` `If` `Return` `Set`/`Plocal`, arithmetic, comparison, bitwise, `Call`, `Rt` | +| **Mechanical** | `While` `Break` `Continue` (the jump patching exists), `Global` `Str` `Zero` `Uninit`, the rest of `place`, `Field` `Deref` `Addr`, `Arr`, `Some_` `None_` `UnwrapSome`, `Match` on a tag | +| **Bulky, not hard** | floats — a second register file, SSE encodings, `Cast`'s eight conversions, and the SSE half of the calling convention. Perhaps a third of the total instruction work for a small fraction of the programs | +| **Fiddly** | aggregate copy on assignment (a struct `store` *is* the copy `spec-memory.md` requires), `Make` `MakeCase` `CaseField` over the payload blob, `CallPtr`, `FnAddr`'s three cases and the cell load behind `Fnval` | +| **No plan** | `Handled` `Signal` `RestartCase` `InvokeRestart` `WithAlloc`, the transfer-channel guard after every call, the landing pad, and `fdefers` on the transfer exit path | + +The last row is the one to take seriously. The spike never emitted a guard or a pad, and the guard is on *every call +site* in the real thing — `emit.ml`'s `guard`, `current_pad`, `emit_restart_case` and `emit_with_alloc` are several +hundred lines of control flow that a second backend reimplements from the spec rather than copies. Conditions are not +an advanced feature to defer: `spec-conditions.md` is load-bearing in the prelude already. + +### Question 3 — the SysV boundary, and the obstacle nobody named + +**The C boundary is the easy half, and `BUILT.md` is why.** `check.ml` rejects an aggregate in a `declare` signature +and the generated shim flattens every struct, so no Flan-emitted call ever passes one to C. A string or slice crosses +as `ptr`+`len` — two arguments, which is the only counting subtlety. The spike calls an eight-argument C function +correctly, including the two that go on the stack, and sets `al` for the variadic case. **No aggregate classifier is +needed for raylib. That is a large piece of `plan.org`'s "three classifiers to write and keep correct forever" that +simply does not apply.** + +**The hard half is Flan calling Flan, and it was found by reading `signature`.** That function spells each parameter +with `ll ty` and flattens nothing. Emitting a trivial program and looking at the `define` lines: + +``` +define i64 @"flan.take-slice"(%slice %p0, i64 %p1, ptr %xfer) +define { i8, i32 } @"flan.index-of-i32"(%slice %p0, i32 %p1, ptr %xfer) +define { i8, float } @"flan.min-f32"(%slice %p0, ptr %xfer) +define { i8, %slice } @"flan.split-next!"(ptr %p0, ptr %xfer) +define %vec @"flan.filter-i32"(%slice %p0, ptr %p1, ptr %xfer) +``` + +The prelude is wall to wall aggregates by value. And what LLVM does with them, measured by `objdump` on clang's own +output rather than read off a table: + +- `%slice` argument → `rdi`:`rsi`, two registers, and the next argument shifts along. +- `{ i8, i64 }` return → tag in `al`, value in `rdx`. +- `{ i8, float }` return → tag in `al`, value in **`xmm0`**. C's psABI would classify that single eightbyte as + INTEGER and pack both into `rax`. **LLVM's lowering of a first-class aggregate in IR is per-field, and it is not + the C ABI.** +- `%vec` return (six words) → a hidden `sret` pointer in `rdi`, the real arguments shifted along behind it, and the + pointer returned in `rax`. **That pointer does not appear in the `define` line at all.** + +So **the internal calling convention is not specified anywhere. It is whatever LLVM's backend does with a first-class +struct, discoverable only by disassembling.** That is the sharpest obstacle in this report, and it is sharper than +raylib for three reasons: the reference is an implementation rather than a document; the failure mode is a garbage +field rather than a link error; and it is not stable by contract across LLVM versions, which is exactly the coupling +`plan.org` chose text IR to avoid. + +It also forces the decision that determines everything else: + +1. **Redefinitions only** — the custom backend emits a new body into an LLVM-built host. Incremental, testable one + function at a time, and the path that fits the dev loop. It requires matching LLVM's aggregate convention + bit-exactly, including the mixed integer/SSE case above. +2. **The whole dev build** — the custom backend owns both sides and *picks* the convention: every aggregate by + pointer, nothing classified, done. No matching problem at all. But it needs complete node coverage on day one, + conditions included, and there is no partial version that runs. + +The spike leaned on option 1 without noticing, because the probe called C and C is the flattened half. A real attempt +has to choose deliberately. + +### Question 4 — where the language leans on LLVM instead of defining itself + +The audit, which stands on its own whatever happens to the backend. Each row is drift you do not get if the language +answers it. + +| | today | defined? | +|---|---|---| +| Integer overflow | no `nsw`/`nuw`, "arithmetic wraps (plan.org, Types)" | **yes** | +| Shift count | masked to the operand width; a literal out of range is rejected by `check` | **yes** | +| Evaluation order | `map_lr`, and the comment says left-to-right is *required, not a preference* | **yes** | +| Division by zero | nothing. `prelude.ml` calls a remainder by zero "immediate undefined behaviour" and routes around it | **no** | +| `INT64_MIN / -1` | nothing, and it is a separate case. LLVM says undefined; x86 `idiv` raises `SIGFPE` | **no** | +| `f64` → `i64` out of range | `fptosi`, undefined in LLVM; x86 `cvttsd2si` answers the "integer indefinite" value | **no** | +| `Uninit` | emitted as `poison` | **no**, and see below | +| `unreachable` | after a `noreturn` call, and after an exhaustive `match` | **no** | +| Alignment | no explicit `align` on loads and stores; LLVM uses the type's ABI alignment | implicitly, via `lay` | + +Two are worth more than a table row. + +**`Uninit` → `poison` is the one that actually bites, and it bites in the direction item 10 fears.** A hand backend +gives a stable garbage value: whatever the stack slot held. LLVM's optimiser may reason from poison and delete the +code that reads it. So `(uninit)` is the one construct where the two backends are *supposed* to differ and where +"works in dev, breaks when shipped" is the expected outcome rather than a bug. The language should say what reading an +uninitialised value means before a second backend exists, not after. + +**`unreachable` is the cheap one.** The spike emits `ud2`: a defined `SIGILL` at the instruction that fell through. +LLVM's `unreachable` is undefined behaviour and licenses the optimiser to delete the path. Defining it as a trap costs +two bytes and turns a class of miscompile into a crash with an address. + +None of this needs a backend. It is a session with `plan.org` and six `check.ml` cases. + +### Question 5 — unloading code, which is the prize + +**The shadow stack is better than expected and still not sufficient, and the two halves of that are separate +questions.** + +*The running half — and the shadow stack does answer it.* The frame push in `emit_fn` is inside a plain `if m.dev` +and is **not** gated: only the *slot table* is gated on `named && n > 0`, and a function with no named slot still +pushes a frame with a null `slots`. So every active Flan function in a dev build is on the chain, lifted handler +clauses included, and each frame points at the `flan_fninfo` belonging to the module it was compiled into — so the +pointer identifies not just the function but *which body*. "No frame on the chain names this body" is answerable +today, with no DWARF and no unwinder. + +Two caveats on that half. The pop happens before `leave; ret`, so a body is briefly executing with no record — +irrelevant if reclamation happens at a safe point on the same thread, fatal if another thread reclaims while the game +thread is returning. And the chain is a plain global, not thread-local, which `flan_dev.c` states and justifies. + +*The pointed-into half, which the shadow stack cannot see and which is the actual reason nothing is `dlclose`d today.* +`BUILT.md` is explicit, and it is not the reason the brief assumed: "a cell holds an address inside a module's text; +unloading it leaves every call site pointing at unmapped memory. The rule is about being *pointed into*." Owning the +code object answers most of this — you own the cells, so redefinition drops the old body's last cell reference — but +not all of it: + +- `FnAddr (Fnval n)` **loads the cell and yields a raw body address**, which can then be stored in a struct, a `Vec` + or a global. Nothing records that it happened. +- `FnAddr (Flanfn _)` and `(Rtfn _)` bypass the cell *by design* — `tast.ml` says they "must never take that path" — + so a `Map`'s hash and equality pair and a handler-bind clause's address are raw pointers into a specific body, held + in data. + +So: **frames are tracked, escaped code pointers are not.** Unloading needs a rule the language does not have yet. The +cheapest honest one is deferred reclamation — retire a body when no frame names it *and* an epoch has passed with no +new capture — and the cleanest is to make a function value a cell pointer rather than a body pointer, which costs one +indirection on `CallPtr` in dev builds and makes the whole question go away. That second option is worth writing down +now whatever happens to the backend, because it is a change to what a `Fn` value *is*. + +### The verdict + +**Feasible, unforgiving, and not the next thing to do.** + +Feasible: the instruction selection is easy, layout is already owned and tested, the C boundary is already flattened, +and one function ran on day one. Nothing here argues the way item 10 feared — the divergence hazard is real but it is +concentrated in three named places (`Uninit`, division, the float cast), not spread through the whole of arithmetic. + +Unforgiving: the internal aggregate convention is defined by LLVM's implementation and not by any document, the +alignment rule is invisible until raylib crashes somewhere else, and conditions are a second full implementation of +`spec-conditions.md` rather than a port. + +Not next: item 13's order still holds, and the spike does not disturb it. Transport is 41µs of a 21ms redefinition and +code generation is 19 of the 21, so the *speed* case remains what item 13 said it was. What this spike adds is that +the **introspection** case is also not free — unloading needs a rule about escaped function values that nothing in the +language has, and that rule is worth having whether or not a backend is ever written. + +**What to do first if it went ahead**, in order, and the first two are worth doing regardless: + +1. **Define the six undefined cases** (question 4). No backend required, and every one is drift avoided rather than + drift managed. +2. **Decide what a `Fn` value is** — body pointer or cell pointer — and write it down. This is the unloading question + and it is a language question, not a backend one. +3. **Choose option 1 or option 2 from question 3**, deliberately. Everything else follows from it. +4. **Only then**, and only if 3 says so, grow `spike/backend/x86.ml` from the node table in question 2 — floats + first, because they gate most of the prelude, and conditions last, because they are the only row with no plan. diff --git a/spike/backend/jit_stubs.c b/spike/backend/jit_stubs.c index 76395b0..f53b516 100644 --- a/spike/backend/jit_stubs.c +++ b/spike/backend/jit_stubs.c @@ -91,15 +91,12 @@ int64_t spike_probe_align(int64_t x) { return x + (int64_t)(v[0] + v[1]); } -/* A double in xmm0 alongside integers, and al = number of vector registers - * used is *not* required here because this is not variadic -- which is itself - * the thing to record. */ -double spike_probe_f(int64_t a, double x, int64_t b, double y) { - return (double)a + x * 2.0 + (double)b * 100.0 + y * 200.0; -} - -/* A small struct by value. BUILT.md's "Why the FFI goes through a C shim" - * says Flan never emits one of these -- the shim flattens it. This is here to - * measure what the shim is saving us from, not because the backend needs it. */ -typedef struct { float x, y; } spike_vec2; -float spike_probe_struct(spike_vec2 v, float s) { return v.x * s + v.y; } +/* No float probe either, for a plainer reason: this emitter has no SSE, so + * there is nothing here that could call one. Floats are counted as work in + * item 15 rather than claimed as done. + * + * And no struct-by-value probe, and that is a finding rather than an + * omission: check.ml rejects an aggregate in a [declare] signature and the + * generated shim flattens every one, so no Flan-emitted call ever passes a + * struct to C. The aggregate problem is real but it is on the Flan-to-Flan + * side, which is measured in DISCUSS.md item 15 and not from here. */ From 6bd353bb8c26d920fd1e7683c3dfb1f972e90227 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 09:23:36 +0700 Subject: [PATCH 6/6] The aggregate claim, checked against a control instead of asserted The same three shapes written in C and as first-class IR aggregates, compiled by the same clang. { i8, i64 } agrees. { i8, float } does not: C packs both halves into rax, the IR form answers in al and xmm0. And a 24-byte struct does not agree at all -- C spills through an sret pointer, the IR form returns it in rax, rdx and rcx, and rcx is a register SysV never uses for a return value. That resolves the ret-big anomaly the first pass noted and moved past, and it makes the finding stronger than it was written: the internal convention is not the C ABI, not only undocumented in the emitted IR. spike_call0 deleted with it -- declared, never bound, and the two unused probes were removed for the same reason. --- DISCUSS.md | 27 +++++++++++++++++++-------- spike/backend/jit_stubs.c | 4 ---- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/DISCUSS.md b/DISCUSS.md index a2cd5f0..e1c391b 100644 --- a/DISCUSS.md +++ b/DISCUSS.md @@ -787,17 +787,28 @@ output rather than read off a table: - `%slice` argument → `rdi`:`rsi`, two registers, and the next argument shifts along. - `{ i8, i64 }` return → tag in `al`, value in `rdx`. -- `{ i8, float }` return → tag in `al`, value in **`xmm0`**. C's psABI would classify that single eightbyte as - INTEGER and pack both into `rax`. **LLVM's lowering of a first-class aggregate in IR is per-field, and it is not - the C ABI.** +- `{ i8, float }` return → tag in `al`, value in **`xmm0`**. - `%vec` return (six words) → a hidden `sret` pointer in `rdi`, the real arguments shifted along behind it, and the pointer returned in `rax`. **That pointer does not appear in the `define` line at all.** -So **the internal calling convention is not specified anywhere. It is whatever LLVM's backend does with a first-class -struct, discoverable only by disassembling.** That is the sharpest obstacle in this report, and it is sharper than -raylib for three reasons: the reference is an implementation rather than a document; the failure mode is a garbage -field rather than a link error; and it is not stable by contract across LLVM versions, which is exactly the coupling -`plan.org` chose text IR to avoid. +The last two are not the C ABI, and that was checked against a control rather than asserted — the same three shapes +written in C, compiled by the same clang at `-O2`, beside the same shapes written as first-class IR aggregates: + +| shape | from C | from IR | +|---|---|---| +| `{ i8, i64 }` | `al` + `rdx` | `al` + `rdx` — agree | +| `{ i8, float }` | **packed into `rax`** (`movd`/`shl`/`or`) | `al` + `xmm0` | +| `{ i64, i64, i64 }` | **`sret` pointer in `rdi`** | **`rax` + `rdx` + `rcx`** | + +The 24-byte case is the striking one: C spills to memory through a hidden pointer, and the IR form returns it in three +registers, one of which — `rcx` — the SysV ABI never uses for a return value at all. Somewhere past that, LLVM does +switch to `sret`, which is what `%vec` gets. + +So **the internal calling convention is not the C ABI and is not specified anywhere. It is whatever LLVM's backend +does with a first-class struct, discoverable only by disassembling.** That is the sharpest obstacle in this report, +and it is sharper than raylib for three reasons: the reference is an implementation rather than a document; the +failure mode is a garbage field rather than a link error; and it is not stable by contract across LLVM versions, which +is exactly the coupling `plan.org` chose text IR to avoid. It also forces the decision that determines everything else: diff --git a/spike/backend/jit_stubs.c b/spike/backend/jit_stubs.c index f53b516..6726793 100644 --- a/spike/backend/jit_stubs.c +++ b/spike/backend/jit_stubs.c @@ -45,13 +45,9 @@ value spike_jit_protect(value vp, value vlen) { /* Every Flan function's emitted signature is its parameters followed by the * transfer channel (emit.ml, [signature]), so the trampolines below all pass a * trailing pointer. Nothing in the spike transfers, so it is NULL. */ -typedef int64_t (*fn0)(void *); typedef int64_t (*fn1)(int64_t, void *); typedef int64_t (*fn2)(int64_t, int64_t, void *); -value spike_call0(value vp) { - return caml_copy_int64(((fn0)Nativeint_val(vp))(NULL)); -} value spike_call1(value vp, value a) { return caml_copy_int64(((fn1)Nativeint_val(vp))(Int64_val(a), NULL)); }