When computing `x + y`, does the sum wrap? There are various ways to find out, some of them well known, some less. Some of these are probably totally unknown, in some cases deservedly so.

This is not meant to be an exhaustive list.

`~x < y`A cute trick in case you don't want to compute the sum, for whatever reason.

Basically a variation of how MISRA C recommends checking for wrapping if you use the precondition test since

`~x = UINT_MAX - x`.`(x + y) < x``(x + y) < y`The Classic™. Useful for being cheap to compute:

`x + y`is often needed anyway, in which case this effectively only costs a comparison. Also recommended by MISRA C, in case you want to express the "has the addition wrapped"-test as a postcondition test.`avg_down(x, y) <s 0``avg_down(x, y) & 0x80000000 // adjust to integer size``<s`is signed-less-than. Performed on unsigned integers here, so be it.`avg_down`is the unsigned average rounded down.`avg_up`is the unsigned average rounded up.Since

`avg_down`is the sum (the full sum, without wrapping) shifted right by 1, what would have been the carry out of the top of the sum becomes the top bit of the average. So, checking the top bit of`avg_down(x, y)`is equivalent to checking the carry out of`x + y`.Can be converted into

`avg_up(~x, ~y) >=s 0`through the equivalence`avg_down(x, y) = ~avg_up(~x, ~y)`.`(x + y) < min(x, y)``(x + y) < max(x, y)``(x + y) < avg(x, y)``(x + y) < (x | y)``(x + y) < (x & y)``~(x | y) < (x & y)`Variants of The Classic™. They all work for essentially the same reason: addition is commutative, including at the bit-level. So if we have

`(x + y) < x`, then we also have`(x + y) < y`, and together they imply that instead of putting`x`or`y`on the right hand side of the comparison, we could arbitrarily select one of them, or anything between them too. Bit-level commutativity takes care of the bottom three variants in a similar way.Wait, is that a signed or unsigned

`min`? Does`avg`round up or down or either way depending on the phase of the moon? It doesn't matter, all of those variants work and more.`(x + y) != addus(x, y)``(x + y) < addus(x, y)``addus`is addition with unsigned saturation, meaning that instead of wrapping the result would be`UINT_MAX`.When are normal addition and addition with unsigned saturation different? Precisely when one wraps and the other saturates. Wrapping addition cannot "wrap all the way back" to

`UINT_MAX`, the highest result*when the addition wraps*is`UINT_MAX + UINT_MAX = UINT_MAX - 1`.When the normal sum and saturating sum are different, the normal sum must be the smaller of the two (it certainly couldn't be greater than

`UINT_MAX`), hence the second variant.`subus(y, ~x) != 0``subus(x, ~y) != 0``addus(~x, ~y) != UINT_MAX``subus`is subtraction with unsigned saturation.Strange variants of

`~x < y`. Since`subus(a, b)`will be zero when`a <= b`, it will be non-zero when`b < a`, therefore`subus(y, ~x) != 0`is equivalent to`~x < y`.`subus(a, b) = ~addus(~a, b)`lets us turn the`subus`variant into the`addus`variant.`(x + y) < subus(y, ~x)`Looks like a cursed hybrid of

`(x + y) < avg(x, y)`and`subus(y, ~x) != 0`, but the mechanism is (at least the way I see it) different from both of them.`subus(y, ~x)`will be zero when`~x >= y`, which is exactly when the sum`x + y`would not wrap.`x + y`certainly cannot be unsigned-less-than zero, so overall the condition`(x + y) < subus(y, ~x)`must be false (which is good, it's supposed to be false when`x + y`would not wrap).In the other case, when

`~x < y`, we know that`x + y`will wrap and`subus(y, ~x)`won't be zero (and therefore cannot saturate). Perhaps there is a nicer way to show what happens, but at least under those conditions (predictable wrapping and no saturation) it is easy to do algebra:`(x + y) < subus(y, ~x)``x + y - 2`^{k}< y - (2^{k}- 1 - x)`x + y - 2`^{k}< y - 2^{k}+ 1 + x`x + y < y + 1 + x``0 < 1`

So the overall condition

`(x + y) < subus(y, ~x)`is true*IFF*`x + y`wraps.`~x < avg_up(~x, y)`Similar to

`~x < y`, but stranger. Averaging`y`with`~x`cannot take a low`y`to above`~x`, nor a high`y`to below`~x`. The direction of rounding is important:`avg_down(~x, y)`could take an`y`that's just one higher than`~x`down to`~x`itself, making it no longer higher than`~x`.`avg_up(~x, y)`cannot do that thanks to rounding up.