Verify QEMU by abstracting over inconsistencies in trace logs via matching algorithm

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

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}',