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