This is an archive of the discontinued LLVM Phabricator instance.

[SCEV] Add false->any implication
ClosedPublic

Authored by mkazantsev on Mar 16 2021, 6:44 AM.

Details

Summary

By definition of Implication operator, false -> true and false -> false. It means that
false implies any predicate, no matter true or false. We don't need to go any further
trying to prove the statement we need and just always say that false implies it in this case.

In practice it means that we are trying to prove something guarded by false condition,
which means that this code is unreachable, and we can safely prove any fact or perform any
transform in this code.

Diff Detail

Event Timeline

mkazantsev created this revision.Mar 16 2021, 6:44 AM
mkazantsev requested review of this revision.Mar 16 2021, 6:44 AM
Herald added a project: Restricted Project. · View Herald TranscriptMar 16 2021, 6:44 AM

Theoretically it should help, but maybe the price of triggered transformations will outweight the benefit. Can we run the automation to figure out if it actually helps?

Theoretically it should help, but maybe the price of triggered transformations will outweight the benefit. Can we run the automation to figure out if it actually helps?

https://llvm-compile-time-tracker.com/compare.php?from=49d0e115d5df40aa89339f4ace7a8dee378c03bb&to=369fd47a59582996bae60e37856b35718f8f4877&stat=instructions

Theoretically it should help, but maybe the price of triggered transformations will outweight the benefit. Can we run the automation to figure out if it actually helps?

https://llvm-compile-time-tracker.com/compare.php?from=49d0e115d5df40aa89339f4ace7a8dee378c03bb&to=369fd47a59582996bae60e37856b35718f8f4877&stat=instructions

Thanks Roman! Let's see if it gives us something..

Theoretically it should help, but maybe the price of triggered transformations will outweight the benefit. Can we run the automation to figure out if it actually helps?

TBF, we don't actually know what causes the cost there, do we?
Perhaps the change is cheap, but it happens to be so good that it enables further optimizations (or at least attempts thereof).

https://llvm-compile-time-tracker.com/compare.php?from=49d0e115d5df40aa89339f4ace7a8dee378c03bb&to=369fd47a59582996bae60e37856b35718f8f4877&stat=instructions

Thanks Roman! Let's see if it gives us something..

And apparently done.
Same situation :)

The cost is spread over all SCEV I guess. If we want to improve it, we should make it sitch by sitch. Apparently this sitution is rare. :( Well, it was worth trying.

nikic added a comment.Mar 16 2021, 7:15 AM

D90926 was a pretty nice improvement to isImpliedCond performance. Our test coverage is really bad though ("deleting a transform breaks no tests" level bad), so I didn't pursue that further at the time.

The cost is spread over all SCEV I guess. If we want to improve it, we should make it sitch by sitch. Apparently this sitution is rare. :( Well, it was worth trying.

While not a compile time win, this seems like an improvement on it's own to me.
The change itself is rather cheap (a plain single comparison).

That being said, i think i'm failing to understand why it implies *anything*?

This seems like a useful change to me purely on the transform impact. The compile time appears to be a wash. A refreshed patch which simply removed the misleading compile time comment would likely warrant an LGTM.

I would suggest auditing the callers to make sure perform checks in the right order though. This could be surprising if the caller isn't expecting to be analyzing potentially dead code.

Maybe even we should assert this condition? Not because it's wrong, but passing a trivial condition here really seems like a missing compile time optimization in each caller? (This is only a lightly considered suggestion, feel free to ignore if a glance at code shows me off base.)

mkazantsev added a comment.EditedMar 18 2021, 3:39 AM

That being said, i think i'm failing to understand why it implies *anything*?

Just by definition of implication: https://en.wikipedia.org/wiki/Truth_table#Logical_implication

In terms of compiler code, "guarded by false" means unreachable code, and basically any transform there is legal.

I would suggest auditing the callers to make sure perform checks in the right order though. This could be surprising if the caller isn't expecting to be analyzing potentially dead code.

The main users of this are is[Loop/BasicBlock]EntryGuardedByCond. They may be called by loop passes in arbitrary order. Imagine that a loop has been unswitched with some stay-in-loop condition turned to false. The consequent loop pass still thinks it's a loop (because dead CFG wasn't broken yet) and will analyze it as it normally would. I don't think every loop path should be doing this check on its own.

mkazantsev retitled this revision from [SCEV] Add false->any implication to save compile time to [SCEV] Add false->any implication.
mkazantsev edited the summary of this revision. (Show Details)

Removed comments regarding compile time.

mkazantsev edited the summary of this revision. (Show Details)Mar 18 2021, 3:47 AM
lebedev.ri accepted this revision.Mar 18 2021, 3:56 AM

That being said, i think i'm failing to understand why it implies *anything*?

Just by definition of implication: https://en.wikipedia.org/wiki/Truth_table#Logical_implication

Right, thanks for reminding me of that.

In terms of compiler code, "guarded by false" means unreachable code, and basically any transform there is legal.

Right. Iff the "guarded by false" dominates the code. (i.e. the code can only be reached through the guard)

With that spelled out explicitly, this looks good to me, thanks!

This revision is now accepted and ready to land.Mar 18 2021, 3:56 AM
This revision was automatically updated to reflect the committed changes.

I wrote a PR about a verifier error showing up with this commit:
https://bugs.llvm.org/show_bug.cgi?id=51179

I wrote a PR about a verifier error showing up with this commit:
https://bugs.llvm.org/show_bug.cgi?id=51179

Ping @mkazantsev : Do you know if that verifier error is anything to worry about?