Stream: git-wasmtime

Topic: wasmtime / PR #13550 [Draft] Update SMT-based ISLE verifier

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

avanhatt opened PR #13550 from avanhatt:upstream-06-02 to bytecodealliance:main:

Update the core ISLE verifier for formal, SMT-based checking of instruction lowering rules. This brings the implementation up-to-date with our work described at OOPSLA 2025, rather than the prior ASPLOS 2024 implementation.

The core improvements are:

  1. Automatic rule chaining. Rather than requiring specifications on every ISLE term, terms can be marked veri chain to be automatically composed/inlined. This reduces the specification burden substantially. See the paper for details.
  2. For the aarch64 backend, most machine inst Minst specifications are automatically derived from the authoritative ARM ASL reference, with our work building on the ASLp project to derive more targeted specifications for this domain.
  3. Our state modeling now handles traps and other side effects more explicitly, see the paper for details.
  4. The specification language is more expressive, including structs and macros. See the language reference updates for details.

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

avanhatt updated PR #13550.

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

:memo: bjorn3 submitted PR review.

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

:speech_balloon: bjorn3 created PR review comment:

Accidental commit?

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

avanhatt updated PR #13550.

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

avanhatt updated PR #13550.

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

:memo: avanhatt submitted PR review.

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

:speech_balloon: avanhatt created PR review comment:

Ah yes, thanks for spotting!

view this post on Zulip Wasmtime GitHub notifications bot (Jun 03 2026 at 20:07):

avanhatt updated PR #13550.

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

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

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

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

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

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

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

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:memo: cfallin submitted PR review:

This largely looks good! I skimmed over any spec/model/attr forms in the diffs of ISLE, and the cranelift/isle/veri tree in general; reviewed more carefully the bits that were touched in Cranelift and the ISLE compiler proper. Some logistical comments but nothing really substantial. Thanks for all the work in getting this in shape for upstreaming!

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

Spurious code-motion in diff?

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

likewise here as above -- no need for doc-comments that just reproduce function names

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

Unnecessary/trivial doc comments here and below? (shift_ones being described as "Shift ones" doesn't add anything; but then we don't need doc-comments here, perhaps we can just drop)

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

For this and related prelude ISLE for the spec (e.g. fpconst.isle, inst_tags.isle, inst_spec.isle, ...) could we put it in a subdirectory, e.g. spec/?

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

Let's use workspace deps here; and I'll need to push vets before this merges to make cargo-vet happy

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

Is this a codegen change? It's not totally clear to me (I haven't traced through the emit code) but this is at least adding some new logic where we passed size through to MInst.MovToFpu directly before.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 04 2026 at 23:35):

:speech_balloon: cfallin created PR review comment:

Likewise here (and elsewhere in this diff) -- workspace deps only, to centralize our deps management and version upgrades.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 01:10):

:memo: avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 01:10):

:speech_balloon: avanhatt created PR review comment:

Ah, we added uses of cranelift_codegen::isa::aarch64::inst::... within cranelift/isle/veri, which made all of these fail deny(missing_docs).

Would we prefer I add an #![allow(missing_docs)] with a comment that we use these within cranelift/isle/veri? Or something else?

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 02:00):

:memo: avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 02:00):

:speech_balloon: avanhatt created PR review comment:

This was actually intentional, but for a niche reason.

The verifier was previously failing to type check the use of the get_exception_handler_address ISLE term. It turned out that this was the only term with both a raw block and an immediate, and that the order that gen_isle added the block, then the immediate, did not match the order of the declaration:

Builder::new("ExceptionHandlerAddress")
                .raw_block()
                .imm(&imm.imm64)
                .build(),

Because the veri code does _not_ expand external extractors and used the generated ISLE decl for this type directly (shown below), this mismatch made the rule appear to have incorrect argument order. Whereas in standard ISLE codegen, the _inlined_ extractor had the same swapped order, essentially cancelling out the mismatch.

Before, generated code on main: 

(decl get_exception_handler_address (Type Block Imm64) Inst) ;; cranelift/codegen/meta/src/gen_isle.rs:243
(extractor ;; cranelift/codegen/meta/src/gen_isle.rs:262
    (get_exception_handler_address ty block index) ;; cranelift/codegen/meta/src/gen_isle.rs:264
    (inst_data_value ty (InstructionData.ExceptionHandlerAddress (Opcode.GetExceptionHandlerAddress) index block))
)

