Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Saturday, April 13 2013

Making oughts from ises

A previous post discussed the nature of uninitialized and indeterminate memory throughout the C standards. The argument was “avoid using uninitialized data, even if you think you know what you are doing; you may be right, but regardless your compiler might think it knows what you are doing and be wrong about it”. I tried to strengthen this argument by claiming that writing the example for that post was how I found my first compiler bug “by hand”.

An example involving unsequenced addition and sequenced comma operators

That bit about a compiler bug being my first, I now fear, was an exaggeration. I had found and forgotten another arguable GCC bug in 2012 while investigating sequence points. First, consider the program below.

#include <stdio.h>

int i, j;

int f(void)
{
  i++;
  return j;
}

int g(void)
{
  j++;
  return i;
}

int main()
{
  printf("%d\n", f() + g());
}

Although functions f() and g() may be called in an unspecified order, calling a function and returning from it are sequence points. The program therefore avoids the sin of undefined behavior caused by C99's clause 6.5:2.

6.5:2 Between the previous and next sequence point an object shall have its stored value modified at most once by the evaluation of an expression. Furthermore, the prior value shall be read only to determine the value to be stored.

The program can only print an unspecified choice of either f() + g() when calling f() first or f() + g() when calling g() first, the two of which happen to result in the same value 1.

The same reasoning that makes the C program above always print 1 should make the program below always print 1 too:

$ cat t2.c
#include <stdio.h>

int i, j;

int main()
{
  printf("%d\n", (0,i++,j) + (0,j++,i));
}

But unfortunately:

$ gcc t2.c
$ ./a.out 
2

This program should print the same result as the previous program (the one with f() and g()) because the modifications of j are sequenced by 0, on the left and ,i on the right, and similarly for i. In C99 at least, the compiler must pick a choice between adding an incremented i to the initial value of j, or the other way round. This example should print 1, in short, for the same reason that the first example in this post could be expected to print 1, or that an example that prints cos(x) * cos(x) + sin(x) * sin(x) with MT-unsafe functions cos() and sin() can still be expected to print a floating-point value close to 1.0.

Pet peeve: guessing at what the standard ought to say from what compilers do

This anecdote slowly but surely brings us to the annoyance I intended to denounce all along, and this annoyance is when programmers infer what the standard ought to be saying from what compilers do. Any discussion of the kind of corner cases I described recently invite arguments about how compilers want to optimize the generated code as if uninitialized data could not be used, or as if the two operands of + were evaluated in parallel.

This is backwards. Yes, compilers want to optimize. But compilers are supposed to follow the standard, not the other way round. And section 6 of the C99 standard does not once use the word “parallel”. It says that the evaluation order of sub-expressions is unspecified (6.5:3), and that unsequenced side-effects cause undefined behavior (6.5:2), but nothing about parallel evaluation.

Never mind the example

Actually, C99's 6.5:3 clause really says “[…] the order of evaluation of subexpressions and the order in which side effects take place are both unspecified”. I am unsure about the implications of this thing about the order of side-effects. I might even, and the long-time reader of this blog will savor this uncharacteristic admission, be wrong: perhaps a compiler is allowed to generate code that prints 2 for t2.c after all.

Nevertheless, this does not detract from the point I intended to make, which is that it is bad engineering practice to take the current behavior of popular compilers as language definition. If the C99 language allows to “miscompile” (0,i++,j) + (0,j++,i), so be it. But having read the relevant parts of the standard (6.5.2.2:10, 6.5.2.2:12, and 5.1.2.3:2 in addition to the previously mentioned clauses), it seems to me that if the standard allows to miscompile the above, it also allows to miscompile f(1) + f(2) for any function f() with global side-effects.

Global side-effects include temporarily modifying the FPU rounding mode, using a statically allocated scratch buffer, initializing a table of constants at first call, calling malloc() and free(), or even random(). All these examples are intended to be invisible to the caller, and lots of library functions you routinely use may be doing them.

So in this case my argument remains very much the same: that compilers are not implementing aggressive optimizations (yet) in presence of f(1) + f(2) should be no excuse for not clarifying whether the standard allows them.

Wednesday, March 13 2013

Reading indeterminate contents might as well be undefined

