Frama-C news and ideas

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

Linux and floating-point: nearly there

In the process of implementing the value analysis built-ins Frama_C_precise_sin() and Frama_C_precise_cos() from last post, I stumbled on some interesting floating-point results. The sensationalistic title blames Linux, but I didn't fully investigate the problem yet, and it could be somewhere else.

If you have the Frama-C sources lying around, you might be able to reproduce it as below. Otherwise, just read on; it is rather obvious what is wrong, even for a floating-point issue.

$ make bin/toplevel.top
...
$ bin/toplevel.top 
        Objective Caml version 3.12.1

# open Ival ;;        
# set_round_upward () ;;
- : unit = ()
# sin (-3.0) ;;
- : float = -2.75991758268585219
# set_round_nearest_even () ;;
- : unit = ()
# sin (-3.0) ;;
- : float = -0.141120008059867214

2.76 is a large amplitude for the sine of any angle, and 3.0 isn't even unreasonable as an argument to pass to trigonometric functions. Trigonometric functions on my other OS work from OCaml in all rounding modes. On this Linux computer, the result is reasonable in the default nearest-even mode. This all rather points to an issue in libraries rather than OCaml itself.

If even desktop computers and servers provide this kind of third-rate trigonometric functions, what should we assume about embedded code?

Comments

1. On Monday, October 3 2011, 13:59 by Anne

Did you have a closer look at this problem ? I have just tested it with C, and it seems that the error occurs with the [double sin(double x)] function when compiled with [gcc -m64]. I just cannot believe it !!!

2. On Saturday, October 8 2011, 16:46 by pascal

Hello, Anne.

This appears to be the same bug as one initially reported in 2002 by Vincent Lefèvre against Debian, and re-reported against glibc (that provides libm) in 2007:

http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=153022 (see message 10)

http://sourceware.org/bugzilla/show_bug.cgi?id=3976

As I said in the post's title, "nearly there". I can't blame the maintainers, though, because I have reproduced the problem with the latest glibc 2.14 (different result but still wrong), and looking at the source code, that part of the library is complex indeed.