SymCC Runtime Integration (#55)

* Removed SymCC submodule & added SymCC-RT submodule. * SymCC Runtime Integration * Option to change SymCC RT backend * Option to compile SymCC RT statically and dynamically * Update working distributions * Adapt Dockerfile and GitHub workflow. * Make it possible to build against all possible LLVM versions as a command line switch TODO: LLVM 18 is not currently working... --------- Co-authored-by: Sebastian Poeplau <[email protected]> Co-authored-by: Aurelien Francillon <[email protected]>
eurecom-s3 · Apr 9, 2024 · 45b4700 · 45b4700
1 parent ba782cb
commit 45b4700
Show file tree

Hide file tree

Showing 12 changed files with 159 additions and 120 deletions.
diff --git a/.dockerignore b/.dockerignore
@@ -1 +1,2 @@
 build
+.git
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -1,13 +1,14 @@
-on:
-  workflow_dispatch:
-  push:
-  pull_request:
-
-jobs:
-  build-and-test:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v4
-    - run: git submodule update --init --recursive symcc
-    - run: docker build -t symcc symcc
-    - run: docker build -t symqemu .
+on:
+  workflow_dispatch:
+  push:
+  pull_request:
+jobs:
+  build-and-test:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - run: git submodule update --init --recursive subprojects/symcc-rt
+    # build and test with default LLVM version 15
+    - run: docker build -t symqemu .
+    # LLVM version 14
+    - run: docker build --build-arg LLVM_VERSION=14 -t symqemu .
diff --git a/.gitmodules b/.gitmodules
@@ -43,6 +43,7 @@
 [submodule "tests/lcitool/libvirt-ci"]
 	path = tests/lcitool/libvirt-ci
 	url = https://gitlab.com/libvirt/libvirt-ci.git
-[submodule "symcc"]
-	path = symcc
-	url = https://github.com/eurecom-s3/symcc.git
+[submodule "subprojects/symcc-rt"]
+	path = subprojects/symcc-rt
+	url = https://github.com/eurecom-s3/symcc-rt.git
+	branch = main
diff --git a/Dockerfile b/Dockerfile
@@ -1,47 +1,58 @@
 # prepare machine
 FROM ubuntu:22.04 as builder
 
-RUN apt update
-RUN apt install -y \
+RUN apt update && apt install -y \
     ninja-build \
     libglib2.0-dev \
     llvm \
     git \
     python3 \
-    python3-pip
-
-#
-FROM builder as symqemu
+    python3-pip \
+    cmake \
+    wget \
+    lsb-release \
+    software-properties-common \
+    gnupg \
+    z3 \
+    libz3-dev \
+    libz3-dev \
+    libzstd-dev
+
+RUN pip install --user meson
+
+# This is passed along to symcc and qsym backend
+arg LLVM_VERSION=15
+
+# installing/building with the right LLVM version, currently:
+# - no plan to support < 11
+# - 12 to 15 are in official packages,
+# - 16 and 17 provided by llvm.org
+# - TODO 18 should be fixed
+RUN if  [ $LLVM_VERSION -le 11 ];  then echo "LLVM <= 11 not supported" ; false ;fi
+RUN if  [ $LLVM_VERSION -ge 18 ];  then echo "LLVM >= 18 currently not supported" ; false ;fi
+RUN if  [ $LLVM_VERSION -eq 12 ] || [ $LLVM_VERSION -eq 13 ] || [ $LLVM_VERSION -eq 14 ] || [ $LLVM_VERSION -eq 15 ]; then 	\
+    apt install -y llvm-${LLVM_VERSION} clang-${LLVM_VERSION} ; 								\
+    else mkdir /llvm && cd  /llvm &&  wget https://apt.llvm.org/llvm.sh && chmod +x llvm.sh && ./llvm.sh ${LLVM_VERSION};   	\
+    fi
 
 COPY . /symqemu_source
 WORKDIR /symqemu_source
 
-# Meson gives an error if symcc is in a subdirectory of symqemu
-RUN mv /symqemu_source/symcc /symcc
-
-# The only symcc artifact needed by symqemu is libSymRuntime.so
-# Instead of compiling symcc in this image, we rely on the existing symcc docker image and
-# we just copy libSymRuntime.so at the location where symqemu expects it
-COPY --from=symcc /symcc_build/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so /symcc/build/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so
-
-RUN ./configure                                                       \
+RUN mkdir build && cd build && ../configure                           \
           --audio-drv-list=                                           \
           --disable-sdl                                               \
           --disable-gtk                                               \
           --disable-vte                                               \
           --disable-opengl                                            \
           --disable-virglrenderer                                     \
-          --disable-werror                                            \
-          --target-list=x86_64-linux-user,riscv64-linux-user          \ 
+          --target-list=x86_64-linux-user,riscv64-linux-user          \
           --enable-debug                                              \
-          --symcc-source=/symcc                                       \
-          --symcc-build=/symcc/build                                  \
           --enable-debug-tcg                                          \
-          --enable-werror
+          --symcc-rt-llvm-version="$LLVM_VERSION"
 
-RUN make -j
+RUN cd build && make -j
 
-RUN make check
+RUN cd build && make check
 
 WORKDIR /symqemu_source/tests/symqemu
 RUN python3 -m unittest test.py
diff --git a/README.md b/README.md
@@ -2,34 +2,25 @@
 
 This is SymQEMU, a binary-only symbolic executor based on QEMU and SymCC. It
 currently extends QEMU 8.1 and works with the most recent version of SymCC.
-(See README.orig for QEMU's original README file.)
-A separate branch is available for the [old version of SymQEMU based on QEMU 4.1.1](https://github.com/eurecom-s3/symqemu/tree/4.1.1) we don't expect much 
+(See README.orig for QEMU's original README file.) A separate branch is
+available for the [old version of SymQEMU based on QEMU
+4.1.1](https://github.com/eurecom-s3/symqemu/tree/4.1.1) we don't expect much
 changes to happen there, but PR may be accepted.
 
 ## How to build
 
-SymQEMU requires [SymCC](https://github.com/eurecom-s3/symcc), so please
-download and build SymCC first. For best results, configure it with the QSYM
-backend as explained in the README. For the impatient, here's a quick summary of
-the required steps that may or may not work on your system:
+First of all, make sure the
+[symcc-rt](https://github.com/eurecom-s3/symcc-rt.git) submodule is initialized:
 
 ``` shell
-$ git clone https://github.com/eurecom-s3/symcc.git
-$ cd symcc
-$ git submodule update --init
-$ mkdir build
-$ cd build
-$ cmake -G Ninja -DQSYM_BACKEND=ON ..
-$ ninja
+$ git submodule update --init --recursive subprojects/symcc-rt
 ```
 
-Next, make sure that QEMU's build dependencies are installed. Most package
-managers provide a command to get them, e.g., `apt build-dep qemu` on Debian and
-Ubuntu, or `dnf builddep qemu` on Fedora and CentOS.
+Make sure that QEMU's build dependencies are installed. Most package managers
+provide a command to get them, e.g., `apt build-dep qemu` on Debian and Ubuntu,
+or `dnf builddep qemu` on Fedora and CentOS.
 
-We've extended QEMU's configuration script to accept pointers to SymCC's source
-and binaries. The following invocation is known to work on Debian 10, Arch and
-Fedora 33:
+The following invocation is known to work on Ubuntu 22.04 and Arch:
 
 ``` shell
 $ mkdir build
@@ -42,9 +33,7 @@ $ ../configure                                                    \
       --disable-opengl                                            \
       --disable-virglrenderer                                     \
       --disable-werror                                            \
-      --target-list=x86_64-linux-user                             \
-      --symcc-source=../symcc                                     \
-      --symcc-build=../symcc/build
+      --target-list=x86_64-linux-user
 $ make -j
 ```
 
@@ -54,6 +43,15 @@ target architectures is possible in principle but will require a bit of work
 because the current implementation assumes that we can pass around host pointers
 in guest registers.
 
+## SymQEMU compilation options
+
+Several compilation options are available:
+- `enable-symcc-shared`: Compile SymQEMU with the shared library of `SymCC
+  Runtime` instead of a static library.
+- `symcc-backend`: Choose a specific backend from `SymCC Runtime`. Please have a
+  look at [symcc-rt](https://github.com/eurecom-s3/symcc-rt.git) to get an
+  exhaustive list of available backends.
+
 ## Running SymQEMU
 
 If you built SymQEMU as described above, the binary will be in
@@ -84,23 +82,14 @@ This is a very basic use of symbolic execution. See SymCC's documentation for
 more advanced scenarios. Since SymQEMU is based on it, it understands all the
 same
 [settings](https://github.com/eurecom-s3/symcc/blob/master/docs/Configuration.txt),
-and you can even run SymQEMU with `symcc_fuzzing_helper` for [hybrid fuzzing](https://github.com/eurecom-s3/symcc/blob/master/docs/Fuzzing.txt): just
+and you can even run SymQEMU with `symcc_fuzzing_helper` for [hybrid
+fuzzing](https://github.com/eurecom-s3/symcc/blob/master/docs/Fuzzing.txt): just
 prefix the target command with `x86_64-linux-user/symqemu-x86_64`. (Note that
 you'll have to run AFL in QEMU mode by adding `-Q` to its command line; the
 fuzzing helper will automatically pick up the setting and use QEMU mode too.)
 
 ## Build with Docker
-First, make sure to have an up-to-date Docker image of SymCC. If you
-don't have one, either in the submodule, run:
-
-``` shell
-git submodule update --init --recursive symcc
-cd symcc
-docker build -t symcc .
-cd ..
-```
-
-Then build the SymQEMU image with (this will also run the tests):
+Build the SymQEMU image with (this will also run the tests):
 ```shell
 docker build -t symqemu .
 ```
@@ -146,23 +135,23 @@ Also, refer to [QEMU's own tests suite documentation](https://www.qemu.org/docs/
 
 ## Documentation
 
-The [paper](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html) contains
-details on how SymQEMU works. A large part of the implementation is the run-time support
-in `accel/tcg/tcg-runtime-sym.{c,h}` and `accel/tcg/tcg-runtime-sym-vec.{c,h}`  (which
-delegates any actual symbolic computation to SymCC's symbolic backend), and we have
-modified most code-generating functions in `tcg/tcg-op.c`, `tcg/tcg-op-vec.c` and
+The [paper](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html)
+contains details on how SymQEMU works. A large part of the implementation is the
+run-time support in `accel/tcg/tcg-runtime-sym.{c,h}` and
+`accel/tcg/tcg-runtime-sym-vec.{c,h}` (which delegates any actual symbolic
+computation to SymCC's symbolic backend), and we have modified most
+code-generating functions in `tcg/tcg-op.c`, `tcg/tcg-op-vec.c` and
 `include/tcg/tcg-op-common.h` to emit calls to the runtime.
 
-For development, configure with `--enable-debug` for run-time assertions; there are tests
-for the symbolic run-time support in `tests/check-sym-runtime.c`.
+For development, configure with `--enable-debug` for run-time assertions; there
+are tests for the symbolic run-time support in `tests/check-sym-runtime.c`.
 
-More information about the port to QEMU 8 and internals of (Sym)QEMU
-can be found in the QEMU 8 merge commit message
-[23e570bf42](https://github.com/eurecom-s3/symqemu/commit/23e570bf42531bcac66a54283eafd4c9c233891a) which
-gives some information about the adaptations performed. There are also
-some detailed explanations about potential problems in section 5.1 of
-Damien Maier's [bachelor
-thesis](https://dmaier.ch/bachelor-thesis.pdf).
+More information about the port to QEMU 8 and internals of (Sym)QEMU can be
+found in the QEMU 8 merge commit message
+[23e570bf42](https://github.com/eurecom-s3/symqemu/commit/23e570bf42531bcac66a54283eafd4c9c233891a)
+which gives some information about the adaptations performed. There are also
+some detailed explanations about potential problems in section 5.1 of Damien
+Maier's [bachelor thesis](https://dmaier.ch/bachelor-thesis.pdf).
 
 ## License
 

diff --git a/configure b/configure
@@ -242,8 +242,6 @@ default_cflags='-O2 -g'
 git_submodules_action="update"
 docs="auto"
 EXESUF=""
-symcc_source=""
-symcc_build=""
 system="yes"
 linux_user=""
 bsd_user=""
@@ -696,10 +694,6 @@ for opt do
   ;;
   --static) static="yes"
   ;;
-  --symcc-source=*) symcc_source="$optarg"
-  ;;
-  --symcc-build=*) symcc_build="$optarg"
-  ;;
   --host=*|--build=*|\
   --disable-dependency-tracking|\
   --sbindir=*|--sharedstatedir=*|\
@@ -880,8 +874,6 @@ Advanced options (experts only):
                            start the emulator (only use if you are including
                            desired devices in configs/devices/)
   --with-devices-ARCH=NAME override default configs/devices
-  --symcc-source=PATH      PATH to SymCC source code
-  --symcc-build=PATH       PATH to the build directory of SymCC with Qsym backend
   --enable-debug           enable common debug build options
   --cpu=CPU                Build for host CPU [$cpu]
   --disable-containers     don't use containers for cross-building
@@ -1678,19 +1670,6 @@ if test "$targetos" = windows; then
   echo "CONFIG_WIN32=y" >> contrib/plugins/$config_host_mak
 fi
 
-echo "# SymQEMU config" >> $config_host_mak
-if test -e "$symcc_source/runtime/RuntimeCommon.h"; then
-  echo "SYMCC_INC=$symcc_source/runtime" >> $config_host_mak
-else
-  error_exit "SymCC (source)" "Point --symcc-source to the SymCC source code"
-fi
-if test -e "$symcc_build/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so"; then
-  echo "SYMCC_BUILD=$symcc_build/SymRuntime-prefix/src/SymRuntime-build" >> $config_host_mak
-  echo "SYMCC_LIBS=$symcc_build/SymRuntime-prefix/src/SymRuntime-build/libSymRuntime.so" >> $config_host_mak
-else
-  error_exit "SymCC (runtime)" "Point --symcc-build to the SymCC build directory"
-fi
-
 # tests/tcg configuration
 (config_host_mak=tests/tcg/config-host.mak
 mkdir -p tests/tcg