← ENSOFT の研究
2014年4月4日

効率的なパス依存解析のための
イベントフローグラフ

Ahmed Tamrawi

Suresh Kothari

Department of Electrical and Computer Engineering
Iowa State University, Ames, Iowa, 50011

概要— 効率的かつ正確なパス依存解析には、(a) 制御フローグラフ（CFG）における指数的に増加する数のパスを解析すること、(b) CFG におけるパスの実行可能性を検査すること、という課題がある。我々は、CFG のパスに同値関係を導入して同値類に分割することで、これらの課題に取り組む。そうすれば、CFG の個々のパスではなく、これらの同値類に対して解析を行えば十分である。この手法には二つの大きな利点がある。(a) CFG のパスの数は指数的に大きくなりうるが、解析すべき本質的な情報は少数の同値類で捉えられる。(b) パスの実行可能性の検査がより簡単になる。重要な課題は、CFG の各パスを調べることなく、CFG のパスの同値類をいかに効率よく計算するかである。本論文では、CFG の各パスを調べる必要なしに同値類を形成する線形時間のアルゴリズムを示す。このアルゴリズムの鍵は、CFG のコンパクトな派生物であるイベントフローグラフ（EFG）の構築である。EFG では、各パスが対応する CFG のパスの同値類を表す。EFG はイベントの集合に関して定義され、そのイベントは解析対象の性質によって定義される。したがって、同値類は元の CFG のすべてのイベントトレースを保存することが保証される。Linux カーネル（v3.12）の実証評価を示す。評価における EFG は、スピンの安全な同期の性質のイベントに関して定義される。評価結果は、EFG に基づく同値類が、対応する CFG のパスの数と比べてはるかに少ないことを示す。パスの数が多い CFG では、この削減は 99% 近くに達する。さらに、対照実験の結果は、EFG が人間にとって理解しやすく、対応する CFG と比べてコンパクトであることを示す。

目次

I. はじめに

正確なパス依存解析には、(a) 制御フローグラフ（CFG）の各パスに沿った実行の効果を単独で、すなわち異なるパスからの効果を併合せずに解析すること、(b) 実行不可能なパスに沿った効果を除外すること、が必要である。したがって、効率的かつ正確なパス依存解析に特有の課題は、(a) パスの数が CFG の入れ子でない分岐ノードの数とともに指数的に増大すること [1], [2]、(b) パスの実行可能性を検査するにはパスに沿った分岐条件の充足可能性を検査する必要があり、その過程でも指数的な計算が生じうること [3], [4], [5], [6], [7], [8]、である。

直観的には、効率的なパス依存解析に対する我々の新しい手法は、次のようにパスの同値類を考えることで機能する。二つのパスは、同じイベントトレースを持つとき同値とみなす。各イベントトレースは CFG パス上のイベントの系列であり、与えられたソフトウェアの性質がそのパスで成り立つかどうかを検査するのに十分な情報を表す。同値類のすべてのパスは同じイベントトレースを持つので、グループ/クラスごとに一つのパスだけを検査すれば十分である。理論上、CFG パスの数が指数的に増大しても同値類の数が小さいままであれば、指数的な計算の増大を回避できる可能性がある。各 CFG パスを明示的に調べずに各クラスのイベントトレースだけを計算するのは直観に反するように思えるかもしれないが、本論文では、各 CFG パスを調べることなくすべてのイベントトレースを計算し、それによって指数的な計算負荷を回避する革新的な線形時間アルゴリズムを示す。

我々はイベントフローグラフ（EFG）と呼ぶ CFG の派生物を定義し、EFG の各パスが CFG の同値なパスのグループ/クラスに対応するような、一対一かつ上への写像が存在することを証明する。EFG は CFG のイベントと関連する分岐ノードを保持し、すべてのイベントトレースを計算するための極小のグラフである。すなわち、EFG の各パスは一意のイベントトレースを生成する。EFG を計算する線形時間アルゴリズムを示す。EFG を導入するもう一つの利点は、パスの実行可能性の検査のための計算を最小化できることである。Linux カーネル（v3.12）の実証評価（第 V-C 節）では、同値類を形成するための関連する分岐ノードだけで、実行可能性の検査にも十分であることがわかった。

実際的なシナリオで EFG を用いる利点を評価するため、Linux カーネル（v3.12）の実証評価を行った。EFG は、スピンの安全な同期の性質の検証に関連するイベントに関して定義される。この性質は、すべての実行可能な実行パスにおいて、スピンオブジェクトのロックの後に同じオブジェクトのアンロックが続くことを要求する。結果は、CFG からその EFG へ移ると、パスの数と分岐ノードの数が劇的に削減されることを示す。対照実験の結果は、EFG が人間にとって理解しやすく、対応する CFG と比べてコンパクトであることを示し、それは手作業による検証時間と実行可能性の検査の労力の削減に表れている。対照実験の結果、新しいバグを報告し [9]、Linux コミュニティに受け入れられた。実証評価のすべての CFG と対応する EFG は [10] で入手できる。第 VI 節では、Linux カーネルを用いた例を示し、手続き内および手続き間のパス依存解析における EFG の使用を説明する。

II. 動機となる例

図 1 は、Linux カーネル（v3.12）の関数 hwrng_attr_current_store の CFG を示す。ノード ⊤ と ⊥ は、それぞれ CFG に追加された一意の入口ノードと出口ノードを表す。また、T と F は、それぞれ分岐ノードからの真の分岐と偽の分岐を表す。この例は、安全な同期の性質を検査するのに必要なイベントトレースに関するものである。この性質は、すべての実行可能な CFG パスにおいて、同期オブジェクトのロックの後に、ロックされた同じオブジェクトのアンロックが続かなければならないことを要求する。この例には、灰色で強調表示された二つのイベントノード mutex_lock_interruptible (&rng_mutex)（e1）と mutex_unlock (&rng_mutex)（e2）が含まれる。

hwrng_attr_current_store の制御フローグラフ。入口ノードと出口ノード、rng_mutex に対する mutex_lock_interruptible と mutex_unlock の灰色のイベントノード、分岐ノード c1 から c5 を持つ。
図 1. 関数 hwrng_attr_current_store の CFG

この CFG では、分岐ノード c2、c3、c4、c5 は無関係な分岐ノードとみなされる。分岐ノードから分岐するすべてのパスが同じイベントノードまたは終端ノードに至るとき、その分岐ノードは無関係である。分岐ノード c1 は関連する分岐ノードである。CFG の与えられたパス P について、P の実行トレースのうち関連する分岐ノードとイベントノードだけからなる部分トレースを、P のイベントトレースと呼ぶ。つまり、c1 の false の分岐から分岐するパスは、同じイベントトレース（⊤e1c1e2⊥）を持つ。同一のイベントトレースを持つパスは同値とみなされ、一つの同値類にまとめられる。c1 の true の分岐から分岐するパスのイベントトレースは ⊤e1c1⊥ であり、それだけで別の同値類をなす。

