Polyspace 解析の外的制約

Polyspace® は指定されたコードを使用して、変数の範囲やポインターに許容されるバッファー サイズなどの項目について仮定を行います。Polyspace が行う仮定は予想よりも幅広くなる場合があり、その結果、Bug Finder で誤検知が発生する場合や、Code Prover のオレンジ チェックが増加する場合があります。このような誤検知やオレンジ チェックを減らすために、以下に対する外的制約を指定できます。

  • グローバル変数。

  • ユーザー定義関数。

  • スタブ関数。

詳細については、Polyspace 解析の外的制約の指定を参照してください。制限の部分的なリストについては、制約指定の制限を参照してください。

外的制約の効果

以下の関数について考えます。

int getFlooredNumber(int total, int size) {
    return total/size;
}
入力 size は不明であるため、この関数の解析を行うと、次のようになります。

  • Polyspace Code Prover™ では、[ゼロ除算] オレンジ チェックが表示されます。オレンジ チェックは、Code Prover がゼロ除算エラーの可能性があると見なしていることを示しますが、このエラーはすべての実行パスで発生するわけではありません。

  • Polyspace Bug Finder™ では、オプション [システムのすべての入力値を考慮する、さらに厳密なチェックを実行] (-checks-using-system-input-values) を使用すると、[整数のゼロ除算] 欠陥と、この欠陥を引き起こした可能性のある 1 つの入力値 (この場合では size の 0) が表示されます。

    より複雑な例 (条件内部で除算が発生する場合など) では、このオプションを使用しなくても、不明な入力からの欠陥が表示されます。

いずれの場合でも、解析において、そのデータ型から入力変数 size が取り得る値が判別されます。変数 size のデータ型は int であるため、int のサイズが 32 ビットであるターゲットでは、この変数の値の範囲は [-231, 231-1] であると想定されます。

ある入力の値が特定の範囲に限定されることが分かっている場合は、入力に外的制約 (データ範囲指定 (DRS) とも呼ばれる) を指定できます。たとえば上記の例では、size にゼロを含まない範囲を指定すると、以下のようになります。

  • Code Prover で [ゼロ除算] オレンジ チェックが表示されなくなります。

  • Bug Finder で [整数のゼロ除算] 欠陥が表示されなくなります。

コードの外部に存在する設計制約をエミュレートするために、外的制約を指定することができます。たとえば、入力変数が車両速度のような物理量を表す場合、変数値を車両に設計されている速度に制約することができます。

制約指定

Polyspace デスクトップ製品のユーザー インターフェイスで、[制約指定] ウィンドウを介して制約を指定できます。制約は、他のプロジェクトで再利用できる XML ファイルに保存されます。

次の表は、[制約指定] ウィンドウのさまざまな列について説明しています。制約 XML ファイルを直接編集して制約を指定する場合 (たとえば、Polyspace サーバー製品の場合) のために、この表では、ユーザー インターフェイスの列と XML ファイルのエントリの間の対応も示しています。太字で強調表示されている XML エントリは、[制約指定] ウィンドウの対応する列に表示されます。

列設定XML ファイル エントリ
名前

プロジェクト内で、データ範囲を指定できる変数と関数の一覧が表示されます。

この列には、以下の展開可能なメニュー項目が 3 つ表示されます。

  • Global Variables – プロジェクト内のグローバル変数が表示されます。

  • User Defined Functions – プロジェクト内のユーザー定義関数が表示されます。入力を確認するには関数名を展開します。

  • Stubbed Functions – プロジェクト内のスタブ関数の一覧が表示されます。入力と戻り値を確認するには関数名を展開します。

<function name = "funcName" ...>

<scalar name = "arg1" ...>

<pointer name = "arg2" ...>

ファイル変数または関数を格納しているソース ファイルの名前が表示されます。 
<file name = "C:\Project1\Sources\file.c" ...>
属性

変数または関数に関する情報が表示されます。

たとえば、静的変数の場合には static と表示されます。呼び出されない関数の場合は、unused と表示されます。

 
<function name="funcName" attributes="unused" ...>
データ型変数の型が表示されます。 
<scalar name="arg1" complete_type="int32" ...>
main ジェネレーターによる呼び出し

ユーザー定義関数にのみ該当します。

