From b0f21ae5131db6d45a92da2785afa668c5a3bea2 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 22:36:14 +0700 Subject: [PATCH] Item 5's guard is reachable in ten lines, and a stub handoff --- HANDOFF-x86-guards.md | 49 +++++++++++++++++++++++++++++++++++++++++++ spike/x86/g5.flan | 10 +++++++++ 2 files changed, 59 insertions(+) create mode 100644 HANDOFF-x86-guards.md create mode 100644 spike/x86/g5.flan diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md new file mode 100644 index 0000000..940548f --- /dev/null +++ b/HANDOFF-x86-guards.md @@ -0,0 +1,49 @@ +# 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 + +```flan +(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) diff --git a/spike/x86/g5.flan b/spike/x86/g5.flan new file mode 100644 index 0000000..643f7c3 --- /dev/null +++ b/spike/x86/g5.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)