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

[via llvm-commits]

llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-llvm-transforms

Author: Yingwei Zheng (dtcxzyw)

<details>
<summary>Changes</summary>

Alive2: https://alive2.llvm.org/ce/z/kiGxCf
Fixes #<!-- -->70374.


---
Full diff: https://github.com/llvm/llvm-project/pull/75524.diff


2 Files Affected:

- (modified) llvm/lib/Analysis/ValueTracking.cpp (+3-4) 
- (modified) llvm/test/Transforms/InstSimplify/implies.ll (+25) 


``````````diff
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..c31f772b184fc4 100644
--- a/llvm/test/Transforms/InstSimplify/implies.ll
+++ b/llvm/test/Transforms/InstSimplify/implies.ll
@@ -316,6 +316,31 @@ 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 @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(

``````````

</details>


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