[PATCH] D104140: [SCEV] Allow negative steps for LT exit count computation

[Philip Reames via Phabricator via llvm-commits]

reames added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:11630
     // Precondition a) implies that if the stride is negative, this is a single
     // trip loop. The backedge taken count formula reduces to zero in this case.
     //
----------------
efriedma wrote:
> reames wrote:
> > efriedma wrote:
> > > I think this needs to be "if the stride is negative and rhs is invariant".
> > I've given this a lot of thought and I don't believe this is true.  Let me explain why I think the code is correct, and you can poke holes in my reasoning.  :)
> > 
> > A negative stride must be greater than half of the addressable space.  Thus, we can only add a negative stride once without producing poison.
> > 
> > We check that if IV becomes poison that the loop must execute UB.  (This is the purpose of the ControlsExit check combined with the flag check.)  Thus, we don't have to worry about IV being poison, but another exit being taken before the one we're analyzing.  (This is important as it cuts off a *lot* of subtle edge case reasoning.)
> > 
> > As a result, we can infer that IV must add the step at most once.  Given we must increment IV on each iteration, this implies the backedge is not taken.
> > 
> > Note that the value of RHS did not appear in any of that logic.   
> > 
> > Chasing through the code for computeMaxBECountForLT, we appear to produce a correct/conservative result for a negative stride.  
> > 
> > Do you have a particular counter example in mind?
> > 
> > p.s. The means by which we prove poison triggers immediate UB could be generalized easily here.  Maybe something to explore in the future if we want to expand support for multiple exit loops.  
> I was thinking of something like this:
> 
> ```
> int a(int *x) {
>   int i = 0;
>   do {
>     i -= 2;
>   } while (i < x[i]);
>   return i;
> }
> int main() {
>     int z[] = {-100000,0,0,0,};
>     __builtin_printf("%d\n", a(z+4));
> }
> ```
> 
> Am I missing some condition that excludes this?
Quick answer: I'd gotten myself confused on nsw semantics of add w/negative RHS again.  Long answer to follow once I've given it a bit more thought.  



CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D104140/new/

https://reviews.llvm.org/D104140