Je dois travailler avec un logiciel de vérification (semi-)automatique (CBMC). (lien) ) qui travaille de manière statique sur les sources C. La virgule flottante est supportée, mais il n'y a pas de définitions pour toutes les fonctions mathématiques. La tentative est de vérifier, s'il est possible de vérifier un logiciel numérique avec lui.
J'ai donc besoin de ces fonctions. Je suis à la recherche de math.h définitions sans utilisation de coprocesseur (par exemple sqrt , pow , reste, tan ; int / float / double ).
Quand je l'ai cherché dans une libc fournie avec certaines distributions linux (peut-être maintenant eglibc), je suis toujours arrivé à un point où il y a des éléments intrinsèques au processeur qui signifient une fonction sqrt matérielle par exemple.
Partie 1 : recherche d'implémentations logicielles
Ce dont j'ai besoin, c'est d'une bibliothèque prenant en charge des fonctions mathématiques présentant les caractéristiques suivantes :
- Le système à virgule flottante IEEE est pris en charge, mais une bibliothèque fonctionnant uniquement sur les entiers serait également parfaite, voire meilleure.
- L'exactitude est un facteur essentiel. (les bogues connus pour des cas particuliers cachés dans certaines sources ne sont pas très cool). Les résultats doivent également être corrects en termes de IEEE-754 (par exemple, les règles pour sqrt).
- Pas d'utilisation d'appels au coprocesseur. Logiciel pur. Le C est préférable, mais l'asm devrait aussi convenir.
Jusqu'à présent, j'ai cherché un peu les différentes implémentations de la libc, en particulier celles concernant les systèmes embarqués. Je pense que la plupart de ces bibliothèques visent la portabilité et la taille des programmes compilés, mais il est difficile de dire si elles utilisent des instructions spécifiques au processeur.
- ** fdlibm semble avoir des définitions purement logicielles à première vue. Je vais examiner cela plus en détail. Mais il y a quelques bogues mentionnés dans les sources (le code n'est pas standard).
- ** newlib semble apporter les mêmes définitions (basé sur le code de sun microsystems). Mais je ne peux pas dire avec certitude pour le moment si ces versions du logiciel sont toujours utilisées, de sorte qu'il y a peut-être des appels au coprocesseur que je ne vois pas pour le moment (voir partie 2).
- ** uClibc semble partager cette caractéristique avec newlib.
Partie 2 : comprendre la structure de ces implémentations
-
Quelqu'un pourrait-il me donner une brève introduction à la structure de ces bibliothèques mathématiques ? Comment répartissent-elles les différentes versions (par exemple, un coprocesseur spécifique) ?
-
Et quelle est la signification de ces différents préfixes dans les noms de fichiers.
e_sqrt.c,k_sin,s_sin?
Je serais heureux d'entendre parler de bibliothèques qui pourrait être utile pour moi. Je préfère prendre une bibliothèque comme elle vient, mais quand c'est nécessaire, il est aussi possible de chercher quelques implémentations de fonctions uniques et de se constituer une petite bibliothèque. Je n'utiliserai pas toutes les fonctions définies dans math.h.
Ce site y este Les articles de SO-posts disent que l'implémentation mathématique de Java est/était basée sur fdlibm ce qui semble indiquer que cette bibliothèque est la voie à suivre. Quelqu'un a-t-il des informations supplémentaires sur cette bibliothèque que je devrais connaître ?
Il semble que j'ai de nombreuses possibilités, dont les deux suivantes :
- Utiliser la glibc et compiler en mode logiciel . Le problème est que je ne peux utiliser aucun des outils de vérification automatique du système (dans configure). Je dois fournir toutes les informations manuellement. Existe-t-il des drapeaux pour interdire l'utilisation du processeur fp et pour interdire les opérations simd ? fp-without devrait être un début, puis il utilise aussi soft-float s'il compile. Je suppose que le processus de compilation est plus ou moins dépendant d'une décision spécifique pour un hôte (comme arm...).
- Utiliser fdlibm (préféré pour l'instant). Problème : comment puis-je lier mes programmes à ce système ? J'ai besoin des fonctions non-libm comme assert, mais je veux lier mes programmes à mon fdlibm et non au system-libm qui est installé (donc -nodefaultlibs interdira l'utilisation de assert).
