Wasmtime GitHub notifications bot (Mar 09 2026 at 05:02): Wasmtime GitHub notifications bot (Mar 09 2026 at 05:02):myunbin opened PR #12742 from myunbin:select-add-030926 to bytecodealliance:main:
This PR adds a batch of select simplification rules.
Added rewrites:
(x == y) ? x : y => y(x | (y != z)) ? y : z => y(x == y) ? x : (x | y) => (x | y)(x != y) ? (x & y) : y => (x & y)(x <_u y) ? 1 : (x == y) => (x <=_u y)(x < y) ? 1 : (x > y) => (x != y)(x ? 1 : (x | y)) => (x ? 1 : y)if x == 1 then (y - 1) else (y - x) => (y - x)select(cond, eq(z, y), eq(p, y)) => eq(y, select(cond, z, p))These rewrites come from a synthesis project with @bongjunj (details: #10979 ).
I grouped these into one PR to reduce overhead from many small PRs.
If you'd prefer splitting by rule family, I'm happy to do that.cc @bongjunj
Wasmtime GitHub notifications bot (Mar 09 2026 at 05:02):myunbin requested cfallin for a review on PR #12742.
Wasmtime GitHub notifications bot (Mar 09 2026 at 05:02):myunbin requested wasmtime-compiler-reviewers for a review on PR #12742.
Wasmtime GitHub notifications bot (Mar 09 2026 at 07:03):github-actions[bot] added the label cranelift on PR #12742.
Wasmtime GitHub notifications bot (Mar 09 2026 at 07:03):github-actions[bot] added the label isle on PR #12742.
Wasmtime GitHub notifications bot (Mar 09 2026 at 07:04):github-actions[bot] commented on PR #12742:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "cranelift", "isle"Thus the following users have been cc'd because of the following labels:
- cfallin: isle
- fitzgen: 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 (Mar 09 2026 at 14:40):cfallin commented on PR #12742:
Thanks for this! Most of these seem like reasonable rewrites to add. I do wonder about the origin and use-cases for some of them, though; for example,
if x == 1 then (y - 1) else (y - x) => (y - x)
seems "oddly specific" -- it is a kind of generalization / the reverse of conditional constant propagation, but it only works for the value
1(why not the other 2^n - 1 values too?).In general we have the principle that rewrites are cheap (due to the ISLE compiler's LHS combining) and so it's fine to add a bunch of rewrite rules for corner-cases, as long as they rewrite in the correct direction. But they do carry a nonzero cost (code-size complexity, generated Rust size and Cranelift compile time, a few extra checks and branches during the mid-end pass) so it's worth ensuring that they are "actually real" in some sense.
So: did you find this LHS in a program? I see in #10979 @bongjunj describes your project as using LLVM optimizers as a source; but per my reading at least, the optimizer gives you the right-hand side but it's unclear how you're harvesting left-hand sides. Could you clarify?
Wasmtime GitHub notifications bot (Mar 09 2026 at 16:15):fitzgen commented on PR #12742:
seems "oddly specific" -- it is a kind of generalization / the reverse of conditional constant propagation, but it only works for the value
1(why not the other 2^n - 1 values too?).And to be clear, because it was left implicit above, we can express the general form of this rule in isle, and that seems like a good rule to add.
Wasmtime GitHub notifications bot (Mar 09 2026 at 16:17):fitzgen submitted PR review.
Wasmtime GitHub notifications bot (Mar 09 2026 at 16:17):fitzgen created PR review comment:
Something like this:
(rule (simplify (select ty (eq cty x (iconst_u ty n)) (isub ty y (iconst_u ty n)) (isub ty y x))) (isub ty y x))
Wasmtime GitHub notifications bot (Mar 10 2026 at 08:00):myunbin commented on PR #12742:
Thanks for the thoughtful question.
So: did you find this LHS in a program? I see in https://github.com/bytecodealliance/wasmtime/pull/10979 @bongjunj describes your project as using LLVM optimizers as a source; but per my reading at least, the optimizer gives you the right-hand side but it's unclear how you're harvesting left-hand sides. Could you clarify?
This exact LHS was not mined directly from an application program pattern. It started from an LLVM unit test, specifically this test case:
define i32 @test_sub_nsw__none_are_safe(i32 %x) { ; CHECK-LABEL: @test_sub_nsw__none_are_safe( ; CHECK-NEXT: [[SUB:%.*]] = sub i32 -2147483648, [[X:%.*]] ; CHECK-NEXT: ret i32 [[SUB]] ; %cmp = icmp eq i32 %x, 1 %sub = sub nsw i32 -2147483648, %x %sel = select i1 %cmp, i32 2147483647, i32 %sub ret i32 %sel }From such concrete LLVM test patterns, our pipeline uses an LLM to generate generalized candidates.
In this case, constants in the test (e.g., -2147483648) were abstracted into a form likeN/N - 1, which led to:def select_eqv_sub (w : Nat) := ∀ (X : BitVec w) (N : BitVec w), (if (X = 1#w) then (N - 1#w) else (N - X)) = (N - X)This generalization step is usually effective, and your point here is helpful for improving it further.
Your proposed commit looks excellent, and we’d be happy to adopt it.Thank you!
cc @bongjunj
Wasmtime GitHub notifications bot (Mar 10 2026 at 08:00):myunbin updated PR #12742.
Wasmtime GitHub notifications bot (Mar 10 2026 at 08:09):myunbin edited a comment on PR #12742:
Thanks for the thoughtful question.
So: did you find this LHS in a program? I see in https://github.com/bytecodealliance/wasmtime/pull/10979 @bongjunj describes your project as using LLVM optimizers as a source; but per my reading at least, the optimizer gives you the right-hand side but it's unclear how you're harvesting left-hand sides. Could you clarify?
This exact LHS was not mined directly from an application program pattern. It started from an LLVM unit test, specifically this test case:
define i32 @test_sub_nsw__none_are_safe(i32 %x) { ; CHECK-LABEL: @test_sub_nsw__none_are_safe( ; CHECK-NEXT: [[SUB:%.*]] = sub i32 -2147483648, [[X:%.*]] ; CHECK-NEXT: ret i32 [[SUB]] ; %cmp = icmp eq i32 %x, 1 %sub = sub nsw i32 -2147483648, %x %sel = select i1 %cmp, i32 2147483647, i32 %sub ret i32 %sel }Because this test is anchored on the fixed constant -2147483648, we summarized it to:
if x == 1 then (y - 1) else (y - x) => (y - x)Your point is very helpful, and your proposed commit looks excellent. We’d be happy to adopt it.
Thank you!
cc @bongjunj
Wasmtime GitHub notifications bot (Mar 10 2026 at 08:22):myunbin updated PR #12742.
Wasmtime GitHub notifications bot (Mar 10 2026 at 08:31):myunbin edited a comment on PR #12742:
Thanks for the thoughtful question.
So: did you find this LHS in a program? I see in https://github.com/bytecodealliance/wasmtime/pull/10979 @bongjunj describes your project as using LLVM optimizers as a source; but per my reading at least, the optimizer gives you the right-hand side but it's unclear how you're harvesting left-hand sides. Could you clarify?
This exact LHS was not mined directly from an application program pattern. It started from an LLVM unit test, specifically this test case:
define i32 @test_sub_nsw__none_are_safe(i32 %x) { ; CHECK-LABEL: @test_sub_nsw__none_are_safe( ; CHECK-NEXT: [[SUB:%.*]] = sub i32 -2147483648, [[X:%.*]] ; CHECK-NEXT: ret i32 [[SUB]] ; %cmp = icmp eq i32 %x, 1 %sub = sub nsw i32 -2147483648, %x %sel = select i1 %cmp, i32 2147483647, i32 %sub ret i32 %sel }Because this test is anchored on the fixed constant -2147483648, we summarized it to:
if x == 1 then (y - 1) else (y - x) => (y - x)Your point is very helpful, and your proposed commit looks excellent. We’d be happy to adopt it.
Additionally: I updated the latest commit to apply the generalized version you suggested.
Thank you!
cc @bongjunj
Wasmtime GitHub notifications bot (Mar 11 2026 at 14:06):cfallin submitted PR review:
Thanks!
Wasmtime GitHub notifications bot (Mar 11 2026 at 14:07):cfallin added PR #12742 [Cranelift] add select simplification rules to the merge queue.
Wasmtime GitHub notifications bot (Mar 11 2026 at 14:30):cfallin merged PR #12742.
Wasmtime GitHub notifications bot (Mar 11 2026 at 14:30):cfallin removed PR #12742 [Cranelift] add select simplification rules from the merge queue.
Last updated: Mar 23 2026 at 16:19 UTC