Conversation
This was referenced May 2, 2026
The v0.4.0 has_dataflow_unsafe_control_flow guard only flagged
BrIf/BrTable. The gale v0.4.0 measurement (PR-A) found CSE produced
an unsound store-hoist on gale_sem_count_take where the function
uses `if (eqz) return; end` — an If with Return inside, which
slipped through the guard.
Root-cause investigation (per-pass tracing on the gale-style input)
showed the reordering happens in constant_folding's
instructions_to_terms / terms_to_instructions round-trip, not in
CSE. The terms IR doesn't preserve early-exit ordering: once a
function with an `If { then_body: [..., Return] }` is converted
to terms and back, the if-block can land at the function tail
with the straight-line code (load/sub/store) hoisted to the
function head — so the store now runs unconditionally.
Fix:
- Extend has_dataflow_unsafe_control_flow to flag any nested
Return/Br as an early-exit pattern. New helper has_unsafe_in_nested
recurses into Block/Loop/If bodies. Top-level Return/Br at the
very last position is allowed (function terminator).
- constant_folding and optimize_advanced_instructions now skip
the function entirely when has_dataflow_unsafe_control_flow is
true (previously they fell back to rewrite_pure, which still
went through the round-trip and reordered).
- Same guard added to simplify_locals, code_folding, LICM,
remove_unused_branches, optimize_added_constants, coalesce_locals,
and both CSE entry points — defense in depth across the rest
of optimize_module's pipeline.
- DCE intentionally NOT guarded — it only deletes unreachable code
after terminators, never reorders, and Return-at-tail is the
primary reason DCE exists. Guarding it would defeat the pass.
- Remove the dead use_dataflow_env branch from constant_folding /
optimize_advanced_instructions; the unsafe path is gone, the
safe path always uses the dataflow env.
Regression test:
- test_early_return_guard_prevents_store_hoist mirrors
gale_sem_count_take and asserts I32Eqz appears before I32Store
in the optimized output. Without this PR, the store ends up at
index 5 and the eqz at 7 (i.e., store hoisted above guard);
with this PR, the original order is preserved exactly.
- The existing test_default_then_override_across_br_table_preserved
also still passes — both regressions covered.
Trace: REQ-1, REQ-3, REQ-5, H-9
avrabe
force-pushed
the
release/v0.5.0-pr-b-hoist-guard-return-br
branch
from
06b20a8 to
70756b2
Compare
avrabe
added a commit
that referenced
this pull request
May 2, 2026
Bump workspace version 0.4.0 → 0.5.0 and add CHANGELOG section. This release ships the v0.5.0 audit follow-ups across five PRs: - #88 PR-A: VerificationResult strict-mode helpers (is_skip, skip_reason, verify_or_revert_strict) + gale v0.4.0 measurement report documenting the CSE soundness bug on production kernel-scheduler code. - #89 PR-B: Close hoist hole on early-exit (Return/Br) patterns. Per-pass tracing showed reordering happens in constant_folding's terms-IR roundtrip; the function ends up with the if-guard moved to the function tail and the load/store sequence hoisted to the function head. Fix: extend has_dataflow_unsafe_control_flow to flag nested Return/Br; constant_folding and optimize_advanced_instructions skip such functions entirely. Defense-in-depth guards on simplify_locals, remove_unused_branches, optimize_added_constants. Regression test pinned. - #90 PR-C: 8 minimal post-MVP wasm fixtures + spec_features.rs test harness. Pins the "parser must never panic" contract for SIMD, ref types, bulk memory, tail calls, exception handling, multi-memory, sign-extension, saturating-trunc. - #91 PR-D: FusedOptimization.v wired into BUILD.bazel. Closes audit D1; the 7 axioms remain (discharge is future work). - #92 chore: top-level concurrency: block on every workflow. Closes the org-wide CI queue backlog; superseded PR runs now cancelled in ~30s, runs on main / tags / releases / scheduled events never cancelled. CHANGELOG.md adds a v0.5.0 section documenting all of the above plus the deferred work for the next release. Trace: REQ-1, REQ-3, REQ-5, REQ-7, REQ-9, REQ-12, REQ-14
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.
Summary
Fixes the CSE soundness bug discovered on
gale_sem_count_take(documented in PR-A's gale measurement report). The v0.4.0 hoist guard only flaggedBrIf/BrTable; functions usingif (cond) return; end(the canonical Rust early-exit guard) slipped through.Root cause
Per-pass tracing on a gale-style fixture showed the reordering happens in
constant_folding, not in CSE as initially suspected. Theinstructions_to_terms→ rewrite →terms_to_instructionsround-trip does not preserve order across early-exit patterns: a function withIf { then_body: [..., Return] }followed by straight-line code emerges with the if-block moved to the function tail and the straight-line code (load/sub/store) hoisted to the function head — so the store runs unconditionally, including when the guard would have returned early.Fix
has_dataflow_unsafe_control_flowto flag any nestedReturn/Bras an early-exit pattern. New helperhas_unsafe_in_nestedrecurses into Block/Loop/If bodies. Top-level Return/Br at the very last position is allowed (function terminator).constant_foldingandoptimize_advanced_instructionsnow skip the function entirely whenhas_dataflow_unsafe_control_flowis true. Previously they fell back torewrite_pure, which still went through the unsound round-trip.simplify_locals,remove_unused_branches,optimize_added_constants(others were already guarded in v0.4.0).eliminate_dead_codeintentionally NOT guarded — it only deletes code after terminators, never reorders. Guarding it would defeat the pass.use_dataflow_envbranch removed; the unsafe path is gone, the safe path always uses the dataflow env.Regression tests
test_early_return_guard_prevents_store_hoist— mirrorsgale_sem_count_take, assertsI32Eqzappears beforeI32Storein optimized output. Without this PR: store at index 5, eqz at 7 (hoisted above guard). With this PR: original order preserved.test_default_then_override_across_br_table_preserved(from v0.4.0 PR-C) still passes.Test plan
v0.5.0 release sequence
🤖 Generated with Claude Code