精確なガーベージコレクションのための局所変数登録誤りの発見

鵜川 始陽

藤本 太希

背景
• eJSVM: JavaScript仮想機械（VM）• C言語で記述されたVM• ガーベージコレクション（GC）の変遷
Boehm GC
(保守的)

精確な

コンパクション

マークスイープ
イマココ

背景• eJSVM: JavaScript仮想機械（VM）• C言語で記述されたVM• ガーベージコレクション（GC）の変遷
Boehm GC
(保守的)

精確なマークスイープのつもり• GCのバグ発覚

コンパクション

イマココ

この話の概要• eJSVMのデバッグ体験• GCのバグを探すのに Coccinelle というツールを使った• 制御フローグラフに対するパタンマッチが有効だった

GCルート集合• GCはポインタをたどって生きているオブジェクトを探す• 探索の起点がGCルート GCルート集合• 大域変数x• 局所変数y• C言語の変数

C言語の局所変数• スタック上に存在• GCはスタックの型が分からない• 変数が初期化済みかどうかも分からない

yxiintachar*

Cスタックヒープ

局所変数の探し方• 保守的GC• オブジェクトを移動できない• スタックマップx• 実装が大変• プログラマが明示

yi

int

achar*eJSVMの実装• 最初は手軽• コードの品質を保つのが大変

Cスタックヒープ

GC_PUSHとGC_POP• ヒープへのポインタを持つ変数のアドレスをGCスタックに積む

ret

ctx

