Integrate QEMU plugin directly into Focaccia ta/uniformize-qemu

9 files changed, 271 insertions, 154 deletions

diff --git a/.gitmodules b/.gitmodules
index d74c6a5..b2597ad 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -2,3 +2,7 @@
 	path = miasm
 	url = git@github.com:taugoust/miasm.git
 
+[submodule "qemu"]
+	path = qemu
+	url = git@github.com:TUM-DSE/focaccia-qemu.git
+	branch = ta/focaccia
diff --git a/README.md b/README.md
index 68033d9..698c3e1 100644
--- a/README.md
+++ b/README.md
@@ -1,26 +1,15 @@
 # Focaccia
 
-This repository contains initial code for comprehensive testing of binary
-translators.
+This repository contains the source code for Focaccia, a comprehensive validator for CPU emulators
+and binary translators.
 
 ## Requirements
 
-For Python dependencies, see the `requirements.txt`. We also require at least LLDB version 17 for `fs_base`/`gs_base`
-register support.
+Python dependencies are handled via pyproject and uv. We provide first-class support for Nix via our
+flake, which integrates with our Python uv environment via uv2nix. 
 
-I had to compile LLDB myself; these are the steps I had to take (you also need swig version >= 4):
-
-```
-git clone https://github.com/llvm/llvm-project <llvm-path>
-cd <llvm-path>
-cmake -S llvm -B build -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_PROJECTS="clang;lldb" -DLLDB_ENABLE_PYTHON=TRUE -DLLDB_ENABLE_SWIG=TRUE
-cmake --build build/ --parallel $(nproc)
-
-# Add the built LLDB python bindings to your PYTHONPATH:
-PYTHONPATH="$PYTHONPATH:$(./build/bin/lldb -P)"
-```
-
-It will take a while to compile.
+We do not support any other build system officially but Focaccia has been known to work on various
+other systems also, as long as its Python dependencies are provided.
 
 ## How To Use
 
@@ -34,19 +23,40 @@ A number of additional tools are included to simplify use when validating QEMU:
 ```bash
 capture-transforms -o oracle.trace bug.out
 qemu-x86_64 -g 12345 bug.out &
-validate-qemu --symb-trace oracle.trace localhost 12345
+validate-qemu --symb-trace oracle.trace --remote localhost:12345
 ```
 
-Alternatively if you have access to the focaccia QEMU plugin:
+The above workflow works for reproducing most QEMU bugs but cannot handle the following two cases:
+
+1. Optimization bugs
+
+2. Bugs in non-deterministic programs
+
+We provide alternative approaches for dealing with optimization bugs. Focaccia currently does not
+handle bugs in non-deterministic programs.
+
+### QEMU Optimization bugs 
+
+When a bug is suspected to be an optimization bug, you can use the Focaccia QEMU plugin. The QEMU
+plugin is exposed, along with the QEMU version corresponding to it, under the qemu-plugin package in
+the Nix flake.
+
+It is used as follows:
 
 ```bash
-validation_server.py --symb-trace oracle.trace --use-socket=/tmp/focaccia.sock --guest_arch=<arch>
+validate-qemu --symb-trace oracle.trace --use-socket=/tmp/focaccia.sock --guest_arch=arch
 ```
-After you see `Listening for QEMU Plugin connection at /tmp/focaccia.sock...` you can start QEMU like this:
+
+Once the server prints `Listening for QEMU Plugin connection at /tmp/focaccia.sock...`, QEMU can be
+started in debug mode:
+
 ```bash
-qemu-<arch> [-one-insn-per-tb] --plugin build/contrib/plugins/libfocaccia.so <bug.out>
+qemu-<arch> [-one-insn-per-tb] --plugin result/lib/plugins/libfocaccia.so bug.out
 ```
 
+Note: the above workflow assumes that you used `nix build .#qemu-plugin` to build the plugin under
+`result`.
+
 Using this workflow, Focaccia can determine whether a mistranslation occured in that particular QEMU run.
 
 ### Box64
@@ -72,31 +82,34 @@ The `tools/` directory contains additional utility scripts to work with focaccia
 
 The following files belong to a rough framework for the snapshot comparison engine:
 