各同値類は、そのクラスのパスの一意のイベントトレースによって表される。これらの同値類を計算すれば、安全な同期の性質を検査するには、すべての同値類のイベントトレースだけを解析すれば十分である。例えば、図 1 の CFG からは、1) トレース ⊤e1c1e2⊥ と 2) トレース ⊤e1c1⊥ の二つのイベントトレースが得られる。CFG のすべてのパスを網羅するには、これら二つのトレースだけを解析すれば十分である。

重要な点をまとめる。

  1. 同じイベントトレースを持つすべての CFG パスは、一つの同値類にまとめられる。この例では、すべての CFG パスが二つの同値類にまとめられる。
  2. イベントトレースを解析することは、すべての CFG パスを解析することと等価である。
  3. 分岐ノードから分岐するすべてのパスが同じイベントノードまたは終端ノードに至るとき、その分岐ノードは無関係である（無関係な分岐ノードのより広い概念は後で定義する）。この例では、五つの分岐ノードのうち四つが無関係である。

III. イベントトレースによるパス依存解析

定義 1: プログラムの制御フローグラフ（CFG）を G = (V, E, ⊤, ⊥) と定義する。ここで G は、プログラムの文を表すノードの集合 V と、文の間の制御フローを表すエッジの集合 E を持つ有向グラフである。⊤ と ⊥ は、それぞれグラフの一意の入口ノードと出口ノードを表す。

A. 実行トレース

CFG の各ノードに一意の識別子をラベル付けした後、CFG パスの実行トレースを、そのパスに沿ったノードラベルの正規表現と定義する。図 1 で最初に示し、図 2(a) に描き直した CFG を用いて、この定義を説明する。強調表示されたノードはイベントノードである。コードの文は、x1 から x15 とラベル付けされたノードに置き換えられている。図 2(b) は CFG パスを示し、その実行トレースは ⊤x1x2e1c1x3x4c2c3c4x9c5x10x11x12x13e2x15⊥ である。図 2(c) はループを持つ CFG パスを示し、その実行トレースは ⊤x1x2e1c1x3x4(c2c3x6)+c2c3c4x7x8e2x15⊥ である。ここで (ni..nk)+ は、ノード ni から nk までの、1 回以上実行されるループを表す。

同じ CFG の三つの見方。ノード x1 から x15 を持つグラフ全体、非巡回の実行パス一つ、c2、c3、x6 を通るループを繰り返す実行パス一つ。
図 2. CFG における実行パス

B. イベントトレース

イベントトレースは、解析対象の性質に関連する関心のあるイベントの集合 ℰ に関して定義される。すべての定義を説明するにあたり、安全な同期の性質の検証を一貫した例として用いる。安全な同期の性質は、すべてのオブジェクト p について、すべての実行可能な実行パスにおいて、ロックのイベント e1(p) の後にアンロックのイベント e2(p) が続くことを要求する。したがって、オブジェクト p についてこの性質を検証するためのイベントの集合 ℰp は、p に対して定義されるロックとアンロックのイベント、およびロックされたオブジェクト p が別名を持つか、パラメータ、戻り値、グローバル変数として別の関数へエスケープするデータフローのイベントからなる。このようなデータフローのイベントは、テイント解析の手法 [11] を用いて決定できる。関心のあるイベントが決まれば、CFG を走査し、各同期オブジェクト（p）について、すべての実行パスでロックのイベント e1(p) の後に常にアンロックのイベント e2(p) が続くことを検査するパス依存の検証アルゴリズムを書ける。ロックのイベントの後にアンロックのイベントが続かない違反パスの場合には、パスの実行可能性の検査を行う必要がある。

定義 2: すべてのオブジェクト p について、すべての実行可能な実行パスでイベント e1(p) の後に別のイベント e2(p) が続かなければならないとき、性質 P は 2 イベント性質である。

イベントに基づく解析は、安全な同期やメモリリークのような 2 イベント性質としてモデル化できる性質の検証に用いられることに注意する。MITRE Corporation が挙げる多くの脆弱性 [12] は、イベントに基づく解析で対処できる。

定義 3: CFG のノードは、解析対象の性質に関連するイベントの集合（ℰ）のイベントに対応するとき、イベントノードである。

定義 4: 有向グラフ G におけるノード u の後続は suc(u) で表され、エッジ (u, v) が ∃ するようなノード v ≠ u の集合からなる。

定義 5: 有向グラフ G における部分グラフ S の後続は suc(S) で表され、u ∈ S について v = suc(u) となるようなノード v ∉ S の集合からなる。

定義 6: 分岐ノード c について、分岐エッジとは c から出ていくエッジである。

定義 7: 次の条件が満たされるとき、分岐ノード c は無関係な分岐ノードである。

  • c は非イベントノードである。
  • c と c のすべての分岐エッジを含む部分グラフ S が存在する。
  • S はイベントノードを持たない。
  • S は一意の後続を持つ。すなわち |suc(S)| = 1 である。

図 3 に、無関係な分岐ノード c の例を示す。

二つの出ていくエッジが、イベントノードを含まず単一の後続 w を持つ部分グラフ S の内側にとどまる分岐ノード c。
図 3. 無関係な分岐ノード c の例

定義 8: CFG のパスのイベントトレースとは、実行トレースの部分式のうち、関連する分岐ノード、イベントノード、⊤ ノードと ⊥ ノードだけからなるものである。

例えば、図 2(b, c) に描かれたパス P1 と P2 のイベントトレースは ⊤e1c1e2⊥ となる。

定義 9: ℰ に関する CFG G のイベントフローグラフ（EFG）GEFG とは、イベントノード、関連する分岐ノード、入口（⊤）ノードと出口（⊥）ノードからなる、G のノード誘導部分グラフである。

分岐ノードの関連性。 関連性の概念は、CFG パスの同値類に関して定義される。関連する分岐ノードと、残りの分岐ノードや非イベントノードとの間に相関がある可能性がある。その場合、パスの実行可能性の検査では、関連する分岐ノードと相関する他のノードを考慮する必要がある。Linux カーネルの実証評価（第 V-C 節）では、そのような相関は見つからなかった。したがって、同値類を形成するための関連する分岐ノードだけで、実行可能性の検査にも十分であった。

C. CFG パスの同値類

この節では、すべての CFG パスで性質 P を検証することが、すべてのイベントトレースについて P を検証することと等価であることを示す。まず、CFG パス上の同値関係を定義する。

定義 10: CFG G と、G のノードの部分集合であるイベント集合 ℰ が与えられたとき、G のパス上の関係 ℛℰ を次のように定義する。二つの CFG パスは、同じイベントトレースを持つとき、かつそのときに限り関係する。

ℛℰ は反射的、対称的、推移的であるので、同値関係であることに注意する。

定理 1:* CFG G、イベントの集合 ℰ、同値関係 ℛℰ が与えられたとき、ℛℰ の同値類と EFG GEFG のパスとの間には一対一かつ上への写像が存在し、各 EFG パスは一つの同値類に対応するイベントトレースを生成する。

* 定理と系の証明は付録 A にある。

定理 2: 2 イベント性質 P が与えられたとき、すべての CFG パスにおけるその検証はイベントトレースを用いて行える。

