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