flan/HANDOFF-x86-guards.md

2.5 KiB

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 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.

Status: in progress. Item 5 is answered and the answer is that the guard is wrong. Item 4 is being probed.

Item 5 — "%s has defers on a transfer path nothing reaches" is reachable, and it is a real hole

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 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

(defn quiet [n i32] i32
  (defer (set log (+ log 1)))
  (* 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.

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.

Item 4 — the flan_transfer_fail branch

(being probed; see below)

Files

(to be filled in)