Warning: on a punctiliousness scale ranging from zero to ten, this post is a good nine-and-a-half. There was no tag for that, so I tagged it both “C99” and “C11”. The faithful reader will know what to expect. There is a bit of C90, too.

To summarize, it may appear that according to the letter of modern C standards, it is only dangerous to use uninitialized variables, instead of very dangerous. Nevertheless, this post shows that it does not matter what the standards say: compilers will bite you even when you are arguably right.

Some context in the form of a link

In 2012, Xi Wang wrote a nice blog post showing it is not a good idea to use an uninitialized variable as a source of additional entropy when trying to create a random seed.

“Xoring an uninitialized variable with whatever other source of entropy you already have cannot hurt”, the conventional thinking goes. Conventional thinking is wrong. Your typical modern compiler deletes the code that gathers the original entropy, since it is only going to be xored with an uninitialized variable. Hence the title of Xi Wang's blog post, More Randomness or Less.

In C90, “indeterminate” was simple

In the nineties, real men were real men, C standards were short, and reading indeterminate contents(such as uninitialized variables) was listed in the very definition of “undefined behavior”:

1.6 DEFINITIONS OF TERMS

Unspecified behavior — behavior, for a correct program construct and correct data, for which the Standard imposes no requirements.

Undefined behavior — behavior, upon use of a nonportable or erroneous program construct, of erroneous data, or of indeterminately-valued objects, for which the Standard imposes no requirements.

“Undefined behavior” means the compiler can do what it wants, so the behavior noticed by Xi Wang can in no way be held against a C90 compiler.

In 1999, C standards became more complicated

The C99 standard does not directly list “reading indeterminate contents” as undefined behavior. Instead, it defines indeterminate contents as “either an unspecified value or a trap representation”. Reading a trap representation causes undefined behavior (6.2.6.1:5). The nuance here is that the type unsigned char is guaranteed not to have any trap representations (and thus can always be used to read indeterminate contents).

Less randomness : the simplified version

“But my compilation platform does not have trap representations for type int, either, therefore I can use an uninitialized int variable and expect an unspecified value (a much better prospect than undefined behavior)”, one may think. This line of reasoning is attractive. It could even explain the behavior shown in Xi Wang's blog post and reproduced in simplified form below:

$ cat i.c
int f(int x)
{
  int u;
  return u ^ x;
}
$ gcc -O2 -std=c99 -S -fomit-frame-pointer i.c
$ cat i.s
…
_f:
Leh_func_begin1:
	ret
…

On this 64-bit platform, the argument x passed to f() is in register %edi, and the result of f() is expected in register %eax. Thus, by executing instruction ret directly, function f() is not even giving us back the entropy we provided it. It is instead giving us the current contents of %eax, which may not be random at all.

(Giving us back the entropy we passed to it would have been mov %edi, %eax followed by ret, a longer sequence.)

One may argue that the compiler has only opportunistically chosen the most convenient value for variable u, that is, x xored with the current contents of %eax, so that u xored with x is just the current contents of register %eax. This fits the interpretation of “unspecified value” for C99's definition of “indeterminate contents”. It is a good argument, but just wait until you have seen the next example.

The next example

#include <stdio.h>

int main(int c, char **v)
{
  unsigned int j;
  if (c==4) 
    j = 1; 
  else
    j *= 2;
  printf("j:%u ",j);
  printf("c:%d\n",c);
}

If fewer than three command-line arguments are passed to the program, it should display an unspecified even number for j, right?

$ gcc -v
Using built-in specs.
Target: x86_64-linux-gnu
…
gcc version 4.4.3 (Ubuntu 4.4.3-4ubuntu5.1) 
$ gcc -O2 t.c
$ ./a.out 
j:1 c:1

GCC version 4.4.3 has decided that since the “else” branch was reading from an uninitialized variable j, only the “then” branch was worth compiling. This is acceptable if reading uninitialized variable j is undefined behavior, but not if it is unspecified behavior. Let us insist:

$ gcc -Wall -O2 -std=c99 t.c
$ ./a.out 
j:1 c:1

Although we are requesting the C99 standard to be followed by GCC, the program is not printing for variable j the even unspecified value we are entitled to.

