"CBMC"というモデル検査ツールの使い方を学ぶ。
組込み分野では有名なツール。すでに開発終了したという人もいる*1が、最新版3.9は2010.12.19リリース。2010年には3.6,3.7,3.8,3.9と4バージョンリリースなので、アクティビティが落ちているようにはみえない。
配列の検査:1
故意に範囲を逸脱して値を代入するプログラムを書く。
cat test1.c #define SIZE 5 int main(int argc, char **argv) { int i; int a[SIZE]; for (i = 0; i <= SIZE; i++) /* 故意に範囲を間違えてみる */ a[i] = i; return 0; }
このソースtest1.cをcbmcに読ませ、静的解析を行う。
$ ./cbmc test1.c --bounds-check --pointer-check file test1.c: Parsing Converting Type-checking test1 .... 略 .... State 29 file test1.c line 11 function main thread 0 ---------------------------------------------------- test1::main::1::a={ 0, 1, 2, 3, 4 } State 30 file test1.c line 10 function main thread 0 ---------------------------------------------------- test1::main::1::i=5 (00000000000000000000000000000101) Violated property: file test1.c line 11 function main array `a' upper bound i < 5 VERIFICATION FAILED
という具合に、不具合をきちんと見つけてくれる(VERIFICATION FAILED)。
配列の検査:2
次にmallocを使って動的にメモリ領域を確保する場合の検査。
ここでもcbmcは静的検証を行う。
#include <stdlib.h> #define SIZE 5 int main(int argc, char **argv) { int i; int *a = (int *)malloc(sizeof(int) * SIZE); for (i = 0; i <= SIZE; i++) /* 故意に範囲を間違えてみる */ a[i] = i; return 0; }
同様に検査。
$ ./cbmc test2.c --bounds-check --pointer-check file test2.c: Parsing Converting Type-checking test2 ... 略 ... State 39 file test2.c line 13 function main thread 0 ---------------------------------------------------- symex_dynamic::dynamic_1_array={ 0, 1, 2, 3, 4 } State 40 file test2.c line 12 function main thread 0 ---------------------------------------------------- test2::main::1::i=5 (00000000000000000000000000000101) Violated property: file test2.c line 13 function main dereference failure: dynamic object upper bound !(4 * (unsigned int)i + (unsigned int)(POINTER_OFFSET(a)) >= 4 * __CPROVER_alloc_size[POINTER_OBJECT(a)]) || !(IS_DYNAMIC_OBJECT(a)) VERIFICATION FAILED
関数毎の検査
検査は関数毎に実行できる。よって巨大なソースファイルであっても、部分的な検査を繰り返すことが可能。
#include <stdlib.h> #define SIZE 5 void foo () { int i; char *a = (char *)malloc(sizeof(char) * SIZE); for (i = 0; i <= SIZE; i++) /* 故意に範囲を間違えてみる */ a[i] = i; } int main(int argc, char **argv) { foo(); return 0; }
関数の指定は"--function"オプションで。
$ ./cbmc test3.c --bounds-check --pointer-check --function foo file test3.c: Parsing Converting Type-checking test3 ... 略 ... State 34 file test3.c line 13 function foo thread 0 ---------------------------------------------------- symex_dynamic::dynamic_1_array={ 0, 1, 2, 3, 4 } State 35 file test3.c line 12 function foo thread 0 ---------------------------------------------------- test3::foo::1::i=5 (00000000000000000000000000000101) Violated property: file test3.c line 13 function foo dereference failure: dynamic object upper bound !((unsigned int)(POINTER_OFFSET(a)) + (unsigned int)i >= __CPROVER_alloc_size[POINTER_OBJECT(a)]) ||\ !(IS_DYNAMIC_OBJECT(a)) VERIFICATION FAILED
事前条件
少し検証っぽく。
事前条件assumeと事後条件assertを書いて、途中の動作をCBMCに検証させる。
CBMCの事前条件は"__CPROVER_assume()"で記述する。
cat test4.c /* * 事前条件 */ #include <stdlib.h> void goo(int a) { int i; int ret = 0; #ifdef __CBMC__ __CPROVER_assume(a < 10); __CPROVER_assume(ret == 0); #endif for (i = 0; i < a; i++) ret++; assert(a < ret); /* この条件は成立しない */ } int main(int argc, char **argv) { goo(10); return 0; }
検証結果は以下のとおり：
$ ./cbmc test4.c -D __CBMC__ --bounds-check --pointer-check --function goo --unwind 10 file test4.c: Parsing Converting Type-checking test4 ... 略 ... State 8 file test4.c line 15 function goo thread 0 ---------------------------------------------------- test4::goo::1::i=0 (00000000000000000000000000000000) Violated property: file test4.c line 19 function goo assertion a < ret VERIFICATION FAILED
cbmcは"-D"でマクロも設定できるので、検証のときだけ事前条件文__CPROVER_assumeを使うこともできる。
ちなみに、goo()@test4.cのassert文、成立するのは"assert(a <= ret)"である。筆者はコーディング時にミスが非常に多いので、こういったツールは有効に使いたいものである。
