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

[Nikita Popov via Phabricator via llvm-commits]

nikic added a comment.

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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103834