1 /* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7 #pragma once 8 9 #include <autoconf.h> 10 #include <sel4/macros.h> 11 12 #ifndef __ASSEMBLER__ 13 /* format of an unknown syscall message */ 14 typedef enum { 15 seL4_UnknownSyscall_X0, 16 seL4_UnknownSyscall_X1, 17 seL4_UnknownSyscall_X2, 18 seL4_UnknownSyscall_X3, 19 seL4_UnknownSyscall_X4, 20 seL4_UnknownSyscall_X5, 21 seL4_UnknownSyscall_X6, 22 seL4_UnknownSyscall_X7, 23 seL4_UnknownSyscall_FaultIP, 24 seL4_UnknownSyscall_SP, 25 seL4_UnknownSyscall_LR, 26 seL4_UnknownSyscall_SPSR, 27 seL4_UnknownSyscall_Syscall, 28 /* length of an unknown syscall message */ 29 seL4_UnknownSyscall_Length, 30 SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg), 31 } seL4_UnknownSyscall_Msg; 32 33 /* format of a user exception message */ 34 typedef enum { 35 seL4_UserException_FaultIP, 36 seL4_UserException_SP, 37 seL4_UserException_SPSR, 38 seL4_UserException_Number, 39 seL4_UserException_Code, 40 /* length of a user exception */ 41 seL4_UserException_Length, 42 SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg), 43 } seL4_UserException_Msg; 44 45 /* format of a vm fault message */ 46 typedef enum { 47 seL4_VMFault_IP, 48 seL4_VMFault_Addr, 49 seL4_VMFault_PrefetchFault, 50 seL4_VMFault_FSR, 51 seL4_VMFault_Length, 52 SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg), 53 } seL4_VMFault_Msg; 54 55 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 56 57 typedef enum { 58 seL4_VGICMaintenance_IDX, 59 seL4_VGICMaintenance_Length, 60 SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg), 61 } seL4_VGICMaintenance_Msg; 62 63 typedef enum { 64 seL4_VPPIEvent_IRQ, 65 SEL4_FORCE_LONG_ENUM(seL4_VPPIEvent_Msg), 66 } seL4_VPPIEvent_Msg; 67 68 69 typedef enum { 70 seL4_VCPUFault_HSR, 71 seL4_VCPUFault_Length, 72 SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg), 73 } seL4_VCPUFault_Msg; 74 75 typedef enum { 76 /* VM control registers EL1 */ 77 seL4_VCPUReg_SCTLR = 0, 78 seL4_VCPUReg_TTBR0, 79 seL4_VCPUReg_TTBR1, 80 seL4_VCPUReg_TCR, 81 seL4_VCPUReg_MAIR, 82 seL4_VCPUReg_AMAIR, 83 seL4_VCPUReg_CIDR, 84 85 /* other system registers EL1 */ 86 seL4_VCPUReg_ACTLR, 87 seL4_VCPUReg_CPACR, 88 89 /* exception handling registers EL1 */ 90 seL4_VCPUReg_AFSR0, 91 seL4_VCPUReg_AFSR1, 92 seL4_VCPUReg_ESR, 93 seL4_VCPUReg_FAR, 94 seL4_VCPUReg_ISR, 95 seL4_VCPUReg_VBAR, 96 97 /* thread pointer/ID registers EL0/EL1 */ 98 seL4_VCPUReg_TPIDR_EL1, 99 100 #if CONFIG_MAX_NUM_NODES > 1 101 /* Virtualisation Multiprocessor ID Register */ 102 seL4_VCPUReg_VMPIDR_EL2, 103 #endif /* CONFIG_MAX_NUM_NODES > 1 */ 104 105 /* general registers x0 to x30 have been saved by traps.S */ 106 seL4_VCPUReg_SP_EL1, 107 seL4_VCPUReg_ELR_EL1, 108 seL4_VCPUReg_SPSR_EL1, // 32-bit 109 110 /* generic timer registers, to be completed */ 111 seL4_VCPUReg_CNTV_CTL, 112 seL4_VCPUReg_CNTV_CVAL, 113 seL4_VCPUReg_CNTVOFF, 114 seL4_VCPUReg_CNTKCTL_EL1, 115 116 seL4_VCPUReg_Num, 117 } seL4_VCPUReg; 118 119 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 120 121 #ifdef CONFIG_KERNEL_MCS 122 typedef enum { 123 seL4_TimeoutReply_FaultIP, 124 seL4_TimeoutReply_SP, 125 seL4_TimeoutReply_SPSR_EL1, 126 seL4_TimeoutReply_X0, 127 seL4_TimeoutReply_X1, 128 seL4_TimeoutReply_X2, 129 seL4_TimeoutReply_X3, 130 seL4_TimeoutReply_X4, 131 seL4_TimeoutReply_X5, 132 seL4_TimeoutReply_X6, 133 seL4_TimeoutReply_X7, 134 seL4_TimeoutReply_X8, 135 seL4_TimeoutReply_X16, 136 seL4_TimeoutReply_X17, 137 seL4_TimeoutReply_X18, 138 seL4_TimeoutReply_X29, 139 seL4_TimeoutReply_X30, 140 seL4_TimeoutReply_X9, 141 seL4_TimeoutReply_X10, 142 seL4_TimeoutReply_X11, 143 seL4_TimeoutReply_X12, 144 seL4_TimeoutReply_X13, 145 seL4_TimeoutReply_X14, 146 seL4_TimeoutReply_X15, 147 seL4_TimeoutReply_X19, 148 seL4_TimeoutReply_X20, 149 seL4_TimeoutReply_X21, 150 seL4_TimeoutReply_X22, 151 seL4_TimeoutReply_X23, 152 seL4_TimeoutReply_X24, 153 seL4_TimeoutReply_X25, 154 seL4_TimeoutReply_X26, 155 seL4_TimeoutReply_X27, 156 seL4_TimeoutReply_X28, 157 seL4_TimeoutReply_Length, 158 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 159 } seL4_TimeoutReply_Msg; 160 161 typedef enum { 162 seL4_Timeout_Data, 163 seL4_Timeout_Consumed, 164 seL4_Timeout_Length, 165 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg) 166 } seL4_TimeoutMsg; 167 #endif 168 #endif /* !__ASSEMBLER__ */ 169 170 #define seL4_DataFault 0 171 #define seL4_InstructionFault 1 172 /* object sizes - 2^n */ 173 #define seL4_PageBits 12 174 #define seL4_LargePageBits 21 175 #define seL4_HugePageBits 30 176 #define seL4_SlotBits 5 177 #define seL4_TCBBits 11 178 #define seL4_EndpointBits 4 179 #ifdef CONFIG_KERNEL_MCS 180 #define seL4_NotificationBits 6 181 #define seL4_ReplyBits 5 182 #else 183 #define seL4_NotificationBits 5 184 #endif 185 186 #define seL4_PageTableBits 12 187 #define seL4_PageTableEntryBits 3 188 #define seL4_PageTableIndexBits 9 189 190 #define seL4_PageDirBits 12 191 #define seL4_PageDirEntryBits 3 192 #define seL4_PageDirIndexBits 9 193 194 #define seL4_NumASIDPoolsBits 7 195 #define seL4_ASIDPoolBits 12 196 #define seL4_ASIDPoolIndexBits 9 197 #define seL4_IOPageTableBits 12 198 #define seL4_WordSizeBits 3 199 200 #define seL4_PUDEntryBits 3 201 202 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40) 203 /* for a 3 level translation, we skip the PGD */ 204 #define seL4_PGDBits 0 205 #define seL4_PGDEntryBits 0 206 #define seL4_PGDIndexBits 0 207 208 #define seL4_PUDBits 13 209 #define seL4_PUDIndexBits 10 210 211 #define seL4_VSpaceBits seL4_PUDBits 212 #define seL4_VSpaceIndexBits seL4_PUDIndexBits 213 #define seL4_ARM_VSpaceObject seL4_ARM_PageUpperDirectoryObject 214 #else 215 #define seL4_PGDBits 12 216 #define seL4_PGDEntryBits 3 217 #define seL4_PGDIndexBits 9 218 219 #define seL4_PUDBits 12 220 #define seL4_PUDIndexBits 9 221 222 #define seL4_VSpaceBits seL4_PGDBits 223 #define seL4_VSpaceIndexBits seL4_PGDIndexBits 224 #define seL4_ARM_VSpaceObject seL4_ARM_PageGlobalDirectoryObject 225 #endif 226 227 #define seL4_ARM_VCPUBits 12 228 #define seL4_VCPUBits 12 229 230 /* word size */ 231 #define seL4_WordBits (sizeof(seL4_Word) * 8) 232 233 /* Untyped size limits */ 234 #define seL4_MinUntypedBits 4 235 #define seL4_MaxUntypedBits 47 236 237 #ifndef __ASSEMBLER__ 238 SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 239 SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 240 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 241 SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits); 242 SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits); 243 #endif 244 245 #ifdef CONFIG_ENABLE_BENCHMARKS 246 /* size of kernel log buffer in bytes */ 247 #define seL4_LogBufferSize (LIBSEL4_BIT(20)) 248 #endif /* CONFIG_ENABLE_BENCHMARKS */ 249 250 #ifdef CONFIG_HARDWARE_DEBUG_API 251 #define seL4_FirstBreakpoint (0) 252 #define seL4_FirstDualFunctionMonitor (-1) 253 #define seL4_NumDualFunctionMonitors (0) 254 #endif 255 256 #define seL4_FastMessageRegisters 4 257 258 /* IPC buffer is 1024 bytes, giving size bits of 10 */ 259 #define seL4_IPCBufferSizeBits 10 260 261 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 262 #ifndef CONFIG_ARM_SMMU 263 /* 1 slot at the end of the vspace is used to hold the VMID assigned to the vspace */ 264 #define seL4_VSpaceReservedSlots 1 265 #else /*CONFIG_ARM_SMMU*/ 266 /* 1 slot at the end of the vspace is used to hold the VMID assigned to the vspace */ 267 /* 1 slot at the end of the vspace is used to hold the number of SMMU CBs assigned to the vspace */ 268 #define seL4_VSpaceReservedSlots 2 269 #endif /*CONFIG_ARM_SMMU*/ 270 271 /* The userspace occupies the range 0x0 to 0xfffffffffff. 272 * The stage-1 translation is disabled, and the stage-2 273 * translation input addree size is constrained by the 274 * ID_AA64MMFR0_EL1.PARange which is 44 bits on TX1. 275 * Anything address above the range above triggers an 276 * address size fault. 277 */ 278 /* First address in the virtual address space that is not accessible to user level */ 279 #if defined(CONFIG_ARM_PA_SIZE_BITS_44) 280 #define seL4_UserTop 0x00000fffffffffff 281 #elif defined(CONFIG_ARM_PA_SIZE_BITS_40) 282 /* Currently other definitions of seL4_UserTop already have free slots at the end and don't need to subtract for seL4_VSpaceReservedSlots. 283 * Each slot used requires subtracting 1GiB from the top address. 284 */ 285 #define seL4_UserTop (0x000000ffffffffff - seL4_VSpaceReservedSlots * 0x40000000) 286 #else 287 #error "Unknown physical address width" 288 #endif 289 290 #else 291 /* First address in the virtual address space that is not accessible to user level */ 292 #define seL4_UserTop 0x00007fffffffffff 293 #endif 294