[InstSimplify] fold sdiv/srem based on compare of dividend and divisor
ClosedPublic

Authored by spatel on Sep 11 2017, 2:22 PM.

Details

Summary

This should bring signed div/rem analysis up to the same level as unsigned. We use icmp simplification to determine when the divisor is known greater than the dividend.

It's possible I've been staring at this too long and made it more complicated than necessary.

Here are attempts to prove correctness in Alive:
http://rise4fun.com/Alive/TRQp
http://rise4fun.com/Alive/DMs

Each positive test is followed by a negative test to show that we're not overstepping the boundaries of the known bits.

Diff Detail

Repository
rL LLVM
spatel created this revision.Sep 11 2017, 2:22 PM
majnemer added inline comments.
lib/Analysis/InstructionSimplify.cpp
1022–1023 ↗(On Diff #114686)

You could make this a little simpler by getting rid of the IsDiv flag.
The remainder side could do something like:

if (Constant *C = dyn_cast_or_null<Constant>(simplifySignedDiv(Op0, Op1, Q, MaxRecurse)))
  if (C->isNullValue())
    return Op0;
spatel added inline comments.Sep 11 2017, 3:04 PM
lib/Analysis/InstructionSimplify.cpp
1022–1023 ↗(On Diff #114686)

Ah, ok. If we go that route, we could just have this return a bool, then the caller can return the proper value. Let me write that up.

spatel updated this revision to Diff 114714.Sep 11 2017, 3:09 PM

Patch updated:
Let the callers (sdiv or srem) choose the appropriate answer based on a bool return from the common helper.

nlopes requested changes to this revision.Sep 12 2017, 2:50 PM

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.

This revision now requires changes to proceed.Sep 12 2017, 2:50 PM

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.
spatel updated this revision to Diff 115073.Sep 13 2017, 10:48 AM

Patch updated:
Handle the signed-min-value cases correctly. I've added 2 tests for those possibilities. We also managed to simplify an existing test with the extra check for the signed-min-value divisor.

nlopes accepted this revision.Sep 13 2017, 11:26 AM

LGTM, thanks.
You're right: the Boolean connector for the second transformation was flipped. All good now :)

This revision is now accepted and ready to land.Sep 13 2017, 11:26 AM
This revision was automatically updated to reflect the committed changes.