fix(#254): inline/vacuum never emit stack-invalid wasm — authoritative validate + revert#256
Merged
Merged
Conversation
inline_functions (and, on the same fixture, vacuum) kept UNCHECKED
transforms when Z3 verification was SKIPPED for functions containing
float load/store. verify_or_revert is lenient — a skipped proof was
treated as "verified" and the folded/inlined body was retained even
when it popped from an empty stack inside a nested block, so
`loom optimize` emitted structurally invalid wasm ("expected i32 but
nothing on stack"). LOOM's own stack validators are shallow (they do
not descend into block bodies) and cannot catch an intra-block
underflow.
A skipped proof must mean "don't transform", never "transform
unchecked" (REQ-5 conservative-over-fast). Each pass now consults the
authoritative WebAssembly spec validator (encode + wasmparser::validate)
on its result and reverts to a pre-pass/pre-iteration snapshot if the
module would be invalid. Worst case a pass is a no-op for that module
and the valid input round-trips unchanged; earlier proven-valid inlines
are preserved.
Reproduced with a meld-fused component core (records.wasm): before the
fix `--passes inline` produced invalid wasm (func failed to validate);
after, the full default pipeline and each pass in isolation validate.
Adds fixture issue254-records-fused.wasm and a regression test that
runs the full pipeline and asserts the output passes wasmparser::validate.
Fixes: #254
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This was referenced Jul 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #254 — critical correctness:
loom optimize(v1.1.17) emitted structurally INVALID wasm (func N failed to validate: expected i32 but nothing on stack) from valid input.Root cause
inline_functionskept the post-inline body afterverify_or_revert, which is lenient: when Z3 is skipped (function has float load/store → unmodelable), the skip was treated as "verified" and the transform kept unchecked. A skipped proof acted as transform-unchecked instead of don't-transform. loom's own stack validators are shallow (treat block bodies as opaque signatures, never descend), so they can't catch an intra-block underflow — which is why the naive stack-validator approach didn't fire.Second instance found: the
vacuumpass has the identical lenient pattern and independently produced the same invalid output on the repro (--passes ...,vacuumwas invalid even without inline). That's why the default pipeline still failed after fixing inline alone. Both are fixed.Fix
After
inline_functionsandvacuum, encode the module and run the authoritativewasmparser::validate. On rejection (or encode failure), roll back to a pre-iteration/pre-pass snapshot ofmodule.functions. Z3-independent; catches structural invalidity regardless of whether Z3 ran or was skipped. Earlier proven-valid inlines are preserved in the snapshot; worst case a pass no-ops and valid input round-trips unchanged.Verification
records.wasm): before →func 157invalid; after →wasm-tools validatePASSES (reverts fire, exit 0), still optimizes (108701→108005 B).--passes inlineand--passes vacuumisolated: both valid. Clean fixtures (repro-219/sem): optimize with no spurious reverts.test_issue254_inline_never_emits_stack_invalid_wasm+ bundled fixtureloom-core/tests/fixtures/issue254-records-fused.wasm.cargo test --release --workspace: all green (loom-core 423). fmt clean; clippy -p loom-core clean.Follow-up (separate, out of scope)
The lenient
verify_or_revert+ shallow-validator pattern is latent in other passes (constant_folding, simplify_locals, …). Worth a uniform authoritative post-pass gate — I'll file a hardening issue (aligns with the documented "positive proof vsverify().is_err()" concern, cf. #220).Suggest a v1.1.18 patch release after merge — this is a shipped miscompile-to-invalid-output affecting gale/synth today.
🤖 Generated with Claude Code
Also fixes #255 (the
vacuumtwin — same lenient-skip bug, fixed by the same gate).