Kex

Kex is a platform for analysis of Java bytecode.

Dependencies

• z3 v4.8.12 with java bindings

  you need to manually install jar package with java bindings to your local maven repository using following command:

  mvn install:install-file -Dfile=/usr/lib/com.microsoft.z3.jar -DgroupId=com.microsoft 
  -DartifactId=z3 -Dversion=4.8.6 -Dpackaging=jar
  

• boolector-java v3.2.5

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

Kotlin refinement types inference

Run inference for jar file with

python refinements.py --jar <path to jar file>

Results are stored as a log file in a results directory at the same path as analyzed jar file.

Usage

Usage: kex
     --config <arg>                  configuration file
 -cp,--classpath <arg[:arg]>        classpath for analysis, jar files and
                                    directories separated by `:`
 -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

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