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#ifdef HAVE_AUTOCONF
10#include <autoconf.h>
11#endif
12
13#define TLS_GDT_ENTRY 6
14#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)
15
16#define IPCBUF_GDT_ENTRY 7
17#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3)
18
19#define seL4_DataFault 0
20#define seL4_InstructionFault 1
21
22#define seL4_PageBits        12 /* 4K */
23#define seL4_SlotBits         4
24#define seL4_TCBBits         11
25#define seL4_EndpointBits     4
26#ifdef CONFIG_KERNEL_MCS
27#define seL4_NotificationBits 5
28#define seL4_ReplyBits        4
29#else
30#define seL4_NotificationBits 4
31#endif
32
33#define seL4_PageTableBits   12
34#define seL4_PageTableEntryBits 2
35#define seL4_PageTableIndexBits 10
36
37#define seL4_PageDirBits     12
38#define seL4_PageDirEntryBits 2
39#define seL4_PageDirIndexBits 10
40#define seL4_VSpaceBits seL4_PageDirBits
41
42#define seL4_IOPageTableBits 12
43#define seL4_NumASIDPoolsBits 2
44#define seL4_ASIDPoolBits    12
45#define seL4_ASIDPoolIndexBits 10
46#define seL4_WordSizeBits 2
47
48#define seL4_HugePageBits    30 /* 1GB */
49#define seL4_PDPTBits         0
50#define seL4_LargePageBits    22 /* 4MB */
51
52#ifndef __ASSEMBLER__
53SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
54SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
55SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
56#endif
57
58/* Previously large frames were explicitly assumed to be 4M. If not using
59 * PAE assuming a legacy environment and leave the old definition */
60#define seL4_4MBits           seL4_LargePageBits
61
62#define seL4_WordBits (sizeof(seL4_Word) * 8)
63
64/* Untyped size limits */
65#define seL4_MinUntypedBits 4
66#define seL4_MaxUntypedBits 29
67
68#ifdef CONFIG_ENABLE_BENCHMARKS
69/* size of kernel log buffer in bytes */
70#define seL4_LogBufferSize (LIBSEL4_BIT(20))
71#endif /* CONFIG_ENABLE_BENCHMARKS */
72
73#ifndef __ASSEMBLER__
74/* format of a vm fault message */
75typedef 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
84typedef enum {
85    seL4_UnknownSyscall_EAX,
86    seL4_UnknownSyscall_EBX,
87    seL4_UnknownSyscall_ECX,
88    seL4_UnknownSyscall_EDX,
89    seL4_UnknownSyscall_ESI,
90    seL4_UnknownSyscall_EDI,
91    seL4_UnknownSyscall_EBP,
92    seL4_UnknownSyscall_FaultIP,
93    seL4_UnknownSyscall_SP,
94    seL4_UnknownSyscall_FLAGS,
95    seL4_UnknownSyscall_Syscall,
96    seL4_UnknownSyscall_Length,
97    SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
98} seL4_UnknownSyscall_Msg;
99
100typedef enum {
101    seL4_UserException_FaultIP,
102    seL4_UserException_SP,
103    seL4_UserException_FLAGS,
104    seL4_UserException_Number,
105    seL4_UserException_Code,
106    seL4_UserException_Length,
107    SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
108} seL4_UserException_Msg;
109
110#ifdef CONFIG_KERNEL_MCS
111typedef enum {
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
120typedef enum {
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_FS_BASE,
132    seL4_TimeoutReply_GS_BASE,
133    seL4_TimeoutReply_Length,
134    SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
135} seL4_TimeoutReply_Msg;
136#endif
137#endif /* __ASSEMBLER__ */
138#ifdef CONFIG_KERNEL_MCS
139#define seL4_FastMessageRegisters 1
140#else
141#define seL4_FastMessageRegisters 2
142#endif
143
144/* IPC buffer is 512 bytes, giving size bits of 9 */
145#define seL4_IPCBufferSizeBits 9
146
147/* First address in the virtual address space that is not accessible to user level */
148#define seL4_UserTop 0xe0000000
149