View on GitHub

Find inconsistencies in Java code

Download the .zip file

What is Inconsistent Code?

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

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 observations 1 and 2 may be interesting, we cannot prove them without knowing the possible values of a. Hence, reporting these issues may be a false alarm. 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 normally 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 4 must violate the assertion in line 6 without that knowledge.

Download and Usage

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

Get the Jar file

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

Download the latest release from GitHub.
-or-
Build from source: 

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

bixie.jar will be created in build/libs/.

Run Bixie on your code

  wget http://sri-csl.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.

Alternately, use our Bixie runner script, which can automatically detect the [class dir] and [classpath] of projects built with ant, maven, or gradle. From the directory of the project you want to check: 

  mvn clean
  python [path-to-bixie]/runner/runner.py -- mvn compile

The runner script optionally supports command line arguments for the location of the Bixie jar file (only needed if you have moved it from the default location in build/libs) and a directory to output results. Run python runner.py without any arguments for help.

Inconsistent Code found by Bixie

We run 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: