Stream: git-wasmtime

Topic: wasmtime / PR #12948 [Cranelift] add simplification rules

Wasmtime GitHub notifications bot (Apr 03 2026 at 08:28):

myunbin opened PR #12948 from myunbin:add-rules-040326 to bytecodealliance:main:

This PR adds several simplification rules:

arithmetic.isle

• (x - y) == x --> y == 0
• ;; (x + y) == y --> x == 0
• -x == -y --> x == y
• -((-y) * x) --> x * y
• ireduce(xext(a) + xext(b)) --> a + b
• ireduce(xext(a) - xext(b)) --> a - b
• max(x, y) >= x --> 1
• x >= min(x, y) --> 1

bitops.isle

• (x & ~y) == ~y --> (x | y) == -1
• x >= (x & y) --> 1 and its dual

Wasmtime GitHub notifications bot (Apr 03 2026 at 08:28):

myunbin requested cfallin for a review on PR #12948.

Wasmtime GitHub notifications bot (Apr 03 2026 at 08:28):

myunbin requested wasmtime-compiler-reviewers for a review on PR #12948.

Wasmtime GitHub notifications bot (Apr 03 2026 at 08:57):

myunbin edited PR #12948:

This PR adds several simplification rules:

arithmetic.isle

• (x - y) == x --> y == 0
• (x + y) == y --> x == 0
• -x == -y --> x == y
• -((-y) * x) --> x * y
• ireduce(xext(a) + xext(b)) --> a + b
• ireduce(xext(a) - xext(b)) --> a - b
• max(x, y) >= x --> 1
• x >= min(x, y) --> 1

bitops.isle

• (x & ~y) == ~y --> (x | y) == -1
• x >= (x & y) --> 1 and its dual

Wasmtime GitHub notifications bot (Apr 03 2026 at 11:54):

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

Wasmtime GitHub notifications bot (Apr 03 2026 at 11:54):

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

Wasmtime GitHub notifications bot (Apr 03 2026 at 11:54):

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

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 (Apr 03 2026 at 14:14):

cfallin submitted PR review:

Thanks! These all look right to me; just one comment about a potential redundancy below. Happy to merge once that's resolved.

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:14):

cfallin created PR review comment:

Isn't this rule the same as the rule two lines up, with x and y swapped? In general I like that we're doing commutativity explicitly here but I think that in this case it's actually just a redundant match -- we'll match the same patterns again with renamed bindings, so the effect is that we'll always add two iadds to the egraph (which is not what we want).

Same pattern in the rest of this rule's variants I believe.

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:26):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:26):

fitzgen created PR review comment:

I would have expected the overlap checker to find true redundancies, do you know why it isn't in this case?

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:52):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:52):

cfallin created PR review comment:

These are in the mid-end so simplify is a multi-constructor (e-graphs!) -- we disable the overlap checker completely for this case.

I guess in theory a static check might still be possible but it would have to be something like: LHSes both fire and RHSes are exactly the same, which is much harder (need to see into external ctor semantics in the general case).

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:53):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Apr 03 2026 at 14:53):

cfallin created PR review comment:

(The driver should dedup the same Value coming back twice though -- see here)

Wasmtime GitHub notifications bot (Apr 06 2026 at 01:52):

myunbin updated PR #12948.

Wasmtime GitHub notifications bot (Apr 06 2026 at 01:58):

myunbin submitted PR review.

Wasmtime GitHub notifications bot (Apr 06 2026 at 01:58):

myunbin created PR review comment:

Thanks for pointing this out. I’ve fixed the duplicated rules.

Wasmtime GitHub notifications bot (Apr 06 2026 at 05:52):

bongjunj submitted PR review.

Wasmtime GitHub notifications bot (Apr 06 2026 at 05:52):

bongjunj created PR review comment:

I think the "redundancy" is somewhat confusing to me, and I think it'd better if we can clarify here.

https://github.com/bytecodealliance/wasmtime/blob/eb4c52792fcfbf90d92805858de7e7a0c645722e/cranelift/codegen/src/opts/README.md?plain=1#L47-L83

The README says that commutative cases are better explicitly coded, not assumed by the compiler or overly generalized with other meta-rules. I see the redundant rules here are to exploit the commutativity, following the doc. Let me know if I'm missing something. Thanks!

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:31):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:31):

cfallin created PR review comment:

@bongjunj I think the issue here is that the left-hand sides are not even different commutative variants but literally the same (just alpha-renamed, i.e. with different binding spellings). With the right-hand sides the same, the effect of this is that matching with a particular x and y will produce both (iadd x y) and (iadd y x) as terms (so I was wrong above: this won't actually dedup -- and there's no reason to have both those forms produced when we don't have further information about x and y).

Said another way: what the README is describing is that we should have all commutative variants as left-hand sides explicitly in variations of a rule. But what the rules are doing here is not moving around pieces on the left-hand side, but just matching the same thing (always exactly equivalently) with different names.

I think "don't write the same left-hand side twice" is probably already implied by our rules but I'm happy to review a PR if you think it could be made more explicit!

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:34):

cfallin submitted PR review:

LGTM!

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:34):

cfallin added PR #12948 [Cranelift] add simplification rules to the merge queue.

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:59):

cfallin merged PR #12948.

Wasmtime GitHub notifications bot (Apr 06 2026 at 14:59):

cfallin removed PR #12948 [Cranelift] add simplification rules from the merge queue.

Wasmtime GitHub notifications bot (Apr 07 2026 at 06:49):

bongjunj submitted PR review.

Wasmtime GitHub notifications bot (Apr 07 2026 at 06:49):

bongjunj created PR review comment:

Ah, now I see what the rules are doing. Thanks for the detailed comment!!

Last updated: Apr 12 2026 at 23:10 UTC