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

[Florian Hahn via llvm-commits]

================
@@ -1159,6 +1159,18 @@ 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)) {
+      MonotonicInfo Info = getMonotonicityInfo(*PN, Backedge);
+      if ((Info.Signed && !Info.Decreasing) ||
----------------
fhahn wrote:

Right, the `isKnownNonNegative` does not add anything with the monotonicty check currently. I had it previously and extended to use `getMonotonicityInfo`. Removed for now.

Alive2 Proof should be https://alive2.llvm.org/ce/z/G3Mv7t

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