From 624a94af7b6eac4f7278c9b46a47ec91e11a0d1a Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 22:46:16 +0700 Subject: [PATCH] A smaller hunk, and the restart-case shape that is not a counterexample --- HANDOFF-x86-guards.md | 5 +++++ lib/x86.ml | 8 +++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md index e1793f4..a6fa101 100644 --- a/HANDOFF-x86-guards.md +++ b/HANDOFF-x86-guards.md @@ -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 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 diff --git a/lib/x86.ml b/lib/x86.ml index 07dbbcb..3214e78 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -2230,7 +2230,7 @@ let emit_fn (md : Emit.m) ~externs ~fns (fn : Tast.fn) : string * string = end 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 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 @@ -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 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. *) - ; + [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