[llvm] [InstCombine] Add combines for unsigned comparison of absolute value to constant (PR #176148)

[Antonio Frighetto via llvm-commits]

================
@@ -4288,6 +4288,40 @@ Instruction *InstCombinerImpl::foldICmpIntrinsicWithConstant(ICmpInst &Cmp,
                             II->getArgOperand(1));
     }
     break;
+  case Intrinsic::abs: {
+    if (!Cmp.getOperand(0)->hasOneUse())
+      return nullptr;
+
+    Value *X = II->getArgOperand(0);
+    APInt IntMinIsPoison =
+        dyn_cast<ConstantInt>(II->getArgOperand(1))->getValue();
+
+    // abs(X) u> K --> K >= 0 ? `X + K u> 2 * K` : `false`
+    if (Pred == CmpInst::ICMP_UGT) {
+      if (C.isNegative()) {
+        Cmp.replaceAllUsesWith(ConstantInt::getFalse(Ty));
+        return nullptr;
+      }
+
+      return new ICmpInst(ICmpInst::ICMP_UGT,
+                          Builder.CreateAdd(X, ConstantInt::get(Ty, C)),
+                          ConstantInt::get(Ty, 2 * C));
+    }
+
+    // abs(X) u< K --> K >= 1 ? `X + (K - 1) u<= 2 * (K - 1)` : K != 0
----------------
antoniofrighetto wrote:

Please split this in two lines, preconditions on first. You may want to use llvm.assume() for assuming constraints in the Alive2 proofs.

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