[all-commits] [llvm/llvm-project] 5ef846: Re-enable "[SCEV] Prove implications of different ...

[max-azul via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: 5ef84688fba28b9f0f69ddc9a5beb75b10696798
      https://github.com/llvm/llvm-project/commit/5ef84688fba28b9f0f69ddc9a5beb75b10696798
  Author: Max Kazantsev <mkazantsev at azul.com>
  Date:   2020-10-28 (Wed, 28 Oct 2020)

  Changed paths:
    M llvm/lib/Analysis/ScalarEvolution.cpp
    M llvm/test/Analysis/ScalarEvolution/srem.ll
    M llvm/unittests/Analysis/ScalarEvolutionTest.cpp

  Log Message:
  -----------
  Re-enable "[SCEV] Prove implications of different type via truncation"

When we need to prove implication of expressions of different type width,
the default strategy is to widen everything to wider type and prove in this
type. This does not interact well with AddRecs with negative steps and
unsigned predicates: such AddRec will likely not have a `nuw` flag, and its
`zext` to wider type will not be an AddRec. In contraty, `trunc` of an AddRec
in some cases can easily be proved to be an `AddRec` too.

This patch introduces an alternative way to handling implications of different
type widths. If we can prove that wider type values actually fit in the narrow type,
we truncate them and prove the implication in narrow type.

The return was due to revert of underlying patch that this one depends on.

Unit test temporarily disabled because the required logic in SCEV is switched
off due to compile time reasons.

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