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 - 2k < y - (2k - 1 - x)
- x + y - 2k < y - 2k + 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.
