-
How Should You Write a Fast Integer Overflow Check?
Detecting integer overflow in languages that have wraparound semantics (or, worse, undefined behavior on overflow, as in C/C++) is a pain. The issue is that programming languages do not provide access to the hardware overflow flag that is set as a side effect of most ALU instructions. With the condition codes hidden, overflow checks become…
-
Testing with Small Capacities
The goal of testing is to expose bugs. To find a bug we must drive the software under test into a part of its state space where the bug becomes evident, for example by causing a crash. Many bugs lurk in dark corners of the state space that are ordinarily difficult to reach. This piece…
-
Find the Integer Bug
Not all of the functions below are correct. The first person to leave a comment containing a minimal fix to a legitimate bug will get a small prize. I’m posting this not because the bug is particularly subtle or interesting but rather because I wrote this code for a piece about integer overflow and thought…
-
A New Development for Coverity and Heartbleed
As a consequence of my last post, I spent some time on the phone Friday with Andy Chou, Coverity’s CTO and former member of Dawson Engler’s research group at Stanford, from which Coverity spun off over a decade ago. Andy confirmed that Coverity does not spot the heartbleed flaw and said that it remained stubborn…
-
Heartbleed and Static Analysis
Today in my Writing Solid Code class we went through some of the 151 defects that Coverity Scan reports for OpenSSL. I can’t link to these results but take my word for it that they are a pleasure to read — the interface clearly explains each flaw and the reasoning that leads up to it,…
-
Automated Reasoning About LLVM Optimizations and Undefined Behavior
Following up on last week’s toy use of Z3 and my LLVM superoptimizer post from a few weeks ago, I wanted to try to prove things about optimizations that involve undefined behavior. We’ll be working with the following example: Clang’s -O0 output for this code is cluttered but after running mem2reg we get a nice…
-
Writing Solid Code Weeks 7 and 8
The students continued with their compressor/decompressor development. Coverity continued to find plenty of issues for the students to fix. I’m about to start doing a bit of differential testing of their code, using voting to determine who is correct and who is wrong. I lectured on paranoid programming and on building a fuzzer, for sort…
-
Paranoid Programming
A lot of software defects stem from developers who lack a proper sense of paranoia. While paranoia can of course be taken to idiotic extremes, a healthy respect for Murphy’s Law is useful in programming. This post is a list of useful paranoid techniques that I hope to use as the basis for a lecture…
-
Writing Solid Code Weeks 5 and 6 — The Plot Thickens
Last week was pretty relaxed, I lectured on doing code reviews — pretty much the standard pitch. This week we spent Tuesday doing a code review, I think it went pretty well. I had chosen a team whose code was strong so that our first code review would be a positive one. Today I announced…
-
Assertions Are Pessimistic, Assumptions Are Optimistic
We assert a condition when we believe it to be true in every non-buggy execution of our program, but we want to be notified if this isn’t the case. In contrast, we assume a condition when our belief in its truth is so strong that we don’t care what happens if it is ever false.…