bixie

Javaの一貫性のないコード検出

マスターのステータス

Develのステータス

オンラインデモを確認してください。

Bixieは、Java Bytecodeの矛盾を検出する静的分析ツールです。コードが例外をスローする必要がある場合、または他のステートメントによって行われた仮定のために到達不可能である場合、矛盾が発生します。

例

 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 bytecodeの条件付き選択として表示されるため、bytecodeに矛盾があり、 identityDistribution.next() % 1一定の値を返すため、1つのケースが到達できません。

指示を作成します

BixieはGradleを使用してビルドを使用します。

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

使用例

すべてが機能しているかどうかを確認するには、それ自体でビクシーを実行します。

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

ビクシーランナー

便利なために、使用するクラスパスとクラスファイルが生成される場所を自動的に決定し、Bixieを呼び出すPythonスクリプト（Runner/Runner.py）があります。 Ant、Maven、またはGradleで構築されたプロジェクトで機能します。例えば：

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

このコマンドは、プロジェクトのMavenビルドプロセスを実行し、Javacが呼び出された場合に出力をスクレイして、その情報をBixieに送ります。ツールは、観察中に実際にコンパイルされたファイルのみを検出できるため、構築する前に掃除してください。

健全性の発言

ビクシーは健全ではありません。並行性や反射などの多くのJava機能は、Bixieによって処理されず、誤ったアラームをもたらす可能性があります。また、Bixieは、ソースコードに対応する矛盾がないバイトコードの矛盾を検出することがあります。たとえば、条件の接続詞を備えた条件付き選択は、誤報を引き起こすことがあります。