How to set up Alive2 on Ubuntu 20.04 LTS from scratch

This blog shares about how to set up Alive2 on Ubuntu 20.04 LTS from scratch. It took me several days to make it work properly T_T. Anyway, let’s start.

According to Alive2 Github page, Alive2 needs recent versions of:

• cmake
• gcc/clang
• re2c
• Z3
• LLVM

I’ll elaborate how to set these up one by one, but at first, given a newly installed Ubuntu, we need to install some necessary packages.

Necessary packages

1. git, for cloning repos from Github
2. Ninja, for building repos cloned
3. Python3 (I think Ubuntu contains installed Python3 by default)
4. python-is-python3. This package allows you call python3 with python

Thus all the commands you will need are:

1
2
3

sudo apt-get install git
sudo apt-get install ninja-build
sudo apt-get install python-is-python3

GCC

It’d be better to use gcc-10 for supporting some c++ 20 features. Thanks to this blog, How to Install GCC (build-essential) on Ubuntu 20.04, to configure gcc-10 on our Ubuntu, we need following commands:

1
2

sudo apt install g++-10
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-10 100 --slave /usr/bin/g++ g++ /usr/bin/g++-10 --slave /usr/bin/gcov gcov /usr/bin/gcov-10

After executing successfully, by checking g++ -v you would see gcc version is 10.2.0.

re2c

re2c is not hard to install. sudo apt-get install re2c is enough.

Z3

Github page of Z3 is pretty exhaustive. After cloning the repo, you should run following commands at repo folder.

1
2
3
4

python scripts/mk_make.py
cd build
make
sudo make install

One thing needs to notice is that if you want to remove z3 for some reason in the future, you might need CheckInstall for removing installed package. Thus, if you use CheckInstall to install, those commands should become:

1
2
3
4

python scripts/mk_make.py
cd build
make
sudo checkinstall

LLVM

After cloning LLVM repo, cd our working directory to the new generated repo (normally the folder name is llvm-project) and execute

1
2
3
4

mkdir build
cd build
cmake -GNinja -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON -DBUILD_SHARED_LIBS=ON -DCMAKE_BUILD_TYPE=Release -DLLVM_TARGETS_TO_BUILD=X86 -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_PROJECTS="llvm;clang" ../llvm
ninja

Commands above would build LLVM with ninja. Some problems would occur if you run ninja with sudo ninja. Finally, to install LLVM into system, you should run

1

ninja install

To test if LLVM works well, you should run

1

ninja check

Alive2

After cloning Alive2, cd working directory into the new generated repo (the name is alive2 by default) and run following commands

1
2
3
4

mkdir build
cd build
cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
ninja

Notice, the argument named -DCMAKE_PREFIX_PATH should be pointed the build folder we created in LLVM section.

If everything works well, by running

1

ninja check

we should pass all test. If so, congratulations! You alive2 is set and ready to go~ You could run commands such as

1

~/llvm/build/bin/llvm-lit -vv -Dopt=$HOME/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll

or

1

~/llvm/build/bin/llvm-lit -vv -Dopt=$HOME/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms

to see results. Finally, if you see some errors like ‘filecheck error: < stdin> is empty’ when you running Alive2 on /test/Transforms folder, don’t be panic. Some files contain bug that make Alive2 exit beforehand. Those files are reported at here. You could check them by clicking, for example. 1da2c7d25c09 on the page and redirect to files.