180 lines
11 KiB
Markdown
180 lines
11 KiB
Markdown
# 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.
|
|
|
|
**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`.
|
|
|
|
## What was built
|
|
|
|
| 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 |
|
|
|
|
`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.
|
|
|
|
## The mechanism, and why it is a datum and not a call
|
|
|
|
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.
|
|
|
|
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
|
|
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.
|
|
|
|
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.
|
|
|
|
`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 / 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 </dev/null` — or a signal to this
|
|
harness's process group comes back as `SURVEY_EXIT=143`, which is not a result. The log is block-buffered
|
|
through the redirect and stays empty until the end; that is not a hang.
|
|
|
|
## 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.
|
|
- 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.
|