flan/HANDOFF-x86-redef.md

5.7 KiB

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 asld -sharedreadelf -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 / :956FnAddr (Flanfn n) / the cell read for Fnval
    • lib/x86.ml:959lea of an FFI/extern symbol
    • lib/x86.ml:1463 / :1574Tast.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

  • Oriented; plan above; baseline running.
  • llc probe for the GOTPCREL spelling.
  • Lgot addressing.
  • X86.redefinition.
  • Assembling + a test that runs it.