[llvm] [ValueTracking] Support horizontal vector add in computeKnownBits (PR #174410)

[Valeriy Savchenko via llvm-commits]

================
@@ -601,6 +601,46 @@ KnownBits KnownBits::abs(bool IntMinIsPoison) const {
   return KnownAbs;
 }
 
+KnownBits KnownBits::reduceAdd(unsigned NumElts) const {
+  if (NumElts == 0)
+    return KnownBits(getBitWidth());
+
+  unsigned BitWidth = getBitWidth();
+  KnownBits Result(BitWidth);
+
+  if (isConstant())
+    // If all elements are the same constant, we can simply compute it
+    return KnownBits::makeConstant(NumElts * getConstant());
+
+  // The main idea is as follows.
+  //
+  // If KnownBits for each element has L leading zeros then
+  // X_i < 2^(W - L) for every i from [1, N].
+  //
+  //   ADD X_i <= ADD max(X_i) = N * max(X_i)
+  //           <  N * 2^(W - L)
+  //           <  2^(W - L + ceil(log2(N)))
+  //
+  // As the result, we can conclude that
+  //
+  //   L' = L - ceil(log2(N)) = L - bit_width(N - 1)
+  //
+  // Similar logic can be applied to leading ones.
+  unsigned LostBits = NumElts > 1 ? llvm::bit_width(NumElts - 1) : 0;
+
+  if (isNonNegative()) {
----------------
SavchenkoValeriy wrote:

Re-implementing `KnownBits::mul` logic in Alive2 or SMT is a bit too involved, so I simply implemented this suggestion and checked what does this exhaustive test produce: 

```
/Users/vsavchenko/source/llvm-project/llvm/unittests/Support/KnownBitsTest.cpp:878: Failure
Value of: checkResult("reduceAdd", Exact, Computed, {EltKnown}, false)
  Actual: false (reduceAdd: Inputs = ????, Computed = ???0, Exact = ????)
Expected: true

/Users/vsavchenko/source/llvm-project/llvm/unittests/Support/KnownBitsTest.cpp:878: Failure
Value of: checkResult("reduceAdd", Exact, Computed, {EltKnown}, false)
  Actual: false (reduceAdd: Inputs = ???1, Computed = ??10, Exact = ???0)
Expected: true
...
```

This happens because we jump from $`\sum {X_i} <= \sum max(X_i) = N * max(X_i)`$ so known-bits of the upper-bound are correct when we try to preserve leading zeros and ones, but not in other cases. And even if I take `countMinLeadingZeros`/`countMinLeadingOnes` from `KnownBits::mul`, I still get counter-examples generated by this test.

https://github.com/llvm/llvm-project/pull/174410