なんだこれは

はてなダイアリーから移転しました。

cbmc すごい。

日記

有界モデル検証(cbmc)というC C++のテスト方法があるらしいのだが、ほとんどが英語情報のためか、普及していない。
すくなくとも自分のみのまわりの開発者はつかっていない。

もったいない。
ちょっと使ってみて、こういう検証方法だと理解したことを書いておく。


cbmc は http://www.cprover.org/cbmc/ で開発されている、有界モデル検証ツールで、Windows, Linux, Mac OSXで使用できる。

ちょっとやってみながら考える

cbmcのチュートリアルにのっていた、file1.c に対して、

int puts(const char *s) { }

int main(int argc, char **argv) {
  int i;
  if(argc>=1)
    puts(argv[2]);
}

cbmc を実行してみよう。これは、配列境界チェックオプション(–bounds-check )と、ポインタチェックオプション(–pointer-checkfile)を有効にして、そのプロパティを表示(–show-properties)している。

cbmc file1.c --show-properties --bounds-check --pointer-checkfile

そうするとつぎのような出力がでた。

file1.c: Parsing
Converting
Type-checking file1
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Property main.1:
  file file1.c line 6 function main
  dereference failure: pointer NULL
  !(2l + argv == ((char **)NULL))
  in "argv[(signed long int)2]"

Property main.2:
  file file1.c line 6 function main
  dereference failure: pointer invalid
  !INVALID-POINTER(argv)
  in "argv[(signed long int)2]"

Property main.3:
  file file1.c line 6 function main
  dereference failure: deallocated dynamic object
  !(POINTER_OBJECT(argv) == POINTER_OBJECT(__CPROVER_deallocated))
  in "argv[(signed long int)2]"

Property main.4:
  file file1.c line 6 function main
  dereference failure: dead object
  !(POINTER_OBJECT(argv) == POINTER_OBJECT(__CPROVER_dead_object))
  in "argv[(signed long int)2]"

Property main.5:
  file file1.c line 6 function main
  dereference failure: dynamic object bounds
  !(16l + POINTER_OFFSET(argv) < 0) && __CPROVER_malloc_size >= 24ul + (unsigned long int)POINTER_OFFSET(argv) || !(POINTER_OBJECT(argv) == POINTER_OBJECT(__CPROVER_malloc_object))
  in "argv[(signed long int)2]"

Property main.6:
  file file1.c line 6 function main
  dereference failure: object bounds
  !(16l + POINTER_OFFSET(argv) < 0) && OBJECT_SIZE(argv) >= 24 + POINTER_OFFSET(argv) || DYNAMIC_OBJECT(argv)
  in "argv[(signed long int)2]"

これの、例えば プロパティ1は、pointer NULL という問題を検出することにして、それを条件文に変換していると考えられる。

  dereference failure: pointer NULL  #問題
  !(2l + argv == ((char **)NULL))    #問題を条件文へ翻訳したもの

つまりこの6個の組み合わせが解くべき問題ということになる。
この問題を解くために、シンボリック実行を行なう。シンボリック実行とは通常の実行とは異なり、変数に値をいれずに実行することだそうである。
とはいっても、先の出力に

file1.c: Parsing
Converting
Type-checking file1
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining

とあるようにfile1.c を等価な解析しやすいソースコードに変換してから実行しているはず。
そして条件分岐にくるたびにどちらのパスにはいるかで、ある程度値が絞られてくるんだと思う。

実際に解析を行なってみる。

cbmc file1.c --bounds-check --pointer-check

こういった出力が得られる。

file file1.c: Parsing
Converting
Type-checking file1
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 46 steps
simple slicing removed 8 assignments
Generated 6 VCC(s), 5 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
947 variables, 2715 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.016s
Building error trace

Counterexample:

State 3 file <built-in-additions> line 35 thread 0
----------------------------------------------------
  __CPROVER_memory_leak=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 4 file <built-in-additions> line 78 thread 0
----------------------------------------------------
  __CPROVER_pipe_count=0 (00000000000000000000000000000000)

State 5 file <built-in-additions> line 22 thread 0
----------------------------------------------------
  __CPROVER_threads_exited=__CPROVER_threads_exited#1 (?)

State 6 file <built-in-additions> line 23 thread 0
----------------------------------------------------
  __CPROVER_next_thread_id=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 7 file <built-in-additions> line 57 thread 0
----------------------------------------------------
  __CPROVER_rounding_mode=0 (00000000000000000000000000000000)

State 8 file <built-in-additions> line 30 thread 0
----------------------------------------------------
  __CPROVER_deallocated=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 9 file <built-in-additions> line 31 thread 0
----------------------------------------------------
  __CPROVER_dead_object=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 10 file <built-in-additions> line 32 thread 0
----------------------------------------------------
  __CPROVER_malloc_object=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 11 file <built-in-additions> line 33 thread 0
----------------------------------------------------
  __CPROVER_malloc_size=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 12 file <built-in-additions> line 34 thread 0
----------------------------------------------------
  __CPROVER_malloc_is_new_array=FALSE (0)

State 16  thread 0
----------------------------------------------------
  argv'[1]=irep("(\"nil\")")[1] (?)

State 19  thread 0
----------------------------------------------------
  argc=1 (00000000000000000000000000000001)

State 20  thread 0
----------------------------------------------------
  argv=argv' (0000001000000000000000000000000000000000000000000000000000000000)

State 21 file file1.c line 4 function main thread 0
----------------------------------------------------
  i=0 (00000000000000000000000000000000)

Violated property:
  file file1.c line 6 function main
  dereference failure: object bounds
  !(16l + POINTER_OFFSET(argv) < 0) && OBJECT_SIZE(argv) >= 24 + POINTER_OFFSET(argv) || DYNAMIC_OBJECT(argv)

VERIFICATION FAILED

どうやら、有界モデル検証が実行されている(Starting Bounded Model Checking)もよう。
この問題を解くのに、MiniSATを使用しているとのこと。
このチェッカーは充足可能性に異義を唱えたもよう(SAT checker: negated claim is SATISFIABLE)
その後、エラートレースを作成している、たぶん。

充足可能性問題、SAT、はてどこかで聞いた語だなと思ったら、数学ガールの乱択アルゴリズムにのっていた、はず。

数学ガール/乱択アルゴリズム (数学ガールシリーズ 4)

http://www.hyuki.com/girl/random.html で確認すると、9章 強く、正しく、美しくが該当しますね。はい、載っていました。

ということは、充足可能性問題のソルバーが MiniSAT 2.2.0 で、これを解いたということですね。
それで式全体が偽になるパターン：反例(counterexample)をエラートレースして示しているわけですか。なるほどー。