feat: complete ISLE pipeline coverage — all standard WASM instructions#53
feat: complete ISLE pipeline coverage — all standard WASM instructions#53
Conversation
…neralize multi-memory adapter collapse Add `mem: u32` field to all 23 load/store instruction variants, propagating the memory index through the full pipeline: parser (memarg.memory), encoder (memory_index), ISLE terms, ValueData, simplify_with_env, and Z3 verification. Previously the parser discarded the memory index and the encoder hardcoded memory_index: 0, silently corrupting multi-memory modules. Now memory indices are faithfully preserved through parse → optimize → encode round-trips. Key changes: - 23 Instruction enum variants gain `mem: u32` - 9 new ISLE term variants (float loads/stores, partial-width stores) - MemoryLocation tracks memory index for redundancy elimination - Fused optimizer: remove single-memory guard, generalize same-memory adapter collapse to work with any consistent memory index N - Cross-memory adapter diagnostic counter - Z3 conservatively skips functions with mem != 0 - Coq proof: generalized_same_memory_collapse_correct theorem (17 total) - 9 new tests covering ISLE round-trip, memory redundancy, multi-memory adapter collapse, and cross-memory detection Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ion pipeline Push F32Const/F64Const onto the ISLE stack in instructions_to_terms and move F32Add/Sub/Mul/Div + F64Add/Sub/Mul/Div out of the skip block into proper handlers. This connects the existing float constant folding and simplification infrastructure (already implemented in loom-shared) to the optimization pipeline — enabling optimizations like f32.const 10.0 + f32.const 32.0 → f32.const 42.0. Also fix Z3 verification for float arithmetic: when both operands are concrete constants, compute the IEEE 754 result natively in Rust (which uses roundTiesToEven, matching WebAssembly) instead of creating opaque symbolic bitvectors that produce false counterexamples. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add end-to-end test verifying f64.const 3.0 * f64.const 7.0 folds to f64.const 21.0 through the full optimization pipeline with Z3 verification. Remove stale #[ignore] annotations from 6 I64 optimization tests. These were disabled with "I64 operations intentionally disabled in ISLE - type tracking needs I32/I64 distinction" but the type tracking issue was resolved in a prior commit. All 6 tests pass: self-xor, self-or, self-sub, self-eq, self-ne, and constant add merging for i64. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
AI Code Review for PR #53
The provided code snippet is a series of tests for various optimizations and deduplication passes in the WebAssembly binary format. These tests are part of a larger suite that verifies the correctness of the WebAssembly toolchain, specifically focusing on memory management and optimization.
Here's a breakdown of the key points from the code:
-
Memory Import Deduplication Tests (Pass 0a):
- The
deduplicate_memory_importsfunction is tested to ensure it correctly deduplicates identical memory imports. - Various scenarios are tested, including different module names, names, limits, and whether they share a local memory.
- The
-
Memory Copy Remapping:
- Functions with MemoryCopy instructions are tested to ensure that they are remapped to use the same memory index after deduplication.
- This is crucial for maintaining consistency in memory usage across functions.
-
Data Segment Remapping:
- Data segments associated with specific memory indices are checked to see if they are correctly remapped to a new index after deduplication.
- This ensures that data segments are not duplicated and are properly managed.
-
Memory Export Deduplication:
- Memory exports are tested to ensure that they are correctly updated to use the same memory index after deduplication.
- This is important for maintaining consistency in how memory is exported from WebAssembly modules.
-
Adapter Collapse Optimization:
- The
deduplicate_memory_importsfunction is also tested to see if it enables the optimization of adapter functions, which are used to manage memory allocations and deallocations. - This ensures that deduplication does not interfere with optimizations that rely on specific memory indices.
- The
-
Type Deduplication:
- The
deduplicate_typesfunction is tested to ensure it correctly removes duplicate type definitions. - This is important for maintaining a clean and efficient WebAssembly module by removing unnecessary type declarations.
- The
These tests are crucial for ensuring the reliability and performance of WebAssembly tools, particularly in scenarios where memory management and optimization are critical.
Reviewed by qwen2.5-coder:3b (local Ollama). Advisory only — may miss issues or report false positives.
Commands
| Command | Description |
|---|---|
/ask <question> |
Discuss this review — ask questions or disagree with findings |
/review-pr |
Re-run the review from scratch |
/review-pr <focus> |
Re-run with specific instructions (e.g. /review-pr focus on error handling) |
Eliminates the float skip block for unary (abs/neg/ceil/floor/trunc/ nearest/sqrt), binary (min/max/copysign), and comparison (eq/ne/lt/gt/ le/ge) operations for both f32 and f64. Functions containing these ops were previously skipped entirely from ISLE optimization — even their integer operations received no optimization. Now all float operations flow through the full pipeline: instructions_to_terms → simplify → terms_to_instructions. Key semantics: - abs/neg/copysign fold unconditionally (pure bit manipulation) - min/max/ceil/floor/trunc/nearest/sqrt fold only for non-NaN inputs - nearest uses round_ties_even() (MSRV bump 1.75→1.77) - Comparisons fold unconditionally (Rust IEEE 754 matches WASM) - Z3 verification upgraded with concrete computation for all 32 ops Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Update workspace edition from 2021 to 2024 - Bump rust-version from 1.77 to 1.85 (required by edition 2024) - Fix match ergonomics in fused_optimizer.rs (remove explicit ref mut binding modifiers now handled by default binding mode) - Replace map_or(true, ...) with is_none_or() per new clippy lint - Reformat imports across all crates per edition 2024 sorting rules Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add complete ISLE pipeline support for float/int conversions, demote/promote, reinterpret, and saturating truncation operations: - 8 trapping truncations (I32TruncF32S/U, I32TruncF64S/U, I64TruncF32S/U, I64TruncF64S/U) - 8 int-to-float conversions (F32ConvertI32S/U, F32ConvertI64S/U, F64ConvertI32S/U, F64ConvertI64S/U) - 2 float-to-float (F32DemoteF64, F64PromoteF32) - 4 reinterpret bit-casts (I32ReinterpretF32, I64ReinterpretF64, F32ReinterpretI32, F64ReinterpretI64) - 8 saturating truncations (I32TruncSatF32S/U, I32TruncSatF64S/U, I64TruncSatF32S/U, I64TruncSatF64S/U) Also removes I32WrapI64/I64ExtendI32S/I64ExtendI32U from skip block (already wired). Constant folding semantics: - Trapping trunc: only fold when in-range (NaN/overflow left unfoldable) - Saturating trunc: always fold (NaN→0, overflow→clamp) - Reinterpret: always fold (pure bit-cast via to_bits/from_bits) - Convert/demote/promote: always fold (Rust as-cast matches WASM) Z3 verification upgraded with concrete computation for all 30 operations. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ipeline - Add MemorySize/MemoryGrow ValueData variants, constructors, and simplify rules - Wire MemorySize/MemoryGrow through instructions_to_terms and terms_to_instructions - Remove MemorySize, MemoryGrow, CallIndirect, and BrTable from skip block - Fix CallIndirect stack validation: with module context, type_idx provides the full stack signature (params + table index consumed, results produced) - Add type_signatures to ValidationContext for CallIndirect validation - Update wasm_terms.isle documentation with new memory operation terms Functions containing these instructions now get full optimization (DCE, constant folding, branch simplification, etc.) instead of being skipped entirely. BrTable functions are still protected from unsafe dataflow optimization by the separate has_dataflow_unsafe_control_flow check. Skip block now only contains: MemoryFill, MemoryCopy, MemoryInit, DataDrop, Unknown. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Add MemoryFill, MemoryCopy, MemoryInit, DataDrop ValueData variants, constructors, and simplify rules (side-effectful, no constant folding) - Wire through instructions_to_terms (as side effects) and terms_to_instructions - Remove all bulk memory ops from has_unsupported_isle_instructions - Skip block now contains ONLY Unknown instructions Every standard WebAssembly instruction is now fully wired into the ISLE optimization pipeline. Functions are only skipped if they contain Unknown (unrecognized) opcodes. This means all functions in standard-compliant WASM files get full optimization coverage. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Summary
This PR achieves 100% ISLE pipeline coverage for all standard WebAssembly instructions. Every function in standard-compliant WASM files now gets full optimization — the skip block only triggers for Unknown (unrecognized) opcodes.
Changes by commit:
763a261): Addmemfield to all load/store instructions, generalize multi-memory adapter collapsefa7f744): Allow memory stores in same-memory adapters91a28c4): Wiref32.const,f64.const, and 8 float arithmetic ops (add/sub/mul/div) into ISLE0a4d29b): Add F64 test coverage, re-enable I64 optimization testsb3a8470): Wire all remaining float ops (unary, binary, comparison) — abs, neg, ceil, floor, trunc, nearest, sqrt, min, max, copysign, eq/ne/lt/gt/le/ge for both f32 and f6448ddc88): Upgrade to Rust edition 2024 and MSRV 1.8585076af): Wire all trapping truncations, saturating truncations, int↔float conversions, demote/promote, and reinterpret bit-castsf50dd04): Wire memory ops, remove CallIndirect/BrTable from skip block, fix CallIndirect stack validation with type_signatures056ad88): Wire MemoryFill/MemoryCopy/MemoryInit/DataDrop — eliminates skip block entirelySkip block elimination
Before: 70+ instruction types blocked (all floats, conversions, memory ops, call_indirect, br_table, bulk memory)
After: Only
Unknownopcodes blocked — all standard WASM instructions supportedKey design decisions
contains_unanalyzable_instructionswhen module context available — type_idx provides full stack signature staticallyhas_dataflow_unsafe_control_flowfor term-rewriting, but now gets DCE, branch simplification, code folding, etc.Test plan
🤖 Generated with Claude Code