Мне приходится работать с некоторым (полу-) автоматическим программным обеспечением для проверки (CBMC (link)), которое статически работает с исходниками C. Поддерживаются числа с плавающей запятой, но нет определений для всех математических функций. Попытка проверить, можно ли с его помощью проверить числовое программное обеспечение.
Так что мне нужны эти функции. Я ищу некоторые math.h определения без использования сопроцессора (например, sqrt, pow, остаток, tan; int/float/double).
Когда я искал его в libc, поставляемой с некоторыми дистрибутивами Linux (возможно, теперь eglibc), я всегда доходил до точки, где есть некоторые внутренние компоненты процессора, означающие, например, аппаратную функцию sqrt.
Часть 1: поиск программных реализаций
Мне нужна библиотека, поддерживающая математические функции со следующими характеристиками:
- IEEE Floating-Point поддерживается, но библиотека, работающая исключительно с целыми числами, тоже была бы отличной, а может быть, и лучше.
- Правильность – решающий фактор. (известные баги для особых случаев, скрытые в некоторых источниках, не так уж и круты). Результаты также должны быть правильными с точки зрения IEEE-754 (например, правила для sqrt).
- Не использовать вызовы сопроцессора. Чистый софт. C предпочтительнее, но asm тоже подойдет.
До сих пор я немного искал различные реализации libc, особенно касающиеся встроенных систем. Я думаю, что большинство этих библиотек нацелены на переносимость и размер скомпилированных программ, но трудно сказать, используют ли они инструкции для конкретного процессора.
- ** На первый взгляд кажется, что fdlibm имеет чисто программные определения. Я проверю это дальше. Но есть некоторые ошибки, упомянутые в исходниках (код не стандартный).
- **newlib, по-видимому, содержит те же определения (на основе кода микросистем Sun). Но на данный момент я не могу точно сказать, всегда ли используются эти версии программного обеспечения, так что, возможно, есть какие-то вызовы сопроцессора, которых я не вижу в данный момент (см. часть 2).
- **uClibc похоже имеет те же характеристики, что и newlib.
Часть 2: понимание структуры этих реализаций
Может ли кто-нибудь дать мне краткое введение в структуру этих математических библиотек. Как они отправляют различные версии (например, конкретный сопроцессор)?
И что означают эти разные префиксы в именах файлов.
e_sqrt.c,k_sin,s_sin?
Я был бы рад услышать о некоторых библиотеках, которые могут оказаться полезными для меня. Я бы предпочел брать библиотеку в том виде, в каком она есть, но когда это необходимо, также можно поискать какие-то отдельные реализации функций и создать небольшую библиотеку. Я не буду использовать все функции, определенные в math.h.
Это и это SO-сообщения говорят, что реализация Java Math / был основан на fdlibm, что звучит так, будто эта библиотека — то, что нужно. Кто-нибудь, у кого есть дополнительная информация об этой библиотеке, которую я должен знать?
Кажется, у меня есть много возможностей, включая следующие два:
- Используйте glibc и скомпилируйте в программном режиме. Проблема в том, что я не могу использовать какие-либо инструменты автоматической проверки системы (в конфигурации). Приходится вводить всю информацию вручную. Есть ли флаги для запрета использования fp-сопроцессора и запрета simd-операций? fp-without должен быть началом, тогда он также использует soft-float, если он компилируется. Я ожидаю, что процесс компиляции более или менее зависит от конкретного решения хоста (например, руки...).
- Используйте fdlibm (на данный момент предпочтительнее). Проблема: как связать с ним свои программы? Мне нужны не-libm-функции, такие как assert, но я хочу связать с моей fdlibm, а не с установленной системной libm (поэтому -nodefaultlibs запретит использование assert).
