Humans are typically not very good at reasoning about integers with limited range, whereas computers fundamentally work with limited-range numbers. This impedance mismatch has been the source of a lot of bugs over the last 50 years. The solution comes in multiple parts.
In most programming languages, the default integer type should be a bignum: an arbitrary-precision integer that allocates more space when needed. Efficient bignum libraries exist and most integers never end up needing more than one machine word anyway, except in domains like crypto. As far as I’m concerned, for ~95% of programming tasks integer overflow is a solved problem: it should never happen. The solution isn’t yet implemented widely enough, but happily there are plenty of languages such as Python that give bignums by default.
When performance and/or predictability is a major consideration, bignums won’t work and we’re stuck with fixed-width integers that wrap, trap, saturate, or trigger undefined behavior upon overflow. Saturation is a niche solution that we won’t discuss further. Undefined behavior is bad but at least it enables a few loop optimizations and also permits trapping implementations. Although wrapping is an extremely poor default, there are a few good things to say about it: wrapping is efficient, people have come to expect it, and it is a good match for a handful of application domains.
Swift is a modern programming language that traps instead of providing bignums, this is also a generally sensible behavior. Why not bignums? The About Swift web page says that Swift gives “the developer the control needed in a true systems programming language,” so perhaps the designers were worried about unpredictable allocations. I’d love to see a study of the performance of best-of-breed trapping and bignum implementations on important modern applications.
The Rust developers have adopted a hybrid solution where integer overflows trap in debug builds and wrap in optimized builds. This is pragmatic, especially since integer overflows do not compromise Rust’s memory safety guarantees. On the other hand, perhaps as MIR matures, Rust will gravitate towards checking in optimized builds.
For safety-critical programs, the solution to integer overflow is to prove that it cannot happen using some combination of manual reasoning, testing, and formal verification. SPARK Ada and the TrustInSoft analyzer are suitable for proving that integer overflows won’t occur. More work is needed to make this sort of verification scalable and less expert-intensive.
Systems programming tasks, such as building operating systems, language runtimes, and web browsers, are caught in the middle. Wrapping sucks, bignums and trapping are slow or at least perceived as slow (and you do not want to trap or allocate while handling a hardware interrupt anyway), and the codes are too large for formal verification and thorough testing. One answer is to work hard on making trapping fast. For example, Swift has a high-level optimization pass specifically for removing integer overflow checks, and then the LLVM optimization passes do more of this, and then the LLVM backends can lower checked math operations to efficient condition code checks, and then modern Intel processors fuse the resulting branch-on-overflow instructions away.
In summary, bignums should be the default whenever this is feasible, and trapping on overflow should be the backup default behavior. Continued work on the compilers and processors will ensure that the overhead of trapping overflow checks is down in the noise. Java-style wrapping integers should never be the default, this is arguably even worse than C and C++’s UB-on-overflow which at least permits an implementation to trap. In domains where wrapping, trapping, and allocation are all unacceptable, we need to be able to prove that overflow does not occur.
I’ll end up with a few random observations:
- Dan Luu wrote a piece on the overhead of overflow checking.
- Arbitrary (fixed) width bitvectors are a handy datatype and I wish more languages supported them. These can overflow but it’s not as big of a deal since we choose the number of bits.
- Explicitly ranged integers as seen in Ada are also very nice, there’s no reason that traps should only occur at the 32-bit or 64-bit boundaries.
- The formal verification community ignored integer overflow for far too long, there’s a long history of assuming that program integers behave like mathematical integers. Things are finally better though.
UPDATE: I didn’t want this piece to be about C and C++ but I should have clarified that it is only signed overflow in these languages that is undefined behavior; unsigned overflow is defined to be two’s complement wraparound. While it is possible to trap on unsigned overflow — UBSan has a flag that turns on these traps — this behavior does not conform to the standards. Even so, trapping unsigned wraparounds can — in some circumstances — be useful for finding software defects. The question is whether the wraparound was intentional or not.
12 responses to “Solutions to Integer Overflow”
Another advantage of seamless conversion to bignums: writing random compiler test generators (and test simplifiers) becomes easier. I wrote a simpleminded generator/simplifier for Common Lisp and it was extremely rare for a bignum to be generated that was so large it couldn’t be handled.
If the generator had added DECLARE forms with integer subranges things would have been harder, of course.
There is another advantage to having a Ada-style type system that allows explicitly ranged integer subtypes: they often allow traps to be omitted entirely without compromising safety, particularly for intermediate results. As a simple example, if a ranged integer type is being used to index an array it may be easy for the compiler to determine that incrementing or decrementing a valid index always results in a value that might not be a valid index but will always fit in the underlying machine type without wrap-around. The compiler can use this fact to justify omitting traps when generating the code for some loops.
I don’t know what a “true systems programming language” is, but in the era after Lisp operating systems, I’m pretty sure it’s just an excuse to omit useful features that people want.
Where can we read a bit more about trapping?
As far as I can gather, the Haskell Integer type uses the native machine integer size (32 or 64 bit) when the represented number fits in that, and switches to a custom bignum implementation only when this would overflow.
Of course, that means entirely unpredictable runtime characteristics. But it’s either that or restricting ourselves to only the types that CPU instructions can handle. If Apple had better tech knowledge, they would easily be able to build a runtime system for Swift with reasonable real-time characteristics, without restricting users of the language to hardware -defined types.
But I mean… if the integer you’re using is about to overflow, would you rather have an exception or a decrease in performance? There’s just no comparison.
Undefined behavior enables loop optimizations?
I’m skeptical. I’ve looked at examples of loop optimizations which were purportedly “made possible” by the undefined-ness of signed overflow when in fact it turns out that a single check OUTSIDE of the loop would would validate the assumption that UB allows them to make. I suspect that if there is any observable performance penalty that comes along with “-fwrapv”, it’s simply an artifact of compiler implementation choices, not because -fwrapv makes some loop optimizations inherently impossible.
I have seen cases where UB-driven optimization eliminates bounds checks, and one could call that an optimization, but I think we can agree that such optimizations are not good things.
On a related note, I see (in various places) other types of undefined behavior in C being defended as helpful for portability or performance reasons, when in fact the cited shortcuts or optimizations would be allowed by a more intuitive, less surprising and less unforgiving language design choice. For example, C could say that an oversized shift amount will result in a number whose value is undefined. There is no justification for the standard to allow shift or addition operations to do worse (e.g. corrupt memory). Yet this notion has stanch support. Why?
Clearly, there are forces of evil at work here. 🙂
Pedro, can you be more specific?
Brian, I don’t think the issue of undefined behavior and loop optimizations has been studied deeply, but certainly there are a lot of opinions out there. I’m happy to believe there are cases where UB provides measurable performance increases, and I’m also happy to do without those optimizations.
Hi John, I’d be curious to know what improvements you’d like to see for formal verification with SPARK to be “scalable and less expert-intensive”. From our own experience with both industrial and academic users, these do not seem to be problematic, at least not as much as the main (usual) issue of adopting a new programming language or a new development environment. (I am the product manager of SPARK at AdaCore.)
Do you know any CPU that would be able to trap on integer overflow ? No compromise between speed and security would be needed.
For what it’s worth I think the default behaviour should be to trap in debug builds, with undefined behaviour in optimised builds. C++ should also give the programmer what she needs (trapping, wrapping, saturating, etc). Don’t forget there are complications with GPGPUs.
There’s no bignum in the C++ standard library, and I’m really interested to see if there’s some constexpr magic that can be done in the new-fangled C++11/14/17 that will be able to make a compile-time representation of something like std::bigint big{“1234567891011121314151617181920”};
Hi Yannick, I only have a little experience with SPARK and this was a while ago, if I have a chance to use it again and I’d love to give some more specific feedback.
Emmanuel, MIPS had (has) support for trap on integer overflow, and I think Alpha too. I love this feature, and maybe it will come back sometime in the future. But in the meantime Intel’s fused jo seems just fine too.