Summary
#682 correctly added the WASM mod-32 AND rm,#31 mask before register-controlled i32 shifts. But the mask is currently emitted unconditionally for the shift-amount operand — including when the amount is statically provably <32 (a constant immediate, or a value carried with a range fact). In that case the mask is dead: it can never change the result, and it costs a real instruction + cycles.
This is a beat-LLVM codegen lever: eliding a provably-dead correctness mask is exactly the proof-carrying-facts pattern (same shape as clamp-elision under a range invariant).
Measured (gale gust_mix, cortex-m3, relocatable)
Same stripped input wasm, only the synth version varies:
| synth |
.text (gust_mix) |
fn-only ticks/call (qemu -icount) |
ratio vs native LLVM |
| 0.30.1 – 0.37.0 |
68 B |
0.600 |
1.50× |
| 0.37.1 (#682) |
82 B (+14) |
0.675 (+0.075) |
1.69× |
gust_mix is clamp(1500 + (ch-1024), 1000, 2000) — its shifts are Q8 fixed-point scales with constant shift amounts (all <32). The mod-32 mask can never fire, yet 0.37.1 emits it, costing ~12 % cycles and 14 B on this function. Correctness is unaffected either way (soundness gate mix_proven ≡ mix_native ≡ gust_mix passes on both).
Ask
Elide the AND rm,#31 shift-amount mask when the amount is statically known <32:
- Constant immediate shift amount (cheapest, covers
gust_mix): if the amount is a constant literal < 32, emit the bare shift — this is the common case and a pure win.
- Range-carried amount: if the SSA value feeding the shift amount carries a
[lo,hi] fact with hi < 32 (the facts infra you already use for bounds), skip the mask.
(1) alone recovers the full 1.69×→1.50× on gale and should be safe/local. (2) generalizes it to the proof-carrying case.
Context
Filed from the gale gust perf loop (0.7× dissolved-vs-native target). This is the residual between the current re-pin (1.69×, pinned to the correctness-complete 0.37.1) and what a mask-eliding backend would ship (1.50×). Repro: benches/gust gust_codegen_bench in pulseengine/gale; COMPARE.md documents the re-pin.
Summary
#682correctly added the WASM mod-32AND rm,#31mask before register-controlled i32 shifts. But the mask is currently emitted unconditionally for the shift-amount operand — including when the amount is statically provably<32(a constant immediate, or a value carried with a range fact). In that case the mask is dead: it can never change the result, and it costs a real instruction + cycles.This is a
beat-LLVMcodegen lever: eliding a provably-dead correctness mask is exactly the proof-carrying-facts pattern (same shape as clamp-elision under a range invariant).Measured (gale
gust_mix, cortex-m3, relocatable)Same stripped input wasm, only the synth version varies:
.text(gust_mix)-icount)gust_mixisclamp(1500 + (ch-1024), 1000, 2000)— its shifts are Q8 fixed-point scales with constant shift amounts (all<32). The mod-32 mask can never fire, yet 0.37.1 emits it, costing ~12 % cycles and 14 B on this function. Correctness is unaffected either way (soundness gatemix_proven ≡ mix_native ≡ gust_mixpasses on both).Ask
Elide the
AND rm,#31shift-amount mask when the amount is statically known<32:gust_mix): if the amount is a constant literal< 32, emit the bare shift — this is the common case and a pure win.[lo,hi]fact withhi < 32(the facts infra you already use for bounds), skip the mask.(1) alone recovers the full 1.69×→1.50× on gale and should be safe/local. (2) generalizes it to the proof-carrying case.
Context
Filed from the gale gust perf loop (0.7× dissolved-vs-native target). This is the residual between the current re-pin (1.69×, pinned to the correctness-complete 0.37.1) and what a mask-eliding backend would ship (1.50×). Repro:
benches/gustgust_codegen_benchin pulseengine/gale; COMPARE.md documents the re-pin.