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
10const register_t msgRegisters[] = {
11    X2, X3, X4, X5
12};
13compile_assert(
14    consistent_message_registers,
15    sizeof(msgRegisters) / sizeof(msgRegisters[0]) == n_msgRegisters
16);
17
18const 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};
22compile_assert(
23    consistent_frame_registers,
24    sizeof(frameRegisters) / sizeof(frameRegisters[0]) == n_frameRegisters
25);
26
27const 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};
32compile_assert(
33    consistent_gp_registers,
34    sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters
35);
36
37#ifdef CONFIG_KERNEL_MCS
38word_t getNBSendRecvDest(void)
39{
40    return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest);
41}
42#endif
43