diff options
Diffstat (limited to '')
| -rw-r--r-- | tools/verify_qemu.py (renamed from tools/invoke_qemu_tool.py) | 47 |
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) |