From d4a8aac8535192b6402aa15ca8e92b4ed86bb922 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 20 Oct 2025 09:04:07 +1100 Subject: [PATCH] arm,smc: verification refactor of decode/invoke - Factor out the inline assembly from invokeSMCCall so that it can be made a separate machine operation in the specification. This part of the change should produce the same binary as before. - Parse IPC buffer arguments in decode, not in invoke. This eliminates the "buffer" argument to the invoke function and keeps argument processing in decode. - Use setMR instead of replicating its functionality. - Reduce decode argument list to the ones that are used. Signed-off-by: Gerwin Klein --- include/arch/arm/arch/object/smc.h | 4 +- src/arch/arm/64/object/objecttype.c | 2 +- src/arch/arm/object/smc.c | 87 +++++++++++++++-------------- 3 files changed, 49 insertions(+), 44 deletions(-) diff --git a/include/arch/arm/arch/object/smc.h b/include/arch/arm/arch/object/smc.h index cd8982741..22c519548 100644 --- a/include/arch/arm/arch/object/smc.h +++ b/include/arch/arm/arch/object/smc.h @@ -8,5 +8,5 @@ #define NUM_SMC_REGS 8 -exception_t decodeARMSMCInvocation(word_t label, word_t length, cptr_t cptr, - cte_t *srcSlot, cap_t cap, bool_t call, word_t *buffer); +exception_t decodeARMSMCInvocation(word_t label, word_t length, cap_t cap, + bool_t call, word_t *buffer); diff --git a/src/arch/arm/64/object/objecttype.c b/src/arch/arm/64/object/objecttype.c index 192ac300b..08fb4f231 100644 --- a/src/arch/arm/64/object/objecttype.c +++ b/src/arch/arm/64/object/objecttype.c @@ -523,7 +523,7 @@ exception_t Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr, #endif /*CONFIG_ARM_SMMU*/ #ifdef CONFIG_ALLOW_SMC_CALLS case cap_smc_cap: - return decodeARMSMCInvocation(label, length, cptr, slot, cap, call, buffer); + return decodeARMSMCInvocation(label, length, cap, call, buffer); #endif default: #else diff --git a/src/arch/arm/object/smc.c b/src/arch/arm/object/smc.c index 7f771ecb3..ccbb18d7f 100644 --- a/src/arch/arm/object/smc.c +++ b/src/arch/arm/object/smc.c @@ -8,63 +8,63 @@ #ifdef CONFIG_ALLOW_SMC_CALLS #include -compile_assert(n_msgRegisters_less_than_smc_regs, n_msgRegisters <= NUM_SMC_REGS); +/** Wrapped in a struct for verification, so the array does not decay to a pointer. */ +typedef struct smc_args_t_ { + word_t arg[NUM_SMC_REGS]; +} smc_args_t; -static exception_t invokeSMCCall(word_t *buffer, bool_t call) +/** We need the function result to be returned on the stack for verification. + * In reality, this function is inlined and the compiler should optimise all + * of this argument shuffling away. */ +static inline smc_args_t doSMC(smc_args_t smc_args) { - word_t i; - seL4_Word arg[NUM_SMC_REGS]; - word_t *ipcBuffer; + register seL4_Word r0 asm("x0") = smc_args.arg[0]; + register seL4_Word r1 asm("x1") = smc_args.arg[1]; + register seL4_Word r2 asm("x2") = smc_args.arg[2]; + register seL4_Word r3 asm("x3") = smc_args.arg[3]; + register seL4_Word r4 asm("x4") = smc_args.arg[4]; + register seL4_Word r5 asm("x5") = smc_args.arg[5]; + register seL4_Word r6 asm("x6") = smc_args.arg[6]; + register seL4_Word r7 asm("x7") = smc_args.arg[7]; - for (i = 0; i < NUM_SMC_REGS; i++) { - arg[i] = getSyscallArg(i, buffer); - } - - ipcBuffer = lookupIPCBuffer(true, NODE_STATE(ksCurThread)); - - register seL4_Word r0 asm("x0") = arg[0]; - register seL4_Word r1 asm("x1") = arg[1]; - register seL4_Word r2 asm("x2") = arg[2]; - register seL4_Word r3 asm("x3") = arg[3]; - register seL4_Word r4 asm("x4") = arg[4]; - register seL4_Word r5 asm("x5") = arg[5]; - register seL4_Word r6 asm("x6") = arg[6]; - register seL4_Word r7 asm("x7") = arg[7]; asm volatile("smc #0\n" : "+r"(r0), "+r"(r1), "+r"(r2), "+r"(r3), "+r"(r4), "+r"(r5), "+r"(r6), "+r"(r7) :: "x8", "x9", "x10", "x11", "x12", "x13", "x14", "x15", "x16", "x17", "memory"); - arg[0] = r0; - arg[1] = r1; - arg[2] = r2; - arg[3] = r3; - arg[4] = r4; - arg[5] = r5; - arg[6] = r6; - arg[7] = r7; + smc_args.arg[0] = r0; + smc_args.arg[1] = r1; + smc_args.arg[2] = r2; + smc_args.arg[3] = r3; + smc_args.arg[4] = r4; + smc_args.arg[5] = r5; + smc_args.arg[6] = r6; + smc_args.arg[7] = r7; + return smc_args; +} + +static exception_t invokeSMCCall(smc_args_t smc_args, bool_t call) +{ + smc_args = doSMC(smc_args); if (call) { - for (i = 0; i < n_msgRegisters; i++) { - setRegister(NODE_STATE(ksCurThread), msgRegisters[i], arg[i]); + tcb_t *thread = NODE_STATE(ksCurThread); + word_t *ipcBuffer = lookupIPCBuffer(true, thread); + + setRegister(thread, badgeRegister, 0); + for (word_t i = 0; i < NUM_SMC_REGS; i++) { + setMR(thread, ipcBuffer, i, smc_args.arg[i]); } - if (ipcBuffer != NULL) { - for (; i < NUM_SMC_REGS; i++) { - ipcBuffer[i + 1] = arg[i]; - } - } - - setRegister(NODE_STATE(ksCurThread), badgeRegister, 0); - setRegister(NODE_STATE(ksCurThread), msgInfoRegister, wordFromMessageInfo( - seL4_MessageInfo_new(0, 0, 0, i))); + word_t length = ipcBuffer ? NUM_SMC_REGS : n_msgRegisters; + setRegister(thread, msgInfoRegister, wordFromMessageInfo( + seL4_MessageInfo_new(0, 0, 0, length))); } setThreadState(NODE_STATE(ksCurThread), ThreadState_Running); return EXCEPTION_NONE; } -exception_t decodeARMSMCInvocation(word_t label, word_t length, cptr_t cptr, - cte_t *srcSlot, cap_t cap, bool_t call, word_t *buffer) +exception_t decodeARMSMCInvocation(word_t label, word_t length, cap_t cap, bool_t call, word_t *buffer) { if (label != ARMSMCCall) { userError("ARMSMCInvocation: Illegal operation."); @@ -87,8 +87,13 @@ exception_t decodeARMSMCInvocation(word_t label, word_t length, cptr_t cptr, return EXCEPTION_SYSCALL_ERROR; } + smc_args_t smc_args; + for (word_t i = 0; i < NUM_SMC_REGS; i++) { + smc_args.arg[i] = getSyscallArg(i, buffer); + } + setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); - return invokeSMCCall(buffer, call); + return invokeSMCCall(smc_args, call); } #endif