無効なシフト演算チェックのレビューと修正

このトピックでは、Polyspace^® Code Prover™ で [無効なシフト演算] チェックの結果を体系的にレビューする方法を説明します。

[無効なシフト演算] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、無効なシフト演算を参照してください。

特にオレンジチェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。

すべてのチェックに適用される一般的なワークフローについては、Polyspace デスクトップユーザーインターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

手順 1: チェック情報の解釈

レッドまたはオレンジの [無効なシフト演算] チェックを選択します。[結果の詳細] ペインから以下の情報を取得します。

チェックがレッドまたはオレンジである理由。考えられる理由は以下のとおりです。
- シフト量が許容される範囲外の可能性がある。
  また、シフト量の許容される範囲が示される。
- 左シフトの左側のオペランドが負である可能性がある。
以下の例では、レッドエラーはシフト量が許容範囲外であるために発生します。シフト量の許容範囲は 0 ～ 31 です。

考えられる解決方法: レッドチェックまたはオレンジチェックを回避するには、シフト量が範囲内である場合のみシフト演算を実行します。
```
if(shiftAmount < (sizeof(int) * 8))
  /* Perform the shift */
else
  /* Error handling */
```
チェックに対して考えられる根本原因 (ソフトウェアによってこの情報が提供される場合)。
前述の例では、スタブ関数 getVal が考えられる原因として識別されています。
考えられる解決方法: オレンジチェックを回避するには、getVal の戻り値を制約します。たとえば、getVal が 0..10 などの特定の範囲内で値を返すよう指定します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。

手順 2: チェックの根本原因の判定

シフト量が範囲外の場合、シフト変数のデータフローをトレースします。シフト変数を制約できる適切なポイントを特定します。
次の例では、shiftAmount のデータフローをトレースします。
```
void func(int val) {
	int shiftAmount = getShiftAmount();
	int res = val >> shiftAmount;
}
```
getShiftAmount は全範囲の値を返す場合があります。
考えられる解決方法:
- shiftAmount が 0 から (sizeof(int))*8 - 1 の間である場合のみシフト演算を実行します。
- getShiftAmount の定義がない場合、getShiftAmount の戻り値を getShiftAmount の本体内または Polyspace の [制約指定] インターフェイスで制約します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。
左シフト演算の左側のオペランドに負の可能性がある場合、左側のオペランド変数のデータフローをトレースします。左側のオペランド変数を制約できる適切なポイントを特定します。
次の例では、shiftAmount のデータフローをトレースします。
```
void func(int shiftAmount) {
	int val = getVal();
	int res = val << shiftAmount;
}
```
getVal は全範囲の値を返す場合があります。
考えられる解決方法:
- val が正である場合のみ、シフト演算を実行します。
- getVal の定義がない場合、getVal の戻り値を getVal の本体内または Polyspace の [制約指定] インターフェイスで制約します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。
- Polyspace で演算を許可する場合、解析オプション [左シフトで負のオペランドを許可] を使用します。左シフトで負のオペランドを許可 (-allow-negative-operand-in-shift)を参照してください。

データフローをトレースするには、チェックを選択し、[結果の詳細] ペインの情報を確認します。

[結果の詳細] ペインでチェックにつながる命令の順序が表示される場合、各命令を選択します。
[結果の詳細] ペインに、そのチェックの考えられる原因の行番号が表示される場合、[ソース] ペインを右クリックします。[行に移動] を選択します。

そうしない場合は、次のようになります。

トレースする変数について前の書き込み操作を検索します。
前の書き込み操作で、逆にトレースするために新しい変数を特定します。
書き込み操作に含まれる変数の上にカーソルを置き、その値を確認します。これらの値は、トレースする変数を判断する際に役立ちます。
新しい変数の前の書き込み操作を検索します。制約を指定するポイントを特定するまでこの方法で逆にトレースを続行します。

変数に応じて、以下のナビゲーションショートカットを使用し、前のインスタンスを検索します。以下の手順は、Polyspace ユーザーインターフェイスでのみ実行できます。

