[RFC] Add integer add with carry op to arith

We would like to propose a new op for the arith dialect to support addition with carry:

%sum, %carry = arith.addi_carry %a, %b: i32, i1

The prototype implementation is available at ⚙ D131893 [mlir] Add arith.addi_carry op.

Both the dialects that arith lowers to, LLVM and SPIR-V, already support add-with-carry (llvm.intr.uadd.with.overflow and spv.IAddCarry), so we think it makes sense support it on the level of the arith dialect as well.

The immediate goal is to add support for emulating i64 operations using i32 types for SPIR-V targets that do not support i64 arithmetic e.g., most mobile GPUs. Rather than implementing the emulation entirely in SPIR-V, we would like to do it at the arith dialect level so that the logic can be shared when lowering to LLVM, to support other targets without i64 instructions.

-Jakub and Lei (@antiagainst)

+1. Thanks @kuhar for pushing on this!

+1 on the direction. Having arith-level emulation routines available “out of the box” would be super useful.

What is the intended semantics of this wrt signless integers? llvm.intr.uadd.with.overflow is not the always-legal lowering because it assumes unsigned integers.

Wouldn’t this imply that we name the arith one addui_carry to match?

Yes, if the intended semantics is unsigned.

I didn’t take a deep look at the semantics, just extended your comment with the convention.

The thing I usually do to determine whether an op is signless or not is to ask if there is a signed and unsigned variant vs just one. In this case, I think it is the same for both. Possibly the intrinsic was named in an obscure way (maybe indicating that it only makes sense with unsigned arithmetic in some context but isn’t actually any different)?

It’s been many years since I’ve formulated instructions like this, so an just surmising.

Thanks for bringing this up, @ftynse.

The LLVM intrinsic does have a signed version too: llvm.intr.sadd.with.overflow. The SPIR-V side only has the unsigned variant.

At first it was not immediately obvious to me if signed/unsigned makes a difference, but I checked with Alive and the carry bit can be different between the two: Compiler Explorer.

So I think we need both variants in arith after all.

Yeah, I was expecting the sadd version to signal overflow on, e.g., i8 0x40 + i8 0x40 (carrying out from the 7th bit) and uadd to be fine with it because there is no carrying out of the 8th bit.