[SCEV] Prove condition invariance via context

[mkazantsev]

Summary

Contextual knowledge may be used to prove invariance of some conditions.
For example, in this case:

; %len >= 0
guard(%iv = {start,+,1}<nuw> <s %len)
guard(%iv = {start,+,1}<nuw> <u %len)

the 2nd check always fails if start is negative and always passes otherwise.

It looks like there is more opportunities of this kind that are still to be implemented.

[mkazantsev]

Ping

[mkazantsev]

Rebased. Suprisingly, one of tests pessimized flags after it did a nice transform, but it means we are lacking another piece of logic somewhere else. The flags have been added just recently, and we might need some extra work to make it more robust.

[mkazantsev]

Ping

[apilipenko]

llvm/lib/Analysis/ScalarEvolution.cpp

10816–10817

we know that ArLHS does not cross zero

Where do you get this fact from?

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

10816–10817

"Does not cross zero" is "hasNoUnsignedWrap", we got it from

auto MonotonicType = getMonotonicPredicateType(ArLHS, Pred);

and assert just here.

[apilipenko]

llvm/lib/Analysis/ScalarEvolution.cpp

10815–10829

Suggested slight rewording of the reasoning and restructuring of the code.

10824

Why don't you use Start(ArLHS) >=s 0 as the resulting invariant condition?

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

10824

Imagine RHS = 100. LHS <u 100 will allow us to infer more facts from it than LHS >=s 0.

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

10815–10829

Makes sense.

[apilipenko]

llvm/lib/Analysis/ScalarEvolution.cpp

10824

Maybe add a comment about it as well?

[uabelho]

Hello,

I think I'm seeing a miscompile with this patch.
Reproduce with:

opt --passes="indvars" bbi-72689.ll -S -o -

indvars does

<   %cmp22.not.i = icmp ult i32 %storemerge13.i, 2
---
>   %cmp22.not.i = icmp ult i32 0, 2

which I think is incorrect.
We have

[...]
%storemerge13.i = phi i32 [ 0, %entry ], [ %dec.i, %for.inc32.i ]
%cmp22.not.i = icmp ult i32 %storemerge13.i, 2
[...]
%dec.i = add i32 %storemerge13.i, -1
[...]

so we start at 0, then add -1 so we get -1, and then do an ult compare between -1 (0xffffffff) and 2, which I suppose should be false?
But indvars changes the compare to icmp ult i32 0, 2 which is always true?

The end result is that the function loops forever instead of returning -1.

bbi-72689.ll990 BDownload

[mkazantsev]

@uabelho thanks for your report. Let me take a look if it's causing the problem or exposing an existing one.

[mkazantsev]

This comment was removed by mkazantsev.

[mkazantsev]

This is what the transform sees:

ArLHS = {0,+,-1}<nuw><nsw><%for.body.i>, RHS = 2

nuw here looks like a bug to me. So this patch has exposed something else. I'll dig into it.

If it was nuw indeed, the transform would be correct.

[mkazantsev]

Filed a https://github.com/llvm/llvm-project/issues/57247, not obvious to me that the bug is caused by my patch. Further details will go there.

[uabelho]

In D129753#3734817, @mkazantsev wrote:

Filed a https://github.com/llvm/llvm-project/issues/57247, not obvious to me that the bug is caused by my patch. Further details will go there.

Ok, thanks!

llvm/include/llvm/Analysis/ScalarEvolution.h

