JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'worktree-agent-ab6daf83988bee428' into dev-loop

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-13 22:50:40 +07:00
commit 60d4c762e1
4 changed files with 272 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

191
HANDOFF-x86-guards.md Normal file
View File

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

25
lib/x86.ml
View File

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

53
spike/x86/p10-defer-transfer.flan Normal file
View File

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

10
spike/x86/p9-dead-defers.flan Normal file
View File

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