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 14 /* format of an unknown syscall message */ 15 typedef enum { 16 seL4_UnknownSyscall_R0, 17 seL4_UnknownSyscall_R1, 18 seL4_UnknownSyscall_R2, 19 seL4_UnknownSyscall_R3, 20 seL4_UnknownSyscall_R4, 21 seL4_UnknownSyscall_R5, 22 seL4_UnknownSyscall_R6, 23 seL4_UnknownSyscall_R7, 24 seL4_UnknownSyscall_FaultIP, 25 seL4_UnknownSyscall_SP, 26 seL4_UnknownSyscall_LR, 27 seL4_UnknownSyscall_CPSR, 28 seL4_UnknownSyscall_Syscall, 29 /* length of an unknown syscall message */ 30 seL4_UnknownSyscall_Length, 31 SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg), 32 } seL4_UnknownSyscall_Msg; 33 34 /* format of a user exception message */ 35 typedef enum { 36 seL4_UserException_FaultIP, 37 seL4_UserException_SP, 38 seL4_UserException_CPSR, 39 seL4_UserException_Number, 40 seL4_UserException_Code, 41 /* length of a user exception */ 42 seL4_UserException_Length, 43 SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg), 44 } seL4_UserException_Msg; 45 46 /* format of a vm fault message */ 47 typedef enum { 48 seL4_VMFault_IP, 49 seL4_VMFault_Addr, 50 seL4_VMFault_PrefetchFault, 51 seL4_VMFault_FSR, 52 seL4_VMFault_Length, 53 SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg), 54 } seL4_VMFault_Msg; 55 56 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 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 typedef enum { 69 seL4_VCPUFault_HSR, 70 seL4_VCPUFault_Length, 71 SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg), 72 } seL4_VCPUFault_Msg; 73 74 typedef enum { 75 seL4_VCPUReg_SCTLR = 0, 76 seL4_VCPUReg_ACTLR, 77 seL4_VCPUReg_TTBCR, 78 seL4_VCPUReg_TTBR0, 79 seL4_VCPUReg_TTBR1, 80 seL4_VCPUReg_DACR, 81 seL4_VCPUReg_DFSR, 82 seL4_VCPUReg_IFSR, 83 seL4_VCPUReg_ADFSR, 84 seL4_VCPUReg_AIFSR, 85 seL4_VCPUReg_DFAR, 86 seL4_VCPUReg_IFAR, 87 seL4_VCPUReg_PRRR, 88 seL4_VCPUReg_NMRR, 89 seL4_VCPUReg_CIDR, 90 seL4_VCPUReg_TPIDRPRW, 91 seL4_VCPUReg_FPEXC, 92 seL4_VCPUReg_LRsvc, 93 seL4_VCPUReg_SPsvc, 94 seL4_VCPUReg_LRabt, 95 seL4_VCPUReg_SPabt, 96 seL4_VCPUReg_LRund, 97 seL4_VCPUReg_SPund, 98 seL4_VCPUReg_LRirq, 99 seL4_VCPUReg_SPirq, 100 seL4_VCPUReg_LRfiq, 101 seL4_VCPUReg_SPfiq, 102 seL4_VCPUReg_R8fiq, 103 seL4_VCPUReg_R9fiq, 104 seL4_VCPUReg_R10fiq, 105 seL4_VCPUReg_R11fiq, 106 seL4_VCPUReg_R12fiq, 107 #if CONFIG_MAX_NUM_NODES > 1 108 seL4_VCPUReg_VMPIDR, 109 #endif /* CONFIG_MAX_NUM_NODES > 1 */ 110 seL4_VCPUReg_SPSRsvc, 111 seL4_VCPUReg_SPSRabt, 112 seL4_VCPUReg_SPSRund, 113 seL4_VCPUReg_SPSRirq, 114 seL4_VCPUReg_SPSRfiq, 115 seL4_VCPUReg_CNTV_CTL, 116 seL4_VCPUReg_CNTV_CVALhigh, 117 seL4_VCPUReg_CNTV_CVALlow, 118 seL4_VCPUReg_CNTVOFFhigh, 119 seL4_VCPUReg_CNTVOFFlow, 120 seL4_VCPUReg_Num, 121 } seL4_VCPUReg; 122 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 123 124 #ifdef CONFIG_KERNEL_MCS 125 typedef enum { 126 seL4_Timeout_Data, 127 /* consumed is 64 bits */ 128 seL4_Timeout_Consumed_HighBits, 129 seL4_Timeout_Consumed_LowBits, 130 seL4_Timeout_Length, 131 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg) 132 } seL4_TimeoutMsg; 133 134 typedef enum { 135 seL4_TimeoutReply_FaultIP, 136 seL4_TimeoutReply_SP, 137 seL4_TimeoutReply_CPSR, 138 seL4_TimeoutReply_R0, 139 seL4_TimeoutReply_R1, 140 seL4_TimeoutReply_R8, 141 seL4_TimeoutReply_R9, 142 seL4_TimeoutReply_R10, 143 seL4_TimeoutReply_R11, 144 seL4_TimeoutReply_R12, 145 seL4_TimeoutReply_R2, 146 seL4_TimeoutReply_R3, 147 seL4_TimeoutReply_R4, 148 seL4_TimeoutReply_R5, 149 seL4_TimeoutReply_R6, 150 seL4_TimeoutReply_R7, 151 seL4_TimeoutReply_R14, 152 seL4_TimeoutReply_Length, 153 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 154 } seL4_TimeoutReply_Msg; 155 #endif /* CONFIG_KERNEL_MCS */ 156 #endif /* !__ASSEMBLER__ */ 157 158 #define seL4_DataFault 0 159 #define seL4_InstructionFault 1 160 /* object sizes - 2^n */ 161 #define seL4_PageBits 12 162 #define seL4_LargePageBits 16 163 #define seL4_SlotBits 4 164 165 #if ( \ 166 defined(CONFIG_HAVE_FPU) && ( \ 167 (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE)) || \ 168 defined(CONFIG_HARDWARE_DEBUG_API) \ 169 ) \ 170 ) 171 #define seL4_TCBBits 11 172 #elif ( \ 173 defined(CONFIG_HAVE_FPU) || \ 174 (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE)) || \ 175 defined(CONFIG_HARDWARE_DEBUG_API) \ 176 ) 177 #define seL4_TCBBits 10 178 #else 179 #define seL4_TCBBits 9 180 #endif 181 182 #define seL4_EndpointBits 4 183 #ifdef CONFIG_KERNEL_MCS 184 #define seL4_NotificationBits 5 185 #define seL4_ReplyBits 4 186 #else 187 #define seL4_NotificationBits 4 188 #endif 189 190 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 191 #define seL4_PageTableBits 12 192 #define seL4_PageTableEntryBits 3 193 #define seL4_PageTableIndexBits 9 194 #define seL4_SectionBits 21 195 #define seL4_SuperSectionBits 25 196 #define seL4_PageDirEntryBits 3 197 #define seL4_PageDirIndexBits 11 198 #define seL4_VCPUBits 12 199 #else 200 #define seL4_PageTableBits 10 201 #define seL4_PageTableEntryBits 2 202 #define seL4_PageTableIndexBits 8 203 #define seL4_SectionBits 20 204 #define seL4_SuperSectionBits 24 205 #define seL4_PageDirEntryBits 2 206 #define seL4_PageDirIndexBits 12 207 #endif 208 209 #define seL4_PageDirBits 14 210 #define seL4_VSpaceBits seL4_PageDirBits 211 212 #ifdef CONFIG_TK1_SMMU 213 #define seL4_NumASIDPoolsBits 6 214 #else 215 #define seL4_NumASIDPoolsBits 7 216 #endif 217 #define seL4_ASIDPoolBits 12 218 #define seL4_ASIDPoolIndexBits 10 219 #define seL4_ARM_VCPUBits 12 220 #define seL4_IOPageTableBits 12 221 222 /* bits in a word */ 223 #define seL4_WordBits (sizeof(seL4_Word) * 8) 224 /* log 2 bits in a word */ 225 #define seL4_WordSizeBits 2 226 227 #ifndef __ASSEMBLER__ 228 SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 229 SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 230 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 231 #ifdef seL4_PGDBits 232 SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits); 233 #endif 234 #endif 235 236 /* Untyped size limits */ 237 #define seL4_MinUntypedBits 4 238 #define seL4_MaxUntypedBits 29 239 240 #ifdef CONFIG_ENABLE_BENCHMARKS 241 /* size of kernel log buffer in bytes */ 242 #define seL4_LogBufferSize (LIBSEL4_BIT(20)) 243 #endif /* CONFIG_ENABLE_BENCHMARKS */ 244 245 #ifdef CONFIG_HARDWARE_DEBUG_API 246 #define seL4_FirstBreakpoint (0) 247 #define seL4_FirstDualFunctionMonitor (-1) 248 #define seL4_NumDualFunctionMonitors (0) 249 #endif 250 251 #define seL4_FastMessageRegisters 4 252 253 /* IPC buffer is 512 bytes, giving size bits of 9 */ 254 #define seL4_IPCBufferSizeBits 9 255