[llvm] [ConstraintElim] Derive an unsigned IV bound from a signed relational latch. (PR #222762)

[Yingwei Zheng via llvm-commits]

================
@@ -1188,6 +1188,20 @@ void State::addInfoForInductions(BasicBlock &BB) {
     WorkList.push_back(FactOrCheck::getConditionFact(
         DTN, ContinuePred, PN, B, ConditionTy(ContinuePred, StartValue, B)));
 
+    // For a non-negative backedge value, 0 s<= PN s< B implies B is
+    // non-negative as well, so the same bound holds in the unsigned system.
+    if (ICmpInst::isSigned(ContinuePred)) {
+      assert((ContinuePred == CmpInst::ICMP_SLT ||
+              ContinuePred == CmpInst::ICMP_SLE) &&
+             "Expected a signed less-than continuation predicate");
+      MonotonicInfo Info = getMonotonicityInfo(*PN, Backedge);
+      if ((Info.Signed && !Info.Decreasing)) {
+        CmpInst::Predicate UPred = ICmpInst::getUnsignedPredicate(ContinuePred);
+        WorkList.push_back(FactOrCheck::getConditionFact(
----------------
dtcxzyw wrote:

So now we have:
+ S s<= Backedge s< B
+ S u< B

-> Backedge u< B https://alive2.llvm.org/ce/z/nTqDqB
-> PN u< B


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