A convert-to-floating-point function at the frontier of formal verification
By pascal on Thursday, April 12 2012, 12:54 - Permalink
The function in this post to the musl mailing list is a good candidate for formal verification. It should just barely be possible to verify the absence of undefined behaviors with Frama-C's value analysis, and it should just barely be possible to verify it functionally with one of the Jessie or Wp plug-ins.
Context
Musl is a libc project. Key quote: “musl is lightweight, fast, simple, free, and strives to be correct in the sense of standards-conformance and safety”.
The function highlighted in this post converts the decimal representation of a number to a long double in a correctly rounded manner. The long double type is not very portable, and therefore I do not expect any Frama-C plug-in to support it, but after replacing all instances of long double with double and choosing the corresponding LDBL_MANT_DIG and LDBL_MAX_EXP, the function becomes a plain decimal-to-double conversion function, that it should be possible to verify formally with Frama-C.
Motivation
The formal verification I am encouraging the valiant reader to attempt would be useful, too! This is a brand-new implementation. I was looking for one such decimal-to-binary function at about the time I was writing this post. At the time, there were about four categories of Open Source implementations:
- the very wrong version, available in Ruby and Tcl to compile on platforms that lack
strtod(). This one can return a result off by 15 ULPs or so; - the slightly wrong and somewhat complicated version (Glibc);
- the correctly rounded but non-portable and terribly complicated version (David M. Gay's implementation);
- and the naïve version (the pseudo-code from Rick Regan that I ended up basing my own function on).
The new function I am suggesting to formally verify nicely fills the gap between 3. and 4. above. It is quite clean and portable, but from a quick code review, I expect it to be faster than, say, my own implementation. It is written to be correctly rounded according to the FPU's rounding mode. It seems to use base-10⁹ multi-precision integers. I am still trying to make sense of parts of it.
Comments
That Ruby version is curious. I assume the authors know it to be "quick and dirty"? On the other hand, this comment in the code makes me wonder: "If the mantissa has more than 18 digits, ignore the extras, since they can't affect the value anyway".
@Rick: the version I called "Ruby's" is found in nearly identical instances in several other places, just like David M. Gay's is. From that and from the headers, I would guess it originates in some early Unix release.
As for whether the Ruby implementers know that it is quick and dirty, I think that question is best left to philosophers. Ruby implementers certainly do not care much, because few systems do not provide their own strtod() nowadays (and if the system's strtod() is buggy, it is not Ruby's fault).
When I finally implemented my own conversion function, it gave me the opportunity to warn about non-exact conversions, and then I agonized about whether it was pertinent for the Frama-C front-end to warn about that. For the very wrong implementation, at least, the warning is quite good at pointing out the beginning of the problem:
warning: Floating-point constant 1.0e32 is not represented exactly. Will use 0x1.3b8b5b5056e17p106. See documentation for option -warn-decimal-float
This is of course not the only issue in the "very wrong" implementation, but it is the first one in source code order.