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