[llvm] [InstCombine] Generalize zext(add X, -C) + C folding (PR #191723)

[via llvm-commits]

================
@@ -1005,13 +1005,21 @@ Instruction *InstCombinerImpl::foldAddWithConstant(BinaryOperator &Add) {
         Add, Builder.CreateBinaryIntrinsic(
                  Intrinsic::usub_sat, X, ConstantInt::get(Add.getType(), -*C)));
 
-  // Fold (add (zext (add X, -1)), 1) -> (zext X) if X is non-zero.
-  // TODO: There's a general form for any constant on the outer add.
-  if (C->isOne()) {
-    if (match(Op0, m_ZExt(m_Add(m_Value(X), m_AllOnes())))) {
-      const SimplifyQuery Q = SQ.getWithInstruction(&Add);
-      if (llvm::isKnownNonZero(X, Q))
-        return new ZExtInst(X, Ty);
+  // Fold (add (zext (add X, -C)), C) -> (zext X) if X u>= C.
----------------
Maiowaa wrote:

Thanks for the suggestion!

I verified the transform using Alive2.
Without the precondition X >= C (unsigned), Alive2 produces counterexamples 
(e.g., X = 0 for C = 4), showing the transformation is not valid in general.
When the precondition is enforced via llvm.assume (icmp uge), Alive2 verifies the transform:

  zext(add(X, -C)) + C --> zext(X)

as correct.

Alive2 proof:
https://alive2.llvm.org/ce/z/3OiG3K

This matches the reasoning that the subtraction must not underflow in the narrower type.

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