On the precise analysis of C programs for FLT_EVAL_METHOD==2

There has been talk recently amongst my colleagues of Frama-C-wide support for compilation platforms that define FLT_EVAL_METHOD as 2. Remember that this compiler-set value, introduced in C99, means that all floating-point computations in the C program are made with long double precision, even if the type of the expressions they correspond to is float or double. This post is a reminder, to the attention of these colleagues and myself, of pitfalls to be anticipated in this endeavor.

We are talking of C programs like the one below.

#include <stdio.h> 
int r1; 
double ten = 10.0; 
int main(int c, char **v) 
{ 
  r1 = 0.1 == (1.0 / ten); 
  printf(1=%d"  r1); 
} 

With a C99 compilation platform that defines FLT_EVAL_METHOD as 0 this program prints "r1=1" but with a compilation platform that sets FLT_EVAL_METHOD to 2 it prints “r1=0”.

Although we are discussing non-strictly-IEEE 754 compilers we are assuming IEEE 754-like floating-point: we're not in 1980 any more. Also we are assuming that long double has more precision than double because the opposite situation would make any discussion specifically about FLT_EVAL_METHOD == 2 quite moot. In fact we are precisely thinking of compilation platforms where float is IEEE 754 single-precision (now called binary32) double is IEEE 754 double-precision (binary64) and long double is the 8087 80-bit double-extended format.

Let us find ourselves a compiler with the right properties :

$ gcc -v 
Using built-in specs. 
Target: x86_64-linux-gnu 
… 
gcc version 4.4.3 (Ubuntu 4.4.3-4ubuntu5.1)  
$ gcc -mfpmath=387 -std=c99 t.c && ./a.out  
r1=0 

Good! (it seems)

The test program sets r1 to 0 because the left-hand side 0.1 of the equality test is the double-precision constant 0.1 whereas the right-hand side is the double-extended precision result of the division of 1 by 10. The two differ because 0.1 cannot be represented exactly in binary floating-point so the long double representation is closer to the mathematical value and thus different from the double representation. We can make sure this is the right explanation by changing the expression for r1 to 0.1L == (1.0 / ten) in which the division is typed as double but computed as long double then promoted to long double in order to be compared to 0.1L the long double representation of the mathematical constant 0.1. This change causes r1 to receive the value 1 with our test compiler whereas the change would make r1 receive 0 if the program was compiled with a strict IEEE 754 C compiler.

Pitfall 1: Constant expressions

Let us test the augmented program below:

#include <stdio.h> 
int r1  r2; 
double ten = 10.0; 
int main(int c  char **v) 
{ 
  r1 = 0.1 == (1.0 / ten); 
  r2 = 0.1 == (1.0 / 10.0); 
  printf("r1=%d r2=%d"  r1  r2); 
} 

In our first setback the program prints “r1=0 r2=1”. The assignment to r2 has been compiled into a straight constant-to-register move based on a constant evaluation algorithm that does not obey the same rules that execution does. If we are to write a precise static analyzer that corresponds to this GCC-4.4.3 this issue is going to seriously complicate our task. We will have to delineate a notion of “constant expressions” that the analyzer with evaluate with the same rules as GCC's rules for evaluating constant expressions and then implement GCC's semantics for run-time evaluation of floating-point expressions for non-constant expressions. And our notion of “constant expression” will have to exactly match GCC's notion of “constant expression” lest our analyzer be unsound.

Clarification: What is a “precise” static analyzer?

This is as good a time as any to point out that Frama-C's value analysis plug-in for instance is already able to analyze programs destined to be compiled with FLT_EVAL_METHOD as 2. By default the value analysis plug-in assumes IEEE 754 and FLT_EVAL_METHOD == 0:

$ frama-c -val t.c 
… 
t.c:9:[kernel] warning: Floating-point constant 0.1 is not represented exactly. 
 Will use 0x1.999999999999ap-4. 
 See documentation for option -warn-decimal-float 
… 
[value] Values at end of function main: 
          r1 ∈ {1} 
          r2 ∈ {1} 

The possibility of FLT_EVAL_METHOD being set to 2 is captured by the option -all-rounding-modes:

$ frama-c -val -all-rounding-modes t.c 
… 
t.c:9:[kernel] warning: Floating-point constant 0.1 is not represented exactly. 
 Will use 0x1.999999999999ap-4. 
 See documentation for option -warn-decimal-float 
… 
[value] Values at end of function main: 
          r1 ∈ {0; 1} 
          r2 ∈ {0; 1} 

The sets of values predicted for variables r1 and r2 at the end of main() each contain the value given by the program as compiled by GCC-4.4.3 but these sets are not precise. If the program then went on to divide r1 by r2 Frama-C's value analysis would warn about a possible division by zero whereas we know that with our compiler the division is safe. The warning would be a false positive.

We are talking here about making a static analyzer with the ability to conclude that r1 is 0 and r2 is 1 because we told it that we are targeting a compiler that makes it so.

The above example command-lines are for Frama-C's value analysis but during her PhD Thi Minh Tuyen Nguyen has shown that the same kind of approach could be applied to source-level Hoare-style verification of floating-point C programs. The relevant articles can be found in the results of the Hisseo project.

To be continued

In the next post we will find more pitfalls revisit a post by Joseph S. Myers in the GCC mailing list and conclude that implementing a precise static analyzer for this sort of compilation platform is a lot of work.