Stream: git-wasmtime

Topic: wasmtime / PR #13935 Cranelift: ISLE: Verify most of the ...

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:44):

avanhatt opened PR #13935 from avanhatt:veri-opt to bytecodealliance:main:

Use the existing (newly-updated) VeriISLE tool to verify most of the midend rules.

This includes most integer and floating point rules rooted in the simplify term, but excludes i128, SIMD, control flow, and rules rooted in simplify_skeleton. Many wide divide/multiply operations also yield unknown with shorter solver timeouts, so we also skip with the slow tag.

For floating point rules, this involves logic to relax the equality condition for non-deterministic NaNs per Wasm semantics, see comments in the README.

The midend verification can be run with:
cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes

Which verifies 4115 chained rule monomorphizations in ~2 minutes on a 12-core MacBook.

This PR also changes the instantiations for some shifts/rotates to include the cartesian product of widths, which required a change to the Rev aarch64 specs.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:44):

avanhatt requested cfallin for a review on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:44):

avanhatt requested wasmtime-compiler-reviewers for a review on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:44):

avanhatt requested fitzgen for a review on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:44):

avanhatt requested wasmtime-default-reviewers for a review on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 15:46):

avanhatt edited PR #13935:

Use the existing (newly-updated) VeriISLE tool to verify most of the midend rules.

This includes most integer and floating point rules rooted in the simplify term, but excludes i128, SIMD, control flow, and rules rooted in simplify_skeleton. Many wide divide/multiply operations also yield unknown with shorter solver timeouts, so we also skip with the slow tag.

For floating point rules, this involves logic to relax the equality condition for non-deterministic NaNs per Wasm semantics, see comments in the README.

The midend verification can be run with:
cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes

Which verifies 4115 chained rule monomorphizations in ~2 minutes on a 12-core MacBook.

This PR also changes the instantiations for some shifts/rotates to include the cartesian product of widths, which required a change to the Rev aarch64 specs. Verifying the full cartesian product is slow, so by default this verifies a narrow width, the same width, and a width with, rather than the full set.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 16:03):

avanhatt updated PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 19:04):

github-actions[bot] added the label cranelift on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 19:04):

github-actions[bot] added the label cranelift:area:aarch64 on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 19:04):

github-actions[bot] added the label cranelift:meta on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 19:04):

github-actions[bot] added the label isle on PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 22 2026 at 19:05):

github-actions[bot] commented on PR #13935:

Subscribe to Label Action

cc @cfallin, @fitzgen

<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:meta", "isle"

Thus the following users have been cc'd because of the following labels:

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

view this post on Zulip Wasmtime GitHub notifications bot (Jul 24 2026 at 22:22):

:thumbs_up: cfallin submitted PR review:

Looks great -- thanks! Once our infrastructure merges we can get this running in CI as well...

view this post on Zulip Wasmtime GitHub notifications bot (Jul 24 2026 at 22:22):

cfallin added PR #13935 Cranelift: ISLE: Verify most of the midend ISLE rules to the merge queue.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 24 2026 at 22:48):

:check: cfallin merged PR #13935.

view this post on Zulip Wasmtime GitHub notifications bot (Jul 24 2026 at 22:48):

cfallin removed PR #13935 Cranelift: ISLE: Verify most of the midend ISLE rules from the merge queue.

Last updated: Jul 29 2026 at 05:03 UTC