論文紹介
Reading:“Giga-Scale Exhaustive Points-toAnalysis for Java in under a Minute”(from OOPSLA’15)
発表者: 稲葉 一浩
複雑ネットワーク・地図グラフ セミナー 2017/1/19

About the paper Presented in OOPSLA:ACM SIGPLAN (= SIG on Programming LANguages)
International Conference on Object-Oriented
Programming, Systems, Languages, and Applications

Points-to Analysis?
 コンピュータープログラムの解析の一つ
 高速化や安全性の検査などに用いられる (典型的には)ラベル付き有向グラフでの制約付きreachability問題に帰着する近似解法で解かれる

Points-to Analysis?
 プログラム中のある箇所で確保したメモリ領域を指す可能性のある変数はどれか？(aやbやresultは⇗を指すか？

void crosProduct(int[] a, int[] b, int[] result){
result[0] = a[1] * b[2] – b[2] * a[1];result[1] = a[2] * b[0] – b[0] * a[2];result[2] = a[0] * b[1] – b[1] * a[0];}int[] newZeroVector() {return new int[3];}巨大なコンピュータプログラム

Alias Analysis
 Points-to Analysisは “Alias Analysis” (二つの変数が同じメモリ領域を指す可能性があるか？) を含み、この解析の情報がよく使われる。

void crosProduct(int[] a, int[] b, int[] result){
result[0] = a[1] * b[2] – b[2] * a[1];result[1] = a[2] * b[0] – b[0] * a[2];result[2] = a[0] * b[1] – b[1] * a[0];}a や b と result が同じ領域を指すか指さないかで大違いAbout the paper Context-Free Points-to Analysis がIn:|V|=160万 |E|=200万
Out: 1.5G組のプログラムに対して 40秒 でできました帰着先:(All-Pairs) Context-Free Language Reachability
 入力 辺ラベル付き有向グラフ
 文脈自由文法(3× 出力 文法に従ったラベル列で到達可能な全点対

 O(|G|・|V|^3 / log|V|)

ExprTerm
Factor＋＋×)

 Known Algorithm

12::= Term | Expr ＋ Term::= Factor | Term × Factor::= 1 | 2 | 3 | ( Expr )Context-Free Points-to Analysis ⇒Context-Free Graph Reachability x = new Object; x = y; x = y.f;
 x.f = y;

xxx
x

alloc
assignload-fstore-fh1

yyy

where h_1 is aunique ID for thisprogram location正確には x = new Object; x = y;xxx

 x = y.f;
 x.f = y;

x

alloc
alloc

assignassignload-fload-fstore-fstore-fh1yyy

Example from the paper(To Java Experts)

x = h;（どちらも y may point-to h） y = x;

 プログラムの実行順序は無視y = x;x = h;

 関数の呼び出しも代入で表現（異なる場所(context)での関数使用は混ざる）
Obj f(Obj x, Obj y) {return y;}z = f(h1, h2);
u = f(h3, h4);x=h1; y=h2; z=y;x=h3; y=h4; u=y;

Grammar

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-f
T::= (assign | Bridge)*
PointsTo ::= T alloc

 x = new Object; x = y; x = y.f;

 x.f = y;

x

alloc

h1x

assignyx

load-fyx

store-fy(for all f)

Grammarx

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-f
T::= (assign | Bridge)*
PointsTo ::= T alloc
pointsToh1

変数 x が h1 で確保されたメモリを指すかもしれない(for all f)

Grammarx

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-fT::= (assign | Bridge)*
PointsTo ::= T alloc

pointsTopointsToy

変数 x と変数 y が同じメモリを指すかもしれない(for all f)

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-f
T::= (assign | Bridge)*
PointsTo ::= T alloc

Grammarzload-fAliasxystore-f(for all f)w

y.f = w;

変数 x と変数 y が同じメモリを指すかもz = x.f;⇒ 要はz=w;と同じ効果

Grammarx

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-f
T::= (assign | Bridge)*
PointsTo ::= T alloc(assign | Bridge)*

yalloc(for all f)

hx=x1; x1=x2; …; xn=y; y=new Object;
変数 x がメモリ h を指すかもhアルゴリズム

Alias::= PointsTo PointsTo
Bridge ::= load-f Alias store-f
T::= (assign | Bridge)*
PointsTo ::= T alloc

Bridge の overapproximaton (後述)
T は 推移閉包(ラベルなしのreachbility)を効率的に管理するデータ構造 [21]現在の T からBridgeかどうか判定

Bridge の over approximation
 CFL Reachability の制限されたケース“Bidirected Dyck CFL Reachability” で近似
 O(|E| log |E|)

 k-Dyck CFL とは、k 種類の括弧対 (2k種類の文字)上の「括弧の対応がとれてる」を意味する文法
 S ::= ε | SS |（S） | 【S】 | ｛S｝| 「S」

 Bidirected: (a,【,b)∈E

iff (b,】,a)∈E assign連結成分を潰し、load-f と store-f を括弧対と考える

実験結果

既存手法2
既存手法1

Datalog
商用ソルバ

提案手法

Bridgeの近似の精度