[Mlir-commits] [mlir] [mlir][arith] doc updates for ub semantics, and int representations (PR #72932)

[Jakub Kuderski]

================
@@ -198,7 +198,9 @@ def Arith_AddIOp : Arith_TotalIntBinaryOp<"addi", [Commutative]> {
     The `addi` operation takes two operands and returns one result, each of
     these is required to be the same type. This type may be an integer scalar
     type, a vector whose element type is integer, or a tensor of integers. It
-    has no standard attributes.
+    has no standard attributes. If an overflow occurs, the result is the 
+    mathematical value of the addition modulo 2^n, where `n` is the width of
+    the integer type. 
----------------
kuhar wrote:

> > It's been implicitly defined through all the lowering paths and existing transforms that depend on it. This just documents the state of the world.
> 
> I don't think so

There are 2 main lowering paths:
- LLVM: https://github.com/llvm/llvm-project/blob/e07fec10ac208c2868a24c5c0be88e45778b297e/mlir/lib/Conversion/ArithToLLVM/ArithToLLVM.cpp#L37 and details in https://github.com/llvm/llvm-project/blob/e07fec10ac208c2868a24c5c0be88e45778b297e/mlir/lib/Conversion/LLVMCommon/Pattern.cpp#L335. This lowers to `llvm.add` without `nsw`/`nu` with well-defined overflow: https://llvm.org/docs/LangRef.html#id89.
- SPIR-V: https://github.com/llvm/llvm-project/blob/main/mlir/lib/Conversion/ArithToSPIRV/ArithToSPIRV.cpp#L1157. This lowers to `OpIAdd` with well-defined overflow: https://registry.khronos.org/SPIR-V/specs/unified1/SPIRV.html#_arithmetic_instructions.

As for existing transforms that rely on this, we do have existing code that assumes the overflow behavior, just a couple of examples:
- https://github.com/llvm/llvm-project/blob/main/mlir/lib/Dialect/Arith/Transforms/EmulateWideInt.cpp
- https://github.com/llvm/llvm-project/blob/1dd387e10624ece478759ec95c18545d051b7dbe/mlir/lib/Dialect/Arith/IR/ArithCanonicalization.td#L91

I think we both aggrege that the state of the world is the arith semantics being under-defined or defined implicitly via usage: lowering and transforms. (I started a discussion on this last year and I believe there's a community-wide consensus on this: https://discourse.llvm.org/t/rfc-define-precise-arith-semantics/65507.) If overflow was *already* implementation-defined or undefined, I would expect us to have code that actively avoids creating overflows -- I'm not aware of any, but I don't claim to know all of mlir so please point me to it does.

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