[Mlir-commits] [mlir] [mlir] [arith] Fix ceildivsi lowering in arith-expand (PR #133774)

[Fehr Mathieu]

math-fehr wrote:

I would be really happy to figure out a way to properly test it, as it's really easy to get it wrong.
The problem I see with integration tests is that here we want to check that we don't trigger poison or UB, and AFAIK that's impossible to do without an interpreter that has an explicit poison/UB. Same with sympy, as it doesn't define UB or poison at all.

The way I checked the correctness of this (and found the bug) was by using my SMT tool, but it relies on my own implementation of ceildivsi in SMT-LIB, so it has the exact same problem.

I thought about trying to use Alive2 in LLVM to prove that correctly, but LLVM doesn't define ceildivsi, so that's not really possible :/

What I can easily do is add integration test for some values that do not trigger poison/UB if you want, but I'm just not sure how to proceed with poison/UB.

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