I have to work with some (semi-)automatical verification software (CBMC (link)) which is statically working on C sources. Floating point is supported, but there are no definitions for all the mathematical functions. The attempt is to check, if it's possible to check numerical software with it.
So I need these functions. I'm looking for some math.h definitions without co-processor use (e.g. sqrt, pow, remainder, tan; int/float/double).
When I looked for it in a libc shipped with some linux distributions (maybe now eglibc), I always reached a point, where there are some processor-intrinsics meaning a hardware sqrt-function for example.
Part 1: searching for software implementations
What I need is a library supporting mathematical functions with the following characteristics:
- IEEE Floating-Point is supported, but a library operating purely on integers would be great too, maybe better.
- Correctness is a critical factor. (known bugs for special cases hidden in some sources are not that cool). The results should also be correct in terms of IEEE-754 (e.g. rules for sqrt).
- No use of co-processor calls. Pure software. C is preferred, but asm should be okay too.
Until now, I searched a bit for various libc implementations, especially ones regarding embedded systems. I think most of these libraries are targeting portability and size of compiled programs, but hard to tell if they are using processor-specific instructions.
- **fdlibm seems to have some pure-software definitions at a first glance. I will inspect this further. But there are some bugs mentioned in the sources (code isn't standard).
- **newlib seems to bring the same definitions (based on code of sun microsystems). But i can't say for sure at the moment if these software versions are alway used, so that there maybe some co-processor calls i don't see at the moment (see part 2).
- **uClibc seems to share the characteristic with newlib.
Part 2: understanding the structure of these implementations
Could someone give me a short introduction to the structure of these math libraries. How do they dispatch the various versions (e.g. a specific co-processor)?
And what are the meaning of these different prefixes in the filenames.
e_sqrt.c,k_sin,s_sin?
I would be happy to hear about some libraries which could be useful for me. I would prefer to take a library as it comes, but when it is necessary, it is also possible to look for some single function implementations and build up a small library. I won't use all of the functions defined in math.h.
This and this SO-posts are saying that the Java Math Implementation is/was based on fdlibm which sounds that this library is the way to go. Anyone with more information about this library I should know?
Seems that I have many possibilities including the following two:
- Use glibc and compile in software-mode. The problem is, that I can't use any of the automatic system checking tools (in configure). I have to give all the information manually. Are there any flags to forbid the use of the fp-coprocessor and to forbid simd-operations? fp-without should be a start, then it is also using soft-float if it compiles. I expect that the compilation process is more or less dependent on a specific decision for a host (like arm...).
- Use fdlibm (preferred at the moment). Problem: how do I link my programs to it? I need the non-libm functions like assert, but want to link against my fdlibm and not the system-libm which is installed (so -nodefaultlibs will forbid the use of assert).
