*CPAcheckerに関するメモ [#j4f0fda2]
[[CPAchecker - A Software Verification Tool for Configurable Program Analysis:http://cpachecker.sosy-lab.org/]]
- [[BLAST:http://www.sosy-lab.org/%7Edbeyer/Blast/index-epfl.php]]の後継。
-- Cソースコードを検証対象とする。
-- CEGAR (counterexample-guided abstraction refinement) - 抽象化の粒度を自動調節する手法 ([[Clarke et al.; 2000:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.407]])。
-- cf. Beyer, D. et al., "[[The software model checker BLAST: Applications to software engineering:http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Checker_BLAST.pdf]]," International Journal on Software Tools for Technology Transfer, Vol.9, No.5, pp.505--525 (2007).
-いろいろな解析法（例えばshape analysis）を組み合わせて使うことができるプラットフォーム。
**検証サンプル [#example]
***例1：3数のうちの最大値 [#z0082a93]
-例プログラム: &ref(maxBug.c);
-- テスト実行したい場合は次のプログラムとリンクすればよい。
--- &ref(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:http://www.info.kochi-tech.ac.jp/y-takata/files/cpa/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：（うまく検証できない例） [#r50facf7]
-例プログラム
--(1) &ref(maxArray.c);
--(2) &ref(maxArrayFor.c);
--(3) &ref(maxArraySafe.c);
-例1と同じく，3数のうちの最大値を返すプログラム。ただし配列を使用している。
--3プログラムとも同じ動作であるので，検証結果も同じであるはずだが，predicateAnalysis オプションでCPAcheckerを実行すると，(1), (2) は UNSAFE，(3) は SAFE と出力される。
**インストールと実行 [#z983d597]
上記Webサイトの Download / Installation から。Mac OS Xの場合はUNIX用バイナリをダウンロードすればよい。
v1.3からJava 7が必須になった。Java 6しかない場合はv1.2以前をダウンロードすること。
***解凍・展開 [#e5256ce2]
$ tar xzf CPAchecker-1.3-unix.tar.bz2
$ cd CPAchecker-1.3-unix
***実行 [#j8ff4454]
$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol doc/examples/example.c
Mac OS XだとSMTソルバの [[MathSAT 5:http://mathsat.fbk.eu/]] を使えない((Linux用にはMathSAT 5 APIをJavaから呼び出すコードが付属しているが，Mac用はなく，かつSnow Leopardではソースから作ることもうまくいかなかった。))ので，[[SMTInterpol:http://ultimate.informatik.uni-freiburg.de/smtinterpol/]] を使うよう指定している（SMTInterpol自体は lib/java/ に同梱されている）。
コマンドラインで指定する代わりに，config/predicateAnalysis.properties の末尾に以下の行を追加しておくのでもよい。
cpa.predicate.solver=SMTInterpol
***解析オプション [#j5dba2a6]
predicateAnalysis が（たぶん）一番標準的な解析を行うオプション。-○○Analysis オプションを指定すると，config/○○Analysis.properties の設定に従った解析が行われる。
README.txt に最低限必要なことが書かれているので参照。
***解析レポートの生成 [#le0e6797]
output/* に出力された情報を HTML と画像に変換する。ただし，graphviz (dotコマンド) と Python 2.7 が必要((ともにMacPortsでインストール可能。Python 2.7はpython27というポート名。python2.7 というコマンド名でインストールされるので，その後 port select --set python python27 を実行すればよい。))。詳しくは doc/BuildReport.txt を参照。
$ python scripts/report-generator.py
$ open -a Firefox output/report.html
Safariでも見られるが，スライドバーによる拡大縮小ができない。
**検証対象サンプル集 [#vbc8cc08]
多くの検証対象サンプルを集めたものが公開されている。
***ダウンロード [#t466d257]
Subversionリポジトリからチェックアウトする。
$ svn co https://svn.sosy-lab.org/software/cpachecker/trunk/test
***実行 [#f58bee68]
scripts/benchmark.py はLinuxに強く依存しているので(([[cgroups>WikiPedia:cgroups]]が使われている))，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>&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((locks/*.c について。ファイル名中の数は規模（ロックの個数）。5から15個の資源に対して，非決定的にそのうちいくつかを選んでlockとunlockを繰り返す。lockしていないものをunlockするとエラー。非決定的な選択によりループを終了するが，無限に終了しない可能性も存在する。))。
nooutオプションは output/* への出力を抑制する。
