¥á¥ó¥Ð¡¼/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¿ô¤Î¤¦¤Á¤ÎºÇÂçÃ͆
- ²¼µ¤Î¥Æ¥¹¥È¥±¡¼¥¹¤ËÂФ·¤Æ¤Ï¤¤¤º¤ì¤âÀµ¤·¤¤Åú¤òÊÖ¤¹¡Ê°ì¸«Àµ¤·¤¤?¡Ë¡£
$ 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>&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 836·ï [¾ÜºÙ] maxArraySafe.c 815·ï [¾ÜºÙ] maxArrayFor.c 824·ï [¾ÜºÙ] maxArray.c 875·ï [¾ÜºÙ] maxBug.c 920·ï [¾ÜºÙ]