Signed integer overflow is UB is problematic

[abadams]

Signed integer overflow for bits >= 32 is undefined behavior in Halide. Therefore, the way the simplifier should work is to assume that there's no overflow in the existing code, and make sure not to introduce new overflow in the code it creates. That's not what it does. Even something as simple as:

(x + c0)*c1 -> x*c1 + c0*c1

can introduce new overflow. Rules like this can't just be deleted, because they're necessary to make sliding window/storage folding proofs work.

This usually isn't a problem for bounds inference, because we don't get close to overflow. But UB-free user code that tries to do integer math on large signed integers can easily be mutated into a form that overflows by the simplifier. There have been several cases of users having to rewrite their code to use UInt for this deeply unsatisfying reason.

A possible (difficult) fix is to give signed integer overflow wrap semantics instead of UB, and add an infinite-precision integer type for indexing and bounds stuff, which is lowered to a fixed bit width type where UB=overflow but we can prove no overflow occurs. Many of the simplifier rules would be disabled for this type, because we need to preserve the no-overflow property.

[steven-johnson]

How hard would it be to add a UBSan-ish mode, in which we wrap all signed integer arithmetic with checks? (This is definitely more of a band-aid than a real fix, but would be useful in sniffing out potential failure sites that haven't failed yet.)