diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md new file mode 100644 index 0000000..eb6b4e4 --- /dev/null +++ b/HANDOFF-x86-guards.md @@ -0,0 +1,191 @@ +# Handoff — the two unreached guards in `lib/x86.ml` + +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 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. + +**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 — `"defers on a transfer path nothing reaches"` is reachable in ten lines + +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. It is any leaf function with a defer. `spike/x86/p9-dead-defers.flan` is ten lines: + +```flan +(defn quiet [n i32] i32 + (defer (set log (+ log 1))) + (* n 2)) +``` + +and before the fix it produced, at exit status 3, + +``` +x86: quiet has defers on a transfer path nothing reaches +``` + +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. + +### 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 one shape that looks like a counterexample and is not: a function whose every call sits inside a `restart-case`, +so that no `guard` ever finds an empty pad stack. It still sets `unwound`, because the guard sets that pad's `used`, +which is what causes the pad to be emitted at all, and the pad's tail — line 1358, the transfer aimed further out +than any clause it offers — re-propagates through `current_pad` with its own frame already popped off `f.pads`. + +### 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 + +| 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. + +## The survey + +`bash spike/x86/survey.sh p9 p10` — the two new probes, both sides, built and run: + +``` +MATCH 2 +DIFFER 0 +REFUSED 0 +``` + +Worth saying what that second row proves for `p10`, because it is not obvious: the survey hands the compiler an +**absolute** `$src`, so the location string in the stderr both binaries print is the absolute path, not the +`spike/x86/…` seen by hand. The two are byte-identical anyway, which is the comparison that matters — a +hand-encoded backend that got the `.rodata` label or the length register wrong would still exit 134 and would still +look like a match to anything comparing only exit statuses. + +And the full run, `SURVEY_QUIET=1 spike/x86/survey.sh`, over `test/programs` and `spike/x86` together: + +``` +MATCH 98 +DIFFER 0 +REFUSED 0 +NOX86 0 +SKIP 36 +``` + +That is `HANDOFF-x86-rt.md`'s 97 plus `p9`, and the `SKIP` 36 is the same 28 / 6 / 2 as before. **Read it as a +sanity check and not as the verification of the fix**, for two reasons the honest version has to name: it does not +include `p10`, whose file did not exist when the run globbed the directory, and `lib/x86.ml` was rebuilt twice while +it was in flight — the `end;` fold and the comment — so some rows were built with the binary before that tidy-up and +some after. Both rebuilds were semantically identical, so the counts are not wrong, but they are not one +measurement. A clean run of the final binary, which includes `p10`, should report **99 / 0 / 0**. + +The invariant that matters is the two zeroes, and it is worth saying why the item-5 fix cannot have moved anything +else: the change removes a refusal and adds no code. A function with `f.unwound` true reaches none of it, and a +function with `f.unwound` false previously failed the whole compile. The baseline was 0 refused, so no program in the +corpus was on that branch and no program's output could change. Before the fix, `p9` was one refusal — which is the +shape the invariant exists to catch, and it caught it. + +## 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. diff --git a/lib/x86.ml b/lib/x86.ml index fc07916..ac64179 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -2296,13 +2296,24 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) end end else begin zero_return (); jmp_lbl f.b f.retlbl end - end - 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; + end; + (* And if [f.unwound] is false there is nothing to emit: the defers on the + transfer exit are dead because no path names that exit. This used to be a + refusal, on the theory that a function with a defer and no transfer exit + was a sign the reasoning had gone wrong. It is not — it is every leaf + function with a defer, and [spike/x86/p9-dead-defers.flan] is ten lines + of it. [emit.ml]'s [emit_fn] writes the whole exit under the same + [if f.unwound], and so drops them too. + + What makes the drop safe is that [unwound] is not an approximation. + Every site that can leave a transfer in the channel and keep going either + emits [guard] — [Signal], [bounds_call], the two [rt_signals] entry + points, and every call by name or by pointer — or jumps to [current_pad] + outright, which is [invoke-restart] and the three re-propagating pads. So + [unwound] is false exactly when no transfer can arrive. A function whose + every call sits inside a [restart-case] is not a counterexample: the + guard sets that pad's [used], the pad is emitted, and its tail + re-propagates through [current_pad] with the pad stack already popped. *) (* The prologue, now that the frame size is known. *) let pb = create () in diff --git a/spike/x86/p10-defer-transfer.flan b/spike/x86/p10-defer-transfer.flan new file mode 100644 index 0000000..d7b295b --- /dev/null +++ b/spike/x86/p10-defer-transfer.flan @@ -0,0 +1,53 @@ +;;;; The second transfer, which the checker can only half refuse. +;;;; +;;;; spec-conditions.md §5 says a defer is the cleanup a transfer runs on its +;;;; way out. Starting a *second* transfer from inside one would leave this +;;;; frame's defers half run with two targets and no way to choose, so both +;;;; backends emit a branch into `flan_transfer_fail` for it and the runtime +;;;; dies there with the frame's location. +;;;; +;;;; `check.ml`'s `Ast.InvokeRestart` arm refuses the *lexical* case -- an +;;;; `invoke-restart` written inside the `defer` form itself -- with the same +;;;; reasoning. What it cannot see is a defer that *calls* a function that +;;;; invokes a restart, because the callee is ordinary code and knows nothing +;;;; about who called it. That is the case below, and it is the only way to +;;;; reach the branch. +;;;; +;;;; The order matters and is what makes this a real second transfer rather +;;;; than a first one: `outer` establishes both restart-cases, calls `middle`, +;;;; `deep` signals, `outer`'s handler aims at `esc-one`, and 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 +;;;; transfer at `esc-two`. Both restart frames are still pushed: `outer`'s +;;;; pad is what pops them, and `outer` has not been reached yet. +;;;; +;;;; Exits 134 with the message on stderr, both ways. + +(defstruct Blip [n i32]) + +(defvar log i64) + +(defn deep [n i32] i32 + (signal (Blip {.n n})) + 0) + +;;; Ordinary code. The checker has nothing to object to here, because from +;;; where it stands this is a function like any other. +(defn second [] i64 + (invoke-restart 'esc-two)) + +(defn middle [n i32] i32 + (defer (set log (second))) + (deep n)) + +(defn outer [n i32] i32 + (restart-case + (restart-case + (handler-bind [(Blip [c] (invoke-restart 'esc-one))] + (middle n)) + (esc-one [] 11)) + (esc-two [] 22))) + +(defn main [] i32 + (print (outer 1)) (println "") + 0) diff --git a/spike/x86/p9-dead-defers.flan b/spike/x86/p9-dead-defers.flan new file mode 100644 index 0000000..643f7c3 --- /dev/null +++ b/spike/x86/p9-dead-defers.flan @@ -0,0 +1,10 @@ +(defvar log i64) + +(defn quiet [n i32] i32 + (defer (set log (+ log 1))) + (* n 2)) + +(defn main [] i32 + (print (quiet 21)) (println "") + (print log) (println "") + 0)