Stream: git-wasmtime

Topic: wasmtime / PR #13998 Cranelift: VeriISLE: type check term...

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

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

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

avanhatt requested cfallin for a review on PR #13998.

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

avanhatt opened PR #13998 from avanhatt:veri-spec-type-check to bytecodealliance:main:

Type check term specs in isolation, and fix the over-constrained specs it finds.

Adds a check that type-checks verification conditions for each term used in an ISLE compilation one at a time, against nothing but its own declared types, so that a genuine type conflict is distinct from an expansion that shouldn't be reached for a specific type.

The one gnarly case is the spec for aarch64 MInst.MovFromVec: because aarch64 does not have separate Reg types for distinct sizes, it's difficult to faithfully model 128-bit-registers via our aslp automatically generated specs. Adds a special case to only spec the low 64-bits of the register and leave the top unconstrained (sound, but incomplete).

view this post on Zulip Wasmtime GitHub notifications bot (Jul 27 2026 at 20:09):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jul 27 2026 at 20:09):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jul 27 2026 at 20:09):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jul 27 2026 at 20:09):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jul 27 2026 at 20:10):

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

Subscribe to Label Action

cc @cfallin, @fitzgen

<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:area:x64", "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>

Last updated: Jul 29 2026 at 05:03 UTC