シンボリック実行入門メモ

参考文献

モチベーション

もともとプログラムを静的に解析してバグなどを検出するのが好きテスト自動生成について調べているとシンボリック実行がよく出てくるし、最近はFacebookがprepackというツールを作っていたが、仕組みがよく分からなかった

Symbolic exectuion and program testing

シンボリック実行はテストを書くのと証明2つの間くらいの立ち位置の方法

テストを書く
- そのテストが十分にプログラムの正しさを表しているか分からん
プログラムを証明
- プログラムの性質を形式的に表してないといけないし、プログラムを書き換える時は、形式的な性質と証明も書き換えないとで大変

テストのように、プログラムにいくつかの具体的な入力のもとで実行結果と期待するOutputとを比較するのではなく、シンボリック実行では任意の値をとりうる "シンボル" を入力としてプログラムを擬似的に実行する。何を言っているのかわからねーと思うが、俺も何を言ってるのか分からなかった…

2. シンボリック実行

本節では "ideal" なシンボリック実行について説明する、"ideal" だというのには以下の理由がある

プログラムはintegerのみを扱うものとする。integerは任意の大きさを持ち、オバーフローすることはないとする
後述するシンボリック実行結果の execution tree は多くのプログラムに対して無限
The symbolic execution of IF statements requires theorem proving which, even for modest programming languages, is mechanically impossible.(?)

簡単のため単純なプログラミング言語を考える

signed int のみ
assign statement と IF THEN ELSE GOTO LABEL
signed int での演算は + - * のみ
IF の条件節における boolean expr は signed int >= 0 のみに制限

ここでプログラムをシンボリック実行するというのは

グローバル変数
プロシージャの引数
外部から読み込む変数

などに対して a_1 a_2 ... といった シンボル (具体的な値ではなく) 変数に与える変数を与える

state of program
- values of program variables
- counter of statement (何個のstmtが実行されたか)
- pc (path condition)
  - boolean expression over input symbols (a_1 ... a_n)
  - ex) { a_1 >= 0 && a_1 + 2 * a_2 >= 0 && !(a_2 >= 0) }
  - 先程定義した単純なプログラムでは各boolean expr は x >= 0 というものにしかならない

このようにpath conditionとは入力として与えた値があるpathへ到達するために満たすべき性質シンボリック実行ではまずpc=trueと初期化

IF文に到達した時

q ⊂ pc ならTHEN節にのみnonforking
q !⊂ pc ならELSE節にのみnonforking
両方偽なら両方にfork

forkしたそれぞれの制御では並列かつindependent THEN節の中ではIFの条件部qがtrueであるべきなので、THEN節にforkした側では pc <- pc ∧ q というassignが実行される同様にELSEでは pc <- pc ∧ !q

3.example

1 POWER: PROCEDURE(x, y);
2      res <- 1;
3      count <- 1;
4 LAB: IF y > count THEN
5      DO; res <- res * x;
6          res <- count + 1;
7          GO TO LAB; END;
8      RETURN (res);
9 END;

このcaseではシンボリック実行は無限に続く

4 execuion tree

symbolic execution tree は以下のような興味深い性質をもつ、この声質はFig7で確認できる

各終端ノードでは(completed exection path) does exist paticular input (non symbolic)
各終端ノードにおけるpcはdistinct

FIG7

TWOLOOPS: PROCEDURE (N);
            DO J = 1 TO N;
              (body of statements) END;
            DO K = 1 TO N;
              (body of statements) END; END;

5. Commutativity

instantiating symbolic results symbolic execution tree の各リーフノードのsymbol に具体的な値j_iを代入し、またpcにも代入する
results: 終端ノードにおいて代入結果のpcが真である値

6. EFFIGY

Tracing: statement numberを指定してある入力に対する計算結果を取得できる
Breakpoint: ユーザは各stmt間にブレークポイントを設置して、実行時にはここでストップ、その時の変数や条件などを取得できるい
State saving:

いろいろ指定可能

CALL SUM(1, 2, 5): すべて具体値
CALL SUM('A', 'B', 'C'): symbolとしてA B Cを指定
CALL SUM('A', 3, 5): combination