- - `focaccia/snapshot.py`: Structures used to work with snapshots. The `ProgramState` class is our primary
-representation of program snapshots.
+ - `focaccia/snapshot.py`: Structures used to work with snapshots. The `ProgramState` class is our
+                           primary representation of program snapshots.
 
  - `focaccia/compare.py`: The central algorithms that work on snapshots.
 
- - `focaccia/arch/`: Abstractions over different processor architectures. Currently we have x86 and aarch64.
+ - `focaccia/arch/`: Abstractions over different processor architectures. Currently we have x86 and
+                     aarch64.
 
 ### Concolic execution
 
 The following files belong to a prototype of a data-dependency generator based on symbolic
 execution:
 
- - `focaccia/symbolic.py`: Algorithms and data structures to compute and manipulate symbolic program transformations.
-This handles the symbolic part of "concolic" execution.
+ - `focaccia/symbolic.py`: Algorithms and data structures to compute and manipulate symbolic program
+                           transformations. This handles the symbolic part of "concolic" execution.
 
- - `focaccia/lldb_target.py`: Tools for executing a program concretely and tracking its execution using
-[LLDB](https://lldb.llvm.org/). This handles the concrete part of "concolic" execution.
+ - `focaccia/lldb_target.py`: Tools for executing a program concretely and tracking its execution
+                              using [LLDB](https://lldb.llvm.org/). This handles the concrete part
+                              of "concolic" execution.
 
- - `focaccia/miasm_util.py`: Tools to evaluate Miasm's symbolic expressions based on a concrete state. Ties the symbolic
-and concrete parts together into "concolic" execution.
+ - `focaccia/miasm_util.py`: Tools to evaluate Miasm's symbolic expressions based on a concrete
+                             state. Ties the symbolic and concrete parts together into "concolic"
+                             execution.
 
 ### Helpers
 
- - `focaccia/parser.py`: Utilities for parsing logs from Arancini and QEMU, as well as serializing/deserializing to/from
-our own log format.
+ - `focaccia/parser.py`: Utilities for parsing logs from Arancini and QEMU, as well as
+                         serializing/deserializing to/from our own log format.
 
  - `focaccia/match.py`: Algorithms for trace matching.
 
@@ -104,14 +117,16 @@ our own log format.
 
 To add support for an architecture <arch>, do the following:
 
- - Add a file `focaccia/arch/<arch>.py`. This module declares the architecture's description, such as register names and
-an architecture class. The convention is to declare state flags (e.g. flags in RFLAGS for x86) as separate registers.
+ - Add a file `focaccia/arch/<arch>.py`. This module declares the architecture's description, such
+   as register names and an architecture class. The convention is to declare state flags (e.g. flags
+   in RFLAGS for x86) as separate registers.
 
  - Add the class to the `supported_architectures` dict in `focaccia/arch/__init__.py`.
 
- - Depending on Miasm's support for <arch>, add register name aliases to the `MiasmSymbolResolver.miasm_flag_aliases`
-dict in `focaccia/miasm_util.py`.
+ - Depending on Miasm's support for <arch>, add register name aliases to the
+   `MiasmSymbolResolver.miasm_flag_aliases` dict in `focaccia/miasm_util.py`.
+
+ - Depending on the existence of a flags register in <arch>, implement conversion from the flags
+   register's value to values of single logical flags (e.g. implement the operation `RFLAGS['OF']`)
+   in the respective concrete targets (LLDB, GDB, ...).
 
- - Depending on the existence of a flags register in <arch>, implement conversion from the flags register's value to
-values of single logical flags (e.g. implement the operation `RFLAGS['OF']`) in the respective concrete targets (LLDB,
-GDB, ...).
diff --git a/flake.lock b/flake.lock
index 0343a0a..a542c41 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,5 +1,37 @@
 {
   "nodes": {
+    "berkeley-softfloat-3": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1741391053,
+        "narHash": "sha256-TO1DhvUMd2iP5gvY9Hqy9Oas0Da7lD0oRVPBlfAzc90=",
+        "owner": "qemu-project",
+        "repo": "berkeley-softfloat-3",
+        "rev": "a0c6494cdc11865811dec815d5c0049fba9d82a8",
+        "type": "gitlab"
+      },
+      "original": {
+        "owner": "qemu-project",
+        "repo": "berkeley-softfloat-3",
+        "type": "gitlab"
+      }
+    },
+    "berkeley-testfloat-3": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1689946593,
+        "narHash": "sha256-inQAeYlmuiRtZm37xK9ypBltCJ+ycyvIeIYZK8a+RYU=",
+        "owner": "qemu-project",
+        "repo": "berkeley-testfloat-3",
+        "rev": "e7af9751d9f9fd3b47911f51a5cfd08af256a9ab",
+        "type": "gitlab"
+      },
+      "original": {
+        "owner": "qemu-project",
+        "repo": "berkeley-testfloat-3",
+        "type": "gitlab"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -18,6 +50,24 @@
         "type": "github"
       }
     },
