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