[all-commits] [llvm/llvm-project] a7efed: [SCEV] Improve handling of not expressions in isIm...

[Nikita Popov via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: a7efed5a20ed4f9b54df492e996f13e006175867
      https://github.com/llvm/llvm-project/commit/a7efed5a20ed4f9b54df492e996f13e006175867
  Author: Nikita Popov <nikita.ppv at gmail.com>
  Date:   2021-03-24 (Wed, 24 Mar 2021)

  Changed paths:
    M llvm/lib/Analysis/ScalarEvolution.cpp
    M llvm/test/Analysis/ScalarEvolution/zext-wrap.ll
    M llvm/unittests/Analysis/ScalarEvolutionTest.cpp

  Log Message:
  -----------
  [SCEV] Improve handling of not expressions in isImpliedCond()

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

Differential Revision: https://reviews.llvm.org/D90926