[PATCH] D88086: [ARM][MVE] tail-predication: checks for the elementcount, cont'd

[Eli Friedman via Phabricator via llvm-commits]

efriedma accepted this revision.
efriedma added a comment.
This revision is now accepted and ready to land.

If you'd prefer to delete the overflow code first, sure.  LGTM

> tripcount: (1 + ((-4 + (4 * ((3 + %N) /u 4))<nuw>) /u 4))<nuw><nsw>

Is this really the expression we end up with?  It would be a lot simpler to analyze this if we could simplify to `(3 + %N) /u 4)`.

> and write a SCEV visitor/matcher, and see if the elementcount is "part of the tripcount", i.e. if they are bound by the same variable modulo the rounding up, then we have a very strong indication that we are talking about a well behaving loop without any chance of overflow. So in a way it is similar to the code removed here in Check 1 but used for another purpose I guess.

Isn't what you're describing part of check 1 (avoiding vctp in a loop that we probably can't tail-predicate)?  Not sure it helps with proving the correctness?

Actually, I guess if you could prove that the tripcount is precisely equal to `(ElementCount + VectorWidth - 1)/VectorWidth`, you could also use that to prove the subtraction doesn't overflow.


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

https://reviews.llvm.org/D88086