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#ifndef __ASSEMBLER__
21/* format of an unknown syscall message */
22enum {
23    seL4_UnknownSyscall_X0,
24    seL4_UnknownSyscall_X1,
25    seL4_UnknownSyscall_X2,
26    seL4_UnknownSyscall_X3,
27    seL4_UnknownSyscall_X4,
28    seL4_UnknownSyscall_X5,
29    seL4_UnknownSyscall_X6,
30    seL4_UnknownSyscall_X7,
31    seL4_UnknownSyscall_FaultIP,
32    seL4_UnknownSyscall_SP,
33    seL4_UnknownSyscall_LR,
34    seL4_UnknownSyscall_SPSR,
35    seL4_UnknownSyscall_Syscall,
36    /* length of an unknown syscall message */
37    seL4_UnknownSyscall_Length,
38    SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
39} seL4_UnknownSyscall_Msg;
40
41/* format of a user exception message */
42enum {
43    seL4_UserException_FaultIP,
44    seL4_UserException_SP,
45    seL4_UserException_SPSR,
46    seL4_UserException_Number,
47    seL4_UserException_Code,
48    /* length of a user exception */
49    seL4_UserException_Length,
50    SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
51} seL4_UserException_Msg;
52
53/* format of a vm fault message */
54enum {
55    seL4_VMFault_IP,
56    seL4_VMFault_Addr,
57    seL4_VMFault_PrefetchFault,
58    seL4_VMFault_FSR,
59    seL4_VMFault_Length,
60    SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
61} seL4_VMFault_Msg;
62
63#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
64
65enum {
66    seL4_VGICMaintenance_IDX,
67    seL4_VGICMaintenance_Length,
68    SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg),
69} seL4_VGICMaintenance_Msg;
70
71enum {
72    seL4_VCPUFault_HSR,
73    seL4_VCPUFault_Length,
74    SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg),
75} seL4_VCPUFault_Msg;
76
77enum {
78    /* VM control registers EL1 */
79    seL4_VCPUReg_SCTLR = 0,
80    seL4_VCPUReg_TTBR0,
81    seL4_VCPUReg_TTBR1,
82    seL4_VCPUReg_TCR,
83    seL4_VCPUReg_MAIR,
84    seL4_VCPUReg_AMAIR,
85    seL4_VCPUReg_CIDR,
86
87    /* other system registers EL1 */
88    seL4_VCPUReg_ACTLR,
89    seL4_VCPUReg_CPACR,
90
91    /* exception handling registers EL1 */
92    seL4_VCPUReg_AFSR0,
93    seL4_VCPUReg_AFSR1,
94    seL4_VCPUReg_ESR,
95    seL4_VCPUReg_FAR,
96    seL4_VCPUReg_ISR,
97    seL4_VCPUReg_VBAR,
98
99    /* thread pointer/ID registers EL0/EL1 */
100    seL4_VCPUReg_TPIDR_EL0,
101    seL4_VCPUReg_TPIDR_EL1,
102    seL4_VCPUReg_TPIDRRO_EL0,
103
104    /* generic timer registers, to be completed */
105    seL4_VCPUReg_CNTV_CTL,
106    seL4_VCPUReg_CNTV_TVAL,
107    seL4_VCPUReg_CNTV_CVAL,
108
109    /* general registers x0 to x30 have been saved by traps.S */
110    seL4_VCPUReg_SP_EL1,
111    seL4_VCPUReg_ELR_EL1,
112    seL4_VCPUReg_SPSR_EL1, // 32-bit
113    seL4_VCPUReg_Num,
114} seL4_VCPUReg;
115
116#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
117
118enum {
119    seL4_TimeoutReply_FaultIP,
120    seL4_TimeoutReply_SP,
121    seL4_TimeoutReply_SPSR_EL1,
122    seL4_TimeoutReply_X0,
123    seL4_TimeoutReply_X1,
124    seL4_TimeoutReply_X2,
125    seL4_TimeoutReply_X3,
126    seL4_TimeoutReply_X4,
127    seL4_TimeoutReply_X5,
128    seL4_TimeoutReply_X6,
129    seL4_TimeoutReply_X7,
130    seL4_TimeoutReply_X8,
131    seL4_TimeoutReply_X16,
132    seL4_TimeoutReply_X17,
133    seL4_TimeoutReply_X18,
134    seL4_TimeoutReply_X29,
135    seL4_TimeoutReply_X30,
136    seL4_TimeoutReply_X9,
137    seL4_TimeoutReply_X10,
138    seL4_TimeoutReply_X11,
139    seL4_TimeoutReply_X12,
140    seL4_TimeoutReply_X13,
141    seL4_TimeoutReply_X14,
142    seL4_TimeoutReply_X15,
143    seL4_TimeoutReply_X19,
144    seL4_TimeoutReply_X20,
145    seL4_TimeoutReply_X21,
146    seL4_TimeoutReply_X22,
147    seL4_TimeoutReply_X23,
148    seL4_TimeoutReply_X24,
149    seL4_TimeoutReply_X25,
150    seL4_TimeoutReply_X26,
151    seL4_TimeoutReply_X27,
152    seL4_TimeoutReply_X28,
153    seL4_TimeoutReply_Length,
154    SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
155} seL4_TimeoutReply_Msg;
156
157enum {
158    seL4_Timeout_Data,
159    seL4_Timeout_Consumed,
160    seL4_Timeout_Length,
161    SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg)
162} seL4_TimeoutMsg;
163
164#endif /* !__ASSEMBLER__ */
165
166#define seL4_DataFault 0
167#define seL4_InstructionFault 1
168/* object sizes - 2^n */
169#define seL4_PageBits 12
170#define seL4_LargePageBits 21
171#define seL4_HugePageBits 30
172#define seL4_SlotBits 5
173#define seL4_TCBBits 11
174#define seL4_EndpointBits 4
175#define seL4_NotificationBits 6
176#define seL4_SchedContextBits 8
177#define seL4_ReplyBits           5
178
179#define seL4_PageTableBits 12
180#define seL4_PageTableEntryBits 3
181#define seL4_PageTableIndexBits 9
182
183#define seL4_PageDirBits 12
184#define seL4_PageDirEntryBits 3
185#define seL4_PageDirIndexBits 9
186
187#define seL4_ASIDPoolBits 12
188#define seL4_ASIDPoolIndexBits 9
189#define seL4_IOPageTableBits 12
190#define seL4_WordSizeBits 3
191
192#define seL4_PGDBits 12
193#define seL4_PGDEntryBits 3
194#define seL4_PGDIndexBits    9
195
196#define seL4_PUDBits 12
197#define seL4_PUDEntryBits 3
198#define seL4_PUDIndexBits 9
199
200#define seL4_ARM_VCPUBits   12
201#define seL4_VCPUBits       12
202
203/* word size */
204#define seL4_WordBits (sizeof(seL4_Word) * 8)
205
206/* Untyped size limits */
207#define seL4_MinUntypedBits 4
208#define seL4_MaxUntypedBits 47
209
210#ifndef __ASSEMBLER__
211SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
212SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
213SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
214SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits);
215SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits);
216#endif
217
218#ifdef CONFIG_ENABLE_BENCHMARKS
219/* size of kernel log buffer in bytes */
220#define seL4_LogBufferSize (LIBSEL4_BIT(20))
221#endif /* CONFIG_ENABLE_BENCHMARKS */
222
223#ifdef CONFIG_HARDWARE_DEBUG_API
224#define seL4_FirstBreakpoint (0)
225#define seL4_FirstDualFunctionMonitor (-1)
226#define seL4_NumDualFunctionMonitors (0)
227#endif
228
229#define seL4_FastMessageRegisters 4
230
231/* IPC buffer is 1024 bytes, giving size bits of 10 */
232#define seL4_IPCBufferSizeBits 10
233
234#endif
235