SymQEMU tests and Dockefile

.dockerignore

@@ -0,0 +1 @@
+build

.gitmodules

@@ -43,3 +43,6 @@
 [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

Dockerfile

@@ -0,0 +1,40 @@
+FROM symcc AS symcc
+
+FROM ubuntu:22.04
+
+RUN apt update
+RUN apt install -y \
+    ninja-build \
+    libglib2.0-dev \
+    llvm \
+    python3 \
+    python3-pip
+
+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 libSymbolize.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                                                       \
+          --audio-drv-list=                                           \
+          --disable-sdl                                               \
+          --disable-gtk                                               \
+          --disable-vte                                               \
+          --disable-opengl                                            \
+          --disable-virglrenderer                                     \
+          --disable-werror                                            \
+          --target-list=x86_64-linux-user                             \
+          --enable-debug                                              \
+          --symcc-source=/symcc                                       \
+          --symcc-build=/symcc/build
+
+RUN make -j
+
+WORKDIR /symqemu_source/tests/symqemu
+RUN python3 -m unittest test.py

README.md

@@ -91,13 +91,15 @@ fuzzing helper will automatically pick up the setting and use QEMU mode too.)
 
 ## 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}` (which delegates any
-actual symbolic computation to SymCC's symbolic backend), and we have modified
-most code-generating functions in `tcg/tcg-op.c` 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`.
+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`.
 
 More information about the port to QEMU 8 and internals of (Sym)QEMU
 can be found in the QEMU 8 merge commit message

accel/tcg/meson.build

@@ -7,6 +7,8 @@ tcg_ss.add(files(
   'tcg-runtime-gvec.c',
   'tcg-runtime.c',
   'tcg-runtime-sym.c',
+  'tcg-runtime-sym-vec.c',
+  'tcg-runtime-sym-common.c',
   'translate-all.c',
   'translator.c',
 ))

accel/tcg/tcg-runtime-sym-common.c

@@ -0,0 +1,95 @@
+#include "qemu/osdep.h"
+#include "cpu.h"
+#include "exec/helper-proto.h"
+#include "exec/cpu_ldst.h"
+#include "qemu/qemu-print.h"
+#include "tcg/tcg.h"
+#include "exec/translation-block.h"
+
+#include "accel/tcg/tcg-runtime-sym-common.h"
+
+/* Include the symbolic backend, using void* as expression type. */
+
+#define SymExpr void*
+#include "RuntimeCommon.h"
+
+void *build_and_push_path_constraint(CPUArchState *env, void *arg1_expr, void *arg2_expr, uint32_t comparison_operator, uint8_t is_taken){
+    void *(*handler)(void *, void*);
+    switch (comparison_operator) {
+        case TCG_COND_EQ:
+            handler = _sym_build_equal;
+            break;
+        case TCG_COND_NE:
+            handler = _sym_build_not_equal;
+            break;
+        case TCG_COND_LT:
+            handler = _sym_build_signed_less_than;
+            break;
+        case TCG_COND_GE:
+            handler = _sym_build_signed_greater_equal;
+            break;
+        case TCG_COND_LE:
+            handler = _sym_build_signed_less_equal;
+            break;
+        case TCG_COND_GT:
+            handler = _sym_build_signed_greater_than;
+            break;
+        case TCG_COND_LTU:
+            handler = _sym_build_unsigned_less_than;
+            break;
+        case TCG_COND_GEU:
+            handler = _sym_build_unsigned_greater_equal;
+            break;
+        case TCG_COND_LEU:
+            handler = _sym_build_unsigned_less_equal;
+            break;
+        case TCG_COND_GTU:
+            handler = _sym_build_unsigned_greater_than;
+            break;
+        default:
+            g_assert_not_reached();
+    }
+
+    void *condition_symbol = handler(arg1_expr, arg2_expr);
+    _sym_push_path_constraint(condition_symbol, is_taken, get_pc(env));
+
+    return condition_symbol;
+}
+
+/* Architecture-independent way to get the program counter */
+target_ulong get_pc(CPUArchState *env)
+{
+    target_ulong pc, cs_base;
+    uint32_t flags;
+
+    cpu_get_tb_cpu_state(env, &pc, &cs_base, &flags);
+
+    return pc;
+}
+
+void *sym_rotate_left(void *arg1_expr, void *arg2_expr) {
+    /* The implementation follows the alternative implementation of
+     * tcg_gen_rotl_i64 in tcg-op.c (which handles architectures that don't
+     * support rotl directly). */
+
+    uint8_t bits = _sym_bits_helper(arg1_expr);
+    return _sym_build_or(
+            _sym_build_shift_left(arg1_expr, arg2_expr),
+            _sym_build_logical_shift_right(
+                    arg1_expr,
+                    _sym_build_sub(_sym_build_integer(bits, bits), arg2_expr)));
+}
+
+void *sym_rotate_right(void *arg1_expr, void *arg2_expr) {
+
+    /* The implementation follows the alternative implementation of
+     * tcg_gen_rotr_i64 in tcg-op.c (which handles architectures that don't
+     * support rotr directly). */
+
+    uint8_t bits = _sym_bits_helper(arg1_expr);
+    return _sym_build_or(
+            _sym_build_logical_shift_right(arg1_expr, arg2_expr),
+            _sym_build_shift_left(
+                    arg1_expr,
+                    _sym_build_sub(_sym_build_integer(bits, bits), arg2_expr)));
+}

accel/tcg/tcg-runtime-sym-common.h

@@ -0,0 +1,4 @@
+void *build_and_push_path_constraint(CPUArchState *env, void *arg1_expr, void *arg2_expr, uint32_t comparison_operator, uint8_t is_taken);
+target_ulong get_pc(CPUArchState *env);
+void *sym_rotate_left(void *arg1_expr, void *arg2_expr);
+void *sym_rotate_right(void *arg1_expr, void *arg2_expr);