[PATCH] D37713: [InstSimplify] fold sdiv/srem based on compare of dividend and divisor

[Sanjay Patel via Phabricator via llvm-commits]

spatel added a comment.

In https://reviews.llvm.org/D37713#868735, @nlopes wrote:

> I was trying to prove this in Alive, but the proof doesn't go through.
>  Some corner cases are not correct: http://rise4fun.com/Alive/iVs
>  For example: 'INT_MIN / something' would be replaced with 0, but shouldn't.


Yes, you're correct. We can't take abs(signed_min) because that's undefined. But I think you have the wrong formula for the constant divisor cases in your proofs - it should be && rather than ||?
Please have a look:
http://rise4fun.com/Alive/WI5

So I think there are 2 bugs:

1. If the dividend constant isMinSignedValue(), bail out - nothing will prove that division is zero. This case miscompiles with this version of the patch.
2. If the divisor constant isMinSignedValue(), just show that the dividend is *not* the divisor. We miss this optimization with this version of the patch.


https://reviews.llvm.org/D37713