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 5 39 40#define seL4_PageTableBits 12 41#define seL4_PageTableEntryBits 3 42#define seL4_PageTableIndexBits 9 43 44#define seL4_PageDirBits 12 45#define seL4_PageDirEntryBits 3 46#define seL4_PageDirIndexBits 9 47 48#define seL4_PDPTBits 12 49#define seL4_PDPTEntryBits 3 50#define seL4_PDPTIndexBits 9 51 52#define seL4_PML4Bits 12 53#define seL4_PML4EntryBits 3 54#define seL4_PML4IndexBits 9 55 56#define seL4_IOPageTableBits 12 57#define seL4_LargePageBits 21 58#define seL4_HugePageBits 30 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 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 117#endif /* __ASSEMBLER__ */ 118#define seL4_FastMessageRegisters 4 119 120/* IPC buffer is 1024 bytes, giving size bits of 10 */ 121#define seL4_IPCBufferSizeBits 10 122 123#endif /* __LIBSEL4_SEL4_SEL4_ARCH_CONSTANTS_H_ */ 124