main ジェネレーターがこの関数を呼び出すかどうかを以下のように指定します。

  • MAIN GENERATOR – main ジェネレーターは、-functions-called-in-loop パラメーター (生成されたコード) または -main-generator-calls パラメーター (手書きコード) の値に基づいて、この関数を呼び出す場合があります。

  • NO – main ジェネレーターはこの関数を呼び出しません。

  • YES – main ジェネレーターはこの関数を呼び出します。 

<function name="funcName" main_generator_called="MAIN_GENERATOR" ...>
初期化モード

ソフトウェアが変数にどのように範囲を割り当てるかを指定します。

  • MAIN GENERATOR – 変数範囲は、main ジェネレーターのオプション -main-generator-writes-variables および -no-def-init-glob の設定に基づいて割り当てられます

  • IGNORE – 変数は、範囲が指定されている場合でも、いかなる範囲にも割り当てられません。

  • INIT – 変数は、初期化時にのみ、指定された範囲に割り当てられ、最初の書き込みまでその範囲が維持されます。

  • PERMANENT – 変数は、指定された範囲に永続的に割り当てられます。プログラムの中でこの範囲外の値が変数に割り当てられた場合、警告は発生しません。警告が必要な場合は、globalassert モードを使用します。

ユーザー定義関数は INIT モードのみをサポートします。

スタブ関数は PERMANENT モードのみをサポートします。

C の検証では、グローバル ポインターは MAIN GENERATOR モード、IGNORE モードまたは INIT モードをサポートします。

  • MAIN GENERATOR – ポインターは main ジェネレーターのオプションに従います。

  • IGNORE – ポインターは初期化されません。

  • INIT – ポインターが NULL になるかどうかと、参照されているオブジェクトをどのように割り当てるかを指定します (ポインターの初期化オプションと 初期化の割り当てオプション)。

 
<scalar name="arg1" init_mode="INIT" ...>
初期化範囲

変数の最小値と最大値を指定します。

min および max というキーワードを使って、変数の型の最小値と最大値を示すことができます。たとえば long 型の場合、min および max は、それぞれ -2^31 および 2^31-1 を意味します。

16 進数値を使うこともできます。たとえば、0x12..0x100 です。

変数 enum の場合、列挙子定数を使用した直接の範囲指定はできません。代わりに、定数が表す値を使用してください。

変数 enum の場合、キーワード enum_min および enum_max を使用し、変数が取ることのできる最小値および最大値を表すこともできます。たとえば、以下で定義する型の変数 enum の場合、enum_min は 0 で enum_max は 5 です。

enum week{ sunday, monday=0, tuesday, wednesday, thursday, friday, saturday};

 
<scalar name="arg1" init_range="-1..0"...>
ポインターの初期化

ポインターにのみ該当します。初期化モードで INIT を指定している場合のみ有効です。

ポインターが NULL になるかどうかを指定します。

  • Maybe NULL‎ – ポインターは、場合によって、NULL ポインターになる場合と、ならない場合とがあります。

  • Not NULL – ポインターは、NULL ポインターとして初期化されることは絶対にありません。

  • NULL – ポインターは、NULL として初期化されます。

メモ

C++ プロジェクトには該当しません。制約指定の制限を参照してください。

 
<pointer name="arg1" initialize_pointer="Not NULL"...>
初期化の割り当て

ポインターにのみ該当します。初期化モードで INIT を指定している場合のみ有効です。

参照されているオブジェクトをどのように割り当てるかを指定します。

  • MAIN GENERATOR – 参照されているオブジェクトは、main ジェネレーターによって割り当てられます。

  • NONE – 参照されているオブジェクトは書き込まれません。

  • SINGLE – 参照されているオブジェクトまたは配列の最初の要素が初期化されます。

    ポイントされているオブジェクトの [初期化範囲] 属性を使用してそのオブジェクトを制約することもできます。つまり、ポインターが ptr の場合、ポイントされているオブジェクト*ptr を制約することもできます。ポイントされているオブジェクトが配列である場合、範囲は配列の最初の要素のみに適用されます。

  • MULTI – すべてのオブジェクト (または配列の要素) が初期化されます。

    ポイントされているオブジェクトの [初期化範囲] 属性を使用してそのオブジェクトを制約することもできます。つまり、ポインターが ptr の場合、ポイントされているオブジェクト*ptr を制約することもできます。ポイントされているオブジェクトが配列である場合、範囲は配列のすべての要素に適用されます。

