Luna Flow
简体中文

testfloat_expr 教程

本教程介绍如何针对 bin_float 运行 Berkeley TestFloat 向量。TestFloat 向量文件由 testfloat_gen 针对某一个函数（如 f64_mulAdd）在某一种舍入模式下生成；每一行以十六进制给出操作数、预期结果和预期异常标志。你用 TestFloatSpec 描述函数，解析各行，执行它们，并读取摘要。命令行运行器是 testfloat_expr_cli。

快速入门

将该包添加到 moon.pkg：

import {
  "Luna-Flow/floating/frontend/testfloat_expr",
}

在 binary64 中检验 1.5×2=31.5 \times 2 = 3：

///|
test "quick start" {
  let spec = @testfloat_expr.TestFloatSpec::parse("f64_mul", "rnear_even").unwrap()
  let vectors =
    #|3FF8000000000000 4000000000000000 4008000000000000 00
    #|
  let document = @testfloat_expr.parse_testfloat("mul.tv", vectors, spec).unwrap()
  let summary = @testfloat_expr.execute_document(document)
  inspect(summary.passed_cases(), content="1")
  inspect(summary.success(), content="true")
}

最后一个字段是 SoftFloat 标志掩码：01 不精确，02 下溢，04 上溢，08 除以零（无穷），10 无效。

日常任务

值和标志都会被检查

编码结果或标志掩码只要有一个不同，该向量即失败：

///|
test "flag mismatch" {
  let spec = @testfloat_expr.TestFloatSpec::parse("f16_add", "rnear_even").unwrap()
  // 1 + 2^-11 is a tie in binary16 and rounds to 1, inexact
  let vectors =
    #|3C00 1000 3C00 01
    #|3C00 1000 3C00 00
    #|
  let summary = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("add.tv", vectors, spec).unwrap(),
  )
  let messages = summary.results().map(r => r.id() + " " + r.message())
  inspect(
    messages.join("; "),
    content="f16_add:1 ; f16_add:2 flags mismatch: expected 0, actual 1",
  )
}

id 由函数名和行号组成。

NaN 结果

当预期结果为 NaN 时，任何静默 NaN 都可接受，因为 IEEE 754 并未规定生成的 NaN 的载荷或符号。但标志仍须匹配：

///|
test "nan results" {
  let spec = @testfloat_expr.TestFloatSpec::parse("f32_mul", "rnear_even").unwrap()
  // inf * 0 is invalid; SoftFloat's default NaN is FFC00000
  let vectors =
    #|7F800000 00000000 FFC00000 10
    #|
  let summary = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("nan.tv", vectors, spec).unwrap(),
  )
  inspect(summary.passed_cases(), content="1")
}

到整数的转换与 exact 变体

对于 to_i32、to_i64、to_ui32 和 to_ui64，结果字段是十六进制的整数。使用 exact=true（对应 TestFloat 的 -exact）时，不精确的转换还会引发不精确标志。无效转换只通过其标志检查：

///|
test "integer conversions" {
  let plain = @testfloat_expr.TestFloatSpec::parse("f64_to_i32", "rnear_even").unwrap()
  let exact = @testfloat_expr.TestFloatSpec::parse(
    "f64_to_i32",
    "rnear_even",
    exact=true,
  ).unwrap()
  // 1.5 -> 2; NaN -> invalid (the value field is SoftFloat's sentinel)
  let plain_rows =
    #|3FF8000000000000 00000002 00
    #|7FF8000000000000 7FFFFFFF 10
    #|
  let exact_rows =
    #|3FF8000000000000 00000002 01
    #|
  let a = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("plain.tv", plain_rows, plain).unwrap(),
  )
  let b = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("exact.tv", exact_rows, exact).unwrap(),
  )
  inspect(a.passed_cases(), content="2")
  inspect(b.passed_cases(), content="1")
}

比较

比较函数预期结果为 0 或 1。发信号的谓词（eq_signaling、le、lt）对任何 NaN 操作数都引发无效；静默谓词（eq、le_quiet、lt_quiet）只对信号 NaN 引发：

///|
test "comparisons" {
  let le = @testfloat_expr.TestFloatSpec::parse("f64_le", "rnear_even").unwrap()
  let le_quiet = @testfloat_expr.TestFloatSpec::parse("f64_le_quiet", "rnear_even").unwrap()
  let row =
    #|7FF8000000000000 3FF0000000000000 0 10
    #|
  let quiet_row =
    #|7FF8000000000000 3FF0000000000000 0 00
    #|
  let signaling = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("le.tv", row, le).unwrap(),
  )
  let quiet = @testfloat_expr.execute_document(
    @testfloat_expr.parse_testfloat("le_quiet.tv", quiet_row, le_quiet).unwrap(),
  )
  inspect(signaling.passed_cases(), content="1")
  inspect(quiet.passed_cases(), content="1")
}

分片

RunOptions 从索引 i 开始，每隔 n 个运行一个向量，因此 n 个进程可以共享同一个文件：

///|
test "shards" {
  let spec = @testfloat_expr.TestFloatSpec::parse("f16_add", "rnear_even").unwrap()
  let vectors =
    #|3C00 3C00 4000 00
    #|0001 0001 0002 00
    #|7C00 FC00 7E00 10
    #|8000 0000 0000 00
    #|3C00 BC00 0000 00
    #|
  let document = @testfloat_expr.parse_testfloat("add.tv", vectors, spec).unwrap()
  let second = @testfloat_expr.execute_document(
    document,
    options=@testfloat_expr.RunOptions::new(shard_count=2, shard_index=1),
  )
  inspect(second.total_cases(), content="5")
  inspect(second.selected_cases(), content="2")
  inspect(second.passed_cases(), content="2")
}

深入了解

  • 生成向量。 just conformance fetch binary 安装固定版本的 SoftFloat 和 TestFloat 源码，just conformance run binary --level 1 生成并执行完整矩阵（所有格式、运算、舍入模式以及两种微小性模式）；参见验证。
  • 微小性。 向 TestFloatSpec::parse 传入 tininess="before"，以匹配用 -tininessbefore 生成的向量；默认是舍入后判定。
  • 函数名。 spec 接受 TestFloat 名称：f16_、f32_、f64_ 或 f128_ 后接 add、sub、mul、div、sqrt、mulAdd、rem、roundToInt、to_i32、to_i64、to_ui32、to_ui64、eq、le、lt、eq_signaling、le_quiet 或 lt_quiet。

常见陷阱

  • 每个文档只对应一个函数。 spec 作用于每一行；请拆分混合文件。
  • 舍入参数不可省略。 rem 和比较运算会忽略它，但 TestFloatSpec::parse 仍需要一个有效名称，例如 rnear_even。
  • 不支持 rodd。 只接受 IEEE 的五种方向。
  • exact 很重要。 来自 -exact 运行的向量中，roundToInt 和整数转换带有不精确标志；请用 exact=true 解析它们。

后续步骤