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#include <autoconf.h> 10 11#define TLS_GDT_ENTRY 7 12#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3) 13 14#define IPCBUF_GDT_ENTRY 8 15#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3) 16 17#define seL4_DataFault 0 18#define seL4_InstructionFault 1 19 20/* for x86-64, the large page size is 2 MiB and huge page size is 1 GiB */ 21#define seL4_WordBits 64 22#define seL4_WordSizeBits 3 23#define seL4_PageBits 12 24#define seL4_SlotBits 5 25#if CONFIG_XSAVE_SIZE >= 832 26#define seL4_TCBBits 12 27#else 28#define seL4_TCBBits 11 29#endif 30#define seL4_EndpointBits 4 31#ifdef CONFIG_KERNEL_MCS 32#define seL4_NotificationBits 6 33#define seL4_ReplyBits 5 34#else 35#define seL4_NotificationBits 5 36#endif 37 38#define seL4_PageTableBits 12 39#define seL4_PageTableEntryBits 3 40#define seL4_PageTableIndexBits 9 41 42#define seL4_PageDirBits 12 43#define seL4_PageDirEntryBits 3 44#define seL4_PageDirIndexBits 9 45 46#define seL4_PDPTBits 12 47#define seL4_PDPTEntryBits 3 48#define seL4_PDPTIndexBits 9 49 50#define seL4_PML4Bits 12 51#define seL4_PML4EntryBits 3 52#define seL4_PML4IndexBits 9 53#define seL4_VSpaceBits seL4_PML4Bits 54 55#define seL4_IOPageTableBits 12 56#define seL4_LargePageBits 21 57#define seL4_HugePageBits 30 58#define seL4_NumASIDPoolsBits 3 59#define seL4_ASIDPoolBits 12 60#define seL4_ASIDPoolIndexBits 9 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 74typedef enum { 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 83typedef enum { 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 107typedef enum { 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 117#ifdef CONFIG_KERNEL_MCS 118typedef enum { 119 seL4_Timeout_Data, 120 seL4_Timeout_Consumed, 121 seL4_Timeout_Length, 122 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg) 123} seL4_TimeoutMsg; 124 125typedef enum { 126 seL4_TimeoutReply_FaultIP, 127 seL4_TimeoutReply_RSP, 128 seL4_TimeoutReply_FLAGS, 129 seL4_TimeoutReply_RAX, 130 seL4_TimeoutReply_RBX, 131 seL4_TimeoutReply_RCX, 132 seL4_TimeoutReply_RDX, 133 seL4_TimeoutReply_RSI, 134 seL4_TimeoutReply_RDI, 135 seL4_TimeoutReply_RBP, 136 seL4_TimeoutReply_R8, 137 seL4_TimeoutReply_R9, 138 seL4_TimeoutReply_R10, 139 seL4_TimeoutReply_R11, 140 seL4_TimeoutReply_R12, 141 seL4_TimeoutReply_R13, 142 seL4_TimeoutReply_R14, 143 seL4_TimeoutReply_R15, 144 seL4_TimeoutReply_TLS_BASE, 145 seL4_TimeoutReply_Length, 146 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 147} seL4_TimeoutReply_Msg; 148#endif 149#endif /* __ASSEMBLER__ */ 150#define seL4_FastMessageRegisters 4 151 152/* IPC buffer is 1024 bytes, giving size bits of 10 */ 153#define seL4_IPCBufferSizeBits 10 154 155/* First address in the virtual address space that is not accessible to user level */ 156#define seL4_UserTop 0x00007ffffffff000 157 158