IEEE 754 single-precision numbers in Frama-C

Every once in a while, someone asks about single-precision floating-point support in Frama-C. Until recently it was often in the context of the value analysis, but actually, thanks to a lot of interesting new results obtained in the context of this project people working on deductive verification within Frama-C can now look forward to being harassed too.

We are not nearly home and dry yet though. Frama-C's front-end is CIL (no relation to something from Microsoft with a similar acronym). CIL is written in OCaml (the rest of Frama-C is written in OCaml too but never mind that). OCaml has a single floating-point type which corresponds to IEEE 754 double precision.

So guess how floating-point literal constants are represented in the abstract syntax tree built by CIL...

If you guessed "as an IEEE 754 double-precision number" you are partly right. Yay! But also as a string. CIL's authors did think about this especially since one of CIL's first use was for source-to-source transformation. Specifically you have all the information in this constructor defined in file frama-c/cil/src/cil_types.mli:

| CReal of float * fkind * string option 
    (** Floating point constant. Give the fkind (see ISO 6.4.4.2) and also 
     * the textual representation  if available. *)

The above is OCaml code and the type float means double-precision floating-point number.

So far so good. If there is a 10.0 literal in the program it stands for the double 10.0. If there is a 0.1 in the program it stands for one of representable numbers no further than 1ulp from the real 0.1. This is slightly annoying because the representable number chosen by CIL may not be the same as the representable number chosen by your actual C compiler but in all likelihood both will round the number from the source code to the nearest double-precision floating-point number. Thus the AST analyzed in Frama-C accurately represents the compiled program and all is well.

The picture gets muddied a little if the target program contains a literal such as 3.14f. This is supposed to represent a single-precision floating-point literal in C. I'm willing to bet without really looking that CIL represents that literal in the AST with the double-precision number nearest to the real number written in decimal in the target program. If you are a Frama-C plug-in author willing to do the right thing you may think of rounding this double-precision number to the nearest single-precision number yourself but that doesn't work: the double rounding can make your final result different from the compiler's which will round only once from real to single-precision. To be correct you have to go back to the string representation that has been saved from the source code.

In fact Frama-C's front-end should be doing this for all plug-ins of course. When the literal is single-precision it should represent it in the AST as an OCaml float containing the single-precision number meant by the programmer (all single-precision numbers can be represented as double-precision numbers). Probably this will be done soon now that the problem is identified. This was just an example of how far support for single-precision numbers in Frama-C is.

Full disclosure: I said I was betting without looking but I wouldn't take the bet if I were you. I do not just risk public humiliation like that without strong presumptions. First I was just working on something related and visible effects of this subtlety came up as one annoying unforeseen issue. Secondly there is no function in OCaml to parse a number as single-precision. There are some OCaml functions to parse double-precision numbers and this task is enough of a bother that these are defined by calling the C function strtod(). The way to fix the front-end is probably to replicate this OCaml-C interface for strtof(). So my bet is in fact that CIL's authors neither implemented a single-precision parsing function in OCaml nor interfaced it from C.