LoopInvariantPredicate(ICmpInst::Predicate Pred, const SCEV *LHS,
                            const SCEV *RHS)
         : Pred(Pred), LHS(LHS), RHS(RHS) {}
   };
   /// If the result of the predicate LHS `Pred` RHS is loop invariant with
   /// respect to L, return a LoopInvariantPredicate with LHS and RHS being
   /// invariants, available at L's entry. Otherwise, return None.
   Optional<LoopInvariantPredicate>
   getLoopInvariantPredicate(ICmpInst::Predicate Pred, const SCEV *LHS,
-                            const SCEV *RHS, const Loop *L);
+                            const SCEV *RHS, const Loop *L,
+                            const Instruction *CtxI = nullptr);
 
   /// If the result of the predicate LHS `Pred` RHS is loop invariant with
   /// respect to L at given Context during at least first MaxIter iterations,
   /// return a LoopInvariantPredicate with LHS and RHS being invariants,
   /// available at L's entry. Otherwise, return None. The predicate should be
   /// the loop's exit condition.
   Optional<LoopInvariantPredicate>
   getLoopInvariantExitCondDuringFirstIterations(ICmpInst::Predicate Pred,

llvm/lib/Analysis/ScalarEvolution.cpp

if (ICmpInst::isUnsigned(Pred)) {
 
     return None;
   }
 }
 
 Optional<ScalarEvolution::LoopInvariantPredicate>
 ScalarEvolution::getLoopInvariantPredicate(ICmpInst::Predicate Pred,
                                            const SCEV *LHS, const SCEV *RHS,
-                                           const Loop *L) {
-
+                                           const Loop *L,
+                                           const Instruction *CtxI) {
   // If there is a loop-invariant, force it into the RHS, otherwise bail out.
   if (!isLoopInvariant(RHS, L)) {
     if (!isLoopInvariant(LHS, L))
       return None;
 
     std::swap(LHS, RHS);
     Pred = ICmpInst::getSwappedPredicate(Pred);
   }
ScalarEvolution::getLoopInvariantPredicate(ICmpInst::Predicate Pred,
   // predicate with its value on the first iteration of the loop (which is
   // loop invariant).
   //
   // A similar reasoning applies for a monotonically decreasing predicate, by
   // replacing true with false and false with true in the above two bullets.
   bool Increasing = *MonotonicType == ScalarEvolution::MonotonicallyIncreasing;
   auto P = Increasing ? Pred : ICmpInst::getInversePredicate(Pred);
 
-  if (!isLoopBackedgeGuardedByCond(L, P, LHS, RHS))
+  if (isLoopBackedgeGuardedByCond(L, P, LHS, RHS))
+    return ScalarEvolution::LoopInvariantPredicate(Pred, ArLHS->getStart(),
+                                                   RHS);
+
+  if (!CtxI)
     return None;
+  // Try to prove via context.
+  // TODO: Support other cases.
+  switch (Pred) {
+  default:
+    break;
+  case ICmpInst::ICMP_ULE:
+  case ICmpInst::ICMP_ULT: {
+    assert(ArLHS->hasNoUnsignedWrap() && "Is a requirement of monotonicity!");
+    // If we can prove that ArLHS <s RHS, and RHS >=s 0, and we know that ArLHS
+    // does not cross zero, there are two options:
+    // - ArLHS is always negative. It means that ArLHS <u RHS is always false;
+    // - ArLHS is always non-negative. It means that
+    //     ArLHS <s RHS <=> ArLHS <u RHS.
+    //   We are guarded by ArLHS <s RHS, so unsigned condition is trivially
+    //   true.
+    // All together it means that ArLHS <u RHS <=> Start(ArLHS) >=s 0.
+    // We can strenthen this to Start(ArLHS <u RHS).
+    auto SignFlippedPred = ICmpInst::getFlippedSignednessPredicate(Pred);
+    if (isKnownNonNegative(RHS) &&
+        isKnownPredicateAt(SignFlippedPred, ArLHS, RHS, CtxI))
+      return ScalarEvolution::LoopInvariantPredicate(Pred, ArLHS->getStart(),
+                                                     RHS);
+  }
+  }
 
-  return ScalarEvolution::LoopInvariantPredicate(Pred, ArLHS->getStart(), RHS);
+  return None;
 }
 
 Optional<ScalarEvolution::LoopInvariantPredicate>
 ScalarEvolution::getLoopInvariantExitCondDuringFirstIterations(
     ICmpInst::Predicate Pred, const SCEV *LHS, const SCEV *RHS, const Loop *L,
     const Instruction *CtxI, const SCEV *MaxIter) {
   // Try to prove the following set of facts:
   // - The predicate is monotonic in the iteration space.

llvm/lib/Transforms/Utils/SimplifyIndVar.cpp

bool SimplifyIndvar::makeIVComparisonInvariant(ICmpInst *ICmp,
   // current loop)
   const Loop *ICmpLoop = LI->getLoopFor(ICmp->getParent());
   const SCEV *S = SE->getSCEVAtScope(ICmp->getOperand(IVOperIdx), ICmpLoop);
   const SCEV *X = SE->getSCEVAtScope(ICmp->getOperand(1 - IVOperIdx), ICmpLoop);
 
   auto *PN = dyn_cast<PHINode>(IVOperand);
   if (!PN)
     return false;
-  auto LIP = SE->getLoopInvariantPredicate(Pred, S, X, L);
+
+  auto LIP = SE->getLoopInvariantPredicate(Pred, S, X, L, ICmp);
   if (!LIP)
     return false;
   ICmpInst::Predicate InvariantPredicate = LIP->Pred;
   const SCEV *InvariantLHS = LIP->LHS;
   const SCEV *InvariantRHS = LIP->RHS;
 
   // Rewrite the comparison to a loop invariant comparison if it can be done
   // cheaply, where cheaply means "we don't need to emit any new

llvm/test/Transforms/IndVarSimplify/cycled_phis.ll

failed.sibling:
   unreachable
 
 done:
   ret i32 %iv
 }
 
 ; Slightly more complex version of previous one (cycled phis).
 ; TODO: remove unsigned comparison by proving non-negativity of iv.start.
+; TODO: When we check against IV_START, for some reason we then cannot infer nuw for IV.next.
+;       It was possible while checking against IV. Missing inference logic somewhere.
 define i32 @start.from.sibling.iv.wide.cycled.phis(i32* %len.ptr, i32* %sibling.len.ptr) {
 ; CHECK-LABEL: @start.from.sibling.iv.wide.cycled.phis(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[LEN:%.*]] = load i32, i32* [[LEN_PTR:%.*]], align 4, !range [[RNG0]]
 ; CHECK-NEXT:    [[SIBLING_LEN:%.*]] = load i32, i32* [[SIBLING_LEN_PTR:%.*]], align 4, !range [[RNG0]]
 ; CHECK-NEXT:    [[SIBLING_LEN_WIDE:%.*]] = zext i32 [[SIBLING_LEN]] to i64
 ; CHECK-NEXT:    br label [[SIBLING_LOOP:%.*]]
 ; CHECK:       sibling.loop:

 ; CHECK-NEXT:    br label [[PREHEADER:%.*]]
 ; CHECK:       preheader:
 ; CHECK-NEXT:    br label [[LOOP:%.*]]
 ; CHECK:       loop:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[IV_START]], [[PREHEADER]] ], [ [[IV_NEXT:%.*]], [[BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    [[SIGNED_CMP:%.*]] = icmp slt i32 [[IV]], [[LEN]]
 ; CHECK-NEXT:    br i1 [[SIGNED_CMP]], label [[SIGNED_PASSED:%.*]], label [[FAILED_SIGNED:%.*]]
 ; CHECK:       signed.passed:
-; CHECK-NEXT:    [[UNSIGNED_CMP:%.*]] = icmp ult i32 [[IV]], [[LEN]]
+; CHECK-NEXT:    [[UNSIGNED_CMP:%.*]] = icmp ult i32 [[IV_START]], [[LEN]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_CMP]], label [[BACKEDGE]], label [[FAILED_UNSIGNED:%.*]]
 ; CHECK:       backedge:
-; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
+; CHECK-NEXT:    [[IV_NEXT]] = add nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[COND]], label [[LOOP]], label [[OUTER_LOOP_BACKEDGE]]
 ; CHECK:       outer.loop.backedge:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA]] = phi i32 [ [[IV_NEXT]], [[BACKEDGE]] ]
 ; CHECK-NEXT:    [[IV_LCSSA2:%.*]] = phi i32 [ [[IV]], [[BACKEDGE]] ]
 ; CHECK-NEXT:    [[OUTER_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[OUTER_COND]], label [[OUTER_LOOP]], label [[DONE:%.*]]
 ; CHECK:       failed.signed:

 ; CHECK-NEXT:    br label [[PREHEADER:%.*]]
 ; CHECK:       preheader:
 ; CHECK-NEXT:    br label [[LOOP:%.*]]
 ; CHECK:       loop:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[IV_START]], [[PREHEADER]] ], [ [[IV_NEXT:%.*]], [[BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    [[SIGNED_CMP:%.*]] = icmp slt i32 [[IV]], [[LEN]]
 ; CHECK-NEXT:    br i1 [[SIGNED_CMP]], label [[SIGNED_PASSED:%.*]], label [[FAILED_SIGNED:%.*]]
 ; CHECK:       signed.passed:
-; CHECK-NEXT:    [[UNSIGNED_CMP:%.*]] = icmp ult i32 [[IV]], [[LEN]]
+; CHECK-NEXT:    [[UNSIGNED_CMP:%.*]] = icmp ult i32 [[IV_START]], [[LEN]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_CMP]], label [[BACKEDGE]], label [[FAILED_UNSIGNED:%.*]]
 ; CHECK:       backedge:
-; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
+; CHECK-NEXT:    [[IV_NEXT]] = add nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[COND]], label [[LOOP]], label [[OUTER_LOOP_SELECTION:%.*]]
 ; CHECK:       outer.loop.selection:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA:%.*]] = phi i32 [ [[IV_NEXT]], [[BACKEDGE]] ]
 ; CHECK-NEXT:    [[IV_LCSSA2:%.*]] = phi i32 [ [[IV]], [[BACKEDGE]] ]
 ; CHECK-NEXT:    [[SWITCH_COND:%.*]] = call i32 @switch.cond()
 ; CHECK-NEXT:    switch i32 [[SWITCH_COND]], label [[TAKE_SAME:%.*]] [
 ; CHECK-NEXT:    i32 1, label [[TAKE_INCREMENT:%.*]]

llvm/test/Transforms/IndVarSimplify/outer_phi.ll

 ; CHECK:       outer:
 ; CHECK-NEXT:    [[OUTER_IV:%.*]] = phi i32 [ 0, [[ENTRY:%.*]] ], [ [[IV_NEXT_LCSSA:%.*]], [[OUTER_BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    br label [[INNER:%.*]]
 ; CHECK:       inner:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[OUTER_IV]], [[OUTER]] ], [ [[IV_NEXT:%.*]], [[INNER_BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    [[SIGNED_COND:%.*]] = icmp slt i32 [[IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[SIGNED_COND]], label [[INNER_1:%.*]], label [[SIDE_EXIT:%.*]]
 ; CHECK:       inner.1:
-; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[IV]], [[B]]
+; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[OUTER_IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_COND]], label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
 ; CHECK:       inner.backedge:
 ; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[INNER_LOOP_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[INNER_LOOP_COND]], label [[INNER]], label [[OUTER_BACKEDGE]]
 ; CHECK:       outer.backedge:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA]] = phi i32 [ [[IV_NEXT]], [[INNER_BACKEDGE]] ]
 ; CHECK-NEXT:    [[OUTER_LOOP_COND:%.*]] = call i1 @cond()

 ; CHECK:       outer:
 ; CHECK-NEXT:    [[OUTER_IV:%.*]] = phi i32 [ 0, [[ENTRY:%.*]] ], [ [[OUTER_MERGE:%.*]], [[OUTER_BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    br label [[INNER:%.*]]
 ; CHECK:       inner:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[OUTER_IV]], [[OUTER]] ], [ [[IV_NEXT:%.*]], [[INNER_BACKEDGE:%.*]] ]
 ; CHECK-NEXT:    [[SIGNED_COND:%.*]] = icmp slt i32 [[IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[SIGNED_COND]], label [[INNER_1:%.*]], label [[SIDE_EXIT:%.*]]
 ; CHECK:       inner.1:
-; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[IV]], [[B]]
+; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[OUTER_IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_COND]], label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
 ; CHECK:       inner.backedge:
 ; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[INNER_LOOP_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[INNER_LOOP_COND]], label [[INNER]], label [[OUTER_BACKEDGE]]
 ; CHECK:       outer.backedge:
 ; CHECK-NEXT:    [[OUTER_MERGE]] = phi i32 [ [[IV_NEXT]], [[INNER_BACKEDGE]] ]
 ; CHECK-NEXT:    [[OUTER_LOOP_COND:%.*]] = call i1 @cond()

 ; CHECK:       no_inner:
 ; CHECK-NEXT:    [[OUTER_COND_2:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br label [[OUTER_BACKEDGE]]
 ; CHECK:       inner:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[IV_NEXT:%.*]], [[INNER_BACKEDGE:%.*]] ], [ [[OUTER_IV]], [[INNER_PREHEADER]] ]
 ; CHECK-NEXT:    [[SIGNED_COND:%.*]] = icmp slt i32 [[IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[SIGNED_COND]], label [[INNER_1:%.*]], label [[SIDE_EXIT:%.*]]
 ; CHECK:       inner.1:
-; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[IV]], [[B]]
+; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[OUTER_IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_COND]], label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
 ; CHECK:       inner.backedge:
 ; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[INNER_LOOP_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[INNER_LOOP_COND]], label [[INNER]], label [[OUTER_BACKEDGE_LOOPEXIT:%.*]]
 ; CHECK:       outer.backedge.loopexit:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA:%.*]] = phi i32 [ [[IV_NEXT]], [[INNER_BACKEDGE]] ]
 ; CHECK-NEXT:    br label [[OUTER_BACKEDGE]]

 ; CHECK-NEXT:    br label [[OUTER_BACKEDGE]]
 ; CHECK:       if.false:
 ; CHECK-NEXT:    br label [[OUTER_BACKEDGE]]
 ; CHECK:       inner:
 ; CHECK-NEXT:    [[IV:%.*]] = phi i32 [ [[IV_NEXT:%.*]], [[INNER_BACKEDGE:%.*]] ], [ [[OUTER_IV]], [[INNER_PREHEADER]] ]
 ; CHECK-NEXT:    [[SIGNED_COND:%.*]] = icmp slt i32 [[IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[SIGNED_COND]], label [[INNER_1:%.*]], label [[SIDE_EXIT:%.*]]
 ; CHECK:       inner.1:
-; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[IV]], [[B]]
+; CHECK-NEXT:    [[UNSIGNED_COND:%.*]] = icmp ult i32 [[OUTER_IV]], [[B]]
 ; CHECK-NEXT:    br i1 [[UNSIGNED_COND]], label [[INNER_BACKEDGE]], label [[SIDE_EXIT]]
 ; CHECK:       inner.backedge:
 ; CHECK-NEXT:    [[IV_NEXT]] = add nuw nsw i32 [[IV]], 1
 ; CHECK-NEXT:    [[INNER_LOOP_COND:%.*]] = call i1 @cond()
 ; CHECK-NEXT:    br i1 [[INNER_LOOP_COND]], label [[INNER]], label [[OUTER_BACKEDGE_LOOPEXIT:%.*]]
 ; CHECK:       outer.backedge.loopexit:
 ; CHECK-NEXT:    [[IV_NEXT_LCSSA:%.*]] = phi i32 [ [[IV_NEXT]], [[INNER_BACKEDGE]] ]
 ; CHECK-NEXT:    br label [[OUTER_BACKEDGE]]