Stream: git-wasmtime

Topic: wasmtime / PR #14269 ISLE: Veri: include counterexample i...

Wasmtime GitHub notifications bot (Sep 02 2026 at 18:13):

avanhatt opened PR #14269 from avanhatt:counterexample to bytecodealliance:main:

Include counterexamples when verification fails in the CI log (capped at 25 total).

Draft for now because this includes an intentional failure to test the logic.

Wasmtime GitHub notifications bot (Sep 02 2026 at 18:56):

avanhatt updated PR #14269.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:22):

avanhatt updated PR #14269.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

avanhatt has marked PR #14269 as ready for review.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

avanhatt requested cfallin for a review on PR #14269.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

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

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

avanhatt requested wasmtime-core-reviewers for a review on PR #14269.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

avanhatt requested alexcrichton for a review on PR #14269.

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:27):

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

Wasmtime GitHub notifications bot (Sep 02 2026 at 19:28):

avanhatt edited PR #14269:

Include counterexamples when verification fails in the CI log (capped at 25 total).

For example, failure log now includes:

==========================
Cache mode:         ReadWrite
Cache source:       cranelift/isle/veri/cache
Cache destination:  cranelift/isle/veri/cache.rebuild
=== VERIFICATION FAILURES (4) ===
FAILURE #4  cranelift/codegen/src/opts/arithmetic.isle line 23  (instantiation 0)   .veriisle/expansions/00004/000/failure.out
#4  cranelift/codegen/src/opts/arithmetic.isle line 23  instantiation=0
model:
state: relax_nan = false
state: clif_trap = false
state: clif_load = {active: false, size_bits: 0, addr: #x0000000000000000}
state: clif_store = {active: false, size_bits: 1, addr: #x0000000000000000, value: #x0000000000000000}
state: loaded_value = #x0000000000000000
iadd({bits: 8}, #x40, #xdf) -> #x1f
ineg({bits: 8}, #x21) -> #xdf
isub({bits: 8}, #x21, #x40) -> #xe1
simplify(#x1f) -> #xe1

Wasmtime GitHub notifications bot (Sep 02 2026 at 20:44):

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

Wasmtime GitHub notifications bot (Sep 02 2026 at 20:44):

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

Wasmtime GitHub notifications bot (Sep 02 2026 at 21:44):

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

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 (Sep 03 2026 at 15:30):

:thumbs_up: cfallin submitted PR review:

Thanks! Looks like a submodule change to tests/component-model got caught in the diff too (git submodule update before committing, I often forget too...) -- happy to merge once that's fixed!

Wasmtime GitHub notifications bot (Sep 04 2026 at 20:40):

avanhatt updated PR #14269.

Wasmtime GitHub notifications bot (Sep 05 2026 at 04:06):

alexcrichton added PR #14269 ISLE: Veri: include counterexample in CI log for failures to the merge queue.

Wasmtime GitHub notifications bot (Sep 05 2026 at 04:32):

:check: alexcrichton merged PR #14269.

Wasmtime GitHub notifications bot (Sep 05 2026 at 04:32):

alexcrichton removed PR #14269 ISLE: Veri: include counterexample in CI log for failures from the merge queue.

Last updated: Sep 20 2026 at 18:08 UTC