Recent improvements in symbolic exit count computation revealed some problems with
SCEV's ability to find invariant predicate during first iterations. Ultimately it is based on its
ability to prove some facts for value on the last iteration. This last value, when it includes
umin as part of exit count, isn't always simplified enough. The motivatin example is following:
https://github.com/llvm/llvm-project/issues/59615
Could not prove:
Pred = 36, LHS = (-1 + (-1 * (2147483645 umin (-1 + %var)<nsw>))<nsw> + %var), RHS = %var FoundPred = 36, FoundLHS = {1,+,1}<nuw><nsw><%bb3>, FoundRHS = %var
Can prove:
Pred = 36, LHS = (-1 + (-1 * (-1 + %var)<nsw>)<nsw> + %var), RHS = %var FoundPred = 36, FoundLHS = {1,+,1}<nuw><nsw><%bb3>, FoundRHS = %var
Here (2147483645 umin (-1 + %var)<nsw>) is exit count composed of two parts from
two different exits: 2147483645 and (-1 + %var)<nsw>. When it was only one (latter)
analyzeable exit, for it everything was easily provable. Unfortunately, in general case umin
in one of add's operands doesn't guarantee that the whole sum reduces, especially in presence
of negative steps and lack of nuw. I don't think there is a generic legal way to somehow play
around this umin.
So the ad-hoc solution is following: if we failed to find an equivalent predicate that is invariant
during first MaxIter iterations, and MaxIter = umin(a, b, c...), try to find solution for at least one
of a, b, c... Because they all are uge than MaxIter, whatever is true during a (b, c) iterations
is also true during MaxIter iterations.
As a followup, handle umin_seq as well? Don't think poison behavior is important here.