wasmtime / PR #14964 ISLE verifier: reject rules whose RH... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / PR #14964 ISLE verifier: reject rules whose RH...

Wasmtime GitHub notifications bot (Oct 23 2026 at 16:34):

yagehu opened PR #14964 from yagehu:veri-rhs-type-soundness to bytecodealliance:main:

Bug

#14957 reported an unsound ISLE rule passing the VeriISLE verifier. This is my take on why it passes currently and my attempt to fix it.

In the given example, cty is the result type of both sextends, but nothing bounds x and y to the same width. The verifier currently reports skipped type assignments (102 in the example) and verifies the 6 where x, y, and ty happen to have the same width. So a rule like
(ireduce ty (iadd cty (sextend cty x) (sextend cty y))) => (iadd ty x y)
was accepted even though x and y may differ in width.

This Fix

A rule fires whenever its left-hand side matches, so its right-hand side must be well-typed under every type assignment the left-hand side accepts. If it isn't, then the rule should be rejected.

This commit changes the verifier so that:

We mark which parts of the rule come from LHS or RHS.

Solve LHS types first, then check RHS under each satisfying assigment.

Report the RHS conflict as error.

Caveat

This addition type check step needs the solver, so --skip-solver would still skip these conflicts.

Wasmtime GitHub notifications bot (Oct 23 2026 at 16:34):

yagehu requested fitzgen for a review on PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 16:34):

yagehu requested wasmtime-compiler-reviewers for a review on PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 16:34):

yagehu removed the review request for wasmtime-compiler-reviewers from PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 18:50):

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

Wasmtime GitHub notifications bot (Oct 23 2026 at 18:50):

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

Wasmtime GitHub notifications bot (Oct 23 2026 at 18:51):

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

Subscribe to Label Action

cc @avanhatt, @cfallin, @fitzgen, @mmcloughlin

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

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

avanhatt: isle

cfallin: isle

fitzgen: isle

mmcloughlin: isle

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

Learn more.
</details>

Wasmtime GitHub notifications bot (Oct 23 2026 at 18:57):

yagehu updated PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 19:03):

yagehu edited PR #14964:

Bug

#14957 reported an unsound ISLE rule passing the VeriISLE verifier. This is my take on why it passes currently and my attempt to fix it.

In the given example, cty is the result type of both sextends, but nothing bounds x and y to the same width. The verifier currently reports skipped type assignments (102 in the example) and verifies the 6 where x, y, and ty happen to have the same width. So a rule like
(ireduce ty (iadd cty (sextend cty x) (sextend cty y))) => (iadd ty x y)
was accepted even though x and y may differ in width.

This Fix

A rule fires whenever its left-hand side matches, so its right-hand side must be well-typed under every type assignment the left-hand side accepts. If it isn't, then the rule should be rejected.

This commit changes the verifier so that:

We mark which parts of the rule come from LHS or RHS.

Solve LHS types first, then check RHS under each satisfying assigment.

Report the RHS conflict as error. But don't report assignments that can never occur due to a guard like (value_type ty).

Lowering rule fixes

With the help of an LLM I made some fixes to the new lowering verification errors on aarch64.

writable_zero_reg was a fixed 32-bit zero but is used as a 64-bit destination. It is now width-polymorphic.

writable_reg_to_reg required equal widths, but scalar float helpers allocate 128-bit vector temporaries and return them as 64-bit Regs. It now keeps the low bits.

FixedToFP! narrowed its operand to the destination float width before converting, so fcvt_from_{u,s}int.f32 of an i64 only converted the low 32 bits. It now converts at full width, as the CLIF spec already does.

trap_if_div_overflow emits flag-setting and flag-consuming instructions without threading the flags, which the specs don't model.

Caveat

This addition type check step needs the solver, so --skip-solver would still skip these conflicts.

Wasmtime GitHub notifications bot (Oct 23 2026 at 19:34):

cfallin commented on PR #14964:

cc @avanhatt @mmcloughlin

Wasmtime GitHub notifications bot (Oct 23 2026 at 21:44):

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

Wasmtime GitHub notifications bot (Oct 23 2026 at 21:46):

fitzgen requested cfallin for a review on PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 21:46):

fitzgen removed the review request for fitzgen from PR #14964.

Wasmtime GitHub notifications bot (Oct 23 2026 at 23:32):

avanhatt commented on PR #14964:

Thanks for the PR!

I'll take a deeper look over the next few days (probably Monday), but some initial thoughts:

I think the issue uncovered here may also warrant a deeper fix where we rule out inapplicable chains at the expansion level to avoid similar gaps from inapplicability in the future.

I'd feel better about resolving the trap_if_div_overflow spec issues in the same PR rather than changing it as TODO based on it being core integer arithmetic we want covered.

The arithmetic-precise.clif/related rules change should possibly live in a separate PR, since it actually changes/improves the optimizer output.

Wasmtime GitHub notifications bot (Oct 24 2026 at 14:50):

yagehu commented on PR #14964:

Thanks for the PR!

I'll take a deeper look over the next few days (probably Monday), but some initial thoughts:
* I think the issue uncovered here may also warrant a deeper fix where we rule out inapplicable chains at the `expansion` level to avoid similar gaps from inapplicability in the future.

* I'd feel better about resolving the `trap_if_div_overflow` spec issues in the same PR rather than changing it as `TODO` based on it being core integer arithmetic we want covered.

