Optimized path: spill frame not deallocated before return (missing 'add sp') on a function with control flow

[avrabe]

Summary

On the optimized (non---relocatable) ARM path, a function that BOTH spills to a stack frame (sub sp,#N) AND contains control flow emits no matching add sp,#N before its return, so it returns with SP imbalanced by N bytes — corrupting the caller's stack. Pre-existing; the --relocatable direct path is unaffected.

Repro (generic)

(module
  (memory 1)
  (export "memory" (memory 0))
  (func (export "nested") (param $sel i32)
    (i32.store (i32.const 20) (i32.const 55))
    (block $outer
      (block $inner
        (br_if $inner (i32.eqz (local.get $sel)))
        (br $outer))
      (i32.store8  (i32.const 24) (i32.const 66))
      (i32.store16 (i32.const 26) (i32.const 77))
      (i32.store8  (i32.const 28) (i32.const 88)))
    (i32.store (i32.const 32) (i32.const 99))))

synth compile nested_heavy.wat -o /tmp/nh.elf -b arm --target cortex-m4 --all-exports
arm-none-eabi-objdump -d -M force-thumb /tmp/nh.elf

nested emits sub.w sp,sp,#16 in the prologue and spills (str [sp,#4], str [sp,#8]) but the epilogue is ... ; bx lr (or, post-#490, pop {r4-r8,pc}) with no add sp,#16. The spill stores also appear interleaved at the br $outer target, suggesting the frame teardown is not emitted on the taken-branch path.

#490 interaction (severity escalation, #215-class)

Before #490 the epilogue was bx lr, which returns via LR regardless of SP — so the bug was a silent SP leak (caller stack corrupted, but control returned). After #490 the epilogue is pop {r4-r8,pc}, which reads the return address from the (imbalanced) SP → pops garbage → branches to a wrong address / crashes. So #490 (a correctness fix, optimized path only — not shipped, gale uses --relocatable) turned a latent SP-imbalance into a fatal one. Classic "an epilogue change exposes a latent frame bug" (cf. #215). Root cause is this missing add sp, not #490.

Notes

• Optimized-path spill + control-flow teardown; belongs to the VCR-* allocator track (Epic: verified-codegen infrastructure (VCR-*) — replace the patch-accreting selector + allocator #242).
• A light (non-spilling) nested fixture compiles and runs correctly (validated in Optimized (non-relocatable) path miscompiles block/br_if: branch target lands mid-instruction #483's differential), so the defect is specific to the spill/frame teardown path under control flow.