diff --git a/local/scripts/test-lowlevel-controllers-qemu.sh b/local/scripts/test-lowlevel-controllers-qemu.sh new file mode 100755 index 00000000..9c156938 --- /dev/null +++ b/local/scripts/test-lowlevel-controllers-qemu.sh @@ -0,0 +1,48 @@ +#!/usr/bin/env bash +# Run the bounded low-level controller proof helpers in sequence. + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" + +usage() { + cat <<'USAGE' +Usage: test-lowlevel-controllers-qemu.sh [config] + +Run the bounded low-level controller/runtime proof helpers in sequence. +Defaults to redbear-desktop. + +Checks run: + - xHCI interrupt path + - IOMMU first-use path + - PS/2 + serio path + - monotonic timer path + +MSI-X remains a separate proof helper because its current default target is redbear-full. +USAGE +} + +for arg in "$@"; do + case "$arg" in + --help|-h|help) + usage + exit 0 + ;; + esac +done + +config="${1:-redbear-desktop}" + +echo ">>> Running xHCI interrupt proof" +bash "$SCRIPT_DIR/test-xhci-irq-qemu.sh" --check "$config" + +echo ">>> Running IOMMU first-use proof" +bash "$SCRIPT_DIR/test-iommu-qemu.sh" --check "$config" + +echo ">>> Running PS/2 + serio proof" +bash "$SCRIPT_DIR/test-ps2-qemu.sh" --check "$config" + +echo ">>> Running monotonic timer proof" +bash "$SCRIPT_DIR/test-timer-qemu.sh" --check "$config" + +echo "All bounded low-level controller checks passed for $config" diff --git a/local/scripts/test-ps2-qemu.sh b/local/scripts/test-ps2-qemu.sh new file mode 100755 index 00000000..3069a8c8 --- /dev/null +++ b/local/scripts/test-ps2-qemu.sh @@ -0,0 +1,120 @@ +#!/usr/bin/env bash +# Launch or validate the PS/2 + serio path in QEMU. + +set -euo pipefail + +find_uefi_firmware() { + local candidates=( + "/usr/share/ovmf/x64/OVMF.4m.fd" + "/usr/share/OVMF/x64/OVMF.4m.fd" + "/usr/share/ovmf/x64/OVMF_CODE.4m.fd" + "/usr/share/OVMF/x64/OVMF_CODE.4m.fd" + "/usr/share/ovmf/OVMF.fd" + "/usr/share/OVMF/OVMF_CODE.fd" + "/usr/share/qemu/edk2-x86_64-code.fd" + ) + local path + for path in "${candidates[@]}"; do + if [[ -f "$path" ]]; then + printf '%s\n' "$path" + return 0 + fi + done + return 1 +} + +usage() { + cat <<'USAGE' +Usage: test-ps2-qemu.sh [--check] [config] [extra qemu args...] + +Launch or validate the PS/2 + serio path on a Red Bear image in QEMU. +USAGE +} + +check_mode=0 +filtered_args=() +config="redbear-desktop" +for arg in "$@"; do + case "$arg" in + --help|-h|help) + usage + exit 0 + ;; + --check) + check_mode=1 + ;; + redbear-*) + config="$arg" + ;; + *) + filtered_args+=("$arg") + ;; + esac +done + +firmware="$(find_uefi_firmware)" || { + echo "ERROR: no usable x86_64 UEFI firmware found" >&2 + exit 1 +} + +arch="${ARCH:-$(uname -m)}" +image="build/$arch/$config/harddrive.img" +extra="build/$arch/$config/extra.img" +extra_qemu_args="${filtered_args[*]:-}" + +if [[ ! -f "$image" ]]; then + echo "ERROR: missing image $image" >&2 + echo "Build it first with: ./local/scripts/build-redbear.sh $config" >&2 + exit 1 +fi + +if [[ ! -f "$extra" ]]; then + truncate -s 1g "$extra" +fi + +pkill -f "qemu-system-x86_64.*$image" 2>/dev/null || true +sleep 1 + +if [[ "$check_mode" -eq 1 ]]; then + expect <&2 + exit 1 +} + +arch="${ARCH:-$(uname -m)}" +image="build/$arch/$config/harddrive.img" +extra="build/$arch/$config/extra.img" +extra_qemu_args="${filtered_args[*]:-}" + +if [[ ! -f "$image" ]]; then + echo "ERROR: missing image $image" >&2 + echo "Build it first with: ./local/scripts/build-redbear.sh $config" >&2 + exit 1 +fi + +if [[ ! -f "$extra" ]]; then + truncate -s 1g "$extra" +fi + +pkill -f "qemu-system-x86_64.*$image" 2>/dev/null || true +sleep 1 + +if [[ "$check_mode" -eq 1 ]]; then + expect <