+    "flake-utils_2": {
+      "inputs": {
+        "systems": "systems_2"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
         "lastModified": 1749285348,
@@ -34,19 +84,19 @@
         "type": "github"
       }
     },
-    "nixpkgs-qemu-60": {
+    "nixpkgs_2": {
       "locked": {
-        "lastModified": 1632168163,
-        "narHash": "sha256-iS3pBopSl0a2jAXuK/o0L+S86B9v9rnErsJHkNSdZRs=",
-        "owner": "nixos",
+        "lastModified": 1759831965,
+        "narHash": "sha256-vgPm2xjOmKdZ0xKA6yLXPJpjOtQPHfaZDRtH+47XEBo=",
+        "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "f8f124009497b3f9908f395d2533a990feee1de8",
+        "rev": "c9b6fb798541223bbb396d287d16f43520250518",
         "type": "github"
       },
       "original": {
-        "owner": "nixos",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
         "repo": "nixpkgs",
-        "rev": "f8f124009497b3f9908f395d2533a990feee1de8",
         "type": "github"
       }
     },
@@ -96,13 +146,30 @@
         "type": "github"
       }
     },
+    "qemu-submodule": {
+      "inputs": {
+        "berkeley-softfloat-3": "berkeley-softfloat-3",
+        "berkeley-testfloat-3": "berkeley-testfloat-3",
+        "flake-utils": "flake-utils_2",
+        "nixpkgs": "nixpkgs_2"
+      },
+      "locked": {
+        "path": "qemu/",
+        "type": "path"
+      },
+      "original": {
+        "path": "qemu/",
+        "type": "path"
+      },
+      "parent": []
+    },
     "root": {
       "inputs": {
         "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs",
-        "nixpkgs-qemu-60": "nixpkgs-qemu-60",
         "pyproject-build-systems": "pyproject-build-systems",
         "pyproject-nix": "pyproject-nix",
+        "qemu-submodule": "qemu-submodule",
         "uv2nix": "uv2nix"
       }
     },
@@ -121,6 +188,21 @@
         "type": "github"
       }
     },
