Use symbolic execution to speed up QEMU testing

We don't need QEMU's log anymore, so we connect to a GDB server instance
that the user has to start with `$ qemu -g <port> ...`.

Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>

1 files changed, 23 insertions, 24 deletions

diff --git a/tools/invoke_qemu_tool.py b/tools/verify_qemu.py
index 152c208..98437cb 100644
--- a/tools/invoke_qemu_tool.py
+++ b/tools/verify_qemu.py
@@ -1,39 +1,32 @@
 """
-This mechanism exists to retrieve per-instruction program snapshots from QEMU,
-specifically including memory dumps. This is surprisingly nontrivial (we don't
-have a log option like `-d memory`), and the mechanism we have implemented to
-achieve this is accordingly complicated.
-
-In short: We use QEMU's feature to interact with the emulation via a GDB server
-interface together with parsing QEMU's logs to record register and memory state
-at single-instruction intervals.
-
-We need QEMU's log in addition to the GDB server because QEMU's GDB server does
-not support querying memory mapping information. We need this information to
-know from where we need to read memory, so we parse memory mappings from the
-log (option `-d page`).
+Spawn GDB, connect to QEMU's GDB server, and read test states from that.
 
 We need two scripts (this one and the primary `qemu_tool.py`) because we can't
 pass arguments to scripts executed via `gdb -x <script>`.
 
-This script (`invoke_qemu_tool.py`) is the one the user interfaces with. It
+This script (`verify_qemu.py`) is the one the user interfaces with. It
 eventually calls `execv` to spawn a GDB process that calls the main
-`qemu_tool.py` script; `python invoke_qemu_tool.py` essentially behaves as if
+`qemu_tool.py` script; `python verify_qemu.py` essentially behaves as if
 something like `gdb --batch -x qemu_tool.py` were executed instead. Before it
 starts GDB, though, it parses command line arguments and applies some weird but
 necessary logic to pass them to `qemu_tool.py`.
-
-The main script `qemu_tool.py`, which runs inside of GDB, finally forks a QEMU
-instance that provides a GDB server and writes its logs to a file. It then
-connects GDB to that server and incrementally reads the QEMU logs while
-stepping through the program. Doing that, it generates program snapshots at
-each instruction.
 """
 
+import argparse
 import os
+import subprocess
 import sys
 
-from qemu_tool import make_argparser
+def make_argparser():
+    """This is also used by the GDB-invoked script to parse its args."""
+    prog = argparse.ArgumentParser()
+    prog.add_argument('--symb-trace',
+                      required=True,
+                      help='A symbolic transformation trace to be used for' \
+                           ' verification.')
+    prog.add_argument('--output', '-o', help='Name of output file.')
+    prog.add_argument('gdbserver_port', type=int)
+    return prog
 
 def quoted(s: str) -> str:
     return f'"{s}"'
@@ -67,12 +60,18 @@ if __name__ == "__main__":
     # mechanism to pass arguments to a script that it executes, so we
     # overwrite `sys.argv` manually before invoking the script.
     argv_str = f'[{", ".join(quoted(a) for a in argv)}]'
+    path_str = f'[{", ".join(quoted(s) for s in sys.path)}]'
 
-    os.execv(args.gdb, [
+    gdb_cmd = [
         args.gdb,
         '-nx',  # Don't parse any .gdbinits
         '--batch-silent' if args.quiet else '--batch',
         '-ex', f'py import sys',
         '-ex', f'py sys.argv = {argv_str}',
+        '-ex', f'py sys.path = {path_str}',
         '-x', qemu_tool_path
-    ])
+    ]
+    proc = subprocess.Popen(gdb_cmd)
+
+    ret = proc.wait()
+    exit(ret)