Solving Shape-Analysis Problems in Languages with Destructive Updating 増山 (米澤研究室) 小野 (西田研究室)

参考文献 Mooly Sagiv et al , Solving Shape-Analysis Problems in Languages with Destructive Updating ACM Transactions on Programming Languages and Systems , 1998

概要 Shape-Analysisとは? 理論 / 解析アルゴリズム 解析の利点、欠点 解析の安全性(safety) 応用 / まとめ DSG SSG 変換関数 / interpretation 解析の利点、欠点 解析の安全性(safety) 応用 / まとめ

Shape-Analysisとは?

Shape-Analysisとは? データの形を静的に解析 入力が リストならば出力もリストを保証 木ならば出力も木を保証 Pointer-Analysis , Alias-Analysis , Type Checking の問題を解くことができる

用途 デバッグツールとして使用 並列化に使用 共有されないデータを見つける

簡単な例: リストのreverse

簡単な例: リストのreverse

簡単な例: リストのreverse

理論 / 解析アルゴリズム

対象言語 破壊的代入を伴うimperativeな言語 Cons-cell を扱う x : = nil x.sel := nil (sel ∈ { car, cdr }) x := new x := y x.sel := y x := y.sel kill generate

プログラムの形式化 プログラムはControl-flow Graph (V,A)で表現 (V.. vertex, A .. arc) 制御の流れを示す

Shape Graph <Ev,Es> ノード 変数 PVar メモリのセルを表す shape_node car,cdrというセレクタを持つ 枝 変数から出る枝　variable-edge (Ev) shape_nodeから出る枝　selector_edge (Es)

DSG: deterministic shape-graph 定義 |Ev(x)| ≦ 1 (x ∈ PVar) |Es(n,sel)| ≦ 1 (n ∈ shape_nodes) DSGのクラスをDSGと書く 実行時のメモリ状態を表現する

Concrete Semantics [] : DSG → DSG

DSGとControl-Flow Graphの 関係

Collecting Semantics 定義　cs: V → 2DSG あるプログラムポイントでの実現しうるメモリ状態全ての集合

SSG: Static Shape-Graph 定義 Shape-Graph(SG#)と、shape_nodeの共有状態を表す真偽値関数(is#)とのペア(<SG#, is#>) shape_nodeは変数の集合で名前付けされている　(例 n{x,y,z}) SSGのクラスをSSGと書く あるプログラムポイントでのメモリ状態を抽象化している

DSGとSSGとControl-Flow Graphの関係

DSGからSSGへの変換 定義 β: DSG → SSG β(l) : shape_node間の変換 DSG上でlを指す変数集合で名前付け is#(n) : SSGのshape_node→{true,false} iis[Es](l) = |{<*,*,l>∈Es}| ≧ 2 is#(n) =

変換の例 x y z w n{w,y} n{z} nφ n{x}

複数のDSGのマージ α: 2DSG→SSG

DSGのマージの例

Concrete and Abstract Properties

Safe Approximation 定義 DSGでpが成り立つならば、SSG上でもp#が成り立つ compatible , = などはSafe Approximationである その対偶である!p# ⇒ !pが重要

Abstract Interpretation DSG SSG Abstract Interpretation DSG SSG Abstract Interpretation SSG

Abstract Semantics 定義 []#: SSG → SSG x := nil x.sel := nil x := new x := y x.sel := y x := y.sel それぞれの文について定義する

x := nil {v7 : t1 := nil}

x.sel := nil {v11 : y.cdr := nil}

x := new 新しく共有されていないshape_nodeを作成 Evに新たな枝 [x,n{x}]を加える

x := y {v6 : y := x}

x.sel := y {v12 : y.cdr := t}

x := y.sel {v8 : t1 := x.cdr}

Shape-Analysis Algorithm 　Control-Flow Graphの各頂点に対して上の式から計算 できるleast fixed pointを求める 　反復法 　SSGのshape_nodeは2|Pvar|で抑えられ、反復によって、 枝数は単調に増加する　⇒　解析は停止する

データタイプを表すSSG

Concretization Function 定義 γ: SSG → 2DSG SSGから実現されうるDSGの集合

この解析の利点、欠点

Strong nullification

e.cdr := t iis#(n{t}) = true n{y,z},n{x,y}からn{t}へ の枝が消せる ⇒ iis#(n{t}) = false ⇒ is#(n{t}) = false

この解析の問題点 nφが多くのノードを抽象化 ノード数がプログラムの変数の数の指数オーダー 精度を落とす原因 nφをより詳しく分類する 分岐が多いプログラムでは特に問題 精度は落ちるがノード数を減らした解析は可能

解析の安全性 (safety)

安全性 Local Safety ∀SG∈DSG,st Grobal Safety ∀v ∈ V (vはControl-Flow Graphのvertex) の定義 SGi# = <<Evi#,Esi#>,isi#>

安全性の証明の流れ

応用 / まとめ

応用 Aliasesの発見 共有されうるデータの発見 あるプログラムポイントvで、2つのアクセスパスe1,e2が 同じcons-cellを指すような実行があるか?　(may) 必ず同じcons-cellを指すか? (must) 共有されうるデータの発見

まとめ Shape-Analysis ヒープの状態を静的に解析 変数のaliasingを正確に追うことである程度正確な解析が可能 状態数の抑制と精度のトレードオフあり