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有時還會檢測到源代碼中沒有相應不一致的字節碼中的不一致。例如，有條件選擇的條件選擇有時會引起虛假警報。