Page MenuHomePhabricator

[SCEV] Don't use not expressions for implied conditions
Needs ReviewPublic

Authored by nikic on Nov 6 2020, 3:16 AM.
This revision needs review, but there are no reviewers specified.



SCEV currently tries to prove implications of x pred y by also trying to imply ~y pred ~x. This is expensive in terms of compile-time (in fact, the vast majority of isImpliedCond compile-time is spent here) and generally not fruitful. The issue is that this also swaps the operands and thus breaks canonical ordering. If originally we were trying to prove an implication like X > C1 => Y > C2, then we'll now try to prove X > C1 => C3 > ~Y, which will not work.

The only real case where we can get some use out of this transform is if the original conditions were in the form X > C1 => Y < C2, were then swapped to X > C1 => C2 > Y and are then swapped again here to X > C1 => ~Y > C3.

As such, handle this at a higher level, where we are doing the swapping in the first place. There's four different ways that we can line up a predicate and a swapped predicate, so we use some heuristics to pick some profitable way.

Because we now try this transform at a higher level (isImpliedCondOperands rather than isImpliedCondOperandsHelper), we can also prove additional facts. Of the added tests, one was proven previously while the other wasn't.


Diff Detail

Event Timeline

nikic created this revision.Nov 6 2020, 3:16 AM
nikic requested review of this revision.Nov 6 2020, 3:16 AM
nikic added inline comments.Nov 6 2020, 3:19 AM

This is a SCEV nowrap caching artifact -- the cached nowrap flags depend on which expressions get constructed. There's no actual change in which implied conditions here. I've put up D90338 as an experiment to improve handling of addrec nowrap flags.

lebedev.ri added inline comments.

What happens if the predicate is swapped instead of operands?

nikic updated this revision to Diff 303489.Nov 6 2020, 9:56 AM
nikic edited the summary of this revision. (Show Details)

Preserve transform at a higher level, where we are lining up swapped predicates.

nikic added inline comments.Nov 6 2020, 10:00 AM

It's not possible to swap the predicate at this point, because this code already works on a single matching predicate only.

However, I think your general idea here is right. I've updated the patch to preserve this transform, but at a higher level: When we try to line up a predicate and a swapped predicate, using this approach allows us to do a "double swap" and thus avoid changing operand order. That allows us to preserve canonical operand ordering, and thus prove useful facts.

Because this is done at a higher level, we'll also try to apply more types of reasoning to the not-ed version.