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