Note the first line has block, then immediate, but the last line has immediate, then block.

It's a bit annoying because making the orders match required me to also change the arg order of the get_exception_handler_address rule in all backends, but it feels like the right move because before, all the rules used an argument order different from the generated decl.

The new generated code:

(decl get_exception_handler_address (Type Block Imm64) Inst) ;; cranelift/codegen/meta/src/gen_isle.rs:243
(extractor ;; cranelift/codegen/meta/src/gen_isle.rs:262
    (get_exception_handler_address ty block index) ;; cranelift/codegen/meta/src/gen_isle.rs:264
    (inst_data_value ty (InstructionData.ExceptionHandlerAddress (Opcode.GetExceptionHandlerAddress) block index))
)

Let me know if you prefer a different fix, though, or for me to land this change separately?

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 02:12):

:memo: avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 02:12):

:speech_balloon: avanhatt created PR review comment:

My intention was to break the recursion (the new size_for_mov_to_fpu actually should not have the rec tag, fixing) to allow chaining, but match the logic/not change codegen.

Reasoning:

That is, we didn't pass size through directly to MInst.MovToFpu directly before in exactly the same case, due to the recursive rule below this one:

(rule 1 (mov_to_fpu x (ScalarSize.Size16))
        (if-let false (use_fp16))
        (mov_to_fpu x (ScalarSize.Size32)))

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 16:55):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 16:57):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 17:06):

avanhatt updated PR #13550.

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

avanhatt updated PR #13550.

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

avanhatt updated PR #13550.

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

avanhatt updated PR #13550.

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

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 05 2026 at 20:00):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 06 2026 at 01:35):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 06 2026 at 17:22):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:57):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:57):

:speech_balloon: cfallin created PR review comment:

Ah, OK, I missed that interaction -- thanks! Resolving this thread.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:58):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:58):

:speech_balloon: cfallin created PR review comment:

Ah! OK, yeah, the pragma-allow is fine for now. I guess at some point we should come through and write proper doc comments (since these will show up in the cranelift-codegen docs now) but that can be a later-problem.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:59):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 16:59):

:speech_balloon: cfallin created PR review comment:

Ah, you actually fixed a latent bug then (in a certain manner of seeing at, at least) -- thanks and this is fine!

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:10):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:10):

:speech_balloon: cfallin created PR review comment:

Does this debug code need to stay in-tree? (It looks like it's trying to help find very deeply nested invocations? In any case I'd rather not have the ad-hoc thread-local magic here if we don't need this check permanently)

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:12):

cfallin commented on PR #13550:

Looks like things are pretty much addressed -- thanks again! One comment above; once that's addressed, as well as the current merge conflict with main, go ahead and flip this out of Draft mode (assuming it's ready and there aren't more TODOs you want to address?), and add a commit with prtest:all in the description; that'll run the full CI pipeline and we can see failures.

(One of those failures will be a cargo vet failure most likely; I can pull down the branch, do my vets locally, and push a new commit on top of your branch to address)

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:52):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:52):

:memo: avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:52):

:speech_balloon: avanhatt created PR review comment:

Oops, did not mean to include, removed!

view this post on Zulip Wasmtime GitHub notifications bot (Jun 08 2026 at 21:54):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 10 2026 at 22:39):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 10 2026 at 23:40):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 11 2026 at 14:29):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 11 2026 at 15:13):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 11 2026 at 17:12):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 11 2026 at 17:14):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 15:13):

mmcloughlin updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 16:09):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 16:10):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 16:12):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 16:14):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

avanhatt has marked PR #13550 as ready for review.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

avanhatt requested alexcrichton for a review on PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jun 12 2026 at 22:56):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jun 13 2026 at 17:20):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 13 2026 at 17:57):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 13 2026 at 18:21):

avanhatt updated PR #13550.

view this post on Zulip Wasmtime GitHub notifications bot (Jun 13 2026 at 20:08):

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

view this post on Zulip Wasmtime GitHub notifications bot (Jun 13 2026 at 20:08):

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

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>

Last updated: Jul 29 2026 at 05:03 UTC