寻找math.h函数的纯c版本(没有协处理器支持)

Question

我必须使用静态验证C源的一些(半)自动验证软件(CBMC (链接)).支持浮点,但没有所有数学函数的定义.尝试检查是否可以用它来检查数字软件.

所以我需要这些功能.我在找一些math.h没有协处理器使用的定义(例如sqrt,pow,其余部分tan; int/ float/ double).

当我在一些Linux发行版附带的libc(也许现在是eglibc)中查找它时,我总是达到一个点,其中有一些处理器内在函数意味着硬件sqrt函数.

第1部分:搜索软件实现

我需要的是一个支持数学函数的库,具有以下特征:

• 支持IEEE浮点数,但纯粹基于整数运行的库也会很棒,也许更好.
• 正确性是一个关键因素.(隐藏在某些来源的特殊情况的已知错误并不那么酷).根据IEEE-754(例如sqrt的规则),结果也应该是正确的.
• 不使用协处理器调用.纯软件.C是首选,但asm也应该没问题.

到目前为止,我搜索了各种libc实现,特别是有关嵌入式系统的实现.我认为这些库中的大多数都是针对编译程序的可移植性和大小,但很难说它们是否使用特定于处理器的指令.

• **fdlibm乍一看似乎有一些纯软件定义.我会进一步检查.但是在源代码中提到了一些错误(代码不是标准的).
• **newlib似乎带来了相同的定义(基于sun microsystems的代码).但是我现在不能肯定地说这些软件版本是否总是被使用,所以可能会有一些我目前看不到的协处理器调用(参见第2部分).
• **uClibc似乎与newlib共享特征.

第2部分:了解这些实现的结构

• 有人能给我一些关于这些数学库结构的简短介绍.他们如何调度各种版本(例如特定的协处理器)？

• 这些不同前缀在文件名中的含义是什么？e_sqrt.c,k_sin,s_sin？

我会很高兴听到一些图书馆这可能是对我有用.我宁愿选择一个库,但是当它有必要时,也可以寻找一些单一的函数实现并构建一个小型库.我不会使用math.h中定义的所有函数.

这个和这个 SO帖子都说Java Math Implementation是基于fdlibm的,这听起来这个库是可行的.有关这个库的更多信息的人我应该知道吗？

似乎我有很多可能性,包括以下两个:

1. 使用glibc并在软件模式下编译.问题是,我不能使用任何自动系统检查工具(在configure中).我必须手动提供所有信息.是否有任何标志禁止使用fp-coprocessor并禁止simd操作？fp-without应该是一个开头,然后如果编译它也使用soft-float.我希望编译过程或多或少依赖于主机的特定决策(如arm ......).
2. 使用fdlibm(目前首选).问题:如何将程序链接到它？我需要像assert这样的非libm函数,但想要链接我的fdlibm而不是安装的system-libm(所以-nodefaultlibs将禁止使用assert).

Answer 1

在glibc/sysdeps/ieee754中有一个完整的IEEE-754软件实现.当您编译库时,它可能会自动替换ia64/fpu/e_acosf.S某个函数的体系结构特定版本(例如),但整个库也在软件中实现.