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: […]
Category Archives: Software Correctness
Isolating a Free-Range Miscompilation
If we say that a compiler is buggy, we need to be able to back up that claim with reproducible, compelling, and understandable evidence. Usually, this evidence centers on a test case that triggers the buggy behavior; we’ll say something like “given this test case, compiler A produces an executable that prints 0 whereas compiler […]
A Month of Invalid GCC Bug Reports, and How to Eliminate Some of Them
During July 2016 the GCC developers marked 38 bug reports as INVALID. Here’s the full list. They fall into these (subjective) categories: 8 bug reports stemmed from undefined behavior in the test case (71753, 71780, 71803, 71813, 71885, 71955, 71957, 71746) 1 bug report was complaining about UB exploitation in general (71892) 15 bug reports […]
C-Reduce 2.5
In May we released C-Reduce 2.5 which builds against LLVM/Clang 3.8. New in this release: Improved reduction of non-preprocessed C/C++ code. C-Reduce now includes #included files that are below a certain size and also uses unifdef to remove #ifdef/#endif pairs. Specialization of #define directives is not implemented yet. Support for reducing multiple files at once. […]
Pointer Overflow Checking
Most programming languages have a lot of restrictions on the kinds of pointers that programs can create. C and C++ are unusually permissive in this respect: pointers to arbitrary objects and subobjects, usually all the way down to bytes, can be constructed. Consequently, most address computations can be expressed either in terms of integer arithmetic […]
Teaching C
The other day Neel Krishnaswami mentioned that he’s going to be teaching the C class at Cambridge in the fall, and asked if I had any advice about that topic. Of course I do! In fact the response got so long that it ended up being a blog post. My main idea is that we […]
Checking Up on Dataflow Analyses
An important tool for reasoning about programs without running them is dataflow analysis, which can be used to compute facts such as: an integer-valued variable is non-negative at a particular program point a conditional branch always goes one way an indirect write cannot modify a particular array Dataflow facts drive optimizations such as constant propagation […]
Efficient Integer Overflow Checking in LLVM
(Here’s some optional background reading material.) We want fast integer overflow checking. Why? First, if the undefined behavior sanitizers go faster then testing goes faster. Second, when overhead drops below a certain point people will become willing to use UBSan to harden production code against integer overflows. This is already being done in parts of […]
SQLite with a Fine-Toothed Comb
One of the things I’ve been doing at Trust-in-Soft is looking for defects in open-source software. The program I’ve spent the most time with is SQLite: an extremely widely deployed lightweight database. At ~113 KSLOC of pointer-intensive code, SQLite is too big for easy static verification. On the other hand, it has an incredibly impressive […]
The Strict Aliasing Situation is Pretty Bad
I’ll start with a quick review of the strict aliasing rules in C and C++ and then present some less well-known material. Strict Aliasing Compiler optimizations are often shot down by the potential for pointers to be aliases. For example, although we might naively expect a compiler to optimize this function to return zero, that […]