Teach SCEV to prove no overflow for an add recurrence by proving
something about the range of another add recurrence a loop-invariant
distance away from it.
Details
Diff Detail
Event Timeline
The logic is great. But we really need to determine whether computing SCEV for each recurrence 5 times is worthwhile. Please do some compile time experiments where SCEV is taking more time than usual to find out how much worse this makes it.
Why did you do this rather than checking SCEV's for existing phis? (I realize this is strictly better, but I'm curious about your motivation given that this is potentially a lot of extra work)
lib/Analysis/ScalarEvolution.cpp | ||
---|---|---|
1343–1344 | I would like better comments here. It should show the formula. e.g. {start - delta,+,step} ult (INT_MAX - delta) |
Sure, I'll run some experiments and measure the compile time.
Why did you do this rather than checking SCEV's for existing phis?
Do you mean just checking the folding set for an _existing_ SCEVAddRec instead of SE.getAddRecExpr(PreStart, Step, AR->getLoop(), SCEV::FlagAnyWrap)? That sounds like a very good idea, I'll try that.
Addresses review.
When writing down a proof for proveNoWrapByVaryingStart (thanks for
prodding me to do that!) I realized that the first version had a bug
- we need to prove (S-X)+X does not overflow for the inference to be
valid. This current version addresses that.
The current version also swaps out a full SCEVAddRecExpr construction
and just looks at the UniqueSCEVs set instead, and gives up if there
isn't a pre-existing add recurrence of the form we need. This should
address the compile time issue.
Otherwise looks great!
lib/Analysis/ScalarEvolution.cpp | ||
---|---|---|
1357 | I still don't see the bug. How can (3) be false with (1) and (2)? A counter example would help. |
lib/Analysis/ScalarEvolution.cpp | ||
---|---|---|
1357 | You're right, (3) is just (1) in the 0th iteration. I'll fix this. |
I would like better comments here. It should show the formula.
e.g.
{start - delta,+,step} ult (INT_MAX - delta)