Expand base overlay patches and controller proofs

This commit is contained in:
2026-04-20 18:37:35 +01:00
parent 3c88e91789
commit 1dbb191a74
15 changed files with 13213 additions and 5830 deletions
@@ -10,15 +10,18 @@ usage() {
Usage: test-lowlevel-controllers-qemu.sh [config]
Run the bounded low-level controller/runtime proof helpers in sequence.
Defaults to redbear-desktop.
Defaults to redbear-mini (mapped by the individual helpers where needed).
Note: the IOMMU first-use proof still requires a target that actually ships `/usr/bin/iommu`, so
the wrapper automatically upgrades that single leg to `redbear-full` when invoked with
`redbear-mini`.
Checks run:
- MSI-X path
- 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
}
@@ -31,13 +34,25 @@ for arg in "$@"; do
esac
done
config="${1:-redbear-desktop}"
config="${1:-redbear-mini}"
iommu_config="$config"
if [[ "$config" == "redbear-mini" ]]; then
iommu_config="redbear-full"
fi
echo ">>> Running MSI-X proof"
bash "$SCRIPT_DIR/test-msix-qemu.sh" "$config"
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"
iommu_image="build/x86_64/${iommu_config}/harddrive.img"
if [[ -f "$iommu_image" ]]; then
bash "$SCRIPT_DIR/test-iommu-qemu.sh" --check "$iommu_config"
else
echo "SKIP: IOMMU first-use proof skipped because $iommu_image is missing"
fi
echo ">>> Running PS/2 + serio proof"
bash "$SCRIPT_DIR/test-ps2-qemu.sh" --check "$config"
@@ -45,4 +60,4 @@ 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"
echo "All bounded low-level controller checks passed for $config (IOMMU leg used $iommu_config)"