Alive2 and missed-optimization bug reports

First, a Ranger update. He is a growing healthy boy, up 50% by weight over the last two weeks.

This week, I want to do a quick writeup of something I tweeted out earlier this week, and explain why I think it’s really cool.

A missed-optimization bug

Earlier this week, my friend Alex Gaynor ran into¹ what looked to be a missed optimization in clang/LLVM, as exhibited by this snippet of C:

  typedef struct {
    uint8_t *data;
    size_t length;
  } slice;

  static inline uint8_t subscript(slice data, size_t index) {
    // After inlining into `check_padding`, this check should be redundant
    if (index >= data.length) { 
      abort();
    }
    return data.data[index];
  }

  bool check_padding(slice data, size_t block_len) {
    if (data.length != block_len || block_len == 0) {       
      return false;
    }
    uint8_t pad_size = subscript(data, block_len - 1);
    return pad_size > 7;
  }

When compiled through clang and LLVM, this example emits two comparisons and conditional jumps in check_padding, even though some simple algebra suggests that the second check should be redundant. One would hope that LLVM would be able to determine the redundancy and delete the second check.

When you run into a situation like this, there are at least two possibilities:

1. The obvious-looking optimization is valid, and this is a real opportunity for LLVM to optimize this code better.
2. The proposed optimization is invalid for some subtle reason. C and LLVM are both notoriously subtle, especially around undefined behavior, and it’s very often the case that an “obviously correct” optimization is actually illegal for some subtle reason.

Historically, if you wanted to report such a bug, your best bet was to think hard and try to convince yourself that there were no odd corner cases that render the optimization invalid, and then to file the bug and wait for some LLVM developers who understand LLVM even better than you do to also think hard and, often, to explain to you the edge case that you hadn’t noticed.

In the case of this bug, Alex and a few others had already looked pretty closely at it and had pretty much convinced themselves we were in case (1). The cases here are fairly straightforward to reason through, and only involve fairly straightforward arithmetic. However, there’s always uncertainty, and even C’s arithmetic operations can be shockingly subtle.

Alive2

When Alex pasted this code into IRC, I remembered reading about a relatively new tool called Alive2, on John Regehr’s blog. Alive2 uses a formal model of LLVM semantics and an SMT solver, and attempts to prove (or disprove) that a proposed piece of LLVM IR is a valid optimization of a different, initial, piece of IR. This is exactly the question we have here: we’d like to prove that the function without the bounds check is a valid optimization of the input. Alive2 knows all about LLVM’s undefined behavior semantics and other corners, so if it approves, we can be confident we aren’t missing anything.

Furthermore, the alive2 collaborators maintain a compiler explorer instance which lets anyone play with it online. Knowing about this tool, I set out to see if we could use it. I compiled Alex’s test case using clang -O3 -emit-llvm into LLVM IR, and cleaned up that IR by hand to remove unnecessary noise. I then manually removed the suspect test and branch, and plugged the resulting two functions into alive2. It did its thing, and reported:

Transformation seems to be correct!

Confirming that removing the branch was a valid optimization! I added the link to the LLVM bug, hopefully bolstering the credibility of our report.

This is cool

Now, in this particular instance, we were already pretty confident in the proposed transformation, after a few engineers looked at it and we experimented with tweaking the input code in a few ways. Alive2 added only marginally to our confidence.

Nonetheless, it was really exciting to me how easy alive2 was to use here, and the fact that we could move — at all — from “we’re pretty sure this works…” to “we have proven this transformation is valid.” As I mentioned, LLVM is notoriously subtle, and being able to substitute a formal semantics and a solver for thinking hard is a huge step forward, and is something I and others can use any other time we run into this kind of situation going forward. I expect it also has the potential to save LLVM developers a lot of trouble triaging bug reports of this sort.

A huge part of this story is that Alive2 exists, not just in a research paper or even as a source dump, but as a drop-in tool on a public web interface. And, furthermore, the authors are continually working on making it support more real programs, so that real programs are increasingly likely to Just Work. It is incredibly rare that a cutting-edge piece of formal methods out of academia is this accessible and useful so soon after its creation, and the team deserves great kudos.