testfloat_expr_cli 设计

设计目标

每个进程以生成某个 TestFloat 测试向量文件时所用的确切配置执行该文件,使工具能够通过有界大小的文件和并行进程处理数以亿计的测试向量。

数学背景

一个 TestFloat 任务是一个元组(格式、操作、舍入、微小性(tininess)、精确性、级别、种子)。其测试向量按照 testfloat_expr 设计中的通过规则检查。将一个任务的向量流拆分为块 V1,V2,…V_1, V_2, \dots,再将每个块拆分为分片,这构成了向量的一个划分;而每个向量的判定与其他向量无关,因此任务的计数器就是各块和各分片上计数之和。

设计决策

配置作为选项,测试向量保持原样

函数、舍入、微小性和精确性都是命令行选项,与 testfloat_gen 自身的标志一一对应。测试向量文件完全保持 TestFloat 的格式,因此生成器的输出可以直接重定向到文件并执行,无需转换。

每次调用处理一个文件

一个进程处理一个块。Python 驱动程序(tools/run_binfloat_interpreter.py)将生成器的输出流写入块文件,对每个块运行运行器,并将块偏移加到报告的 FUNCTION:LINE id 上。有界的块使最大的 mulAdd 任务也能保持恒定内存。

JSON 与分片的共享选项

--json 和分片选项来自 internal/runner_cli,因此其行为与 GDA 运行器完全相同。

正确性 / 不变式

  • 当且仅当没有被选中的测试向量失败时退出码为 0;selectedCases = passedCases + failedCases。
  • 规格错误(TestFloatSpec::parse)或解析错误会在执行任何测试向量之前以 2 退出。

被否决的替代方案

  • 将配置编码到测试向量文件中。 这需要改写 TestFloat 的输出。
  • 从 MoonBit 中运行 testfloat_gen。 进程管理属于工具的职责;运行器保持可移植、可测试。

边界

  • 不负责测试向量生成、分块或 id 重映射(由 Python 工具负责)。
  • 格式和操作与 frontend/testfloat_expr 相同。