系 1: 2 イベント性質 P が与えられたとき、CFG G のすべてのパスにおけるその検証は、対応する EFG GEFG で行える。

証明は上の二つの定理から直ちに従う。

注意 1: CFG と集合 ℰ が与えられたとき、対応する EFG は一意である。EFG のノードはちょうどイベントノードと関連する分岐ノードなので、一意に定まるからである。EFG のエッジも CFG のエッジから誘導されるので、一意に定まる。

D. 最適なパス依存解析のための EFG

2 イベント性質が与えられたとき、そのパス依存解析は CFG の代わりに EFG を用いて次のように行える。

すべてのオブジェクト p について:

  1. p に対して定義されたイベント e1 と e2、および p のデータフローのイベントを含め、関心のあるすべてのイベント（すなわち集合 ℰp）を決定する。
  2. オブジェクト p がパラメータまたは戻り値として他の関数に渡される場合、そのような関数をすべて関連する関数とみなす。
  3. 関連する関数について、ℰp に関する EFG を構築する。
  4. CFG の代わりに EFG を用いてパス依存解析を行う。
  5. e1(p) の後に e2(p) が続かないパスがある場合、パスの実行可能性の検査が必要である。EFG を用いると、パスの実行可能性の検査は条件（関連する分岐ノード）の充足可能性を検査することで行われる。条件の間の相関は、[15] のように、定数伝播 [13] や大域値番号付け [14] によって計算できる。

EFG は手続き間のパス依存解析を行うのに使える。第 VI 節では、EFG を用いた手続き間の検証の事例研究を示す。まとめると、2 イベント性質 P とそれに関連するイベントの集合 ℰ が与えられたとき、EFG は、正確かつ効率的なパス依存解析のためにすべてのイベントトレースを生成する極小のグラフである。EFG を実際に役立てるため、次の節では与えられた CFG から EFG を構築する効率的なアルゴリズムを示す。

IV. CFG のイベントトレースの計算

この節では、まず与えられた CFG を T 既約グラフに圧縮するアルゴリズムを示す。この圧縮アルゴリズムは、後で EFG の計算に用いる。次に、有向グラフの強連結成分を計算する Tarjan のアルゴリズム [16] に基づいて、CFG パスの同値類を線形時間で効率よく計算するアルゴリズムを示す。

A. アルゴリズム I: T 既約グラフ

定義 11: 彩色有向グラフ（CDG）を G = (V, E, C, ⊤, ⊥) と定義する。ここで (V, E) は、ノードの集合 V とエッジの集合 E を持つ有限の有向グラフである。⊤ と ⊥ は、それぞれグラフの一意の入口ノードと出口ノードを表す。C ⊆ V は彩色ノードの集合である。

このアルゴリズムでは、イベントノードを彩色ノードとして扱うことで、CFG を CDG としてモデル化する。

T1: 分岐しない非彩色ノードの除去

G = (V, E, C, ⊤, ⊥) を CDG とし、n を単一の後続 m を持つ非彩色ノード（n ∉ C）とする。T1 変換は、ノード n を m に吸収させるものである。ノード n の先行ノードがノード m の先行ノードになるよう、誘導エッジが導入される（図 4(a)）。

T1 変換は、分岐ノードでもイベントノードでもないすべてのノードを CFG から除去する。これらのノードは、結果のイベントトレースに含まれないので解析に無関係であり、除去される。

T2: 自己ループエッジの除去

G = (V, E, C, ⊤, ⊥) を CDG とし、n を自己ループエッジ (n, n) を持つ非彩色ノード（n ∉ C）とする。T2 変換はそのエッジを除去する（図 4(b)）。

T2 変換の背後にある直観は次のとおりである。イベントノードを含まないループブロックでは、ループの実行は重要でない。したがって、T2 は自己ループエッジを除去する。

T3: 無関係な分岐ノードの除去

G = (V, E, C, ⊤, ⊥) を CDG とし、n を、二つ以上のエッジを持ち、そのすべてが n の同じ後続 m を指す非彩色ノード（n ∉ C）とする。このとき T3 変換は、ノード n を m に吸収させるものであり、ノード n の先行ノードはノード m の先行ノードになる（図 4(c)）。

T3 変換の背後にある直観は次のとおりである。分岐ノード n の分岐上に非彩色ノードしかなく、それらの分岐がすべて最終的にノード m で合流する場合を考える。それらの分岐上の非彩色ノードが T1 変換で除去されれば、すべての分岐はノード m を指す。この時点で n での分岐は無関係なので、分岐ノード n を除去できる。

アルゴリズム I の変換。T1 は分岐しない非彩色ノードを吸収し、T2 は非彩色ノードの自己ループを削除し、T3 はすべてのエッジが同じ後続に至る非彩色の分岐ノードを吸収する。
図 4. アルゴリズム I の変換: (a)T1、(b)T2、(c)T3

定義 12: T = {T1, T2, T3} を上で述べた基本変換の集合とする。T の変換を適用してもそれ以上縮約できないとき、CDG G は T 既約である。

アルゴリズム I は、変換 T1、T2、T3 を用いて、次のように T 既約グラフを構築する。

  • CFG GCFG = (VGCFG, EGCFG, ⊤, ⊥) から始め、それを CDG GCDG = (VGCFG, EGCFG, C, ⊤, ⊥) に変換する。彩色ノードの集合 C は、解析対象の性質に関連する集合 ℰ によって定義されるイベントノードの集合である。すなわち、イベントノードを彩色ノードとして扱うことで、CFG を CDG としてモデル化する。
  • T の変換を適用して、GCDG を T 既約グラフに変換する。

B. アルゴリズム II: CFG から EFG への変換

CFG G を対応するイベントフローグラフ（EFG）GEFG に変換することで、極小の数の同値類を生成する線形時間のアルゴリズムを示す。直観的には、すべてのイベントトレースを計算する問題には CFG の各パスを個別に調べる必要があると思うかもしれないが、アルゴリズム II はそうでないことを示す。Linux カーネルの実証評価で観察したように、CFG パスの数は指数的に増大しうるが、イベントトレースの数はそうではない。そのようなシナリオでは、アルゴリズム II は CFG パスの数ではなくイベントトレースの数に比例する計算負荷しか必要としないので、非常に効率的である。

アルゴリズム II が生成するグラフは、まさに先に定義し、正確かつ効率的なパス依存解析に必要なすべてのイベントトレースを生成する極小のグラフであることを示したイベントフローグラフ（EFG）であると主張する。まず CFG から EFG への変換アルゴリズムを示し、その後、生成されるグラフが実際に EFG であることの証明を与える。アルゴリズム II をさらに説明するため、次の追加の定義を用いる。

定義 13: 有向グラフ G の各強連結成分（SCC）が GCG の単一のノードに縮約され、GCG のエッジが G のエッジから誘導されるとき、GCG は G の凝縮グラフである。したがって、GCG は有向非巡回グラフ（DAG）である。

第 III-D 節の手順 (1) で計算した CFG GCFG とイベントの集合 ℰ が与えられたとする。では、CFG GCFG をその EFG GEFG に変換するアルゴリズム II を詳しく説明する。