変数変数の前のインスタンスの検索方法

変数	変数の前のインスタンスの検索方法
ローカル変数	次のいずれかの方法を使用してください。変数の検索。変数を右クリックします。[すべての参照を検索] を選択します。変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。 [検索] ペインで前のインスタンスを選択します。ソースコードの参照。 [ソース] ペインで変数をダブルクリックします。変数のすべてのインスタンスは強調表示されます。上にスクロールして前のインスタンスを検索します。
グローバル変数変数を右クリックします。オプション [変数アクセスビューで表示] が表示される場合、変数はグローバル変数です。	オプション [変数アクセスビューで表示] を選択します。 [変数アクセス] ペインでは、変数の現在のインスタンスが表示されます。このペインで、変数の前のインスタンスを選択します。変数の書き込み操作はで示され、読み取り操作はで示されます。
関数の戻り値 ret=func();	関数定義を検索します。 [ソース] ペインの `func` を右クリックします。オプションが存在する場合、[定義に移動] を選択します。Polyspace で定義を利用できない場合は、オプションを選択すると関数宣言に移動します。 `func` の定義では、各 `return` ステートメントを特定します。関数が返す変数が逆にトレースするための新しい変数です。

ローカル変数

次のいずれかの方法を使用してください。

変数の検索。
1. 変数を右クリックします。[すべての参照を検索] を選択します。
  変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。
2. [検索] ペインで前のインスタンスを選択します。
ソースコードの参照。
1. [ソース] ペインで変数をダブルクリックします。
  変数のすべてのインスタンスは強調表示されます。
2. 上にスクロールして前のインスタンスを検索します。

グローバル変数

変数を右クリックします。オプション [変数アクセスビューで表示] が表示される場合、変数はグローバル変数です。

オプション [変数アクセスビューで表示] を選択します。
[変数アクセス] ペインでは、変数の現在のインスタンスが表示されます。
このペインで、変数の前のインスタンスを選択します。
変数の書き込み操作はで示され、読み取り操作はで示されます。

関数の戻り値

ret=func();

関数定義を検索します。
[ソース] ペインの func を右クリックします。オプションが存在する場合、[定義に移動] を選択します。Polyspace で定義を利用できない場合は、オプションを選択すると関数宣言に移動します。
func の定義では、各 return ステートメントを特定します。関数が返す変数が逆にトレースするための新しい変数です。

任意の操作に含まれる変数が前の操作に関連しているかどうかを判断することもできます。コード内の変数間の関係の検出を参照してください。

手順 3: チェックの一般的な原因の検索

[無効なシフト演算] チェックの一般的な原因を確認します。

正しいターゲットプロセッサタイプを指定したかどうかを確認します。ターゲットプロセッサタイプは特定の変数の型に許容されるビット数を決定します。
許容されるビット数を決定するには、次の手順に従います。
1. 変数定義に移動します。変数の型に注意してください。
  オプションが存在する場合、変数を右クリックし、[定義に移動] を選択します。
2. 型で許容されるビット数を確認します。
  結果に使用される構成では、[ターゲットおよびコンパイラ] ノードを選択します。[ターゲットプロセッサタイプ] リストの隣の [編集] ボタンをクリックします。
負のオペランドを使用する左シフトについては、代わりに右シフトの実行を意図していたかどうかを確認します。

手順 4: Polyspace の前提条件へのチェックをトレース

コードの前方で発生する Polyspace 前提条件にオレンジチェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。Polyspace ユーザーインターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。

たとえば、未定義の関数から変数を取得し、変数に左シフトを実行するとします。ここで、次のようにします。

Polyspace は、関数が負の値を返す可能性があると仮定します。
左シフト演算は負の値で発生する可能性があり、そのため演算に対してオレンジチェックとなります。
関数が正の値を返すとわかっている場合、コメントおよび正当化情報を追加し、コードを変更しなかった理由を説明します。

詳細については、Code Prover 解析の前提条件を参照してください。