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 125#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 126#endif /* !__ASSEMBLER__ */ 127 128#define seL4_DataFault 0 129#define seL4_InstructionFault 1 130/* object sizes - 2^n */ 131#define seL4_PageBits 12 132#define seL4_LargePageBits 16 133#define seL4_SlotBits 4 134 135#if ((defined(CONFIG_DEBUG_BUILD) || CONFIG_MAX_NUM_NODES > 1) && defined(CONFIG_HAVE_FPU) && defined(CONFIG_HARDWARE_DEBUG_API)) \ 136 || (defined(CONFIG_HAVE_FPU) && defined(CONFIG_ARM_HYPERVISOR_SUPPORT)) 137#define seL4_TCBBits 11 138#elif defined(CONFIG_HAVE_FPU) 139#define seL4_TCBBits 10 140#else 141#define seL4_TCBBits 9 142#endif 143 144#define seL4_EndpointBits 4 145#define seL4_NotificationBits 4 146 147#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 148#define seL4_PageTableBits 12 149#define seL4_PageTableEntryBits 3 150#define seL4_PageTableIndexBits 9 151#define seL4_SectionBits 21 152#define seL4_SuperSectionBits 25 153#define seL4_PGDEntryBits 3 154#define seL4_PGDIndexBits 2 155#define seL4_PGDBits (seL4_PGDIndexBits + seL4_PGDEntryBits) 156#define seL4_PageDirEntryBits 3 157#define seL4_PageDirIndexBits 11 158#define seL4_VCPUBits 12 159#else 160#define seL4_PageTableBits 10 161#define seL4_PageTableEntryBits 2 162#define seL4_PageTableIndexBits 8 163#define seL4_SectionBits 20 164#define seL4_SuperSectionBits 24 165#define seL4_PageDirEntryBits 2 166#define seL4_PageDirIndexBits 12 167#endif 168 169#define seL4_PageDirBits 14 170 171#define seL4_ASIDPoolBits 12 172#define seL4_ASIDPoolIndexBits 10 173#define seL4_ARM_VCPUBits 12 174#define seL4_IOPageTableBits 12 175 176/* bits in a word */ 177#define seL4_WordBits (sizeof(seL4_Word) * 8) 178/* log 2 bits in a word */ 179#define seL4_WordSizeBits 2 180 181#ifndef __ASSEMBLER__ 182SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 183SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 184SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 185#endif 186 187/* Untyped size limits */ 188#define seL4_MinUntypedBits 4 189#define seL4_MaxUntypedBits 29 190 191#ifdef CONFIG_ENABLE_BENCHMARKS 192/* size of kernel log buffer in bytes */ 193#define seL4_LogBufferSize (LIBSEL4_BIT(20)) 194#endif /* CONFIG_ENABLE_BENCHMARKS */ 195 196#ifdef CONFIG_HARDWARE_DEBUG_API 197#define seL4_FirstBreakpoint (0) 198#define seL4_FirstDualFunctionMonitor (-1) 199#define seL4_NumDualFunctionMonitors (0) 200#endif 201 202#define seL4_FastMessageRegisters 4 203 204/* IPC buffer is 512 bytes, giving size bits of 9 */ 205#define seL4_IPCBufferSizeBits 9 206 207#endif 208