(1) T 既約グラフの構築: CFG GCFG から始め、アルゴリズム I を適用して T 既約グラフ GT-irr に変換する。

(2) 非彩色凝縮グラフの構築: GT-irr の非彩色ノードによって誘導される部分グラフ GI を計算する。次に、GI の非彩色凝縮グラフ GNCCG を構築する。

(3) 彩色凝縮グラフ: GT-irr の彩色ノードを GNCCG に追加して、新しい CDG GCCG を構築する。GT-irr において SCC と彩色ノード n の間にエッジが存在するなら、GCCG において、その SCC を縮約したノードと彩色ノード n の間にエッジを導入する。

(4) 凝縮 EFG の構築: アルゴリズム I を適用して、GCCG を T 既約グラフ GcEFG に変換する。

(5) EFG の構築: GcEFG に残っている縮約された各 SCC を、GT-irr にある元の SCC に展開し直して、GcEFG を GEFG に変換する。

注意 2: 手順 (4) の後に得られるグラフ GcEFG は凝縮 EFG である。さらに、手順 (5) の後に得られるグラフ GEFG が EFG であると主張する。

図 5(a-f) は、CFG（グラフ a）から始まり EFG（グラフ f）で終わる、アルゴリズム II が順に構築するグラフを示す。

アルゴリズム II の六つの段階。元の CFG、T 既約グラフ、強連結成分の凝縮、非彩色凝縮グラフ、彩色凝縮グラフ、最終的なイベントフローグラフ。
図 5. CFG から EFG への変換

C. アルゴリズム II の計算量

T 既約グラフの構築（手順 1 と 4）のアルゴリズム計算量は O(|V| + |E|) である。ここで |V| と |E| は、それぞれ CFG のノード数とエッジ数である。手順 (2) で SCC を検出するには、有向グラフの強連結成分を計算する Tarjan のアルゴリズム [16] を用いる。このアルゴリズムの実行時間も O(|V| + |E|) であり、アルゴリズム II の実行時間の計算量は線形の O(|V| + |E|) となる。

D. アルゴリズム I とアルゴリズム II の比較

アルゴリズム II が構築する EFG は、アルゴリズム I では不可能な CFG の重要な圧縮を実現する。アルゴリズム I が生成するグラフ GT-irr は、無関係な分岐ノードを含みうることを思い出されたい。例えば、suc(A) = {B, E} かつ suc(B) = {A, E} である二つの分岐ノード A と B を考える。ここで E はイベントノードである。分岐ノード A と B は無関係であり、除去されるべきである。二つの分岐ノード A と B からなる部分グラフは一意の後続 E を持つので、それらは凝縮 EFG GcEFG で除去される。上のシナリオでは、互いの後続となる分岐ノードが二つより多くありうるが、それらが同じイベントノードを後続として持つ限り、そのような分岐ノードはすべて無関係であり、アルゴリズム II によって除去されることに注意する。したがって、手順 (2-5) を含めることで、アルゴリズム II はアルゴリズム I を超える圧縮を実現できる。

二つ以上の後続を持つ分岐ノードの強連結成分（SCC）が存在することがあり、その場合、それらの分岐ノードは保持されなければならないことに注意する。そのようなシナリオの例を図 6 に示す。これは Linux カーネル（v3.12）の関数 cancel_bulk_urbs の EFG を描いている。この EFG では、分岐ノード c1 と c2 からなる SCC は、終端ノード ⊥ とイベントノード e1 の二つの後続を持つので保持される。

cancel_bulk_urbs のイベントフローグラフ。分岐ノード c1 と c2 が、イベントノード e1 と出口ノードの二つの後続を持つ強連結成分をなす。
図 6. 関数 cancel_bulk_urbs の EFG

E. EFG: 正しさの証明

アルゴリズム II において、手順 (5) の後に得られるグラフ GEFG が EFG であると主張するだけでは十分でない。ここで、アルゴリズム II が EFG を正しく生成することを証明する。これは、アルゴリズム II がすべての無関係な分岐ノードを除去することを証明することに帰着する。

定理 3: G を彩色された T 既約かつ非巡回のグラフとする。このとき、G の非彩色ノードを含む任意の部分グラフ S について |suc(S)| ≥ 2 である。

系 2: G を CFG とし、GcEFG を凝縮 EFG とする。このとき、GcEFG の非彩色ノードを含む任意の部分グラフ S について |suc(S)| ≥ 2 である。

系 3: アルゴリズム II が生成するグラフは、無関係な分岐ノードを一つも含まない。

V. 実証評価

パス依存解析を行うために、制御フローグラフ（CFG）ではなくイベントフローグラフ（EFG）を用いることの適用可能性と利点を示す実証評価を提示する。具体的には、次のことを評価する。

  • CFG から EFG へ移る際のノードとエッジの削減。
  • EFG では関連する分岐ノードだけが保持されるので、分岐ノードの削減。
  • パスの実行可能性を検査する労力の削減。

A. 実験設定

実証評価には Linux カーネル（v3.12）を用いる。解析で関心のあるイベント（ℰ）を定義するために、スピンの安全な同期の性質を考える。ℰ、CFG、EFG の計算には EnSoft の C-Atlas [17] プラットフォームを用いた。C-Atlas はまず Linux カーネル（v3.12）をコンパイルし、さまざまなプログラムの成果物の間の関係（呼び出し、制御フロー、データフローなど）のデータベースを事前に計算する。この処理には 34 分かかった。次に、C-Atlas のデータベースにクエリを発行して、すべてのスピン同期オブジェクト 𝒫 を見つける。このクエリは、スピンのロック関数（spin_lock、spin_trylock）とアンロック関数（spin_unlock）にパラメータとして渡されるすべての変数を特定する。

第 III-D 節の手順 (1-3) に従い、テイント解析の手法 [11] に基づいて C-Atlas の API を用いる Java プログラムを書いた。このプログラムは、すべてのオブジェクト p ∈ 𝒫 について、p に対して定義されたイベント e1 と e2 に加え、p がパラメータや戻り値として他の関数に渡されるものを含む p の関連するデータフローのイベントを特定することで、集合 ℰp を決定する。これらのイベントに基づき、各オブジェクト p について解析が必要な Linux カーネルのすべての関数（関連する関数と呼ぶ）を決定する。その後、C-Atlas の API を用いて、集合 ℰp に基づき、関連する各関数の EFG を対応する CFG から構築する Java プログラムを書いた。

Linux カーネル（v3.12）には 531 個のスピンオブジェクトがあり、すべてのオブジェクトの解析のための関連する関数は合計 3,894 個である。アルゴリズム II を用いた CFG から EFG への変換は、すべての関連する関数について 9 秒かかった。すべての実験は、Windows 8、Intel Core i7 2.40Ghz、8GB RAM のラップトップコンピュータで行った。

表 I に、Linux カーネル（v3.12）の成果物の数をまとめる。LOC はコード行数、ソースファイルはソースファイル、関数は関数、関連関数は関連する関数、スピンオブジェクトはスピンロックオブジェクト、イベントはスピンの安全な同期の性質に関心のあるイベントである。

