diff options
Diffstat (limited to 'tools/verify_qemu.py')
| -rw-r--r-- | tools/verify_qemu.py | 47 |
1 files changed, 37 insertions, 10 deletions
diff --git a/tools/verify_qemu.py b/tools/verify_qemu.py index 98437cb..da2e985 100644 --- a/tools/verify_qemu.py +++ b/tools/verify_qemu.py @@ -17,15 +17,46 @@ 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. + +The GDB server is assumed to be at 'localhost'. +""" + prog.add_argument('port', + type=int, + help='The port at which QEMU\'s GDB server resides.') 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) + 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 trace' + ' of QEMU 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: @@ -41,20 +72,16 @@ if __name__ == "__main__": prog = make_argparser() prog.add_argument('--gdb', default='/bin/gdb', help='GDB binary to invoke') - prog.add_argument('--quiet', '-q', action='store_true', - help='Suppress all output') args = prog.parse_args() filepath = os.path.realpath(__file__) - qemu_tool_path = os.path.join(os.path.dirname(filepath), 'qemu_tool.py') + 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) - try_remove(argv, '--quiet') - try_remove(argv, '-q') # 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 @@ -65,7 +92,7 @@ if __name__ == "__main__": gdb_cmd = [ args.gdb, '-nx', # Don't parse any .gdbinits - '--batch-silent' if args.quiet else '--batch', + '--batch', '-ex', f'py import sys', '-ex', f'py sys.argv = {argv_str}', '-ex', f'py sys.path = {path_str}', |