KLEE を試してみた。

シンボリック実行のツールとして公開されているKLEEを試してみました。

目次

dockerのインストール

KLEEの環境を構築するのはdockerのイメージを使うのが一番手軽に試せるようです。
dockerについてはこちらの記事を参考にインストールしてみました。
qiita.com

dockerイメージの実行

dockerのインストールが完了したらイメージを取得して実行します。

# イメージの取得

$ docker pull klee/klee

$ docker image ls

REPOSITORY          TAG                 IMAGE ID            CREATED             SIZE

klee/klee           latest              f0052ebadb00        7 months ago        1.31GB
# 実行

$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee
# dockerのコンテナを起動するとシェルが立ち上がります。

klee@684a74481856:~$ pwd                                                                                 

/home/klee

klee@684a74481856:~$ ls

klee_build  klee_src

チュートリアル

KLEEの最初のチュートリアルがこちらのサイトで解説されています。
klee.github.io

シンボリック実行を試すコードは以下のようなコードとして示されています。
引数で渡された数値の符号を判定する関数のようです。

/*
 * First KLEE tutorial: testing a small function
 */

#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;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
} 

チュートリアル自体は丁寧に解説が書かれていますのでここでは詳細は書きませんが、注意点として、上記のコンテナのシェル上では、 klee/klee.hは klee_src/include に展開されています。
従って get_sign.c を /home/klee 以下で配置した場合にビットコードにコンパイルするコマンドは

$ clang -I klee_src/include -emit-llvm -c -g get_sign.c

になります。

感想

dockerを普段使うことがないのでとまどいました(というかまだよくわかっていないのでもう少しdockerに対する勉強が必要そうです。
今回は以前に買って積本になっていたdocker教科書第2版が役に立ちました。

プログラマのためのDocker教科書 第2版 インフラの基礎知識&コードによる環境構築の自動化

KLEE本体がちゃちゃっとmakeして使えないのは不便な気もしますが、dockerで配布しているということはmacやwindowsでも使えるということですよね。KLEEをwindowsでも使えないか試してみたいと思います。

Dockerエキスパート養成読本［活用の基礎と実践ノウハウ満載！］ (Software Design plus)