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 <gerwin.klein@proofcraft.systems>

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);

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

src/arch/arm/object/smc.c

@@ -8,63 +8,63 @@
 #ifdef CONFIG_ALLOW_SMC_CALLS
 #include <arch/object/smc.h>
 
-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