From 188e6bc72f615d337ca227e51b91bc69e1fee458 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:07:26 +0700 Subject: [PATCH 1/4] A plan for measuring the aggregate case across the reload boundary --- HANDOFF-x86-aggregates.md | 49 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 HANDOFF-x86-aggregates.md diff --git a/HANDOFF-x86-aggregates.md b/HANDOFF-x86-aggregates.md new file mode 100644 index 0000000..1dc9a9b --- /dev/null +++ b/HANDOFF-x86-aggregates.md @@ -0,0 +1,49 @@ +# Handoff — the aggregate case across the reload boundary + +Branch `dev-loop`, from `957ba07`. This closes item 4 of `HANDOFF-x86-redef.md`: a redefined function that +takes and returns a struct, which is the one case the two backends' conventions disagree about and the reason +`X86.redefinition` exists at all rather than reusing `Emit.redefinition`. + +*Status: in progress. This file is written early and on purpose, so that a lane that picks the work up mid-way +has the plan and not just the diff.* + +## The plan + +1. A fixture pair, `test/programs/reload-agg.flan` and `reload-agg-v2.flan`, beside the existing `reload.flan` + rather than inside it — `reload.flan`'s transcript is shared with the LLVM path and must not move. + No `main`; the host is `test/reload_host.c` unchanged, which wants `outer : () -> i64` and a `counter` + global. Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the + redefined body, because the C boundary is where the two conventions are required to agree and is not what + is under test. +2. Four struct shapes, because SysV treats them in four different ways and `x86.ml` treats all four the same: + - `≤16 bytes, all integer` — SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`; `x86.ml` passes a + pointer and returns through a hidden `sret`. Diverges in both directions. + - `>16 bytes` — SysV copies the argument onto the stack, which `x86.ml` does not; the *return*, though, + is a hidden pointer in the first integer register for SysV too, so that half may well coincide. Worth + knowing, and worth not assuming either way. + - `{f64, f64}` — SysV classifies both eightbytes SSE and uses `xmm0`:`xmm1`. + - `{i64, f64}` — one INTEGER and one SSE eightbyte, so `rax` and `xmm0`, which is a third register pattern + again. +3. Every field weighted by position in the printed answer (`a + 100*b + 10000*c + …`), so that a scrambled + field order, a wrong base pointer or a half-loaded eightbyte prints a visibly wrong integer rather than the + right one by symmetry. A test whose answer is a symmetric sum of the fields passes under a convention + mismatch that merely permutes them. +4. Run it on both backends: the LLVM `Emit.redefinition` path as the control, and the `X86.redefinition` path + as the claim. The same transcript from both is the measurement. + +## Open questions recorded rather than asked + +- Whether the MEMORY-return half of the matrix genuinely coincides between the two conventions, or only looks + as though it should. Measured by the mismatch spike rather than argued. + +## Baseline + +| | before | +|---|---| +| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 refused | +| `spike/x86/cells.sh` | 4/4 ok | +| `dune test --root .` | exit 0 | + +Note in advance: `survey.sh` globs `test/programs/*.flan`, so each new no-`main` fixture adds one to its +`no-main` skip count. That number moving is the fixtures existing and is not a regression; the MATCH count is +what must not move. From 8ae77db92cb2b7ce701cc56946e23098447533d1 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:12:43 +0700 Subject: [PATCH 2/4] A redefined function that takes and returns a struct, on both backends --- test/programs/reload-agg-v2.flan | 69 +++++++++++++++++++++ test/programs/reload-agg.flan | 101 +++++++++++++++++++++++++++++++ test/test_reload.ml | 96 +++++++++++++++++++++++++++++ 3 files changed, 266 insertions(+) create mode 100644 test/programs/reload-agg-v2.flan create mode 100644 test/programs/reload-agg.flan diff --git a/test/programs/reload-agg-v2.flan b/test/programs/reload-agg-v2.flan new file mode 100644 index 0000000..34702bd --- /dev/null +++ b/test/programs/reload-agg-v2.flan @@ -0,0 +1,69 @@ +;;;; The aggregate case across the reload boundary, v2. +;;;; +;;;; The same four signatures with different arithmetic, so that the host's +;;;; un-rebuilt `outer' printing a different number can only mean its call +;;;; sites followed four redefined bodies that take and return structs. +;;;; +;;;; The `defstruct' blocks are byte-identical to v1's and must stay that way. +;;;; Layout is computed per module, so a field reordered here would make the +;;;; host and the module disagree about offsets — a real bug, but one wearing +;;;; this test's clothes, and it would be indistinguishable in the transcript +;;;; from the convention mismatch the fixture exists to detect. +;;;; +;;;; The four `weigh' functions are changed and the change must be dead text: a +;;;; module declares a sibling rather than defining it, so each call has to +;;;; land on the host's copy. With the bodies identical nothing at run time +;;;; would notice a module that grew its own; multiplied by ten, it is the +;;;; difference between 1611 and 12411 in the first term alone. +;;;; +;;;; Nothing here introduces a name the host was not built with. X86.redefinition +;;;; refuses those by name — that is the registry path, and it is item 1 of +;;;; HANDOFF-x86-redef.md's "what remains" rather than anything to do with +;;;; aggregates. + +(defstruct Pair [a i64 b i64]) +(defstruct Quad [a i64 b i64 c i64 d i64]) +(defstruct Duo [x f64 y f64]) +(defstruct Mix [n i64 z f64]) + +(defvar counter i64) + +(defn weigh-pair [p Pair] i64 (+ (.a p) (* 30 (.b p)))) + +(defn weigh-quad [q Quad] i64 + (+ (+ (.a q) (* 30 (.b q))) (+ (* 50 (.c q)) (* 70 (.d q))))) + +(defn weigh-duo [d Duo] i64 (+ (i64 (.x d)) (* 30 (i64 (.y d))))) + +(defn weigh-mix [m Mix] i64 (+ (.n m) (* 30 (i64 (.z m))))) + +(defn step-pair [p Pair] Pair + (println "a2") + (set counter (+ counter 10)) + (Pair {.a (+ (.a p) 10) .b (+ (.b p) (* 2 (weigh-pair p)))})) + +(defn step-quad [q Quad] Quad + (Quad {.a (+ (.a q) 10) .b (+ (.b q) 20) .c (+ (.c q) 30) + .d (+ (.d q) (* 2 (weigh-quad q)))})) + +(defn step-duo [d Duo] Duo + (Duo {.x (+ (.x d) 10.0) .y (+ (.y d) (f64 (* 2 (weigh-duo d))))})) + +(defn step-mix [m Mix] Mix + (Mix {.n (+ (.n m) 10) .z (+ (.z m) (f64 (* 2 (weigh-mix m))))})) + +(defn sum-pair [p Pair] i64 (+ (.a p) (* 100 (.b p)))) + +(defn sum-quad [q Quad] i64 + (+ (+ (.a q) (* 100 (.b q))) (+ (* 10000 (.c q)) (* 1000000 (.d q))))) + +(defn sum-duo [d Duo] i64 (+ (i64 (.x d)) (* 100 (i64 (.y d))))) + +(defn sum-mix [m Mix] i64 (+ (.n m) (* 100 (i64 (.z m))))) + +(defn outer [] i64 + (let [p (step-pair (Pair {.a 1 .b 2})) + q (step-quad (Quad {.a 1 .b 2 .c 3 .d 4})) + d (step-duo (Duo {.x 1.0 .y 2.0})) + m (step-mix (Mix {.n 1 .z 2.0}))] + (+ (+ (sum-pair p) (sum-quad q)) (+ (sum-duo d) (sum-mix m))))) diff --git a/test/programs/reload-agg.flan b/test/programs/reload-agg.flan new file mode 100644 index 0000000..840991f --- /dev/null +++ b/test/programs/reload-agg.flan @@ -0,0 +1,101 @@ +;;;; The aggregate case across the reload boundary, v1 (HANDOFF-x86-redef.md, +;;;; item 4). +;;;; +;;;; `reload.flan' proves that a redefined body is reached; every signature in +;;;; it is scalar. That is the half of the reload primitive the two backends +;;;; cannot disagree about. `lib/x86.ml' licenses its own calling convention on +;;;; the grounds that a dev build is compiled entirely by it and a release +;;;; build entirely by LLVM, and the conventions agree on every scalar and +;;;; disagree on every aggregate — here each goes by pointer with a hidden +;;;; sret, while LLVM classifies per eightbyte. So a redefined function taking +;;;; or returning a struct is the case that would expose a mismatch, and it is +;;;; the case nothing measured. This fixture is that case. +;;;; +;;;; No `main': the host is test/reload_host.c, unchanged, which links this and +;;;; then dlopens rebuilt copies. Everything aggregate happens *inside* Flan, +;;;; between the host's compiled-once call site and the redefined body. The C +;;;; boundary stays scalar on purpose — that is where the two conventions are +;;;; required to agree, and it is not what is under test. +;;;; +;;;; Four struct shapes, because SysV treats them four different ways and +;;;; x86.ml treats all four the same: +;;;; +;;;; Pair two eightbytes, both INTEGER — SysV passes it in rdi:rsi and +;;;; returns it in rax:rdx. Diverges from x86.ml in both directions. +;;;; Quad thirty-two bytes, so MEMORY — SysV copies the argument onto the +;;;; stack, where x86.ml passes a pointer. The *return* is a hidden +;;;; pointer in the first integer register for SysV too, so that half +;;;; of the matrix may well coincide; it is covered because assuming +;;;; which half coincides is exactly the kind of argument this fixture +;;;; exists to replace with a measurement. +;;;; Duo two SSE eightbytes — xmm0:xmm1. +;;;; Mix one INTEGER and one SSE — rax and xmm0, a third pattern again. +;;;; +;;;; Every field is weighted by position in the answer — a + 100b + 10000c — +;;;; rather than summed. A symmetric sum would print the right number under a +;;;; convention mismatch that merely permuted the fields, which is the way a +;;;; test like this passes while proving nothing. + +(defstruct Pair [a i64 b i64]) +(defstruct Quad [a i64 b i64 c i64 d i64]) +(defstruct Duo [x f64 y f64]) +(defstruct Mix [n i64 z f64]) + +;;; The state that has to survive a reload, written by a loaded module rather +;;; than by the host: a redefinition declares it external, so the store lands +;;; on the host's copy and not on a private one. +(defvar counter i64) + +;;; The other direction. These are never redefined, so a module reaches each +;;; one through its cell and hands it an aggregate — module to host, where the +;;; four `step' functions below are host to module. Each is also a tripwire: +;;; v2 changes all four, and since a module declares a sibling rather than +;;; defining it, that changed text must be dead. A module that grew its own +;;; copy prints a visibly different number. +(defn weigh-pair [p Pair] i64 (+ (.a p) (* 3 (.b p)))) + +(defn weigh-quad [q Quad] i64 + (+ (+ (.a q) (* 3 (.b q))) (+ (* 5 (.c q)) (* 7 (.d q))))) + +(defn weigh-duo [d Duo] i64 (+ (i64 (.x d)) (* 3 (i64 (.y d))))) + +(defn weigh-mix [m Mix] i64 (+ (.n m) (* 3 (i64 (.z m))))) + +;;; The four redefined bodies. Each takes an aggregate and returns one, so a +;;; single call crosses the boundary in both directions at once. +(defn step-pair [p Pair] Pair + (println "a1") + (set counter (+ counter 1)) + (Pair {.a (+ (.a p) 1) .b (+ (.b p) (weigh-pair p))})) + +(defn step-quad [q Quad] Quad + (Quad {.a (+ (.a q) 1) .b (+ (.b q) 2) .c (+ (.c q) 3) + .d (+ (.d q) (weigh-quad q))})) + +(defn step-duo [d Duo] Duo + (Duo {.x (+ (.x d) 1.0) .y (+ (.y d) (f64 (weigh-duo d)))})) + +(defn step-mix [m Mix] Mix + (Mix {.n (+ (.n m) 1) .z (+ (.z m) (f64 (weigh-mix m)))})) + +;;; The reducers the host itself calls, so that what crosses back into C is an +;;; integer and the transcript is exact. +(defn sum-pair [p Pair] i64 (+ (.a p) (* 100 (.b p)))) + +(defn sum-quad [q Quad] i64 + (+ (+ (.a q) (* 100 (.b q))) (+ (* 10000 (.c q)) (* 1000000 (.d q))))) + +(defn sum-duo [d Duo] i64 (+ (i64 (.x d)) (* 100 (i64 (.y d))))) + +(defn sum-mix [m Mix] i64 (+ (.n m) (* 100 (i64 (.z m))))) + +;;; The call site that has to follow a reload: compiled once, into the host, +;;; and never rebuilt. If a redefined `step-pair' runs when the host calls +;;; this, the cell is doing its job — and doing it for a signature the two +;;; conventions disagree about. +(defn outer [] i64 + (let [p (step-pair (Pair {.a 1 .b 2})) + q (step-quad (Quad {.a 1 .b 2 .c 3 .d 4})) + d (step-duo (Duo {.x 1.0 .y 2.0})) + m (step-mix (Mix {.n 1 .z 2.0}))] + (+ (+ (sum-pair p) (sum-quad q)) (+ (sum-duo d) (sum-mix m))))) diff --git a/test/test_reload.ml b/test/test_reload.ml index 626f0a3..b5ed8a3 100644 --- a/test/test_reload.ml +++ b/test/test_reload.ml @@ -252,6 +252,102 @@ let () = | _ -> fail "x86 redefinition accepted a name the host does not have" | exception X86.Unsupported _ -> ()); + (* The aggregate case, which is the whole reason X86.redefinition exists + rather than an --x86 host dlopening what Emit.redefinition made. + + Everything above this point is scalar, and scalars are the half of the + calling convention the two backends cannot disagree about. They disagree + on every aggregate: x86.ml passes each one by pointer and returns it + through a hidden sret, LLVM classifies per eightbyte. So a redefined + function taking or returning a struct is the case that would expose a + mismatch, and until now the claim that an --x86 host plus --x86 modules + is same-convention-by-construction was an argument rather than a + measurement. + + programs/reload-agg.flan crosses the boundary in four shapes at once — + two integer eightbytes, thirty-two bytes of MEMORY, two SSE eightbytes, + and one of each — because SysV treats those four differently and this + backend treats them identically, so a single shape would measure a + quarter of the disagreement and read like all of it. Each `step' takes + an aggregate and returns one, so a single call crosses in both + directions, and each calls a `weigh' the module does not define, which + hands an aggregate the other way. + + Both backends run the same fixture and are compared against the same + transcript. The LLVM row is not decoration: a wrong expected number + would otherwise be indistinguishable from a backend that is right, and + two independently-built agreements on one string are what rule that + out. *) + let a1 = checked "programs/reload-agg.flan" in + let a2 = checked "programs/reload-agg-v2.flan" in + let agg_known = + let names = + List.map (fun (f : Tast.fn) -> f.Tast.name) a1.Tast.fns + @ List.map (fun (g : Tast.global) -> g.Tast.gname) a1.Tast.globals + in + fun n -> List.exists (String.equal n) names + in + let agg_fns = [ "step-pair"; "step-quad"; "step-duo"; "step-mix" ] in + (* The arithmetic, derived rather than observed, because a number read off + a run is a record of what happened and not a statement of what should: + + v1 Pair {1,2} -> weigh 1+3*2 = 7, so {2, 2+7} and 2 + 100*9 = 902 + Quad {1,2,3,4} -> weigh (1+6)+(15+28) = 50, so {2,4,6,54} and + 2 + 400 + 60000 + 54000000 = 54060402 + Duo {1,2} -> weigh 7, so {2.0, 9.0} and 902 + Mix {1,2} -> weigh 7, so {2, 9.0} and 902 + total 54063108 + v2 Pair -> weigh is still the *host's* 7, so {11, 2+14} and 1611 + Quad -> weigh still 50, so {11,22,33,104} and + 11 + 2200 + 330000 + 104000000 = 104332211 + Duo -> {11.0, 16.0} and 1611 + Mix -> {11, 16.0} and 1611 + total 104337044 + + 1611 rather than 12411 in the first term is the tripwire: v2's text for + `weigh-pair' multiplies by thirty, and a module that grew its own copy + of a sibling rather than reaching the host's through a cell would say + so here. `counter' is stepped from inside the redefined body, by one in + v1 and by ten in v2, so 1 + 1 + 10 = 12 is the host's global being + written by three different bodies in turn. *) + let agg_want = + "a1\nhost 54063108\na1\nafter1 54063108\na2\nafter2 104337044\n\ + counter 12\n" + in + let agg_run label opts mkmod = + let h = tmp ("agg-host-" ^ label) in + ignore + (Build.executable ~opts ~csrcs:[ "reload_host.c" ] ~lflags:[ "-ldl" ] + a1 ~out:h); + let m1 = mkmod a1 ("agg-" ^ label ^ "-1.so") in + let m2 = mkmod a2 ("agg-" ^ label ^ "-2.so") in + let o = tmp ("agg-out-" ^ label) and e = tmp ("agg-err-" ^ label) in + let code = + Sys.command + (Printf.sprintf "%s %s %s > %s 2> %s" (Filename.quote h) + (Filename.quote m1) (Filename.quote m2) (Filename.quote o) + (Filename.quote e)) + in + let text = In_channel.with_open_bin o In_channel.input_all in + if code <> 0 || text <> agg_want then + fail "%s aggregate reload\n got: %S (exit %d)\n wanted: %S" + label text code agg_want; + List.iter (fun p -> try Sys.remove p with Sys_error _ -> ()) + [ h; m1; m2; o; e ] + in + agg_run "llvm" dev (fun q name -> + let o = tmp name in + let ir = Emit.redefinition ~dev:true ~known:agg_known q ~fns:agg_fns in + ignore (Build.shared ~opts:dev ~ir ~out:o ()); + o); + agg_run "x86" x86 (fun q name -> + let o = tmp name in + let asm = + X86.redefinition ~checks:true ~dev:true ~known:agg_known q ~fns:agg_fns + in + ignore (Build.shared_x86 ~opts:x86 ~asm ~out:o ()); + o); + (* The layout-drift guard, which needs a process of its own because what it does is abort one. [extra] does not exist in the host: v3 introduced it at run time, so flan_dev.c allocated its storage and recorded its size, From ed3291550180d2afe4cc2b0901d888abf9f9e101 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:15:40 +0700 Subject: [PATCH 3/4] The two redefinition builders refuse to be crossed --- lib/build.ml | 27 +++++++++++++++++++++++++++ test/test_reload.ml | 29 +++++++++++++++++++++++++++++ 2 files changed, 56 insertions(+) diff --git a/lib/build.ml b/lib/build.ml index e4f62ac..e0726d3 100644 --- a/lib/build.ml +++ b/lib/build.ml @@ -879,6 +879,25 @@ let run what cmd = let shared ?(opts = default) ~ir ~out () : timing = let opts = if opts.debug then { opts with opt = "-O0" } else opts in + (* An [--x86] host must get [--x86] modules, and this is the one place that + can say so cheaply. The two backends' conventions agree on every scalar + and disagree on every aggregate, so a crossed pair links, loads, and then + dies at the first call into a redefined function that takes or returns a + struct — measured as SIGSEGV, in test_reload.ml's aggregate section. The + option record is where the backend choice lives, so a builder handed the + other backend's record refuses by name rather than producing that object. + + This is a guard and not a proof: a caller holding two option records can + still pick the wrong one, and the loaded object carries no mark saying + which backend made it. The complete answer is a marker symbol the host + defines and a module references, so the loader refuses the pair at dlopen + rather than the processor refusing it at a call. See + HANDOFF-x86-aggregates.md. *) + if opts.x86 then + failwith + "--x86: Build.shared is the LLVM redefinition path, and an --x86 host \ + must get --x86 modules — the two calling conventions disagree on every \ + aggregate. Use Build.shared_x86 with X86.redefinition."; if wasm_target opts then failwith ((if web_target opts then "web" else "wasm32") @@ -928,6 +947,14 @@ let shared ?(opts = default) ~ir ~out () : timing = let assembler = try Sys.getenv "FLAN_AS" with Not_found -> "as" let shared_x86 ?(opts = default) ~asm ~out () : timing = + (* The other half of the same guard, and it is the half that costs nothing to + get right: a module built here for a host that was built by LLVM is the + same mismatch seen from the other side. *) + if not opts.x86 then + failwith + "Build.shared_x86 is the --x86 redefinition path and was handed an LLVM \ + option record — an --x86 host must get --x86 modules, and an LLVM host \ + must get LLVM ones. Set [x86] on the options, or use Build.shared."; let dir = workdir () in let base = Filename.remove_extension (Filename.basename out) in let src = Filename.concat dir (base ^ ".s") in diff --git a/test/test_reload.ml b/test/test_reload.ml index b5ed8a3..f690f5f 100644 --- a/test/test_reload.ml +++ b/test/test_reload.ml @@ -347,6 +347,35 @@ let () = in ignore (Build.shared_x86 ~opts:x86 ~asm ~out:o ()); o); + (* The mismatch, which is the same measurement run crossed. An --x86 host + given LLVM-built modules dies with SIGSEGV on the first call into a + redefined aggregate body — measured, not argued: + + got: "a1\nhost 54063108\na1\n" (exit 139) + + That is not asserted here. It is undefined behaviour and what it prints + is a property of whichever LLVM is installed; a test that pins it would + be pinning the shape of a crash. What is asserted is that the two + builders refuse to be crossed when the option record says which backend + is in play — see below. *) + + (* Which is the only thing that stands between a future caller and that + segfault. [Build.opts] is where the backend choice lives, so a builder + handed an option record belonging to the other backend refuses rather + than producing an object that links, loads, and then dies at a call + site. It is not a complete defence and must not be read as one: a caller + that keeps two option records and picks the wrong one by hand defeats + it, and the CLI can still do exactly that — see + HANDOFF-x86-aggregates.md. *) + (match Build.shared ~opts:x86 ~ir:"" ~out:(tmp "never.so") () with + | _ -> fail "Build.shared accepted an --x86 option record" + | exception Failure m when has m "--x86" -> () + | exception Failure m -> fail "Build.shared refused for the wrong reason: %s" m); + (match Build.shared_x86 ~opts:dev ~asm:"" ~out:(tmp "never.so") () with + | _ -> fail "Build.shared_x86 accepted an LLVM option record" + | exception Failure m when has m "--x86" -> () + | exception Failure m -> + fail "Build.shared_x86 refused for the wrong reason: %s" m); (* The layout-drift guard, which needs a process of its own because what it does is abort one. [extra] does not exist in the host: v3 introduced it From c9394a6bcd874fa4c4fdf2e1af4451ed3025cd88 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:18:25 +0700 Subject: [PATCH 4/4] The mismatch is reachable from flan reload, and the guard does not close it --- HANDOFF-x86-aggregates.md | 188 ++++++++++++++++++++++++++++++-------- lib/build.ml | 16 ++-- test/test_reload.ml | 19 ++-- 3 files changed, 168 insertions(+), 55 deletions(-) diff --git a/HANDOFF-x86-aggregates.md b/HANDOFF-x86-aggregates.md index 1dc9a9b..17d41a2 100644 --- a/HANDOFF-x86-aggregates.md +++ b/HANDOFF-x86-aggregates.md @@ -4,46 +4,156 @@ Branch `dev-loop`, from `957ba07`. This closes item 4 of `HANDOFF-x86-redef.md`: takes and returns a struct, which is the one case the two backends' conventions disagree about and the reason `X86.redefinition` exists at all rather than reusing `Emit.redefinition`. -*Status: in progress. This file is written early and on purpose, so that a lane that picks the work up mid-way -has the plan and not just the diff.* +**The claim is now measured and it holds.** An `--x86` host dlopening `--x86` modules gets the right answer +when four redefined functions each take a struct and return one. The same fixture, built and reloaded entirely +through LLVM, prints the same transcript. And the crossed pair — an `--x86` host given LLVM-built modules — +dies with SIGSEGV on the first such call, which is the measurement the "same-convention-by-construction" +argument was standing in for. -## The plan +## What was built -1. A fixture pair, `test/programs/reload-agg.flan` and `reload-agg-v2.flan`, beside the existing `reload.flan` - rather than inside it — `reload.flan`'s transcript is shared with the LLVM path and must not move. - No `main`; the host is `test/reload_host.c` unchanged, which wants `outer : () -> i64` and a `counter` - global. Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the - redefined body, because the C boundary is where the two conventions are required to agree and is not what - is under test. -2. Four struct shapes, because SysV treats them in four different ways and `x86.ml` treats all four the same: - - `≤16 bytes, all integer` — SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`; `x86.ml` passes a - pointer and returns through a hidden `sret`. Diverges in both directions. - - `>16 bytes` — SysV copies the argument onto the stack, which `x86.ml` does not; the *return*, though, - is a hidden pointer in the first integer register for SysV too, so that half may well coincide. Worth - knowing, and worth not assuming either way. - - `{f64, f64}` — SysV classifies both eightbytes SSE and uses `xmm0`:`xmm1`. - - `{i64, f64}` — one INTEGER and one SSE eightbyte, so `rax` and `xmm0`, which is a third register pattern - again. -3. Every field weighted by position in the printed answer (`a + 100*b + 10000*c + …`), so that a scrambled - field order, a wrong base pointer or a half-loaded eightbyte prints a visibly wrong integer rather than the - right one by symmetry. A test whose answer is a symmetric sum of the fields passes under a convention - mismatch that merely permutes them. -4. Run it on both backends: the LLVM `Emit.redefinition` path as the control, and the `X86.redefinition` path - as the claim. The same transcript from both is the measurement. - -## Open questions recorded rather than asked - -- Whether the MEMORY-return half of the matrix genuinely coincides between the two conventions, or only looks - as though it should. Measured by the mismatch spike rather than argued. - -## Baseline - -| | before | +| file | what | |---|---| -| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 refused | -| `spike/x86/cells.sh` | 4/4 ok | -| `dune test --root .` | exit 0 | +| `test/programs/reload-agg.flan` | the fixture. No `main`, so `test/reload_host.c` is the host, unchanged | +| `test/programs/reload-agg-v2.flan` | the same four signatures with different arithmetic | +| `test/test_reload.ml` | the aggregate section, run on both backends against one transcript, plus the two refusal checks | +| `lib/build.ml` — `shared`, `shared_x86` | a symmetric refusal when the option record names the other backend. Two `failwith`s and their comments; nothing else in the file moved | -Note in advance: `survey.sh` globs `test/programs/*.flan`, so each new no-`main` fixture adds one to its -`no-main` skip count. That number moving is the fixtures existing and is not a regression; the MATCH count is -what must not move. +Nothing in `lib/x86.ml` was touched. + +## The fixture, and why it is shaped this way + +Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the redefined body. +The C boundary stays scalar on purpose: that is where the two conventions are required to agree, `check.ml` +already refuses an aggregate in a `declare` signature, and it is not what is under test. `outer` returns `i64` +and `counter` is `i64`, so `reload_host.c` needed no change at all. + +Four struct shapes, because SysV treats them four different ways and `x86.ml` treats all four the same: + +- `Pair` — two INTEGER eightbytes; SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`. +- `Quad` — thirty-two bytes, so MEMORY. +- `Duo` — two SSE eightbytes, `xmm0`:`xmm1`. +- `Mix` — one INTEGER and one SSE. + +Each of the four redefined `step-*` takes its struct and returns it, so a single call crosses the boundary in +both directions. Each calls a `weigh-*` the module does *not* define, which hands an aggregate the other way — +module to host — and doubles as the tripwire `reload.flan`'s `helper` is: v2's text for all four `weigh` +functions multiplies by ten, and since a module declares a sibling rather than defining it, that text has to be +dead. A module that grew its own copy would print 12411 where the expected transcript says 1611. + +Every field is weighted by position in the answer (`a + 100b + 10000c + 1000000d`) rather than summed. A +symmetric sum would print the right number under a convention mismatch that merely permuted the fields, which +is the way a test like this passes while proving nothing. + +The `defstruct` blocks are byte-identical between the two files and must stay that way. Layout is computed per +module, so a field reordered in v2 would make host and module disagree about offsets — a real bug, but one +wearing this test's clothes and indistinguishable in the transcript from the thing the fixture is for. + +The arithmetic in the test is derived in a comment rather than read off a run, and both backends are held to +the same string. The LLVM row is not decoration: a wrong expected number would otherwise be indistinguishable +from a backend that is right, and two independently-built agreements on one transcript are what rule that out. + +## The transcript + +``` +a1 +host 54063108 +a1 +after1 54063108 +a2 +after2 104337044 +counter 12 +``` + +Identical from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86`. +`counter` is stepped from inside the redefined body — by one in v1, by ten in v2 — so 1 + 1 + 10 = 12 is the +host's global written by three different bodies in turn. + +## The mismatch, measured + +The same run crossed: an `--x86` host, LLVM-built modules. + +``` +FAIL cross aggregate reload + got: "a1\nhost 54063108\na1\n" (exit 139) + wanted: "a1\nhost 54063108\na1\nafter1 54063108\na2\nafter2 104337044\ncounter 12\n" +``` + +Exit 139 is SIGSEGV. It dies on the first call into a redefined aggregate body, before `after1` is printed. + +Note what this does and does not say. It says the crossed pair is fatal. It does **not** give a per-shape +breakdown: `step-pair` is called first and kills the process, so `step-quad`, `step-duo` and `step-mix` never +run under the crossed pair at all. Whether the MEMORY-return half of the matrix happens to coincide between the +two conventions is still unmeasured, and would need four crossed runs isolating one `step` at a time. Nothing +in this lane needs the answer; the four shapes earn their place as *all four cross correctly on a matched +pair*, which is what was asked for. + +This case is not in `dune test`. It is undefined behaviour, and what it prints is a property of whichever LLVM +is installed; a test that pinned it would be pinning the shape of a crash. + +## The serious finding: nothing refuses a mismatched pair, and the CLI can build one + +There is no check anywhere that a redefinition module was built by the same backend as its host. +`Build.shared` and `Build.shared_x86` are unrelated functions, neither looked at `opts.x86`, and the loaded +object carries no mark saying which backend made it. + +**It is reachable from the CLI, by a user doing nothing unusual.** `bin/main.ml:441` reads `--x86` for +`flan build` only. `flan reload` (`bin/main.ml:506`–523) hardcodes `Build.shared` with +`{ default with dev = true; debug }` and has no `--x86` spelling at all. So: + +``` +flan build game.flan --x86 --dev -o game # an --x86 host, with cells +flan reload game.flan changed.flan -o v2.so # an LLVM module, silently +``` + +and the agent in `vendor/agent/flan_agent.c` dlopens `v2.so` into that host. If any redefined function in +`changed.flan` takes or returns a struct, that is the exit-139 above, at a call site, in a running game, with +nothing anywhere having said a word. + +### What was done about it + +`Build.shared` now refuses an option record with `x86` set, and `Build.shared_x86` refuses one without it, each +naming the reason. Both refusals are asserted in `test/test_reload.ml`. + +**That guard does not close the hole, and it was re-measured after landing to be sure.** The crossed run above +passes both refusals — it hands `Build.shared` an honest LLVM option record and simply loads the result into an +x86 host — and it still segfaults. The guard catches a caller holding *one* option record and reaching for the +wrong builder, which is the accident a lane wiring item 3 would make. It cannot catch a caller holding two, and +`flan reload` is exactly that caller. + +### The recommended complete fix, not done here + +A marker symbol. `X86.program` defines `flan.abi.x86` and `X86.redefinition` emits an undefined reference to +it; `Emit.program` defines `flan.abi.llvm` and `Emit.redefinition` references that. A crossed pair then fails +at `dlopen` with an undefined-symbol message naming the ABI, before a single instruction of the new body runs — +the loader refusing the pair rather than the processor refusing it at a call. It costs one symbol in each of +four functions and nothing at run time. + +It was not done here because it needs edits in `lib/x86.ml`, which two other lanes are in, and because a +refusal at the wrong moment is worse than a loud one slightly later. It should be done next, together with item +3 of `HANDOFF-x86-redef.md` — when `flan dev` and `flan reload` learn to choose host and module backend +together, the marker is what makes the choice checkable rather than merely intended. + +## Baseline, before and after + +| | before | after | +|---|---|---| +| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 REFUSED / 0 NOX86 | **99 / 0 / 0 / 0** | +| skip breakdown | 28 does-not-compile / 6 no-main / 2 runs-forever | 28 / **8** / 2 | +| `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** | +| `dune test --root .` | exit 0 | **exit 0** | + +The `no-main` count moving from 6 to 8 is the two new fixtures existing: `survey.sh` globs +`test/programs/*.flan`, and a program with no `main` fails the LLVM link and is classified there, before the +x86 build is attempted. The MATCH count is what must not move, and it did not. + +One thing to know if you re-run the survey to check this: the shell expands that glob once, when the loop +starts. A survey launched before the fixtures were written will report 6 and look like a contradiction. + +## What remains + +- The marker symbol above, and item 3 of `HANDOFF-x86-redef.md` with it. +- A per-shape crossed measurement, if anyone ever wants to know *which* of the four disagree and how. Four runs + isolating one `step` at a time. Nothing depends on it. +- Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched: the new-name path, the transient thunk, and items 2–7 + of `HANDOFF-x86-rt.md` §6. diff --git a/lib/build.ml b/lib/build.ml index e0726d3..f9d35e5 100644 --- a/lib/build.ml +++ b/lib/build.ml @@ -887,12 +887,16 @@ let shared ?(opts = default) ~ir ~out () : timing = option record is where the backend choice lives, so a builder handed the other backend's record refuses by name rather than producing that object. - This is a guard and not a proof: a caller holding two option records can - still pick the wrong one, and the loaded object carries no mark saying - which backend made it. The complete answer is a marker symbol the host - defines and a module references, so the loader refuses the pair at dlopen - rather than the processor refusing it at a call. See - HANDOFF-x86-aggregates.md. *) + Be clear about how little this catches, because a guard that reads wider + than it is is worse than none. It catches a caller holding one option + record and reaching for the wrong builder. It does not catch a caller + holding two and picking the wrong one — the crossed pair that was measured + segfaulting passes this check and still segfaults, because it hands an + LLVM record to the LLVM builder and simply loads the result into an x86 + host. [flan reload] is precisely that caller. The complete answer is a + marker symbol the host defines and a module references, so the loader + refuses the pair at dlopen rather than the processor refusing it at a + call. See HANDOFF-x86-aggregates.md. *) if opts.x86 then failwith "--x86: Build.shared is the LLVM redefinition path, and an --x86 host \ diff --git a/test/test_reload.ml b/test/test_reload.ml index f690f5f..083489a 100644 --- a/test/test_reload.ml +++ b/test/test_reload.ml @@ -355,17 +355,16 @@ let () = That is not asserted here. It is undefined behaviour and what it prints is a property of whichever LLVM is installed; a test that pins it would - be pinning the shape of a crash. What is asserted is that the two - builders refuse to be crossed when the option record says which backend - is in play — see below. *) + be pinning the shape of a crash. - (* Which is the only thing that stands between a future caller and that - segfault. [Build.opts] is where the backend choice lives, so a builder - handed an option record belonging to the other backend refuses rather - than producing an object that links, loads, and then dies at a call - site. It is not a complete defence and must not be read as one: a caller - that keeps two option records and picks the wrong one by hand defeats - it, and the CLI can still do exactly that — see + What is asserted is narrower, and the gap between the two is the finding + rather than a caveat on it: [Build.opts] is where the backend choice + lives, so a builder handed the *other* backend's option record refuses. + The crossed run above passes both refusals — it hands [Build.shared] an + LLVM record and never calls [Build.shared_x86] at all — and it still + segfaults with this guard in place, re-measured after it landed. The + guard catches a caller holding one option record; it cannot catch a + caller holding two, and [flan reload] is exactly that caller. See HANDOFF-x86-aggregates.md. *) (match Build.shared ~opts:x86 ~ir:"" ~out:(tmp "never.so") () with | _ -> fail "Build.shared accepted an --x86 option record"