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_SEL4_ARCH_CONSTANTS_H_ 14#define __LIBSEL4_SEL4_SEL4_ARCH_CONSTANTS_H_ 15 16#include <autoconf.h> 17 18#define TLS_GDT_ENTRY 7 19#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3) 20 21#define IPCBUF_GDT_ENTRY 8 22#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3) 23 24#define seL4_DataFault 0 25#define seL4_InstructionFault 1 26 27/* for x86-64, the large page size is 2 MiB and huge page size is 1 GiB */ 28#define seL4_WordBits 64 29#define seL4_WordSizeBits 3 30#define seL4_PageBits 12 31#define seL4_SlotBits 5 32#if CONFIG_XSAVE_SIZE >= 832 33#define seL4_TCBBits 12 34#else 35#define seL4_TCBBits 11 36#endif 37#define seL4_EndpointBits 4 38#define seL4_NotificationBits 6 39#define seL4_PageTableBits 12 40#define seL4_PageTableEntryBits 3 41#define seL4_PageTableIndexBits 9 42 43#define seL4_PageDirBits 12 44#define seL4_PageDirEntryBits 3 45#define seL4_PageDirIndexBits 9 46 47#define seL4_PDPTBits 12 48#define seL4_PDPTEntryBits 3 49#define seL4_PDPTIndexBits 9 50 51#define seL4_PML4Bits 12 52#define seL4_PML4EntryBits 3 53#define seL4_PML4IndexBits 9 54 55#define seL4_IOPageTableBits 12 56#define seL4_LargePageBits 21 57#define seL4_HugePageBits 30 58#define seL4_ASIDPoolBits 12 59#define seL4_ASIDPoolIndexBits 9 60#define seL4_ReplyBits 5 61 62/* Untyped size limits */ 63#define seL4_MinUntypedBits 4 64#define seL4_MaxUntypedBits 47 65 66#ifndef __ASSEMBLER__ 67 68SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 69SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 70SEL4_SIZE_SANITY(seL4_PDPTEntryBits, seL4_PDPTIndexBits, seL4_PDPTBits); 71SEL4_SIZE_SANITY(seL4_PML4EntryBits, seL4_PML4IndexBits, seL4_PML4Bits); 72SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 73 74enum { 75 seL4_VMFault_IP, 76 seL4_VMFault_Addr, 77 seL4_VMFault_PrefetchFault, 78 seL4_VMFault_FSR, 79 seL4_VMFault_Length, 80 SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg), 81} seL4_VMFault_Msg; 82 83enum { 84 seL4_UnknownSyscall_RAX, 85 seL4_UnknownSyscall_RBX, 86 seL4_UnknownSyscall_RCX, 87 seL4_UnknownSyscall_RDX, 88 seL4_UnknownSyscall_RSI, 89 seL4_UnknownSyscall_RDI, 90 seL4_UnknownSyscall_RBP, 91 seL4_UnknownSyscall_R8, 92 seL4_UnknownSyscall_R9, 93 seL4_UnknownSyscall_R10, 94 seL4_UnknownSyscall_R11, 95 seL4_UnknownSyscall_R12, 96 seL4_UnknownSyscall_R13, 97 seL4_UnknownSyscall_R14, 98 seL4_UnknownSyscall_R15, 99 seL4_UnknownSyscall_FaultIP, 100 seL4_UnknownSyscall_SP, 101 seL4_UnknownSyscall_FLAGS, 102 seL4_UnknownSyscall_Syscall, 103 seL4_UnknownSyscall_Length, 104 SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg) 105} seL4_UnknownSyscall_Msg; 106 107enum { 108 seL4_UserException_FaultIP, 109 seL4_UserException_SP, 110 seL4_UserException_FLAGS, 111 seL4_UserException_Number, 112 seL4_UserException_Code, 113 seL4_UserException_Length, 114 SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg) 115} seL4_UserException_Msg; 116 117enum { 118 seL4_Timeout_Data, 119 seL4_Timeout_Consumed, 120 seL4_Timeout_Length, 121 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg) 122} seL4_TimeoutMsg; 123 124enum { 125 seL4_TimeoutReply_FaultIP, 126 seL4_TimeoutReply_RSP, 127 seL4_TimeoutReply_FLAGS, 128 seL4_TimeoutReply_RAX, 129 seL4_TimeoutReply_RBX, 130 seL4_TimeoutReply_RCX, 131 seL4_TimeoutReply_RDX, 132 seL4_TimeoutReply_RSI, 133 seL4_TimeoutReply_RDI, 134 seL4_TimeoutReply_RBP, 135 seL4_TimeoutReply_R8, 136 seL4_TimeoutReply_R9, 137 seL4_TimeoutReply_R10, 138 seL4_TimeoutReply_R11, 139 seL4_TimeoutReply_R12, 140 seL4_TimeoutReply_R13, 141 seL4_TimeoutReply_R14, 142 seL4_TimeoutReply_R15, 143 seL4_TimeoutReply_TLS_BASE, 144 seL4_TimeoutReply_Length, 145 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 146} seL4_TimeoutReply_Msg; 147 148#endif /* __ASSEMBLER__ */ 149#define seL4_FastMessageRegisters 4 150 151/* IPC buffer is 1024 bytes, giving size bits of 10 */ 152#define seL4_IPCBufferSizeBits 10 153 154#endif /* __LIBSEL4_SEL4_SEL4_ARCH_CONSTANTS_H_ */ 155