表 I. Linux カーネル（v3.12）のプログラムの成果物
LOCソースファイル関数関連関数スピンオブジェクトイベント
11,479,68336,61363,1903,8945318,086

B. 実験 I: CFG から EFG への削減

CFG から EFG へ移る際のノードとエッジの削減を示す。EFG はイベントノードと関連する分岐ノードからなり、削減は非イベントノードと無関係な分岐ノードの除去によるものであることを思い出されたい。

表 II は、すべての関連する関数（FRelevant）について、CFG と EFG の両方のノード、エッジ、分岐ノードの分布を示す。ノード数の多いグラフを評価すると、(> 30) 個のノードを持つ CFG が 1,058 個であるのに対し、EFG は 15 個しかなく、∼99% の削減である。エッジ数の多いグラフを評価すると、(> 30) 本のエッジを持つ CFG が 1,309 個であるのに対し、EFG は 76 個しかなく、∼94% の削減である。分岐ノード数の多いグラフを評価すると、(> 10) 個の分岐ノードを持つ CFG が 597 個であるのに対し、EFG は 107 個しかなく、∼90% の削減である。パスの実行可能性の検査が簡単な場合を評価すると、分岐ノードを持たない CFG は 559 個であるのに対し、EFG は 1,458 個であり、161% の増加である。

表 II. Linux カーネル（v3.12）の関連する 3,894 個の関数（FRelevant）に対する CFG と EFG の統計
グラフ成果物分布
CFGノード≤ 56 → 1011 → 3031 → 50> 50
1857591,892614444
エッジ≤ 56 → 1011 → 3031 → 50> 50
2666611,658691618
分岐ノード= 01 → 56 → 1011 → 30> 30
5591,996742493104
EFGノード≤ 56 → 1011 → 3031 → 50> 50
2,1851,246448141
エッジ≤ 56 → 1011 → 3031 → 50> 50
2,1599107496313
分岐ノード= 01 → 56 → 1011 → 30> 30
1,4582,0622671025

CFG から EFG への削減は、複雑な CFG、特に分岐ノードの数が多い CFG で特に重要である。表 III に、FRelevant のうち分岐ノードの数が最も多い 10 個の関数の削減を挙げる†。P(%) の列は、ノード、エッジ、分岐ノードの削減率を表す。例えば、関数 xs_udp_data_ready では、CFG から EFG への削減は、ノードが 1,101 から 8 へ、エッジが 1,513 から 11 へ、分岐ノードが 317 から 4 へである。

† Linux カーネル（v3.12）におけるスピンの安全な同期の性質に関するすべての関連する関数の完全な比較は [10] で入手できる。

表 III. CFG と EFG の比較
関数名ノードエッジ分岐ノード
CFGEFGP(%)CFGEFGP(%)CFGEFGP(%)
xs_udp_data_ready11,101899.31,5131199.3317498.7
tcp_v4_err21,024799.31,400999.4287399.0
udpv6_queue_rcv_skb28381798.01,1532897.62441295.1
udp_queue_rcv_skb28381698.11,1522697.72431195.5
tcp_v6_rcv27322496.79994195.92051891.2
tcp_v4_rcv27312496.79984195.92051891.2
tcp_v6_err2720699.2984799.3203299.0
tcp_recvmsg25834193.07907590.51733579.8
tcp_v4_conn_request26051897.08223296.11701690.6
tcp_close2601998.58151098.8167298.8

スピンロックのオブジェクト: 1: rpc_xprt.transport_lock, 2: sock.sk_lock.slock.

C. 実験 II: 手作業による検証

この実験では、Linux カーネル（v3.12）から 400 個のロックのイベントを無作為に選び、二人の分析者‡に、それらのイベントについてスピンの安全な同期の性質を手作業で検証するよう依頼した。分析者には次のことを報告するよう依頼した。1) 各イベントの解析時間、2) ロックのイベント e1(p) の後にアンロックのイベント e2(p) が続かないパス（すなわち違反パス）の場合に、パスの実行可能性を判断するために用いた条件（分岐ノード）、3) 各ロックのイベントについての「バグあり」または「安全」の判定。ここでバグありとは、違反パスが実行可能であることを意味する。

‡ プログラミング経験 ∼ 9 年の博士課程の学生二人。

実験は 2 ラウンドで行い、各ラウンドで分析者に 200 個のイベントの検証を依頼した。第 1 ラウンド R1 では、第一の分析者 A1 は CFG だけを用い、もう一人の分析者 A2 は EFG を用いた。第 2 ラウンド R2 では、A1 が EFG を用い、A2 が CFG を用いた。分析者には次の情報を与えた。

  • 関数 fi と、検証が必要なロックのイベント ej(p) の行番号。
  • ロックのイベント ej(p) の解析のためのすべての関連する関数の集合。
  • ℰp のイベントに対応するノードは、対応する CFG と EFG で強調表示される。すべての分岐ノードはひし形である。

パスの実行可能性の検査の場合、分析者は、パスが実行されるために真でなければならない条件のブール結合、すなわち AND(∧)、OR(∨)、NOT(¬) を計算する。次に、その結合の充足可能性を検査する。簡単のため、分析者は割り当てられたグラフ内の情報だけから条件の間の相関を推論できる。

表 IV に、各ラウンドにおける各分析者の解析時間と、安全なイベントとバグのあるイベントの数を示す。また、パスの実行可能性の検査（Feas.）を行った回数も示す。両方の分析者は安全とバグありについて同一の判定に至り、実行可能性の検査に用いた条件/分岐ノードの集合もまったく同じものを報告した。R2 の A1 と R1 の A2 は、検証を行うには EFG で十分であり、関連する分岐ノードは実行可能性の検査に十分であったと報告した。実行可能性の検査の回数は、CFG を用いる場合と EFG を用いる場合とで異なる。これは、実行可能性を検査する CFG の複数のパスがたまたま同値であり、そのため対応する EFG では一つのパス（イベントトレース）で表される場合に起きる。

さらに、両方の分析者は新しいバグ [9] を報告し、それは Linux コミュニティに受け入れられ、複数のカーネルバージョンにまたがるものであることが判明した。

表 IV. 対照実験の結果
分析者ラウンド 1 (R1)ラウンド 2 (R2)
安全バグあり実行可能性時間安全バグあり実行可能性時間
A120004910 時間 44 分1991212 時間 49 分
A22000183 時間 16 分19915811 時間 22 分

VI. EFG の応用研究

この研究では、Linux カーネル（v3.12）の実際の例を示し、手続き間のパス依存の検証で EFG を用いることの適用可能性と利点を説明する。読み取りセマフォの同期オブジェクト（cpufreq_rwsem）について、すべてのロックのイベント（down_read、down_read_trylock）の後に、すべての実行可能な実行パスで常にアンロックのイベント（up_read）が続くことを検証することで、安全な同期の性質の検証を説明する。この研究には三つの関数 cpufreq_bp_resume（f1）、cpufreq_cpu_get（f2）、cpufreq_cpu_put（f3）が関わる。図 7 は解析のための関連する関数を捉えており、f1 がまず f2 を呼び出し、次に f3 を呼び出すことを示す。解析に EFG を用いる第一の利点は、EFG が対応する CFG よりも単純でコンパクトなことである。CFG の統計は表 V に示し、EFG は図 7 に示す。

