From 188e6bc72f615d337ca227e51b91bc69e1fee458 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:07:26 +0700 Subject: [PATCH] A plan for measuring the aggregate case across the reload boundary --- HANDOFF-x86-aggregates.md | 49 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 HANDOFF-x86-aggregates.md diff --git a/HANDOFF-x86-aggregates.md b/HANDOFF-x86-aggregates.md new file mode 100644 index 0000000..1dc9a9b --- /dev/null +++ b/HANDOFF-x86-aggregates.md @@ -0,0 +1,49 @@ +# 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`. + +*Status: in progress. This file is written early and on purpose, so that a lane that picks the work up mid-way +has the plan and not just the diff.* + +## The plan + +1. A fixture pair, `test/programs/reload-agg.flan` and `reload-agg-v2.flan`, beside the existing `reload.flan` + rather than inside it — `reload.flan`'s transcript is shared with the LLVM path and must not move. + No `main`; the host is `test/reload_host.c` unchanged, which wants `outer : () -> i64` and a `counter` + global. Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the + redefined body, because the C boundary is where the two conventions are required to agree and is not what + is under test. +2. Four struct shapes, because SysV treats them in four different ways and `x86.ml` treats all four the same: + - `≤16 bytes, all integer` — SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`; `x86.ml` passes a + pointer and returns through a hidden `sret`. Diverges in both directions. + - `>16 bytes` — SysV copies the argument onto the stack, which `x86.ml` does not; the *return*, though, + is a hidden pointer in the first integer register for SysV too, so that half may well coincide. Worth + knowing, and worth not assuming either way. + - `{f64, f64}` — SysV classifies both eightbytes SSE and uses `xmm0`:`xmm1`. + - `{i64, f64}` — one INTEGER and one SSE eightbyte, so `rax` and `xmm0`, which is a third register pattern + again. +3. Every field weighted by position in the printed answer (`a + 100*b + 10000*c + …`), so that a scrambled + field order, a wrong base pointer or a half-loaded eightbyte prints a visibly wrong integer rather than the + right one by symmetry. A test whose answer is a symmetric sum of the fields passes under a convention + mismatch that merely permutes them. +4. Run it on both backends: the LLVM `Emit.redefinition` path as the control, and the `X86.redefinition` path + as the claim. The same transcript from both is the measurement. + +## Open questions recorded rather than asked + +- Whether the MEMORY-return half of the matrix genuinely coincides between the two conventions, or only looks + as though it should. Measured by the mismatch spike rather than argued. + +## Baseline + +| | before | +|---|---| +| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 refused | +| `spike/x86/cells.sh` | 4/4 ok | +| `dune test --root .` | exit 0 | + +Note in advance: `survey.sh` globs `test/programs/*.flan`, so each new no-`main` fixture adds one to its +`no-main` skip count. That number moving is the fixtures existing and is not a regression; the MATCH count is +what must not move.