Page MenuHomePhabricator

[SCEV] Prove implications of different type via truncation
ClosedPublic

Authored by mkazantsev on Oct 16 2020, 6:17 AM.

Details

Summary

When we need to prove implication of expressions of different type width,
the default strategy is to widen everything to wider type and prove in this
type. This does not interact well with AddRecs with negative steps and
unsigned predicates: such AddRec will likely not have a nuw flag, and its
zext to wider type will not be an AddRec. In contraty, trunc of an AddRec
in some cases can easily be proved to be an AddRec too.

This patch introduces an alternative way to handling implications of different
type widths. If we can prove that wider type values actually fit in the narrow type,
we truncate them and prove the implication in narrow type.

Diff Detail

Event Timeline

mkazantsev created this revision.Oct 16 2020, 6:17 AM
Herald added a project: Restricted Project. · View Herald TranscriptOct 16 2020, 6:17 AM
mkazantsev requested review of this revision.Oct 16 2020, 6:17 AM
mkazantsev added inline comments.Oct 19 2020, 2:28 AM
llvm/test/Analysis/ScalarEvolution/srem.ll
32

Bug in underpying patch.

mkazantsev added inline comments.Oct 19 2020, 3:34 AM
llvm/test/Analysis/ScalarEvolution/srem.ll
32

It happens just because we create zero extend SCEV (and not proving further ule). A subject for a follow-up fix.

fhahn accepted this revision.Oct 20 2020, 9:14 AM

LGTM, thanks! As mentioned inline, I think it would be good to have a fix for the issue pointed out ready before the change goes in.

llvm/test/Analysis/ScalarEvolution/srem.ll
32

It would probably be good to have a fix lined up before this goes in

This revision is now accepted and ready to land.Oct 20 2020, 9:14 AM
mkazantsev added inline comments.Oct 20 2020, 9:19 PM
llvm/test/Analysis/ScalarEvolution/srem.ll
32

Agreed, I'm looking into it. Thanks!

mkazantsev added inline comments.Oct 20 2020, 9:51 PM
llvm/test/Analysis/ScalarEvolution/srem.ll
32

Root cause here: by the moment when we query this, nuw flag is not set and one of rules in range computation does not apply. General problem: we don't drop constant ranges when we update flags when we should.

mkazantsev added inline comments.Oct 20 2020, 10:40 PM
llvm/test/Analysis/ScalarEvolution/srem.ll
32

Fix: https://reviews.llvm.org/D89847

The problem is old, general and exists regardless of this patch. So I don't think it should be holding it away.

mkazantsev reopened this revision.Oct 20 2020, 11:10 PM

The underlying patch D89381 was reverted again, and nothing will work without it. Reopenning until this has beeen resolved.

This revision is now accepted and ready to land.Oct 20 2020, 11:10 PM