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

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

6年前关闭。




Improve this question




我必须使用一些静态处理 C 源代码的(半)自动验证软件 (CBMC (link))。支持浮点，但没有对所有数学函数的定义。尝试是检查是否可以用它检查数值软件。

所以我需要这些功能。 我在找一些 math.h不使用协处理器的定义 (例如 sqrt 、 pow 、余数、 tan ； int/float/double )。

当我在一些 linux 发行版(现在可能是 eglibc)附带的 libc 中寻找它时，我总是达到一个点，其中有一些处理器内部函数，例如硬件 sqrt 函数。

第 1 部分:搜索软件实现

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

支持 IEEE 浮点数，但纯粹对整数进行运算的库也很棒，也许更好。

正确性是一个关键因素。 (隐藏在某些来源中的特殊情况的已知错误并不那么酷)。根据 IEEE-754(例如 sqrt 规则)，结果也应该是正确的。

不使用协处理器调用。纯软件。 C 是首选，但 asm 也应该没问题。

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

** fdlibm乍一看似乎有一些纯软件定义。我将进一步检查这一点。但是在源代码中提到了一些错误(代码不是标准的)。

** newlib似乎带来了相同的定义(基于太阳微系统的代码)。但是我目前不能确定是否总是使用这些软件版本，因此可能有一些我目前看不到的协处理器调用(参见第 2 部分)。

** uClibc似乎与 newlib 共享特性。

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

有人能给我简单介绍一下这些数学库的结构吗？他们如何分派(dispatch)各种版本(例如特定的协处理器)？

以及文件名中这些不同前缀的含义是什么。 e_sqrt.c , k_sin , s_sin ?

我很高兴听到一些图书馆 可以 对我有用。我更愿意拿一个库来，但在必要的时候，也可以寻找一些单一的函数实现，并建立一个小库。我不会使用 math.h 中定义的所有函数。

This和 this SO 帖子说 Java 数学实现是/曾经基于 fdlibm 这听起来这个图书馆是要走的路。任何有关于这个图书馆的更多信息的人我应该知道吗？

似乎我有很多可能性，包括以下两种:

使用 glibc 并在软件模式下编译 .问题是，我不能使用任何自动系统检查工具(在配置中)。我必须手动提供所有信息。是否有任何标志禁止使用 fp 协处理器和禁止 simd 操作？ fp-without 应该是一个开始，然后它也使用 soft-float 如果它编译。我希望编译过程或多或少取决于主机的特定决定(例如 arm ...)。

使用 fdlibm (目前首选)。问题:如何将我的程序链接到它？我需要像assert这样的非libm函数，但想要链接到我的fdlibm而不是安装的system-libm(所以-nodefaultlibs将禁止使用assert)。

Answer 1

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