(In passing, a proper static analyzer would know that if it is going to show variable j as containing 1, it might as well show c as containing 4. Also, a proper static analyzer would remind you that your program must, in essence, only be used with three command-line arguments. The reason compilers do not do this is covered elsewhere)

Between 1999 and 2011, C standards did not get shorter

In 2007, Rich Peterson, working at HP, was disappointed to find that the “Not a Thing” (NaT) value that registers can have on the Itanium architecture could not be used to implement an uninitialized unsigned char.

One thing led to another, and the C11 standard was amended with the phrase “If the lvalue designates an object of automatic storage duration that could have been declared with register storage class (never had its address taken), and that object is uninitialized (not declared with an initializer, and no assignment to it has been performed prior to the use), the behavior is undefined.”

That would have been my reaction too, if I was paid by the word. Anyway, this additional sentence re-introduces undefined behavior where there was none in C99.


In the example above, the address of j was never taken, so maybe that's GCC's excuse. Let us check:

#include <stdio.h>

int main(int c, char **v)
{
  unsigned int j;
  unsigned int *p = &j;
  if (c==4) 
    j = 1; 
  else
    j *= 2;
  printf("j:%u ",j);
  printf("c:%d\n",c);
}

$ gcc -O2 t.c
$ ./a.out 
j:1 c:1

No, GCC is still acting as if j *= 2; was undefined.

Conclusion

I am not saying that this is not a bug in GCC. Perhaps it was fixed in later versions (in fact, that version does not accept -std=c11, so it must be rather old). My thesis is that you might as well avoid reading from uninitialized variables as if it was undefined behavior, because otherwise compilers will bite you. This statement holds even if what we have witnessed here is a bug in GCC version 4.4.3.


Also, if this is a bug in GCC 4.4.3, this is the first time I identify a bug in GCC without the assistance of a random program generator. In other words, compiler bugs are rare, but they become surprisingly common if you stick to a strict interpretation of a necessarily ambiguous standard. And speaking of Csmith, if there is indeed a GCC bug here, said bug cannot be detected with Csmith, which does not generate programs like mine.

Thursday, November 29 2012

Solution to yesterday's quiz

Yesterday's quiz was about the expression *(char*)(float[]){x*x} - 63 (for big-endian architectures) or *(3+(char*)(float[]){x*x}) - 63 (for little-endian ones). This post provides an explanation.


First, let us try the function on a few values:

int main(){
  for (unsigned int i=0; i<=20; i++)
    printf("l(%2u)=%d\n", i, l(i));
}

This may provide the beginning of a hint:

l( 0)=-63
l( 1)=0
l( 2)=1
l( 3)=2
l( 4)=2
l( 5)=2
l( 6)=3
l( 7)=3
l( 8)=3
l( 9)=3
l(10)=3
l(11)=3
l(12)=4
l(13)=4
l(14)=4
l(15)=4
l(16)=4
l(17)=4
l(18)=4
l(19)=4
l(20)=4


The construct (float[]){…} is C99's syntax for anonymous arrays, a kickass programming technique. This is an unabated quote.


In the case at hand, the construct converts to float the contents of the braces and puts the result in memory. The function puts the float in memory in order to read its most significant byte. That's *(char*)… on a big-endian architecture, and *(3+(char*)…) on a little-endian one.


One reason to read a single char is to circumvent strict aliasing rules—which do not apply to type char. A simpler version of the same function would have been (*(int*)(float[]){x} >> 23) - 127, but that version would break strict aliasing rules. Also, it would be too obvious.


The most significant bits of a single-precision IEEE 754 floating-point representation are, in order, one sign bit and eight exponent bits. By reading the most significant byte, we get most of the exponent, but one bit is lost. To compensate for this, the operation is applied to x*x, whose exponent is double the exponent of x.


In conclusion, yesterday's one-liner returns an integer approximation of the base-2 logarithm of a reasonably small unsigned int x. On a typical 32-bit architecture, it is exact for powers of two up to 2¹⁵. If x is zero, the function returns its best approximation of -∞, that is, -63.

Wednesday, November 28 2012

C99 quiz

Here is a convenient one-liner:

int l(unsigned int x)
{
  return *(char*)(float[]){x*x} - 63;
}

What does it do on my faithful PowerMac?


The Intel version is not as nice. That's progress for you: *(3+(char*)(float){x*x}) - 63