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:
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 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/
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]
[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:
- Apache Cassandra: see pull request
- Apache Hive: see pull request
- Apache jMeter: see pull request
- Apache Maven: see pull request
- Apache Tomcat: see pull request
- Bouncy Castle: see pull request
- Soot: see pull request 1 and 2 and 3
- WildFly: see pull request
- Apache Flume: see 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