Skip to content

feat: complete ISLE pipeline coverage — all standard WASM instructions#53

Open
avrabe wants to merge 8 commits intomainfrom
feat/multi-memory-index-tracking
Open

feat: complete ISLE pipeline coverage — all standard WASM instructions#53
avrabe wants to merge 8 commits intomainfrom
feat/multi-memory-index-tracking

Conversation

@avrabe
Copy link
Contributor

@avrabe avrabe commented Mar 1, 2026

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:

  1. Memory index tracking (763a261): Add mem field to all load/store instructions, generalize multi-memory adapter collapse
  2. Fused optimizer relaxation (fa7f744): Allow memory stores in same-memory adapters
  3. F32/F64 constants + arithmetic (91a28c4): Wire f32.const, f64.const, and 8 float arithmetic ops (add/sub/mul/div) into ISLE
  4. F64 constant folding tests (0a4d29b): Add F64 test coverage, re-enable I64 optimization tests
  5. 32 float operations (b3a8470): 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 f64
  6. Edition 2024 (48ddc88): Upgrade to Rust edition 2024 and MSRV 1.85
  7. 30 conversion operations (85076af): Wire all trapping truncations, saturating truncations, int↔float conversions, demote/promote, and reinterpret bit-casts
  8. MemorySize/MemoryGrow + CallIndirect/BrTable (f50dd04): Wire memory ops, remove CallIndirect/BrTable from skip block, fix CallIndirect stack validation with type_signatures
  9. Bulk memory ops (056ad88): Wire MemoryFill/MemoryCopy/MemoryInit/DataDrop — eliminates skip block entirely

Skip block elimination

Before: 70+ instruction types blocked (all floats, conversions, memory ops, call_indirect, br_table, bulk memory)
After: Only Unknown opcodes blocked — all standard WASM instructions supported

Key design decisions

  • Trapping truncations only fold when value is in range (not NaN, not overflow) — preserves trap semantics
  • Saturating truncations always fold: NaN→0, overflow→clamp per WASM spec
  • Float min/max fold only when both operands are non-NaN (WASM returns NaN if either is NaN)
  • CallIndirect removed from contains_unanalyzable_instructions when module context available — type_idx provides full stack signature statically
  • BrTable still protected by has_dataflow_unsafe_control_flow for term-rewriting, but now gets DCE, branch simplification, code folding, etc.
  • Bulk memory ops treated as side effects in instructions_to_terms (consume stack values, produce no stack output)
  • Z3 verification upgraded with concrete computation for all float and conversion operations

Test plan

  • 224+ lib tests pass (including new memory, call_indirect, bulk memory tests)
  • 82 optimization tests pass
  • 32 Z3 verification tests pass
  • 5 stress tests pass (including 10K EMI iterations)
  • All real-world WASM files optimize correctly
  • Pre-commit hooks pass (fmt, clippy, test, build)

🤖 Generated with Claude Code

avrabe and others added 3 commits March 1, 2026 18:23
…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>
Copy link

@temper-pulseengine temper-pulseengine bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

  1. Memory Import Deduplication Tests (Pass 0a):

    • The deduplicate_memory_imports function 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.
  2. 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.
  3. 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.
  4. 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.
  5. Adapter Collapse Optimization:

    • The deduplicate_memory_imports function 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.
  6. Type Deduplication:

    • The deduplicate_types function 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.

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)

avrabe and others added 3 commits March 2, 2026 10:33
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>
@avrabe avrabe changed the title feat: memory index tracking + multi-memory adapter collapse feat: memory index tracking, full float/conversion ISLE pipeline, edition 2024 Mar 2, 2026
…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>
@avrabe avrabe changed the title feat: memory index tracking, full float/conversion ISLE pipeline, edition 2024 feat: full ISLE pipeline coverage — floats, conversions, memory ops, call_indirect Mar 2, 2026
- 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>
@avrabe avrabe changed the title feat: full ISLE pipeline coverage — floats, conversions, memory ops, call_indirect feat: complete ISLE pipeline coverage — all standard WASM instructions Mar 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant