[llvm] [ValueTracking] Improve knownbits from conditions where `Val` is used by `and`/`or`. (PR #86059)

[Yingwei Zheng via llvm-commits]

================
@@ -698,13 +698,26 @@ static void computeKnownBitsFromCmp(const Value *V, CmpInst::Predicate Pred,
     break;
   }
   default:
-    const APInt *Offset = nullptr;
-    if (match(LHS, m_CombineOr(m_V, m_Add(m_V, m_APInt(Offset)))) &&
-        match(RHS, m_APInt(C))) {
-      ConstantRange LHSRange = ConstantRange::makeAllowedICmpRegion(Pred, *C);
-      if (Offset)
-        LHSRange = LHSRange.sub(*Offset);
-      Known = Known.unionWith(LHSRange.toKnownBits());
+    if (match(RHS, m_APInt(C))) {
+      const APInt *Offset = nullptr;
+      if (match(LHS, m_CombineOr(m_V, m_AddLike(m_V, m_APInt(Offset))))) {
+        ConstantRange LHSRange = ConstantRange::makeAllowedICmpRegion(Pred, *C);
+        if (Offset)
+          LHSRange = LHSRange.sub(*Offset);
+        Known = Known.unionWith(LHSRange.toKnownBits());
+      }
+      // X & Y u> C -> X u> C && Y u> C
+      if ((Pred == ICmpInst::ICMP_UGT || Pred == ICmpInst::ICMP_UGE) &&
+          match(LHS, m_c_And(m_V, m_Value()))) {
+        Known.One.setHighBits(
----------------
dtcxzyw wrote:

Could you please provide the alive2 proof?


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