[Cranelift] add simplification rules

[myunbin]

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

[github-actions]

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 .github/subscribe-to-label.json configuration file.

Learn more.

[cfallin]

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

[cfallin]

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.

[fitzgen]

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

[cfallin]

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).

[cfallin]

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