[Mlir-commits] [mlir] [mlir][arith] Fold trivial integer division and remainder (PR #212074)

[Victor Perez]

victor-eds wrote:

@Hardcode84 @kuhar 

> Folding `div(x, 0) -> poison` may be more profitable, but then we have an ordering problem between `div(x, x)` and `div(x, 0)` foldings. Can you check alive2 and llvm proper if 1. poison folding is actually allowed, 2. how they handle ordering.

Good point. [Here's the LLVM equivalent patterns](https://godbolt.org/z/dzTjYjs4e). LLVM *does* apply the `div(x, 0) -> poison` transformation you mention, and it in fact applies it with higher priority than the ones I am proposing here. Note I didn't originally add `div(x, 0) -> poison` as that would require adding a dependency with the UB dialect. I can do it if we agree that's reasonable.

Also, as requested: Alive2 verification (all report "Transformation seems to be correct!"):

| Fold | `udiv` | `sdiv` | `urem` | `srem` |
| :--- | :---: | :---: | :---: | :---: |
| `X / 0` -> `poison` | [Correct](https://alive2.llvm.org/ce/z/AyT9Rz) | [Correct](https://alive2.llvm.org/ce/z/-AevcK) | [Correct](https://alive2.llvm.org/ce/z/VLDE5N) | [Correct](https://alive2.llvm.org/ce/z/APvEKa) |
| `X / X` -> `1` / `0` | [Correct](https://alive2.llvm.org/ce/z/YjZCEA) | [Correct](https://alive2.llvm.org/ce/z/BSWQrm) | [Correct](https://alive2.llvm.org/ce/z/gx5sRH) | [Correct](https://alive2.llvm.org/ce/z/VUYkr4) |
| `0 / X` -> `0` | [Correct](https://alive2.llvm.org/ce/z/keqeCZ) | [Correct](https://alive2.llvm.org/ce/z/jyf5wm) | [Correct](https://alive2.llvm.org/ce/z/fZa6ND) | [Correct](https://alive2.llvm.org/ce/z/fo6ss8) |

And the ordering overlap, [udiv 0, 0 -> poison](https://alive2.llvm.org/ce/z/AEW4ms).

I'll add these tests to the commit message/PR when we agree on the extent of the changes.


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