ほとんど参加できなかったJaSST'13 Tokyoに絡んで、秋山浩一さんから「concolic testing」という言葉を聞きました。
@kz_suzuki @krsna_sub 私も聞き取れなかったのですが、たぶん、Concolic testing のような物の事だと思いました。
— akiyama924🎄 (@akiyama924) 2013年1月30日
用語どころか「concolic」という単語も初めて耳にしたものだったので、少しだけ調べてみることにしました。
例によって勝手な理解のメモですので、話半分で読んでください。
入力値を自動生成する技術
concolic testingは、プログラムに対する入力値を自動的に生成するための、ホワイトボックス的なテスト技法です。
参考文献[2]には、入力値を生成するテスト技法として以下が挙げられています。
- random testing
- symbolic execution
- concolic testing
- model based testing
- search based testing
4.のモデルベースドテストは、最近よく聞きますよね。厳密に定義されたモデルから網羅的にテストケースを生成できるというのは、とりあえずイメージはしやすい。ただし、現実のソフトウェア開発では、必ずしも厳密にモデルを定義しているわけではなく、適用が難しい場合が多いとのことです。
5.はSoftware Testing ManiaXの7巻の、辰巳敬三さんの「最近出てきたテスト技法」という記事で紹介されていますが、かなり難しい・・・。原典にあたらないとだめですね。
実は3.のconcolic testingも、辰巳さんの記事で言及があります。
「concolic」は、「symbolic」（記号）と「concrete」（記号に対して、具体値）と合成語。上の1と2を合わせた技法のようです。concreteは具体値なのでわかりますが、symbolic testingとはどのようなものなのでしょう。
symbolic testingのあらまし
symbolic testingは、プログラムに対する入力を、具体的な値（concrete value）ではなく任意の記号（symbol）としたまま、プログラムの制御フローパスを解析する技法です。ソースコードさえあれば適用可能な、ホワイトボックス的な技法。
symbolic testingが初めに提案されたのは、1976年のJames C.King氏の論文(pdf)のようです。歴史の長い技法ですが、アルゴリズムの改善やマシンパワーの劇的な向上により、実用性が再注目されている模様。
参考文献[1]にある事例を少し改変して、考えてみましょう。
int a = A, b = B, c = C;
// symbolic
int x = 0, y = 0, z = 0;
if (a) {
x = -2;
}
if (b < 5) {
if (!a && c) { y = 1; }
}
z = 2;
assert(x+y+z!=3)
引数a、b、cに対し、1行目で与えられているA、B、Cが、symbolです。具体値ではなく、記号。
具体値不定のまま行を進んでいくと、4行目でif文に突き当たります。この判定「if(a)」でtrueの方向に進むための制約（constraint）が、「A = true」です。
さらに進むと、次の判定「b < 5」をtrueにする制約「B < 5」が現れます。この先にも判定「!a && c」があるのですが、「A = true」のままなのでtrueにしようがない。
ということで、1つのパスを通る制約「path constraint」（path condition、PC）として、「A∧(B<5)」が得られました。この制約を満たすすべてのA・B（・C）が、true/trueを通ることになります。
すべてのパスを塗りつぶしたいわけですから、「b < 5」をfalseにするPCは「A∧(B≧5)」というように、条件を洗い出していきます。
このプログラムのPCは以下の5つになります。あとはこのA・B・Cに具体的な値を与えれば、すべてのパスを通る入力パターンができます。
- A∧(B<5)
- A∧(B≥5)
- ￢A∧(B<5)∧C
- ￢A∧(B<5)∧￢C
- ￢A∧(B≥5)
このような制約を機械的に解析するのが、constraint solverというものだそうです。
単純なプログラムだと、簡単そうに思えるのですが、パスの数の爆発の他、solverが解決できる制約にも制限があるようです。文献[2]で挙げられている弱点は、たとえば以下の制約。
- float型・double型の変数
- ポインタ
- 非線形の算術操作
- ビット演算
文献[3]には、線形の制約の例として「X > Y Λ Y+X ≤ 10」が。非線形の制約として「X * Y < 100」「X % 3 Λ Y > 10」などが挙げられていますが、スミマセン、定義はよくわかりません。足し算引き算と大小比較は線形？
そして、conclic testing
concolic testingは、random testingとsymbolic testingのハイブリッドですね。
文献[2]によると、concolic testingも、パスの探索方法はsymbolic testingと同様。
ただ、constraint solverが苦手とするような複雑な制約に突き当たった場合にそこで立ち止まらず、その先を具体値（concrete value）を代入して進めてみて、solverが解きやすい形になるようにする。つまり、symbolic testingの制約を緩くして、機械的に辿れる範囲を増やすることができるのが、concolic testingのメリットのようです。
途中までは任意の値を代表するsymbolで、理詰めで進めていくのですが、途中から具体値になるので、そこでバグを取りこぼす可能性がある。これがconcolic testingの弱点です。また理詰めで進めていく部分は、上で挙げたようなsolverの弱点もそのまま引き継いでいます。
擬人化
方程式 x3 - 3*x2 + 4 = 0 を解く学生の例でいうと、こういう3人がいます。
random testingさん
「理屈じゃねえんだよ！とにかく力技で、いろんな値で0にならんか試してみるぜー！」
→「100万パターンぐらい試してみたけど、全部解けたかよくわかんねえわ・・・」
symbolic testingさん
「ふっ、野蛮な・・・。解の公式を使ったり因数分解したりして、理詰めで漏れなく解を導出すればいいのですよ」
→「・・・5次方程式には一般的な解の公式がない・・・ですって・・・？」
concolic testingさん
「途中まで解析的に問いてみたけど進めなくなったから近似してみた」
→「近似したら解なしになったわ・・・」
全然違いますか。
参考文献
[1] Jeff Foster, "Symbolic Execution," 2011
[2] Xiao Qu, Brian Robinson, "A Case Study of Concolic Testing Tools and Theis Limitations"
[3] Saswat Anand, "Symbolic Execution," 2009
