View on GitHub

Find inconsistencies in Java code

Download the .zip file

What is Inconsistent Code?

Inconsistent Code is a form of code smell. It is code that has no normal terminating execution. That is, it is either not reachable, or any execution reaching it is doomed to fail. Inconsistent Code is not necissarily a bug (it might be just unreachable), but it raises the question why this code has been written if it cannot be executed without a crash. Let's look at the example below:

Try Bixie Online

What can we say about this code?

  1. The assertion in line 6 may be violated.
  2. Line 4 may be unreachable.
  3. The assertion in line 6 must be violated if line 4 is executed.
  4. Line 4 is inconsistent with line 6.
While the observations 1 and 2 may be interesting, we cannot prove them without knowing the possible values of a. Hence, reporting these issues may result in a false alarm. The observations 3 and 4, however, can be verified without any additional information.

Bixie proves that any execution containing line 4 must fail. That is, Bixie uses formal methods to verify that this procedure has no terminating execution containing line 4. Note that Bixe does not check if a can be 0 or not, but we can prove that any execution passing line 3 must violate the assertion in line 5.

Download and Usage

If you just want to play with Bixie use our Web Interface.

Before you start, check your Java version. You need at least JDK 7

Get the Jar file

Download the latest release from GitHub.

	wget https://github.com/martinschaef/bixie/releases/download/1.3/ATVA15.zip
	unzip ATVA15.zip
	cd ATVA15/

-or-
Build from source:
	git clone https://github.com/martinschaef/bixie.git
	./gradlew jar
	cd build/libs/

Run Bixie on your code

	wget http://martinschaef.github.io/bixie/Demo.java
	mkdir classes
	javac Demo.java -d classes/
	java -Xms2g -Xss4m -jar bixie.jar -j classes/

To run Bixie on your own project use

java -jar bixie.jar -j [class dir] -cp [classpath] -o [output] 

Where [class dir] is the root directory of your class files (usually 'classes'), [classpath] is the classpath that was used to generate the class files, and [output] is the ouput file where Bixie puts its report.

To rerun the experiments from our papers on various open-source projects, look at the python scripts on GitHub or in the release archive. Note that this may take hours or even days.

Inconsistent Code found by Bixie

We keep running Bixie on open-source projects and report our findings. In order to avoid spamming developers, we inspect each warning manually to make sure that it is relevant. Here are some instances of inconsistent code that were found and fixed by Bixie in popular projects:

During the development of Bixie we also found a case where the Java compiler generates unreachable bytecode (see here).

Papers

The papers below describe how the actual checking for inconsistent code is implemented in Bixie: