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