表 V. 応用研究の CFG の統計
関数名ノードエッジ分岐ノード
cpufreq_bp_resume1662
cpufreq_cpu_get173111
cpufreq_cpu_put661
cpufreq_bp_resume、cpufreq_cpu_get、cpufreq_cpu_put の手続き間のイベントフローグラフ。ロックのイベント、最初の関数から他の二つへの呼び出し、実行可能性の議論に用いる分岐ノードを示す。
図 7. 関数 cpufreq_cpu_get におけるロックのイベントの手続き間の検証

f2 には、CFG のパスの四つの同値類（すなわち一意のイベントトレース）に対応する四つのパスが存在する。それらの同値類のうち三つは、検証が必要な e1 を含む。Linux カーネルでは、関数（down_read_trylock）はロックが起きれば 1 を、そうでなければ 0 を返す。この例では、e1 のイベントはロックが起きなければ true に評価され、そうでなければ false に評価される。つまり、e1 を含む三つの同値類のうち、true の分岐を含む同値類は、ロックが起きるとき実行不可能である。したがって、この分岐を含むパスは検証を必要としない。次に、e1 の false の分岐を含む他の二つの同値類については、それらのパスはアンロックのイベント（up_read）を持たなければならない。f2 では、分岐ノード c3 の true の分岐を含むパスはアンロックのイベント e2 を含む。つまり、それらのパスではイベント e1 は検証される。しかし、c3 の false の分岐を含むパス（パス A）には、アンロックのイベントがない。f2 の EFG だけを見れば、このパス A は検査対象の性質に関する違反に寄与すると結論づけられる。しかし、パス A のロックのイベント e1 は、関数 f1 を介して、関数 f3 のアンロックのイベント e3 によって検証される。これは次のように行われる。

f1 では、c3 の false の分岐に対応するパス（パス A）は二つのパスに膨らむ。c1 の true の分岐を通るパス B と、c1 の false の分岐を通るパス C である。パス B ではアンロックのイベントが起きずに関数が戻るので、バグに寄与すると結論づけられる。しかし、f2 のパス A がとられる場合、パス B は実行不可能であることがわかる。その理由は次のとおりである。(1) パス A は c3 の false の分岐を通ってとられるパスであり、c3 は false に評価される。(2) c1 = c3 であり、変数 policy は f2 から f1 に返される。したがって、パス A がとられるなら、c1 は false に評価されなければならない。つまり、パス A がとられるとき、パス B は実行不可能である。言い換えれば、パス B は検証の必要がない。残るのは、実行可能でアンロックのイベントを持つべきパス C である。

f1 では、パス C は f3 を呼び出す。f3 では、パス C は、それぞれ c4 の true と false の分岐を通るパス D と E に膨らむ。パス B と同様の推論を用いると、パス D はバグに寄与すると結論づけられる。しかし、パス A がとられるとき、パス D は実行不可能である。その理由は、パス A は c3 の false の分岐を通ってとられるパスであり、c2 の false の分岐も通ることを意味するからである。したがって、c2 は false に評価される。言い換えれば、（cpufreq_disabled()）は false を返さなければならず、パス A がとられるなら c4 は false に評価される。つまり、パス A がとられるとき、パス D は実行不可能である。言い換えれば、パス D は検証の必要がない。残るのは、実行可能でアンロックのイベントを持つ一つのパス E である。最終的に、安全な同期の性質に対する違反はなく、関数 f2 の e1 は、f2 の e2（手続き内）と、f1 を介した f3 の e3（手続き間）によって検証されると結論できる。

この事例研究は次のことを示す。1) EFG を用いて、手続き内と手続き間の両方のパス依存解析を効率よく正確に行える。また、2) EFG に含まれる分岐ノードは、イベントに関連し、パスの実行可能性の判断に関連する分岐ノードである。この事例研究では、分岐ノードの数は、対応する CFG の 14 個に対し 5 個に削減される。

VII. 関連研究

イベントフローグラフは、Neginhal et al. の研究 [18] に着想を得ている。彼らはイベントビューの概念を導入した C-Vision ツールを開発した。C-Vision の縮約は、除去すべき無関係なノード/エッジを決めるためのユーザー入力に基づく。コンパクトな CFG を計算するアルゴリズム的な概念はない。これに対し本論文は、解析対象の性質に関心のある与えられたイベントに関して、イベントフローグラフを計算する線形時間アルゴリズムを示す。EFG は効率的なパス依存解析を可能にし、パス依存解析のために研究されてきた既存の解析手法を補完できる。

多くのモデル検査の手法 [19] は、プログラムのモデルが時相論理で記述された与えられた性質を満たすかどうかを検証するために開発された。これらの手法はスケーラビリティを犠牲にして精度と正確さを重視する。これらの手法の多くはすべてのパスを探索し、状態空間爆発の問題を招く [20], [21], [22], [8], [23]。

我々の手法は、CFG パスの同値類を形成し、各同値類から一つのパスを解析することで、問題となる指数的な数のパスに対処する。Linux カーネルの実証評価は、特にパスと分岐ノードの数が多い複雑な CFG について、EFG がノード、エッジ、分岐ノードの点で大幅な削減を実現することを示す。したがって、CFG の代わりに EFG を用いて効率的なモデル検査の解析を行うことは非常に有益でありうる。

別の研究の流れは、解析を行う前に実行不可能なパスを特定して除去することに焦点を当てている。[24] は、多くのプログラムでパスの 9-40% を実行不可能なパスとして静的に特定できると主張した。Goldberg et al. [25] は定理証明を適用し、Ngo と Tan [3] は実行不可能なパスを特定するヒューリスティックな手法を提案した。Vojdani et al. [4] は大域不変条件の概念を適用し、実行不可能なパスを除去して指数的に多数のパスに対処する。Holley と Rosen [26] は、実行不可能なパスを残りのパスから区別するために限定付きデータフロー解析を導入した。他の研究者は、実行不可能なパスを検出するために記号評価を用いた [5], [6], [7], [8]。

実行不可能なパスの検出は、パスに沿った条件の充足可能性の検査に依存するので高コストである。EFG は、パスの実行可能性の検査のための計算を最小化できる。Linux カーネルの実証評価（第 V-C 節）で示したように、同値類を形成するための関連する分岐ノードは、実行可能性の検査にも十分であった。

正確なパス依存解析がもたらすもう一つの課題は、異なるパスに沿った実行の効果/影響の分離である。多くのヒューリスティックな方式は、論理和を用いて異なるパスの効果を選択的に結合または分離する、部分的なパス依存の解を目指している [1], [27], [28], [29], [30], [21], [8]。他の手法 [4], [31], [23], [32], [1], [33] は、分岐ノードから分岐する個々の実行パスを解析することで、分岐ノードの関連性を判断する。この処理には実行パスの数に比例する計算が必要である。

