-
Partial Evaluation and Immutable Servers
Although I haven’t figured out exactly what immutability means for a server (I’m probably just being picky) the general idea of rebuilding a system from spec rather than evolving it with one-off hacks is very appealing. Lately I’ve been thinking about what could be accomplished if the system compiler were able to take advantage of…
-
Proposal for a Friendly Dialect of C
[This post is jointly authored by Pascal Cuoq, Matthew Flatt, and John Regehr.] In this post, we will assume that you are comfortable with the material in all three parts of John’s undefined behavior writeup and also with all three parts of Chris Lattner’s writeup about undefined behavior. Additionally, this paper is excellent background reading.…
-
Non-Transparent Memory Safety
[This paper contains more detail about the work described in this post.] Instrumenting C/C++ programs to trap memory safety bugs is a popular and important research topic. In general, a memory safety solution has three goals: efficiency, transparency, and compatibility. Efficiency is obvious. Transparency means that we can turn on memory safety with a switch,…
-
ALIVe: Automatic LLVM InstCombine Verifier
[This post was jointly written by Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr.] A modern compiler is a big, complex machine that contains a lot of moving parts, including many different kinds of optimizations. One important class of optimization is peephole optimizations, each of which translates a short sequence of instructions into a…
-
Finding Compiler Bugs by Removing Dead Code
I was pretty bummed to miss PLDI this year, it has been my favorite conference recently. One of the talks I was most interested in seeing was Compiler Validation via Equivalence Modulo Inputs by some folks at UC Davis. Although I had been aware of this paper (which I’ll call “the EMI paper” from now…
-
Early Superoptimizer Results
[Here’s a shortcut to the results. But it would be best to read the post first.] Following my previous superoptimizer post, my student Jubi and I were getting up to speed on the prerequisites — SMT solvers, LLVM internals, etc. — when Googler Peter Collingbourne contacted me saying that he had recently gotten a superoptimizer…
-
This Is Not a Defect
In several previous blog entries I’ve mentioned that in some recent versions of C and C++, left-shifting a 1 bit into the high-order bit of a signed integer is an undefined behavior. In other words, if you have code that computes INT_MIN by evaluating 1
-
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…
-
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…
-
Let’s Work on an LLVM Superoptimizer
A compiler optimization has two basic parts. First, it needs to recognize an optimizable situation in the IR (intermediate representation), such as adjacent increments of the same variable. For the optimization to be maximally effective, the situation recognizer should cast as wide a net as possible. For example, we might broaden the applicability of an…