MACKE is a wrapper around KLEE, that decomposes the analyzed programs into several smaller units, analyze these seperately and finally merge all found errors to one interactive report. Please read the MACKE-paper for more details.
- Python 3.4+
- A system able to run LLVM. See official requirements for LLVM
Building KLEE can be a complicated task and there are multiple strategies for it. We suggest the setup described in our Step-by-Step manual. But whatever way you choose, MACKE needs a special search mode, that is not part of the official KLEE code, yet. We aim to merge it into KLEE someday, but till then, you need to use our fork of KLEE and checkout its targeted_search branch.
For our step-by-step manual, this means, that you have to adapt one command. Instead of:
git clone --depth 1 --branch v1.2.0 https://github.com/klee/klee.git
in Step 6, you must use:
git clone --depth 1 --branch targeted_search https://github.com/hutoTUM/klee.git
MACKE performs several modifications on LLVM bitcode level. Doing this inside python requires a lot more effort, than directly writing the operations in C++ - especially if you are forced to use the same, old version of LLVM as KLEE uses. Therefore, we decide to seperate all low level operations into another repository.
If you choose a different directory structure than suggested in our Step-by-Step manual, please adapt the pathes to match your needs.
git clone --depth 1 https://github.com/hutoTUM/macke-opt-llvm.git
cd macke-opt-llvm
make LLVM_SRC_PATH=~/build/llvm/ KLEE_BUILDDIR=~/build/klee/Release+Asserts KLEE_INCLUDES=~/build/klee/include/
# and if you want to run some tests before executing
make integrationtest LLVM_SRC_PATH=~/build/llvm/ KLEE_BUILDDIR=~/build/klee/Release+Asserts KLEE_INCLUDES=~/build/klee/include/
We are done with the dependencies - now to the main project.
git clone --depth 1 https://github.com/hutoTUM/macke.git
cd macke
make dev
Before you can actually start using MACKE, you have to modify the ./config.ini with your favorite text editor. Please adapt the pathes there to the directories, you have created earlier in this guide. Afterwards you can run:
source .venv/bin/activate # Note: just needed once per open shell
macke 2beAnalyzed.bc
We wish you happy testing! If you have problems converting existing source code bases to bitcode files, you should have a look at this tool for improving make.
Email me if something is broken. Ditto if you would like to contribute!