README.md

Kex

Kex is a platform for analysis of Java bytecode.

Build

Prerequisits

• JDK 8, 11 or 17 (other versions are not tested)
• OS: Linux, Windows or Mac
• Arch: amd64, x86_64, ARM (Mac only)

Build

• build jar with all the dependencies:

  mvn clean package
  

• build with specific SMT solver support:

  mvn clean package -Psolver
  

  where solver can be:

  • z3
  • boolector (supported only on linux)
  • ksmt — used by default
  • full-smt — build with z3, boolector and KSMT

Run all the tests:

mvn clean verify [-Psolver]

Usage

Usage: kex
    --config <arg>                  configuration file
 -cp,--classpath <arg[:arg]>        classpath for analysis, jar files and
                                    directories separated by `:`
    --depth <arg>                   depth with which to analyze the crash,
                                    required for the crash mode
 -h,--help                          print this help and quit
    --libraryTarget <arg>           package where to analyze library usages,
                                    required for the libchecker mode
 -m,--mode <arg>                    run mode: crash, symbolic, concolic,
                                    libchecker, defectchecker
    --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;
                                    required for symbolic, concolic and defect
                                    modes
    --trace <arg>                   path to a trace file with a crash, required
                                    for the crash mode

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:0.0.11 --classpath /home/myproject/target/myproject.jar \
 --target myproject.\* --output /home/kex-output --mode concolic

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 run Kex on it using following command:

python ./kex.py --classpath test.jar --target TestClass --output test --mode concolic

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() {
  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)
}