The two redefinition builders refuse to be crossed

This commit is contained in:
Joseph Ferano 2026-09-13 23:15:40 +07:00
parent 8ae77db92c
commit ed32915501
2 changed files with 56 additions and 0 deletions

View File

@ -879,6 +879,25 @@ let run what cmd =
let shared ?(opts = default) ~ir ~out () : timing = let shared ?(opts = default) ~ir ~out () : timing =
let opts = if opts.debug then { opts with opt = "-O0" } else opts in 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 if wasm_target opts then
failwith failwith
((if web_target opts then "web" else "wasm32") ((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 assembler = try Sys.getenv "FLAN_AS" with Not_found -> "as"
let shared_x86 ?(opts = default) ~asm ~out () : timing = 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 dir = workdir () in
let base = Filename.remove_extension (Filename.basename out) in let base = Filename.remove_extension (Filename.basename out) in
let src = Filename.concat dir (base ^ ".s") in let src = Filename.concat dir (base ^ ".s") in

View File

@ -347,6 +347,35 @@ let () =
in in
ignore (Build.shared_x86 ~opts:x86 ~asm ~out:o ()); ignore (Build.shared_x86 ~opts:x86 ~asm ~out:o ());
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 (* 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 does is abort one. [extra] does not exist in the host: v3 introduced it