testfloat_expr チュートリアル

このチュートリアルでは、Berkeley TestFloat のベクトルを bin_float に対して実行する方法を説明します。TestFloat のベクトルファイルは、f64_mulAdd のような 1 つの関数について、1 つの丸めモードのもとで testfloat_gen により生成されます。各行にはオペランド、期待される結果、期待される例外フラグが 16 進で記述されています。TestFloatSpec で関数を記述し、行を構文解析して実行し、要約を読みます。コマンドラインランナーは testfloat_expr_cli です。

クイックスタート

moon.pkg にパッケージを追加します。

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

binary64 で $1.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 は inexact、02 はアンダーフロー、04 はオーバーフロー、08 はゼロ除算（無限大）、10 は invalid を表します。

日常的なタスク

値とフラグの両方が検査される

エンコードされた結果かフラグマスクのどちらかが異なれば、そのベクトルは失敗です。

///|
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 の場合は、任意の quiet 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 では、結果フィールドは 16 進の整数です。exact=true（TestFloat の -exact）では、正確でない変換は inexact フラグも発生させます。無効な変換はフラグだけで検査されます。

///|
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 オペランドに対して invalid を発生させ、quiet な述語（eq、le_quiet、lt_quiet）は signaling 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 個のプロセスで 1 つのファイルを分担できます。

///|
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 は完全なマトリクス（すべての形式、演算、丸めモード、両方の極小性モード）を生成して実行します。検証 を参照してください。
• 極小性。 -tininessbefore で生成されたベクトルに合わせるには、TestFloatSpec::parse に tininess="before" を渡します。既定は丸め後判定です。
• 関数名。 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 のいずれかを付けます。

よくある落とし穴

• 1 つの文書につき 1 つの関数。 spec はすべての行に適用されるため、混在したファイルは分割してください。
• 丸めの引数は省略できません。 rem と比較関数はこれを無視しますが、それでも TestFloatSpec::parse には rnear_even のような有効な名前が必要です。
• rodd はサポートされません。 受け付けるのは IEEE の 5 つの方向だけです。
• exact は重要です。 -exact で実行して得たベクトルには、roundToInt と整数変換について inexact フラグが含まれます。exact=true を指定して構文解析してください。

次のステップ

• すべての項目については testfloat_expr API。
• 正確な合格規則については testfloat_expr 設計。
• 公開されている TestFloat に関する主張については bin_float の適合性。