A Docker image containing KoAT2 can be downloaded here.
We also included iRankFinder to perform CFR in Docker images from older releases.
However, we have replaced it by our native, probabilistic version of CFR in our newest release.
The image can be loaded into Docker (provided Docker is installed, see here for installation instructions) by changing to the directory where you stored koat2_docker.tar.xz and executing:
docker load --input=koat2_docker.tar.xz
Examples can be added by mounting a directory.
Assume that the directory /home/user/examples contains an example named myExample.koat.
Then
docker run --rm -v '/home/user/examples:/koat2/examples:ro' -t koat2:latest its analyse -i /koat2/examples/myExample.koat
first mounts the directory in the Docker container and then executes KoAT2 on myExample.koat. On Windows, if the example is in the directory C:\Users\user\examples, then replace /home/user/examples by /c/Users/user/examples.
The parameter its specificies that the input is the encoding of an integer program.
If instead you wish to analyze a C program example.c on integers, please run
docker run --rm -v '/home/user/examples:/koat2/examples:ro' -t koat2:latest c analyse -i /koat2/examples/myExample.c
Here, the translation from C to integer programs is achieved using the tools Clang and llvm2kittel which are both contained in the Docker image. Note that in this case the input has to be the last parameter.
If you want to save KoAT2’s output in a file, this can be achieved by
the usual command line instruction, e.g., docker run --rm -v '/home/user/examples:/koat2/examples:ro' -t koat2:latest its analyse -i /koat2/examples/myExample.koat > output.txt.
To specify methods for local runtime bound computations, use the flag --local with arguments twn or mprf, i.e., KoAT only uses MΦRFs if the flag --local mprf is used and both techniques if the flag --local mprf,twn is passed to KoAT, while a second flag --depth x limits the maximum depth of MΦRFs to x.
The flag --cfr pe activates control-flow refinement via partial evaluation (see here).
For example, to analyze example.c using both the twn-technique and MΦRFs of depth up to 5, as well as control-flow refinement (this corresponds to the configuration KoAT2 + TWN + MΦRF5 from this article), you should execute
docker run --rm -v '/home/user/examples:/koat2/examples:ro' -t koat2:latest c analyse --local mprf,twn --depth 5 --cfr pe -i /koat2/examples/myExample.c
If KoAT2 should analyze a probabilistic program with all improvements enabled, this can be achieved by
docker run --rm -v '/home/user/examples:/koat2/examples:ro' -t koat2:latest its prob-analyse -i /koat2/examples/myExample.koat --classic-local mprf,twn --depth 5 --closed-form-size-bounds --pe`
In particular, KoAT2 uses our native (probabilistic) CFR procedure (see here).
Furthermore, we enabled our new technique (see here) to infer classical size bounds using the flag --closed-form-size-bounds.