二分決定図（BDD）[34] は、状態空間の爆発を抑える方法として、プログラム分析のさまざまな文脈で用いられてきた [6], [35], [36]。二分決定木（BDT）から BDD への縮約も、パス依存解析に用いられてきた [37], [38]。EFG は BDT から BDD への縮約の代わりに使える。EFG はブール式を単純化するための一般的な手法をなすが、パス依存解析については BDD に対していくつかの利点がある。BDT から BDD への変換は、アルゴリズム I（第 IV-A 節）の議論で示したものと似ている。BDT から BDD への縮約とは異なり、EFG の変換はさらなる削減を実現し、入力の CFG が非巡回であることを必要としない。EFG の変換は、有向グラフの強連結成分を計算する Tarjan の線形時間アルゴリズム [16] を組み込むことで、巡回グラフを扱う。

すべてのパスを探索する計算量を克服するため、[39], [15] で CFG の枝刈りの手法が提案されている。EFG の変換はグラフのサイズをさらに削減するので、EFG はそれらの手法を補完できる。データフローグラフを最適化するために、Choi et al. [40] と Ramalingam [41] によって他の枝刈りの手法も導入されている。いくらか共通点はあるが、それらの手法はパス依存解析にはあまり適さない。[40], [41] で定義された同値関係は、データフロー解析の問題に関して定義されている。この同値関係は EFG で定義されたものとは異なる。パス依存解析では一意のイベントトレースを保存する必要があり、それは引用した手法では実現されない。

VIII. 結論

効率的かつ正確なパス依存解析には、(a) CFG の指数的に増大する数のパスの解析と、(b) CFG のパスの実行可能性の検査という課題がある。本論文は、これらの課題に対処するために CFG パスの同値類を用いる手法を示す。イベントフローグラフ（EFG）の概念を導入し、CFG を EFG に圧縮することで同値類を計算する線形時間アルゴリズムを示す。EFG の各パスは、CFG のパスの一つの同値類を表す。CFG の個々のパスすべてではなく、EFG が生成する同値類だけでパス依存解析を行えば十分であることを示す。

Linux カーネル（v3.12）の実証評価は、EFG を用いることでパス依存解析の効率を大幅に改善できることを示す。さらに、対照実験の結果は、EFG は検証すべきパスが少なく、実行可能性の検査のための分岐ノードも少ないので、対応する CFG に比べて人間に理解しやすくコンパクトであることを示す。EFG を応用して、手続き内と手続き間のパス依存解析を行う例を示した。

今後の課題として、Linux カーネルにおける安全な同期の性質の検証とメモリリークの解析のための検証フレームワークを現在開発している。このフレームワークは、EFG に基づくパス依存解析を活用し、Linux カーネルのような大規模なシステムにもよくスケールする健全な検証フレームワークの開発を可能にする。

付録

定理と系の証明

定理 1 の証明. 同値関係 ℛℰ は CFG パスを同値類に分割し、一つの同値類のすべてのパスは同じイベントトレースを持ち、異なる同値類にある CFG パスは異なるイベントトレースを持つ。

GEFG は、イベントノードと関連する分岐ノードからなる、与えられた CFG G のノード誘導部分グラフなので、EFG パス S が与えられればそれは一意のイベントトレース T を生成し、逆にイベントトレース T が与えられればイベントトレースが T となる一意の EFG パス S が存在する。したがって、ℛℰ の同値類と EFG GEFG のパスとの間には一対一かつ上への写像が存在する。

定理 2 の証明. すべての CFG パスでオブジェクト p について性質 P が成り立つなら、対応するすべてのイベントトレースについても明らかに成り立つ。したがって、論じなければならないのは、CFG パス S でオブジェクト p について性質 P が破られる場合である。T をパス S のイベントトレースとする。パス S は多くの分岐ノードを通りうる。トレース T を持つ実行可能なパスの存在を判断するうえで重要なのは、そのパス上の関連する分岐ノードだけであることを論じる。トレース T を持つ実行可能な CFG パスが存在するのは、S 上の関連する分岐ノードに関して実行可能な、トレース T を持つパス S′ が存在するとき、かつそのときに限ることを論じる。

トレース T を持つすべてのパスが関連する分岐ノードに関して実行不可能なら、無関係な分岐ノードを加えても実行不可能なパスを実行可能なパスに変えることはできないので、S と同値なすべてのパスも実行不可能である。一方、関連する分岐ノードに関して実行可能な、トレース T を持つパス S′ が存在するとする。無関係な分岐ノードの定義により、同値類は無関係な分岐ノードにおいて可能なすべての分岐を通るパスを持つので、パス S′ がいくつかの無関係な分岐ノードを持つために実行可能でないなら、それらのノードで実行可能な分岐を選んで、実行可能で S′ と同値な新しい CFG パスを構築できる。したがって、S 上の関連する分岐ノードに関して実行可能な、トレース T を持つパス S′ が存在するなら、トレース T を持つ実行可能な CFG パスが常に存在する。

したがって、パス S で性質 P が破られるなら、次のことが成り立つ。(a) S が S 上の関連する分岐ノードに関して実行可能なら、S の同値類に実行可能なパスがあり、P の違反は真陽性である。(b) S が S 上の関連する分岐ノードに関して実行可能でないなら、S と同値なすべてのパスも実行可能でない。

定義 14: 有向グラフ G における部分グラフ S の境界は boundary(S) で表され、suc(u) ∈ suc(S) となるようなノード u ∈ S の集合である。

定理 3 の証明. 非彩色ノード u ∈ G が後続を一つしか持たないなら、それは変換 T1 によって除去される。したがって、G は T 既約なので、すべての非彩色ノード u ∈ G について |suc(u)| ≥ 2 である。また、仮定により G は非巡回グラフである。これら二つの事実を用いて、すべての部分グラフ S が S の外に少なくとも二つの後続を持つノードを持ち、したがって |suc(S)| ≥ 2 であることを示す。

Pv0 → vn : (v0, v1), (v1, v2), ⋯ , (vn−1, vn)) を部分グラフ S の極大パスとする。vn はこの極大パス P の終端ノードなので、その後続はパス P 上にない S の別のノードではありえない。また、Gc は非巡回グラフなので、vn の後続はパス P 上の別のノードでもありえない。したがって vn は境界ノードでなければならず、そのすべての後続は部分グラフ S の外になければならない。vn は非彩色ノードなので |suc(vn)| ≥ 2 である。S のノードである vn が S の外に少なくとも二つの後続を持つので、|suc(S)| ≥ 2 となる。以上で証明を終える。

系 2 の証明. 凝縮 EFG GcEFG は、EFG 構築アルゴリズムの手順 (4) から得られるグラフであることに注意する。構築の仕方から、凝縮グラフ GcEFG は彩色された T 既約グラフである。また、構築の仕方から GcEFG は非巡回グラフである。上の定理を GcEFG に適用すると、系の証明が得られる。

