bixie

Java的代码检测不一致

主人的状态

Devel的状态

检查我们的在线演示。

Bixie是一种静态分析工具，可检测Java字节码中的不一致。当代码必须抛出异常或无法实现时，会发生不一致的情况，因为其他陈述的假设。

例子

 if (operator == null) {
 	throw new SemanticException("Operator " + operator.getName());
 }

在此示例中，hive operator.getName()与条件operator == null不一致。

在Cassandra的示例中：

 public Boolean generate() {
	return identityDistribution.next() % 1 == 0;
}

字节码存在不一致之处，因为identityDistribution.next() % 1 == 0在字节码中作为条件选择出现，并且一种情况是无法实现的，因为identityDistribution.next() % 1返回常数值。

建立说明

Bixie使用Gradle来构建：

 git clone https://github.com/SRI-CSL/bixie.git
cd bixie
./gradlew shadowJar

用法示例

要检查一切是否有效，请自己运行Bixie：

 cd build/libs/
java -jar bixie.jar -j ../classes/main/

Bixie Runner

为了方便起见，有一个Python脚本（Runner/Runner.py），它将自动确定要使用哪些类Path以及生成类文件的何处，然后调用Bixie。它适用于使用蚂蚁，小牛或gradle构建的项目。例如：

 cd <path-to-project>
mvn clean
python <path-to-bixie>/runner/runner.py -- mvn compile

该命令将执行项目的Maven构建过程，并为调用Javac的实例刮擦其输出，然后将该信息馈送给Bixie。确保在构建前清洁，因为该工具只能检测到观察时实际编译的文件。

健全的评论

Bixie不是听起来的。 Bixie并未处理许多Java功能，例如并发和反射，可能会导致错误警报。 Bixie有时还会检测到源代码中没有相应不一致的字节码中的不一致。例如，有条件选择的条件选择有时会引起虚假警报。