+    "systems_2": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    },
     "uv2nix": {
       "inputs": {
         "nixpkgs": [
diff --git a/flake.nix b/flake.nix
index fccabba..931cba9 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,8 +6,6 @@
 
 		nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
 
-		nixpkgs-qemu-60.url = "github:nixos/nixpkgs/f8f124009497b3f9908f395d2533a990feee1de8";
-
 		flake-utils.url = "github:numtide/flake-utils";
 
 		pyproject-nix = {
@@ -27,21 +25,24 @@
 			inputs.nixpkgs.follows = "nixpkgs";
 			inputs.pyproject-nix.follows = "pyproject-nix";
 		};
+
+		qemu-submodule = {
+			url = "path:qemu/";
+			flake = true;
+		};
 	};
 
-	outputs = inputs@{
-		self,
+	outputs = {
 		uv2nix,
 		nixpkgs,
 		flake-utils,
 		pyproject-nix,
 		pyproject-build-systems,
+		qemu-submodule,
 		...
 	}:
 	flake-utils.lib.eachSystem [ "x86_64-linux" "aarch64-linux" ] (system:
 	let
-		qemu-60 = inputs.nixpkgs-qemu-60.qemu;
-
 		# Refine nixpkgs used in flake to system arch
 		pkgs = import nixpkgs {
 			inherit system;
@@ -271,6 +272,8 @@
 				];
 			});
 
+			qemu-plugin = qemu-submodule.packages.${system}.default;
+
 			default = focaccia;
 		};
 
@@ -302,7 +305,6 @@
 
 			validate-qemu = {
 				type = "app";
-				# program = "${packages.focaccia}/bin/validate-qemu";
 				program = let
 					wrapper = pkgs.writeShellScriptBin "validate-qemu" ''
 						exec ${packages.focaccia}/bin/validate-qemu --gdb "${gdbInternal}/bin/gdb" "$@"
diff --git a/pyproject.toml b/pyproject.toml
index 9e52dfb..54fad82 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -29,8 +29,8 @@ dev = [
 [project.scripts]
 focaccia = "focaccia.cli:main"
 convert = "focaccia.tools.convert:main"
-capture-transforms = "focaccia.tools.capture_transforms:main"
 validate-qemu = "focaccia.tools.validate_qemu:main"
+capture-transforms = "focaccia.tools.capture_transforms:main"
 
 [build-system]
 requires = ["hatchling"]
diff --git a/qemu b/qemu
new file mode 160000
+Subproject 3b2a0fb80eb9b6b5f216fa69069e66210466f5e
diff --git a/src/focaccia/tools/_qemu_tool.py b/src/focaccia/tools/_qemu_tool.py
index 706a9fe..631c79b 100644
--- a/src/focaccia/tools/_qemu_tool.py
+++ b/src/focaccia/tools/_qemu_tool.py
@@ -106,11 +106,11 @@ class GDBProgramState(ReadableProgramState):
             raise MemoryAccessError(addr, size, str(err))
 
 class GDBServerStateIterator:
-    def __init__(self, address: str, port: int):
+    def __init__(self, remote: str):
         gdb.execute('set pagination 0')
         gdb.execute('set sysroot')
         gdb.execute('set python print-stack full') # enable complete Python tracebacks
-        gdb.execute(f'target remote {address}:{port}')
+        gdb.execute(f'target remote {remote}')
         self._process = gdb.selected_inferior()
         self._first_next = True
 
@@ -291,22 +291,12 @@ def collect_conc_trace(gdb: GDBServerStateIterator, \
     return states, matched_transforms
 
 def main():
-    prog = make_argparser()
-    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.')
-
-    args = prog.parse_args()
-
-    gdbserver_addr = 'localhost'
-    gdbserver_port = args.port
+    args = make_argparser().parse_args()
 
     try:
-        gdb_server = GDBServerStateIterator(gdbserver_addr, gdbserver_port)
+        gdb_server = GDBServerStateIterator(args.remote)
     except:
-        raise Exception(f'Unable to perform basic GDB setup')
+        raise Exception('Unable to perform basic GDB setup')
 
     try:
         if args.executable is None:
diff --git a/src/focaccia/tools/validate_qemu.py b/src/focaccia/tools/validate_qemu.py
index 2b7e65c..edef9ae 100755
--- a/src/focaccia/tools/validate_qemu.py
+++ b/src/focaccia/tools/validate_qemu.py
@@ -6,6 +6,8 @@ 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>`.
 
+Alternatively, we connect to the Focaccia QEMU plugin when a socket is given.
+
 This script (`validate_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 validate_qemu.py` essentially behaves as if
@@ -21,6 +23,8 @@ import sysconfig
 import subprocess
 
 from focaccia.compare import ErrorTypes
+from focaccia.arch import supported_architectures
+from focaccia.tools.validation_server import start_validation_server
 
 verbosity = {
     'info':    ErrorTypes.INFO,
@@ -50,6 +54,7 @@ memory, and stepping forward by single instructions.
                       action='store_true',
                       help='Don\'t print a verification result.')
     prog.add_argument('-o', '--output',
+                      type=str,
                       help='If specified with a file name, the recorded'
                            ' emulator states will be written to that file.')
     prog.add_argument('--error-level',
@@ -59,6 +64,23 @@ memory, and stepping forward by single instructions.
                       default=None,
                       help='The executable executed under QEMU, overrides the auto-detected' \
                             'executable')
+    prog.add_argument('--use-socket',
+                      type=str,
+                      nargs='?',
+                      const='/tmp/focaccia.sock',
+                      help='Use QEMU plugin interface given by socket instead of GDB')
+    prog.add_argument('--guest-arch',
+                      type=str,
+                      choices=supported_architectures.keys(),
+                      help='Architecture of the emulated guest'
+                           '(Only required when using --use-socket)')
+    prog.add_argument('--remote',
+                      type=str,
+                      help='The hostname:port pair at which to find a QEMU GDB server.')
+    prog.add_argument('--gdb', 
+                      type=str,
+                      default='gdb',
+                      help='GDB binary to invoke.')
     return prog
 
 def quoted(s: str) -> str:
@@ -71,50 +93,62 @@ def try_remove(l: list, v):
         pass
 
 def main():
-    prog = make_argparser()
-    prog.add_argument('--gdb', default='gdb',
-                      help='GDB binary to invoke.')
-    args = prog.parse_args()
-
-    script_dirname = os.path.dirname(__file__)
-    qemu_tool_path = os.path.join(script_dirname, '_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)}]'
-
-    paths = sysconfig.get_paths()
-    candidates = [paths["purelib"], paths["platlib"]]
-    entries = [p for p in candidates if p and os.path.isdir(p)]
-    venv_site = entries[0]
+    argparser = make_argparser()
+    args = argparser.parse_args()
+
+    # Get environment
     env = os.environ.copy()
-    env["PYTHONPATH"] = ','.join([script_dirname, venv_site])
-
-    print(f"GDB started with Python Path: {env['PYTHONPATH']}")
-    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}',
-        "-ex", f"py import site; site.addsitedir({venv_site!r})",
-        "-ex", f"py import site; site.addsitedir({script_dirname!r})",
-        '-x', qemu_tool_path
-    ]
-    proc = subprocess.Popen(gdb_cmd, env=env)
-
-    ret = proc.wait()
-    exit(ret)
-
-if __name__ == "__main__":
-    main()
+
+    # Differentiate between the QEMU GDB server and QEMU plugin interfaces
+    if args.use_socket:
+        if not args.guest_arch:
+            argparser.error('--guest-arch is required when --use-socket is specified')
+
+        # QEMU plugin interface
+        start_validation_server(args.symb_trace,
+                                args.output,
+                                args.use_socket,
+                                args.guest_arch,
+                                env,
+                                verbosity[args.error_level],
+                                args.quiet)
+    else:
+        # QEMU GDB interface
+        script_dirname = os.path.dirname(__file__)
+        qemu_tool_path = os.path.join(script_dirname, '_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)}]'
+
+        paths = sysconfig.get_paths()
+        candidates = [paths["purelib"], paths["platlib"]]
+        entries = [p for p in candidates if p and os.path.isdir(p)]
+        venv_site = entries[0]
+        env["PYTHONPATH"] = ','.join([script_dirname, venv_site])
+
+        print(f"GDB started with Python Path: {env['PYTHONPATH']}")
+        gdb_cmd = [
+            args.gdb,
+            '-nx',  # Don't parse any .gdbinits
+            '--batch',
+            '-ex',  'py import sys',
+            '-ex', f'py sys.argv = {argv_str}',
+            '-ex', f'py sys.path = {path_str}',
+            "-ex", f'py import site; site.addsitedir({venv_site!r})',
+            "-ex", f'py import site; site.addsitedir({script_dirname!r})',
+            '-x', qemu_tool_path
+        ]
+        proc = subprocess.Popen(gdb_cmd, env=env)
+
+        ret = proc.wait()
+        exit(ret)
 
diff --git a/src/focaccia/tools/validation_server.py b/src/focaccia/tools/validation_server.py
index b87048a..db33ff3 100755
--- a/src/focaccia/tools/validation_server.py
+++ b/src/focaccia/tools/validation_server.py
@@ -1,25 +1,26 @@
 #! /usr/bin/env python3
 
+import os
+import socket
+import struct
+import logging
 from typing import Iterable
 
 import focaccia.parser as parser
 from focaccia.arch import supported_architectures, Arch
-from focaccia.compare import compare_symbolic
-from focaccia.snapshot import ProgramState, ReadableProgramState, \
-                              RegisterAccessError, MemoryAccessError
+from focaccia.compare import compare_symbolic, ErrorTypes
+from focaccia.snapshot import ProgramState, RegisterAccessError, MemoryAccessError
 from focaccia.symbolic import SymbolicTransform, eval_symbol, ExprMem
-from focaccia.trace import Trace, TraceEnvironment
+from focaccia.trace import Trace
 from focaccia.utils import print_result
 
-from validate_qemu import make_argparser, verbosity
 
-import socket
-import struct
-import os
+logger = logging.getLogger('focaccia-qemu-validation-server')
+debug = logger.debug
+info = logger.info
+warn = logger.warning
 
 
-SOCK_PATH = '/tmp/focaccia.sock'
-
 def endian_fmt(endianness: str) -> str:
     if endianness == 'little':
         return '<'
@@ -124,9 +125,8 @@ class PluginProgramState(ProgramState):
                 raise StopIteration
 
             if len(resp) < 180:
-                print(f'Invalid response length: {len(resp)}')
-                print(f'Response: {resp}')
-                return 0
+                raise RegisterAccessError(reg, f'Invalid response length when reading {reg}: {len(resp)}'
+                                          f' for response {resp}')
 
             val, size = unmk_register(resp, self.arch.endianness)
 
@@ -283,7 +283,7 @@ def record_minimal_snapshot(prev_state: ProgramState,
                 regval = cur_state.read_register(regname)
                 out_state.set_register(regname, regval)
             except RegisterAccessError:
-                pass
+                out_state.set_register(regname, 0)
         for mem in mems:
             assert(mem.size % 8 == 0)
             addr = eval_symbol(mem.ptr, prev_state)
@@ -377,27 +377,20 @@ def collect_conc_trace(qemu: PluginStateIterator, \
     return states, matched_transforms
 
 
-def main():
-    prog = make_argparser()
-    prog.add_argument('--use-socket',
-                      required=True,
-                      type=str,
-                      help='Use QEMU Plugin interface at <socket> instead of GDB')
-    prog.add_argument('--guest_arch',
-                      required=True,
-                      type=str,
-                      help='Architecture of the guest being emulated. (Only required when using --use-socket)')
-
-    args = prog.parse_args()
-
+def start_validation_server(symb_trace: str,
+                            output: str,
+                            socket: str,
+                            guest_arch: str,
+                            env,
+                            verbosity: ErrorTypes,
+                            is_quiet: bool = False):
     # Read pre-computed symbolic trace
-    with open(args.symb_trace, 'r') as strace:
+    with open(symb_trace, 'r') as strace:
         symb_transforms = parser.parse_transformations(strace)
 
-    arch = supported_architectures.get(args.guest_arch)
-    sock_path = args.use_socket
+    arch = supported_architectures.get(guest_arch)
 
-    qemu = PluginStateIterator(sock_path, arch)
+    qemu = PluginStateIterator(socket, arch)
 
     # Use symbolic trace to collect concrete trace from QEMU
     conc_states, matched_transforms = collect_conc_trace(
@@ -405,15 +398,12 @@ def main():
         symb_transforms.states)
 
     # Verify and print result
-    if not args.quiet:
+    if not is_quiet:
         res = compare_symbolic(conc_states, matched_transforms)
-        print_result(res, verbosity[args.error_level])
+        print_result(res, verbosity)
 
-    if args.output:
+    if output:
         from focaccia.parser import serialize_snapshots
-        with open(args.output, 'w') as file:
+        with open(output, 'w') as file:
             serialize_snapshots(Trace(conc_states, env), file)
 
-if __name__ == "__main__":
-    main()
-