Skip to content

{ Category Archives } Computer Science

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 […]

Research Advice from Alan Adler

Although I am a happy French press user, I enjoyed reading an article about Alan Adler and the AeroPress that showed up recently on Hacker News. In particular, I love Adler’s advice to inventors: Learn all you can about the science behind your invention. Scrupulously study the existing state of your idea by looking at […]

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, […]

Xv6

I’m teaching a small Advanced Operating Systems course this spring. Preparing for the course over winter break, I spent some time reading various Linux subsystems such as the scheduler, and was a bit shocked at how complex it has become. I’ve been using Linux, looking at its code, and occasionally hacking it for more than […]

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 […]

That Was Easy

I wanted to play around with the Python interface to Z3 and the classic SEND + MORE = MONEY puzzle seemed like a good way to get started. This turned out to be so easy that my code worked almost on the first try: Then: $ python ./send_more_money.py sat D = 7 S = 9 […]

Reproducibility in Computer Systems Research

These results about reproducibility in CS have been the subject of lively discussion at Facebook and G+ lately. The question is, for 613 papers, can the associated software be located, compiled, and run? In contrast with something I often worry about — producing good software — the bar here is low, since even a system […]

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 […]

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 […]