Solving Shape-Analysis Problems in Languages with

Solving Shape-Analysis
Problems in Languages with
Destructive Updating
増山 (米澤研究室)
小野 (西田研究室)
参考文献
• Mooly Sagiv et al , Solving ShapeAnalysis Problems in Languages with
Destructive Updating
ACM Transactions on Programming
Languages and Systems , 1998
概要
• Shape-Analysisとは?
• 理論 / 解析アルゴリズム
– DSG
– SSG
– 変換関数 / interpretation
• 解析の利点、欠点
• 解析の安全性(safety)
• 応用 / まとめ
Shape-Analysisとは?
Shape-Analysisとは?
• データの形を静的に解析
– 入力が
• リストならば出力もリストを保証
• 木ならば出力も木を保証
– Pointer-Analysis , Alias-Analysis , Type
Checking の問題を解くことができる
用途
• デバッグツールとして使用
• 並列化に使用
– 共有されないデータを見つける
簡単な例: リストのreverse
簡単な例: リストのreverse
簡単な例: リストのreverse
理論 / 解析アルゴリズム
対象言語
• 破壊的代入を伴うimperativeな言語
• Cons-cell を扱う
x : = nil
kill
x.sel := nil (sel ∈ { car, cdr })
x := new
x := y
generate
x.sel := y
x := y.sel
プログラムの形式化
• プログラムはControl-flow Graph (V,A)で表
現 (V.. vertex, A .. arc)
• vertex
– 代入文か条件式がひとつのvertexに対応
• 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の
関係
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
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
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
SSG
SSG
SSG
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
x
w
w
y
y
n{x}
nφ
n{w,y}
z
z
n{z}
複数のDSGのマージ
• α: 2DSG→SSG
DSGのマージの例
Concrete and Abstract Properties
Safe Approximation
• 定義
• DSGでpが成り立つならば、SSG上でもp#
が成り立つ
• compatible , = などはSafe Approximationで
ある
• その対偶である!p# ⇒ !pが重要
Abstract Interpretation
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
DSG
SSG
Abstract
Interpretation
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を正確に追うことである程度正
確な解析が可能
– 状態数の抑制と精度のトレードオフあり

Download Report