[llvm] [InstCombine] Fold max(max(x, c1) << c2, c3) —> max(x << c2, c3) when c3 >= c1 * 2 ^ c2 (PR #140526)

[Yingwei Zheng via llvm-commits]

dtcxzyw wrote:

> If we use this [Alive2 proof](https://alive2.llvm.org/ce/z/sS_Urz) then our aim "Fold max(max(x, c1) << c2, c3) —> max(x << c2, c3) when c3 >= c1 * 2 ^ c2" itself becomes false

It still holds for umin/umax. It is enough to address the motivating issue.

> Shouldn't we do the Alive2 experiment with only one x and all other constant(like [Alive2](https://alive2.llvm.org/ce/z/wR826y))?

No. We must ensure the transformation is valid for all possible inputs. In your case, both src and tgt return poison, which is always correct.
See also https://llvm.org/docs/InstCombineContributorGuide.html#use-generic-values-in-proofs


https://github.com/llvm/llvm-project/pull/140526