From 1e816702b6ec69b288b33800960d2b165ead36fc Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 22:43:52 +0700 Subject: [PATCH] The handoff for both guards: one correct, one wrong --- HANDOFF-x86-guards.md | 150 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 124 insertions(+), 26 deletions(-) diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md index 940548f..e1793f4 100644 --- a/HANDOFF-x86-guards.md +++ b/HANDOFF-x86-guards.md @@ -2,28 +2,24 @@ Branch `dev-loop`, worktree `agent-ab6daf83988bee428`, on top of `b1cc67b`. This lane is items 4 and 5 of `HANDOFF-x86-rt.md`'s "What remains": the `flan_transfer_fail` branch in the transfer exit, and the -`"defers on a transfer path nothing reaches"` refusal beside it. Both were described as guards that exist so that -if the reasoning behind them is wrong they say so, and that no program in the corpus reaches. The question this -lane was given is whether they are correct or merely untested. +`"defers on a transfer path nothing reaches"` refusal beside it. Both were described the same way — a guard that +exists so that if the reasoning behind it is wrong it says so, and that no program in the corpus reaches. The +question this lane was given is whether each is correct or merely untested. -**Status: in progress.** Item 5 is answered and the answer is that the guard is wrong. Item 4 is being probed. +**The two answers are different, and that is the whole of the result.** Item 4's guard is correct, and it is now +reached by a program and the two backends agree about it byte for byte. Item 5's guard is wrong — not the reasoning +behind it, which is sound, but the guard itself, which fires on the most ordinary function in the language. -## Item 5 — `"%s has defers on a transfer path nothing reaches"` is reachable, and it is a real hole +## Item 5 — `"defers on a transfer path nothing reaches"` is reachable in ten lines -`lib/x86.ml:2234`. It fires when a function has function-level defers (`fn.Tast.fdefers <> []`) and `f.unwound` is -false — that is, when nothing in the body ever named the function's own transfer exit as a landing pad. `f.unwound` -is set in exactly one place, `current_pad` (`lib/x86.ml:757`), when the pad stack is empty, and `current_pad` has -exactly one caller that matters here: `guard`, the two-load-and-branch check emitted after every Flan call. So the +The refusal stood at `lib/x86.ml:2234`. It fired when a function had function-level defers (`fn.Tast.fdefers <> []`) +and `f.unwound` was false — that is, when nothing in the body ever named the function's own transfer exit as its +landing pad. `f.unwound` is set in exactly one place, `current_pad` (`lib/x86.ml:757`), when the pad stack is empty, +and the caller that matters here is `guard`, the two-load-and-branch check emitted after every Flan call. So the condition reads, in source terms: **a function that has a defer and makes no guarded call at all** — neither in the body nor in the defers, which are spliced onto the normal exit path and so are lowered as part of the body. -That is not an exotic shape. `spike/x86/g5.flan` is ten lines and reaches it: - -``` -x86: quiet has defers on a transfer path nothing reaches -``` - -exit status 3, from +That is not an exotic shape. It is any leaf function with a defer. `spike/x86/p9-dead-defers.flan` is ten lines: ```flan (defn quiet [n i32] i32 @@ -31,19 +27,121 @@ exit status 3, from (* n 2)) ``` -The same program compiles and runs under LLVM. `lib/emit.ml`'s `emit_fn` (~line 2283) has no counterpart to this -refusal: it writes the whole transfer exit under `if f.unwound then`, so when nothing can unwind the block and the -defers on it are simply not emitted. The two backends agree about the *reasoning* — the defers on that path are -dead — and disagree only about what to do with the observation. `x86.ml` refuses; `emit.ml` drops them. +and before the fix it produced, at exit status 3, -**The correct lowering is to drop them,** matching `emit.ml`. The reasoning behind the guard is sound; the guard -itself is not, because "nothing reaches that path" is the ordinary case for any leaf function with a defer, not a -sign that something has gone wrong. +``` +x86: quiet has defers on a transfer path nothing reaches +``` -## Item 4 — the `flan_transfer_fail` branch +The same program compiles and runs under LLVM and prints `42` then `1`. `lib/emit.ml`'s `emit_fn` (the block at +~2283) has no counterpart to the refusal: it writes the *whole* transfer exit under `if f.unwound then`, so when +nothing can unwind, the block and the defers on it are simply not emitted. The two backends agreed about the +reasoning — the defers on that path are dead — and disagreed only about what to do with the observation. So this was +a genuine gap of exactly the kind the survey is meant to catch, and the corpus missed it only because every +`test/programs` function with a defer also happens to call something. -(being probed; see below) +### What made the fix safe rather than assumed + +Dropping the defers is right only if `unwound` is not an under-approximation — if a function could transfer while +`unwound` stayed false, the transfer exit would never be emitted and the unwinding frame would fall through its +epilogue, which is far worse than a spurious refusal. So every site in `lib/x86.ml` that can leave a transfer in the +channel and then continue was enumerated, by grepping the two writers (`xfer_store`, and `chan_into` for the calls +that signal through it): + +| line | site | what it does about the pad | +|---|---|---| +| 1098 | `Signal (Ssignal, …)` → `flan_signal` | `guard f` | +| 1110 | `Signal (Serror, …)` → `flan_error` | `guard f`, then `ud2` | +| 1619 | `bounds_call` — every bounds and slice check | `guard f`, then `ud2` | +| 1777 | `call_flan` — every call, by name or by pointer | `guard f` | +| 1822 | `call_native ~chan` — `flan_vec_at`, `flan_vec_as_slice` | `if chan then guard f` | +| 1433 | `emit_invoke_restart` | `jmp (current_pad f)` | +| 1184, 1214, 1358 | the handler-bind, with-allocator and restart-case pads re-propagating | `jmp (current_pad f)` | + +Every one of them either calls `guard` or jumps to `current_pad` outright, and both touch `current_pad`. An ordinary +foreign call gets neither, correctly: a transfer cannot cross a C frame, because the channel is not in the SysV +signature C sees. So `unwound` is false **exactly** when no transfer can arrive, and the defers on that exit are +dead in fact and not merely by assumption. + +### The edit, for the merge + +`lib/x86.ml`, in `emit_fn`, the tail of the transfer-exit block. The six lines that were + +``` + else if fn.Tast.fdefers <> [] then + (* Nothing in this function can transfer, so the second exit has no path + to it and the defers on it are dead. Left as a refusal rather than + quietly dropped: if that reasoning is ever wrong, this says so. *) + unsupported "%s has defers on a transfer path nothing reaches" + fn.Tast.name; +``` + +are gone, replaced by a comment and a bare `;` closing the preceding `if f.unwound then begin … end`. **That is the +only change to `lib/x86.ml` in this lane** — nothing else in the file was touched, and the concurrent redefinition +lane should need to resolve nothing but this one hunk. The comment records the table above so the next reader does +not have to rebuild the argument. + +## Item 4 — the `flan_transfer_fail` branch is reachable, and it is correct + +`lib/x86.ml:2229`, inside the transfer exit: while the function's defers run with the channel cleared, a fresh pad +named `cleanup` is the innermost one, and anything that finds the channel set again lands there and dies in +`flan_transfer_fail`. Two separate questions, and both now answered by a program. + +**Is the block emitted?** Yes, whenever a defer body contains a guarded call in a function that can unwind. `used` is +a `bool ref` set by `current_pad`, so a defer that only assigns — which is what `p6-transfer.flan`'s `middle` does — +never emits it. `objdump -d` over `spike/x86/p10-defer-transfer.flan` built with `--x86` finds two references to +`flan_transfer_fail`. + +**Does anything arrive there?** Yes. The thing that makes this hard to construct is that `lib/check.ml`'s +`Ast.InvokeRestart` arm (~line 1636) refuses an `invoke-restart` written *lexically* inside a `defer`, with the same +reasoning the runtime's message carries. The runtime's own comment at `runtime/flan_rt.c:449` says exactly where the +remaining case lives: "this is the one that reaches a function through a call, where nothing static could see it." +So the probe puts the `invoke-restart` in an ordinary `defn` and has the defer call it. The checker has nothing to +object to, because from where it stands `second` is a function like any other. + +`spike/x86/p10-defer-transfer.flan` is that program. `outer` establishes two nested restart-cases and a handler-bind +and calls `middle`; `deep` signals; the handler aims a transfer at `esc-one`; the transfer unwinds `deep` and then +`middle`; `middle`'s transfer exit clears the channel and runs its defers; and the defer calls `second`, which aims a +second transfer at `esc-two`. The restart frames are both still pushed at that moment — it is `outer`'s own pad that +pops them, and `outer` has not been reached — so the second transfer really is created rather than failing an +unarmed-restart or no-such-restart check first. That was the thing worth checking before writing the probe, and it +is why the second restart-case has to be established *outside* the first. + +Both backends, verbatim and identical, at exit status 134: + +``` +spike/x86/p10-defer-transfer.flan:39:7: a defer invoked a restart, which a defer may not do — it is the cleanup a transfer runs on its way out +``` + +The location is `Loc.to_string fn.Tast.floc` — `middle`'s own `defer` form — on both sides, which is the part a +hand-written backend can get wrong silently: the string is a `.rodata` label and a length in a register here and a +`string_bytes` constant there, and a wrong one looks exactly like a match to anything that only compares exit +statuses. `survey.sh` compares stderr for this reason, and this is the program that makes that comparison earn its +keep. + +So item 4's guard is not a guess that happened to be unexercised. It is right, it is the only branch either backend +has for the case, and the corpus simply had no program that started a transfer from a defer. ## Files -(to be filled in) +| file | state | what | +|---|---|---| +| `lib/x86.ml` — `emit_fn`, tail of the transfer exit | working | the item-5 refusal removed; one hunk, six lines out, a comment in. Nothing else in the file | +| `spike/x86/p9-dead-defers.flan` | working, MATCH | a leaf function with a defer and no call. Was the refusal | +| `spike/x86/p10-defer-transfer.flan` | working, MATCH at 134 | a defer that calls a function that invokes a restart, while a first transfer unwinds | + +`lib/emit.ml`, `lib/check.ml` and `runtime/flan_rt.c` were not modified; no change to any of them was needed. + +## What this leaves + +Items 1, 2, 3, 6 and 7 of `HANDOFF-x86-rt.md` are untouched and still stand. Two smaller things this lane turned up +and did not do: + +- **`emit.ml` drops the dead defers silently and now so does `x86.ml`, but neither says so.** The defers on an + unreachable transfer exit are dead code the user wrote and that never runs, which is fine and is what the spec + implies, but it is the kind of thing a `--verbose` build could reasonably mention. Not a correctness item. +- **The survey's blind spot is real and is not about these two guards.** Item 5 sat behind a ten-line program for as + long as it existed, and was reachable the whole time, because every function with a defer in `test/programs` also + calls something. `HANDOFF-x86-rt.md` already asks for `survey.sh` in CI; the stronger version of that request is + that `spike/x86` is where the shapes the corpus does not have belong, and it is worth adding them deliberately + rather than when a lane happens to need one.