fix: per-function Z3 rollback, async component model, stats overflow#80
Open
fix: per-function Z3 rollback, async component model, stats overflow#80
Conversation
avrabe
force-pushed
the
fix/per-function-verification-rollback-async-stats
branch
2 times, most recently
from
223419f to
6989cd8
Compare
…sync support Per-function Z3 verification rollback: - constant_folding and optimize_advanced_instructions now revert individual functions on Z3 counterexample instead of aborting the entire pass. Pure ISLE rewrites for control-flow functions: - Functions with BrIf/BrTable are no longer skipped entirely. - New rewrite_pure() applies structural ISLE rules (constant folding, algebraic identities, strength reduction) without dataflow env tracking. - rewrite_with_dataflow() (formerly simplify_with_env) is used only for straight-line code where local/memory propagation is safe. - Backward-compatible aliases simplify() and simplify_with_env() retained. Async component model support: - Enable cm_async, cm_async_stackful, cm_async_builtins in wasmparser Validator. Components with task.return now parse correctly. Stats percentage overflow fix: - Cast to f64 before subtraction to prevent unsigned wraparound. Fixes: H-19 Trace: REQ-5, REQ-11, SC-8 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
fix/per-function-verification-rollback-async-stats
branch
from
6989cd8 to
58301c4
Compare
Resilient component pipeline: - Each core-module pass now saves state and reverts on failure or post-pass validation error instead of aborting the entire optimization. Enables partial success on async components where one pass (e.g. LICM) may produce invalid locals. Pipeline phase reordering: - Phase 1: inline_functions (unlocks cross-function optimization) - Phase 10: second eliminate_dead_code (catches LICM-produced dead code) - Phase 11: coalesce_locals (must run last — touches local indices) verify_or_revert helper: - New TranslationValidator::verify_or_revert() reverts a single function's instructions and locals on Z3 counterexample instead of propagating error and aborting the enclosing pass. Applied to all 13 passes that had translator.verify(func)? — each pass now downgrades from "fail whole module" to "skip this function". - simplify_locals catches both validate and verify failures and reverts, since its panic-prone Z3 path needs defense-in-depth. Pre-commit speedup: - cargo-test hook now runs --lib --bins only (~10x faster). - Full --all suite still runs in CI (ci.yml:71), so integration test coverage is preserved at merge-gate, not commit-gate. Trace: REQ-5, REQ-11, SC-8
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
Three fixes for real-world component optimization:
1. Per-function Z3 verification rollback (critical)
Previously, when Z3 found a counterexample for ONE function in constant_folding, the
?operator aborted the entire pass — all other functions in the module fell back to original bytes. Now, each function's instructions are saved before optimization and reverted individually on Z3 rejection, allowing other functions to still benefit from optimization.2. Async component model support
Components using WASI async (
task.return,task.wait, streams, futures) failed validation because wasmparser'sValidator::new()doesn't enable async features by default. Now usesValidator::new_with_features()withcm_async,cm_async_stackful, andcm_async_builtinsenabled. Applied to both the parser and all component optimizer validation calls.3. Stats percentage overflow
(before - after) as f64caused unsigned wraparound when output was larger than input (showing ~9829770584193684% reduction). Fixed by casting to f64 before subtraction.Test plan
cargo test --release— 403 tests passtask.return)🤖 Generated with Claude Code