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

A smaller hunk, and the restart-case shape that is not a counterexample

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-13 22:46:16 +07:00
parent 1e816702b6
commit 624a94af7b
2 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
HANDOFF-x86-guards.md
View File

@ -63,6 +63,11 @@ foreign call gets neither, correctly: a transfer cannot cross a C frame, because
signature C sees. So `unwound` is false **exactly** when no transfer can arrive, and the defers on that exit are 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. 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 ### The edit, for the merge
`lib/x86.ml`, in `emit_fn`, the tail of the transfer-exit block. The six lines that were `lib/x86.ml`, in `emit_fn`, the tail of the transfer-exit block. The six lines that were

8
lib/x86.ml
View File

@ -2230,7 +2230,7 @@ let emit_fn (md : Emit.m) ~externs ~fns (fn : Tast.fn) : string * string =
end end
end end
else begin zero_return (); jmp_lbl f.b f.retlbl end else begin zero_return (); jmp_lbl f.b f.retlbl end
end end;
(* And if [f.unwound] is false there is nothing to emit: the defers on the (* 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 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 refusal, on the theory that a function with a defer and no transfer exit
@ -2244,8 +2244,10 @@ let emit_fn (md : Emit.m) ~externs ~fns (fn : Tast.fn) : string * string =
emits [guard] — [Signal], [bounds_call], the two [rt_signals] entry emits [guard] — [Signal], [bounds_call], the two [rt_signals] entry
points, and every call by name or by pointer — or jumps to [current_pad] 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 outright, which is [invoke-restart] and the three re-propagating pads. So
[unwound] is false exactly when no transfer can arrive. *) [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. *) (* The prologue, now that the frame size is known. *)
let pb = create () in let pb = create () in