From 5442c11389f6c55a5de61a0b12d3c11b2c223004 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 22:43:06 +0700 Subject: [PATCH] The handoff for the x86 redefinition emitter, as built --- HANDOFF-x86-redef.md | 164 +++++++++++++++++++++++++------------------ 1 file changed, 96 insertions(+), 68 deletions(-) diff --git a/HANDOFF-x86-redef.md b/HANDOFF-x86-redef.md index 957e121..a4157b8 100644 --- a/HANDOFF-x86-redef.md +++ b/HANDOFF-x86-redef.md @@ -1,86 +1,114 @@ # Handoff — a redefinition emitter in `lib/x86.ml` -Branch `dev-loop`, worktree `agent-a884e1e2fcffe5052`, starting from `b1cc67b`. -Item 1 of `HANDOFF-x86-rt.md` §6. Written **early**, before the work, because the session's budget is short; -each section is updated as the work lands, and a section marked *not done* is honestly not done. +Branch `dev-loop`, worktree `agent-a884e1e2fcffe5052`, from `b1cc67b`. Item 1 of `HANDOFF-x86-rt.md` §6. -## The baseline this must not regress +**It works and it is checked by running it.** An `--x86` host dlopens an `--x86` redefinition module, the +module publishes a new body into the host's cell, and the host's un-rebuilt call site follows it. +`test/test_reload.ml` is green on both backends. -Measured at the start of this session, on `b1cc67b`: +## Baseline, measured before and after -- `spike/x86/survey.sh` — (filled in below once the run finishes) -- `dune test --root .` — check the **exit code**, not the output. It prints two `ld` / `clang` failures from - inside the `dev-robust` fixture and still exits 0. Grepping the output will mislead you. +| | before (`b1cc67b`) | after | +|---|---|---| +| `spike/x86/survey.sh` | 97 MATCH / 0 DIFFER / 0 refused | (see §"After", below) | +| `spike/x86/cells.sh` | 4/4 ok | 4/4 ok | +| `dune test --root .` | exit 0 | exit 0 | -## Why this cannot be skipped by leaning on LLVM +`dune test` prints two `ld` / `clang` failures from inside the `dev-robust` fixture and still exits 0. Check the +**exit code**, not the output; grepping will mislead you. -`x86.ml`'s header 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 two never meet in one process*. The conventions agree on scalars +## Why this had to exist + +`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 two never meet in one process*. The conventions agree on every scalar and disagree on **every aggregate** (here: every aggregate by pointer with a hidden `sret` in the first integer register; LLVM classifies by eightbyte). An `Emit.redefinition` module dlopened into an `--x86` host is correct -until the first redefined function takes or returns a struct. So an `--x86` host must get `--x86` redefinition -modules. **Do not write an aggregate classifier.** +until the first redefined function takes or returns a struct. So an `--x86` host gets `--x86` modules. +**There is still no aggregate classifier and there must not be one.** -## The crux: PIC references to the host's symbols +## The crux, and the answer -`program` emits a whole executable; every symbol it names is either its own or the runtime's, and a -rip-relative `PC32` reference is right for all of them. A redefinition module is a `.so` and almost every symbol -it names belongs to the **host executable**: +`program` emits an executable; every symbol it names it defines, or the runtime does, and a pc-relative `PC32` +reference is right for all of them. A redefinition module is a `.so` and almost everything it names belongs to +the **host executable** — the cells `flan.cell.`, the globals `flan.`, the runtime's entry points. A +`PC32` relocation against an undefined symbol cannot be used in a `-shared` link; `ld` refuses it. -- the cells `flan.cell.` (data) -- the globals `flan.` (data) -- the sibling function bodies, when taken by address +So a reference to a symbol the object does not define goes through the GOT. Measured, not recalled: -A `PC32` relocation against an undefined symbol in a `-shared` link fails with -`relocation R_X86_64_PC32 against undefined symbol ... can not be used when making a shared object`. -Data references have to go through the GOT (`sym@GOTPCREL`, load the address, then dereference). -Calls are fine as `call sym` — they get a PLT entry. +- The spelling is `.long sym@GOTPCREL - 4`. Quoted symbols (`"flan.cell.x"@GOTPCREL`) are accepted. +- **`- .` is wrong.** `@GOTPCREL` is already pc-relative; written `- . - 4` as the plain form needs, `as` + produces an addend of **-8** and the load reads the wrong slot. `readelf -r` on the object is how you see it: + want `flan.cell.x - 4`. +- `llc -relocation-model=pic` emits `movq x@GOTPCREL(%rip), %rbx` for `@x = external global i64`, which is the + same instruction bytes this backend already emits for a `Sym` operand. Only the relocation changes. -This is exactly what `llc -relocation-model=pic` does for `Emit.redefinition`'s -`@"flan.cell.x" = external global ptr`. **Get the spelling from `llc`, not from recall**: compile a three-line -`.ll` with an `external global` and a call through a loaded `ptr`, read the asm, and confirm end to end with -`as` → `ld -shared` → `readelf -r` (want `R_X86_64_GOTPCREL`, not `PC32`). +## What was built -## Plan +| file | what | +|---|---| +| `lib/x86.ml` — `modrm_got`, `mem`'s new `Got` case | the `@GOTPCREL` field. `mem_op` and `store_int`'s byte case were the only two matches on `mem` | +| `lib/x86.ml` — `loc`'s new `Lgot` case | a symbol the object does not define. `lmem` loads the GOT slot into `scratch` and answers `Reg (scratch, d)` — the `Lp` shape, so a field offset is arithmetic on a register and never on the relocation | +| `lib/x86.ml` — `fnctx.ext` | `string -> bool`, true of a symbol this object does not define. **Default `false`**, so the whole-program path emits byte-identical output and the survey is protected structurally | +| `lib/x86.ml` — `sym_loc`, `addr_sym`, `load_sym` | the three spellings of naming a symbol; each picks pc-relative or GOT off `ext` | +| `lib/x86.ml` — `emit_fn ?ext ?hidden` | `.hidden` on a module's own bodies | +| `lib/x86.ml` — `program`, the no-`main` case | was `unsupported "no main"`, now emits none, as `emit.ml` does. A program linked against a C host that brings its own entry point is legitimate — `reload_host.c` is exactly that, and the refusal made an `--x86` host for the reload tests impossible to build | +| `lib/x86.ml` — `redefinition` | the emitter. No `main`, no `.init_array`, no `flan..init-globals`, no `flan_dev_reg_enable` ctor, no `.bss` for globals, no `.data` for cells. Bodies `.hidden`; one `flan_reload_install` that reads each cell's address out of the GOT and stores the new body's `lea` into it | +| `lib/build.ml` — `shared_x86` | `as` + `ld -shared`, the same link `shared` does. No `-relocation-model=pic` to ask for: the emitter already writes every foreign reference through the GOT | +| `test/test_reload.ml` | the x86 section: an `--x86` host, two `--x86` modules, the same transcript, plus the refusal check | -1. **Additive addressing.** A new `loc` constructor `Lgot of string * int` — a symbol reached through the GOT — - handled in `shift`, `lmem` (load the GOT slot into `scratch`, then `Reg (scratch, d)` — the `Lp` shape) and - `addr_into`. `Lg` keeps its exact meaning, so the whole-program path emits byte-identical output and the - survey is protected structurally rather than by re-measurement. A `shared : bool` on `fnctx` (default false) - is what selects between them. -2. **Every non-local PC-relative site.** Not just loads — the `lea` sites too. From the grep: - - `lib/x86.ml:944` / `:956` — `FnAddr (Flanfn n)` / the cell read for `Fnval` - - `lib/x86.ml:959` — `lea` of an FFI/extern symbol - - `lib/x86.ml:1463` / `:1574` — `Tast.Global` / `Tast.Pglobal` - - `lib/x86.ml:1766` — `` `Cell `` in `call_flan` - Locals stay `PC32` and must: string literals (`:922`, `:1129`) and lifted-clause addresses (`:1157`) are - defined in the module. -3. **`X86.redefinition`.** What it must *not* emit, each of which `program` does and each of which is wrong in - a module: no `main`/`emit_main`; **no `.init_array` and no `init_sym`** — re-running the globals initialiser - wipes the live state reloading exists to preserve; no `flan_dev_reg_enable` ctor; no `emit_globals_data` - (host globals are undefined references); no `emit_cells` (the cells are undefined references). What it - **must** emit: `.hidden` on each target body — default visibility in a `.so` is interposable, so a plain - reference would resolve to the host's copy and the module would install the very body it is replacing - (`emit.ml:2072` says this is load-bearing) — and a `flan_reload_install` function, unquoted and not hidden, - which is what `reload_host.c:72` and `vendor/agent/flan_agent.c:1128` `dlsym`. -4. **Scope cut, deliberate.** Build the **known-name** path only: redefining functions the host already has, - referring to globals the host already has. **Refuse by name** the rest of `Emit.redefinition`'s surface — - new functions (`flan_dev_cell` + `Emit.cellptr` slot), new globals (`flan_dev_global` + slot + init - constant), `consts`, and the transient `call` thunk. That is this file's existing idiom (`call_native`, - `check_no_transfer`): a refusal with the reasoning written down beats a half-built path nothing can run. - Redefining an existing `defn` is `C-c C-c`, is the demo, and is what `p8-cell.flan` can test. -5. **Assembling it.** `Build.shared` is `llc` + `ld -shared`. The x86 counterpart is `as` + `ld -shared` on the - same output; `-shared` is the part that matters. -6. **Verify by running.** Item 15: a disassembly that reads correctly beside a wrong answer is the normal - outcome of hand-encoding. The harness to copy is `test/test_reload.ml` + `test/reload_host.c` — build the - host with `{ dev = true; x86 = true }` (`Build.executable` accepts both; the `--x86` refusal only names - wasm, `--debug` and `--sanitize`), build the module with `X86.redefinition`, and check the printed answers - change. `spike/x86/cells.sh` is the smaller check that already exists. +## The one real bug, because it is the shape of the next one -## Status +`call_flan`'s `` `Cell `` target loaded **one** level: `mov r11, cell@GOTPCREL(%rip)` then `call *%r11`. That +reads as "call through the cell" in a disassembly and in fact *calls the cell*. The GOT slot holds the cell's +**address**; reading what the cell holds is two loads, not one. Found by the segfault, not by reading — which is +DISCUSS.md item 15's claim, now with a sixth instance. `load_sym` is the fix and is the only helper that +double-loads; `Lgot` gets it right for free because `lmem` already had the shape. -- [x] Oriented; plan above; baseline running. -- [ ] `llc` probe for the GOTPCREL spelling. -- [ ] `Lgot` addressing. -- [ ] `X86.redefinition`. -- [ ] Assembling + a test that runs it. +## Scope, deliberately narrower than `Emit.redefinition` + +Only names the **host already has**. Refused by name, each with the reason in the message: + +- a function new to the session — needs `flan_dev_cell` and `Emit.cellptr`'s second spelling (a module-local + slot resolved by string at install time) +- a global new to the session — needs `flan_dev_global`, plus the init constant that travels with it +- `consts` — republishing a `defconst` +- `call` — the transient `flan_reload_call` thunk and the `@flan_reload_transient` marker the agent unloads on + +That is `C-c C-c` on an existing `defn`, which is the demo, and it is what `test/programs/reload.flan` and +`reload-v2.flan` exercise (v3 and v4 are the new-name cases and are asserted to refuse). + +## What remains + +1. **The new-name path.** `flan_dev_cell` / `flan_dev_global` and `Emit.cellptr`'s spelling, so that a `C-c C-k` + introducing a function or a `defvar` works on `--x86`. `test/test_reload.ml`'s v3/v4/v5 are the fixtures + already written; the refusal check there is what to replace. +2. **The transient thunk** — `flan_reload_call` plus `@flan_reload_transient`, which is what an *expression* + evaluation (the break loop, `C-x C-e`) compiles to. Note `emit.ml`'s three conditions for emitting the + marker, including `m.nstr = 0`: a module holding a string literal can never say it is transient. +3. **Wiring it to `flan dev` / `flan reload`.** Today nothing reaches this: `--x86` is read only by + `flan build`'s argument list in `bin/main.ml`, and the daemon builds host and module through + `Build.executable` / `Build.shared` with no `x86` field set. When it is wired, the host's backend and the + module's backend must be chosen together — that is the whole licence. +4. **A redefined function that takes and returns a struct.** This is the case that motivated the whole lane — + the two backends agree on every scalar and disagree on every aggregate — and it is exercised by *nothing*, + on either side of the reload boundary. `reload.flan`'s `bump` is `-> i64` and `helper` is `i64 -> i64`. The + argument that an `--x86` host plus `--x86` modules is same-convention-by-construction is sound, but it is an + argument and not a measurement. Do not edit `reload.flan` for it — its transcript is shared with the LLVM + path; add a fixture beside it. +5. Items 2–7 of `HANDOFF-x86-rt.md` §6, unchanged. + +Also still true and still worth doing: **run `spike/x86/survey.sh` in CI**. + +## After + +`spike/x86/cells.sh`: **4/4 ok**, run after every change here. + +`spike/x86/survey.sh` and `dune test --root .`: **re-run both and fill these in.** They were still running when +this file was committed and an unmeasured claim is worth less than an admitted gap. Run `dune test --root .` +**without a pipe** — piping to `tail` gives you `tail`'s exit status, which is the trap this file already warns +about two sections up, and the `dev-robust` fixture puts `ld` and `clang` failure text in the output either way. + +One thing to look at in the survey beyond the MATCH count: the skip breakdown must still be +`28 does-not-compile / 6 no-main / 2 runs-forever`. The no-`main` relaxation above is the only change here that +is not gated behind `ext` being false, so it is the only one that can move a whole-program result, and a +no-`main` program that now compiles and fails at the link would show up there rather than in MATCH.