浮動小数点の丸めモード (-float-rounding-mode)

浮動小数点演算の結果を判定する際に考慮する丸めモードの指定

説明

このオプションは Code Prover 解析のみに影響します。

浮動小数点演算の結果を判定する際に考慮する丸めモードを指定します。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [検証の前提条件] ノードを選択してから、このオプションの値を選択します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [検証の前提条件] ノードを選択してから、このオプションの値を選択します。

  • コマンド ラインとオプション ファイル: オプション -float-rounding-mode を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

既定の検証では、最も近い整数への丸めモードが使用されます。

最も近い整数への丸め以外の丸めモードを指定するルーチン (fesetround など) がコードに含まれている場合、丸めモードに [all] を使用します。検証では fesetround の仕様は無視されますが、指定した丸めモードを含むすべての丸めモードが考慮されます。あるいは、拡張精度を使用可能なターゲット (フラグ -mfpmath=387 の使用など) には、丸めモードに [all] を使用します。ただし、Polyspace 解析の結果が実行時の動作と一致する場合は、-ffloat-store などのフラグによって拡張精度を使用するのは避けなければなりません。

そうでない場合、既定の丸めモード [to-nearest] を引き続き使用します。all を指定すると、すべての丸めモードが考慮されるため、過大近似によりオレンジの [オーバーフロー] チェックが多くなることがあります。

設定

既定値: to-nearest

to-nearest

検証で最も近い整数への丸めモードが想定されます。

all

検証で浮動小数点変数を含む各演算に対してすべての丸めモードが想定されます。考慮される丸めモードは、最も近い整数への丸め、ゼロ方向への丸め、正の無限大方向への丸め、負の無限大方向への丸めです。

ヒント

  • Polyspace 解析では、IEEE® 754 規格に準拠する浮動小数点演算が使用されます。たとえば、この演算では、SSE 命令セットに含まれる浮動小数点命令が使用されます。GNU® C フラグ -mfpmath=sse により、この命令セットを使用しなければならないことが指定されます。コードをコンパイルするために、このフラグを指定して GNU C コンパイラを使用すると、Polyspace 解析の結果が実行時の動作と一致します。

    ただし、たとえば GNU C フラグ -mfpmath=387 を使用してコードで拡張精度を使用すると、一部の特殊ケースでは、Polyspace 解析の結果が実行時の動作と一致しないことがあります。こうした特殊ケースについては、polyspaceroot\polyspace\verifier\code_prover_desktop 内の codeprover_limitations.pdf の例を参照してください。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2019a です。

    拡張精度の使用を避ける場合、SSE がサポートされないターゲットでは、-ffloat-store などのフラグを使用します。Polyspace 解析の場合、丸めモードに all を使用して、二重の丸めを考慮します。

  • [オーバーフロー] チェックでは、指定した丸めモードが使用されます。次の表に、丸めモードを変更するとチェックの結果がどのように変わるかについての例を示します。

    丸めモード: to-nearest丸めモード: all

    浮動小数点演算の結果を最も近い値に丸める場合、次のようになります。

    • 1 つ目の加算演算では、eps1 が十分に大きく、FLT_MAX + eps1 に最も近い値が FLT_MAX よりも大きくなります。[オーバーフロー] チェックは、レッドになります。

    • 2 つ目の加算演算では、eps2 が十分に小さく、FLT_MAX + eps2 に最も近い値が FLT_MAX になります。[オーバーフロー] チェックは、グリーンになります。

    #include <float.h>
#define eps1 0x1p103
#define eps2 0x0.FFFFFFp103

float func(int ch) {
    float left_op = FLT_MAX;
    float right_op_1 = eps1, right_op_2 = eps2;
    switch(ch) {
    case 1:
        return (left_op + right_op_1);
    case 2:
        return (left_op + right_op_2);
    default:
        return 0;
    }
}

    [オーバーフロー] チェックで、最も近い整数への丸めモード以外の丸めモードも考慮されます。

    • 1 つ目の加算演算では、最も近い整数への丸めモードの場合、FLT_MAX + eps1 に最も近い値が FLT_MAX よりも大きくなるため加算がオーバーフローします。しかし、負の無限大方向に丸めると、結果が FLT_MAX になるため加算はオーバーフローしません。これらの 2 つの丸めモードの組み合わせにより、[オーバーフロー] チェックはオレンジになります。

    • 2 つ目の加算演算では、最も近い整数への丸めモードの場合、FLT_MAX + eps2 に最も近い値が FLT_MAX になるため加算はオーバーフローしません。しかし、正の無限大方向に丸めると、結果が FLT_MAX よりも大きくなるため加算がオーバーフローします。これらの 2 つの丸めモードの組み合わせにより、[オーバーフロー] チェックはオレンジになります。

    #include <float.h>
#define eps1 0x1p103
#define eps2 0x0.FFFFFFp103

float func(int ch) {
    float left_op = FLT_MAX;
     float right_op_1 = eps1, right_op_2 = eps2;
    switch(ch) {
    case 1:
        return (left_op + right_op_1);
    case 2:
        return (left_op + right_op_2);
    default:
        return 0;
    }
}

コマンド ライン情報

パラメーター: -float-rounding-mode
値: to-nearest | all
既定値: to-nearest
例 (Code Prover): polyspace-code-prover -sources file_name -float-rounding-mode all
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -float-rounding-mode all

バージョン履歴

R2016a で導入

参考

トピック