CPAchecker

Last-modified: 2014-02-27 (木) 15:06:04

Top/メンバー/y-takata/CPAchecker

CPAcheckerに関するメモ†

CPAchecker - A Software Verification Tool for Configurable Program Analysis

BLASTの後継。
- Cソースコードを検証対象とする。
- CEGAR (counterexample-guided abstraction refinement) - 抽象化の粒度を自動調節する手法 (Clarke et al.; 2000)。
- cf. Beyer, D. et al., "The software model checker BLAST: Applications to software engineering," International Journal on Software Tools for Technology Transfer, Vol.9, No.5, pp.505--525 (2007).
いろいろな解析法（例えばshape analysis）を組み合わせて使うことができるプラットフォーム。

↑

検証サンプル†

↑

例1：3数のうちの最大値†

例プログラム: maxBug.c
- テスト実行したい場合は次のプログラムとリンクすればよい。
  - getInt.c

下記のテストケースに対してはいずれも正しい答を返す（一見正しい?）。

$ gcc maxBug.c getInt.c
$ ./a.out
10 20 30
answer=30
$ ./a.out
10 30 20
answer=30
$ ./a.out
30 20 10
answer=30

CPAcheckerを使って検証するとUNSAFEと出力される。

$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol maxBug.c
...
Verification result: UNSAFE. Error path found by chosen configuration.
...

report-generator.py を使ってレポート (ErrorPath.0.html) を生成し，エラー経路を調べる。

$ python scripts/report-generator.py
$ open -a Firefox output/ErrorPath.0.html

この例に対する ErrorPath.0.html
- 一見ではわかりにくいが，(a > b), !(b > c), (x = c), !(x >= a) という経路によってエラー状態に到達することが示されている。
- つまり，これらの4つの論理式をすべて満たす a, b, c（a > c >= b である a, b, c）が存在し，それが入力されるとエラー状態に到達する。

25行目の b > c を a > c に修正してCPAcheckerに入力し直すと，SAFE と出力される。

↑

例2：（うまく検証できない例）†

例プログラム
- (1) maxArray.c
- (2) maxArrayFor.c
- (3) maxArraySafe.c
例1と同じく，3数のうちの最大値を返すプログラム。ただし配列を使用している。
- 3プログラムとも同じ動作であるので，検証結果も同じであるはずだが，predicateAnalysis オプションでCPAcheckerを実行すると，(1), (2) は UNSAFE，(3) は SAFE と出力される。

↑

インストールと実行†

上記Webサイトの Download / Installation から。Mac OS Xの場合はUNIX用バイナリをダウンロードすればよい。

v1.3からJava 7が必須になった。Java 6しかない場合はv1.2以前をダウンロードすること。

↑

解凍・展開†

$ tar xzf CPAchecker-1.3-unix.tar.bz2
$ cd CPAchecker-1.3-unix

↑

実行†

$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol doc/examples/example.c

Mac OS XだとSMTソルバの MathSAT 5 を使えない*1ので，SMTInterpol を使うよう指定している（SMTInterpol自体は lib/java/ に同梱されている）。

コマンドラインで指定する代わりに，config/predicateAnalysis.properties の末尾に以下の行を追加しておくのでもよい。

cpa.predicate.solver=SMTInterpol

↑

解析オプション†

predicateAnalysis が（たぶん）一番標準的な解析を行うオプション。-○○Analysis オプションを指定すると，config/○○Analysis.properties の設定に従った解析が行われる。

README.txt に最低限必要なことが書かれているので参照。

↑

解析レポートの生成†

output/* に出力された情報を HTML と画像に変換する。ただし，graphviz (dotコマンド) と Python 2.7 が必要*2。詳しくは doc/BuildReport.txt を参照。

$ python scripts/report-generator.py
$ open -a Firefox output/report.html

Safariでも見られるが，スライドバーによる拡大縮小ができない。

↑

検証対象サンプル集†

多くの検証対象サンプルを集めたものが公開されている。

↑

ダウンロード†

Subversionリポジトリからチェックアウトする。

$ svn co https://svn.sosy-lab.org/software/cpachecker/trunk/test

↑

実行†

scripts/benchmark.py はLinuxに強く依存しているので*3，Mac OS X で実行するのは困難。

SAFE / UNSAFE の結果が得たければ，例えば以下のようなスクリプトを実行する。

$ for i in test/programs/benchmarks/locks/*.c
  do
    echo -n `basename $i`'  ' 
    scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol -noout $i 2&gt;&1 |
    grep result | awk '{print $3}'
  done
test_locks_10_true-unreach-label.c  SAFE.
test_locks_11_true-unreach-label_false-termination.c  SAFE.
test_locks_12_true-unreach-label_false-termination.c  SAFE.
test_locks_13_true-unreach-label.c  SAFE.
test_locks_14_false-unreach-label.c  UNSAFE.
test_locks_14_true-unreach-label.c  SAFE.
test_locks_15_false-unreach-label.c  UNSAFE.
test_locks_15_true-unreach-label_false-termination.c  SAFE.
test_locks_5_true-unreach-label_false-termination.c  SAFE.
test_locks_6_true-unreach-label_false-termination.c  SAFE.
test_locks_7_true-unreach-label_false-termination.c  SAFE.
test_locks_8_true-unreach-label_false-termination.c  SAFE.
test_locks_9_true-unreach-label.c  SAFE.

この場合，ERRORラベルへの到達可能性を調べているので，ファイル名に true-unreach-label とあるものは SAFE，false-unreach-label とあるものは UNSAFE*4。

nooutオプションは output/* への出力を抑制する。

*1 Linux用にはMathSAT 5 APIをJavaから呼び出すコードが付属しているが，Mac用はなく，かつSnow Leopardではソースから作ることもうまくいかなかった。
*2 ともにMacPortsでインストール可能。Python 2.7はpython27というポート名。python2.7 というコマンド名でインストールされるので，その後 port select --set python python27 を実行すればよい。
*3 cgroupsが使われている
*4 locks/*.c について。ファイル名中の数は規模（ロックの個数）。5から15個の資源に対して，非決定的にそのうちいくつかを選んでlockとunlockを繰り返す。lockしていないものをunlockするとエラー。非決定的な選択によりループを終了するが，無限に終了しない可能性も存在する。

添付ファイル:

getInt.c 842件 [詳細]

maxArraySafe.c 820件 [詳細]

maxArrayFor.c 829件 [詳細]

maxArray.c 885件 [詳細]

maxBug.c 923件 [詳細]