about summary refs log tree commit diff stats
path: root/tools/verify_qemu.py
diff options
context:
space:
mode:
authorTheofilos Augoustis <theofilos.augoustis@tum.de>2025-08-28 13:31:51 +0000
committerTheofilos Augoustis <theofilos.augoustis@tum.de>2025-08-28 13:31:51 +0000
commit1ed51b9a902d7669c4dd26edf1a75d79c888bef4 (patch)
tree30ecfa2ce98474fd4447d2dcf1814d4c16661602 /tools/verify_qemu.py
parentff3c9a0136b1b308a06d01108157146cc315274b (diff)
downloadfocaccia-1ed51b9a902d7669c4dd26edf1a75d79c888bef4.tar.gz
focaccia-1ed51b9a902d7669c4dd26edf1a75d79c888bef4.zip
Refactor tool handling to match flake system
Diffstat (limited to 'tools/verify_qemu.py')
-rwxr-xr-xtools/verify_qemu.py106
1 files changed, 0 insertions, 106 deletions
diff --git a/tools/verify_qemu.py b/tools/verify_qemu.py
deleted file mode 100755
index 7402852..0000000
--- a/tools/verify_qemu.py
+++ /dev/null
@@ -1,106 +0,0 @@
-#!/usr/bin/env python3
-
-"""
-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 (`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 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`.
-"""
-
-import argparse
-import os
-import subprocess
-import sys
-
-from focaccia.compare import ErrorTypes
-
-verbosity = {
-    'info':    ErrorTypes.INFO,
-    'warning': ErrorTypes.POSSIBLE,
-    'error':   ErrorTypes.CONFIRMED,
-}
-
-def make_argparser():
-    """This is also used by the GDB-invoked script to parse its args."""
-    prog = argparse.ArgumentParser()
-    prog.description = """Use Focaccia to test QEMU.
-
-Uses QEMU's GDB-server feature to read QEMU's emulated state and test its
-transformation during emulation against a symbolic truth.
-
-In fact, this tool could be used to test any emulator that provides a
-GDB-server interface. The server must support reading registers, reading
-memory, and stepping forward by single instructions.
-"""
-    prog.add_argument('hostname',
-                      help='The hostname at which to find the GDB server.')
-    prog.add_argument('port',
-                      type=int,
-                      help='The port at which to find the GDB server.')
-    prog.add_argument('--symb-trace',
-                      required=True,
-                      help='A pre-computed symbolic transformation trace to' \
-                           ' be used for verification. Generate this with' \
-                           ' the `tools/capture_transforms.py` tool.')
-    prog.add_argument('-q', '--quiet',
-                      default=False,
-                      action='store_true',
-                      help='Don\'t print a verification result.')
-    prog.add_argument('-o', '--output',
-                      help='If specified with a file name, the recorded'
-                           ' emulator states will be written to that file.')
-    prog.add_argument('--error-level',
-                      default='warning',
-                      choices=list(verbosity.keys()))
-    return prog
-
-def quoted(s: str) -> str:
-    return f'"{s}"'
-
-def try_remove(l: list, v):
-    try:
-        l.remove(v)
-    except ValueError:
-        pass
-
-if __name__ == "__main__":
-    prog = make_argparser()
-    prog.add_argument('--gdb', default='gdb',
-                      help='GDB binary to invoke.')
-    args = prog.parse_args()
-
-    filepath = os.path.realpath(__file__)
-    qemu_tool_path = os.path.join(os.path.dirname(filepath), '_qemu_tool.py')
-
-    # We have to remove all arguments we don't want to pass to the qemu tool
-    # manually here. Not nice, but what can you do..
-    argv = sys.argv
-    try_remove(argv, '--gdb')
-    try_remove(argv, args.gdb)
-
-    # Assemble the argv array passed to the qemu tool. GDB does not have a
-    # 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)}]'
-
-    gdb_cmd = [
-        args.gdb,
-        '-nx',  # Don't parse any .gdbinits
-        '--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)