KLEEで記号実行してみた~チュートリアルその1(Testing a Small Function)~

TL;DR

筆者はシンボリック実行, KLEE, LLVMについては疎く, 誤った情報が含まれているかもしれない.
不十分な点や誤った情報が書かれていた場合は, コメント欄にてお知らせ頂きたい.

First tutorial: Testing a Small Function

公式がここから

前回の続きです.
環境構築が済んだので, 実際に動かしてみました.

Marking input as symbolic

kleeリポジトリ内の, examples/get_signのソース

#include<klee/klee.h>
int get_sign(int x) {
  if (x == 0)
    return 0;

  if (x < 0)
    return -1;
  else
    return 1;
}
int main() {
  int a;
  // シンボリック変数としてaを定義. 左からアドレス, サイズ, 名前を付与
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

Compiling to LLVM bitcode

examples/get_signディレクトリから下記を実行

$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c 

LLVMのbitcode形式のファイルget_sign.bcファイルが生成されました.

Running KLEE

それをkleeを使って実行する

$ klee get_sign.bc
KLEE: output directory is "/path/to/klee-out-0"
KLEE: Using STP solver backend

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

戻って貰うと分かりますが, get_sign関数は
aが0の時(if(x == 0)), 0未満の時(if(x < 0)), その他(else), と3つのパスに別れています.
KLEEは, それらの3つのパスを探索し, 探索した各パスに対して1つのテストケースを生成します.klee-out-Nという形で同ディレクトリに出力されるはずです.
またklee-lastはそのシンボリックリンクです.klee-lastの中身についてはこちら

.ktestファイルがテストケースです.3つあることが確認できますね.

$ ls klee-out-0/
assembly.ll   run.istats        test000002.ktest
info          run.stats         test000003.ktest
messages.txt  test000001.ktest  warnings.txt

KLEE-generated test cases

次にktest-toolを使って, .ktestファイルを調べてみましょう.

$ ktest-tool klee-last/test000001.ktest 
ktest file : 'klee-last/test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

$ ktest-tool klee-last/test000002.ktest 
ktest file : 'klee-last/test000002.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

$ ktest-tool klee-last/test000003.ktest 
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x01\x01\x01\x01'
object 0: hex : 0x01010101
object 0: int : 16843009
object 0: uint: 16843009
object 0: text: ....

結果を見てもらえれば分かりますが,
test000001はint : 0から, if(a == 0)の時を表しています.
他にもtest000002はint : -2147483648から, if(a < 0)を. test000003はint : 16843009からelse
を表しています.

こうして、具体値と共にそれぞれのパスを示してくれます.

Replaying a test case

KLEEでは, 実際にそれぞれのテストケースを入力した際の出力結果を表示できます.

msy@:tutorial$ export LD_LIBRARY_PATH=/path/to/klee/build/lib/:$LD_LIBRARY_PATH
$ gcc -I ../../include -L ../../build/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-out-1/test000001.ktest ./a.out 
$ echo $?
0
$ KTEST_FILE=klee-out-1/test000002.ktest ./a.out 
$ echo $?
255
$ KTEST_FILE=klee-out-1/test000003.ktest ./a.out 
$ echo $?
1

結果がそれぞれ0, -1(255へ変換), 1となり, 再現できた事が分かります.

最後に

今回は, 1つ目のチュートリアルを動かしてみました.
シンボリック実行は前々から興味があったのに動かした事がなかった為, やるやる詐欺になってました.

KLEEも万能ではなく, 苦手なケースや制約を課さないといけない場合もあるのですが, それはまた後日書くかも.

それではまた次の記事でお会いしましょう.