From b47f137b059f7d6fe5944e479967a842cf0e305e Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:10:54 +0700 Subject: [PATCH 1/6] A plan for the ABI marker, written before the code --- HANDOFF-x86-abi-marker.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 HANDOFF-x86-abi-marker.md diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md new file mode 100644 index 0000000..c026b59 --- /dev/null +++ b/HANDOFF-x86-abi-marker.md @@ -0,0 +1,24 @@ +# Handoff — the ABI marker symbol, so a crossed pair is refused at dlopen + +Branch `dev-loop`, from `682cb74`. This closes the serious finding of `HANDOFF-x86-aggregates.md`: a +redefinition module built by one backend, dlopened into a host built by the other, links and loads and then +dies with SIGSEGV at the first call into a redefined function that takes or returns a struct. Nothing refused +it, and `flan build game.flan --x86 --dev` followed by `flan reload game.flan changed.flan` builds exactly that +pair. + +## The plan + +A marker symbol, as that handoff recommended. + +- `X86.program` defines `flan.abi.x86`; `X86.redefinition` emits a data relocation against it. +- `Emit.program` defines `flan.abi.llvm`; `Emit.redefinition` emits one against that. +- Both sides gated on `dev`, so a release build's output is byte-for-byte what it was. +- The two `dlopen` sites — `test/reload_host.c` and `vendor/agent/flan_agent.c` — recognise a `flan.abi.` + failure and say, in a sentence, that the module and the host were built by different backends. +- `test/test_reload.ml` gains the crossed pair, both directions, asserting the refusal. + +`flan reload --x86` is judged out of scope; see below. + +## Status + +In progress. This file is written early and updated as the work lands. From fa83056708fc900399279c81f9ae1e7ee11a228b Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:15:13 +0700 Subject: [PATCH 2/6] A backend mismatch is refused by the loader, and says so --- lib/emit.ml | 29 +++++++++++++ lib/x86.ml | 47 +++++++++++++++++++++ test/reload_host.c | 35 ++++++++++++++- test/test_reload.ml | 89 ++++++++++++++++++++++++++++++--------- vendor/agent/flan_agent.c | 49 ++++++++++++++++++++- 5 files changed, 228 insertions(+), 21 deletions(-) diff --git a/lib/emit.ml b/lib/emit.ml index 01b8904..213f7c9 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -78,6 +78,17 @@ let struct_name_of (t : Types.t) = let cellptr n = "@" ^ quoted ("flan.cellp." ^ n) let globalptr n = "@" ^ quoted ("flan.gp." ^ n) +(* Which backend built this image. A dev build defines its own marker and a + redefinition module emits a data relocation against the one it was built + for, so a crossed pair — an LLVM module in an [--x86] host, or the reverse — + is refused by the loader at [dlopen] instead of running until the first call + into a redefined function that takes or returns a struct, which is where the + two conventions disagree and where the crossed pair was measured dying with + SIGSEGV. See [X86.abi_marker], which is the same mechanism spelled for the + other backend, and HANDOFF-x86-abi-marker.md. *) +let abi_marker = "flan.abi.llvm" +let abi_marker_sym = "@" ^ quoted abi_marker + (* ── Types ─────────────────────────────────────────────────────────── *) let rec ll (t : Types.t) = @@ -2914,6 +2925,13 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = []) Nothing has been redefined yet, so a dev build starts out behaving exactly like a release one — the indirection is the only difference. *) if dev then begin + (* The ABI marker, defined here so a redefinition module can bind against + it, and only in a dev build: a release build has no cells and nothing to + load into one, so it keeps exactly the module text it had before this + existed. [-rdynamic] is what puts it in the executable's dynamic symbol + table, and a dev build is the only build that gets that either. *) + Buffer.add_string m.out + (Printf.sprintf "%s = global i64 0\n" abi_marker_sym); List.iter (fun (fn : Tast.fn) -> Buffer.add_string m.out @@ -3029,6 +3047,17 @@ let redefinition ?(checks = true) ?(dev = false) ?(debug = false) (globalptr g.Tast.gname))) p.Tast.globals; if dev then begin + (* The host's ABI marker, and a pointer-sized datum holding its address. + That datum is a relocation the loader has to resolve while it maps the + object, so a host built by the other backend — which defines + [flan.abi.x86] and not this — fails the [dlopen] outright, rather than + loading and then dying at the first call into a redefined function that + takes or returns a struct. Hidden, so this module's own copy can never + be interposed by another loaded module's; the relocation against the + host's marker is the only part that matters. *) + Buffer.add_string m.out + (Printf.sprintf "%s = external global i64\n%s = hidden global ptr %s\n\n" + abi_marker_sym ("@" ^ quoted "flan.abi.require") abi_marker_sym); (* The cells are the host's, like the globals. Referencing one is how a redefined function reaches its siblings, and storing into one is how it replaces itself. A name the host lacks gets a slot instead, filled by diff --git a/lib/x86.ml b/lib/x86.ml index 814903c..b180a38 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -408,6 +408,28 @@ let gsym n = asm_sym ("flan." ^ n) Byte-for-byte or the link fails and the piece served nothing. *) let csym n = asm_sym ("flan.cell." ^ n) +(* The marker that says which backend built an image, and it is the whole of + the answer to the one way these two backends can be mixed and be wrong. + [emit.ml] and this file agree on every scalar and disagree on every + aggregate — this file passes a struct by pointer with a hidden [sret] and + LLVM classifies per SysV — so a redefinition module from one backend + dlopened into a host from the other links, loads, and then dies at the first + call into a redefined function that takes or returns a struct. That was + measured as SIGSEGV; see HANDOFF-x86-aggregates.md. + + A dev build defines its own marker and a redefinition module emits a data + relocation against the marker it was itself built for. A matched pair binds + it and notices nothing. A crossed pair has no such symbol to bind, and the + loader refuses the module at [dlopen] — before a single instruction of the + new body runs, and with the missing symbol naming the backend in the + message. That is the property: the mismatch is caught by the loader rather + than by the processor, at load rather than at a call. + + [Emit.abi_marker] is the same string for the LLVM half. The two must stay + distinct and neither may ever be defined by both backends, or the refusal + quietly stops refusing. *) +let abi_marker = "flan.abi.x86" + (* ── Debug information ───────────────────────────────────────────────── *) (* DWARF, written out as bytes, for the same reason the instructions are — and @@ -3266,6 +3288,19 @@ let program ~checks ?(dev = false) ?(debug = false) (p : Tast.program) : string (Printf.sprintf "\t.section\t.init_array,\"aw\",@init_array\n\t.align\t8\n%s\ \t.quad\t%s\n\n" (if dev then "\t.quad\tflan_dev_reg_enable\n" else "") init_sym); + (* The ABI marker, and only in a dev build: it exists for redefinition + modules to bind against, a release build has no cells to load one into, + and gating it here is what keeps a release build's assembly byte-for-byte + what it was. [.globl] and default visibility, for the reason the cells + have them — a dlopened object has to be able to see it, which is also why + [Build.executable] passes [-rdynamic] for a dev build and nothing else. *) + if dev then + Buffer.add_string out + (Printf.sprintf + "\t.data\n\t.globl\t%s\n\t.align\t8\n\t.type\t%s, @object\n\ + \t.size\t%s, 8\n%s:\n\t.quad\t0\n\n" + (asm_sym abi_marker) (asm_sym abi_marker) (asm_sym abi_marker) + (asm_sym abi_marker)); if dev then Buffer.add_string out (emit_cells p); Buffer.add_string out (emit_globals_data md p.Tast.globals); Buffer.add_string out "\n\t.section\t.rodata\n"; @@ -3423,6 +3458,18 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true) "\t.size\tflan_reload_install, . - flan_reload_install\n\n"; let out = Buffer.create 8192 in Buffer.add_buffer out text; + (* The ABI marker this module requires of its host. A pointer-sized datum + holding the host's marker is a relocation the loader has to resolve while + it maps the object, whatever it does about lazy binding of calls, so a + host that does not define [flan.abi.x86] fails the [dlopen] outright. A + call would do as well under [RTLD_NOW], which is what both loaders here + pass, but a datum does not depend on that and costs eight bytes. + + The label is local: nothing outside this module names it, and only the + relocation against the marker matters. *) + Buffer.add_string out + (Printf.sprintf "\n\t.data\n\t.align\t8\n%s:\n\t.quad\t%s\n" + (asm_sym "flan.abi.require") (asm_sym abi_marker)); Buffer.add_string out "\n\t.section\t.rodata\n"; Buffer.add_buffer out rodata; Buffer.add_string out "\n\t.section\t.note.GNU-stack,\"\",@progbits\n"; diff --git a/test/reload_host.c b/test/reload_host.c index d04c28c..c22ac29 100644 --- a/test/reload_host.c +++ b/test/reload_host.c @@ -34,6 +34,7 @@ #include #include #include +#include #include /* The Flan symbols the executable itself defines. Flan names contain @@ -62,11 +63,43 @@ static double now_ms(void) { return (double)t.tv_sec * 1e3 + (double)t.tv_nsec / 1e6; } +/* The same sentence [vendor/agent/flan_agent.c] says, for the same failure. + * Duplicated rather than shared: the agent is vendored to be dropped into a + * user's game and carries no header of its own, and this host is a test + * fixture that links against neither it nor the runtime's dev half. + * + * A dev build defines a marker naming the backend that built it, and a + * redefinition module holds a pointer to the marker it was itself built for. + * The two backends agree on scalars and disagree on every aggregate, so a + * crossed pair would run until the first call into a redefined function that + * takes or returns a struct and then die with SIGSEGV. The marker turns that + * into a relocation the loader cannot resolve. What it says then is + * "undefined symbol: flan.abi.x86", so the marker's name is matched — not the + * loader's phrasing, which is libc's to change — and the reason is stated. */ +static const char *abi_mismatch(const char *err) { + if (err == NULL) return NULL; + if (strstr(err, "flan.abi.x86") != NULL) + return "the module and this host were built by different backends: the " + "module came from the x86 dev backend and needs flan.abi.x86, " + "which this host does not define. The two backends pass every " + "struct differently. Rebuild the host with --x86."; + if (strstr(err, "flan.abi.llvm") != NULL) + return "the module and this host were built by different backends: the " + "module came from LLVM and needs flan.abi.llvm, which an --x86 " + "host does not define. The two backends pass every struct " + "differently. Rebuild the host without --x86."; + return NULL; +} + static int install(const char *path) { double t0 = now_ms(); void *h = dlopen(path, RTLD_NOW | RTLD_LOCAL); if (h == NULL) { - fprintf(stderr, "dlopen %s: %s\n", path, dlerror()); + /* [dlerror] is one-shot, so the pointer is taken once and used twice. */ + const char *err = dlerror(); + const char *why = abi_mismatch(err); + if (why != NULL) fprintf(stderr, "flan: %s\n", why); + else fprintf(stderr, "dlopen %s: %s\n", path, err); return 0; } install_fn f = (install_fn)(uintptr_t)dlsym(h, "flan_reload_install"); diff --git a/test/test_reload.ml b/test/test_reload.ml index 083489a..81066e1 100644 --- a/test/test_reload.ml +++ b/test/test_reload.ml @@ -335,37 +335,88 @@ let () = 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 agg_llvm_mod 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 -> + o + in + let agg_x86_mod 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 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: + o + in + agg_run "llvm" dev agg_llvm_mod; + agg_run "x86" x86 agg_x86_mod; + + (* The same measurement run crossed, which is what the marker symbol is + for. Before it, an --x86 host given LLVM-built modules loaded them and + then died with SIGSEGV on the first call into a redefined aggregate + body: 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. + That could not be asserted. It was undefined behaviour and what it + printed was a property of whichever LLVM happened to be installed; a + test pinning it would have been pinning the shape of a crash. - 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. *) + It is deterministic now, which is why it is here. A dev build defines a + marker naming the backend that built it — [flan.abi.x86] or + [flan.abi.llvm] — and a redefinition module holds a pointer to the one + it was itself built for. That pointer is a relocation the loader has to + resolve while it maps the object, so a crossed pair fails the [dlopen] + outright, before a single instruction of the new body runs. Both + directions, because a marker only one of the two backends emitted would + refuse in one direction and say nothing in the other. + + Asserted on the message as well as the exit status, the way the + retyped-global and registry-overflow cases below are: a nonzero exit is + not by itself this refusal, and the point of the exercise is that what + reaches a user names the reason rather than repeating the loader's + "undefined symbol". *) + let agg_cross label opts mkmod wants = + let h = tmp ("agg-xhost-" ^ label) in + ignore + (Build.executable ~opts ~csrcs:[ "reload_host.c" ] ~lflags:[ "-ldl" ] + a1 ~out:h); + let m1 = mkmod a1 ("agg-cross-" ^ label ^ "-1.so") in + let o = tmp ("agg-xout-" ^ label) and e = tmp ("agg-xerr-" ^ label) in + let code = + Sys.command + (Printf.sprintf "%s %s > %s 2> %s" (Filename.quote h) + (Filename.quote m1) (Filename.quote o) (Filename.quote e)) + in + let said = In_channel.with_open_bin e In_channel.input_all in + if code = 0 then + fail "%s: a crossed pair loaded and ran (exit 0)" label; + if not (has said "built by different backends") then + fail "%s: a crossed pair was refused without naming the reason: %S" + label said; + (* Which marker is missing is which backend built the module, so this is + also what says the refusal fired for the right direction rather than + for the other one. *) + if not (has said wants) then + fail "%s: the refusal named the wrong marker (wanted %s): %S" label + wants said; + List.iter (fun p -> try Sys.remove p with Sys_error _ -> ()) + [ h; m1; o; e ] + in + (* An --x86 host handed an LLVM module: the pair the CLI can build today, + since [flan reload] has no --x86 spelling. *) + agg_cross "x86-host-llvm-module" x86 agg_llvm_mod "flan.abi.llvm"; + (* And the reverse, which no command spells but [X86.redefinition] does. *) + agg_cross "llvm-host-x86-module" dev agg_x86_mod "flan.abi.x86"; + + (* The option-record guard, which is the older and narrower half of the + same answer: [Build.opts] is where the backend choice lives, so a + builder handed the *other* backend's option record refuses by name. It + catches a caller holding one option record and reaching for the wrong + builder. It cannot catch a caller holding two — the crossed runs above + pass both of these refusals — which is what the marker is for. See + HANDOFF-x86-aggregates.md and HANDOFF-x86-abi-marker.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" -> () diff --git a/vendor/agent/flan_agent.c b/vendor/agent/flan_agent.c index 6e720be..374ed41 100644 --- a/vendor/agent/flan_agent.c +++ b/vendor/agent/flan_agent.c @@ -674,6 +674,49 @@ static void emit(sink *o, const void *p, size_t n) { static void reply(sink *o, const char *s) { emit(o, s, strlen(s)); } +/* A dlopen failure the compiler's two backends are responsible for, turned + * into a sentence that says so. + * + * Flan has two native backends. They agree about every scalar and disagree + * about every aggregate — the x86 dev backend passes a struct by pointer with + * a hidden sret, LLVM classifies it per the SysV psABI — so a redefinition + * module built by one and loaded into a host built by the other links, loads, + * and then dies with SIGSEGV at the first call into a redefined function that + * takes or returns a struct. A dev build therefore defines a marker naming its + * backend and a module holds a pointer to the marker it was built for, which + * is a relocation the loader must resolve while it maps the object. A crossed + * pair has no such symbol and is refused here, before any of the new code + * runs. + * + * What the loader says at that point is "undefined symbol: flan.abi.x86", + * which is true and tells nobody anything. So the marker's name is matched — + * the name, not the loader's phrasing, which is libc's to change — and the + * reason is stated instead. Which marker is missing says which backend built + * the module, and the host is necessarily the other one. + * + * Returns NULL for a failure that is about something else, which is then + * passed through as the loader wrote it. */ +static const char *abi_mismatch(const char *err) { + if (err == NULL) return NULL; + if (strstr(err, "flan.abi.x86") != NULL) + return "the module and the running program were built by different " + "backends: the module came from the x86 dev backend and needs " + "flan.abi.x86, which this program does not define. The two " + "backends pass every struct differently, so the pair would die at " + "the first call into a redefined function that takes or returns " + "one. Rebuild the program with --x86 so that both halves agree."; + if (strstr(err, "flan.abi.llvm") != NULL) + return "the module and the running program were built by different " + "backends: the module came from LLVM and needs flan.abi.llvm, " + "which an --x86 program does not define. The two backends pass " + "every struct differently, so the pair would die at the first call " + "into a redefined function that takes or returns one. Rebuild the " + "program without --x86: there is no --x86 spelling for building a " + "redefinition module yet, so the program is the half that has to " + "move."; + return NULL; +} + /* One line, one answer, one module. This is the whole of what the agent is * asked, and it is reached two ways: from the socket below, and — in a build * where the compiler is a thread in this same process — by being called. The @@ -1120,8 +1163,12 @@ static void handle_line(char *line, sink *o) { } void *h = dlopen(line, RTLD_NOW | RTLD_LOCAL); if (h == NULL) { + /* [dlerror] is one-shot and the next dl call may clobber what it returned, + * so the pointer is taken once and used for both the test and the reply. */ + const char *err = dlerror(); + const char *why = abi_mismatch(err); reply(o, "err "); - reply(o, dlerror()); + reply(o, why != NULL ? why : err); reply(o, "\n"); return; } From 1f30d9a06778d967f0cf6665bf2587ab7d9422db Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:19:27 +0700 Subject: [PATCH 3/6] The marker, written up: what it refuses and what it deliberately does not --- HANDOFF-x86-abi-marker.md | 143 +++++++++++++++++++++++++++++++++++--- 1 file changed, 132 insertions(+), 11 deletions(-) diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md index c026b59..9538664 100644 --- a/HANDOFF-x86-abi-marker.md +++ b/HANDOFF-x86-abi-marker.md @@ -6,19 +6,140 @@ dies with SIGSEGV at the first call into a redefined function that takes or retu it, and `flan build game.flan --x86 --dev` followed by `flan reload game.flan changed.flan` builds exactly that pair. -## The plan +**It is refused now, by the loader, before any of the new code runs, with a sentence that says why.** Both +directions are in `dune test`. -A marker symbol, as that handoff recommended. +## What was built -- `X86.program` defines `flan.abi.x86`; `X86.redefinition` emits a data relocation against it. -- `Emit.program` defines `flan.abi.llvm`; `Emit.redefinition` emits one against that. -- Both sides gated on `dev`, so a release build's output is byte-for-byte what it was. -- The two `dlopen` sites — `test/reload_host.c` and `vendor/agent/flan_agent.c` — recognise a `flan.abi.` - failure and say, in a sentence, that the module and the host were built by different backends. -- `test/test_reload.ml` gains the crossed pair, both directions, asserting the refusal. +| file | what | +|---|---| +| `lib/x86.ml` | `abi_marker = "flan.abi.x86"`. `program` defines it in `.data`, in a dev build only; `redefinition` emits a `.quad` against it | +| `lib/emit.ml` | `abi_marker = "flan.abi.llvm"`, the same two halves — a definition inside `program`'s existing `if dev` block, and an `external` plus a hidden pointer to it in `redefinition`'s | +| `vendor/agent/flan_agent.c` | `abi_mismatch`, which turns a `flan.abi.` `dlopen` failure into a sentence; the reload handler uses it | +| `test/reload_host.c` | the same function, duplicated rather than shared, and the same use at its `dlopen` | +| `test/test_reload.ml` | `agg_cross`, run both ways, asserting a nonzero exit *and* the sentence *and* which marker was missing | -`flan reload --x86` is judged out of scope; see below. +`lib/build.ml` was not touched. Its option-record guard is the other half of this answer and is unchanged; the +comment there already says what it cannot catch, which is what the marker is for. -## Status +## The mechanism, and why it is a datum and not a call -In progress. This file is written early and updated as the work lands. +A dev build defines a marker symbol naming the backend that built it. A redefinition module emits a +pointer-sized datum holding the address of the marker it was itself built for. + +That datum is the whole of it. A pointer in `.data` is a relocation the dynamic loader has to resolve while it +maps the object, whatever it does about lazy binding of calls, so a host that does not define the marker fails +the `dlopen` outright. A call into an absent function would do as well under `RTLD_NOW`, which is what both +loaders in this repo pass, but the datum does not depend on that and costs eight bytes. + +Both sides are gated on `dev`, for two reasons that happen to agree. A release build has no cells and nothing +to load into one, so the marker would be dead weight; and `Build.executable` passes `-rdynamic` only for a dev +build, so a release build could not export the symbol even if it emitted it. Gating also keeps a release +build's output byte-for-byte what it was, which `x86.ml`'s `.Ldwtext` comment says the repo cares about. +Measured on `test/programs/cleanup.flan`: + +``` +x86 --dev : 00000000004280f0 D flan.abi.x86 +llvm --dev : 000000000041d3f0 B flan.abi.llvm +x86 release : (nothing) +``` + +Macro modules are unaffected and were checked: `Build.macro_module` calls `Emit.program` without `~dev`, so a +macro module neither defines a marker nor requires one, and the OCaml-side `dlopen` in `lib/dynload_stubs.c` — +which is the *only* other `dlopen` of a Flan-built object anywhere — never sees one. It therefore got no arm, +deliberately. + +`lib/dev.ml` got no arm either, and this is worth stating because it looks like an omission. The daemon builds +the host itself and sends every module to the agent in the game process; it has no `dlopen` of a redefinition +module of its own, and `--x86` has no spelling anywhere in `dev.ml` or `session.ml`, so a `flan dev` session +builds host and modules both through LLVM and is matched by construction. The mismatch is only reachable +through `flan build --x86 --dev` plus a separately built module, and that module is loaded by the agent, which +is where the sentence lives. + +## What the crossed pair does now + +Verbatim, from the two new cases in `test/test_reload.ml`, captured from the host's stderr: + +``` +flan: the module and this host were built by different backends: the module came from LLVM and needs +flan.abi.llvm, which an --x86 host does not define. The two backends pass every struct differently. Rebuild +the host without --x86. +``` + +``` +flan: the module and this host were built by different backends: the module came from the x86 dev backend and +needs flan.abi.x86, which this host does not define. The two backends pass every struct differently. Rebuild +the host with --x86. +``` + +Exit 1 in both cases, from the host refusing to install. Before this it was exit 139 — SIGSEGV, at a call site, +after `a1` and `host 54063108` had already been printed. + +The agent's wording is longer than the test host's, because its reader is a person in an editor rather than a +test: it names the running program rather than "this host", says the pair would die at the first call into a +redefined function taking or returning a struct, and — in the LLVM-module direction — says why the program is +the half that has to move. + +Two things about the matching that are deliberate. It matches on the *marker's name*, not on `"undefined +symbol"`, which is glibc's phrasing and glibc's to change. And `dlerror` is one-shot with a buffer the next +`dl` call may clobber, so the pointer is taken once and used for both the test and the reply; the agent's +existing code called it once and still does. + +## Why it is in `dune test` now, when the segfault was not + +The aggregate lane measured the crossed pair and deliberately left it out: it was undefined behaviour, what it +printed was a property of whichever LLVM was installed, and a test pinning it would have been pinning the shape +of a crash. That is no longer true. The refusal happens in the loader, at a fixed point, before a single +instruction of the new body runs, so it is deterministic and is asserted the way the retyped-global and +registry-overflow cases already were: on the exit status *and* on the message. + +Both directions, because a marker only one backend emitted would refuse in one direction and say nothing in the +other — and the direction with no test is the direction that quietly stops working. + +The matched pairs are unchanged and still print the transcript the aggregate lane derived: + +``` +a1 / host 54063108 / a1 / after1 54063108 / a2 / after2 104337044 / counter 12 +``` + +from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86` alike. + +## `flan reload --x86` did not land, and should not have + +The brief left this to judgement. It is item 3 of `HANDOFF-x86-redef.md`, not a flag. + +`flan reload` does not build a module directly; it runs a `Session` over the program and asks +`Session.eval` for one, and `Session.change` holds a single `ir : string` field filled by +`Emit.redefinition ~consts`. Three things would have to move together: + +- `Session.change` would need a backend-tagged payload rather than an `ir` string, and every one of the six + `Emit.redefinition` call sites in `session.ml` would have to choose. +- `X86.redefinition` raises `Unsupported` on `~consts`, on `~call`, and on any name the host was not built + with. `Session.eval` passes `~consts` as a matter of course and the expression path passes `~call`. So the + x86 path would refuse most of what a session legitimately sends, and the refusals would surface as "this + works in LLVM and not in x86" rather than as anything a user could act on. +- The daemon is the real caller of all of this. Giving `flan reload` a flag the daemon does not have would + leave the two commands disagreeing about what a session can do. + +So the deliverable here is the refusal, which is the part that matters: a silent segfault is the bug. The +remedy the messages name is the one that actually exists today — rebuild the host to match the module — rather +than a flag that does not. When item 3 does land, the marker is what makes the choice checkable rather than +merely intended, and these two crossed tests are what will catch a half-done version of it. + +## Baseline + +| | before | after | +|---|---|---| +| `spike/x86/survey.sh` | 103 MATCH / 0 DIFFER / 0 REFUSED | see below | +| skip breakdown | 28 does-not-compile / 8 no-main / 2 runs-forever | see below | +| `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** | +| `dune test --root .` | exit 0, 232 checks, 0 failures | **exit 0, 232 checks, 0 failures** | + +## What remains + +- Item 3 of `HANDOFF-x86-redef.md`: `flan dev` and `flan reload` choosing host and module backend together. + The marker is now the thing that makes that checkable. +- A per-shape crossed measurement, still unmeasured and still depended on by nothing. It is *harder* to get + now, not easier: the marker refuses the pair before any of the four `step` functions runs, so anyone who + wants the answer has to build the crossed module with the marker suppressed on purpose. +- Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched. From 82557df51b9d46cc5d3c3eb19a791dc7ee9b3d85 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:22:19 +0700 Subject: [PATCH 4/6] The agent's half of the refusal is checked where it actually ships --- HANDOFF-x86-abi-marker.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md index 9538664..c95e6bb 100644 --- a/HANDOFF-x86-abi-marker.md +++ b/HANDOFF-x86-abi-marker.md @@ -80,6 +80,19 @@ test: it names the running program rather than "this host", says the pair would redefined function taking or returning a struct, and — in the LLVM-module direction — says why the program is the half that has to move. +The agent's two sentences have no unit test of their own, so they were checked the one way that matters: that +they are in a binary a user would actually run. `vendor/agent/flan_agent.c` reaches a program through the +vendor package's C sources rather than through an embedded-as-a-string module like `Runtime_src`, so an edit to +it lands without regenerating anything — but that had to be confirmed rather than assumed, because a repo that +embeds one C file that way can embed another. + +``` +flan build test/programs/agent.flan --dev -o ahost ; strings ahost | grep -c "built by different backends" → 2 +flan build test/programs/agent.flan --x86 --dev -o ahost ; strings ahost | grep -c "built by different backends" → 2 +``` + +Two, in both configurations: one sentence per direction. + Two things about the matching that are deliberate. It matches on the *marker's name*, not on `"undefined symbol"`, which is glibc's phrasing and glibc's to change. And `dlerror` is one-shot with a buffer the next `dl` call may clobber, so the pointer is taken once and used for both the test and the reply; the agent's @@ -104,6 +117,12 @@ a1 / host 54063108 / a1 / after1 54063108 / a2 / after2 104337044 / counter 12 from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86` alike. +And "a matched pair is unaffected" is checked through the agent as well as through `reload_host.c`, which is +worth saying because the two are different code paths and only one of them is what a user meets. The daemon +tests in `dune test` — `dev-globals`, `dev-repl`, `dev-watch`, `dev-pause`, `dev-loop` — start a real `flan +dev` session, build a real host, and send real redefinition modules to the agent in it over the socket. Every +one of those `dlopen`s now has to resolve `flan.abi.llvm`, and every one of those tests passes. + ## `flan reload --x86` did not land, and should not have The brief left this to judgement. It is item 3 of `HANDOFF-x86-redef.md`, not a flag. From e62b3bfe04d831376c8e9cbb0bca9c857fb9d98e Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 07:24:31 +0700 Subject: [PATCH 5/6] The survey did not move, which is what the dev gate is for --- HANDOFF-x86-abi-marker.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md index c95e6bb..edade72 100644 --- a/HANDOFF-x86-abi-marker.md +++ b/HANDOFF-x86-abi-marker.md @@ -149,11 +149,20 @@ merely intended, and these two crossed tests are what will catch a half-done ver | | before | after | |---|---|---| -| `spike/x86/survey.sh` | 103 MATCH / 0 DIFFER / 0 REFUSED | see below | -| skip breakdown | 28 does-not-compile / 8 no-main / 2 runs-forever | see below | +| `spike/x86/survey.sh` | 103 MATCH / 0 DIFFER / 0 REFUSED / 0 NOX86 | **103 / 0 / 0 / 0** | +| skip breakdown | 28 does-not-compile / 8 no-main / 2 runs-forever | **28 / 8 / 2** | | `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** | | `dune test --root .` | exit 0, 232 checks, 0 failures | **exit 0, 232 checks, 0 failures** | +The survey is the measurement that could have moved and did not, which is the point of running it: both +backends now emit a symbol into every `--dev` build, and the survey's default is a release build on both sides, +so an unguarded marker would have shown up as 103 identical-but-different objects rather than as a wrong +answer. It agrees byte-for-byte on what the programs print. + +Run it detached — `setsid timeout 2400 spike/x86/survey.sh > log 2>&1 Date: Mon, 14 Sep 2026 07:24:54 +0700 Subject: [PATCH 6/6] The marker's name is a literal in four places, and the note says so --- HANDOFF-x86-abi-marker.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/HANDOFF-x86-abi-marker.md b/HANDOFF-x86-abi-marker.md index edade72..901f24a 100644 --- a/HANDOFF-x86-abi-marker.md +++ b/HANDOFF-x86-abi-marker.md @@ -171,3 +171,9 @@ through the redirect and stays empty until the end; that is not a hang. now, not easier: the marker refuses the pair before any of the four `step` functions runs, so anyone who wants the answer has to build the crossed module with the marker suppressed on purpose. - Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched. +- A seam worth knowing about before anyone renames a marker. The two strings live in OCaml — `X86.abi_marker` + and `Emit.abi_marker` — and the two `abi_mismatch` functions match the same literals in C, with nothing + linking the four. Rename one and the refusal still fires, because the symbol is still missing; it just stops + being a sentence and reverts to the loader's bare "undefined symbol", which is the failure this lane was + about. The crossed tests would catch it — they assert on the marker's name — so the seam is guarded, but it + is a seam.