[Cranelift] add select simplification rules

[myunbin]

This PR adds a batch of select simplification rules.

Added rewrites:

1. (x == y) ? x : y => y
2. (x | (y != z)) ? y : z => y
3. (x == y) ? x : (x | y) => (x | y)
4. (x != y) ? (x & y) : y => (x & y)
5. (x <_u y) ? 1 : (x == y) => (x <=_u y)
6. (x < y) ? 1 : (x > y) => (x != y)
7. (x ? 1 : (x | y)) => (x ? 1 : y)
8. if x == 1 then (y - 1) else (y - x) => (y - x)
9. 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

[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 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?

[fitzgen]

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.

[myunbin]

Thanks for the thoughtful question.

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?

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