Page MenuHomePhabricator

[SCEV] Use knowledge of stride to prove loops finite for LT exit count computation

Authored by reames on Thu, Jun 10, 2:57 PM.



This came up in the post commit review discussion of D103834.

The basic idea is that the general case was using a loop being finite by assumption to prove that step was non-zero. Non-zero combined with NoWrap flags in turns proves the loop must exit before overflow occurs. This change adds an explicit check for when the loop isn't known mustprogress, but we can directly prove that the step isn't zero. This will mostly help non-C/C++ family languages, though it may benefit some C language test cases as well.

Diff Detail

Event Timeline

reames created this revision.Thu, Jun 10, 2:57 PM
reames requested review of this revision.Thu, Jun 10, 2:57 PM
Herald added a project: Restricted Project. · View Herald TranscriptThu, Jun 10, 2:57 PM

I don't see any obvious issue here. I'd like to work through the known miscompiles before we start expanding this, though.

mkazantsev accepted this revision.Fri, Jun 11, 2:51 AM

Looks fine, but agreed with Eli. Please don't land it for some more days to find and fix miscompiles from underlying patches (if any).


Please refactor as

if (PredicatedIV || !NoWrap || isKnownNonPositive(Stride))
     return getCouldNotCompute();
bool StrideNonZero = loopIsFiniteByAssumption || isLoopEntryGuardedByCond ...
 if (!StrideNonZero )
     return getCouldNotCompute();

The dom tree walking is expensive, let's only do it if easy checks failed.

This revision is now accepted and ready to land.Fri, Jun 11, 2:51 AM

I agree with the request to hold until latent miscompile in underlying code is addressed. I will hold this patch until that happens, and then land without further review. Max, good suggestion on condition ordering, will address in landed patch.