スタブ関数のポインター引数には他の 2 つのオプションを使用できます。

  • SINGLE_CERTAIN_WRITE – 参照されているオブジェクトまたは配列の最初の要素がスタブ関数によって初期化されます。

  • MULTI_CERTAIN_WRITE – 参照されているすべてのオブジェクト (または配列要素) がスタブ関数によって初期化されます。

スタブ関数では、オプション [SINGLE] および [MULTI] は、特定の初期化ではなく可能な初期化を意味します。

メモ

C++ プロジェクトには該当しません。制約指定の制限を参照してください。

 
<pointer name="arg1" init_pointed="MAIN_GENERATOR"...>
割り当て可能オブジェクト数

ポインターにのみ該当します。

ポインターによって参照されるオブジェクトの個数を指定します (参照される各オブジェクトは 1 つの配列と見なされます)。

[初期化の割り当て] パラメーターは、割り当てられたオブジェクトが実際に初期化される個数を指定します。たとえば、次のコードを考えます。

void func(int *ptr) {
    assert(ptr[0]==1);
    assert(ptr[1]==1);
}
以下の制約を指定するとします。

  • ptr の [初期化の割り当て] を MULTI に設定し、[割り当て可能オブジェクト数] を 2 に設定。

  • *ptr の [初期化範囲] を 1..1 に設定。

どちらのアサーションもグリーンです。以下の制約を指定するとします。

  • ptr の [初期化の割り当て] を SINGLE に設定。

  • *ptr の [初期化範囲] を 1..1 に設定。

2 番目のアサーションはオレンジになります。ptr が指す最初のオブジェクトのみが 1 に初期化されます。最初のオブジェクト以外のオブジェクトは全範囲を取る可能性があります。

ファイル サイズが不明な非常に大きな配列内の任意の場所をポインターで指すことができることを指定するには、キーワード "max " を使用します。解析結果を見ると、そのポインターのオフセットとバッファーのサイズが非常に大きくなっていることが分かります。オフセットとバッファーのサイズは、使用するターゲット プロセッサ タイプのポインター サイズやその他の特性によって異なります。Polyspace がこの方法を使用して作成する最大のオブジェクトは、2^27-1 バイト (134217726 バイト) のバッファーです。

メモ

C++ プロジェクトには該当しません。制約指定の制限を参照してください。

 
<pointer name="arg1" number_allocated="10"...>
グローバル アサートグローバル初期化のとき、および各割り当ての後に、変数にアサート チェックを実行するかどうかを指定します。 
<scalar name="glob" global_assert="YES"...>
グローバル アサート範囲チェックする範囲の最小値と最大値を指定します。 
<scalar name="glob" assert_range="0..200"...>
コメントDRS 値の理由など、入力の説明です。 
<scalar name="glob" comment="Speed Range"...>

制約指定の制限

次のタイプの制約は、制約指定インターフェイスを使用して指定することはできません。これらの制限の一部は、回避するために独自のスタブと main() を定義できます。詳細は、手動スタブと手動の main() 関数を使用した Polyspace 解析の変数範囲の制約を参照してください。

制約指定インターフェイスでは、次の制約はサポートされていません。

  • C++ では、関数のポインター引数または参照引数を制約することはできません。

    多態性により、C++ のポインターまたは参照はクラス階層内の複数のクラスのオブジェクトを指す可能性があり、異なるコンストラクターを呼び出すことが必要になる場合があります。制約指定の予備解析で、制約するオブジェクト タイプや呼び出すコンストラクターを判別することはできません。

  • 関数の戻り値をその入力に関連付ける制約は指定できません。制約には一定の範囲のみを指定できます。

  • 制約には複数の範囲を指定できません。たとえば、関数引数が値 -1 か、範囲 [1,100] の値のどちらかをもつように指定することはできません。代わりに、範囲 [-1,100] を指定するか、もしくは値 -1 を 1 回、範囲 [1,100] を 1 回指定して、2 回の別々の分析を実行します。

  • 1 つの共用体に属する異なるフィールドに別々の制約を指定することはできません。

  • 複数レベルの間接参照でアクセスされるオブジェクトを制約することはできません。たとえば、ポインターには制約を指定できますが、ポインターへのポインターには制約を指定できません。

参考

トピック