1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#ifndef __LIBSEL4_SEL4_ARCH_CONSTANTS_H 14#define __LIBSEL4_SEL4_ARCH_CONSTANTS_H 15 16#ifdef HAVE_AUTOCONF 17#include <autoconf.h> 18#endif 19 20#ifndef __ASSEMBLER__ 21/* format of an unknown syscall message */ 22enum { 23 seL4_UnknownSyscall_X0, 24 seL4_UnknownSyscall_X1, 25 seL4_UnknownSyscall_X2, 26 seL4_UnknownSyscall_X3, 27 seL4_UnknownSyscall_X4, 28 seL4_UnknownSyscall_X5, 29 seL4_UnknownSyscall_X6, 30 seL4_UnknownSyscall_X7, 31 seL4_UnknownSyscall_FaultIP, 32 seL4_UnknownSyscall_SP, 33 seL4_UnknownSyscall_LR, 34 seL4_UnknownSyscall_SPSR, 35 seL4_UnknownSyscall_Syscall, 36 /* length of an unknown syscall message */ 37 seL4_UnknownSyscall_Length, 38 SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg), 39} seL4_UnknownSyscall_Msg; 40 41/* format of a user exception message */ 42enum { 43 seL4_UserException_FaultIP, 44 seL4_UserException_SP, 45 seL4_UserException_SPSR, 46 seL4_UserException_Number, 47 seL4_UserException_Code, 48 /* length of a user exception */ 49 seL4_UserException_Length, 50 SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg), 51} seL4_UserException_Msg; 52 53/* format of a vm fault message */ 54enum { 55 seL4_VMFault_IP, 56 seL4_VMFault_Addr, 57 seL4_VMFault_PrefetchFault, 58 seL4_VMFault_FSR, 59 seL4_VMFault_Length, 60 SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg), 61} seL4_VMFault_Msg; 62 63#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 64 65enum { 66 seL4_VGICMaintenance_IDX, 67 seL4_VGICMaintenance_Length, 68 SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg), 69} seL4_VGICMaintenance_Msg; 70 71enum { 72 seL4_VCPUFault_HSR, 73 seL4_VCPUFault_Length, 74 SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg), 75} seL4_VCPUFault_Msg; 76 77enum { 78 /* VM control registers EL1 */ 79 seL4_VCPUReg_SCTLR = 0, 80 seL4_VCPUReg_TTBR0, 81 seL4_VCPUReg_TTBR1, 82 seL4_VCPUReg_TCR, 83 seL4_VCPUReg_MAIR, 84 seL4_VCPUReg_AMAIR, 85 seL4_VCPUReg_CIDR, 86 87 /* other system registers EL1 */ 88 seL4_VCPUReg_ACTLR, 89 seL4_VCPUReg_CPACR, 90 91 /* exception handling registers EL1 */ 92 seL4_VCPUReg_AFSR0, 93 seL4_VCPUReg_AFSR1, 94 seL4_VCPUReg_ESR, 95 seL4_VCPUReg_FAR, 96 seL4_VCPUReg_ISR, 97 seL4_VCPUReg_VBAR, 98 99 /* thread pointer/ID registers EL0/EL1 */ 100 seL4_VCPUReg_TPIDR_EL0, 101 seL4_VCPUReg_TPIDR_EL1, 102 seL4_VCPUReg_TPIDRRO_EL0, 103 104 /* generic timer registers, to be completed */ 105 seL4_VCPUReg_CNTV_CTL, 106 seL4_VCPUReg_CNTV_TVAL, 107 seL4_VCPUReg_CNTV_CVAL, 108 109 /* general registers x0 to x30 have been saved by traps.S */ 110 seL4_VCPUReg_SP_EL1, 111 seL4_VCPUReg_ELR_EL1, 112 seL4_VCPUReg_SPSR_EL1, // 32-bit 113 seL4_VCPUReg_Num, 114} seL4_VCPUReg; 115 116#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 117 118enum { 119 seL4_TimeoutReply_FaultIP, 120 seL4_TimeoutReply_SP, 121 seL4_TimeoutReply_SPSR_EL1, 122 seL4_TimeoutReply_X0, 123 seL4_TimeoutReply_X1, 124 seL4_TimeoutReply_X2, 125 seL4_TimeoutReply_X3, 126 seL4_TimeoutReply_X4, 127 seL4_TimeoutReply_X5, 128 seL4_TimeoutReply_X6, 129 seL4_TimeoutReply_X7, 130 seL4_TimeoutReply_X8, 131 seL4_TimeoutReply_X16, 132 seL4_TimeoutReply_X17, 133 seL4_TimeoutReply_X18, 134 seL4_TimeoutReply_X29, 135 seL4_TimeoutReply_X30, 136 seL4_TimeoutReply_X9, 137 seL4_TimeoutReply_X10, 138 seL4_TimeoutReply_X11, 139 seL4_TimeoutReply_X12, 140 seL4_TimeoutReply_X13, 141 seL4_TimeoutReply_X14, 142 seL4_TimeoutReply_X15, 143 seL4_TimeoutReply_X19, 144 seL4_TimeoutReply_X20, 145 seL4_TimeoutReply_X21, 146 seL4_TimeoutReply_X22, 147 seL4_TimeoutReply_X23, 148 seL4_TimeoutReply_X24, 149 seL4_TimeoutReply_X25, 150 seL4_TimeoutReply_X26, 151 seL4_TimeoutReply_X27, 152 seL4_TimeoutReply_X28, 153 seL4_TimeoutReply_Length, 154 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 155} seL4_TimeoutReply_Msg; 156 157enum { 158 seL4_Timeout_Data, 159 seL4_Timeout_Consumed, 160 seL4_Timeout_Length, 161 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg) 162} seL4_TimeoutMsg; 163 164#endif /* !__ASSEMBLER__ */ 165 166#define seL4_DataFault 0 167#define seL4_InstructionFault 1 168/* object sizes - 2^n */ 169#define seL4_PageBits 12 170#define seL4_LargePageBits 21 171#define seL4_HugePageBits 30 172#define seL4_SlotBits 5 173#define seL4_TCBBits 11 174#define seL4_EndpointBits 4 175#define seL4_NotificationBits 6 176#define seL4_SchedContextBits 8 177#define seL4_ReplyBits 5 178 179#define seL4_PageTableBits 12 180#define seL4_PageTableEntryBits 3 181#define seL4_PageTableIndexBits 9 182 183#define seL4_PageDirBits 12 184#define seL4_PageDirEntryBits 3 185#define seL4_PageDirIndexBits 9 186 187#define seL4_ASIDPoolBits 12 188#define seL4_ASIDPoolIndexBits 9 189#define seL4_IOPageTableBits 12 190#define seL4_WordSizeBits 3 191 192#define seL4_PGDBits 12 193#define seL4_PGDEntryBits 3 194#define seL4_PGDIndexBits 9 195 196#define seL4_PUDBits 12 197#define seL4_PUDEntryBits 3 198#define seL4_PUDIndexBits 9 199 200#define seL4_ARM_VCPUBits 12 201#define seL4_VCPUBits 12 202 203/* word size */ 204#define seL4_WordBits (sizeof(seL4_Word) * 8) 205 206/* Untyped size limits */ 207#define seL4_MinUntypedBits 4 208#define seL4_MaxUntypedBits 47 209 210#ifndef __ASSEMBLER__ 211SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 212SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 213SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 214SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits); 215SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits); 216#endif 217 218#ifdef CONFIG_ENABLE_BENCHMARKS 219/* size of kernel log buffer in bytes */ 220#define seL4_LogBufferSize (LIBSEL4_BIT(20)) 221#endif /* CONFIG_ENABLE_BENCHMARKS */ 222 223#ifdef CONFIG_HARDWARE_DEBUG_API 224#define seL4_FirstBreakpoint (0) 225#define seL4_FirstDualFunctionMonitor (-1) 226#define seL4_NumDualFunctionMonitors (0) 227#endif 228 229#define seL4_FastMessageRegisters 4 230 231/* IPC buffer is 1024 bytes, giving size bits of 10 */ 232#define seL4_IPCBufferSizeBits 10 233 234#endif 235