To compare BASIL with LLVM verifiers like SeaHorn, we need a compiler that generates LLVM, such as clang. Unfortunately, most self-contained cross-compilation tools are GCC-based, so we must take it upon ourselves to provide clang with the standard libraries and headers it needs for aarch64 targets.
This repo includes a Dockerfile and associated build scripts to, on any host machine:
- Generate a docker container containing everything one needs to generate
.ll,.gts, and aarch64 binaries from a given c program. - Automate the generation of these files with a single command.
Usage:
# build the docker image
git clone [email protected]:UQ-PAC/clang-toolchain.git
cd clang-toolchain && docker build -t lifter .
# create the container, name it 'lifter', and mount the root directory of your source files as 'host', e.g.
docker create -it --name lifter -v /path/to/src/files/root:/host lifter
# for convenience, move lift.sh to your source files root or add it to your PATH
mv lift.sh /path/to/src/files/root
# you can now use lift.sh to compile and lift your c file
# the input file should have no file extension and should be relative to the path you mounted to the container (NOT the current path)
cd /path/to/src/files/root
sh lift.sh tests/simple # converts tests/simple.c to tests/simple.ll, tests/simple.gts, and tests/simple