The set constraint/CFL reachability connection in practice - 昏論会ウィキ

The set constraint/CFL reachability connection in practice

背景

• なにか色々なプログラム解析は "CFL reachability" という問題に帰着できる
  • 変数が taint/untainted 外部入力を受けるかどうか解析、という例が載ってた
  • CFL = 文脈自由言語
• CFL reachability は、"set constraint" という問題に帰着できる
  • CFL reachability は多項式時間で解けるんだけど、かなり重いので専用のset constraint solverに飛ばした方が速い

内容

ところで CFL, CFL っていうけど、プログラム解析に使う文脈自由言語なんて種類限られてませんか？

「そう、DyckCFL という言語に限られているのだー！」

ということで DyckCFL に特化したset constraintへのエンコード方式を考えたよ速いよ、という論文。

※ DyckCFL : 要するに「対応の取れた括弧の列」のこと

(){[(){}]}

はDyckCFLに入るけど

))))

とかは入らない

やり方

の前に CFL reachability とは、

• 有向グラフ G
  • edge には文字が書いてある
• 頂点u, v
• 文脈自由文法 L

が与えられたら、uからvまでLにマッチする文字列になる順番でedgeをたどりながら行けますか判定して下さい、という問題。Warshall-Floyd法とCYK法を同時にやると合わせて O(|L|^3 |G|^3) でできる。しかしこれはちょっと重い。

これがどうプログラム解析に使われるかというと

int foo(int f1) { return ...; }

int bar(int b1, int b2) {
  int b3 = foo(b1);
  int b4 = foo(b2);
}

b1 ----[----> f1 ---ここにfooの中身---> retFoo ---]--->b3
              A                            |
b2 ----{------+                            +------}--->b4

みたいなグラフで

• b1 から b3 に情報は伝わる
• b2 から b4 に情報は伝わる
• b1 から b4 には行かない。b2 から b3 にも

といった情報を表現したくて、それは括弧のバランスが合った歩き方ができれば伝わる、みたいな定式化ができる。

これがないと、fooの呼び出し箇所全部inline化するなどしなくてはダメで、コストがヤバい。再帰があるともう全然ダメ。

あらためてやり方

set constraint というのは、大雑把にいうと

• 集合 U にタグ c をつけてwrapする
• 複数いっぺんにタプルにタグをつけることも
• タグ c が付いてたらそれを取る
• 同時にタプルから指定のi番目の要素を取ることも

という操作と、その包含関係 ⊆ からなる連立方程式で、それが解を持つ == CFL-reachable になるようにエンコードする。

普通の CFL の場合、A → B C という規則を

みたいにエンコードする。これの U はノードに対応していて、グラフのノード数分だけこの不等式を作らないといけない

ところが、元々 set constraint にはタグを「つける／外す」という括弧の対みたいな操作があるので、それを有効活用すれば A → { A } というDyckCFL規則は

• { の書いてあるu→vという辺はところは
• } の書いてあるu→vという辺はところは

というようにすると綺麗にタグの付け外しが消えられるところだけ括弧があってることになるので万事解決

注意事項

ところで論文も半ばにして

「やっぱり現実はあんまりDyckCFLばかりではなかった」ことが発覚。

要するにDyckCFLを使うということは、関数を呼んで戻るみたいな関係がマッチしてることを意味するんだけど

• 関数間のデータの受け渡しのような制御フローは「括弧の数」がマッチしないので表せない
  • → 「DyckCFLの部分文字列」にも使えるように頑張って対応
• グローバル変数みたいなものが挟まると好き勝手にいろんなものが挟まって大変
  • → なにか頑張って対応

と頑張る。