Ping.
To put it shortly, I'm not sure how to differentiate between:
example range of a: [3,3]
(ulong)(a + UINT_MAX) + 1 --> (ulong)(a) + (ulong)(-1 + 1), sign extend
example range of a: [0,0]
(ulong)(a + UINT_MAX) + 1 --> (ulong)(a) + (ulong)(UINT_MAX + 1), no
sign extend
In this case, there is an "ok" overflow in the first example's range and
no overflow in the second, but I don't think this suffices as criterion.
As said, your proposed canonicalization (" unsigned X plus CST to
unsigned X minus CST' if CST' has a smaller absolute value than CST)
might help here, but I'm unsure how to do it currently.
