[Cranelift] `(n < m) → ((if c then m else x) < (if c then n else x)) …

[bongjunj]

…= false`

[github-actions]

Subscribe to Label Action

cc @cfallin, @fitzgen

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.

[fitzgen]

Thanks again for finding another missing optimization! Comment below with a suggested way to do this a little differently.

[fitzgen]

It might make sense to add a general rule to dedupe selects, something like this:

(rule (simplify (slt ty (select _ cond a b)
                        (select _ cond c d)))
      (select ty cond (slt ty cond a c)
                      (slt ty cond b d)))

I think this could be an intermediate step that would reveal optimization possibilities for existing small rules and effectively subsume this larger rule. I think this is also beneficial on its own, since selects should generally be more expensive than slts (although I am not sure that our cost functions encode that at the moment), so I'm not worried about unnecessarily blowing up the enode count in this case.

All that said, we would really want the equivalent of this rule for ~all operators, not just slt:

(rule (simplify (iadd ty (select _ cond a b)
                         (select _ cond c d)))
      (select ty cond (iadd ty cond a c)
                      (iadd ty cond b d)))

And all those rules would be annoying to write in ISLE today without macros or higher-order terms.

But then again, roughly the same could be said about this rule as-is (it is combining a cprop rule, a x < x ==> false rule, and the pull-selects-out rule I sketched above; we could do the same kind of thing for all other operators' rules by combining them with their own version of the pull-selects-out rule).

So after writing all this out, I think I have convinced myself that my proposed intermediate rule is the way to go, rather than writing out the "combined" rule as you have here. (And we don't need to add all the other operator variants of that rule now, but probably should eventually.) But we should check that adding that rule really is enough to do the "combined" rewrite you've proposed in this PR. We should be able to check that via your existing tests.

Does all that make sense?

[fitzgen]

(although I am not sure that our cost functions encode that at the moment)

#12006