Kex

Kex is a platform for analysis of Java bytecode.

Dependencies

• z3 v4.8.12 with java bindings
• boolector-java v3.2.6

Build

• build jar with all the dependencies:

  mvn clean package
  

• build with only one SMT solver support:

  mvn clean package -Psolver
  

  where solver stand for required solver name (boolector or z3)

Run all the tests:

mvn clean verify

Usage

Usage: kex
     --config <arg>                 configuration file
 -cp,--classpath <arg[:arg]>        classpath for analysis, jar files and
                                    directories separated by path separator
 -h,--help                          print this help and quit
 -m,--mode <arg>                    run mode: symbolic, concolic, libchecker
    --option <section:name:value>   set kex option through command line
    --output <arg>                  directory for all temporary output
 -t,--target <arg>                  target to analyze: package, class or method

Docker

If you want to try out Kex you can use these Docker images with the latest version installed. Example:

docker run -v ~/myproject:/home/myproject -v ~/kex-output:/home/kex-output \
 abdullin/kex-standalone:run --classpath /home/myproject/target/myproject.jar \
 --target myproject.\* --output /home/kex-output

Example

Consider an example class:

class TestClass {
    class Point(val x: Int, val y: Int)

    fun test(a: Array<Point>) {
        if (a.size == 2) {
            if (a[0].x == 10) {
                if (a[1].y == 11) {
                    error("a")
                }
            }
        }
    }
}

Compile that class into the jar file and tun Kex on it using following command:

./kex.sh --classpath test.jar --target TestClass --output test

Kex will produce directory test with all the results and logs. test/tests directory will contain tests generated by Kex:

fun <T> unknown(): T {
    TODO()
}

fun test(): Unit {
    val generatedTerm1197 = TestClass()
    val generatedTerm1198 = arrayOfNulls<Point>(2)
    val generatedTerm1503 = Test.Point(10, 0)
    generatedTerm1198[0] = generatedTerm1503
    val generatedTerm1279 = Test.Point(0, 11)
    generatedTerm1198[1] = generatedTerm1279
    generatedTerm1197.test(generatedTerm1198)
}