环境

Ubuntu：Ubuntu 20.04.1

GCC：9.4.0

Linux version：Linux version 5.13

Clang：clang version 10.0.1

LLVM：llvm 10.0.1

Z3：4.8.18

CMake：cmake version 3.16.3

安装前置

sudo apt upgrade
sudo apt install -y git cmake ninja-build clang build-essential python2 python3-pip && sudo pip3 install lit
# sudo apt install -y git cargo cmake g++ ninja-build python2 python3-pip zlib1g-dev && sudo pip3 install lit

如果出现E: Unable to locate package这样的错误，用sudo apt-get update更新安装源就行

安装Z3

下载：git clone https://github.com/Z3Prover/z3.git

进入z3文件夹，进行安装（参考z3/README-CMake.md at master · Z3Prover/z3 (github.com)中的ninja部分）：

mkdir build && cd build
CC=clang CXX=clang++ cmake -G "Ninja" -DCMAKE_BUILD_TYPE=Debug ../
sudo ninja install

安装LLVM

参考（可直接看后续安装步骤，此处仅列出引用参考）：

安装参考：Documentations/environments.md · IceyBlackTea/cminus_compiler-2021-fall - Gitee.com

路径配置参考：(61条消息) llvm安装_消逝者的博客-CSDN博客_llvm安装

下载（llvm10.0.0）：

# 下载
wget https://github.com/llvm/llvm-project/archive/llvmorg-10.0.1.tar.gz
# 解压缩
tar zxvf llvmorg-10.0.1.tar.gz
mv llvm-project-llvmorg-10.0.1 llvm

编译安装：

mkdir ~/llvm-install
cd llvm && mkdir build && cd build
cmake  -DLLVM_ENABLE_PROJECTS="clang" -DCMAKE_BUILD_TYPE=Debug  -DCMAKE_INSTALL_PREFIX=$HOME/llvm-install ../llvm
# cmake  -DLLVM_ENABLE_PROJECTS="clang" -DLLVM_ENABLE_RUNTIMES="libcxx;libcxxabi" -DCMAKE_BUILD_TYPE=Debug  -DCMAKE_INSTALL_PREFIX=$HOME/llvm-install ../llvm
make -j 16 
make install

路径配置：

sudo gedit /etc/profile
# 打开后，在后面加上export PATH=the_path_to_your_llvm-install_bin:$PATH 
source /etc/profile
# 验证方法，clang --version，然后看路径

安装SYMCC

下载：git clone https://github.com/eurecom-s3/symcc.git

进入symcc文件夹，更新子模块：

git submodule init
git submodule update

更新子模块可能会有点慢，耐心等一下，多试几次

编译运行：

# mkdir build && cd build
cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Debug -DQSYM_BACKEND=ON #-DLLVM_DIR=/home/linmo/symcc/llvm/build 

ninja check

正确的话，应该pass16个

自己编写测试

在当前目录（symcc/build）下创建一个test.c文件

#include <stdio.h>
#include <stdint.h>
#include <unistd.h>

int foo(int a, int b) {
    if (2 * a < b)
        return a;
    else if (a % b)
        return b;
    else
        return a + b;
}

int main(int argc, char* argv[]) {
    int x;
    if (read(STDIN_FILENO, &x, sizeof(x)) != sizeof(x)) {
        printf("Failed to read x\n");
        return -1;
    }
    printf("%d\n", foo(x, 7));
    return 0;
}

$ ./symcc test.c -o test.out
$ mkdir results
$ export SYMCC_OUTPUT_DIR=`pwd`/results
$ echo 'aaaa' | ./test.out