- Notifications
You must be signed in to change notification settings - Fork1.6k
[Cranelift](n < m) → ((if c then m else x) < (if c then n else x)) …= false#12001
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to ourterms of service andprivacy statement. We’ll occasionally send you account related emails.
Already on GitHub?Sign in to your account
base:main
Are you sure you want to change the base?
Uh oh!
There was an error while loading.Please reload this page.
Conversation
Subscribe to Label ActionDetailsThis issue or pull request has been labeled: "cranelift", "isle"Thus the following users have been cc'd because of the following labels:
To subscribe or unsubscribe from this label, edit the |
fitzgen left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
Thanks again for finding another missing optimization! Comment below with a suggested way to do this a little differently.
| ;; (n < m) → ((if c then m else x) < (if c then n else x)) = false | ||
| (rule | ||
| (simplify (slt cty | ||
| (select ty c (iconst_s ty z) x) | ||
| (select ty c (iconst_s ty y) x))) | ||
| (if-let true (i64_lt y z)) | ||
| (iconst_u cty0)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
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 tycond (slt tycond a c) (slt tycond 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, sinceselects should generally be more expensive thanslts (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 justslt:
(rule (simplify (iadd ty (select _cond a b) (select _cond c d))) (select tycond (iadd tycond a c) (iadd tycond 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, ax < 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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
(although I am not sure that our cost functions encode that at the moment)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
Hi, just want to let you know it could take a while to leave my thoughts here due to my schedule. Gonna come back later soon! Thanks for your thoughtful comment.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others.Learn more.
For sure, no rush! I’m out of office visiting family for a week or so, so I will also be slow to respond
(n < m) → ((if c then m else x) < (if c then n else x)) …= false
…= false`