Page MenuHomePhabricator

[ScalarEvolution] Try harder to prove overflow in howManyLessThans.
Changes PlannedPublic

Authored by efriedma on Jul 19 2021, 6:24 PM.



If we have an instruction "add nsw (IV - Stride), Stride" feeding into the icmp, we know Start - Stride doesn't overflow.

It's unfortunate we can't deduce this more directly, but we don't really have any SCEV infrastructure to support this sort of check.

Diff Detail

Event Timeline

efriedma created this revision.Jul 19 2021, 6:24 PM
efriedma requested review of this revision.Jul 19 2021, 6:24 PM
Herald added a project: Restricted Project. · View Herald TranscriptJul 19 2021, 6:24 PM
efriedma updated this revision to Diff 359979.Jul 19 2021, 6:26 PM

Missed a test update

reames requested changes to this revision.Jul 20 2021, 9:58 AM

Not really a fan of the structure of this change. Bear with me as I talk through a couple of approaches (only the last of which may work.)

Let me throw out an approach for this in terms of SCEVs. I'm going to use the variable names from foo1 in trip-count-unknown-stride.ll to make this understandable.
%i.05 = {0, +, %s}
%add = {0 + %s, +, %s}

The condition we need to prove is that (0 + %s - %s < 0 + %s. (Remember that the start here is in terms of %add, not %i.05.)

One tactic would be to prove (0 - %s) < 0. (i.e. cancel %s on either side - we don't care whether the addition of %s would wrap in that step.) This reduces to proving %s > 0. This is interesting as we already have a framework for proving strides positive. Maybe we can extend that?

Interestingly, we can do that with SCEV. Consider the following code:

if (!PositiveStride) {
  if (IsSigned && NoWrap &&
      isLoopInvariant(RHS, L) && IV->getStart() == Stride &&
      isLoopEntryGuardedByCond(L, Cond, getZero(RHS->getType()), RHS) && 
    PositiveStride = true;

I'd written this for another purpose which didn't work out, but I think the structure is valid. This is maybe too specific for a zero start on i.05 - though maybe we can generalize?

Anyways, that isn't a fully solution, but I'd strongly prefer you try to use a SCEV proof here over mixing IR and SCEV proofs.

This revision now requires changes to proceed.Jul 20 2021, 9:58 AM
efriedma planned changes to this revision.Jul 20 2021, 12:08 PM
efriedma updated this revision to Diff 360226.Jul 20 2021, 12:12 PM
efriedma retitled this revision from [ScalarEvolution] Try harder to prove overflow in howManyLessThans. to [WIP][ScalarEvolution] Try harder to prove overflow in howManyLessThans..

Added another interesting case to look at. Still considering possible solutions that don't involve poking at IR directly.

The easiest thing here would be if SCEV recorded the flags somewhere... but unfortunately, we don't; when we discover the flags aren't universally applicable, we throw them away. We could try to construct some sort of side-table, I guess, to provide an API getNoWrapFlagsWithContext(SCEV*, Instruction*). So basically the same logic as this, but factored away.

One alternative I considered is looking at the nowrap flags of the AddRec "IV - Stride". We do often manage to deduce nsw/nuw, and if the backedge is taken, it proves Start - Stride doesn't overflow. But if we're doing that, I'm not sure how we prove the case where the backedge isn't taken.

Any comments on whether we want to merge this patch? Or how we can encode the necessary information into ScalarEvolution? (Really, I'm more concerned about the pointer_iv_nowrap_guard case than the unknown-stride case.)

reames accepted this revision.Aug 31 2021, 5:19 PM

LGTM. I'm not completely opposed to this and don't want to block progress further. I do think we need something better and more general. If you've got some time in the next couple days, I'd really like to get on a call and chat through what that might be.

One, possibly crazy, idea would be to use the SCEV <-> Value maps we have, and then do a forward propagation on the values to see if a given addrec being poison is guaranteed to trigger UB before the latch is taken. In this case, we should be able to map from the addrec to the IR expressions, and then find the poison reaching latch without needing to explicitly pass in the conditions.


I don't understand this line of the diff. Can you remove for the moment, and do this in a separate change?

The mixed usage of OrigStart and Start here is confusing.

125 ↗(On Diff #360226)

Please land this separately, and then rebase over so that the landed diff shows the change.

This revision is now accepted and ready to land.Aug 31 2021, 5:19 PM

Committed new test separately. Split off the Start/OrigStart thing to D109465.

@efriedma Can I ask you to prioritize landing this? I suspect this is going to reduce the test diffs implied by any fix to D106852, and I'd like to get this in so we can build on it.

(For context, we're likely to loose ability to infer flags on the add forming the start expression for the post-increment IV. As such, being able to directly derive the fact from the IR - this patch - becomes much more relevant. )

efriedma updated this revision to Diff 372361.Sep 13 2021, 4:08 PM
efriedma retitled this revision from [WIP][ScalarEvolution] Try harder to prove overflow in howManyLessThans. to [ScalarEvolution] Try harder to prove overflow in howManyLessThans..


efriedma planned changes to this revision.May 17 2022, 12:42 PM

(This currently doesn't apply cleanly.)

Herald added a project: Restricted Project. · View Herald TranscriptMay 17 2022, 12:42 PM
bsmith added a subscriber: bsmith.May 18 2022, 3:15 AM