Frama-C news and ideas

In a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point!

Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the 4-color theorem really holds. It would be supremely ironic if an undefined behavior in a bit of C code in the OCaml implementation used to compile Coq caused it to accept as valid some incorrect proofs, for instance in the formally verified (in Coq) compiler CompCert.

Your mission, should you decide to accept it

Where are these undefined behaviors? They are in several places, but some of them are in the implementation of the bytecode arithmetic operations. In OCaml, basic operations such as addition and multiplication are specified as returning the mathematical result modulo 2^31, 2^32, 2^63 or 2^64, depending on the compilation platform and the integer type.

The problem here is not limited to OCaml. The Java Virtual Machine too specifies that arithmetic operations on its 32-bit integer type return results modulo 2^32. Someone wishing to implement a JVM in portable C would face the same issues.

In fact, this is just such a big issue that we should collectively try to work out a solution now.

A safer signed addition instruction

Let us assume a 32-bit platform. In this case, values of the unboxed OCaml type int range between -2^30 and 2^30-1 (31 bits of information). They are stored at run-time in the 31 most significant bits of a machine word, with the least significant bit set to one to distinguish it from a pointer. This representation is taken into account when applying arithmetic operations to machine words representing unboxed integers.

Here is an example, in file interp.c in the OCaml implementation. We are in the middle of the large switch that decodes bytecode instructions:

    Instruct(ADDINT):
      accu = (value)((intnat) accu + (intnat) *sp++ - 1); Next;

The - 1 in this expression compensates for the fact that the least significant bit is set in both operands, and we want it to be set in the result (and no carry to be propagated). But as written, there is an undefined overflow in the C implementation of the bytecode interpreter when the unboxed integers in accu and *sp total more than 2^30-1. In order to avoid a signed overflow here, the instruction ADDINT could be written:

      accu = (value)((uintnat) accu + (uintnat) *sp++ - 1U); Next;

