[Draft] Update SMT-based ISLE verifier by avanhatt · Pull Request #13550 · bytecodealliance/wasmtime

avanhatt · 2026-06-03T19:15:57Z

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:

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.
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.
Our state modeling now handles traps and other side effects more explicitly, see the paper for details.
The specification language is more expressive, including structs and macros. See the language reference updates for details.

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

bjorn3 · 2026-06-03T19:22:46Z

Accidental commit?

Ah yes, thanks for spotting!

cfallin

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!

cfallin · 2026-06-08T21:10:04Z

    }

    fn add_binding(&mut self, id: BindingId, binding: &Binding) -> Result<()> {
+        dbg_depth!("add_binding");


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)

Oops, did not mean to include, removed!

cfallin · 2026-06-08T21:12:27Z

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)

Replace the personal mmcloughlin/aslp fork with the upstream UQ-PAC packages: aslp 0.3.2 (symbolic-opcode support, merged via PR bytecodealliance#145) plus the aslp_server_http server, which migrated to the aslp-rpc repo (v0.1.4). The server is wire-compatible, so the Rust client and parser are unchanged. setup/install-aslp.sh installs both packages into a dedicated `aslp` opam switch (OCaml >= 5.0, required by aslp_server_http's eio deps) via opam pin, replacing the fork tarball + dune build. The installers (aslp, cvc5, z3) move from veri/script/install/ to a shared setup/ dir at the subtree root, matching wasmtime's flat install-<tool>.sh convention. generate.sh and the aslp test-data script launch aslp_server_http / asli via `opam exec --switch` (overridable with ASLP_SWITCH); no PATH setup. README updated accordingly. EXTR is temporarily disabled in the alu_rrr_shift sweep: upstream 0.3.2 cannot lift it (the symbolic lsb yields an unsimplified, non-constant slice width that the RASL backend rejects), a regression vs the fork. Tracked separately.

Temporarily pin asli to mmcloughlin/aslp#extr-fix (UQ-PAC/aslp PR bytecodealliance#152), which fixes symbolic-EXTR lifting: is_pure_exp now treats bit-literals as pure, so sym_sub_int folds EXTR's slice width to a constant instead of leaving a non-constant expression the RASL check rejects. With that, isaspec can lift EXTR again, so re-enable ALUOp::Extr in the alu_rrr_shift sweep. Regenerate the AArch64 ISA specs with upstream ASLp + the fix. EXTR returns to alu_rrr_shift.isle; the rest of the churn is upstream's equivalent reformulation -- loads keep the loaded value in a constdecl (new RASL load invariant), conds use a branchless bitvector mux, SDIV drops a redundant INT_MIN/-1 special-case, and loads/stores gain `modifies` annotations. Revert the asli pin to an upstream release once PR bytecodealliance#152 merges.

Drive hyper over a tokio TcpStream instead, removing reqwest's async/TLS tree and the duplicate hyper/http/base64 versions it introduced. No new lockfile crates; regenerated specs are byte-identical.

Parse attributes with syn::meta::parser and report errors via an `expand` function returning syn::Result + into_compile_error, matching the convention in the other wasmtime proc-macros. Removes the unmaintained proc-macro-error (RUSTSEC-2024-0370) and the syn 1.0 duplicate it pulled in.

Make the ident/bits grammar rules compound-atomic so their quoted content comes through as inner pairs, and read those directly instead of stripping quotes with enquote. Regenerated specs are byte-identical.

Move pest/pest_derive (aslp) and num-bigint/num-traits/easy-smt (veri) out of the workspace root and into the single crate that uses each, keeping the shared workspace dependencies to crates with more than one consumer. Versions and lock resolution are unchanged.

Bump pest/pest_derive to 2.8.6, num-bigint to 0.4.6, and num-traits to 0.2.19 (version-floor hygiene; lock unchanged), and easy-smt 0.2 -> 0.3.2, adjusting for its ContextBuilder solver/solver_args split.

The symbolic-EXTR lift fix merged upstream (UQ-PAC/aslp#152), so asli no longer needs the fork. Pin it to the upstream merge commit (not yet in a tagged release). Regenerated specs are byte-identical.

avanhatt and others added 6 commits June 3, 2026 15:04

Changes to the veri subtree: replace entire verification engine

a0f29b7

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

New ISLE spec files

c3abc29

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

ISLE implementation changes

77235e9

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

Changes to existing ISLE backend files and related

c6a4692

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

Remaining broader changes.

c4803cb

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

Update comment

7792758

bjorn3 reviewed Jun 3, 2026

View reviewed changes

avanhatt added 3 commits June 3, 2026 15:34

Delete some output files

93a0a85

More cleanup

f743bff

Reference tweaks

79b3c95

avanhatt mentioned this pull request Jun 3, 2026

Non-draft mirror of https://github.com/bytecodealliance/wasmtime/pull/13550 wellesley-prog-sys/wasmtime#44

Open

github-actions Bot added cranelift Issues related to the Cranelift code generator cranelift:area:aarch64 Issues related to AArch64 backend. cranelift:meta Everything related to the meta-language. labels Jun 3, 2026

More cleanup

7a1f3fa

cfallin reviewed Jun 4, 2026

View reviewed changes

avanhatt added 13 commits June 4, 2026 22:13

Remove unneeded rec tag

ea0e4f6

Remove pub comments, revert more unneeded changes

ab7e63c

Merge branch 'main' into upstream-06-02

ab1276f

More veri prelude files to spec subdir

cb9f472

fmt

a020777

Update CI exclude

26972cd

Workspace deps, clippy

2959ac5

Merge branch 'main' into upstream-06-02

fe1aae8

Update github workflow

88b096c

Remove more pub comments

e7a7690

Missing docs reason

99717bf

More format

cc11047

fmt

07133ad

cfallin reviewed Jun 8, 2026

View reviewed changes

avanhatt and others added 13 commits June 8, 2026 17:52

Update threading logic, README

12da984

Merge branch 'main' into upstream-06-02

1bbeec8

Small readme tweak

7092026

Clarify ASLp fork-pin comment in install-aslp.sh

e2452ae

Drop reqwest from the ASLp client

72a565e

Drive hyper over a tokio TcpStream instead, removing reqwest's async/TLS tree and the duplicate hyper/http/base64 versions it introduced. No new lockfile crates; regenerated specs are byte-identical.

Drop enquote from the ASLp parser

e5f9f4d

Make the ident/bits grammar rules compound-atomic so their quoted content comes through as inner pairs, and read those directly instead of stripping quotes with enquote. Regenerated specs are byte-identical.

Update veri-only deps to current versions

c6dc576

Bump pest/pest_derive to 2.8.6, num-bigint to 0.4.6, and num-traits to 0.2.19 (version-floor hygiene; lock unchanged), and easy-smt 0.2 -> 0.3.2, adjusting for its ContextBuilder solver/solver_args split.

Remove veri_ir

e3668e2

Pin ASLp to upstream now that UQ-PAC/aslp#152 has landed

0465b1c

The symbolic-EXTR lift fix merged upstream (UQ-PAC/aslp#152), so asli no longer needs the fork. Pin it to the upstream merge commit (not yet in a tagged release). Regenerated specs are byte-identical.

mmcloughlin force-pushed the upstream-06-02 branch from da0f8f6 to 0465b1c Compare June 11, 2026 17:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Draft] Update SMT-based ISLE verifier#13550

[Draft] Update SMT-based ISLE verifier#13550
avanhatt wants to merge 36 commits into
bytecodealliance:mainfrom
avanhatt:upstream-06-02

avanhatt commented Jun 3, 2026

Uh oh!

bjorn3 Jun 3, 2026

Uh oh!

avanhatt Jun 3, 2026

Uh oh!

cfallin left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cfallin Jun 8, 2026

Uh oh!

avanhatt Jun 8, 2026

Uh oh!

cfallin commented Jun 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

avanhatt commented Jun 3, 2026

Uh oh!

bjorn3 Jun 3, 2026

Choose a reason for hiding this comment

Uh oh!

avanhatt Jun 3, 2026

Choose a reason for hiding this comment

Uh oh!

cfallin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cfallin Jun 8, 2026

Choose a reason for hiding this comment

Uh oh!

avanhatt Jun 8, 2026

Choose a reason for hiding this comment

Uh oh!

cfallin commented Jun 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants