Documentation

Build

There are multiple ways to use KoAT. First, it can be built from source code. Second, a Docker image can be used to build KoAT. Finally, a statically linked binary can be constructed by using the Docker container. If you want to use our web interface, then see here.

Build directly from source code

1. Use opam init and follow the instructions to set up Opam and install OCaml 4.06.1 if necessary.
2. opam install -j$(nproc) . --deps-only
   • requires the gmp and mpfr libraries
3. Run dune build to build KoAT.
4. You may add export PATH=$PATH:"path-to-Koat2-repository/_build/install/default/bin/" (with the substituted path) into your .bashrc file to use koat2 directly.
5. In older KoAT2-releases before we integrated CFR for (probabilistic) programs, we used the tool iRankFinder for control-flow refinement. If you are using an older release, for control-flow refinement download iRankFinder and unzip it. Add export PATH=$PATH:"path-to-irankfinder-folder/irankfinder/" (with the substituted path) into your .bashrc file such that KoAT is able to find iRankFinder.

Build Docker image

1. Install Docker as described here.
2. Execute ./build_container.sh in the top directory of this repository. This builds a Docker image with the name koat2. The Docker image contains a static binary.

Static Binary

To get a statically linked binary, please execute the script compile_static_binary.sh. This will set up a Docker container in which OCaml 4.09.1 for compiling static binaries using musl is installed with all required packages to compile KoAT. Please note that in this case, the used libraries (see below) are linked statically into the resulting binary. The code of these libraries can be found when following the given links below.

Run ./koat2 in main to get the help page of koat2. For further information run ./koat2 commandname --help. The main command proceeding a full analysis is the analyse command.

Input Format

Concerning the input format, for integer programs we use the corresponding input format from the Termination and Complexity Competition as described here. Note that a disjunction is modeled by two parallel transitions with the same update, and negations are modeled by flipping every comparator (i.e., ¬(x<y) is equivalent to x≥y).

For C programs, we also use the corresponding input format from the Termination and Complexity Competition as described here. To analyze C programs, KoAT translates them into its format for integer programs using Clang and llvm2kittel.

Used Libraries

KoAT makes use of the following external tools and libraries.

• APRON
• Batteries
• Cmdliner
• FPath
• Ocamlgraph
• Ocamlnet for HTML proof output
• Parmap
• ppx_deriving
• ppx_deriving_cmdliner
• ppx_getenv
• Z3

External Tools

In its analysis, KoAT may use control-flow refinement via partial evaluation (see here for more details). To this end, it used the external tool iRankFinder in older releases before we integrated CFR for (probabilistic) programs. To use iRankFinder, please install it on your system. However, iRankFinder is already included in the older Docker images.

KoAT uses SymPy for many linear algebra calculations. If you want to use it, please install it on your system. SymPy is already included in the Docker image.

To generate an image of the graph of an integer program, KoAT invokes Graphviz, which has to be manually installed on the system. Note that when building the Docker image, the current Ubuntu binaries of Graphviz are installed. Thus, the resulting image already contains Graphviz.

Moreover, the Docker image also contains both Clang and llvm2kittel which are used to transform C programs into the input format of KoAT.

External Tools & Libraries (Website)

• GitHub
• Hydeout
• Jekyll
• Pygments

Contact

If you encounter any difficulties, either use GitHub issues or contact us via aprove [at] i2.informatik.rwth-aachen.de.