John Regehr

Do note I'm not being adversarial when I say I don't have to give examples since it uses a known-good technique. The status quo for compilers is they have plenty of bugs. The number of bugs go up like most software with the complexity (eg lines of code or paths). Highly-optimizing compilers should be expected to have more bugs than barely optimizing ones. Evidence on application of formal methods in industry showed the programs had way fewer bugs. Cleanroom and Praxis Correct by Construction w/ SPARK Ada regularly hit some of lowest defect rates in existence.

http://infohost.nmt.edu/~al/cseet-paper.html

http://www.anthonyhall.org/c_by_c_secure_system.pdf

So, we have one trend saying complicated software will have lots of errors with another saying verified software will have fewer errors. The hypothesis we should have at that point is a verified compiler will have either few errors in general (optimism) or much fewer than non-formally-verified compilers (pessimism). The empirical evidence confirms this with bug trackers on most compilers but especially the Csmith testing pitting CompCert against other C compilers:

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

https://embed.cs.utah.edu/csmith/

It was the first time (IIRC) a program was custom designed to toss computer-years worth of input against compilers to find problems. Found hundreds in common compilers despite them being analyzed and used so much that many bugs were already found. When they applied it…

First of all: fantastic article. In-depth, insightful, and the examples are absolutely top-notch. On the razor's edge between accessible and profound. Hats off to the author.

I will say that the problems seem to lie in a few interesting interlanguage quirks, and not so much on language specs. For example, LLVM and C have different definitions of "undefined behavior"[1] -- this is pointed out when looking at the `poison` identifier. In LLVM this might just be a weird side-effect we don't care about, but actually having an integer overflow is a big deal in C that introduces UB. Given the introduction, LLVM (incorrectly) introduces (C) UB at times.

The second section, on pointer provenance, is much trickier, as there's no "obvious" UB introduced there. Further, I would argue that pointer provenance is a meta-language (or meta-computational) concept (which the Rust docs hint at), and logically speaking, might be intractable in the general case (I'd have to think about this more). Pointer arithmetic can fiddle with meta-state, whereas IRs like LLVM tend to focus purely on symbol manipulation.

As a side note, I'd be curious what happens when LLVM sees something like: `void *p = &p` which is a self-referential pointer. What does it deduce about it? Does it optimize it away?

Cool thought-provoking article.

[1] https://www.cs.utah.edu/~regehr/llvm-ub.pdf

As others have said, yes, that's mostly the case.

Even parsing C and elaborating it to a correctly typed AST is not quite as simple as others are making it out to be, though. Getting all the implicit type conversions correct is not completely trivial, and is a popular source of bugs (see some examples in http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf for instance).

There are also some annoying ambiguities in the grammar and in name resolution rules that mean that sometimes it's not easy to tell whether something is supposed to be a type name or a variable name: https://jhjourdan.mketjh.fr/pdf/jourdan2017simple.pdf

C is a "simple" language in many senses of the word, but it has a lot of complex details. It's fine to gloss over them when writing a compiler for a language very similar to C for learning purposes, but getting everything just right for actual C is tough.

At least a lot of it was due to having to specify around the weird quirks of existing compiler implementations. C has far more undefined behavior than it needs for optimization, and modern programming language theory and compiler research has shown that most undefined behavior isn't really necessary at all. [0] For example, safe Rust has extremely close (and sometimes superior) performance to C, and has almost* no undefined behavior at all. [1]

[0] https://www.cs.utah.edu/~regehr/papers/undef-pldi17.pdf

[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/fastest/gcc-rust.html

* Some is inherited from LLVM, some is bugs, some is dumb corner cases like using kernel syscalls to overwrite the program's own memory with random bits.

Interesting that there was only one compiler that was immune to a wide class of bugs they found everywhere else:

"The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users."
http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

> I'm not sure how C is specifically to blame for something like int overflow

C is not a good choice when safety is paramount.

"The low-level nature of C and C++ means that bit- and byte-level manipulation of objects is commonplace; the line between mathematical and bit-level operations can often be quite blurry. Wraparound behavior using unsigned integers is legal and well-defined, and there are code idioms that deliberately use it. On the other hand, C and C++ have undefined semantics for signed overflow and shift past bitwidth: operations that are perfectly well-defined in other languages such as Java."

http://www.cs.utah.edu/~regehr/papers/overflow12.pdf