系 3 の証明. 構築の仕方から、アルゴリズム II の手順 (1) の後に得られるグラフ GT-irr は、イベントノード、関連する分岐ノード、アルゴリズム I が保持した無関係な分岐ノードだけからなる。ここで、アルゴリズム II の手順 (4) で GcEFG を構築するとき、すべての無関係な分岐ノードが除去されることを論じる。無関係な分岐ノードの定義（定義 7）によれば、c とそのすべての分岐エッジを含む部分グラフ S があり、S がイベントノードを持たず、|suc(S)| = 1 であるとき、ノード c は無関係である。この定義と系 2 から、GcEFG は無関係な分岐ノードを一つも含まない。したがって、アルゴリズム II が生成する最終的なグラフは、GcEFG のノードとすべてのイベントノードからなるので、やはり無関係な分岐ノードを一つも含まない。

謝辞

本研究は、契約番号 FA8750-12-2-0126 のもとで DARPA の支援を受けた。

参考文献

  1. M. Das, S. Lerner, and M. Seigle, “ESP: Path-sensitive program verification in polynomial time,” ACM SIGPLAN Notices, 2002.
  2. L. Carter, J. Ferrante, and C. Thomborson, “Folklore confirmed: reducible flow graphs are exponentially larger,” in Proceedings of the 30th ACM SIGPLAN-SIGACT, 2003.
  3. M. Ngo and K. Tan, “Detecting large number of infeasible paths through recognizing their patterns.” ACM, 2007.
  4. V. Vojdani and V. Vene, “Goblint: Path-sensitive data race analysis,” in Annales Univ. Sci. Budapest., Sect. Comp, 2009.
  5. A. Navabi, N. Kidd, and S. Jagannathan, “Path-sensitive analysis using edge strings,” 2010.
  6. T. Ball and S. K. Rajamani, “Bebop: A path-sensitive interprocedural dataflow engine.” ACM, 2001, pp. 97–103.
  7. Z. Xu and J. Zhang, “Path and context sensitive inter-procedural memory leak detection,” in The Eighth International Conference on Quality Software, 2008s.
  8. I. Dillig, T. Dillig, and A. Aiken, “Sound, complete and scalable path-sensitive analysis,” in ACM SIGPLAN Notices, vol. 43, no. 6. ACM, 2008, pp. 270–280.
  9. “Reported bug,” https://bugzilla.kernel.org/show_bug.cgi?id=68011.
  10. https://sites.google.com/site/efgwebsite/.
  11. M. Potet, L. Mounier, and N. Tapus, “Detecting software vulnerabilities static taint analysis,” 2009.
  12. “Common weakness enumeration,” http://cwe.mitre.org.
  13. M. N. Wegman and F. K. Zadeck, “Constant propagation with conditional branches,” TOPLAS, 1991.
  14. C. Click, “Global code motion/global value numbering,” in ACM SIGPLAN Notices. ACM, 1995.
  15. H. K. Cho, T. Kelly, Y. Wang, S. Lafortune, H. Liao, and S. Mahlke, “Practical lock/unlock pairing for concurrent programs,” in Code Generation and Optimization (CGO), 2013.
  16. R. Tarjan, “Depth-first search and linear graph algorithms,” SIAM journal on computing, vol. 1, no. 2, pp. 146–160, 1972.
  17. “Ensoft corp.” http://www.ensoftcorp.com.
  18. S. Neginhal and S. Kothari, “Event views and graph reductions for understanding system level c code,” in ICSM, 2006.
  19. R. Jhala and R. Majumdar, “Software model checking,” ACM Computing Surveys (CSUR), vol. 41, no. 4, p. 21, 2009.
  20. E. Clarke, D. Kroening, and F. Lerda, “A tool for checking ANSI-C programs,” in Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2004, pp. 168–176.
  21. G. Balakrishnan, S. Sankaranarayanan, F. Ivančić, O. Wei, and A. Gupta, “SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement,” Static Analysis, 2008.
  22. W. R. Harris, S. Sankaranarayanan, F. Ivančić, and A. Gupta, “Program analysis via satisfiability modulo path programs,” in ACM Sigplan Notices, vol. 45, no. 1. ACM, 2010, pp. 71–82.
  23. N. Dor, S. Adams, M. Das, and Z. Yang, “Software validation via scalable path-sensitive value flow analysis,” in ACM SIGSOFT Software Engineering Notes, vol. 29, no. 4, 2004.
  24. R. Bodik, R. Gupta, and M. L. Soffa, “Refining data flow information using infeasible paths,” in Software Engineering—ESEC/FSE’97. Springer, 1997, pp. 361–377.
  25. A. Goldberg, T. C. Wang, and D. Zimmerman, “Applications of feasible path analysis to program testing,” in Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis.
  26. L. H. Holley and B. K. Rosen, “Qualified data flow problems,” IEEE Transactions on Software Engineering, no. 1, 1981.
  27. D. Dhurjati, M. Das, and Y. Yang, “Path-sensitive dataflow analysis with iterative refinement,” in Static Analysis. Springer, 2006, pp. 425–442.
  28. J. Fischer, R. Jhala, and R. Majumdar, “Joining dataflow with predicates,” in ACM Software Engineering Notes, 2005.
  29. L. Mauborgne and X. Rival, “Trace partitioning in abstract interpretation based static analyzers,” in Programming Languages and Systems. Springer, 2005, pp. 5–20.
  30. S. Sankaranarayanan, F. Ivančić, I. Shlyakhter, and A. Gupta, “Static analysis in disjunctive numerical domains,” in Static Analysis. Springer, 2006, pp. 3–17.
  31. Y. Wang, Y. Gong, Q. Xiao, and Z. Yang, “An improved global analysis for program bug checking,” in International Conference on Test and Measurement, 2009.
  32. J. Jaffar and V. Murali, “A path-sensitively sliced control flow graph.”
  33. H. Cui, G. Hu, J. Wu, and J. Yang, “Verifying systems rules using rule-directed symbolic execution,” in ACM SIGPLAN Notices, 2013.
  34. S. B. Akers, “Binary decision diagrams,” IEEE Trans. Computers, vol. 27, no. 6, pp. 509–516, 1978.
  35. R. Manevich, G. Ramalingam, J. Field, D. Goyal, and M. Sagiv, “Compactly representing first-order structures for static analysis,” in Static Analysis, ser. Lecture Notes in Computer Science, 2002.
  36. J. Whaley and M. S. Lam, “Cloning-based context-sensitive pointer alias analysis using binary decision diagrams,” in Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation. ACM.
  37. Y. Xie and A. Aiken, “Saturn: A scalable framework for error detection using boolean satisfiability,” ACM Trans. Program. Lang. Syst., vol. 29, no. 3, May 2007.
  38. X. Zhang, R. Gupta, and Y. Zhang, “Efficient forward computation of dynamic slices using reduced ordered binary decision diagrams,” in ICSE, 2004.
  39. M. Ramanathan, A. Grama, and S. Jagannathan, “Path-sensitive inference of function precedence protocols,” in ICSE, 2007.
  40. J.-D. Choi, R. Cytron, and J. Ferrante, “Automatic construction of sparse data flow evaluation graphs,” in Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1991, pp. 55–66.
  41. G. Ramalingam, On sparse evaluation representations. Springer, 1997.