KnownBits: refine srem for high-bits

[artagnon]

KnownBits::srem does not correctly set the leader zero-bits, omitting the fact that LHS may be known-negative or known-non-negative. Fix this.

Alive2 proof: https://alive2.llvm.org/ce/z/Ugh-Dq

[llvmbot]

@llvm/pr-subscribers-backend-arm
@llvm/pr-subscribers-llvm-support

@llvm/pr-subscribers-llvm-analysis

Author: Ramkumar Ramachandra (artagnon)

Changes

KnownBits::srem does not correctly set the leader zero-bits, omitting the fact that LHS may be known-negative or known-non-negative. Fix this.

Alive2 proof: https://alive2.llvm.org/ce/z/WcDkSX

-- 8< --
Based on #109006.

---

Full diff: https://github.com/llvm/llvm-project/pull/109121.diff

2 Files Affected:

• (modified) llvm/lib/Support/KnownBits.cpp (+7-3)
• (renamed) llvm/test/Analysis/ValueTracking/knownbits-rem.ll (+22)

diff --git a/llvm/lib/Support/KnownBits.cpp b/llvm/lib/Support/KnownBits.cpp
index 8e31e0ced2d731..c6f4b7255d8e15 100644
--- a/llvm/lib/Support/KnownBits.cpp
+++ b/llvm/lib/Support/KnownBits.cpp
@@ -1075,9 +1075,13 @@ KnownBits KnownBits::srem(const KnownBits &LHS, const KnownBits &RHS) {
 
   // The sign bit is the LHS's sign bit, except when the result of the
   // remainder is zero. The magnitude of the result should be less than or
-  // equal to the magnitude of the LHS. Therefore any leading zeros that exist
-  // in the left hand side must also exist in the result.
-  Known.Zero.setHighBits(LHS.countMinLeadingZeros());
+  // equal to the magnitude of either operand.
+  uint32_t LeadR =
+      RHS.isNegative() ? RHS.countMinLeadingOnes() : RHS.countMinLeadingZeros();
+  if (LHS.isNegative())
+    Known.One.setHighBits(std::max(LHS.countMinLeadingOnes(), LeadR));
+  else if (LHS.isNonNegative())
+    Known.Zero.setHighBits(std::max(LHS.countMinLeadingZeros(), LeadR));
   return Known;
 }
 
diff --git a/llvm/test/Analysis/ValueTracking/knownbits-rem-lowbits.ll b/llvm/test/Analysis/ValueTracking/knownbits-rem.ll
similarity index 89%
rename from llvm/test/Analysis/ValueTracking/knownbits-rem-lowbits.ll
rename to llvm/test/Analysis/ValueTracking/knownbits-rem.ll
index 0521c7130055fe..4f60c41c581323 100644
--- a/llvm/test/Analysis/ValueTracking/knownbits-rem-lowbits.ll
+++ b/llvm/test/Analysis/ValueTracking/knownbits-rem.ll
@@ -12,6 +12,17 @@ define i8 @urem_low_bits_know(i8 %xx, i8 %yy) {
   ret i8 %r
 }
 
+define i8 @urem_high_bits_know(i8 %xx, i8 %yy) {
+; CHECK-LABEL: @urem_high_bits_know(
+; CHECK-NEXT:    ret i8 0
+;
+  %x = and i8 %xx, 2
+  %y = and i8 %yy, -4
+  %rem = urem i8 %x, %y
+  %r = and i8 %rem, 8
+  ret i8 %r
+}
+
 define i8 @urem_low_bits_know2(i8 %xx, i8 %yy) {
 ; CHECK-LABEL: @urem_low_bits_know2(
 ; CHECK-NEXT:    ret i8 2
@@ -80,6 +91,17 @@ define i8 @srem_low_bits_know(i8 %xx, i8 %yy) {
   ret i8 %r
 }
 
+define i8 @srem_high_bits_know(i8 %xx, i8 %yy) {
+; CHECK-LABEL: @srem_high_bits_know(
+; CHECK-NEXT:    ret i8 8
+;
+  %x = or i8 %xx, -2
+  %y = and i8 %yy, -4
+  %rem = srem i8 %x, %y
+  %r = and i8 %rem, 8
+  ret i8 %r
+}
+
 define i8 @srem_low_bits_know2(i8 %xx, i8 %yy) {
 ; CHECK-LABEL: @srem_low_bits_know2(
 ; CHECK-NEXT:    ret i8 1

[artagnon]

Sorry, this patch is incorrect: KnownBitsTest should not fail. Investigating.

[dtcxzyw]

Alive2 proof: https://alive2.llvm.org/ce/z/WcDkSX

Please provide a generic proof:
https://llvm.org/docs/InstCombineContributorGuide.html#use-generic-values-in-proofs

[artagnon]

Quick question: is this Alive2 proof correct or is there a bug in Alive2? If there is no bug in Alive2, there's something wrong with my implementation, which I will work on.

https://alive2.llvm.org/ce/z/UMaBDK

[RKSimon]

I'm not sure if you can use assume in the tgt for verification, maybe try something like this: https://alive2.llvm.org/ce/z/Ugh-Dq

[artagnon]

I'm not sure if you can use assume in the tgt for verification, maybe try something like this: https://alive2.llvm.org/ce/z/Ugh-Dq

Thanks, the modified proof is indeed correct, and the fix in the code was easy :)

[jayfoad]

I think the patch is OK as written but it is strange that you only handle the cases where LHS and RHS are both positive or both negative. What about a case like LHS % 3 where LHS is known to be negative? The inline suggestions try to handle those cases too - but would need extra test coverage.

[artagnon]

@jayfoad Thanks for the extra improvement! I've now added additional tests, and the patch should be ready.

[artagnon]

Alive2 proof: https://alive2.llvm.org/ce/z/Ugh-Dq

I haven't run tests locally, so relying on CI for latest change. In the meantime, do we have any opinions on whether this Alive2 proof is useful to include with the implementation?

[nikic]

LGTM