Inconsistent code detection for Java.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
config
gradle/wrapper
lib
runner
src
.gitignore
.travis.yml
LICENSE
README.md
build.gradle
gradlew
gradlew.bat
pre-commit.sh

README.md

Bixie Inconsistent Code Detection for Java

Status of Master

Build Status Coverage Status

Status of Devel

Build Status Coverage Status

Check our the Online Demo.

Bixie is a static analysis tool that detects inconsistencies in Java bytecode. An inconsistency occurs when code must throw an exception or is unreachable because because of assumptions made by other statements.

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

In this example from Hive, operator.getName() is inconsistent with the conditional operator == null.

In this example from Cassandra:

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

There is an inconsistency in the bytecode because the expression identityDistribution.next() % 1 == 0 appears as a conditional choice in the bytecode, and one case is unreachable because identityDistribution.next() % 1 returns a constant value.

Build instructions

Bixie uses gradle to build:

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

Usage example

To check if everything is working, run Bixie on itself:

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

Bixie runner

For your convenience, there is a Python script (runner/runner.py) that will automatically determine what classpaths to use and where class files are generated, and then invoke Bixie. It works for projects built with ant, maven, or gradle. For example:

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

This command will execute the maven build process for the project and scrape its output for instances where javac was called, then feed that information to Bixie. Be sure to clean before building, as the tool can only detect files that were actually compiled while it is observing.

Soundness remarks

Bixie is not sound. Many Java features, such as concurrency and reflection, are not handled by Bixie and may result in false alarms. Bixie also sometimes detects inconsistencies in the bytecode that have no corresponding inconsistency in the source code. For example, conditional choices with conjunctions in the condition sometimes raise false alarms.