160 lines
8.8 KiB
Markdown
160 lines
8.8 KiB
Markdown
# 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`.
|
||
|
||
**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.
|
||
|
||
## What was built
|
||
|
||
| file | what |
|
||
|---|---|
|
||
| `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 |
|
||
|
||
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.
|