The plan for an x86 redefinition emitter, written before the work
This commit is contained in:
parent
b1cc67b36f
commit
dd5eac2821
86
HANDOFF-x86-redef.md
Normal file
86
HANDOFF-x86-redef.md
Normal file
@ -0,0 +1,86 @@
|
||||
# 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.
|
||||
|
||||
## The baseline this must not regress
|
||||
|
||||
Measured at the start of this session, on `b1cc67b`:
|
||||
|
||||
- `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.
|
||||
|
||||
## Why this cannot be skipped by leaning on LLVM
|
||||
|
||||
`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
|
||||
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.**
|
||||
|
||||
## The crux: PIC references to the host's symbols
|
||||
|
||||
`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**:
|
||||
|
||||
- the cells `flan.cell.<n>` (data)
|
||||
- the globals `flan.<g>` (data)
|
||||
- the sibling function bodies, when taken by address
|
||||
|
||||
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.
|
||||
|
||||
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`).
|
||||
|
||||
## Plan
|
||||
|
||||
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.
|
||||
|
||||
## Status
|
||||
|
||||
- [x] Oriented; plan above; baseline running.
|
||||
- [ ] `llc` probe for the GOTPCREL spelling.
|
||||
- [ ] `Lgot` addressing.
|
||||
- [ ] `X86.redefinition`.
|
||||
- [ ] Assembling + a test that runs it.
|
||||
Loading…
x
Reference in New Issue
Block a user