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#define TLS_GDT_ENTRY 6 21#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3) 22 23#define IPCBUF_GDT_ENTRY 7 24#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3) 25 26#define seL4_DataFault 0 27#define seL4_InstructionFault 1 28 29#define seL4_PageBits 12 /* 4K */ 30#define seL4_SlotBits 4 31#define seL4_TCBBits 11 32#define seL4_EndpointBits 4 33#define seL4_NotificationBits 5 34 35#define seL4_PageTableBits 12 36#define seL4_PageTableEntryBits 2 37#define seL4_PageTableIndexBits 10 38 39#define seL4_PageDirBits 12 40#define seL4_PageDirEntryBits 2 41#define seL4_PageDirIndexBits 10 42 43#define seL4_IOPageTableBits 12 44#define seL4_ASIDPoolBits 12 45#define seL4_ASIDPoolIndexBits 10 46#define seL4_WordSizeBits 2 47#define seL4_ReplyBits 4 48 49#define seL4_HugePageBits 30 /* 1GB */ 50#define seL4_PDPTBits 0 51#define seL4_LargePageBits 22 /* 4MB */ 52 53#ifndef __ASSEMBLER__ 54SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits); 55SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits); 56SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits); 57#endif 58 59/* Previously large frames were explicitly assumed to be 4M. If not using 60 * PAE assuming a legacy environment and leave the old definition */ 61#define seL4_4MBits seL4_LargePageBits 62 63#define seL4_WordBits (sizeof(seL4_Word) * 8) 64 65/* Untyped size limits */ 66#define seL4_MinUntypedBits 4 67#define seL4_MaxUntypedBits 29 68 69#ifdef CONFIG_ENABLE_BENCHMARKS 70/* size of kernel log buffer in bytes */ 71#define seL4_LogBufferSize (LIBSEL4_BIT(20)) 72#endif /* CONFIG_ENABLE_BENCHMARKS */ 73 74#ifndef __ASSEMBLER__ 75/* format of a vm fault message */ 76enum { 77 seL4_VMFault_IP, 78 seL4_VMFault_Addr, 79 seL4_VMFault_PrefetchFault, 80 seL4_VMFault_FSR, 81 seL4_VMFault_Length, 82 SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg), 83} seL4_VMFault_Msg; 84 85enum { 86 seL4_UnknownSyscall_EAX, 87 seL4_UnknownSyscall_EBX, 88 seL4_UnknownSyscall_ECX, 89 seL4_UnknownSyscall_EDX, 90 seL4_UnknownSyscall_ESI, 91 seL4_UnknownSyscall_EDI, 92 seL4_UnknownSyscall_EBP, 93 seL4_UnknownSyscall_FaultIP, 94 seL4_UnknownSyscall_SP, 95 seL4_UnknownSyscall_FLAGS, 96 seL4_UnknownSyscall_Syscall, 97 seL4_UnknownSyscall_Length, 98 SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg), 99} seL4_UnknownSyscall_Msg; 100 101enum { 102 seL4_UserException_FaultIP, 103 seL4_UserException_SP, 104 seL4_UserException_FLAGS, 105 seL4_UserException_Number, 106 seL4_UserException_Code, 107 seL4_UserException_Length, 108 SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg) 109} seL4_UserException_Msg; 110 111enum { 112 seL4_Timeout_Data, 113 /* consumed is 64 bits */ 114 seL4_Timeout_Consumed_HighBits, 115 seL4_Timeout_Consumed_LowBits, 116 seL4_Timeout_Length, 117 SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg), 118} seL4_Timeout_Msg; 119 120enum { 121 seL4_TimeoutReply_FaultIP, 122 seL4_TimeoutReply_SP, 123 seL4_TimeoutReply_FLAGS, 124 seL4_TimeoutReply_EAX, 125 seL4_TimeoutReply_EBX, 126 seL4_TimeoutReply_ECX, 127 seL4_TimeoutReply_EDX, 128 seL4_TimeoutReply_ESI, 129 seL4_TimeoutReply_EDI, 130 seL4_TimeoutReply_EBP, 131 seL4_TimeoutReply_TLS_BASE, 132 seL4_TimeoutReply_FS, 133 seL4_TimeoutReply_GS, 134 seL4_TimeoutReply_Length, 135 SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg) 136} seL4_TimeoutReply_Msg; 137 138#endif /* __ASSEMBLER__ */ 139#define seL4_FastMessageRegisters 1 140 141/* IPC buffer is 512 bytes, giving size bits of 9 */ 142#define seL4_IPCBufferSizeBits 9 143 144#endif 145