Sireum/Kiasan的初步使用

Sireum/Kiasan是一个类似于JPF的软件检测工具，可以进行基于合同的自动检测和测试用例的生成。

Sireum/Kiasan for Java is a JML contract-based automatic verification and test case generation tool-set for Java program units. In contrast to regular unit testing methods, Kiasan does not need input parameters for checking units. Without assertions or contracts (e.g., pre-/post-conditions), Kiasan, by default, detects possible uncaught runtime exceptions such as NullPointerException, ArithmeticException, ArrayIndexOutOfBoundsException, etc. With assertions embedded in the code, Kiasan automatically determines whether the assertions are possibly violated. When Java Modeling Language (JML) contracts (e.g., object/class invariants, method pre/postconditions) are supplied, Kiasan can leverage the contracts to ﬁlter out input parameters (i.e., pre-states) that do not satisfy the contracts while ensuring the states after execution (i.e., post-states) satisfy the contracts. In contrast to other bug ﬁnding tools, Kiasan generates a low number of false alarms due to its formal semantic-based analysis engine, and it has a stronger and quantiﬁable coverage on the unit behavior that it analyzes. Furthermore, Kiasan generates helpful analysis feedback by visualizing program states (e.g., object heap graphs) and JUnit test cases useful for illustrating property violations (e.g., assertion failures) as well as for code understanding or inspection (e.g., by visualizing code effects on program states).

最近，对其进行了初步的使用，感觉配置起来比JPF要麻烦些，不过它存在很多选项，比如可以指定循环展开的次数等，可以说它执行的是BMC（Bounded Model Checking），这一点跟CBMC类似，只不过是针对不同的语言罢了。

下面讲述一下它的配置过程。

本人是在Linux上配置的，在windows下尝试了很久，没能成功，感兴趣的可以自己试试。

Linux下安装配置步骤：

1）下载Sireum http://www.sireum.org/node/10

2）Sireum依赖Yices，而Yices依赖GMP，把这些都下载下来

Yices ：http://yices.csl.sri.com/

　　GMP ：http://gmplib.org/

3）安装GMP

　　解压下载下来的GMP包，我用的是5.0.4，然后控制台输入

　　./configure

　　make

　　make check

　　sudo make install (安装到/usr/lib下，其实就是在/usr/lib下加上编译好的GMP动态库)

4）安装Yices

　　Linux下要下载动态链接版本，之后将lib下的.so文件拷贝到/usr/lib下就OK了

5）安装Sireum

　　1.设置环境变量LD_LIBRARY_PATH（我是在/etc/enviroment下设的，/etc/profile下也可），追加

　LD_LIBRARY_PATH="~/workspace/tools/Sireum/kiasanlib/lib:~/workspace/tools/Sireum/kiasan/lib:$LD_LIBRARY_PATH"

　　2.将kiasanlib/lib下的文件拷贝到kiasan/lib下，就搞定了。

小小测试了一下

zztian@ubuntu:~/workspace/tools/Sireum/kiasan$ java -jar lib/Kiasan.jar -cp examples/bin/:ContainerTest/classes/ -sp examples/src/ --outdir ContainerTest/classes/ -cd ContainerTest/src/ --reportdir ContainerTest/report/ kiasan.examples.Container
Executing kiasan.examples.Container.<init> ...

Generating report ...
Done!

Executing kiasan.examples.Container.swap ...

Uncaught exception: java.lang.NullPointerException
at kiasan.examples.Container.swap(Container.java:8)