コンピュータ サイエンスにおいて、確実な代入分析とは、変数または場所が使用される前に必ず代入されることを保守的に保証するために コンパイラが使用するデータ フロー分析です。

モチベーション

CおよびC++プログラムでは、初期化されていない変数の読み取りによって生じる非決定的な動作が、特に診断が難しいエラーの原因となります。この動作は、プラットフォーム、ビルド、さらには実行ごとに異なる場合があります。

この問題を解決する一般的な方法は 2 つあります。1 つは、すべてのロケーションが読み取られる前に書き込まれるようにすることです。ライスの定理により、この問題は一般にすべてのプログラムに対して解決できるわけではないことが証明されています。ただし、この制約を満たすプログラムのみを受け入れ、一部の正しいプログラムを拒否する保守的な (不正確な) 解析を作成することは可能です。確実な代入解析はそのような解析です。Java [1]およびC# [2]プログラミング言語仕様では、解析が失敗した場合にコンパイラがコンパイル時エラーを報告することを要求しています。どちらの言語も、非常に詳細に記述された特定の形式の解析を必要とします。Java では、この解析は Stärk ら[3]によって形式化され、一部の正しいプログラムが拒否されるため、不要な代入を明示的に導入するように変更する必要があります。C# では、この解析は Fruja によって形式化され、すべての制御フロー パスに沿って代入されたすべての変数が確実に代入されていると見なされるという意味で、正確かつ健全です。[4] Cyclone言語では、 Cプログラムの移植を容易にするために、ポインタ型の変数に対してのみ、プログラムが明確な代入解析を通過することを要求します。[5]

問題を解決する2つ目の方法は、すべての場所を定義時点で固定かつ予測可能な値に自動的に初期化することですが、これは新たな代入を発生させ、パフォーマンスを低下させる可能性があります。この場合、明確な代入分析によってコンパイラの最適化が可能になり、冗長な代入（代入の後に他の代入のみが続き、その間に読み込みが発生する可能性がない代入）を排除できます。この場合、プログラムが拒否されることはありませんが、分析によって明確な代入が認識されないプログラムには、冗長な初期化が含まれる可能性があります。共通言語基盤はこのアプローチに依存しています。[6]

用語

変数または場所は、プログラムの任意の時点で、次の 3 つの状態のいずれかにあると言えます。

  • 確実に割り当て済み: 変数は確実に割り当て済みであることがわかっています。
  • 確実に未割り当て: 変数は未割り当てであることが確実です。
  • 不明: 変数は割り当てられているか、割り当てられていない可能性があります。分析ではどちらであるかを判断できるほど正確ではありません。

分析

以下は、C#の手続き内（単一メソッド）における確実な代入解析のFrujaによる形式化に基づいています。この解析は、すべてのローカル変数が使用前に確実に代入されることを保証する役割を果たします。[4]この解析は、確実な代入解析とブール値の定数伝播を同時に行います。5つの静的関数を定義します。

様々な式や文におけるこれらの関数の値を、構文上の部分式における関数の値を用いて定義するデータフロー方程式を提供します。ここでは、goto、break、continue、return、例外処理文は存在しないものとします。以下に、これらの方程式の例をいくつか示します。

  • 確実に割り当てられた変数の集合に影響を与えない式または文e ： after（e）= before（e）
  • eを代入式loc = vとします。すると、before ( v ) = before ( e )、after ( e ) = after ( v ) U {loc}となります。
  • eを式trueとすると、true ( e ) = before ( e ) かつfalse ( e ) = vars ( e ) となります。言い換えれば、e がfalseと評価された場合、 eはfalse と評価されないため、すべての変数は（空虚に）確実に代入されます。
  • メソッドの引数は左から右に評価されるため、before( arg i  + 1 ) = after( arg i ) となります。メソッドの実行が完了すると、出力パラメータが確実に代入されます。
  • sを条件文if ( e ) s 1 else s 2とします。すると、 before ( e ) = before ( s )、before ( s 1 ) = true ( e )、before ( s 2 ) = false ( e )、 after( s ) = after( s 1 ) は after( s 2 ) と交差します。
  • s をwhile ループ文while ( e ) s 1とします。すると、 before( e ) = before( s )、 before( s 1 ) = true( e )、 after( s ) = false( e ) となります。
  • 等々。