get_obj_prop(C *ctx, JV o, JV p){
JV ret;if (!is_string(p)) {GC_PUSH(o); // gc_push(&o)
p = to_string(ctx, p);
GC_POP(o); // gc_pop()}// 引数はデバッグ用
do {
if (get_prop(o, p, &ret))
return ret;
} while (get__proto__(o, &o));return JS_UNDEFINED;op

GCスタックCスタック}

GC_PUSH挿入の条件• GCが起こる可能性がある• JV型の変数• GCまでに初期化されている• GC後にその値がget_obj_prop(C *ctx, JV o, JV p){
JV ret;if (!is_string(p)) {GC_PUSH(o); // gc_push(&o)
p = to_string(ctx, p);
GC_POP(o); // gc_pop()}// 引数はデバッグ用使われる

GC前にGC_PUSH

do {if (get_prop(o, p, &ret))
return ret;
} while (get__proto__(o, &o));return JS_UNDEFINED;}

GC_PUSH挿入の条件
コンテキスト（C型）の引数をとる• GCが起こる関数の中でしか起こらない可能性がある• JV型の変数• GCまでに初期化されている• GC後にその値がget_obj_prop(C *ctx, JV o, JV p){
JV ret;if (!is_string(p)) {GC_PUSH(o); // gc_push(&o)
p = to_string(ctx, p);
GC_POP(o); // gc_pop()}// 引数はデバッグ用

使われる

GC前にGC_PUSH

do {if (get_prop(o, p, &ret))
return ret;
} while (get__proto__(o, &o));return JS_UNDEFINED;}

堅実な挿入方法• 全てのJV型変数は宣言と同時に初期化• 全てのJV型変数をスコープに入ると同時にGC_PUSH••

get_obj_prop(C *ctx, JV o, JV p){
JV ret = NULL;
GC_PUSH3(o, p, ret);if (!is_string(p))
パフォーマンス悪い?
p = to_string(ctx, p);
この方法でもミスする do {if (get_prop(o, p, &ret))
return ret;
} while (get__proto__(o, &o));
GC_POP3(o, p, ret);
return JS_UNDEFINED;}

解きたい問題• GC_PUSHの挿入漏れを探す• 手動でGC_PUSHを挿入してあるプログラムが対象• GCが起こる可能性がある• JV型の変数• GCまでに初期化されている• GC後にその値が使われる

GC前にGC_PUSH

方針• テスト → 不完全，バグの特定が難しい• 静的解析
• 実行経路（パス）に関するパタンマッチ• Coccinelle• 構文的なパタンマッチ → 向かない
• ASTgrep, ASTMatcher, PMD, …
• 抽象実行，型，難しい解析，… → 使うコストが大きい？

なぜパスに関するパタン?
• GCが起こる• JV型の変数• GCまでに初期化されている• GC後にその値が使われる

GC前にGC_PUSH

JV a;…
a = args[i];…
while(k < len){if(has_array_elem(a,k)){kv = cint_to_fixnum(k);nv = cint_to_fixnum(n);e = get_array_prop(a,kv);
set_array_prop(ctx,b,nv,e);}n++; k++;}なぜパスに関するパタン?
• GCが起こる• JV型の変数• GCまでに初期化されている• GC後にその値が使われる

GC前にGC_PUSH

JV a;…
a = args[i];…
while(k < len){if(has_array_elem(a,k)){kv = cint_to_fixnum(k);nv = cint_to_fixnum(n);e = get_array_prop(a,kv);
set_array_prop(ctx,b,nv,e);}n++; k++;}目次• 背景と目的• Coccinelle• GC_PUSH漏れ発見のパタン作成• 評価とケーススタディ• 議論

Coccinelle[Muller, Lawall, et al. 2009]• プログラムのパタンマッチと編集を行うソフトウェア• Linuxカーネルのデバッグやソフトウェア進化に利用• バグの発見，ライブラリAPIの変更に伴うコードの修正• 現在でも開発が続いている [Kang et al. (ECOOP 2019)]
SmPL

Coccinelle
patch

セマンティックパッチ

編集対象に対するパッチファイル

C
編集対象ソースコード

端末出力

Coccinelleの利用例• Linux[Lawall et al. 2009, Palix et al. 2014]• OpenSSL [Lawall et al. 2010]• GCのバグ発見に利用した例はないセマンティックパッチ• patchコマンドに入力するdiﬀに似ている（開発者の見解）• 意味的なパタンマッチをする• 空白や括弧の有無などは無視• 構文要素や出現位置をメタ変数で抽象化• 「...」で途中を省略（省略部分の条件を指定可）• 同じ意味の構文を同一視例) x == NULL と NULL == x@@
expression E,E1;@@
if (E == NULL+
IS_ERR(E)) {<+... when != E = E1
PTR_ERR(E)...+> }A semantic patch correcting a casewhere a value is compared to NULL
and subsequently passed to PTR_ERR
http://coccinelle.lip6.fr/rules/ より

Coccinelleの内部制御フローグラフ（CFG）に対するパタンマッチ• セマンティックパッチをメタ変数付き計算木論理（CTL-V）式に変換してモデル検査 [Brunel et al. 2009]
Coccinelle

SmPL

CTL-V
モデル検査

セマンティックパッチ

エンジン

C
編集対象ソースコード

CFG

パッチ生成

ルールの組み合わせ• 複数のルールでパッチを構成できる• 後続のルールが先行ルールに依存する• マッチしたメタ変数を後続のルールで利用できる• 複数のルールに依存するルールも作れる• 先行ルールに「マッチしない」という条件も指定できる
R1

x = a, b×R2

y = u, v(x,y) = (a, u), (a, v),(b, u),(b, v)@R3 depends on R1 && R2@
R3

目次• 背景と目的• Coccinelle• GC_PUSH漏れ発見のパタン作成• 評価とケーススタディ• 議論

GC_PUSH漏れバグ
GC_PUSH挿入の条件• GCが置こる

バグの条件
1.GCが起こる• JV型の変数• GCまでに初期化

2.JV型の変数されている• GC後にその値が使われる

3.GCまでに初期化されている
4.GC後にその値が使われる
5.GC前にGC_PUSH

GC前にGC_PUSHがない

「GCまでに初期化されている」
は条件に含めない• GC後に初期化して使う場合• GCの時の値は使われない

1.GCが起こる

条件4にマッチしない

2.JV型の変数

条件3は不要

3.GCまでに初期化• GC後にも初期化せず使われる場合• GCに関係ないバグ

されている
4.GC後にその値がgccが検出使われる

条件3は不要

5.GC前にGC_PUSHがない

条件の詳細な記述
1.GCが起こる
2.JV型の変数
3.GCまでに初期化されている

forall GCが起こる位置 g
forall JV型の変数 v とその宣言位置 dforall 変数 v の参照位置 u
次を探す:
d4.GC後にその値が使われる経路が存在する
gv への代入がない

5.GC前にGC_PUSHがない

GC_PUSH(v)がない経路が存在するuセマンテックパッチの構成
forall GCが起こる位置 g
forall JV型の変数 v とその宣言位置 dforall 変数 v の参照位置 u
次を探す:
gc

decl

d

MissingPush

GC_PUSH(v)がない経路が存在する

usegv への代入がない経路が存在する

MissingPush

uuseuse と MissingPush@use depends on gc&&decl@ @MissingPush depends on use@
identifier decl.v;
identifier pre.push, decl.v;
expression e, gc.gc_fun; expression e, gc.gc_fun;
position gc.gc_p, use_p; position gc.gc_p,decl.decl_p;@@
type decl.T;
dgc_fun@gc_p@@
GC_PUSH(v)がない... when != v = e(when exists
T v@decl_p;
経路が存在するgv@use_p|
T v@decl_p = e;)g... when != GC_PUSH(v)v への代入がない
when exists
経路が存在する
gc_fun@gc_pu

偽陽性の除去• 最初のパッチでは偽陽性が多い••

g(ctx); // GC
v = …
if (…) {vへの代入がvの参照にマッチする
GC_PUSH(v);h(ctx); // GC
GC_POP(v);
GC_PUSH(v)がvの参照にマッチする }• GCを起こす関数の呼出しがある文の中でのvへの代入が考慮されていない

gv への代入がない• ルールを追加してフィルタする経路が存在するuフィルタ
gcdeclusefalseuseimmassMissingPush@falseuse …@(v@use_p = e|
GC_PUSH(v@use_p)|
GC_POP(v@use_p))@immass …@
v = <+... gc_fun@gc_p …+>@MissingPush depends on
use && !falseuse && !immass@

目次• 背景と目的• Coccinelle• GC_PUSH漏れ発見のパタン作成• 評価とケーススタディ
• 議論

評価
• eJSVMのソースコードを利用• ファイル数20 （発表資料にある unix.c は間違い）• 行数 9459 行（コメント，空白含む）• 手動で挿入していたGC_PUSHを取り除いてGC_PUSH漏れとして検出できるか調査

結果の分類手動
Coccinelle

検出漏れ

正しい

バグ検出 偽陽性※ 真の正解は誰にも分からない

結果
手動
Coccinelle

正しい• 検出漏れはなかった

バグ検出 偽陽性

結果
手動
Coccinelle

不要• 検出漏れはなかった• 不要なGC_PUSHがあった

正しい

バグ検出 偽陽性

結果
手動
Coccinelle

不要
6

正しい27

• 検出漏れはなかった• 不要なGC_PUSHがあった

バグ検出
64

偽陽性
1

• 偽陽性は1つだけ• eJSVMのコードの品質が悪い?

評価（２）• 他人のソースコードを利用• C言語によるAVL木の実装• 新しいGCの実験用コード• ファイル1個，368行• 全ての関数がGCを起こす可能性がある• コンテキストは大域変数

結果
手動
Coccinelle

不要
10

正しい
28

• 不要なGC_PUSHは存在した• バグも検出された

バグ検出 偽陽性70

目次• 背景と目的• Coccinelle• GC_PUSH漏れ発見のパタン作成• 評価とケーススタディ
• 議論

有効性
• CFG上のパタンマッチが有効だった• GC_PUSHを追加する条件の特徴• 関数内で閉じている（通常のリソース管理は閉じていない）• パスに関する条件• CFGを作るライブラリを使って専用ツール化の検討• Coccinelleを使うのに比べ改善される点が少ない• 問題ごとに設定が異なるので割に合わなさそう

限界: データに依存する場合• データに依存して分岐が制限される場合は偽陽性になる
if (low_exists)
low_val = get(ctx, low_index);gif (high_exists)
high_val = get(ctx, high_index);
if (low_exists && high_exists) {set(ctx, low_index, high_val);…

u限界: PUSHとPOPの対応• GC_PUSHとGC_POPが精確に対応しているかは検査できなかった• eJSVMではGC_POPの引数はデバッグ用なので間違っていても動く

GC_PUSH(a);GC_PUSH(b);f(ctx);
GC_POP(a);GC_POP(b);GC_PUSH自動挿入• 現在は自動化していない• どこにGC_PUSHするかは人間が判断• それなりの個所に挿入することはできるがそれが正しいかは確認が必要• 次の情報を提示することで十分実用的• 変数の宣言位置• GCが起こる可能性がある位置• 変数が参照される位置

まとめ• GCのためのソースコードの修正漏れを静的検査により探した• 検査にはCoccinelleを使った• 制御フローグラフに対するパタンマッチが有効だった• eJSプロジェクトで現在も使っている