From a4c7f87e332ca20085ee388fc7f3f469fbf54cc7 Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Thu, 3 Aug 2023 14:38:21 +1000 Subject: [PATCH 01/19] aarch64: Minimal update for vspace API change The aarch64 vspace API is changed to only have a single pagetable object and capability type for all intermediate page table levels. The root vspace object is still a separate object and capability type. Signed-off-by: Kent McLeod --- apps/sel4test-tests/src/tests/vspace.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/apps/sel4test-tests/src/tests/vspace.c b/apps/sel4test-tests/src/tests/vspace.c index fd0582e2..86b710a8 100644 --- a/apps/sel4test-tests/src/tests/vspace.c +++ b/apps/sel4test-tests/src/tests/vspace.c @@ -79,7 +79,11 @@ test_unmap_after_delete(env_t env) cspacepath_t path; int error; +#if seL4_PGDBits > 0 seL4_CPtr pgd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageGlobalDirectoryObject, 0); +#else + seL4_CPtr pgd = 0; +#endif seL4_CPtr pud = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageUpperDirectoryObject, 0); seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0); seL4_CPtr pt = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageTableObject, 0); From a188dbbf55e768f881359ec1135c0a6d49a038f0 Mon Sep 17 00:00:00 2001 From: Hesham Almatary Date: Mon, 31 Jul 2023 14:44:01 +0100 Subject: [PATCH 02/19] Fix: NULL-terminate existing_frames[] array libsel4utils/reserve_initial_task_regions iterates over existing_frames and expects it to be null-terminated. Without this commit, the behaviour will rely on whatever the stack had before allocating existing_frames[] in the stack, and subsequent calls may fail, hang, or reserve incorrect frames; depending on the stack values. Sponsored by: DARPA. Signed-off-by: Hesham Almatary --- apps/sel4test-tests/src/main.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/apps/sel4test-tests/src/main.c b/apps/sel4test-tests/src/main.c index 53cf39b2..d77a5423 100644 --- a/apps/sel4test-tests/src/main.c +++ b/apps/sel4test-tests/src/main.c @@ -119,13 +119,14 @@ static void init_allocator(env_t env, test_init_data_t *init_data) arch_init_allocator(env, init_data); /* create a vspace */ - void *existing_frames[init_data->stack_pages + 2]; + void *existing_frames[init_data->stack_pages + 3]; existing_frames[0] = (void *) init_data; existing_frames[1] = seL4_GetIPCBuffer(); assert(init_data->stack_pages > 0); for (int i = 0; i < init_data->stack_pages; i++) { existing_frames[i + 2] = init_data->stack + (i * PAGE_SIZE_4K); } + existing_frames[init_data->stack_pages + 2] = NULL; error = sel4utils_bootstrap_vspace(&env->vspace, &alloc_data, init_data->page_directory, &env->vka, NULL, NULL, existing_frames); From a4ef8fc880aabffbf67b177e427916f98faebafd Mon Sep 17 00:00:00 2001 From: Robbie VanVossen <986572+Furao@users.noreply.github.com> Date: Tue, 29 Aug 2023 03:56:09 -0400 Subject: [PATCH 03/19] settings: Disable timer tests for RocketChipZCU102 (#102) Signed-off-by: Robbie VanVossen --- settings.cmake | 2 ++ 1 file changed, 2 insertions(+) diff --git a/settings.cmake b/settings.cmake index 7454784d..ae8e55a9 100644 --- a/settings.cmake +++ b/settings.cmake @@ -80,11 +80,13 @@ if(NOT Sel4testAllowSettingsOverride) KernelPlatformZynqmp OR KernelPlatformPolarfire OR KernelPlatformQuartz64 + OR KernelPlatformRocketchipZCU102 OR (SIMULATION AND (KernelArchRiscV OR KernelArchARM)) ) # Frequency settings of the ZynqMP make the ltimer tests problematic # Polarfire does not have a complete ltimer implementation # Quartz64 does not have a complete ltimer implementation + # Rocket Chip on the ZCU102 FPGA does not have a timer peripheral set(Sel4testHaveTimer OFF CACHE BOOL "" FORCE) else() set(Sel4testHaveTimer ON CACHE BOOL "" FORCE) From 99a462e595977fac503b20400e40adcd0e7dee89 Mon Sep 17 00:00:00 2001 From: Robbie VanVossen Date: Thu, 8 Dec 2022 09:25:52 -0500 Subject: [PATCH 04/19] Add tests for SMC Capability Signed-off-by: Robbie VanVossen --- apps/sel4test-driver/include/test_init_data.h | 5 ++ apps/sel4test-driver/src/testtypes.c | 5 ++ apps/sel4test-tests/src/main.c | 3 + apps/sel4test-tests/src/tests/smc.c | 77 +++++++++++++++++++ 4 files changed, 90 insertions(+) create mode 100644 apps/sel4test-tests/src/tests/smc.c diff --git a/apps/sel4test-driver/include/test_init_data.h b/apps/sel4test-driver/include/test_init_data.h index 15f569e6..7bf2911c 100644 --- a/apps/sel4test-driver/include/test_init_data.h +++ b/apps/sel4test-driver/include/test_init_data.h @@ -64,6 +64,11 @@ typedef struct { /* sched control cap */ seL4_CPtr sched_ctrl; +#ifdef CONFIG_ALLOW_SMC_CALLS + /* smc cap */ + seL4_CPtr smc; +#endif /* CONFIG_ALLOW_SMC_CALLS */ + /* device frame cap */ seL4_CPtr device_frame_cap; diff --git a/apps/sel4test-driver/src/testtypes.c b/apps/sel4test-driver/src/testtypes.c index 27c8de63..2b2b8611 100644 --- a/apps/sel4test-driver/src/testtypes.c +++ b/apps/sel4test-driver/src/testtypes.c @@ -227,6 +227,11 @@ void basic_set_up(uintptr_t e) sel4utils_copy_cap_to_process(&(env->test_process), &env->vka, sched_ctrl); } } +#ifdef CONFIG_ALLOW_SMC_CALLS + env->init->smc = sel4utils_copy_cap_to_process(&(env->test_process), &env->vka, simple_get_init_cap(&env->simple, + seL4_CapSMC)); +#endif /* CONFIG_ALLOW_SMC_CALLS */ + /* setup data about untypeds */ env->init->untypeds = copy_untypeds_to_process(&(env->test_process), env->untypeds, env->num_untypeds, env); /* copy the fault endpoint - we wait on the endpoint for a message diff --git a/apps/sel4test-tests/src/main.c b/apps/sel4test-tests/src/main.c index d77a5423..60886cf1 100644 --- a/apps/sel4test-tests/src/main.c +++ b/apps/sel4test-tests/src/main.c @@ -198,6 +198,9 @@ int main(int argc, char **argv) env.asid_pool = init_data->asid_pool; env.asid_ctrl = init_data->asid_ctrl; env.sched_ctrl = init_data->sched_ctrl; +#ifdef CONFIG_ALLOW_SMC_CALLS + env.smc = init_data->smc; +#endif #ifdef CONFIG_IOMMU env.io_space = init_data->io_space; #endif diff --git a/apps/sel4test-tests/src/tests/smc.c b/apps/sel4test-tests/src/tests/smc.c new file mode 100644 index 00000000..07736ec4 --- /dev/null +++ b/apps/sel4test-tests/src/tests/smc.c @@ -0,0 +1,77 @@ +/* + * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include +#include +#include +#include +#include + +#include +#include + +#include "../test.h" +#include "../helpers.h" +#include "sel4/simple_types.h" + +#ifdef CONFIG_ALLOW_SMC_CALLS + +#define ARM_STD_SVC_VERSION 0x8400ff03 +#define UNASSIGNED_SMC 0x82000000 + +static int test_smc_calls(env_t env) +{ + seL4_ARM_SMCContext smc_args; + seL4_ARM_SMCContext smc_results; + int error; + + seL4_CPtr smc_cap = env->smc; + seL4_CPtr badged_smc_cap = get_free_slot(env); + + error = cnode_mint(env, smc_cap, badged_smc_cap, seL4_AllRights, ARM_STD_SVC_VERSION); + test_error_eq(error, seL4_NoError); + + /* Set function and arguments */ + smc_args.x0 = ARM_STD_SVC_VERSION; + smc_args.x1 = 0; + smc_args.x2 = 2; + smc_args.x3 = 3; + smc_args.x4 = 0; + smc_args.x5 = 0; + smc_args.x6 = 0; + smc_args.x7 = 0; + + /* This should succeed */ + error = seL4_ARM_SMC_Call(badged_smc_cap, &smc_args, &smc_results); + test_error_eq(error, seL4_NoError); + + /* Make sure the call returned something other than the input */ + test_neq(smc_results.x0, smc_args.x0); + + /* Check that the version returned is non-zero */ + seL4_Word version_sum = smc_results.x0 + smc_results.x1; + test_geq(version_sum, 1UL); + + /* Check that the remaining result registers are clobbered */ + test_eq(smc_results.x2, 0UL); + test_eq(smc_results.x3, 0UL); + + /* This should fail - SMC call with a different function id from badge */ + smc_args.x0 = UNASSIGNED_SMC; + error = seL4_ARM_SMC_Call(badged_smc_cap, &smc_args, &smc_results); + test_error_eq(error, seL4_IllegalOperation); + + /* This should fail - can't mint from cap with non-zero badge */ + seL4_CPtr bad_badged_cap = get_free_slot(env); + error = cnode_mint(env, badged_smc_cap, bad_badged_cap, seL4_AllRights, UNASSIGNED_SMC); + test_error_eq(error, seL4_IllegalOperation); + + return sel4test_get_result(); +} +DEFINE_TEST(SMC0001, "Test SMC calls", test_smc_calls, true) + +#endif From e7d9607a0bd1d5ddffa5ee1aa56e5b00dc74689e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 27 Oct 2023 12:23:03 +1100 Subject: [PATCH 05/19] SCHED0021: decrease chances of a race condition Decrease the chance that the monitor thread is preempted just when it has released the preemption threads, but before it has yielded itself. (If that happens, the preemption threads get two time slices.) See also #42 Signed-off-by: Gerwin Klein --- apps/sel4test-tests/src/tests/scheduler.c | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 3e6dcd83..b645bf68 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1598,11 +1598,17 @@ static int test_simple_preempt(struct env *env) /* Set a timeout for the test. * Each thread should be run for one tick */ - uint64_t start = time_now(env); - uint64_t now = start; /* Start executing other threads */ ZF_LOGD("Releasing Threads"); + /* Release our time slice now to get a new one. That should ensure we are + * not interrupted due to bad luck by the preemptive scheduler right after + * setting test_simple_preempt_start to 1 and then voluntarily yielding + * (which gives the preemption threads 2 time slices instead of one). For + * the same reason we are also printing the ZF_LOGD() above already. + */ + seL4_Yield(); + uint64_t start = time_now(env); test_simple_preempt_start = 1; /* Yield should cause all other threads to execute before returning * to the current thread. */ @@ -1610,7 +1616,7 @@ static int test_simple_preempt(struct env *env) test_simple_preempt_start = 0; /* Get the total time taken to synchronise */ - now = time_now(env); + uint64_t now = time_now(env); uint64_t duration = now - start; for (size_t thread = 0; thread < PREEMPTION_THREADS; thread += 1) { From ed4fb5ae10d78cd2679e65f76bb5a559dc474f92 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 9 Nov 2023 23:05:27 +0100 Subject: [PATCH 06/19] fix typo in comment Signed-off-by: Axel Heider --- apps/sel4test-tests/src/tests/scheduler.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index b645bf68..61b3b489 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1179,7 +1179,7 @@ sched0015_helper(int id, env_t env, volatile unsigned long long *counters) int test_budget_overrun(env_t env) { - /* Run two periodic threads that do not yeild but count the approximate + /* Run two periodic threads that do not yield but count the approximate * amount of time that they run for in 10's of nanoseconds. * * Each thread has a different share of the processor. From ab9189188ff3eff46d703e36081350f0f637b647 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 9 Nov 2023 23:05:17 +0100 Subject: [PATCH 07/19] fix description, the time slice is 100 ms Signed-off-by: Axel Heider --- apps/sel4test-tests/src/tests/scheduler.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 61b3b489..f79a25a4 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1003,7 +1003,7 @@ sched0011_helper(void) int test_scheduler_accuracy(env_t env) { /* - * Start a thread with a 1s timeslice at our priority, and make sure it + * Start a thread with a 100ms timeslice at our priority, and make sure it * runs for that long */ helper_thread_t helper; From b383b19b457c98b4e1fdf47aaaefa8270c406101 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 11 Jan 2024 20:56:10 +0100 Subject: [PATCH 08/19] CI: simulation and HW build with LLVM on RISCV Signed-off-by: Axel Heider --- .github/workflows/sel4test-hw.yml | 6 ++---- .github/workflows/sel4test-sim.yml | 5 ----- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml index af102b5b..c8d96906 100644 --- a/.github/workflows/sel4test-hw.yml +++ b/.github/workflows/sel4test-hw.yml @@ -33,11 +33,9 @@ jobs: strategy: fail-fast: false matrix: - march: [armv7a, armv8a, nehalem] + # There is no "rv32imac" hardware yet. + march: [armv7a, armv8a, nehalem, rv64imac] compiler: [gcc, clang] - include: - - march: rv64imac - compiler: gcc steps: - name: Build uses: seL4/ci-actions/sel4test-hw@master diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml index b54b78bb..98c0618b 100644 --- a/.github/workflows/sel4test-sim.yml +++ b/.github/workflows/sel4test-sim.yml @@ -21,11 +21,6 @@ jobs: matrix: march: [armv7a, armv8a, nehalem, rv32imac, rv64imac] compiler: [gcc, clang] - exclude: - - march: rv32imac - compiler: clang - - march: rv64imac - compiler: clang steps: - uses: seL4/ci-actions/sel4test-sim@master with: From 0a488b92bc7a08acc14d49524d1f22656f286627 Mon Sep 17 00:00:00 2001 From: Alwin Joshy Date: Mon, 15 Jan 2024 17:27:39 +1100 Subject: [PATCH 09/19] hw debug API: aarch64 sw break, single step tests Ported software breakpoint test to aarch64 and moved single stepping test from x86-only to arch-independent. Signed-off-by: Alwin Joshy --- apps/sel4test-tests/arch/arm/arch/debug.h | 9 + .../src/arch/x86/tests/breakpoints.c | 172 ------------------ apps/sel4test-tests/src/tests/breakpoints.c | 156 ++++++++++++++++ 3 files changed, 165 insertions(+), 172 deletions(-) delete mode 100644 apps/sel4test-tests/src/arch/x86/tests/breakpoints.c diff --git a/apps/sel4test-tests/arch/arm/arch/debug.h b/apps/sel4test-tests/arch/arm/arch/debug.h index aec8d537..2b5153e3 100644 --- a/apps/sel4test-tests/arch/arm/arch/debug.h +++ b/apps/sel4test-tests/arch/arm/arch/debug.h @@ -5,12 +5,21 @@ */ #pragma once +#ifdef CONFIG_ARCH_AARCH32 #define TEST_SOFTWARE_BREAK_ASM() \ asm volatile( \ ".global sbreak, post_sbreak\n\t" \ ".type post_sbreak, function\n\t" \ "sbreak:\n\t" \ "bkpt\n\t") +#elif CONFIG_ARCH_AARCH64 +#define TEST_SOFTWARE_BREAK_ASM() \ + asm volatile( \ + ".global sbreak, post_sbreak\n\t" \ + ".type post_sbreak, function\n\t" \ + "sbreak:\n\t" \ + "brk #0\n\t") +#endif /* Tell C about the symbols exported by the ASM above. */ extern char sbreak; diff --git a/apps/sel4test-tests/src/arch/x86/tests/breakpoints.c b/apps/sel4test-tests/src/arch/x86/tests/breakpoints.c deleted file mode 100644 index 4e10e5df..00000000 --- a/apps/sel4test-tests/src/arch/x86/tests/breakpoints.c +++ /dev/null @@ -1,172 +0,0 @@ -/* - * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) - * - * SPDX-License-Identifier: BSD-2-Clause - */ -#include - -#ifdef CONFIG_HARDWARE_DEBUG_API - -#include -#include - -#include -#include "../../../helpers.h" -#include "../../../test.h" -#include "../../../tests/breakpoints.h" - -/* Single-step test is currently only for x86. ARM requires some extra - * components before it can be usable. - */ -static volatile int counter; - -NO_INLINE static void stop_point(void) -{ - /* Counter is volatile so the compiler cannot optimize this away */ - counter = counter; -} - -NO_INLINE static void single_step_guinea_pig(void) -{ - for (; counter < SINGLESTEP_TEST_MAX_LOOP_ITERATIONS; counter++) { - /* This syscall is inserted here to ensure that syscalls are being - * stepped over successfully on x86. On ARM, we can just disable single- - * stepping in PL1 and PL2 altogether, so the problem doesn't arise. - */ - seL4_Yield(); - } - stop_point(); -} - -int debugger_main(seL4_Word a0, seL4_Word reply, seL4_Word a2, seL4_Word a3) -{ - seL4_CPtr debuggee_tcb_cap = a0; - seL4_Word badge; - seL4_MessageInfo_t tag; - seL4_TCB_ConfigureSingleStepping_t result; - - /* The main thread sets a breakpoint in the debuggee thread, and this thread - * will get a fault on the fault EP. At that point we can enable - * single-stepping on the debuggee thread. - */ - tag = api_wait(fault_ep_cspath.capPtr, &badge); - - if (seL4_MessageInfo_get_label(tag) != seL4_Fault_DebugException) { - ZF_LOGE("debugger: Got unexpected fault %zd.\n", - seL4_MessageInfo_get_label(tag)); - return -1; - } - - fault_data.vaddr = seL4_GetMR(seL4_DebugException_FaultIP); - fault_data.reason = seL4_GetMR(seL4_DebugException_ExceptionReason); - fault_data.bp_num = seL4_GetMR(seL4_DebugException_BreakpointNumber); - if (fault_data.reason != seL4_InstructionBreakpoint - || fault_data.vaddr != (seL4_Word)&single_step_guinea_pig) { - ZF_LOGE("debugger: debug exception not triggered by expected conditions.\n"); - return -1; - } - - /* So now we can set the single stepping going. */ - ZF_LOGV("debugger: Instruction BP triggered: beginning single-stepping.\n"); - seL4_TCB_UnsetBreakpoint(debuggee_tcb_cap, TEST_FIRST_INSTR_BP); - result = seL4_TCB_ConfigureSingleStepping(debuggee_tcb_cap, TEST_FIRST_INSTR_BP + 1, 1); - - test_eq((int)result.bp_was_consumed, SINGLESTEP_EXPECTED_BP_CONSUMPTION_VALUE); - test_eq(result.error, seL4_NoError); - - /* Resume() the debuggee thread, and keep stepping until it reaches the - * stop point (when it calls stop_point()). - * - * Set the counter to 0. The debuggee thread will be incrementing this. - * We will check its value afterward to verify that the debuggee ran as - * expected. - */ - counter = 0; - seL4_TCB_Resume(debuggee_tcb_cap); - - for (;;) { - tag = api_recv(fault_ep_cspath.capPtr, &badge, reply); - - if (seL4_MessageInfo_get_label(tag) != seL4_Fault_DebugException) { - ZF_LOGE("Debugger: while single stepping, got unexpected fault.\n"); - return -1; - } - - fault_data.vaddr = seL4_GetMR(seL4_DebugException_FaultIP); - fault_data.reason = seL4_GetMR(seL4_DebugException_ExceptionReason); - fault_data.bp_num = seL4_GetMR(seL4_DebugException_TriggerAddress); - if (fault_data.reason != seL4_SingleStep) { - ZF_LOGE("Debugger: while single stepping, got debug exception, but " - "for the wrong reason (reason %zd).\n", - fault_data.reason); - return -1; - } - - if (fault_data.vaddr == (seL4_Word)&stop_point) { - /* We're done: disable single-stepping */ - ZF_LOGV("About to disable stepping and resume debuggee.\n"); - tag = seL4_MessageInfo_set_label(tag, 0); - seL4_SetMR(0, 0); - api_reply(reply, tag); - break; - } - - tag = seL4_MessageInfo_set_label(tag, 0); - seL4_SetMR(0, 1); - api_reply(reply, tag); - } - - if (fault_data.vaddr != (seL4_Word)&stop_point) { - ZF_LOGE("Exited loop, but the debuggee thread did not get where we " - "expected it to.\n"); - return -1; - } - - /* Test the value of "counter", which the debuggee thread was incrementing. */ - if (counter <= 0 || counter != SINGLESTEP_TEST_MAX_LOOP_ITERATIONS) { - return -1; - } - - return 0; -} - -int debuggee_main(seL4_Word a0, seL4_Word a1, seL4_Word a2, seL4_Word a3) -{ - ZF_LOGV("Debuggee: about to execute guinea_pig.\n"); - single_step_guinea_pig(); - return 0; -} - -static int test_debug_api_single_step(struct env *env) -{ - helper_thread_t debugger, debuggee; - int error; - - test_eq(setup_caps_for_test(env), 0); - - create_helper_thread(env, &debugger); - set_helper_priority(env, &debugger, BREAKPOINT_TEST_HANDLER_PRIO); - - error = setup_faulter_thread_for_test(env, &debuggee); - test_eq(error, seL4_NoError); - error = seL4_TCB_SetBreakpoint(get_helper_tcb(&debuggee), - TEST_FIRST_INSTR_BP, (seL4_Word)&single_step_guinea_pig, - seL4_InstructionBreakpoint, 0, seL4_BreakOnRead); - test_eq(error, seL4_NoError); - - start_helper(env, &debugger, &debugger_main, - get_helper_tcb(&debuggee), - get_helper_reply(&debuggee), 0, 0); - start_helper(env, &debuggee, &debuggee_main, 0, 0, 0, 0); - - wait_for_helper(&debugger); - wait_for_helper(&debuggee); - - cleanup_helper(env, &debuggee); - cleanup_helper(env, &debugger); - return sel4test_get_result(); -} -DEFINE_TEST(SINGLESTEP_001, "Attempt to step through a function", - test_debug_api_single_step, config_set(CONFIG_HARDWARE_DEBUG_API)); - -#endif /* #ifdef CONFIG_HARDWARE_DEBUG_API */ diff --git a/apps/sel4test-tests/src/tests/breakpoints.c b/apps/sel4test-tests/src/tests/breakpoints.c index 93efe0eb..d7db717c 100644 --- a/apps/sel4test-tests/src/tests/breakpoints.c +++ b/apps/sel4test-tests/src/tests/breakpoints.c @@ -449,6 +449,8 @@ DEFINE_TEST(BREAKPOINT_007, "Attempt to pass various invalid values to the " "invocations, and expect error return values.", test_debug_api_setbp_invalid_values, config_set(CONFIG_HARDWARE_DEBUG_API)) +/* Test software breakpoints */ + static int test_debug_api_software_break_request(struct env *env) { @@ -482,4 +484,158 @@ DEFINE_TEST(BREAK_REQUEST_001, "Use an INT3/BKPT instruction to trigger a " "listening handler.", test_debug_api_software_break_request, config_set(CONFIG_HARDWARE_DEBUG_API)) + +/* Test single stepping */ + +static volatile int counter; + +NO_INLINE static void stop_point(void) +{ + /* Counter is volatile so the compiler cannot optimize this away */ + counter = counter; +} + +NO_INLINE static void single_step_guinea_pig(void) +{ + for (; counter < SINGLESTEP_TEST_MAX_LOOP_ITERATIONS; counter++) { + /* This syscall is inserted here to ensure that syscalls are being + * stepped over successfully on x86. + */ + seL4_Yield(); + } + stop_point(); +} + +int debugger_main(seL4_Word a0, seL4_Word reply, seL4_Word a2, seL4_Word a3) +{ + seL4_CPtr debuggee_tcb_cap = a0; + seL4_Word badge; + seL4_MessageInfo_t tag; + seL4_TCB_ConfigureSingleStepping_t result; + + /* The main thread sets a breakpoint in the debuggee thread, and this thread + * will get a fault on the fault EP. At that point we can enable + * single-stepping on the debuggee thread. + */ + tag = api_wait(fault_ep_cspath.capPtr, &badge); + + if (seL4_MessageInfo_get_label(tag) != seL4_Fault_DebugException) { + ZF_LOGE("debugger: Got unexpected fault %zd.\n", + seL4_MessageInfo_get_label(tag)); + return -1; + } + + fault_data.vaddr = seL4_GetMR(seL4_DebugException_FaultIP); + fault_data.reason = seL4_GetMR(seL4_DebugException_ExceptionReason); + fault_data.bp_num = seL4_GetMR(seL4_DebugException_BreakpointNumber); + if (fault_data.reason != seL4_InstructionBreakpoint + || fault_data.vaddr != (seL4_Word)&single_step_guinea_pig) { + ZF_LOGE("debugger: debug exception not triggered by expected conditions.\n"); + return -1; + } + + /* So now we can set the single stepping going. */ + ZF_LOGV("debugger: Instruction BP triggered: beginning single-stepping.\n"); + seL4_TCB_UnsetBreakpoint(debuggee_tcb_cap, TEST_FIRST_INSTR_BP); + result = seL4_TCB_ConfigureSingleStepping(debuggee_tcb_cap, TEST_FIRST_INSTR_BP + 1, 1); + + test_eq((int)result.bp_was_consumed, SINGLESTEP_EXPECTED_BP_CONSUMPTION_VALUE); + test_eq(result.error, seL4_NoError); + + /* Resume() the debuggee thread, and keep stepping until it reaches the + * stop point (when it calls stop_point()). + * + * Set the counter to 0. The debuggee thread will be incrementing this. + * We will check its value afterward to verify that the debuggee ran as + * expected. + */ + counter = 0; + seL4_TCB_Resume(debuggee_tcb_cap); + + for (;;) { + tag = api_recv(fault_ep_cspath.capPtr, &badge, reply); + + if (seL4_MessageInfo_get_label(tag) != seL4_Fault_DebugException) { + ZF_LOGE("Debugger: while single stepping, got unexpected fault.\n"); + return -1; + } + + fault_data.vaddr = seL4_GetMR(seL4_DebugException_FaultIP); + fault_data.reason = seL4_GetMR(seL4_DebugException_ExceptionReason); + fault_data.bp_num = seL4_GetMR(seL4_DebugException_TriggerAddress); + if (fault_data.reason != seL4_SingleStep) { + ZF_LOGE("Debugger: while single stepping, got debug exception, but " + "for the wrong reason (reason %zd).\n", + fault_data.reason); + return -1; + } + + if (fault_data.vaddr == (seL4_Word)&stop_point) { + /* We're done: disable single-stepping */ + ZF_LOGV("About to disable stepping and resume debuggee.\n"); + tag = seL4_MessageInfo_set_label(tag, 0); + seL4_SetMR(0, 0); + api_reply(reply, tag); + break; + } + + tag = seL4_MessageInfo_set_label(tag, 0); + seL4_SetMR(0, 1); + api_reply(reply, tag); + } + + if (fault_data.vaddr != (seL4_Word)&stop_point) { + ZF_LOGE("Exited loop, but the debuggee thread did not get where we " + "expected it to.\n"); + return -1; + } + + /* Test the value of "counter", which the debuggee thread was incrementing. */ + if (counter <= 0 || counter != SINGLESTEP_TEST_MAX_LOOP_ITERATIONS) { + return -1; + } + + return 0; +} + +int debuggee_main(seL4_Word a0, seL4_Word a1, seL4_Word a2, seL4_Word a3) +{ + ZF_LOGV("Debuggee: about to execute guinea_pig.\n"); + single_step_guinea_pig(); + return 0; +} + +static int test_debug_api_single_step(struct env *env) +{ + helper_thread_t debugger, debuggee; + int error; + + test_eq(setup_caps_for_test(env), 0); + + create_helper_thread(env, &debugger); + set_helper_priority(env, &debugger, BREAKPOINT_TEST_HANDLER_PRIO); + + error = setup_faulter_thread_for_test(env, &debuggee); + test_eq(error, seL4_NoError); + error = seL4_TCB_SetBreakpoint(get_helper_tcb(&debuggee), + TEST_FIRST_INSTR_BP, (seL4_Word)&single_step_guinea_pig, + seL4_InstructionBreakpoint, 0, seL4_BreakOnRead); + test_eq(error, seL4_NoError); + + start_helper(env, &debugger, &debugger_main, + get_helper_tcb(&debuggee), + get_helper_reply(&debuggee), 0, 0); + start_helper(env, &debuggee, &debuggee_main, 0, 0, 0, 0); + + wait_for_helper(&debugger); + wait_for_helper(&debuggee); + + cleanup_helper(env, &debuggee); + cleanup_helper(env, &debugger); + return sel4test_get_result(); +} +DEFINE_TEST(SINGLESTEP_001, "Attempt to step through a function", + test_debug_api_single_step, config_set(CONFIG_HARDWARE_DEBUG_API)); + + #endif /* CONFIG_HARDWARE_DEBUG_API */ From dae2ff3097965eb0242f9d677d610774a2267dea Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 7 Feb 2024 16:01:30 +1100 Subject: [PATCH 10/19] github: bump actions to node20 GitHub has started issuing warnings for node16 actions. Signed-off-by: Gerwin Klein --- .github/workflows/sel4test-hw.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml index c8d96906..5b9e100d 100644 --- a/.github/workflows/sel4test-hw.yml +++ b/.github/workflows/sel4test-hw.yml @@ -44,7 +44,7 @@ jobs: compiler: ${{ matrix.compiler }} sha: ${{ github.event.pull_request.head.sha }} - name: Upload images - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: images-${{ matrix.march }}-${{ matrix.compiler }} path: '*-images.tar.gz' @@ -76,13 +76,13 @@ jobs: matrix: ${{ fromJson(needs.the_matrix.outputs.matrix) }} steps: - name: Get machine queue - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: seL4/machine_queue path: machine_queue token: ${{ secrets.PRIV_REPO_TOKEN }} - name: Download image - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: images-${{ matrix.march }}-${{ matrix.compiler }} - name: Run From f1fa98c10eadf79d6a6dc7777dae81a4281c1a7f Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Mon, 14 Aug 2023 12:41:23 +1000 Subject: [PATCH 11/19] aarch64,smc: Add tests for SMC cap behaviors SMC caps are a new cap type for performing SMC calls on aarch64. These tests check that CNode operations behave as expected when manipulating capabilities of this type. Signed-off-by: Kent McLeod --- apps/sel4test-tests/src/tests/smc.c | 129 ++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) diff --git a/apps/sel4test-tests/src/tests/smc.c b/apps/sel4test-tests/src/tests/smc.c index 07736ec4..91e068ee 100644 --- a/apps/sel4test-tests/src/tests/smc.c +++ b/apps/sel4test-tests/src/tests/smc.c @@ -74,4 +74,133 @@ static int test_smc_calls(env_t env) } DEFINE_TEST(SMC0001, "Test SMC calls", test_smc_calls, true) + +int test_smc_2(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_copy(env, env->smc, dest, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} +DEFINE_TEST(SMC0002, "SMC Caps can be copied", test_smc_2, true) + +int test_smc_3(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_copy(env, env->smc, dest, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + error = cnode_revoke(env, env->smc); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0003, "Copied SMC Caps lose revocable authority", test_smc_3, true) + +int test_smc_4(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0004, "Unbadged SMC Caps can be badged", test_smc_4, true) + + +int test_smc_5(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_mint(env, dest, dest2, seL4_AllRights, 2); + test_error_eq(error, seL4_IllegalOperation); + test_assert(is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0005, "Badged SMC caps cannot change badge", test_smc_5, true) + +int test_smc_6(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_copy(env, dest, dest2, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} +DEFINE_TEST(SMC0006, "Badged SMC caps can be copied", test_smc_6, true) + + +int test_smc_7(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_copy(env, dest, dest2, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + error = cnode_revoke(env, dest); + test_assert(is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0007, "Original badged SMC caps can revoke copies", test_smc_7, true) + +int test_smc_8(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_mint(env, env->smc, dest2, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + + seL4_CPtr dest3 = get_free_slot(env); + error = cnode_copy(env, dest2, dest3, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest3)); + + error = cnode_revoke(env, dest2); + test_assert(is_slot_empty(env, dest3)); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + + +DEFINE_TEST(SMC0008, "Original badged SMC caps don't revoke other original badges", test_smc_8, true) + #endif From eb1b944338e9354d86cf6f3f4b6b72c9ed1ce19d Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Wed, 21 Feb 2024 08:36:18 +1100 Subject: [PATCH 12/19] SMC0001: Remove test of clobbered registers ATF implementations don't clobber x2 and x3 registers in response to ARM_STD_SVC_VERSION calls. Signed-off-by: Kent McLeod --- apps/sel4test-tests/src/tests/smc.c | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/apps/sel4test-tests/src/tests/smc.c b/apps/sel4test-tests/src/tests/smc.c index 91e068ee..0d43f0ae 100644 --- a/apps/sel4test-tests/src/tests/smc.c +++ b/apps/sel4test-tests/src/tests/smc.c @@ -38,8 +38,8 @@ static int test_smc_calls(env_t env) /* Set function and arguments */ smc_args.x0 = ARM_STD_SVC_VERSION; smc_args.x1 = 0; - smc_args.x2 = 2; - smc_args.x3 = 3; + smc_args.x2 = 0; + smc_args.x3 = 0; smc_args.x4 = 0; smc_args.x5 = 0; smc_args.x6 = 0; @@ -56,10 +56,6 @@ static int test_smc_calls(env_t env) seL4_Word version_sum = smc_results.x0 + smc_results.x1; test_geq(version_sum, 1UL); - /* Check that the remaining result registers are clobbered */ - test_eq(smc_results.x2, 0UL); - test_eq(smc_results.x3, 0UL); - /* This should fail - SMC call with a different function id from badge */ smc_args.x0 = UNASSIGNED_SMC; error = seL4_ARM_SMC_Call(badged_smc_cap, &smc_args, &smc_results); From 9ff09115ff5a674b9b968b3e677d76bb46432b3d Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Fri, 16 Feb 2024 17:59:51 +1100 Subject: [PATCH 13/19] 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 --- apps/sel4test-tests/src/tests/vcpu.c | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 apps/sel4test-tests/src/tests/vcpu.c diff --git a/apps/sel4test-tests/src/tests/vcpu.c b/apps/sel4test-tests/src/tests/vcpu.c new file mode 100644 index 00000000..f841b6bd --- /dev/null +++ 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 + +#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 From 8a8ccec3c8d8026a17324f3a62a26ece04250267 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Sun, 31 Mar 2024 04:22:32 +0200 Subject: [PATCH 14/19] cmake: don't overwrite NANOPB_SRC_ROOT_FOLDER Signed-off-by: Axel Heider --- settings.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/settings.cmake b/settings.cmake index ae8e55a9..81397c8c 100644 --- a/settings.cmake +++ b/settings.cmake @@ -17,7 +17,7 @@ list( ${project_modules} ) -set(NANOPB_SRC_ROOT_FOLDER "${project_dir}/tools/nanopb" CACHE INTERNAL "") +set(NANOPB_SRC_ROOT_FOLDER "${project_dir}/tools/nanopb" CACHE STRING "NanoPB Folder location") set(OPENSBI_PATH "${project_dir}/tools/opensbi" CACHE STRING "OpenSBI Folder location") set(SEL4_CONFIG_DEFAULT_ADVANCED ON) From a8f83c5b13a1900749066b7c9dfc5103bcc9c8e5 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Sun, 31 Mar 2024 04:19:00 +0200 Subject: [PATCH 15/19] cmake: remove trailing slash Signed-off-by: Axel Heider --- settings.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/settings.cmake b/settings.cmake index 81397c8c..1b096ebe 100644 --- a/settings.cmake +++ b/settings.cmake @@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 3.7.2) -set(project_dir "${CMAKE_CURRENT_LIST_DIR}/../../") +set(project_dir "${CMAKE_CURRENT_LIST_DIR}/../..") file(GLOB project_modules ${project_dir}/projects/*) list( APPEND From b416516310529af174313239147afe48c80b9c52 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 1 Apr 2024 00:15:54 +0200 Subject: [PATCH 16/19] CI: the seL4/machine_queue repo is public now Signed-off-by: Axel Heider --- .github/workflows/sel4test-hw.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml index 5b9e100d..0723bfb1 100644 --- a/.github/workflows/sel4test-hw.yml +++ b/.github/workflows/sel4test-hw.yml @@ -80,7 +80,6 @@ jobs: with: repository: seL4/machine_queue path: machine_queue - token: ${{ secrets.PRIV_REPO_TOKEN }} - name: Download image uses: actions/download-artifact@v4 with: From e0cb8031d586fec78dc949d4c284a545dbfec93d Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 2 Apr 2024 00:23:50 +0200 Subject: [PATCH 17/19] CI: cancel older concurrent PR runs Remove the space in the workflow name to ensure there are no side effects when using it as an identifier. Signed-off-by: Axel Heider --- .github/workflows/sel4test-hw.yml | 8 +++++++- .github/workflows/sel4test-sim.yml | 7 +++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml index 0723bfb1..ec1cdb2a 100644 --- a/.github/workflows/sel4test-hw.yml +++ b/.github/workflows/sel4test-hw.yml @@ -6,7 +6,7 @@ # # See sel4test-hw/builds.yml in the repo seL4/ci-actions for configs. -name: seL4Test HW +name: seL4Test-HW on: # needs PR target for secrets access; guard by requiring label @@ -17,6 +17,12 @@ on: permissions: contents: read +# Cancel older runs of this workflow that are still not finished for the +# current PR. This reduces the CI load. +concurrency: + group: ${{ github.workflow }}-pr-${{ github.event.number }} + cancel-in-progress: true + jobs: hw-build: name: HW Build diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml index 98c0618b..267839ee 100644 --- a/.github/workflows/sel4test-sim.yml +++ b/.github/workflows/sel4test-sim.yml @@ -13,6 +13,13 @@ on: branches: [master] pull_request: +# Cancel older runs of this workflow that are still not finished for the +# current PR. This reduces the CI load. For deployment to the master branch, +# the workflow will run on each push, but no cancellation happens here. +concurrency: + group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && format('pr-{0}', github.event.number) || format('run-{0}', github.run_id) }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + jobs: simulation: name: Simulation From 95522e9c2b2d3af5262430e905aeaa434c2a5d75 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 21 May 2024 13:13:34 +0200 Subject: [PATCH 18/19] TIMER0001: remove unused variable Signed-off-by: Axel Heider --- apps/sel4test-driver/src/tests/timer.c | 1 - 1 file changed, 1 deletion(-) diff --git a/apps/sel4test-driver/src/tests/timer.c b/apps/sel4test-driver/src/tests/timer.c index 2d650eb7..18b1860a 100644 --- a/apps/sel4test-driver/src/tests/timer.c +++ b/apps/sel4test-driver/src/tests/timer.c @@ -33,7 +33,6 @@ static int test_callback(uintptr_t token) int test_timer(driver_env_t env) { - uint64_t time = 0; test_finished = false; timer_test_data_t test_data = { .goal_count = 3 }; From 1df49ec846a8d4f7ec07a36af7ffbdf0f30ecfae Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Wed, 22 May 2024 22:54:59 +0200 Subject: [PATCH 19/19] trivial: fix comment Signed-off-by: Axel Heider --- apps/sel4test-driver/src/timer.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/sel4test-driver/src/timer.h b/apps/sel4test-driver/src/timer.h index 5fd0d9bf..100271af 100644 --- a/apps/sel4test-driver/src/timer.h +++ b/apps/sel4test-driver/src/timer.h @@ -11,7 +11,7 @@ #define TIMER_ID 0 -/* Timing related functions used only by in sel4test-driver */ +/* Timing related functions used only within sel4test-driver */ void handle_timer_interrupts(driver_env_t env, seL4_Word badge); void wait_for_timer_interrupt(driver_env_t env); void timeout(driver_env_t env, uint64_t ns, timeout_type_t timeout);