多くのプログラぬではシンボリック実行は停止しなかったりする EFFIGYではユーザがインタラクティブにどちらのpathに進むか選択できる

7 further example

SEARCH は Array[singed int] から signed int X を二部探索するプロシージャ探索範囲は L と U により決定することができる (Lower bound と Upper bound)

もし X が見つかった場合は、そのインデックスが J に格納され、 FOUND は 1
見つからなかった場合は、

SEARCH :
  PROC(A, L, U, X, FOUND, J);
    DCL A(*) INTEGER;
    DCL (L, U, X, FOUND, J) INTEGER;
    FOUND = 0;
    DO WHILE (L <= U & FOUND=0);
      J = (L+U)/2;
      IF X = A(J) THEN FOUND = 1
      ELSE IF X < A(J)
        THEN U = J -1
        ELSE L = J + 1;
    END;
    IF FOUND = 0 THEN J = L - 1
END

1-base A(1) ~ A(5)

(DCLってなんやねん)

例その1

例えば CALL SEARCH(A, 1, 5, "X", FOUND, J)

J=3 となり
IF X = A(3) となるので、ユーザーは go true か go false を使ってforkする
もしユーザが go true とした場合は、pc = 'X' = A(3) となる

シンボリック実行をやっていくと、最終的に11このterminal nodeを取得することができる

EFFIGY ではそれらのtermional nodeを以下のようにして取得することができる TEST(200) SEARCH(A, L, U, X, FOUND, J)

200というのは symbolic execution tree をたどる(stmt)の数のlimit 今回の例では symbolic execution tree は小さく有限なのでlimitはいらないかな

例その2

CALL SEARCH(A, "N", "N" + 4, "X", FOUND, J)

これは先程のテストをgeneralizeしたものo これも対して難しく、このテストからわかることは、Nの値は別に対してpropertyに対して影響を与えない

例その3

CALL SEARCH(A, "N", "N", "X", FOUND, J)

これのleaf nodeは3つだけ、いえーい簡単

generalな例

CALL SEARCH (A, 1, "N", "X", FOUND, J)
CALL SEARCH (A, "U', "U", "X", FOUND, J)

これは大変やで... 両方のシンボリック実行はinfinite

limitしてやるといくつかのleaf nodeが得られるしかしこのシンボリック実行ではAもまたシンボルで具体的な値(配列の長さも含めて)は得られないので、SEARCHの範囲外アクセスはcoverできない

こんな感じでinputの条件に対するoutputの対応が得られる

もちろんシンボリック実行がいつでも最高というわけではなくて、必要最低限なテスト(具体的な入力値と出力値の対応)がわかっているならシンボリック実行など必要ないのであった

8 Program correctness

プログラムがcorrect(これはテクニカルな意味ではなく英語的な意味)であることを確かめるためにはinputとoutputの述語が想定したものと同じである

ASSUME(B) はそのpath conditionにおいてBを評価し、pc <= pc && value(B)
PROOF(B): pc implies value(B) が true か false かを返す

DART

CUTE: A Concolic Unit Testing Engine for C

1.Introduction

ユニットテストでは、エンジニアが各Unitに対してinputと期待するoutputを定める

input と output をエンジニアが決めていくのは手間
どういうテストを書けば条件網羅したテストケースとなるのか難しい

このような課題に対する幾つかの手法が研究されており、

起こりうる入力をランダムに選択
- 同じ動作をする入力を複数してしまい、無駄なテストをたくさんしてしまうかも
- テストのカバレッジはランダムだしな...
無駄なテストの生成を少なくして、カバレッジをあげるための手法としてSymbolicExectuion
- すべてのPathに到達するための入力条件をつくる、これをSMTソルバとかにかけて入力値の条件を自動生成
- 複雑なコントロールフローを持つUnitなどはSymbolic実行が止まらなかったり...
- statementの数に制限をかけたり、interactiveに実行を制御したり工夫はされてる
Concreate input と symbolic input を組み合わせたシンボリック実行手法があるどん
- これによってシンボリック実行で通過するPathを制限できる
先の手法ではシンボリック実行のinputとして一部concreteな値で置き換えていたがGodefloidの手法では

tanishiking/symbolic_execution.md