実際に使われている800行規模のCプログラムに対してCBMCを使ってみる。
ここでは拙作mcbというmemcachedのベンチマークプログラムを俎上にのせる。
このプログラムのバージョン1.0rc2はここで指摘されているように、初歩的なミスを含んでいる稚拙なものであった*1。
CBMC対応したmcb.c
現時点での最新バージョンは1.0rc5で、CBMCで検査しやすいように構造化を進め多くの事前条件を組み込んでいる。
また、CBMCとは直接関係ないassertも多数組込み、入力値の厳密な検査も行うようにした。
検査
ここでは、バグ報告があった部分に対応する1.0rc5の関数:send_cmd()について述べる。
以下は1.0rc5のsend_cmd()である。
最初に中身を把握するために必要最小限のコードだけ示す。次にCBMCに関連するところだけ抜粋し、CBMCを使うに当たっての注意点など記する。
では、最初は事前条件も事後条件もないバージョン。
static void send_cmd(const int fd, const int id, char *data, char *buff) { int key, msg_len, str_len; int _rand = rand(); double r; r = (double) (_rand / (RAND_MAX + 1.0)); key = 1 + (int) ((double) (sysval.max_key * r)); str_len = 1 + (int) ((double) ((sysval.data_len * 2) * r)); data[str_len] = '\0'; msg_len = build_mc_cmd(buff, buff_size, sysval.command, key, data, /*strlen(data) = */ str_len, id); /* marking */ data[str_len] = 'X'; do_cmd(fd, buff, msg_len, id); }
次に、CBMCで検査するために事前条件(+ダミーの変数)、事後条件を入れたバージョンを示す。
static void send_cmd(const int fd, const int id, char *data, char *buff) { int key, msg_len, str_len; int _rand = rand(); double r; /* * rについて検査する。 */ #ifdef __CBMC__ __CPROVER_assume(0 <= _rand && _rand <= RAND_MAX); /* assumption no.1 */ #endif r = (double) (_rand / (RAND_MAX + 1.0)); assert(0.0 <= r && r < 1.0); /* assertion no.1 */ /* * 次にkeyの設定値について検査する。 * あとでまとめて上部で定義すればよい。 */ #ifdef __CBMC__ /* * MAX_KEYはデフォルト値は65535と巨大なので、検査に莫大な時間がかかる。 * 検査に影響がない範囲で小さな値にする。 */ #undef MAX_KEY #define MAX_KEY 100 /* ダミーの値を設定 */ sysval.max_key = 10; // dummy : 構造体sysval_t sysvalを定義してもよいが、検索範囲を狭めるには必要な変数のみダミー値を設定するほうがよい。 /* sysval.max_keyの範囲を事前条件として記述する */ __CPROVER_assume(0 < sysval.max_key && sysval.max_key <= MAX_KEY); /* assumption no.2 */ #endif key = 1 + (int) ((double) (sysval.max_key * r)); assert(0 < key && key <= sysval.max_key); /* assertion no.2 */ /* * 次にstr_lenの検査 * こちらもあとで上にまとめればよい。 */ #ifdef __CBMC__ /* 上と同様、事前条件+(ダミーの)変数設定を記述する */ sysval.data_len = 10; // dummy __CPROVER_assume(0 < sysval.data_len && sysval.data_len <= MAX_DATA_LEN); /* assumption no.3 */ data_size = DATA_SIZE; #endif str_len = 1 + (int) ((double) ((sysval.data_len * 2) * r)); assert(0 < str_len && str_len < data_size); /* assertion no.3 */ /* 今回のメインパート。 * 旧バージョンではメモリアクセスに問題が発生した箇所。 */ #ifdef __CBMC__ char *data = (char *) malloc((DATA_SIZE)); #endif /* * --pointer-check,--bounds-checkで不正なアクセスの有無を検査 */ data[str_len] = '\0'; /* build_mc_cmd()内で検査する */ msg_len = build_mc_cmd(buff, buff_size, sysval.command, key, data, /*strlen(data) = */ str_len, id); #ifndef __CBMC__ assert(msg_len <= buff_size); #endif /* marking */ data[str_len] = 'X'; /* do_cmd()内で検査する */ do_cmd(fd, buff, msg_len, id); }
関数内のコメントで書いたように、内部を小分けにして事前条件+(ダミーの)変数設定をマメに入れるのがうまく検査するコツのようである。すべてうまくいったらまとめればよい。
実際にCBMCで検査する。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 .... 114934 variables, 248853 clauses SAT checker: negated claim is UNSATISFIABLE, i.e., holds Runtime decision procedure: 3.227s VERIFICATION SUCCESSFUL
CBMCを信じれば「mcb.cの1.0rc5にはメモリ関連のバグはない(ｷﾘｯ」。
CBMCの結果が正しいか疑ってみる
念のため、条件を変えて問題を検出するかどうか調べてみる*2。
最初にassertion no.2の範囲を変えて、間違った範囲を指定する。
/* * わざとエラーを出す */ static void send_cmd(const int fd, const int id, char *data, char *buff) { 略 ... key = 1 + (int) ((double) (sysval.max_key * r)); assert(1 < key && key <= sysval.max_key); /* assertion no.2' */ ... 略 ... }
これでCBMCを実行すると、範囲がおかしい旨報告される。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 ... Violated property: file mcb.c line 494 function send_cmd assertion 1 < key && key <= sysval.max_key FALSE VERIFICATION FAILED
また、今回のメインである配列dataの不正アクセスの可能性について、本当に検査できているのか確認してみる。
ここでは、わざと配列dataの大きさを1byteだけ小さくし、それによって不正アクセスをCBMCが検出するかどうかをみてみる。
static void send_cmd(const int fd, const int id, char *data, char *buff) { ... 略 ... #ifdef __CBMC__ char *data = (char *) malloc((DATA_SIZE) - 1); /* わざと1byte小さく確保 */ #endif data[str_len] = '\0'; ... 略 ... }
これでCBMCを実行すると、きちんと不正アクセスの可能性有りと報告してくれる。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 ... Violated property: file mcb.c line 513 function send_cmd dereference failure: dynamic object upper bound !((unsigned int)(POINTER_OFFSET(data)) + (unsigned int)str_len >= __CPROVER_alloc_size[POINTER_OBJECT(data)]) || !(IS_DYNAMIC_OBJECT(data)) VERIFICATION FAILED
これなら、CBMCの結果を信じてもよさそうだ。
その他の関数の検査
実際のところ、mcb.cについてCBMCで検査できる関数はsend_cmd()、master_thread()、connector_thread()など数個に留まった。これはCBMCの問題ではもちろんなく、mcb.cが簡単な処理しか行っていないため、そもそも検査項目が限られているためである。
しかし、検査をするための準備過程でtypoの修正やassertの挿入、入力範囲の厳密チェックなど、間接的にソースの品質向上に役立ったことも多いので、単に利用率だけをみてツールの有効性云々をいうことは出来ないと感じた。
その他
mcbの検証
念のため、Intel Inspectorでもチェックを行い、こちらもパスした。valgrindで動的検査も行い、こちらもパスした。
Inspectorほど簡単ではないが、CBMCでもInspector並の検証ができることを確認できた。
なお、入力値の検査はできていない。これは入力テストを網羅的に行うツールが別途必要。
並行処理
今回はマルチスレッドとはいえ、各スレッドは独立して動作するので(共有資源がない)うまくいった。
CBMCは並行処理には対応していないので、並行処理を行うプログラムの検証には注意が必要。
応用
CBMCが(boundは規定したうえで)すべての実行可能なパスを検査することを利用して、ある箇所への到達可能性を検査したり、絶対に通過してはいけない場所にあえてassert(false)文を挿入して危険性を検出するなど、様々な使い方があるようだ。
また、"Automatic Test Generation for Coverage Analysis Using CBMC"という論文では、CBMCを使ってテストパターンを生成するなんてこともされている模様*3。
*1:sourceforgeの記事の著者様から、記事掲載前にバグ情報を提供して頂いたことをここに記しておく。
*2:本当なら、条件でなく演算式をいじるべきだが、面倒なので。
*3:読むには有料(結構高い)なので読んでない
