Frama-C news and ideas

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

Tag - conversions-and-promotions

Entries feed - Comments feed

Tuesday, November 8 2011

Floating-point quiz

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?

  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

  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

  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

  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

  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.

Tuesday, July 26 2011

Fun with usual arithmetic conversions

A facetious colleague reports the following program as a bug:

int main () {
  signed char c=0;
  while(1) c++;
  return 0;

The commandline frama-c -val -val-signed-overflow-alarms charpp.c, he says, does not emit any alarm for the c++; instruction.

Indeed, the c++; above is equivalent to c = (signed char) ((int)c + 1);.

If the implementation-defined( §3) conversions from int to signed char are assumed to give the expected modulo results, this instruction never displays undefined behavior. The really dangerous operation, signed addition, takes place between arguments of type int and returns an int. Thus, in this particular program and for the default x86_32 target architecture, the result of the addition is always representable in the result type.

Monday, April 11 2011

C99 promotion rules: what ?!

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

The fun starts earlier, in, 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 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.

page 2 of 2 -