1 /*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7 #include <assert.h>
8 #include <arch/machine/registerset.h>
9
10 const register_t msgRegisters[] = {
11 X2, X3, X4, X5
12 };
13 compile_assert(
14 consistent_message_registers,
15 sizeof(msgRegisters) / sizeof(msgRegisters[0]) == n_msgRegisters
16 );
17
18 const register_t frameRegisters[] = {
19 FaultIP, SP_EL0, SPSR_EL1,
20 X0, X1, X2, X3, X4, X5, X6, X7, X8, X16, X17, X18, X29, X30
21 };
22 compile_assert(
23 consistent_frame_registers,
24 sizeof(frameRegisters) / sizeof(frameRegisters[0]) == n_frameRegisters
25 );
26
27 const register_t gpRegisters[] = {
28 X9, X10, X11, X12, X13, X14, X15,
29 X19, X20, X21, X22, X23, X24, X25, X26, X27, X28,
30 TPIDR_EL0, TPIDRRO_EL0,
31 };
32 compile_assert(
33 consistent_gp_registers,
34 sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters
35 );
36
37 #ifdef CONFIG_KERNEL_MCS
getNBSendRecvDest(void)38 word_t getNBSendRecvDest(void)
39 {
40 return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest);
41 }
42 #endif
43