diff --git a/.dockerignore b/.dockerignore index 378eac25d3..10ea399322 100644 --- a/.dockerignore +++ b/.dockerignore @@ -1 +1,2 @@ build +.git diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0fdbf3845d..1d7208dccd 100644 --- 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 index 085606a21d..ea7bea87f2 100644 --- 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 index 55f5495903..2b5d6f50e7 100644 --- 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 index 2e49ef53c6..f940a49781 100644 --- 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 index 58b500a405..d7e0926ff1 100755 --- 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 diff --git a/meson.build b/meson.build index 6a3ee8c9fa..96f2380a26 100644 --- a/meson.build +++ b/meson.build @@ -1,5 +1,5 @@ project('qemu', ['c'], meson_version: '>=0.63.0', - default_options: ['warning_level=1', 'c_std=gnu11', 'cpp_std=gnu++11', 'b_colorout=auto', + default_options: ['warning_level=1', 'c_std=gnu11', 'cpp_std=gnu++17', 'b_colorout=auto', 'b_staticpic=false', 'stdsplit=false', 'optimization=2', 'b_pie=true'], version: files('VERSION')) @@ -13,6 +13,7 @@ not_found = dependency('', required: false) keyval = import('keyval') ss = import('sourceset') fs = import('fs') +cmake = import('cmake') targetos = host_machine.system() sh = find_program('sh') @@ -1080,6 +1081,29 @@ if targetos == 'linux' and (have_system or have_tools) required: get_option('libudev')) endif +symcc_rt_backend = get_option('symcc_rt_backend') + +if not fs.is_file('subprojects/symcc-rt/RuntimeCommon.h') + error('''Symcc Runtime does not seem to be present. +Did you initialize the symcc-rt submodule? (git submodule update --init --recursive subprojects/symcc-rt)''') +endif + +symcc_rt = not_found + +symcc_rt_vars = cmake.subproject_options() +symcc_rt_vars.add_cmake_defines({ + 'SYMCC_RT_BACKEND': symcc_rt_backend, + 'Z3_TRUST_SYSTEM_VERSION': get_option('symcc_rt_trust_system_z3'), + 'LLVM_VERSION': get_option('symcc_rt_llvm_version'), +}) + +symcc_rt_proj = cmake.subproject('symcc-rt', options: symcc_rt_vars) +if get_option('symcc_rt_shared') + symcc_rt = symcc_rt_proj.dependency('SymccRtShared') +else + symcc_rt = symcc_rt_proj.dependency('SymccRtStatic') +endif + mpathlibs = [libudev] mpathpersist = not_found if targetos == 'linux' and have_tools and get_option('mpath').allowed() @@ -3508,7 +3532,6 @@ subdir('plugins') subdir('ebpf') common_user_inc = [] -common_user_inc += config_host['SYMCC_INC'].split() subdir('common-user') subdir('bsd-user') @@ -3738,6 +3761,9 @@ common_ss.add(qom, qemuutil) common_ss.add_all(when: 'CONFIG_SYSTEM_ONLY', if_true: [system_ss]) common_ss.add_all(when: 'CONFIG_USER_ONLY', if_true: user_ss) +common_ss.add(symcc_rt) +specific_ss.add(symcc_rt) + common_all = common_ss.apply(config_all, strict: false) common_all = static_library('common', build_by_default: false, @@ -3885,16 +3911,13 @@ foreach target : target_dirs exe_name += '-unsigned' endif - symcc_libs = files(config_host['SYMCC_LIBS'].split()) - emulator = executable(exe_name, exe['sources'], install: true, c_args: c_args, dependencies: arch_deps + deps + exe['dependencies'], - objects: [lib.extract_all_objects(recursive: true), symcc_libs], + objects: lib.extract_all_objects(recursive: true), link_depends: [block_syms, qemu_syms] + exe.get('link_depends', []), link_args: link_args, - build_rpath: config_host['SYMCC_BUILD'], win_subsystem: exe['win_subsystem']) if targetos == 'darwin' @@ -4341,6 +4364,18 @@ summary_info += {'netmap support': have_netmap} summary_info += {'l2tpv3 support': have_l2tpv3} summary(summary_info, bool_yn: true, section: 'Network backends') +# SymQEMU +summary_info = {} +summary_info += {'SymCC Runtime Backend': symcc_rt_backend} +summary_info += {'SymCC Runtime trust system\'s Z3': get_option('symcc_rt_trust_system_z3')} +summary_info += {'SymCC Shared Library': get_option('symcc_rt_shared')} +if get_option('symcc_rt_llvm_version') != '' + summary_info += {'SymCC Runtime with LLVM Version': get_option('symcc_rt_llvm_version')} +else + summary_info += {'SymCC Runtime with LLVM Version': 'To be detected by SymCC Runtime build'} +endif +summary(summary_info, bool_yn: true, section: 'SymQEMU') + # Libraries summary_info = {} summary_info += {'libtasn1': tasn1} diff --git a/meson_options.txt b/meson_options.txt index c9baeda639..7a32ab5b30 100644 --- a/meson_options.txt +++ b/meson_options.txt @@ -368,3 +368,13 @@ option('qemu_ga_version', type: 'string', value: '', option('hexagon_idef_parser', type : 'boolean', value : true, description: 'use idef-parser to automatically generate TCG code for the Hexagon frontend') + +# SymQEMU related options +option('symcc_rt_backend', type: 'string', value: 'qsym', + description: 'SymCC Runtime backend to use. Please check SymCC Runtime for a list of available backends.') +option('symcc_rt_trust_system_z3', type: 'boolean', value: true, + description: 'Trust the system version of Z3 to build SymCC Runtime') +option('symcc_rt_shared', type: 'boolean', value: true, + description: 'Compile SymCC Runtime dynamically instead of statically.') +option('symcc_rt_llvm_version', type: 'string', value: '', + description: 'LLVM Version to use to compile SymCC Runtime.') diff --git a/scripts/meson-buildoptions.sh b/scripts/meson-buildoptions.sh index 680fa3f581..a8cd8d62c9 100644 --- a/scripts/meson-buildoptions.sh +++ b/scripts/meson-buildoptions.sh @@ -19,6 +19,12 @@ meson_options_help() { printf "%s\n" ' --disable-install-blobs install provided firmware blobs' printf "%s\n" ' --disable-qom-cast-debug cast debugging support' printf "%s\n" ' --disable-relocatable toggle relocatable install' + printf "%s\n" ' --disable-symcc-rt-shared' + printf "%s\n" ' Compile SymCC Runtime dynamically instead of' + printf "%s\n" ' statically.' + printf "%s\n" ' --disable-symcc-rt-trust-system-z3' + printf "%s\n" ' Trust the system version of Z3 to build SymCC' + printf "%s\n" ' Runtime' printf "%s\n" ' --docdir=VALUE Base directory for documentation installation' printf "%s\n" ' (can be empty) [share/doc]' printf "%s\n" ' --enable-block-drv-whitelist-in-tools' @@ -71,6 +77,10 @@ meson_options_help() { printf "%s\n" ' [QEMU]' printf "%s\n" ' --qemu-ga-version=VALUE version number for qemu-ga installer' printf "%s\n" ' --smbd=VALUE Path to smbd for slirp networking' + printf "%s\n" ' --symcc-rt-backend=VALUE SymCC Runtime backend to use. Please check SymCC' + printf "%s\n" ' Runtime for a list of available backends. [qsym]' + printf "%s\n" ' --symcc-rt-llvm-version=VALUE' + printf "%s\n" ' LLVM Version to use to compile SymCC Runtime.' printf "%s\n" ' --sysconfdir=VALUE Sysconf data directory [etc]' printf "%s\n" ' --tls-priority=VALUE Default TLS protocol/cipher priority string' printf "%s\n" ' [NORMAL]' @@ -488,6 +498,12 @@ _meson_option_parse() { --disable-stack-protector) printf "%s" -Dstack_protector=disabled ;; --enable-strip) printf "%s" -Dstrip=true ;; --disable-strip) printf "%s" -Dstrip=false ;; + --symcc-rt-backend=*) quote_sh "-Dsymcc_rt_backend=$2" ;; + --symcc-rt-llvm-version=*) quote_sh "-Dsymcc_rt_llvm_version=$2" ;; + --enable-symcc-rt-shared) printf "%s" -Dsymcc_rt_shared=true ;; + --disable-symcc-rt-shared) printf "%s" -Dsymcc_rt_shared=false ;; + --enable-symcc-rt-trust-system-z3) printf "%s" -Dsymcc_rt_trust_system_z3=true ;; + --disable-symcc-rt-trust-system-z3) printf "%s" -Dsymcc_rt_trust_system_z3=false ;; --sysconfdir=*) quote_sh "-Dsysconfdir=$2" ;; --enable-tcg) printf "%s" -Dtcg=enabled ;; --disable-tcg) printf "%s" -Dtcg=disabled ;; diff --git a/subprojects/symcc-rt b/subprojects/symcc-rt new file mode 160000 index 0000000000..c45c238d6b --- /dev/null +++ b/subprojects/symcc-rt @@ -0,0 +1 @@ +Subproject commit c45c238d6b5bd6906cd2522c5932d88b9cec578f diff --git a/symcc b/symcc deleted file mode 160000 index d04d5b4219..0000000000 --- a/symcc +++ /dev/null @@ -1 +0,0 @@ -Subproject commit d04d5b4219b161e85710cb9f71318ce83b2973d8 diff --git a/tests/unit/meson.build b/tests/unit/meson.build index 5ddf17581a..45837648fa 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -190,17 +190,13 @@ foreach test_name, extra: tests args = [] lwith = [] - # SymQEMU unit tests executable construction is a bit more complicated + # SymQEMU unit tests executable construction if test_name == 'check-sym-runtime' - # lookup the libSymRuntime.so and add it as a dependence - libdir = meson.current_build_dir() / '../../' / config_host['SYMCC_BUILD'] - symcc_runtime = cc.find_library('SymRuntime', dirs : libdir) - deps += [symcc_runtime] + deps += [symcc_rt] # embeds most of qemu objects, including SymQEMU lwith += [lib] args += ['-I../target/i386/', - '-I' + config_host['SYMCC_INC'], '-DCONFIG_TARGET="x86_64-linux-user-config-target.h"', '-DNEED_CPU_H', '-Ix86_64-linux-user']