[all-commits] [llvm/llvm-project] 80852a: [SCEV] Prove implications of different type via tr...

[max-azul via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: 80852a4f2fb154c6094bb9d9e3457757d5a60ad1
      https://github.com/llvm/llvm-project/commit/80852a4f2fb154c6094bb9d9e3457757d5a60ad1
  Author: Max Kazantsev <mkazantsev at azul.com>
  Date:   2020-10-21 (Wed, 21 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:
  -----------
  [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.

Differential Revision: https://reviews.llvm.org/D89548
Reviewed By: fhahn