* The arithmetic-precise.clif/related rules change should possibly live in a separate PR, since it actually changes/improves the optimizer output.
Totally makes sense. I can address points 2 and 3. Let me know what's a better deeper fix after you've thought about it.

Wasmtime GitHub notifications bot (Oct 24 2026 at 20:07):

yagehu updated PR #14964.

Wasmtime GitHub notifications bot (Oct 24 2026 at 20:16):

yagehu updated PR #14964.

Wasmtime GitHub notifications bot (Oct 24 2026 at 20:26):

yagehu edited PR #14964:

Bug

#14957 reported an unsound ISLE rule passing the VeriISLE verifier. This is my take on why it passes currently and my attempt to fix it.

In the given example, cty is the result type of both sextends, but nothing bounds x and y to the same width. The verifier currently reports skipped type assignments (102 in the example) and verifies the 6 where x, y, and ty happen to have the same width. So a rule like
(ireduce ty (iadd cty (sextend cty x) (sextend cty y))) => (iadd ty x y)
was accepted even though x and y may differ in width.

This Fix

A rule fires whenever its left-hand side matches, so its right-hand side must be well-typed under every type assignment the left-hand side accepts. If it isn't, then the rule should be rejected.

This PR changes the verifier so that:

We mark which parts of the rule come from LHS or RHS.

Solve LHS types first, then check RHS under each satisfying assigment.

Report the RHS conflict as error. But don't report assignments that can never occur due to a guard like (value_type ty).

What the new check found

Making these conflicts visible exposed rules that previously verified vacuously, because every type assignment was silently dropped. For example, the sdiv_base_base_64 rule uses (writable_zero_reg) as a 64-bit destination register. But its spec was a fixed 32-bit value:
(spec (writable_zero_reg) (provide (= result #x00000000)))
All the type assignments conflicted and were dropped. In this case the problem was the spec, but treating "no type assignment works" as "this rule doesn't apply" also hid this problem.

Mid end (opt)

The x > max(x, y) --> 0 rules in arithmetic.isle reuse one ty for a comparison's result type and for its operands. When matched, the type of an icmp is its result type (i8), so these rules only fire for i8 operands. The verifier also can't relate that ty to the comparison's width. I've tagged them TODO here. Switching them to a separate comparison type changes optimizer output, so it will be a separate PR.

aarch64 lowering

With the help of an LLM I made some fixes to the new lowering verification errors on aarch64.

writable_zero_reg was a fixed 32-bit zero but is used as a 64-bit destination. It is now polymorphic.

writable_reg_to_reg required equal widths, but scalar float helpers allocate 128-bit vector temporaries and return them as 64-bit Regs. It now keeps the low bits.

FixedToFP! narrowed its operand to the destination float width before converting, so fcvt_from_{u,s}int.f32 of an i64 only converted the low 32 bits. It now converts at full width, as the CLIF spec already does.

Load and store addresses are scalars, but their specs left the lane count open, so the verifier could pick a vector address. The specs now say it's a scalar.

trap_if_div_overflow emits flag-setting and flag-consuming instructions without threading the flags, which the specs don't model.

Enabling with_flags

Verifying sdiv overflow check needs with_flag, which was tagged TODO. Removing it brings flag-using lowering rules into scope, and some of them fail or have no spec. I've excluded the specific cases as TODO. I think this is OK because they were all excluded before, just implicitly.

Caveat

This addition type check step needs the solver, so --skip-solver would still skip these conflicts.

Wasmtime GitHub notifications bot (Oct 24 2026 at 20:27):

yagehu commented on PR #14964:

I've updated the PR to drop the arithmetic-precise.clif related rules because they change optimizer behavior. I've also addressed the trap_if_div_overflow spec issue. PR description updated to reflect the changes.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:repeat: avanhatt submitted PR review:

Thanks again for the PR! The general approach makes sense (while the rhs boolean tracking logic as is seems a bit fragile, I don't see another obvious approach without a larger redesign of type inference).

My thought about avoiding Inapplicable altogether didn't actually pan out, since some actual inapplicable rule chains require the solver to rule out rather than just information available at expansion time.

More comments inline, including some requests for changes.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

The implicit rhs = false logic is a bit easy to miss, would prefer this to be a parameter or otherwise set more explicitly.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

For clarity/symmetry, would prefer this be lhs_width_domains on the System.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

I would add here that we need the solver to determine the satisfiability of value constraints.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

I think we should actually revert this back to just be (provide true) since it is just a write sink as it was in the paper version (this was a mistake I introduced when upstreaming).

As is, it seems this verifies the relevant sdiv rule below without modeling all cases (e.g., it forces y = -1): if you break the rule to trap on cases it should not trap on, it still passes.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

Ah, I was missing that these failed as written under the new design. If you would rather the previous change that allows them to pass in this PR, I now think it's related enough to make sense. Sorry for the churn!

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

These below should be resolvable with spec fixes, but I can resolve that in a followup PR.

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

Likewise for lhs_constraints there

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

This should also now call resolve_single_lane_maps() (or maybe should have a shared prelude with Solver encode ).

Wasmtime GitHub notifications bot (Oct 26 2026 at 23:18):

:speech_balloon: avanhatt created PR review comment:

It's not clear to me why this (or the corresponding_scalars helper) is necessary. signatures/specs are assumed to be correct, so I don't see the case where self.signature_type(&call.ret, sig.ret.clone()); below is insufficient. Could you explain what case you think this is necessary for?