[llvm] 1fea712 - [ValueTracking] Infer `X u<= X +nuw Y` for any Y (#75524)

[via llvm-commits]

Author: Yingwei Zheng
Date: 2023-12-15T16:33:39+08:00
New Revision: 1fea712cd1898202eb051f4460b39470331aa67c

URL: https://github.com/llvm/llvm-project/commit/1fea712cd1898202eb051f4460b39470331aa67c
DIFF: https://github.com/llvm/llvm-project/commit/1fea712cd1898202eb051f4460b39470331aa67c.diff

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

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

Added: 
    

Modified: 
    llvm/lib/Analysis/ValueTracking.cpp
    llvm/test/Transforms/InstSimplify/implies.ll

Removed: 
    


################################################################################
diff  --git a/llvm/lib/Analysis/ValueTracking.cpp b/llvm/lib/Analysis/ValueTracking.cpp
index 5445746ab2a1bc..8f32a1bad98ceb 100644
--- a/llvm/lib/Analysis/ValueTracking.cpp
+++ b/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

diff  --git a/llvm/test/Transforms/InstSimplify/implies.ll b/llvm/test/Transforms/InstSimplify/implies.ll
index d72dad95bfbd09..b70dc90da655ef 100644
--- a/llvm/test/Transforms/InstSimplify/implies.ll
+++ b/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(