Comments
Description
Transcript
C 言語のための現実的なポインタ解析
C 言語のための現実的なポインタ解析∗ 関口 龍郎 [email protected] 東京大学 1 はじめに ムは実行時に危険な振舞を行う可能性のあるコードを発 見するとプログラマに対して警告を発する。例えば配列 C 言語 [13] は 1973 年にオペレーティングシステムを のサイズよりも配列の添字が大きくなる可能性を発見 記述するために開発されたプログラミング言語である すれば、配列の不正仕様の可能性をプログラマに通知す が、その実用上の重要性は現在になってもいささかも衰 る。もちろん正確な添字は解析時には分からない場合が えていない。 C 言語の欠点を克服したと称するたくさ んの言語が開発されたが未だに様々な分野において C 言語と、その拡張である C++ 言語によってアプリケー あるので整数区間を利用して値が実行時に取りうるすべ ての可能性を表現している。解析には一種の整数制約系 の単純化アルゴリズムを用いている。 ションが記述されている。 Wagner のシステム [23] は Larochell のものと似てい C 言語には、宣言された変数の型を偽ることができ るが semantic comment なしに C 言語のソースコード る、変数の別名 (エイリアス) を簡単に作れる、言語仕 を直接解析可能である。 Wagner はそのツールを Send様を逸脱するプログラムを簡単に記述できる等の特徴が mail に適用し、未報告のバグをいくつか発見すること あり、システム記述の際に生じる多様な要求に柔軟に応 に成功した。 Wagner のシステムも整数区間表現によ えることができる。しかし、これらの特徴は同時に最適 化、デバグ、検証の障害となっている。そのため近年 C 言語を対象とした大域的なプログラム解析によって最適 化、デバグ、検証の効果を高めるツールが登場し始めて いる。 る値の抽象化を行い、解析手法も一種の整数制約系の単 純化アルゴリズムに基づいている。 Necula は全く別のアプローチを取っている。 Necula のシステム [15] は C 言語のサブセットを対象とした独 Larochell のシステム [14] は LCLint[10] の拡張であ 自の型概念に基づいた解析をし、ソースコード上で危 る。このシステムは C 言語のプログラムに semantic 険な操作を行う可能性のある部分を特定する。しかし comment を付与したものを入力として受け取り、プ Larochell や Wagner のシステムとは異なりプログラマ ログラマの意図の整合性を検証する。 Semantic com- に対して警告を出すのではなく、危険な操作を行う可 ment とは変数や値の使い方に関するプログラマの意 能性のある部分にシステムが実行時チェックのコードを 図を表現したものである。例えば nonnull という se- 自動的に挿入する。したがって悪意を持つ攻撃者がソフ mantic comment が付加された変数は実行中に決して トウェアの欠陥を攻撃しようとしても挿入された実行時 NULL にならないことを指示している。またこのシステ チェックコードによってそれは防がれることになる。も ∗ この研究は科学技術振興機構戦略的創造研究推進事業個人型研究 (さきがけタイプ) の研究助成を受けて実施された。 ちろん静的な解析はプログラムの実行時の振舞を完全に 知ることはできないので、実際には安全である部分に実 行時チェックコードが挿入される場合があり得る。その はとりわけ重要である。しかし C 言語の semantics に 時は本来であれば不必要な実行時オーバヘッドが生じる は以下に挙げられている曖昧性がある。 ことになる。 本研究の目的はこのような最適化1 、デバグ、検証の Unspecified behavior 意味は確定しているが、コン パイラの特定の実装によって定義される。 ためのツールに直接適用可能なポインタ解析のアルゴリ ズムを構築し、その実装を提供することにある。我々の Undefined behavior いわゆるエラー状態を想定し ポインタ解析は特にメモリに関する詳細な情報を表現 た動作である。この動作を実行後にあらゆる予測 することができる。我々の開発している実装は現在の標 不能な事態を引き起こして良い。特定のコンパイ 準的な計算機において現実的なサイズ (数万行∼十数万 ラの出力したコードがどのような結果を引き起こ 行) の C 言語のアプリケーションを現実的な時間 (数秒 したとしてもそのコンパイラは仕様に適合してい ∼数十分) で解析することを目標にしている。 る。 ポインタ解析 [1] とは変数 (特にポインタ値を保持す る変数) の指す対象を求める静的解析である。ポインタ 解析は一般に決定不能 [18] であり、常に正確な結果を 得るアルゴリズムは存在しない。そのため精度の考え 方が必要である。精度は一般に計算量とのトレードオフ がある。精度の良いアルゴリズムでは数万行程度の現実 的なアプリケーションの解析を、通常の計算機 (数 GB のメモリを持つ) と現実的な時間 (数分∼ 24 時間) では 解き終らない場合があり [11]、計算量に対する要求はシ ビアである。そのため解析の精度を向上させた時に増 加する計算量が、精度の向上に見合うかどうかの議論 コンパイラの特定の実装によって確定する意味がある ためにソースコードだけからではプログラムの意味を決 定できない [16]。プログラムの意味が分からなければ適 用できる解析手法が制限されてしまう [26]。我々は un- specified behavior の意味をできるだけ標準的なコンパ イラにおける定義と等しくなるように設定したが、実際 のコンパイラにおいて我々とは異なる意味を定義してい る場合は残念ながら我々の解析結果が正しいとは言えな い。 我々の解析ではプログラムのある演算が undefined behavior を起こす可能性があるかどうか判断するが、 [11, 19] も良く行われている。暗黙に利用される場合も undefined behavior を起こした後の状態は考慮しな 含めてポインタが極めて多用される C 言語のプログラ ムではポインタ解析が静的解析の精度を高めるために重 要である。 本論文では C 言語の仕様書として [12] を採用してい る。 い。言い替えると我々はプログラムの実行について以下 の 3 通りのみ考慮する。それは undefined behavior を 起こして停止する場合、正常に実行を続ける場合、正常 に停止した場合の 3 通りである。 2.1 2 C 言語の実行モデル メモリのモデル C 言語の通常の実行環境は 32 ビットまたは 64 ビッ この解析は C 言語のプログラムを対象としている。 トの整数によってメモリの場所を指し示す方式を採用 解析の正しさを考えるためにはプログラムの実行の意味 しているが、本論文では互いに disjoint な連続領域の を定義しなければならない。特に本論文の解析アルゴリ 集合としてメモリを定義する。一つの領域は整数によっ ズムは抽象解釈に基づいているため semantics の定義 て場所を指定する通常のメモリと同様である。メモリ 1 ここでは列挙しないが大域的解析を利用した最適化手法は多数存 在している。 の場所 (アドレス) は領域を指し示す識別子 (r, q, ...) と 整数で表されるオフセットの組 (hr, 10i, hq, 30i, ...) に i, j ∈ Int i +ii j = i + j r, q ∈ Rsym hr, ii +pi j = hr, i + ji v ::= i | hr, ii ∈ Value hr, ii +pi hq, ji = hr, i + ji R ∈ Region = Int → Value i −ii j = i − j M ∈ Rsym → Region hr, ii −pi j = hr, i − ji hr, ii −pp hr, ji = i − j 図 1: Dynamic semantic objects. char *p = char *q = p - q; // p > q; // malloc (12); malloc (8); subtraction of two pointers comparision of two pointers 図 3: 値同士の加減算の定義 おり、同じ配列オブジェクトに属するポインタ同士のみ 比較、減算の意味が定義されている。したがって同じ領 域内を指すポインタ同士の比較であっても undefined 図 2: 領域間の演算の例 である場合がある。 C 言語の仕様上では undefined behavior であっても よって表現される。メモリとは領域識別子から領域への プログラマの間の暗黙の共通理解として想定されている 部分関数であり、領域は整数から値への部分関数であ 仕様があるのではないか、という議論もあり得る。実際 る。プログラムの実行時に領域に割り当てられる物理ア に我々が設計した実行モデルでは仕様上 undefined と ドレスはプログラムローダや malloc の特定の実装に なっている演算でも多くのプログラマが利用しており、 よって決定されることになるため、静的解析ではこれら かつ無害と考えられるものには意味を定義している。し の値を仮定することはできない。 たがって我々の解析ではすべての undefined behavior このようなモデル化には違和感を感じるかもしれな い。なぜなら C 言語では図 2に示すように複数の領域 に関わる演算を非常に簡単に記述できるからである。図 中変数 p と q には malloc 別の呼び出しによって確保さ れた領域のアドレスが割り当てられている。当然ながら 変数 p と q は別々の領域を指したポインタである。ほ を検出する訳ではない。しかし有効な意味を見出せない undefined behavior はそのままであり、ここで挙げた 複数の領域間のポインタの演算も undefined としてい る。 2.2 値のモデルと演算 とんどのコンパイラにおいてこれらの演算の結果は物理 C 言語ではポインタの値を整数型の変数に保持するこ アドレス同士の減算、比較にそれぞれコンパイルされ、 とができる。この整数変数の値を元のポインタ型の値に プログラマの意図通りに実行される。 キャストした場合にそのポインタ型の値は有効である。 しかし仕様ではあくまでも異なる領域に属するポイン このような事態を表現するためには値のドメインは整数 タの減算、比較は undefined である。仕様に忠実に解 とポインタの両方を含んでいなければならない。実行モ 釈すれば図 2のコードは合法ではない。したがって断片 デルを定義するのに使われるドメインを図 1に示す。 化された領域の集合としてメモリを定義するのは仕様と 我々は仕様と矛盾のないように C 言語の演算子の意 良く適合している。仕様では更に厳しい定義がなされて 味を定義した。いくつかの定義を図 3に示す。ただし本 論文ではオーバフロー、アンダフロー等の例外的な状況 は無視して考えることにする2 。図中で +ii は整数型の n, m ∈ Int 変数同士の加算を意味する。 +pi はポインタ型の変数 l, u ∈ Int ∪ {−∞, ∞} と整数型の変数の加算を意味する。同様に −ii は整数型 I, J ::= [l, u] | n[l, u] + m ∈ AInt の変数同士の減算、 −pi はポインタ型の変数と整数型 R, Q ⊆ Rsym の変数の減算、 −pp はポインタ型の変数同士の減算を hR, Ii ∈ AVal = P(Rsym) × AInt 意味する。 C 言語ではポインタ型の変数同士の加算は 型エラーであるため +pp のような演算は存在しない。 R : ARegion = AInt → AVal 以上の定義は C 言語のすべての演算子に対して定義さ M : Rsym → ARegion れているが、本論文では省略する。 多くの定義は自然なものであるが、ポインタ値同士 図 4: Static semantic objects. の加算の定義がやや人工的かもしれない。図 3の定義で はポインタ値 hr, ii と整数変数が保持するポインタ値 hq, ji の加算の結果を hr, i + ji としているが、この グラムの実行が終了するように抽象的な値のドメイン を lattice とし、抽象的な演算子はその lattice の上 結果には領域 q のアドレスが反映されていない。整数 の monotonic な関数として定義しなければならない。 に変換されたポインタを整数として利用する場合の動作 抽象的な値とは例えば整数の場合では符号 (正、零、 は unspecified behavior であり、この演算の動作は特 負)、偶奇性 (偶数、奇数) などである。抽象的な演算と 定の実装によって定義される。領域 q の物理アドレス は例えば、正 × 正 = 正、偶数 + 偶数 = 偶数などの演 をソースコードだけから決定できないため図 3の定義は 多くのコンパイラで定義されている意味とは異なってい る。この問題は抽象演算子の定義によって解決される。 3 C 言語の抽象解釈 算である。抽象的な演算の結果は必ず具体的な演算の結 果を含んでいなければならない。 C 言語の抽象解釈では値、演算子に加えてメモリも抽 象化しなければならない。抽象演算子は抽象値と抽象メ モリの組同士の書き換え規則として定式化される。 抽象解釈 [4] は古典的な静的解析の手法であり、プロ グラミング言語の semantics からシステマティックに 解析アルゴリズムを得られることに特徴がある。特定の 高級な型システムや言語機構に依存していないため C 言語のような型システムが信頼できない言語にも適用す 3.1 値の抽象ドメイン 我々は整数を表現するのに区間 (とその倍数) という 抽象領域を用いる。区間とは上限と下限によって定義さ れる整数の集合である。 ることができる。 抽象解釈ではプログラミング言語の semantics から [l, u] = {x | l ≤ x ≤ u} 抽象的な semantics を半自動的に作成する。値や演算 子などに対応する抽象的な値、抽象的な演算子を定義 n[l, u] + m = {nx + m | l ≤ x ≤ u} し、その抽象的な semantics の上でプログラムを仮想 ただし l, u はそれぞれ −∞, ∞ であってもよい。また倍 実行し、解析を行う。一般にプログラムの実行は停止し 数の n は正の整数である。特に [−∞, ∞] は整数全体の ないことがあるが、抽象的な semantics では必ずプロ 集合 Z と等しい。区間の間の順序関係を集合の包含関 2 実装された解析器では例外的な状況も考慮されている。 係と定義すると、このドメインは空集合 ∅ を最小元、Z を最大元とする lattice となる。このドメインを抽象的 結果の精度が極めて悪くなるが、これはやむを得ないこ な整数のドメイン AInt と呼ぶ。 とである。 抽象整数の演算の例は次のようになる。 3.2 [a, b] +ii [c, d] = [a + c, b + d] メモリの抽象ドメイン 抽象的なメモリは抽象的な領域の有限集合である。抽 n[a, b] +ii m[c, d] = g[(na + mc)/g, (nb + md)/g] 象領域は抽象整数から抽象値への関数と定義する。多く ただし g = gcd(n, m) である。一般の演算については どの関数によって動的に確保される領域に対してはサイ 省略するが、抽象解釈の正しさを言うためには抽象的な ズが静的には分からない場合がある。このような領域を 演算は必ず具体的な演算の結果を含んでいなければなら 安全に近似するために領域のインデックスとして無限集 ない。ある演算子 ⊕ に対し抽象的な値 A, B の結果が 合を許している。 A ⊕ B = C となるならば C は必ず C ⊇ {a ⊕ b|a ∈ A, b ∈ B} でなければならない。抽象的な値の演算はす べてこの規則を満たすように定義されている。 C 言語では整数型の変数にポインタ値を保持すること ができるため、変数が持つ値の抽象ドメインは整数とポ インタのドメインを融合したものとなる。一つの変数は の場合、領域のインデックスは整数であるが malloc な {4[0, ∞] 7→ 0} 例えばこの抽象領域は任意の大きさの領域の可能性があ り、すべての要素が 0 である。抽象領域のインデックス の定義の仕方には任意性があり、細かく区別した方がよ り詳細な情報が得られる。 複数の領域に属するポインタを指すことができるため抽 象的なポインタは複数の領域に関する情報を持たなけれ R1 = {0 7→ 255, 4 7→ 0, 4[2, ∞] 7→ 0} ばならない。そのため抽象的な値は領域の有限集合 R R2 = {8[0, ∞] 7→ 0, 8[0, ∞] + 4 7→ 0} と抽象整数 I の組 hR, Ii で表現する。ポインタではな い純粋な整数は R が空集合である抽象値として表現す 例えばこの 2 つの領域は等価であるが、どちらが適切で る。 あるかどうかは領域の使われ方に依存している。前者は 第 2.2 節で、ポインタと、整数変数に保持しているポ 最初の 2 ワードにヘッダ情報を持ち、残りが配列である インタを加算する時に問題があった。整数として利用さ ような領域、後者は 2 ワードの要素を持つ構造体の配列 れたポインタの仕様は unspecified behavior であり、 を表すのに適している。ただしこの表現では 1 ワードが 4 バイトで表されていると仮定しており、そのためアド タのアドレスとして解釈されているが、ポインタのアド レスが 4 または 8 の倍数となっている。我々の解析器 特定の実装によって決定される。多くの実装ではポイン レスは実装依存であり、ほとんどの場合プログラムロー は領域の型情報を利用して抽象領域のインデックスを作 ド時に決定され、静的には分からない。しかし抽象演算 成する。以上をまとめると図 4のようになる。 の結果は必ず具体的な値を含んでいなければならない。 抽象領域を融合する操作が必要になる場合がある。 これらの要求を満たすために抽象的なポインタ値の加 我々は多段的な構造を扱う方法として Das のアルゴリ 算を以下のように定義する。ここで抽象的なポインタを ズム [7] を採用しているが、このアルゴリズムではメモ h{r}, Ii、整数変数が保持しているポインタの抽象値を リに複数の異なったポインタが書き込まれた場合に、そ れらのポインタの指す領域を融合しなければならない。 h{q}, Ji とおく。 領域の融合とは対象となる複数の領域を同一視すること h{r}, Ii +pi h{q}, Ji = h{r}, [−∞, ∞]i である。言い替えると、融合される領域の少なくとも一 はせず、関数呼び出しは単純に引数と返り値の代入文の Var ::= x | y | z | ... Insn ::= x := v | x := y | x := y +ii z | x := y +pi z | x := y −ii z | x := y −pi z | x := y −pp z 列へと変換される。別の関数内で同じ名前の変数を使用 していた場合には干渉が起こらない新しい名前の変数に 置き換えられる。関数内部では flow sensitive な解析 を行っている。同じ名前の変数に複数回代入を行ってい た場合はデータフローが干渉しないように変数を置き換 | x := ∗y え、同じ変数への代入は一つしかない形式へと変換して | ∗x := y いる3 。この変換には SSA 変換 [5] を用いている。 E : Var → AVal プログラムが関数ポインタを使用している場合には コールグラフを決定するのが難しい。この問題について 図 5: Machine instructions. は本論文では扱わない。 3.4 つの領域で区別されないインデックス、値は融合後の領 解析アルゴリズム 域でも区別されないようにしなければならない。例えば 我々の解析はプログラムを抽象的な演算子による命 領域 R1 では最初の 2 ワードは区別されているが領域 令列と解釈し、その命令列を抽象的な値とメモリ、環境 R2 では区別されていない。領域 R2 では 2 ワード単位 を使って仮想実行することによって行う。抽象的な演算 で区別されているが領域 R1 では区別されていない。し は、抽象的なメモリと環境の組の上の単調増加な関数と たがって R1 と R2 を融合した領域は例えば次のように なるように意味を定義する。ただし抽象的なメモリ M と環境 E の組の上順序は次のように定義する。 M, E v なる。 M0 , E 0 であるとは: {4[0, ∞] 7→ 255[0, 1]} Das のアルゴリズムについては第 5.5節で簡単に触れて いる。 3.3 命令コード 1. Dom(M) = Dom(M0 ), Dom(E) = Dom(E 0 ). 2. ∀r ∈ Dom(M).M(r) v M0 (r). 3. ∀x ∈ Dom(E).E(x) v E 0 (x). C 言語の式、文の意味は非常に複雑であるため一度等 を満たすことである。ただし抽象領域間の順序は次のよ 価な意味を持つ単純な命令列へと変換し解析を行って うに定義される。 R v R0 であるとは Dom(R) = いる。複雑な式は分解され、元の式の意味は一種の三 Dom(R0 ) かつ ∀i ∈ Dom(R).R(i) v R0 (i) となるこ 組コードによって表現される。 L-value を含む式は l- とである。また抽象値同士の順序は次のように定義され value を使わない等価な命令列へと変換される。我々の る。 hR, Ii v hR0 , I 0 i とは R ⊆ R0 かつ I ⊆ I 0 となる 使用している命令の一部を図 5に示す。命令には定数の ことである。 代入、変数の代入がある。 2 項演算子は必ず変数同士の 加算は引数に対して元々単調増加な演算子であるため 演算として表される。メモリを読む命令と (x := ∗y) と 問題ないが、減算は二番目の引数に対して単調増加な演 書き込む命令 (∗x := y) が用意されている。 算ではない。このため減算を行う時には以前の値と新し 我々の解析アルゴリズムは context insensitive であ るため関数全体を transfer function [24] で表すこと 3 厳密に言えば φ 関数は代入文の列へと変換されるため最終的には 同じ名前の変数に対する代入が複数存在することもある。 い値の upper bound によって変数の値を置き換える。 ある変数の値が無限列を作るのは値の依存関係に循環が 具体的には x := y −ii z という命令はメモリと環境を次 あった場合である。循環を構成する変数の数の回数だけ のように書き換える。 プログラムを仮想実行するとその変数の値は必ず増加 M, {x 7→ v} ∪ E −→ M, {x 7→ v t (E(y) −ii E(z))} ∪ E (または減少) する。値を持つ部分は環境と抽象メモリ の両者にある。したがって環境が持つ変数の個数と抽象 ただし x 6= y, z の場合である。他の演算子の意味につ メモリに含まれる領域のインデックスの数を加えた回数 いては省略する。 だけ仮想実行すればどんな循環があっても必ず一回実行 抽象的なメモリと環境の初期値はソースコードの情報 される。したがって一定回数としてこの値を選べば、ど を利用して設定される。大域変数に対して初期値が定義 んな循環があっても 4 の段階で必ず循環を構成する変数 されていれば、そのメモリ領域は指定されている初期値 のオフセット部に ∞(または −∞) が導入される。 がそのまま設定される。初期値のない領域や実行時に確 保される領域は 0 が設定される。変数の値の場合も同様 4 実験結果 であり、初期値が指定されていればその値が設定され、 指定されていない場合には 0 が設定される。 演算子は単調増加となるよう定義されているが、値の ドメインが無限の長さの上昇列を持っているため収束し ない可能性がある。抽象値は領域シンボルの集合とオフ セットの組 hR, Ii として表される。一つのプログラム ポインタ解析の精度を測るには主に以下の 2 種類の方 法が知られている。 • points-to set の大きさを測る。 points-to set とは 一つのポインタが指す可能性のあるメモリ領域の 個数であり、少ない程精度が良い。 に対して定義される領域シンボルの数は有限個であるた め R に関する無限の長さの上昇列は存在しないが、オ フセット部 I に関して無限の長さの上昇列を作る可能 性がある。例えば命令列が以下のような命令を含んでい る時に無限の長さの上昇列ができる。 x :=1 y :=y +ii x このような場合であっても解析が必ず終了するように アルゴリズムは以下のようになっている。 1. 一定回数仮想実行する。 • ポインタ解析の結果を実際の最適化に適用し、性 能の向上を調べる。 ここでは後者を採用した。 我々は本論文で述べたポインタ解析を Fail-Safe C [17] に適用し、動的なチェックの除去を行った。 FailSafe C は ANSI C 言語コンパイラの一つの実装であ り、メモリに関して undefined behavior を引き起こさ ないように動的なチェックが挿入された実行コードを出 力する。ここでは詳しくは述べないが Fail-Safe C では ポインタの演算に対して以下の 5 種類の動的なチェック が行われる。 2. すべての変数の値を保存する。 • キャストフラグのチェック 3. 一定回数仮想実行する。 4. 変数の値を保存した値と比較して、増加 (減少) し ていたら上限 (下限) を ∞(−∞) に置き換える。 5. 収束するまで仮想実行する。 • ヌルチェック • 型チェック • アラインメントチェック 181.mcf 256.bzip2 ノード数 SPARC IA32 5618 13278 19.5sec 39.5sec 9.35sec 19.5sec 表 1: 解析時間とノード数 チェック数 除去数 割合 705 83 83 622 329 23 23 411 47% 28% 28% 66% 181.mcf この中でポインタ解析を利用した最適化によって除去 null check type check alignment check boundary check の対象となるのが後 4 者である。 Fail-Safe C のコン 256.bzip2 パイラは Objective CAML によって記述されており null check type check alignment check 1352 764 764 816 443 443 60% 58% 58% boundary check 588 142 24% • 境界チェック 約 26000 行である。このうちポインタ解析の部分は約 2000 行である。解析の対象としては SPECCPU 2000 から 181.mcf (約 2000 行) と 256.bzip2 (約 5000 行) を用いた。実行環境としては Sun ワークステーション (UltraSPARC II 400MHz) と PC (Pentium III Xeon 700MHz) で行った。 4.1 表 2: 動的なチェックの除去数 解析時間 表 1に解析にかかった時間とノード数の関係を示す。 ノード数とは環境に含まれる変数の数である。我々は プログラムを三つ組コードに変換するためプログラム 中に含まれる変数よりも変換後の命令列に含まれる変 数の数が多くなる。この表を見るとノード数に対して SPARC superlinear な関係にある。 Wilson のアルゴリズムで は約 4700 行のプログラムの解析に 15.5 秒かかってお 181.mcf 256.bzip2 り、我々のアルゴリズムと同水準である。 IA32 181.mcf 256.bzip2 4.2 orig opt improvement 5.19sec 87.1sec 4.52sec 66.1sec 13% 24% 2.66sec 41.5sec 2.06sec 26.6sec 23% 36% 動的なチェックの除去 次に動的なチェックをポインタ解析によって除去した 個数を表 2に示す。この表によるとベンチマークによっ て除去されるの数にばらつきが見られるが、およそ 2 割 ∼ 7 割のチェックを除去できていることが分かる。 表 3: 最適化の実行時間への効果 4.3 実行時間への効果 最後に最適化による実行時間への効果を表 3に示す。 この表によるとおよそ 1 割から 4 割の速度向上が得ら れたことが分かる。 5 関連研究 域に対して読み書きが行われた場合にその領域全体があ たかも一つの変数であるかのように扱われ、要素同士の 区別を行わない。これは配列の添字が一般に静的には分 からないため仕方がない面もあるが、要素を区別しない と解析の精度が非常に悪くなる [9]。 Wilson のアルゴリズム [24] では領域を location sets と呼ばれる概念を利用して分割している。 location sets この節ではポインタ解析の研究の中における本研究の とは我々の抽象領域でインデックスの区間の上限と下限 位置付けについて触れる。一つのポインタ解析は以下に をそれぞれ ∞ と −∞ に置き換えたものである。例え 示す様々な要素によって成り立っている。 ば次のような領域である。 • 解析アルゴリズム • 値の表現 {8[−∞, ∞] 7→ [0, 10], 8[−∞, ∞] + 4 7→ {r, q}} この領域はおそらく 8 バイトの構造体の配列であり、構 造体の最初の要素は整数であり、ここでは 0 から 10 の • flow sensitivity 間の整数が代入されている。構造体の二番目の要素はポ • context sensitivity インタを保持し、領域 r と領域 q を指すポインタが代入 されている。この例から分かるように location sets は • 構造の深さ 個々の要素についての本研究の位置付けを以下に述べ る。 構造体の配列を表現するのに適している。 我々の抽象領域の概念は Wilson の location sets を 拡張したものになっている。我々の方式では Wilson の 方式と比べてオフセットの区間についてより詳細な情報 5.1 解析アルゴリズムについて が得られる。特に boundary checking の除去などの最 適化を Wilson のアルゴリズムの解析結果から行うのは ほとんどのポインタ解析のアルゴリズムは、必ずし も明示されていないが抽象解釈に基づいている (ただし 整数制約系を併用するものもある)。抽象解釈を使わず にポインタ解析を行うアルゴリズムは我々の知る限り right-regular equivalence relation を使うもの [8] のみ である。この手法はメモリのモデルを必要としないとい う特徴がある。ただし C 言語のようにある値を本来と は別の型としてアクセスできる機能をうまく表現できな いため、我々は採用しなかった。我々のポインタ解析の アルゴリズムは抽象解釈に基づいている。 5.2 値の表現 難しいと考えられる。 Yong のポインタ解析 [26] では 2 つの異なる構造体の 先頭の要素列が同じ型を持つ時に対応する要素同士は区 別される。型が変わる要素については混合される可能性 があると見なされる。これは C 言語の仕様に忠実であ る。仕様では異なる構造体の先頭の要素列が同じ型であ ればそれらの対応する要素は同じオフセットに置くよう に定めている。我々のアルゴリズムで使われているメモ リブロックの表現法でも先頭の共通の要素列はそれぞれ 区別される。 Yong の論文中では配列をどうやって表す のか記述されていない。 整数の制約の集合によってポインタ演算を表すシステ ほとんどのポインタ解析では領域を 1 点に潰してい ム [25] では我々の表現法よりも詳細な結果が得られる る。つまり配列や構造体のような複数の要素を持てる領 ことがある。しかし [25] で使われている制約解消のア ルゴリズムである Fourier-Motzkin elimination [6] は 変数の数に対して指数時間を要するアルゴリズムであ る。 5.3 int int int a = a = **a; *b, *d; c, e; &b; b = &c; &d; d = &e; Flow sensitivity Flow sensitive な解析には変数のみを flow sensitive にするものとメモリも含めて flow sensitive にするもの がある。後者の場合、 control flow graph のノードの 数だけメモリ全体の表現が必要になる (ノード間でのメ モリ表現の差分だけを保存する sparse representation と呼ばれるテクニックはある)。本研究では前者の flow sensitivity を採用している。また if 文の条件部が整 図 6: 多段的な構造を作るプログラム 1c b ³³ ³ 1 a³ PP q dP qe P 図 7: Andersen のアルゴリズムによる解析結果 数定数との比較を行っている場合、条件分岐の後の基本 ブロックではその情報を利用して解析の精度を高めてい る。しかしこれは良く知られたテクニック [2] であり、 詳細については本論文では省略する。 5.4 Context sensitivity る。一方 Steensgaard のアルゴリズム [22] は疑似線形 時間 O(nα(n)) の計算量であるが、多段的な構造の情報 を融合させる。例えば図 6のようなプログラムに対して 両アルゴリズムはそれぞれ図 7と図 8に示した結果を出 力する。図から明らかなように Andersen のアルゴリズ 本研究のアルゴリズムは context insensitive であ ムでは b と d の指す対象は区別されているが、 Steens- り、いわゆる 0CFA である。プログラムが generic な gaard のアルゴリズムでは変数 b が変数 e のアドレス 配列読み / 書き関数やユーザ定義のメモリ確保関数など を指す可能性があると解釈されている。 の多相的な関数を含んでいた場合に context insensitive な解析では精度が低下することになる。 Context sensi- ポインタによってメモリ上に作られるデータ構造の扱 い方は精度と計算量に大きな影響がある。ポインタに tivity が解析の精度に与える影響を調べた研究 [11, 19] よってメモリ上に作られるデータ構造を計算量を押えな によると context sensitivity は解析の精度にほとんど がらできるだけ詳しく表現する手法には k-limiting な 影響ないというものであった。これは C 言語のプログ どの様々なテクニック [3, 20, 21] があるが Das のアル ラムでは ML で良く使われる多相関数のようにポイン ゴリズム [7] は計算時間が Steensgaard のアルゴリズム タを利用する関数がほとんどないということを示唆して とほとんど変わらず、精度は Andersen のアルゴリズム いる。 とほとんど同じものである。本研究でも Das のアルゴ 5.5 構造の深さ リズムを採用している。 ポインタが指す先がまたポインタであることもあり得 る。このような多段的な構造を扱うやり方は精度と計算 量に大きな影響を持っている。 Andersen のアルゴリズ a - {b,d} - {c,e} ム [1] は多段的な構造をできるだけ保存する解析である が、ノード数を n として O(n3 ) の計算量を必要とす 図 8: Steensgaard のアルゴリズムによる解析結果 6 おわりに この論文の目的は数万行から十数万行の現実的な C 言語のアプリケーションに適用することを目指したポイ ンタ解析のアルゴリズムを記述することにある。本論文 Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 238–252, 1977. で記述したアルゴリズムは実際に SPECCPU 2000 ベ ンチマークに適用し、アルゴリズムの計算量は充分ス ケールしそうな感触が得られた。本アルゴリズムのメモ リ領域の抽象化方式は知られている多項式時間アルゴ リズムの中で最も精度が良いものである。本アルゴリズ ムの有効性を示すためにポインタ解析を利用した動的 チェックの除去アルゴリズムを Fail-Safe C コンパイラ に適用し 2 割∼ 7 割の動的チェックを除去し、実行時 間は 1 割∼ 4 割向上することが分かった。 今後は解析ツールを一般に公開するとともに他のポイ ンタ解析のアルゴリズムとの詳細な比較を行いたい。 参考文献 [1] Lars Ole Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, May 1994. [2] Rastislav Bodik, Rajiv Gupta, and Vivek Sarkar. ABCD: Eliminating Array Bounds Checks on Demand. In Proceedings of the SIGPLAN ’00 Conference on Program Language Design and Implementation, June 2000. [5] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Transactions on Programming Languages and Systems, 13(4):451–490, October 1991. [6] G. B. Dantzig and B. C. Eaves. Fourier-Motzkin Elimination and its Dual. Journal of Combinatorial Theory (A), 14:288–297, 1973. [7] Manuvir Das. Unification-Based Pointer Analysis with Directional Assignments. In Proceedings of the SIGPLAN ’00 Conference on Program Language Design and Implementation, June 2000. [8] Alain Deutsch. Semantic Models and Abstract Interpretation Techniques for Inductive Data Structures and Pointers. In Proceedings of ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation PEPM’95, pages 226–228, 1995. June. [3] David R. Chase, Mark Wegman, and F. Kenneth Zadeck. Analysis of Pointers and Structures. In [9] Amer Diwan, Kathryn S. McKinley, and J. Elliot B. Moss. Type-Based Alias Analysis. In Proceedings of the ACM SIGPLAN’98 Confer- Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Im- ence on Programming Language Design and Implementation, June 1998. plementation, June 1990. [10] David Evans. [4] Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Static Detection of Dynamic Memory Errors. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Lan- guage Design and Implementation, pages 44–53, 1996. [19] Erik Ruf. Context-Insensitive Alias Analysis Reconsidered. In Proceedings of the ACM SIGPLAN ’95 Conference on Programming Lan[11] Jeffrey S. Foster, Manuel Fähndrich, and guage Design and Implementation, pages 13–22, Alexander Aiken. Monomorphic versus PolyJune 1995. morphic Flow-insensitive Points-to Analysis for C. In Proceedings of the 7th International Static [20] Marc Shapiro and Susan Horwitz. Fast and Accurate Flow-Insensitive Points-to Analysis. Analysis Symposium, pages 175–198, 2000. In Conference Record of POPL’97: 24th ACM [12] INTERNATIONAL STANDARD Programming SIGPLAN-SIGACT Symposium on Principles Languages — C Second Edition, 1999. ISO/IEC of Programming Languages, pages 1–14, January 9899;1999. 1997. [13] B. W. Kerninghan and D. M. Rtchie. The C Programming Language. Prentice-Hall, 1978. [14] David Larochell and David Evans. Statically Detecting Likely Buffer Overflow Vulnerabilities. In 2001 USENIX Security Symposium, pages 177– 190, August 2001. [21] Marc Shapiro and Susan Horwitz. The Effects of the Precision of Pointer Analysis. In Proceedings of the 4th International Static Analysis Symposium, volume 1302 of Lecture Notes in Computer Science, pages 16–34, 1997. [22] Bjarne Steensgaard. Points-to Analysis in Almost Linear Time. In Conference Record [15] George C. Necula, Scott McPeak, and Westof POPL’96: 23nd ACM SIGPLAN-SIGACT ley Weimer. CCured: Type-Safe Retrofitting Symposium on Principles of Programming Lanof Legacy Code. In Proceedings of the ACM guages, 1996. SIGPLAN’96 Conference on Programming Lan[23] David Wagner, Jeffrey S. Foster, Eric A. Brewer, guage Design and Implementation, 2002. and Alexander Aiken. A First Step Towards Au[16] Michael Norrish. Formalising C in HOL. PhD tomated Detection of Buffer Overrun Vulnerabilthesis, University of Cambridge, 1998. ities. In Network and Distributed Systems Security Symposium NDSS, February 2000. [17] Yutaka Oiwa, Tatsurou Sekiguchi, Eijiro Sumii, and Akinori Yonezawa. Fail-Safe ANSI-C Com- [24] Robert P. Wilson and Monica S. Lam. Efficient piler: An Approach to Making C Programs. In Context-Sensitive Pointer Analysis for C ProSoftware Security — Theories and Systems, volgrams. In Proceedings of the ACM SIGPLAN ume 2609 of Lecture Notes in Computer Science, ’95 Conference on Programming Language Depages 133–153. Springer-Verlag, 2003. sign and Implementation, June 1995. [18] G. Ramalingam. The Undecidability of Aliasing. [25] Hongwei Xi and Frank Pfenning. EliminatACM Transactions on Programming Languages ing Array Bound Checking through Dependent and Systems, 16(5):1467–1471, 1994. Types. In Proceedings of the ACM SIGPLAN’98 Conference on Programming Language Design and Implementation, June 1998. [26] Suan Hsi Yong, Susan Horwitz, and Thomas Reps. Pointer Analysis for Programs with Structures and Casting. In Proceedings of the ACM Conference on Programming Language Design and Implementation, 1999.