frontend/testfloat_expr 设计

设计目标

Berkeley TestFloat¹1 J. R. Hauser, Berkeley TestFloat and Berkeley SoftFloat, release 3e. 基于 SoftFloat 参考实现，为每种格式、舍入方向和微小性（tininess）模式生成 IEEE 754 二进制算术的测试向量。本包针对 bin_float 执行这些向量，对结果和异常标志进行逐位精确比较。它是 bin_float 符合性中 IEEE 754 相关结论的依据。本包是纯的；向量生成和进程编排位于 tools/。

数学背景

格式与编码

宽度为 $k$ 、精度为 $p$ 、最大指数为 $e_{\max}$ 的二进制交换格式（binary16： $(16, 11, 15)$ ，binary32： $(32, 24, 127)$ ，binary64： $(64, 53, 1023)$ ，binary128： $(128, 113, 16383)$ ，且 $e_{\min} = 1 - e_{\max}$ ）可表示 $\pm 0$ 、次正规数、正规数、 $\pm\infty$ 和 NaN。其编码 $\operatorname{enc} : \mathbb{F} \to \{0,1\}^k$ 在非 NaN 值上是单射，并区分 $+0$ 与 $-0$ 。TestFloat 将操作数和结果以 $\operatorname{enc}$ 的十六进制形式写出。

正确舍入的运算与标志

对于运算 $\mathrm{op}$ 和操作数 $x$ ，IEEE 754 要求结果为 $r = \circ_\rho(\mathrm{op}(x))$ ，即沿方向 $\rho$ 一次舍入到该格式，并给出一组异常²2 IEEE 754-2019，第 7 条（异常）、第 7.5 条（下溢及两种微小性规则）、第 3.4 条（二进制交换编码）。：

invalid：用于没有有意义结果的运算（例如 $\infty \cdot 0$ 、 $\sqrt{-1}$ 、信号 NaN 操作数、超出范围的整数转换）；
division by zero：由有限操作数得到精确无穷结果时；
overflow：当以无界指数舍入后的结果超过最大有限数时；
underflow：当结果是微小的且不精确时，其中微小性的检测要么在舍入前（ $0 < |\mathrm{op}(x)| < 2^{e_{\min}}$ ），要么在舍入后（ $0 < |\circ_\rho^{\,p,\infty}(\mathrm{op}(x))| < 2^{e_{\min}}$ ，即以无界指数舍入到 $p$ 位）；
inexact：当 $r \ne \mathrm{op}(x)$ 时。

SoftFloat 将它们报告为掩码 $\text{inexact} = 1$ 、 $\text{underflow} = 2$ 、 $\text{overflow} = 4$ 、 $\text{infinite} = 8$ 、 $\text{invalid} = 16$ ，并打印为两位十六进制数字。BinaryFlags::to_testfloat_bits 生成相同的掩码。

通过规则

设 $\hat r$ 为在 format.context(rounding~, tininess~) 中计算得到的 bin_float 结果， $\hat F$ 为其标志， $(e, M)$ 为期望的编码与掩码。对于算术运算，执行器将 $\hat r$ 重新编码到该格式中，得到 $\operatorname{enc}(\hat r)$ 和标志 $F_{\mathrm{enc}}$ ，向量通过的条件是

\Bigl( \bigl(e \text{ is a NaN} \wedge \hat r \text{ is a quiet NaN}\bigr) \vee \operatorname{enc}(\hat r) = e \Bigr) \;\wedge\; \operatorname{mask}(\hat F \cup F_{\mathrm{enc}}) = M .

对于整数转换，值检查替换为：若 $16 \in M$ ，则转换必须报告 invalid，否则必须返回位模式为 $e$ 的整数。对于比较运算，值检查为布尔值相等。标志掩码必须始终相等。

设计决策

逐位精确的结果，按类别比较 NaN

比较编码使得零的符号、次正规数与零之间的选择，以及上溢的精确边界都成为每次测试的一部分。NaN 是例外：IEEE 754 将无效运算产生的 NaN 的载荷与符号交由实现决定（SoftFloat 的默认 NaN 有其自身的位模式），因此期望值为 NaN 时只要求实际结果是静默 NaN。若结果是信号 NaN 则会失败，这正是 IEEE 的要求。

精确的标志掩码

掩码比较是相等比较，因此缺少 inexact 或多出 underflow 都会使向量失败。合并重新编码步骤的标志意味着：若 bin_float 返回了该格式无法精确容纳的值，编码标志会将其暴露出来。

无效转换仅按标志判断

对于无效的整数转换，SoftFloat 返回平台相关的哨兵整数，而 bin_float 返回 None 表示没有整数结果。因此执行器恰好在期望掩码含 invalid 位时要求 None，并忽略哨兵值。其他所有转换都按整数位模式比较。

每个文档一个规格

一次 TestFloat 运行针对一个函数、舍入模式、微小性模式和精确性生成向量。将这些信息一次性记录在 TestFloatSpec 中，可以让向量行保持 TestFloat 自身的格式，因此 testfloat_gen 生成的文件可以原样使用。

按向量索引分片

向量 $k$ 属于分片 $k \bmod n$ 。与 gda_expr 设计中一样，各分片互不相交、覆盖整个文件、大小为 $\lceil (N-i)/n \rceil$ ，且每个向量的结果与其他向量无关，因此合并后的分片计数等于串行计数。

正确性 / 不变式

通过的可靠性。 若期望向量正确，则通过的算术向量表明 bin_float 返回了正确舍入、正确编码的结果，并且恰好触发了 IEEE 规定的异常（NaN 载荷除外）。

计数恒等式。 每个被选中的向量都会被执行： $\text{selected} = \text{passed} + \text{failed}$ ，且 $\text{total} = N$ ，即文档中的向量数。

完全性。 解析将每一行变为一个向量或一条诊断；元数会对照运算进行检查，因此执行时绝不会遇到操作数个数错误的向量。

复杂度。 每个向量执行一次 bin_float 运算和一次编码，与向量数量呈线性关系。

被否决的替代方案

按数值比较解码后的值。 这会把 $-0$ 当作 $+0$ 接受，并掩盖次正规数中的编码错误。
要求与 SoftFloat 的 NaN 位模式一致。 这检验的是 SoftFloat 的实现选择，而不是 IEEE 754。
要求与 SoftFloat 的无效转换哨兵值一致。 这些值因平台而异，而在一个以 None 报告无效结果的 API 中也没有意义。

边界

仅支持 binary16/32/64/128 以及 TestFloatOperation 的十八种运算；不支持格式之间的转换、与十进制字符串之间的转换，也不支持从整数转换。
仅支持五种 IEEE 舍入方向；TestFloat 的 round-to-odd 会被 TestFloatSpec::parse 拒绝。
不比较 NaN 的载荷与符号。
文件读取、向量生成和声明的测试矩阵由 cli/testfloat_expr_cli 和 tools/run_binfloat_interpreter.py 处理。

J. R. Hauser, Berkeley TestFloat and Berkeley SoftFloat, release 3e. ↩
IEEE 754-2019，第 7 条（异常）、第 7.5 条（下溢及两种微小性规则）、第 3.4 条（二进制交换编码）。 ↩