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