148 lines
9.5 KiB
Markdown
148 lines
9.5 KiB
Markdown
# 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 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.
|
|
|
|
## 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.
|