llvm-project

History

Valeriy Savchenko 9d6f011333

[VectorCombine] Fold vector.reduce.OP(F(X)) == 0 -> OP(X) == 0 (#173069 )

This commit introduces a pattern to do the following fold:

  vector.reduce.OP f(X_i) == 0 -> vector.reduce.OP X_i == 0

In order to decide on this fold, we use the following properties:

1. OP X_i == 0 <=> \forall i \in [1, N] X_i == 0 1'. OP X_i == 0 <=>
\exists j \in [1, N] X_j == 0
  2.  f(x) == 0 <=> x == 0

From 1 and 2 (or 1' and 2), we can infer that

  OP f(X_i) == 0 <=> OP X_i == 0.

For some of the OP's and f's, we need to have domain constraints on X to
ensure properties 1 (or 1') and 2.

In this change we support the following operations f:

  1. f(x) = shl nuw x, y for arbitrary y
  2. f(x) = mul nuw x, c for defined c != 0
  3. f(x) = zext x
  4. f(x) = sext x
  5. f(x) = neg x

And the following reductions OP:

  a. OR X_i   - has property 1  for every X
  b. UMAX X_i - has property 1  for every X
  c. UMIN X_i - has property 1' for every X
  d. SMAX X_i - has property 1  for X >= 0
  e. SMIN X_i - has property 1' for X >= 0
  f. ADD X_i  - has property 1  for X >= 0 && ADD X_i doesn't sign wrap

The matrix of Alive2 proofs for every pair of {f,OP}:
  | OP\f | zext | sext | neg | mul | shl |
  |------|------|------|-----|-----|-----|
| or | [proof](https://alive2.llvm.org/ce/z/EqHAPd) |
[proof](https://alive2.llvm.org/ce/z/DS3eP2) |
[proof](https://alive2.llvm.org/ce/z/65A5x9) |
[proof](https://alive2.llvm.org/ce/z/TVPpUf) |
[proof](https://alive2.llvm.org/ce/z/kj--vH) |
| umin | [proof](https://alive2.llvm.org/ce/z/AK39LL) |
[proof](https://alive2.llvm.org/ce/z/xEPH2S) |
[proof](https://alive2.llvm.org/ce/z/N-ubNr) |
[proof](https://alive2.llvm.org/ce/z/dgUEH4) |
[proof](https://alive2.llvm.org/ce/z/2TUNDu) |
| umax | [proof](https://alive2.llvm.org/ce/z/Cy_DJS) |
[proof](https://alive2.llvm.org/ce/z/f42bGQ) |
[proof](https://alive2.llvm.org/ce/z/ReUx4M) |
[proof](https://alive2.llvm.org/ce/z/qSsvdG) |
[proof](https://alive2.llvm.org/ce/z/cE3Qgw) |
| smin | [proof](https://alive2.llvm.org/ce/z/j5TwTA) |
[proof](https://alive2.llvm.org/ce/z/DhNxPQ) | — |
[proof](https://alive2.llvm.org/ce/z/m03AOt) |
[proof](https://alive2.llvm.org/ce/z/bp58Q3) |
| smax | [proof](https://alive2.llvm.org/ce/z/3zmbRn) |
[proof](https://alive2.llvm.org/ce/z/6FTfRJ) | — |
[proof](https://alive2.llvm.org/ce/z/KDfKEW) |
[proof](https://alive2.llvm.org/ce/z/dajm7T) |
| add | [proof](https://alive2.llvm.org/ce/z/3kt7BB) |
[proof](https://alive2.llvm.org/ce/z/cyqzQH) | — |
[proof](https://alive2.llvm.org/ce/z/n_oGjT) |
[proof](https://alive2.llvm.org/ce/z/67bkJm) |

Proofs for known bits:
* Leading zeros - [4vi32](https://alive2.llvm.org/ce/z/w--S2D),
[16vi8](https://alive2.llvm.org/ce/z/hEdVks)
* Leading ones - [4vi16](https://alive2.llvm.org/ce/z/RyPdBS),
[v16i8](https://alive2.llvm.org/ce/z/UTFFt9)