CBMCの使い方入門:2

検証

次回に向けて、はやくも落ち穂拾い。

double

intだけでなくdoubleでも使えるか、確認。

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

int main (int argc, char **argv) {
  int _rand = rand();
  double r;

#ifdef __CBMC__
  __CPROVER_assume(0 <= _rand && _rand <= RAND_MAX);
#endif
  r = (double)(_rand / (RAND_MAX + 1.0));

  assert(0.0 < r && r < 1.0);   /* わざと範囲を間違えてみる */

  return 0;
}

このソースをcbmcにかけると、問題を指摘してくれる。

./cbmc test.c  -D __CBMC__  --bounds-check --pointer-check

... 略 ...

Violated property:
  file test-a.c line 15 function main
  assertion 0.0 < r && r < 1.0
  FALSE

VERIFICATION FAILED

念のため、正しい範囲で再度cbmcにかけると、問題ないと知らせてくれる。

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

int main (int argc, char **argv) {
  int _rand = rand();
  double r;

#ifdef __CBMC__
  __CPROVER_assume(0 <= _rand && _rand <= RAND_MAX);
#endif

  r = (double)(_rand / (RAND_MAX + 1.0));
  assert(0.0 <= r && r < 1.0);   /* 正しい範囲を設定 */            

  return 0;
}

./cbmc test.c  -D __CBMC__  --bounds-check --pointer-check

... 略 ...

9473 variables, 37501 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.414s
VERIFICATION SUCCESSFUL

関数検査の小技

別関数で確保したメモリ領域の扱いは小技を使う。例えば、以下のように、main()で確保したメモリ領域bufを関数foo()の引数で渡す場合、普通にcbmcにかけるとうまくいかない。

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

void foo(char *buf) {
  int i;
  for (i = 0; i < 10; i++)
    buf[i] = 'c';
}

int main (int argc, char **argv) {
  char *buf = malloc(10);
  foo(buf);
  return 0;
}

./cbmc test.c  --bounds-check --pointer-check --function foo

... 略 ...

Violated property:
  file test-b.c line 8 function foo
  dereference failure: dynamic object lower bound
  !(POINTER_OFFSET(buf) + i < 0) || !(IS_DYNAMIC_OBJECT(buf))

VERIFICATION FAILED

こんなときは、cbmcだけがわかるようにダミーのmalloc()を関数foo()内部で宣言する。

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

void foo(char *buf) {
  int i;
#ifdef __CBMC__
  char *buf = malloc(10);
#endif
  for (i = 0; i < 10; i++)
    buf[i] = 'c';
}

int main (int argc, char **argv) {
  char *buf = malloc(10);
  foo(buf);
  return 0;
}

こうすれば、cbmcで検査できる。

./cbmc test.c  -D __CBMC__  --bounds-check --pointer-check --function foo

... 略 ...

SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.038s
VERIFICATION SUCCESSFUL

これに限らず、ダミーの変数を適度に差し込むのは常套手段のようである。

unwind オプション*1

forやwhileのあるプログラムをcbmcにかけるときは、unwindに十分な回数(forやwhileで実際にまわる回数より多め)を設定しなければならない。

私はうまく説明できないので、詳しいことはこちらのドキュメントを参照されたし。



CBMCの使い方入門1
CBMCの使い方入門3

*1:"--show-vcc"オプションを設定すると、推論式のようなものを出力する。なんとなくわかりそうだが、詳しい出力の読み方はまだ身についていないので今回は説明パス。