A static analysis tool for Automated (Expected) Amortised Complexity Analysis.
Contains source code of the function definitions to be analyzed
(*.ml files in subdirectories). This is a Git submodule.
Contains tactics for guided proof.
Contains grammars of the input languages for reference.
Start by executing
atlas --help
This will show a list of (global) options and commands. Take note of the option
--search. It defines where atlas will look for input files. For example
atlas --search=src/test/resources/examples [COMMAND]
The search path can also be set through the environment variable ATLAS_SEARCH.
The log level can be adjusted with --log, which takes (one of) the following
values: trace, debug, info, warn, error, off. The default log level and the
default log level file name are defined in atlas.properties.
The most important command is "run". To show help, execute
atlas run --help
The atlas run command, can be used to check types and their annotations
present in the source code, or, if enabled via --infer, disregard type
annotations in the source and infer types.
To speed up solving, tactics can be passed via --tactics.
Behaviour of the tool can be controlled by setting Java properties.
Z3 specific configuration can be set via com.microsoft.z3.*,
for example com.microsoft.z3.memory_max_size=25769803776 or
com.microsoft.z3.unsat_core=true (see also atlas.properties).
Logging-specific configuration can be set via org.slf4j.simpleLogger.*.
Tool-specific configuration can be set via xyz.leutgeb.lorenz.atlas.*.
Configuration file that can be used to change Z3 parameters and logging settings. By setting the log level to "debug" or "trace", much more detailled output can be obtained.
Some of the above properties are exposed as command-line arugments.
atlas is built using Gradle. Pre- and postprocessing is implemented in
Java, and the Z3 Theorem Prover is used for solving.
atlas can be built for multiple target environments:
- JAR file. Requires a JVM and Z3 shared libraries on the target system.
- ELF x86_64 binary (from the JAR via GraalVM Native Image). Requires a loader, some (very common) shared libraries, and Z3 shared libraries.
- Docker Image (based on ELF x86_64 binary).
- Open Virtual Appliance (OVA; based on ELF x86_64 binary, and NixOS).
x86_64 is the only architecture supported. Linux is the only operating system supported.
The build process is fully automated with Nix as a flake; Nix will run Gradle and build Z3 on demand. See also "How Nix works".
However, Nix is not strictly necessary: Without Nix, Gradle can still directly handle download and installation of all dependencies except the shared libraries for the Z3 Theorem Prover. Thus, the only manual steps required are building Z3 and making sure that the resulting shared libraries can be loaded.
The following two sections describe how to build atlas (1.) with Nix, and
(2.) without Nix.
This section assumes that Nix is installed and functional, and that the experimental feature "Flakes" is enabled.
To get an overview of the derivations/packaes that are available run following command. Their names roughly match the "target environments" listed in the previous section.
$ nix flake show
For additional information on derivations/packages, please
read metadata and comments in flake.nix.
Then, to build, for example:
# Build the default package (atlas x86_64 ELF binary, and related files)
$ nix build .#defaultPackage.x86_64-linux
# Build an OVA
$ nix build --print-build-logs .#packages.x86_64-linux.atlas-ova
After completion, the result of the build will be available as ./result.
Note that ./result may be a directory, or a file of arbitrary type, depending
on which environment was targeted. This is a Nix default.
Install GraalVM. In your build environment java -version
should mention "GraalVM", and the environment variable JAVA_HOME must point at
your GraalVM installation.
For development, GraalVM Community JDK 17.0.1+12-jvmci-21.3-b05, was used Any GraalVM version with a major version of 21 and a Java major version of 17 is expected to work.
Make sure that the Git submodule at
src/test/resources/examples is initialized and updated
(see The Git Book "Git Tools - Submodules").
For interfacing with Z3, three files are required: The JAR file
com.microsoft.z3.jar and libz3java.so work to bridge between the
Java Virtual Machine and Z3's C API, and libz3.so is the actual solver
implementation.
It is not straightforward to integrate all three files in the Gradle build
definition. Only com.microsoft.z3.jar is automatically downloaded and handled
by the Gradle build.
The two shared object files need to be obtained separately manually. There are at least two options to achieve this, summarized in the following two sections.
Refer to the Z3 README.md and its section on Java
as well as the Z3 example using Java.
Follow instructions to build libz3java.so and libz3.so.
Note that some Linux distributions allow for convenient installation of the
required libraries. For example, Ubuntu package libz3-jni
contains libz3java.so and in turn depends on package libz3-4,
which contains libz3.so.
The Java Virtual Machine or the ELF loader must find above *.so files for
linking. If there are linking issues, copy libz3.so and libz3java.so to
a path listed in $LD_LIBRARY_PATH or ./lib.
atlas is developed and tested to interface with Z3 v4.8.12, released on
2021-07-13. It is not the newest release, but the one packaged with Ubuntu LTS.