メソッドの開始時点では、ローカル変数は明確に代入されていません。検証ツールは抽象構文木を繰り返し反復処理し、データフロー方程式を用いてセット間の情報を移行し、最終的に固定点に到達します。次に、検証ツールはローカル変数を使用するすべての式のbeforeセットを調べ、その変数が含まれていることを確認します。

このアルゴリズムは、 goto、break、continue、returnといった制御フロージャンプや例外処理の導入によって複雑化しています。これらのジャンプの対象となる文は、ジャンプ元で確実に代入された変数の集合と、そのbefore setが交差している必要があります。これらのジャンプが導入されると、結果として得られるデータフローには、次の例のように複数の固定点が含まれる場合があります。 

 整数i = 1 ;   
 L ：
 Lへ移動します。

ラベルLは2つの場所から到達できるため、gotoの制御フロー方程式は、before (2) = after (1)がbefore (3)と交差することを示しています。しかし、before (3) = before (2)であるため、before (2) = after (1)がbefore (2)と交差します。これはbefore (2)の2つの固定点、{i}と空集合を持ちます。しかし、データフロー方程式の単調形式により、確実に割り当てられた変数に関する可能な限り最大の情報を提供する唯一の最大固定点（最大サイズの固定点）が存在することが示されます。このような最大（または最大）固定点は標準的な手法で計算できます。データフロー解析を参照してください。

追加の問題は、制御フローのジャンプによって特定の制御フローが実行不可能になる可能性があることです。たとえば、次のコード フラグメントでは、変数i は使用される前に確実に割り当てられます。 

 整数i ; 
 j < 0の場合、戻り値を返します。そうでない場合はi = jです。        
 印刷( i );

ifのデータフロー方程式は、after (2) = after( return ) が after( i = j ) と交差することを示しています。これを正しく動作させるために、すべての制御フロージャンプに対してafter ( e ) = vars ( e ) と定義します。これは、 false ( true ) = vars ( e )という方程式が妥当であるのと同じ意味で、空虚に妥当です。なぜなら、制御フロージャンプの直後に制御が別のポイントに到達することは不可能だからです。

参考文献

  1. ^ J. Gosling、B. Joy、G. Steele、G. Bracha. 「Java言語仕様、第3版」、第16章（527～552ページ） 。 2008年12月2日閲覧。
  2. ^ 「標準ECMA-334、C#言語仕様」ECMA International . セクション12.3（122～133ページ） . 2008年12月2日閲覧。
  3. ^ スターク、ロバート F.; E.ボーガー;ヨアヒム・シュミット (2001)。Java と Java 仮想マシン: 定義、検証、検証。米国ニュージャージー州セコーカス: Springer-Verlag New York, Inc.、セクション 8.3。ISBN 3-540-42088-6。
  4. ^ ab Fruja, Nicu G. (2004年10月). 「C#における明確な代入分析の正確性」. Journal of Object Technology . 3 (9): 29– 52. CiteSeerX 10.1.1.165.6696 . doi :10.5381/jot.2004.3.9.a2 . 2008年12月2日閲覧。我々は正しさ以上のことを証明しています。分析の解が完全な解である（安全な近似値であるだけでなく）ことを示しています。 
  5. ^ 「Cyclone: Definite Assignment」. Cyclone ユーザーズマニュアル. 2008年12月16日閲覧。
  6. ^ 「標準ECMA-335、共通言語基盤（CLI）」ECMA International . セクション1.8.1.1（パートIII、19ページ） . 2008年12月2日閲覧。