[PATCH] D103834: [SCEV] Properly guard reasoning about infinite loops being UB on mustprogress
Bjorn Pettersson via Phabricator via llvm-commits
llvm-commits at lists.llvm.org
Thu Jun 10 09:51:10 PDT 2021
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
More information about the llvm-commits
mailing list