Stream: git-wasmtime

Topic: wasmtime / PR #14608 ISLE: veri: error on `opt` RHS build...

view this post on Zulip Wasmtime GitHub notifications bot (Oct 07 2026 at 18:46):

avanhatt opened PR #14608 from avanhatt:veri-require-illtyped to bytecodealliance:main:

#14526 exposes an issue where an opt ISLE rule could build an Clif term with invalid type widths (in that case, irreduce to a wider width than the current width). This would cause the midend to output invalid clif that would fail the validator (or crash the backend).

The verifier did not catch this for a few different reasons:

For the most clear error messages, this PR also explicitly calls out the "ill typed width" as part of the counterexample.

Draft for now so I can check it errors in CI when #14526 is reverted.

Note this is related to also catching #14566 in the verifier step, but will not yet fix it because we do not explicitly model lanes in the type's verification model.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 07 2026 at 18:46):

avanhatt edited PR #14608:

Note: primarily a cranelift/isle/veri/spec change, with a small change to the ISLE parser for new spec form.

#14526 exposes an issue where an opt ISLE rule could build an Clif term with invalid type widths (in that case, irreduce to a wider width than the current width). This would cause the midend to output invalid clif that would fail the validator (or crash the backend).

The verifier did not catch this for a few different reasons:

For the most clear error messages, this PR also explicitly calls out the "ill typed width" as part of the counterexample.

Draft for now so I can check it errors in CI when #14526 is reverted.

Note this is related to also catching #14566 in the verifier step, but will not yet fix it because we do not explicitly model lanes in the type's verification model.

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

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

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

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

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

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

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:

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 (Oct 08 2026 at 14:06):

avanhatt updated PR #14608.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 08 2026 at 14:06):

avanhatt commented on PR #14608:

Reverting a01376f to test for CI failure

view this post on Zulip Wasmtime GitHub notifications bot (Oct 08 2026 at 14:40):

avanhatt commented on PR #14608:

CI fails as expected on the old rules. Lightly edited output:

=== veri: cranelift/isle/veri/configs/opt.args ===
=== VERIFICATION FAILURES (6) ===
FAILURE #1305   cranelift/codegen/src/opts/shifts.isle line 83  (instantiation 333) .veriisle/expansions/01305/333/failure.out
#1305   cranelift/codegen/src/opts/shifts.isle line 83  instantiation=333
ill-typed term reachable: cranelift/codegen/src/spec/inst_specs.isle line 492: e177: cannot sign extend to smaller width
model:
// ...
FAILURE #1305   cranelift/codegen/src/opts/shifts.isle line 83  (instantiation 334) .veriisle/expansions/01305/334/failure.out
#1305   cranelift/codegen/src/opts/shifts.isle line 83  instantiation=334
ill-typed term reachable: cranelift/codegen/src/spec/inst_specs.isle line 492: e177: cannot sign extend to smaller width
model:
// ...
FAILURE #1305   cranelift/codegen/src/opts/shifts.isle line 83  (instantiation 704) .veriisle/expansions/01305/704/failure.out
#1305   cranelift/codegen/src/opts/shifts.isle line 83  instantiation=704
ill-typed term reachable: cranelift/codegen/src/spec/inst_specs.isle line 492: e177: cannot sign extend to smaller width
model:
// ...
FAILURE #1309   cranelift/codegen/src/opts/shifts.isle line 87  (instantiation 333) .veriisle/expansions/01309/333/failure.out
#1309   cranelift/codegen/src/opts/shifts.isle line 87  instantiation=333
ill-typed term reachable: cranelift/codegen/src/spec/inst_specs.isle line 486: e177: cannot zero extend to smaller width
model:
// ...
FAILURE #1309   cranelift/codegen/src/opts/shifts.isle line 87  (instantiation 334) .veriisle/expansions/01309/334/failure.out
// ...
FAILURE #1309   cranelift/codegen/src/opts/shifts.isle line 87  (instantiation 704) .veriisle/expansions/01309/704/failure.out
#1309   cranelift/codegen/src/opts/shifts.isle line 87  instantiation=704
ill-typed term reachable: cranelift/codegen/src/spec/inst_specs.isle line 486: e177: cannot zero extend to smaller width
model:
// ...

view this post on Zulip Wasmtime GitHub notifications bot (Oct 08 2026 at 14:40):

avanhatt updated PR #14608.

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

avanhatt edited PR #14608:

Note: primarily a cranelift/isle/veri/spec change, with a small change to the ISLE parser for new spec form.

#14526 exposes an issue where an opt ISLE rule could build an Clif term with invalid type widths (in that case, ireduce to a wider width than the current width). This would cause the midend to output invalid clif that would fail the validator (or crash the backend).

The verifier did not catch this for a few different reasons:

For the most clear error messages, this PR also explicitly calls out the "ill typed width" as part of the counterexample.

Draft for now so I can check it errors in CI when #14526 is reverted.

Note this is related to also catching #14566 in the verifier step, but will not yet fix it because we do not explicitly model lanes in the type's verification model.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 09 2026 at 14:26):

avanhatt has marked PR #14608 as ready for review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 09 2026 at 14:26):

avanhatt requested alexcrichton for a review on PR #14608.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 09 2026 at 14:26):

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

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

alexcrichton unassigned alexcrichton from PR #14608 ISLE: veri: error on opt RHS building ill-typed clif terms.

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

alexcrichton requested cfallin for a review on PR #14608.

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

alexcrichton commented on PR #14608:

Redirecting to @cfallin as he's more familiar with this than I, but it may also be a moment as I think his queue is a bit large at this time

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

cfallin commented on PR #14608:

Working through reading/triaging my backlog now but I should be able to get to this soon!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 09 2026 at 19:13):

:thumbs_up: cfallin submitted PR review:

Seems reasonable to me -- thanks!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 09 2026 at 19:13):

cfallin added PR #14608 ISLE: veri: error on opt RHS building ill-typed clif terms to the merge queue.

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

:check: cfallin merged PR #14608.

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

cfallin removed PR #14608 ISLE: veri: error on opt RHS building ill-typed clif terms from the merge queue.

Last updated: Oct 11 2026 at 04:10 UTC