[all-commits] [llvm/llvm-project] f38365: [InstCombine] Add support for maximum(a, b) + minim...

serguei-katkov via All-commits all-commits at lists.llvm.org
Thu Apr 6 22:38:32 PDT 2023

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: f38365aef436d0f2ae042ad3038c8a6159dafe78
  Author: Serguei Katkov <serguei.katkov at azul.com>
  Date:   2023-04-07 (Fri, 07 Apr 2023)

  Changed paths:
    M llvm/include/llvm/IR/PatternMatch.h
    M llvm/lib/Transforms/InstCombine/InstCombineAddSub.cpp
    M llvm/lib/Transforms/InstCombine/InstCombineMulDivRem.cpp
    M llvm/test/Transforms/InstCombine/fadd-maximum-minimum.ll
    M llvm/test/Transforms/InstCombine/fmul-maximum-minimum.ll

  Log Message:
  [InstCombine] Add support for maximum(a,b) + minimum(a,b) => a + b

Unfortunately alive2 cannot prove the correctness due to fails by timeout even for
float type half.

However it should be correct. If a and b are not NaN, maximum and minimum will just
return different values (a and b) and take into account a + b == b + a this is the same.
If a or b is NaN, than maximum and minimum are equal to NaN and NaN + NaN is NaN.
a + b is also a NaN.

In terms of preserving fast flags, we cannot preserve ninf due to
minimum(NaN, Infinity) == maximum(NaN, Infinity) == NaN,
minimum(NaN, Infinity) +ninf maximum(NaN, Infinity) == NaN +ninf NaN = NaN
However transformation will change
minimum(NaN, Infinity) + maximum(NaN, Infinity) to NaN +ninf Infinity == poison.

But if fadd is marked as nnan, we can preserve because NaN +ninf/nnan NaN = poison as well.

The same optimization for
  maximum(a,b) * minimum(a,b) => a * b
is added.
All said above for fadd is correct for fmul.

Reviewed By: mkazantsev
Differential Revision: https://reviews.llvm.org/D147299

More information about the All-commits mailing list