Buscando un c-versión pura de funciones math.h (no hay soporte co-procesador) [cerrado]

Question

Tengo que trabajar con un poco de (semi) automático de verificación de software (CBMC (enlace) ) que está trabajando estáticamente en fuentes C. punto flotante es compatible, pero no hay definiciones para todas las funciones matemáticas. El intento es comprobar, si es posible comprobar de programa digital con él.

Así que necesito estas funciones. Busco algunas definiciones math.h sin el uso de co-procesador (por ejemplo sqrt, pow, resto, tan; int / float / double).

Cuando busqué en una libc enviado con algunas distribuciones de Linux (tal vez ahora eglibc), siempre llega a un punto, donde hay algunas procesador intrínsecos que significa un sqrt-función de hardware, por ejemplo.

Parte 1: la búsqueda de las implementaciones de software

Lo que necesito es una biblioteca de apoyo a las funciones matemáticas con las siguientes características:

• IEEE de punto flotante es compatible, pero una biblioteca que opera exclusivamente en números enteros Sería muy bueno también, tal vez mejor.
• La corrección es un factor crítico. (Bugs conocidos para casos especiales ocultos en algunas fuentes no son tan fresco). Los resultados también deben ser correcta en términos de-754 IEEE (reglas por ejemplo, para sqrt).
• No uso de las llamadas co-procesador. software puro. se prefiere C, pero ASM debería estar bien también.

Hasta ahora, he buscado un poco por diversas implementaciones de libc, especialmente las relativas a los sistemas embebidos. Creo que la mayoría de estas bibliotecas están apuntando la portabilidad y el tamaño de los programas compilados, pero es difícil saber si se está utilizando instrucciones de procesador específicas.

• fdlibm parece tener algunas definiciones en software puro, a la primera vista. Voy a inspeccionar más a fondo. Sin embargo, hay algunos errores mencionados en las fuentes (código no es estándar).
• newlib parece traer las mismas definiciones (basado en el código de Sun Microsystems). Pero no puedo decir con certeza en este momento si se utilizan todos los días estas versiones de software, de modo que allí quizá algunos co-procesador de llamadas que no veo en este momento (ver parte 2).
• uClibc parece compartir la característica con newlib.

Parte 2: la comprensión de la estructura de estas implementaciones

• Podría alguien dar una breve introducción a la estructura de estas librerías matemáticas. ¿Cómo hacer que envían las diferentes versiones (por ejemplo, un co-procesador específico)?

• Y cuáles son el significado de estos diferentes prefijos en los nombres de archivo. e_sqrt.c, k_sin, s_sin?

Yo sería feliz de escuchar acerca de algunas bibliotecas que podría ser útil para mí. Yo prefiero tener una biblioteca como viene, pero cuando es necesario, también es posible buscar algunas implementaciones de función única y construir una pequeña biblioteca. No voy a usar todas las funciones definidas en math.h.

Este y this SO-mensajes están diciendo que el Java Implementación de matemáticas está / estaba basada en fdlibm , que los sonidos que esta biblioteca es el camino a seguir. Cualquier persona con más información acerca de esta biblioteca que debería saber?

Parece que tengo muchas posibilidades, incluyendo los dos siguientes:

1. Uso glibc y compilación de software de modo . El problema es que no puedo utilizar cualquiera de las herramientas automáticas de comprobación del sistema (en configurar). Tengo que dar toda la información manually. ¿Hay banderas de prohibir el uso de la FP-coprocesador SIMD y prohibir-operaciones? fp-sin debería ser un comienzo, entonces se usa también soft-flotador si se compila. Espero que el proceso de compilación depende más o menos en una decisión específica para un host (como el brazo ...).
2. Uso fdlibm (preferido en el momento). Problema: ¿Cómo puedo enlazar mis programas a ella? Necesito las funciones no libm como afirman, pero quiero enlace en contra de mi fdlibm y no el sistema de libm que está instalado (por lo -nodefaultlibs prohibirá el uso de aserción).

Answer 1

Hay una aplicación de software completa de IEEE-754 en glibc / sysdeps / IEEE754 . Al compilar la biblioteca podría sustituir de forma automática en una versión específica de la arquitectura (por ejemplo ia64/fpu/e_acosf.S) de alguna función, sino a toda la biblioteca está implementado en el software también.