[ValueTracking] Infer X u<= X +nuw Y for any Y (#75524)

Alive2: https://alive2.llvm.org/ce/z/kiGxCf
Fixes #70374.

Author: dtcxzyw

llvm/lib/Analysis/ValueTracking.cpp

@@ -8102,10 +8102,9 @@ static bool isTruePredicate(CmpInst::Predicate Pred, const Value *LHS,
   }
 
   case CmpInst::ICMP_ULE: {
-    const APInt *C;
-
-    // LHS u<= LHS +_{nuw} C   for any C
-    if (match(RHS, m_NUWAdd(m_Specific(LHS), m_APInt(C))))
+    // LHS u<= LHS +_{nuw} V for any V
+    if (match(RHS, m_c_Add(m_Specific(LHS), m_Value())) &&
+        cast<OverflowingBinaryOperator>(RHS)->hasNoUnsignedWrap())
       return true;
 
     // RHS >> V u<= RHS for any V

llvm/test/Transforms/InstSimplify/implies.ll

@@ -316,6 +316,44 @@ define i1 @test_uge_icmp(i32 %length.i, i32 %i) {
   ret i1 %res
 }
 
+; Test from PR70374
+define i1 @pr70374(i32 %x, i32 %y, i32 %z) {
+; CHECK-LABEL: @pr70374(
+; CHECK-NEXT:    [[ADD:%.*]] = add nuw i32 [[Y:%.*]], [[Z:%.*]]
+; CHECK-NEXT:    [[CMP1:%.*]] = icmp ule i32 [[ADD]], [[X:%.*]]
+; CHECK-NEXT:    ret i1 [[CMP1]]
+;
+  %add = add nuw i32 %y, %z
+  %cmp1 = icmp ule i32 %add, %x
+  %cmp2 = icmp uge i32 %x, %y
+  %res = and i1 %cmp2, %cmp1
+  ret i1 %res
+}
+
+define i1 @pr70374_commuted_add(i32 %x, i32 %y, i32 %z) {
+; CHECK-LABEL: @pr70374_commuted_add(
+; CHECK-NEXT:    [[ADD:%.*]] = add nuw i32 [[Z:%.*]], [[Y:%.*]]
+; CHECK-NEXT:    [[CMP1:%.*]] = icmp ule i32 [[ADD]], [[X:%.*]]
+; CHECK-NEXT:    ret i1 [[CMP1]]
+;
+  %add = add nuw i32 %z, %y
+  %cmp1 = icmp ule i32 %add, %x
+  %cmp2 = icmp uge i32 %x, %y
+  %res = and i1 %cmp2, %cmp1
+  ret i1 %res
+}
+
+define i1 @test_uge_icmp_value(i32 %length.i, i32 %i, i32 %j) {
+; CHECK-LABEL: @test_uge_icmp_value(
+; CHECK-NEXT:    ret i1 true
+;
+  %iplusj = add nuw i32 %i, %j
+  %var29 = icmp uge i32 %length.i, %i
+  %var30 = icmp uge i32 %length.i, %iplusj
+  %res = icmp ule i1 %var30, %var29
+  ret i1 %res
+}
+
 ; negative case, X + 1 <(s) Y !==> X <(s) Y (X = 0x7fffffff, Y = 0x7fbfffff)
 define i1 @test_sgt_icmp_no_nsw(i32 %length.i, i32 %i) {
 ; CHECK-LABEL: @test_sgt_icmp_no_nsw(