This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( www.kmonos.net ), under my own understanding of.

Presentation on theme: "This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( www.kmonos.net ), under my own understanding of."— Presentation transcript:

1 This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of the papers published at PLDI So, it may include many mistakes etc For your correct understanding, please consult the original paper and/or the authors’ presentation slide!

2 The Set Constraint/CFL Reachability Connection in Practice
　　 k.inaba (稲葉 一浩), reading: PLDIr #12 Mar 12, 2011 paper written by J. Kodumal and A. Aiken (PLDI 2004) The Set Constraint/CFL Reachability Connection in Practice

3 解きたい問題（の例） 「tainted とマークされた値が untainted マークの変数に入らない」の静的検証
int id(int y1) { int y2 = y1; return y2; } int main(void) { tainted int x1; int z1, x2; untainted int z2; z1 = id(x1); // call site 1 z2 = id(x2); // call site 2 }

4 典型手法: グラフの到達可能性問題と見なす
int id(int y1){int y2=y1; return y2;} int main(void) { tainted int x1; int z1, x2; untainted int z2; z1 = id(x1); // call site 1 z2 = id(x2); // call site 2 } 危 から 安 に行ける？ x1 y1 y2 z1 z2 x2 危 安

5 Betterな精度の典型手法: グラフのCFL到達可能性問題と見なす
int id(int y1){int y2=y1; return y2;} int main(void) { tainted int x1; int z1, x2; untainted int z2; z1 = id(x1); // call site 1 z2 = id(x2); // call site 2 } 危 から 安 に c1r1 | c2r2 で 行ける？ x1 y1 y2 z1 z2 x2 危 安 r1 r2 c1 c2

6 CFL Reachability を解く典型手法: “Set Constraint” 問題に帰着
CYK構文解析 + Warshall-Floyd 到達可能性 多項式時間だけど実用には厳しい重さ ヒューリスティックス Solver のある 問題に帰着  “Set Constraint” 問題

7 “Set Constraint” 問題 cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one cons
こんな連立方程式を解く問題。 集合Xの要素とYの要素をconsしたら Y に入る nil というアトムは集合 Y に入る 集合 Y の cons の形の要素の第一要素はone cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one cons

8 既存のやり方の流れ r1 r2 c1 c2 解く cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one cons
int id(int y1){int y2=y1; return y2;} int main(void) { tainted int x1; int z1, x2; untainted int z2; z1 = id(x1); // call site 1 z2 = id(x2); // call site 2 } x1 y1 y2 z1 z2 x2 危 安 r1 r2 c1 c2 cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one cons 解析の問題を CFL Reachability に CFLReachability を Set Constraint に 解く

9  まだ遅い 問題点 r1 r2 c1 c2 cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one
z1 z2 x2 危 安 r1 r2 c1 c2 cons(X, Y) ⊆ Y nil ⊆ Y 1(Y) ⊆ one cons CFL Reachability を Set Constraint に [Melski&Reps 97]  まだ遅い

10 観察 c1 r1 r2 c2 危 一般の CFLReach を解きたいわけじゃない
x1 y1 y2 z1 z2 x2 危 安 r1 r2 c1 c2 一般の CFLReach を解きたいわけじゃない プログラム解析から現れるような CFLReach が解ければよい “Call-Ret の対応が取れてる” を表す文法の CFLReach が解ければ十分では？

11 この論文のやったこと: “DyckCFL” に特化した帰着法
k-DyckCFL S ::= P* P ::= (1 S )1 | (2 S )2 | … | (k S )k 「対応のとれた括弧の列」

12 tbw

13 結果 漸近計算量 O( |文法|3 |グラフ|3 )  O( |文法| |グラフ|3 )