Embedded in Academia

Split Vote

In my group’s recent compiler testing paper we wrote:

We have never seen an “interesting” split vote where randomized differential testing of a collection of C compilers fails to produce a clear consensus answer

Randomized differential testing is just a fancy way of describing this process:

  1. Randomly generate a test input
  2. Run it through several different implementations of the same specification
  3. Check if all implementations produced equivalent output

Today we saw our first split vote using a program generated by Csmith. The reduced test case is:

#include <stdio.h>
struct S0 {
  unsigned f1 : 1;
};

struct S0 s;

int main (void) {
  int x = -3;
  int y = x >= (0, s.f1);
  printf ("%d\n", y);
  return 0;
}

GCC, KCC, and CompCert all print “0\n”. MSVC 2010, Intel CC 12.0.2, and today’s development snapshot of Clang (all for x86-64) print “1\n”. All compilers have optimizations turned off. There are two possibilities:

  1. The test case is ill-formed or ambiguous.
  2. Three of the six tools are wrong.

I’m pretty sure that (using the C99 standard) the test case is fine and the correct value for y is 0. The reasoning is that s.f1, an unsigned value, is promoted to signed int before the comparison is performed, making the comparison operator signed, resulting in false, or zero. The type and value of the left operand to the comma operator should be irrelevant.

There are a few interesting things going on here:

  • Two of the three (apparently) correct results were produced by relatively lightly-tested research compilers.
  • Most compiler bugs are in the optimizers. Therefore, problems like this that show up with optimizations disabled are relatively rare.
  • C is not the simple “portable assembly language” that people like to claim it is. Nobody gets all of its corner cases right, even for something relatively simple like integers.
  • Just yesterday, Xuejun — the main Csmith hacker — added support for the comma operator. Most compilers’ implementations of it are probably not very well tested.
  • Intuitively, n-version programming should work. Knight and Leveson famously showed that it may not.

Related previous posts from this blog are here and here.

Update: I should have added that I’m interested to see if there are any other compilers that get this wrong. If you have access to a compiler not on my list above and wouldn’t mind running the test and posting the result in a comment, I’d appreciate it.

Update from July 13: The behavior of this program is a bit more subtle than my explanation above indicates. John McCall’s comment has the best explanation I’ve seen so far.

Update from July 14: In C, a global variable DOES NOT need an explicit initializer. It is automatically initialized to zero.

regehr

, ,

59 responses to “Split Vote”

« Older Comments

  1. Given the audience of this blog, 2 is a shockingly high number of people not knowing basic properties of C.

  2. Rajan, I don’t think the resolution to DR315 resolves the ambiguity in this post’s test case. C99 seemingly allows me to reason like this:
    1. The bit-field f1 has type unsigned int.
    2. s.f1 has the same type as f1.
    3. The comma operator has the type of its right-hand side, so (0, s.f1) also has type unsigned int.
    4. (0, s.f1) is a comma expression, not a bit-field, so it promotes to unsigned int.

    The best objections I can think of apply to #1 and #4. For #1, there are a couple of places that describe bit-fields as having a normal integer type like “unsigned int”, but there’s also a place that says, “A bit-field is interpreted as a signed or unsigned integer type consisting of the specified number of bits.” For #4, maybe the bit-field integral promotion rule applies to “an expression whose value comes from a bit-field” like John McCall suggested, instead of just the . and -> expressions.

    The resolution to DR315 emphasizes that bit-fields are promoted using the width, but it doesn’t clarify whether (0, s.f1) is a bit-field or whether it has some kind of special 1-bit type.

  4. Sorry about the uninitialized comment… I had a braino and saw that as an automatic declaration somehow. Bleah.

    Anyway, 6.7.2.1/4 says “A bit-field shall have a type that is a qualified or unqualified version of _Bool, signed int, unsigned int, or some other implementation-defined type.” I’m not 100% sure *precisely* what that means, but it’s the only place in the spec that explicitly says what the “type” of a bitfield is.

    So if s.f1 is an unsigned int, then the result of the comma operator can only be considered to be an rvalue “unsigned int”, which doesn’t require any promotion here. Indeed, the comma operator spec explicitly says that it evaluates the right operand, generating a result, and comma is not specified to use integer promotion or the “usual arithmetic conversions” in its evaluation. Stated another way, the result of the comma operator is not literally “s.f1” but a completely new rvalue with the same value and type as s.f1. Whether the size of the bitfield is part of that type isn’t really specified, as you can’t have a standalone variable of bitfield type.

    I.e., you could reasonably interpret the evaluation of the comma operator as being equivalent to “unnamedTemp = s.f1” (where unnamedTemp is an unsigned int), as that also results in an rvalue with the same type as s.f1.

    Of course, all that’s ambiguous enough that I’m not ready to say that “1” is the only correct answer, but it seems sufficient to make it at least an arguably correct one.

  5. Did some more testing and VC 10 is just wrong. It continues to set y to 1 even if you remove the comma operator entirely, and say “y = x >= s.f1;”, though in both cases it does warn of a signed/unsigned comparison, which would cause most people to put in an explicit cast. So it’s not using any of the clever interpretations mentioned in these comments.

    (and that’s obviously wrong because >= *does* explicitly require the usual arithmetic conversions on its operands, which includes promotion… VC just seems to ignore 6.3.1.1/2)

  6. hacksoncode, thanks for the VC results, very interesting! I don’t have good contacts in the MS compiler group, but should develop some.

  9. I might have missed a comment, but I just tested and realized that MSVC 2010 and GCC (ver 4.5.0) evaluates (x >= s.f1) as true as long as s.f1 remains unsigned regardless of the comma operator.

    struct ST {
    unsigned f1;
    }s = { 1 };

    int main (void) {
    int x = -3;
    printf(“%d >= %d = %d”, x, s.f1, (x >= s.f1));
    return 0;
    }

    prints out “-3 >= 1 = 1”. If the expression is (x >= (signed) s.f1), both compilers print out “-3 >= 1 = 0” which is correct.

    I’m not a compiler builder, but shouldn’t an unsigned value be promoted before the testing with a signed value?

« Older Comments