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:
What can we say about this code?
- The assertion in line 6 may be violated.
- Line 4 may be unreachable.
- The assertion in line 6 must be violated if line 4 is executed.
- Line 4 is inconsistent with line 6.
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.
Build from source:
git clone https://github.com/SRI-CSL/bixie.git ./gradlew jar
bixie.jar will be created in
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]
[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
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:
- Apache Cassandra: pull request
- Apache Hive: pull request
- Apache jMeter: pull request
- Apache Maven: pull request
- Apache Tomcat: pull request
- Bouncy Castle: pull request
- Soot: pull requests 1, 2, and 3
- WildFly: pull request
- Apache Flume: pull request
The papers below describe how the actual checking for inconsistent code is implemented in Bixie:
- Severity Levels of Inconsistent Code, ATVA 2015
- Bixie: Finding and Understanding Inconsistent Code, ICSE 2015
- Conflict-Directed Graph Coverage, NFM 2015
- Explaining Inconsistent Code, FSE 2013
- A Theory for Control-Flow Graph Exploration, ATVA 2013
- Joogie: Infeasible Code Detection for Java, CAV 2012
- It's doomed; we can prove it, FM 2009