-
Undefined Behavior Executed by Coq
I built a version of OCaml with some instrumentation for reporting errors in using the C language’s integers. Then I used that OCaml to build the Coq proof assistant. Here’s what happens when we start Coq: [regehr@gamow ~]$ ~/z/coq/bin/coqtop intern.c:617:10: runtime error: left shift of 255 by 56 places cannot be represented in type ‘intnat’…
-
It’s Time to Get Serious About Exploiting Undefined Behavior
[Note: I promise, this is almost my last post about undefined behavior for a while. Maybe just one more in the queue.] The current crop of C and C++ compilers will exploit undefined behaviors to generate efficient code (lots of examples here and here), but not consistently or well. It’s time for us to take this…
-
Undefined Behavior Consequences Contest Winners
The contest that I posted the other day received some very nice entries. I decided to pick multiple winners since the best entries illustrate consequences of several kinds of undefined behavior. First, here’s the runner up, submitted by Octoploid: This program is undefined by C99, where signed left shifts must not push a 1 bit…
-
Contest: Craziest Compiler Output due to Undefined Behavior
[UPDATE: Winners are here.] The C and C++ standards fail to assign a meaning to a program that overflows a signed integer or performs any of the 190+ other kinds of undefined behavior. In principle, a conforming compiler can turn such a program into a binary that posts lewd messages to Twitter and then formats…
-
When is Undefined Behavior OK?
Under what circumstances is it acceptable for a programming language to admit undefined behaviors? Here I mean undefined behavior in the C/C++ sense where, for example, “anything can happen” when you use an uninitialized variable. In my opinion, five conditions need to be fulfilled. First, the undefined behavior must provide a significant, robust performance win.…
-
Academic Attention for Undefined Behavior
Undefined behaviors are like blind spots in a programming language; they are areas where the specification imposes no requirements. In other words, if you write code that executes an operation whose behavior is undefined, the language implementation can do anything it likes. In practice, a few specific undefined behaviors in C and C++ (buffer overflows and…
-
Finding Integer Undefined Behaviors Using Clang 2.9
My student Peng Li modified Clang to detect integer-related undefined behaviors in C and C++ code. We’ve released the code here, to go along with the recent LLVM 2.9 release. This checker has found problems in PHP, Perl, Python, Firefox, SQLite, PostgreSQL, BIND, GMP, GCC, LLVM, and quite a few other projects I can’t think…
-
Better Testing With Undefined Behavior Coverage
[The bit puzzle results are based on data from Chad Brubaker and the saturating operation results are based on data from Peng Li. They are respectively an undergrad and a grad student in Utah’s CS program.] Klee is a tool that attempts to generate a collection of test cases inducing path coverage on a system…
-
Undefined Integer Behaviors in Student Code, Part 2
[This post is based on data gathered by my student Peng Li. He also wrote the undefined behavior checker.] The other day I posted about undefined integer behaviors in code written by students in a class I used to teach. This post is more of the same, this time from CS 5785, my advanced embedded…
-
Undefined Integer Behaviors in Student Code, Part 1
[This post is based on material from Chad Brubaker, a really smart CS undergrad at Utah who did all the work getting these data. The integer undefined behavior checker was created by my student Peng Li.] Integer undefined behaviors in C/C++, such as INT_MAX+1 or 1<<-1, create interesting opportunities for compiler optimizations and they also…