[PATCH] D103834: [SCEV] Properly guard reasoning about infinite loops being UB on mustprogress

[Bjorn Pettersson via Phabricator via llvm-commits]

bjope added a comment.

In D103834#2810888 <https://reviews.llvm.org/D103834#2810888>, @nikic wrote:

> In D103834#2810849 <https://reviews.llvm.org/D103834#2810849>, @bjope wrote:
>
>> One thing that might cause problems here is that it seems like getting the MustProgress attribute on a Function is quite hard. It is basically inferred by having WillReturn on the Function, and afaict the WillReturn attribute is never inferred if the Functions contain loops.
>>
>> In the godbolt example above the Function has no MustProgress attribute, however the loop has a MustProgress attribute. So maybe `loopIsFiniteByAssumption` should check if the loop has MustProgress as well?
>
> Yes, it should be checking `hasMustProgress(L)` as well.
>
>> That wouldn't however help for the regressions we see downstream, because we do not get any MustProgress attributes on the loops either in that case. No idea why really, but I figure those depend on the C-standard in some way. But aren't the loops in my example finite? So why is MustProgress attributes important here?
>
> Consider your example with `n = 1`:
>
>   long foo(long A[]) {
>     long x = 0;
>     for (long j = 0; j < 1; ++j)
>       for (long i = j; i < 1; i += 1/2)
>         x += A[i];
>     return x;
>   }
>
> Note that thus `j == 0`,  and `1/2 == 0`:
>
>   long foo(long A[]) {
>     long x = 0;
>     for (long i = 0; i < 1; i += 0)
>       x += A[i];
>     return x;
>   }
>
> This is an infinite loop.

Sorry, I used wrong example in the link. I've changed it to something where I do "i += n" instead of "i += n/2".

Is perhaps the problem that "i += n" might overflow (UB) and thereby we can't guarantee "must progress"?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103834