This is an archive of the discontinued LLVM Phabricator instance.

[SCEV] Prove condition invariance via context
ClosedPublic

Authored by mkazantsev on Jul 14 2022, 4:45 AM.

Details

Summary

Contextual knowledge may be used to prove invariance of some conditions.
For example, in this case:

; %len >= 0
guard(%iv = {start,+,1}<nuw> <s %len)
guard(%iv = {start,+,1}<nuw> <u %len)

the 2nd check always fails if start is negative and always passes otherwise.

It looks like there is more opportunities of this kind that are still to be implemented.

Diff Detail

Event Timeline

mkazantsev created this revision.Jul 14 2022, 4:45 AM
Herald added a project: Restricted Project. · View Herald TranscriptJul 14 2022, 4:45 AM
Herald added a subscriber: hiraditya. · View Herald Transcript
mkazantsev requested review of this revision.Jul 14 2022, 4:45 AM
Herald added a project: Restricted Project. · View Herald TranscriptJul 14 2022, 4:45 AM
mkazantsev updated this revision to Diff 449617.Aug 3 2022, 3:03 AM

Rebased. Suprisingly, one of tests pessimized flags after it did a nice transform, but it means we are lacking another piece of logic somewhere else. The flags have been added just recently, and we might need some extra work to make it more robust.

apilipenko added inline comments.
llvm/lib/Analysis/ScalarEvolution.cpp
10811–10812

we know that ArLHS does not cross zero

Where do you get this fact from?

mkazantsev added inline comments.Aug 11 2022, 9:11 PM
llvm/lib/Analysis/ScalarEvolution.cpp
10811–10812

"Does not cross zero" is "hasNoUnsignedWrap", we got it from

auto MonotonicType = getMonotonicPredicateType(ArLHS, Pred);

and assert just here.

apilipenko added inline comments.Aug 11 2022, 10:34 PM
llvm/lib/Analysis/ScalarEvolution.cpp
10810–10824

Suggested slight rewording of the reasoning and restructuring of the code.

10819

Why don't you use Start(ArLHS) >=s 0 as the resulting invariant condition?

mkazantsev added inline comments.Aug 11 2022, 10:37 PM
llvm/lib/Analysis/ScalarEvolution.cpp
10819

Imagine RHS = 100. LHS <u 100 will allow us to infer more facts from it than LHS >=s 0.

mkazantsev added inline comments.Aug 11 2022, 10:38 PM
llvm/lib/Analysis/ScalarEvolution.cpp
10810–10824

Makes sense.

apilipenko accepted this revision.Aug 11 2022, 10:39 PM
apilipenko added inline comments.
llvm/lib/Analysis/ScalarEvolution.cpp
10819

Maybe add a comment about it as well?

This revision is now accepted and ready to land.Aug 11 2022, 10:39 PM
This revision was automatically updated to reflect the committed changes.

Hello,

I think I'm seeing a miscompile with this patch.
Reproduce with:

opt --passes="indvars" bbi-72689.ll -S -o -

indvars does

<   %cmp22.not.i = icmp ult i32 %storemerge13.i, 2
---
>   %cmp22.not.i = icmp ult i32 0, 2

which I think is incorrect.
We have

[...]
%storemerge13.i = phi i32 [ 0, %entry ], [ %dec.i, %for.inc32.i ]
%cmp22.not.i = icmp ult i32 %storemerge13.i, 2
[...]
%dec.i = add i32 %storemerge13.i, -1
[...]

so we start at 0, then add -1 so we get -1, and then do an ult compare between -1 (0xffffffff) and 2, which I suppose should be false?
But indvars changes the compare to icmp ult i32 0, 2 which is always true?

The end result is that the function loops forever instead of returning -1.

@uabelho thanks for your report. Let me take a look if it's causing the problem or exposing an existing one.

This comment was removed by mkazantsev.
mkazantsev added a comment.EditedAug 19 2022, 2:33 AM

This is what the transform sees:

ArLHS = {0,+,-1}<nuw><nsw><%for.body.i>, RHS = 2

nuw here looks like a bug to me. So this patch has exposed something else. I'll dig into it.

If it was nuw indeed, the transform would be correct.

Filed a https://github.com/llvm/llvm-project/issues/57247, not obvious to me that the bug is caused by my patch. Further details will go there.

Filed a https://github.com/llvm/llvm-project/issues/57247, not obvious to me that the bug is caused by my patch. Further details will go there.

Ok, thanks!