Page MenuHomePhabricator

[PSCEV] Create AddRec for Phis in cases of possible integer overflow, using runtime checks

Authored by dorit on Feb 16 2017, 5:25 AM.



Extend the SCEVPredicateRewriter to work a bit harder when it encounters an UnknownSCEV whose Value is a Phi node.
The goal it to build an AddRecurrence for Phi nodes whose update chain involves casts, that can be ignored under the proper runtime overflow test.
This is the first step in addressing PR30654.
Next steps will improve upon it, as detailed in the comment in the body of the patch (under "TODO").

(BTW, If some of these steps seem critical I am happy to include them with this first patch, if this patch looks in principle ok (I don't want to build much upon a wrong direction...)).

Diff Detail


Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
dorit updated this revision to Diff 95137.Apr 13 2017, 8:44 AM
dorit added a comment.Apr 13 2017, 9:00 AM

Regarding testing: it would be nicer to add some LAA tests, since the LAA analysis results will print the added predicates and the SCEV expressions for the bounds.

Until your patch in D17080 is committed my patch does not have an effect on loop-access-analysis PSE (only to loop-vectorizer's PSE)… So for now nothing is printed. I'm happy to add a loop-accesses analysis test as soon as your patch is committed.

Thanks very much for your comments,

1665 ↗(On Diff #92622)

The point of the mapping would be to remove existing loop-variant SCEVUnknowns from the analysis result, so we should have a better name for this? Maybe PredicatedAnalyzableSCEVs?

Changed to PredicatedSCEVRewrites (since we can rewrite the SCEVUnknowns into the SCEV on the RHS if we add the predicate). But if your suggestion is more intuitive to you I'll change to that.

10424 ↗(On Diff #92622)

Yes, I think you're right… This simplifies a few things… :-) so no need for a visitTruncateExpr case at all in this rewriter... the base class rewriter can handle the Truncate (without any predicates) (right?)


dorit added inline comments.Apr 14 2017, 10:07 PM
1665 ↗(On Diff #92622)

We should also remove mappings in forgetLoop().

Just noticed there's also a forgetMemoizedResults(S). Looks like we should be removing the mapping for S there too, right?

dorit updated this revision to Diff 95409.Apr 16 2017, 8:56 AM

Remove mappings from PredicatedSCEVRewrites also in forgetMemoizedResults().

dorit added a comment.Apr 23 2017, 1:09 AM

ping :-)

nitpick: you should run a spell checker over the patch.

This generally looks ok to me but since this is a complex change @sanjoy should approve it before being committed.


4220 ↗(On Diff #95409)

I think we need a more formal explanation here on why this predicate guarantees that this is an AddRecExpr.

We're trying to prove that if we have:

SymbolicPHI = phi({Start, LoopHead}, {NextValue, LoopLatch})
NextValue = (Sext ix (Trunc iy (%SymbolicPHI) to ix) to iy) + InvariantAccum

then SymolicPHI = {Start, +, InvariantAccum}.

At iteration 0 both values are equal to Start, so it's enough to prove that

SymbolicPhi + Invariant == (Sext (trunc (SymbolicPHI)) + Invariant, which should be true from the SCEV predicate.

10424 ↗(On Diff #92622)

Correct, we shouldn't need to do anything here.

sanjoy requested changes to this revision.Apr 24 2017, 11:02 PM

Some comments inline.

1208 ↗(On Diff #95409)


1211 ↗(On Diff #95409)


4042 ↗(On Diff #95409)

This is very minor, but we usually spell these as SExt and ZExt, in keeping with camel case.

4081 ↗(On Diff #95409)


4112 ↗(On Diff #95409)

Usually for out parameters like this, the type is const SCEVPredicate *&. But I'd prefer just returning an std::pair.

4124 ↗(On Diff #95409)

Can you do find({SymbolicPHI, L})?

4137 ↗(On Diff #95409)

Pair isn't clear. Please either name it something more specific, or (IMO better) use {SymbolicPHI, L} instead of Pair.

4138 ↗(On Diff #95409)

Can you do {SymbolicPHI, nullptr} instead of make_pair?

4202 ↗(On Diff #95409)

Do you also need to check that the recurrence is affine?

4216 ↗(On Diff #95409)


4221 ↗(On Diff #95409)

I'm not sure that this is correct. Say we had a loop with 4 iterations, StartVal was i16 257, Accum was i16 1, TruncTy was i8 and the PHI was being zero extended. In that case, the value of the PHI node on the second iteration (i.e. after taking the backedge once) would be (trunc 257) + 1 = 2. However, despite {(trunc 257),+,1} = {1,+,1} not unsigned-overflowing in 4 iterations, {257,+,1} would not produce the correct values for the PHI node.

10384 ↗(On Diff #95409)

Doesn't PredicatedSCEVRewrites.erase(I++) invalidate E?

10682 ↗(On Diff #95409)

Use auto * for pointers.

This revision now requires changes to proceed.Apr 24 2017, 11:02 PM
dorit added a comment.Apr 25 2017, 5:30 AM

Hi Sanjoy, I will upload a new fixed version soon; just have two quick followup questions below. Thanks a lot!

4202 ↗(On Diff #95409)

Oh, probably so…

Do you think the isAffine check is also required in createAddRecFromPHI()? createAddRecFromPHIWithCasts() is basically a subset of createAddRecFromPHI, modified to consider also the sext-trunc cast pattern (the intention is later to try to factor out common parts as much as possible). I copied this check from there without thinking much…

4221 ↗(On Diff #95409)

I see.

So I guess we should be returning a {(sext (trunc Start)),+,{(sext (trunc Accum))} as the newAR, right...?

sanjoy added inline comments.Apr 25 2017, 10:11 AM
4202 ↗(On Diff #95409)

I was suggesting the isAffine since IIRC (but please check) you cannot create a no wrap predicate on a non-affine add recurrence.

4221 ↗(On Diff #95409)

Not sure how that will work -- won't {(sext (trunc Start)),+,{(sext (trunc Accum))} be {1,+,1} and thus be 1 instead of 257 in the first iteration? I haven't thought this through, but I suspect you'll have to check that the starte value fits in the narrower type or something like that.

In any case, I agree with Silviu here -- whatever you go with, please justify why that is correct with a proof here.

10676 ↗(On Diff #95409)

I'm also not a big fan of the name analyzeUnknownSCEVPHI here -- analyze does not mean anything specific, and the UnknownSCEV part is redundant. How about convertToAddRecWithPreds?

sbaranga added inline comments.Apr 25 2017, 10:40 AM
4221 ↗(On Diff #95409)

Maybe have two extra SCEVEqualPredicates to test that (sext (trunc Start)) == Start and {(sext (trunc Accum))} == Accum and return {Start, + Accum}?

Before adding the extra predicates it would be worth testing if SCEV can prove these properties statically first (for example for cases where either Start or Acum are constants).

dorit added inline comments.Apr 26 2017, 4:16 AM
4221 ↗(On Diff #95409)

Good idea! Sanjoy, Silviu: Are you ok with extending the SCEVEqualPredicate to a non constant on the RHS? (I think currently only SCEV == constant is supported).

sbaranga added inline comments.Apr 26 2017, 9:10 AM
4221 ↗(On Diff #95409)

That's ok with me.

dorit updated this revision to Diff 98422.May 10 2017, 3:29 AM
dorit edited edge metadata.

Main changes:

  1. SCEVEqualPredicate can take any SCEV on LHS/RHS (instead of only SCEVUnknown/SCEVConstant )
  2. We add three predicates instead of only one; so we now have pairs of <SCEV, SmallVector of predicates> (instead of <SCEV, single Predicate>)
  3. Added a proof for why these predicates guarantee the correctness of the proposed rewrite
  4. Addressed Style and Spelling comments


dorit updated this revision to Diff 98427.May 10 2017, 4:55 AM

(discovered typo in the documentation)

sbaranga added inline comments.May 22 2017, 3:20 PM
4355 ↗(On Diff #98427)

I originally had in mind testing the SCEV expressions for equality (Expr == ExtendedExpr) and checking that both are loop invariant.

I had a look at the implementation of isKnownPredicate, and I'm not convinced this would work as expected. Can we add a regression test for this?

I think we need to check anyway that both expressions are loop invariant before adding the predicate.

dorit updated this revision to Diff 100147.May 24 2017, 12:42 PM
  • We now require that Accum is loop invariant.
  • Added a simple Expr == ExtendedExpr check, and only if it fails we call isKnownPredicate().
  • Extended the testcase:

• Check that we have both the overflow runtime check and the equality runtime check in doit1 and doit2
• Added doit3: where step is not invariant (not very interesting - we do nothing)
• Added doit4: where we can figure out at compile time that step == sext(trunc(step)). Here we check that we only have the overflow runtime check (without the equality runtime check).


dorit added inline comments.May 24 2017, 12:43 PM
4355 ↗(On Diff #98427)

Right. I was assuming Accum is invariant in the loop, forgot I was allowing it to not be invariant. Thanks.

dorit added a comment.Jun 5 2017, 3:53 AM


Sorry for the delay, I missed the last update. I have a few minor suggestions, but otherwise I think it generally looks good.
I think Sanjoy still needs to approve this before it can go in.


244 ↗(On Diff #100147)

Ideally we would have something (not necessarily in SCEVEqualPredicate) to verify that these predicates can be checked.

We should also be making the LHS->RHS substitution in the rewriter at some point (not necessarily in this change).

4109 ↗(On Diff #100147)


4295 ↗(On Diff #100147)

This is a bit hard to follow with NewExpr, Expr, etc and the initial statement problem should be simplified.

I guess we just want to prove that Expr(i) = Start + i *Accum, given that

(1) Expr(0) = Start
(2) Expr(i+1) = (Ext ix (Trunc iy (Expr(i)) to ix) to iy) + Accum

4319 ↗(On Diff #100147)

No text should be required for iteration 2, proving the induction step should be enough.

4341 ↗(On Diff #100147)

It would be better to just use Ext and Trunc as separate operators instead SExtTrunc.

4 ↗(On Diff #100147)

Could you add some text for each of these saying what predicates get added?

Thanks Silviu. I'll iron the comments following your suggestions.

244 ↗(On Diff #100147)

Can you please clarify what check is missing?

And where would be an appropriate place add a TODO comment about the substitution?

4319 ↗(On Diff #100147)

I thought it's helpful to have an example step before the formal step. I'll drop it.

sbaranga added inline comments.Jun 14 2017, 9:03 AM
244 ↗(On Diff #100147)

If we would have a Loop * as a member of SCEVEqualPredicate, and we could check that both LHS and RHS are invariant inside the constructor.

However, we don't need the Loop for anything else so I'm not sure that would be the right solution.

I guess since we already have an assert in AppendPredicate that should be enough for now.

dorit updated this revision to Diff 102963.Jun 18 2017, 12:34 AM

Addressed Silviu's last comments on the documentation:

  • Added the predicates that are added for each of the loops in the testcase
  • In the proof:
    • dropped all the introductory text and jump directly to the formal proof.
    • expanded the short notation I was using (SExTrunc) into the explicit notation (Ext ix (Trunc iy () to ix ) to iy)

@sbaranga, @sanjoy, ping :-)

dorit added a comment.Jul 2 2017, 1:24 AM



It looks ok to me, thanks!


dorit added a comment.Jul 9 2017, 12:12 AM

@sanjoy, is the patch ok with you?


sanjoy requested changes to this revision.Jul 11 2017, 4:04 PM

Mostly minor stuff.

245 ↗(On Diff #102963)

Now that the type system does not guarantee this, how about adding an assert that LHS != RHS?

1719 ↗(On Diff #102963)

Why not have the key type be std::pair<const SCEVUnknown *, const Loop *>?

4169 ↗(On Diff #102963)

s/const SCEV *SymbolicPHI/const SCEVUnknown *SymbolicPHI/

4186 ↗(On Diff #102963)

How about doing this check as the very first thing (to avoid doing this extra work when it would have failed anyway)?

4262 ↗(On Diff #102963)

IMO a slightly more idiomatic pattern (which would obviate the need for the *** Part1 comment) is to have a createAddRecFromPHIWithCasts and a createAddRecFromPHIWithCastsImpl, where the first function checks PredicatedSCEVRewrites for an existing solution, and delegates to createAddRecFromPHIWithCastsImpl if we don't have a cached solution.

4276 ↗(On Diff #102963)

Is this semantically important? That is, if you remove this and instead ensure that we always populate PredicatedSCEVRewrites[{SymbolicPHI, L}] before leaving this function, will we enter an infinite loop somewhere?

4318 ↗(On Diff #102963)

Should we be getting here in the Add->getOperand(i) == SymbolicPHI case? Shouldn't the regular add recurrence creating logic have triggered?

4399 ↗(On Diff #102963)

You should be able to cast<> here.

This revision now requires changes to proceed.Jul 11 2017, 4:04 PM
dorit updated this revision to Diff 106616.Jul 14 2017, 4:16 AM
dorit edited edge metadata.

Addressing Sanjoy's comments.

dorit marked 7 inline comments as done.Jul 14 2017, 4:30 AM

Hi Sanjoy,
Thanks! Comments addressed,

245 ↗(On Diff #102963)

Added in the constructor.

1719 ↗(On Diff #102963)

Absolutely right (that was the intention, but somehow it made it only to the comment... )

4276 ↗(On Diff #102963)

I added a clarification on the motivation for this early initialization. There is nothing semantic behind it. It is just to avoid having to initialize it upon every exit from the function (keep things a bit more compact, avoid the slight code duplication, make sure we don't forget it…). Is that ok with you with the clarification?

4318 ↗(On Diff #102963)

yes, I would indeed expect it would have been caught already; added a comment here, and an assert in isSimpleCastedPHI.

sanjoy accepted this revision.Jul 15 2017, 12:33 PM

lgtm with one nit

4276 ↗(On Diff #102963)

Given that you now have the createAddRecFromPHIWithCastsImpl split out, a cleaner way to achieve the same property would be to insert the result into the cache in createAddRecFromPHIWithCasts.

This revision is now accepted and ready to land.Jul 15 2017, 12:33 PM
dorit updated this revision to Diff 106819.Jul 16 2017, 2:35 PM
dorit marked 4 inline comments as done.

Hi Sanjoy,


I addressed your last comment + made another small change:

Should we be getting here in the Add->getOperand(i) == SymbolicPHI case? Shouldn't the regular add recurrence creating logic have triggered?

I realized that we may be getting here with Op == SymbolicPHI because we haven't yet processed the rest of the operands of the Add... (so createAddRecFromPHI may have failed because one of them is not invariant). So I changed the assert back to an if, with a detailed comment (in isSimpleCastedPHI).

Will wait a bit before I commit.

Many thanks Sanjoy and Silviu for all your help with this patch,


This revision was automatically updated to reflect the committed changes.