Add ARM vCPU inject IRQ test

This patch aims to test the scenario where we inject an IRQ on a vCPU that does not have a TCB associated with it. Currently this results in the kernel crashing inside invokeVCPUInjectIRQ. This test aims to confirm that the eventual fix to the kernel is correct. Signed-off-by: Ivan Velickovic <[email protected]>
seL4 · Feb 19, 2024 · c78bdc5 · c78bdc5
1 parent dae2ff3
commit c78bdc5
Showing 1 changed file with 26 additions and 0 deletions.
diff --git a/apps/sel4test-tests/src/tests/vcpu.c b/apps/sel4test-tests/src/tests/vcpu.c
@@ -0,0 +1,26 @@
+/*
+ * Copyright 2024, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/* This file contains tests related to vCPU syscalls. */
+
+#include <sel4/sel4.h>
+
+#include "../helpers.h"
+
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+int test_vcpu_inject_without_tcb(env_t env)
+{
+    vka_object_t vcpu;
+    int error = vka_alloc_vcpu(&env->vka, &vcpu);
+    assert(!error);
+
+    error = seL4_ARM_VCPU_InjectIRQ(vcpu.cptr, 0, 0, 0, 0);
+    test_eq(error, seL4_NoError);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(VCPU0001, "Inject IRQ without TCB associated with vCPU", test_vcpu_inject_without_tcb, true)
+#endif