This solution takes advantage of the fact that unlike signed addition, the behavior of unsigned addition when the result overflows the destination type is defined by the C standard. The solution above does make assumptions about the conversion from a signed to an unsigned type and vice versa, but these are implementation-defined (and we are only targeting implementations that define these conversions as 2's-complement).

No overhead is involved in this approach: a half-decent C compiler should generate the same instruction sequence for the new version as it already generates for the old version.

Multiplication

You may be vaguely worried about multiplication. For instance, you may remember that while, in a typical instruction set, there is only one addition instruction that works for both signed and unsigned operands, there are dedicated signed multiplication and unsigned multiplication instructions. These are IMUL and MUL in the x86 family of processors.

Fear not! The two multiplications are only because on x86 and many other processors, 32-bit multiplication returns a 64-bit result. If you want all 64 bits of the results to be what you expect, you need to choose the instruction that interprets the operands' highest bit correctly. But if on the other hand you only care for the lowest 32 bits of the result (that is, you only want a result modulo 2^32), then it does no matter that you use unsigned multiplication. Think of it as (x + k1 * 2^32) * (y + k2 * 2^32) for unknown k1 and k2.

And this is our case. Thus, in interp.c, the implementation for bytecode instruction MULINT could be changed from:

Instruct(MULINT):
  accu = Val_long(Long_val(accu) * Long_val(*sp++)); Next;

to:

Instruct(MULINT):
  accu = Val_long((intnat)((uintnat)Long_val(accu) * (uintnat)Long_val(*sp++))); Next;

Conclusion

As pointed out by John Regehr in the comments, the two fixes above are appropriate because the OCaml language definition specifies wrap-around behavior for its (signed) arithmetic operations. One should not assume that all the warnings emitted by IOC have a similar cause. Some may be deeper bugs requiring the logic to be fixed, instead of conversions to unsigned types that only ensure wrap-around behavior.

Issues of the nature discussed here should be in the bytecode version of the OCaml compiler only. By contrast, the native compiler should translate OCaml-level multiplication directly to assembly multiplication, bypassing the portable^Wwoefully underspecified assembly that is the C language.

Even programs generated by the native compiler interface with bits of OCaml runtime written in C, but this runtime is small.

So actually, there is not much cause for worry. If you are using a C compiler or a static analysis platform that involve OCaml code on a modern computer, they are probably already compiled with the native OCaml compiler.

I do not have any solution I am 100% happy with to the overflow dilemma in the previous post. Here is one of the solutions that does not make me 100% happy.

The first (partial) solution is: program so that overflows correspond exactly to unwanted circumstances (and then it becomes meaningful to verify the absence of overflows. There are great automatic tools for that. Have you heard of them?)

“Program so that…” sounds abstract, but it may be as simple as using larger integer types that won't overflow for all intermediate computations:

  s = (int)((long long) u1 - (long long)u2);

Then the desired property (variable s contains the mathematical difference of u1 and u2) entirely rests on the final conversion from long long to int.

This solution doesn't apply in the common situation where the code is already written and gratuitous changes to it are prohibited. Also, you need to have an integer type large enough to contain all intermediate computations without overflows. In this example, unsigned int is 32-bit and long long is 64-bit, but the standard does not prevent unsigned int to be 64-bit and the same size as long long, in which case the conversion from unsigned int to long long could overflow. Rte would only insert additional assertions for the two intermediate conversions that we have added in the assignment. This wouldn't help; it would only make things worse.

“Won't the generated code be less efficient?”, you rightly ask. That all depends on the compiler. Optimizing compilers have no trouble at all optimizing the above assignment so that it uses only one 32-bit subtraction. On the Linux workstation on which I tried this, both clang -m32 -O0 and gcc -m32 -O0 did. It is amusing, because the code generated by both compilers with -O0 is ugly (gratuitously moving registers to memory and then to registers again) but, even with optimizations disabled, they still both get the fact that it is only necessary to compute the least significant 32 bits of the result.

With optimizations, both Clang and GCC generate clean code that naturally still uses a single 32-bit subtraction:

$ gcc -S -O2 -m32 t.c
$ cat t.s
...
f:
	pushl	%ebp
	movl	%esp, %ebp
	movl	8(%ebp), %eax
        subl	12(%ebp), %eax
	popl	%ebp
	ret

As an anecdote, when generating x86-64 code (and therefore having 64-bit subtraction available as a single instruction, with only the drawback of a slightly larger encoding), gcc -O0 keeps using 32-bit subtraction but clang -O0 uses 64-bit subtraction. This does not reveal anything about the compilers: it does not make sense to compare for efficiency the code they generate with optimization disabled.

That's all for this post.

There are only positive constants in C, as per section 6.4.4 in the C99 standard:

integer-constant: 
        decimal-constant integer-suffixopt 
        octal-constant integer-suffixopt 
        hexadecimal-constant integer-suffixopt 
decimal-constant: 
        nonzero-digit 
        decimal-constant digit 
octal-constant: 
        0 
        octal-constant octal-digit 
hexadecimal-constant: 
        hexadecimal-prefix hexadecimal-digit 
        hexadecimal-constant hexadecimal-digit 
...

The minus sign is not part of the constant according to the grammar.

The expression -0x80000000 is parsed and typed as the application of the unary negation operator - to the constant 0x80000000. The table in section 6.4.4.1 of the standard shows that, when typing hexadecimal constants, unsigned types must be tried. The list of types to try to fit the hexadecimal constant in is, in order, int, unsigned int, long, unsigned long, long long, unsigned long long.

For many architectures, the first type in the list that fits 0x80000000 is unsigned int. Unary negation, when applied to an unsigned int, returns an unsigned int, so that -0x80000000 has type unsigned int and value 0x80000000.

Following the same reasoning as above, reading from the "Decimal Constant" column of the table in the C99 standard, the types to try are int, long, and long long. This might lead you to expect -2147483648 for the value of the expression -2147483648 compiled with GCC. Instead, when compiling this expression on a 32-bit architecture, GCC emits a warning, and the expression has the value 2147483648 instead. The warning is:

t.c:6: warning: this decimal constant is unsigned only in ISO C90

Indeed, there is a subtlety here for 32-bit architectures. GCC by default follows the C90 standard. It's not so much that the spirit of the table in section 6.4.4.1 in C99 changed between C90 and C99. The spirit remained the same, with unsigned types being tried for octal and hexadecimal constants, and mostly only signed types being tried for decimal constants. Here is the relevant snippet from the C90 standard:

The type of an integer constant is the first of the corresponding list in which its value can be represented. Unsuffixed decimal: int, long int, unsigned long int;

The difference really stems from the fact C90 did not have a long long type, and the list of types to try for a decimal constant ended in unsigned long, since that type contained values that did not fit in any other type. On a 32-bit architecture, where long and int are both 32-bit, 2147483648 fits neither int nor long, and so ends up being typed as an unsigned long. Note that on an architecture where long is 64-bit, then 2147483648 and -2147483648 are typed as long.

Finally, when GCC is told, with option -std=c99, to apply C99 rules on an architecture where long is 32-bit, then 2147483648 is typed as long long, so that the expression -2147483648 has type long long and value -2147483648.

This should explain the results obtained when compiling the three programs from last post with GCC on 32-bit and on 64-bit architectures.

Here is a little quiz you can use to test your C floating-point expertise. I have tried to write the examples below so that the results do not depend too much on the platform and compiler. This is theoretically impossible since C99 does not mandate IEEE 754 floating-point semantics, but let us assume that the compiler at least tries. It could be a recent GCC on 8087-class hardware, for instance.

Question 1

What's the return code of this program?

main(){
  return 0.1 == 0.1f;
}

Answer: the program returns 0. Promotion and conversion rules mean that the comparison take place between double numbers. The decimal number 0.1 is represented differently as a single-precision float and as a double-precision double (and none of these two representations is exact), so when 0.1f is promoted to double, the result is quite a bit different from the double representing 0.1.

Question 2

main(){
  float f = 0.1;
  return f == 0.1f;
}

Answer: the program returns 1. This time, the comparison takes place between float numbers. But first things first: variable f is initialized with the double representation of 0.1, but this number has to be converted to float to fit f. As a result, f ends up containing only those digits of 0.1 that fit into a float mantissa. When the contents of f are read back, they compare exactly to the 0.1f single-precision constant.

Question 3

main(){
  float f = 0.1;
  double d = 0.1f;
  return f == d;
}

Answer: the program returns 1. The comparison takes place between double numbers again. The left-hand side is the promotion to double of the single-precision representation of 0.1. The right-hand side is the contents of double-precision variable d, that has been initialized with the conversion to double of the single-precision representation of 0.1. The two sequences of operations produce the same result.

Question 4

main(){
  double d1 = 1.01161128282547f;
  double d2 = 1.01161128282547;
  return d1 == d2;
}

Answer: the program returns 0. The decimal number 1.01161128282547 is no more representable than 0.1, and again, its double representation in d2 has more digits than its float representation converted to double in d1.

For a fractional number to be representable as a (base 2) floating-point number, its decimal expansion has to end in 5, although the converse isn't true. Numbers 0.5 and 0.625 are representable as floating-point numbers, but 0.05, 0.1 and 1.01161128282547 aren't. A number may also have the same representation as float and double although neither of these two representations is exact: for this to happen, it suffices that the 29 additional binary digits available in the double format be all zeroes.

Question 5

main(){
  float f1 = 1.01161128282547f;
  float f2 = 1.01161128282547;
  return f1 == f2;
}

Answer: if this looks like a trick question, it's because it is. The program returns 0. Variable f1 is initialized with the single-precision representation of 1.01161128282547. On the other hand, f2 receives the conversion to float of the double representation of this number. In this particular case, the two are not the same: the number 1.01161128282547 is actually very close to the middle point of two successive floating-point numbers. When it is first rounded to double (when initializing f2), it is rounded to the middle point itself (which happens to be representable as a double). When that double is rounded to a float, applicable rounding rules send it to the float on the opposite side of the middle point we started from. On the other hand, when initializing f1, the original number is rounded directly to the nearest float.

       ~1.01161122                    ~1.01161128                     ~1.01161134
            +------------------------------+------------------------------+
           f2                                ^                            f1
                                       original number

I could make another series of questions, somewhat symmetrical to this one, where two different but standard-complicant compilers produce different results each time, but that wouldn't be as much fun. The examples here were relatively well defined. The rules that make them puzzling (or not) apply indiscriminately to most compilers. Unless they do not even try to follow C99's guideline that recommends IEEE 754 arithmetics.

I reported bug 785 after getting three-quarters sure that the problem was in Frama-C (I used two different versions of GCC as oracles).

I still cannot believe how twisted integer promotion rules are in C99. I had read them before, but I had not followed the precise path I followed today in the various cases of 6.3.1.8.

The fun starts earlier, in 6.3.1.3, with the definition of conversion rank.

rank(long long int) > rank(long int), even when these two types have the same size. But:

The rank of any standard integer type shall be greater than the rank of any extended integer type with the same width.

So if a compiler defines an extended long long long type, programs that use them will become differently typed the day long long long becomes a standard type. Until it is standardized, it has lower rank than a standardized type of the same size. When it becomes standardized, it will probably get a higher rank than other standardized types of the same size.

Well, never mind this: it is unclear whether this can have any effect on the computations in practice (it matters only when types have exactly the same size). Let's see what in 6.3.1.8 applies to bug 785, starting with the promotions applicable to 0x090E7AF82577C8A6LL | x9[1][0].

We have a `long long` on the left-hand side, an `unsigned long` on the right-hand side. Oh, and in this platform description, `long` and `long long` are both the same size, 64-bit.

1. blah blah "If both operands have the same type" nope
2. "if both operands have signed integer types or both have unsigned integer types" nope
3. "if the operand that has unsigned integer type has rank greater or equal to the rank of the type of the other operand" nope
4. "if the type of the operand with signed integer type can represent all of the values of the type of the operand with unsigned integer type" nope, it's missing half of them.
5. "Otherwise, both operands are converted to the unsigned integer type corresponding to the type of the operand with signed integer type."

There is a philosophy hidden in there. The philosophy seems to be "favor unsigned types, unless the signed type makes more sense". Even a signed type of higher hank may see its values converted to the unsigned version of the same type, changing the meaning of half of them. The rank matters only when it confirms that the unsigned type should be favored. You may be forgiven for wondering why we bother with ranks at all.

In conclusion, both 0x090E7AF82577C8A6LL and x9[1][0] should be promoted to unsigned long long, which shall also be the type of the result. This is not what Carbon does.