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#ifndef __ASSEMBLER__
14/* format of an unknown syscall message */
15typedef enum {
16    seL4_UnknownSyscall_X0,
17    seL4_UnknownSyscall_X1,
18    seL4_UnknownSyscall_X2,
19    seL4_UnknownSyscall_X3,
20    seL4_UnknownSyscall_X4,
21    seL4_UnknownSyscall_X5,
22    seL4_UnknownSyscall_X6,
23    seL4_UnknownSyscall_X7,
24    seL4_UnknownSyscall_FaultIP,
25    seL4_UnknownSyscall_SP,
26    seL4_UnknownSyscall_LR,
27    seL4_UnknownSyscall_SPSR,
28    seL4_UnknownSyscall_Syscall,
29    /* length of an unknown syscall message */
30    seL4_UnknownSyscall_Length,
31    SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
32} seL4_UnknownSyscall_Msg;
33
34/* format of a user exception message */
35typedef enum {
36    seL4_UserException_FaultIP,
37    seL4_UserException_SP,
38    seL4_UserException_SPSR,
39    seL4_UserException_Number,
40    seL4_UserException_Code,
41    /* length of a user exception */
42    seL4_UserException_Length,
43    SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
44} seL4_UserException_Msg;
45
46/* format of a vm fault message */
47typedef enum {
48    seL4_VMFault_IP,
49    seL4_VMFault_Addr,
50    seL4_VMFault_PrefetchFault,
51    seL4_VMFault_FSR,
52    seL4_VMFault_Length,
53    SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
54} seL4_VMFault_Msg;
55
56#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
57
58typedef enum {
59    seL4_VGICMaintenance_IDX,
60    seL4_VGICMaintenance_Length,
61    SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg),
62} seL4_VGICMaintenance_Msg;
63
64typedef enum {
65    seL4_VPPIEvent_IRQ,
66    SEL4_FORCE_LONG_ENUM(seL4_VPPIEvent_Msg),
67} seL4_VPPIEvent_Msg;
68
69
70typedef enum {
71    seL4_VCPUFault_HSR,
72    seL4_VCPUFault_Length,
73    SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg),
74} seL4_VCPUFault_Msg;
75
76typedef enum {
77    /* VM control registers EL1 */
78    seL4_VCPUReg_SCTLR = 0,
79    seL4_VCPUReg_TTBR0,
80    seL4_VCPUReg_TTBR1,
81    seL4_VCPUReg_TCR,
82    seL4_VCPUReg_MAIR,
83    seL4_VCPUReg_AMAIR,
84    seL4_VCPUReg_CIDR,
85
86    /* other system registers EL1 */
87    seL4_VCPUReg_ACTLR,
88    seL4_VCPUReg_CPACR,
89
90    /* exception handling registers EL1 */
91    seL4_VCPUReg_AFSR0,
92    seL4_VCPUReg_AFSR1,
93    seL4_VCPUReg_ESR,
94    seL4_VCPUReg_FAR,
95    seL4_VCPUReg_ISR,
96    seL4_VCPUReg_VBAR,
97
98    /* thread pointer/ID registers EL0/EL1 */
99    seL4_VCPUReg_TPIDR_EL1,
100
101#if CONFIG_MAX_NUM_NODES > 1
102    /* Virtualisation Multiprocessor ID Register */
103    seL4_VCPUReg_VMPIDR_EL2,
104#endif /* CONFIG_MAX_NUM_NODES > 1 */
105
106    /* general registers x0 to x30 have been saved by traps.S */
107    seL4_VCPUReg_SP_EL1,
108    seL4_VCPUReg_ELR_EL1,
109    seL4_VCPUReg_SPSR_EL1, // 32-bit
110
111    /* generic timer registers, to be completed */
112    seL4_VCPUReg_CNTV_CTL,
113    seL4_VCPUReg_CNTV_CVAL,
114    seL4_VCPUReg_CNTVOFF,
115    seL4_VCPUReg_CNTKCTL_EL1,
116
117    seL4_VCPUReg_Num,
118} seL4_VCPUReg;
119
120#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
121
122#ifdef CONFIG_KERNEL_MCS
123typedef enum {
124    seL4_TimeoutReply_FaultIP,
125    seL4_TimeoutReply_SP,
126    seL4_TimeoutReply_SPSR_EL1,
127    seL4_TimeoutReply_X0,
128    seL4_TimeoutReply_X1,
129    seL4_TimeoutReply_X2,
130    seL4_TimeoutReply_X3,
131    seL4_TimeoutReply_X4,
132    seL4_TimeoutReply_X5,
133    seL4_TimeoutReply_X6,
134    seL4_TimeoutReply_X7,
135    seL4_TimeoutReply_X8,
136    seL4_TimeoutReply_X16,
137    seL4_TimeoutReply_X17,
138    seL4_TimeoutReply_X18,
139    seL4_TimeoutReply_X29,
140    seL4_TimeoutReply_X30,
141    seL4_TimeoutReply_X9,
142    seL4_TimeoutReply_X10,
143    seL4_TimeoutReply_X11,
144    seL4_TimeoutReply_X12,
145    seL4_TimeoutReply_X13,
146    seL4_TimeoutReply_X14,
147    seL4_TimeoutReply_X15,
148    seL4_TimeoutReply_X19,
149    seL4_TimeoutReply_X20,
150    seL4_TimeoutReply_X21,
151    seL4_TimeoutReply_X22,
152    seL4_TimeoutReply_X23,
153    seL4_TimeoutReply_X24,
154    seL4_TimeoutReply_X25,
155    seL4_TimeoutReply_X26,
156    seL4_TimeoutReply_X27,
157    seL4_TimeoutReply_X28,
158    seL4_TimeoutReply_Length,
159    SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
160} seL4_TimeoutReply_Msg;
161
162typedef enum {
163    seL4_Timeout_Data,
164    seL4_Timeout_Consumed,
165    seL4_Timeout_Length,
166    SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg)
167} seL4_TimeoutMsg;
168#endif
169#endif /* !__ASSEMBLER__ */
170
171#define seL4_DataFault 0
172#define seL4_InstructionFault 1
173/* object sizes - 2^n */
174#define seL4_PageBits 12
175#define seL4_LargePageBits 21
176#define seL4_HugePageBits 30
177#define seL4_SlotBits 5
178#define seL4_TCBBits 11
179#define seL4_EndpointBits 4
180#ifdef CONFIG_KERNEL_MCS
181#define seL4_NotificationBits 6
182#define seL4_ReplyBits           5
183#else
184#define seL4_NotificationBits 5
185#endif
186
187#define seL4_PageTableBits 12
188#define seL4_PageTableEntryBits 3
189#define seL4_PageTableIndexBits 9
190
191#define seL4_PageDirBits 12
192#define seL4_PageDirEntryBits 3
193#define seL4_PageDirIndexBits 9
194
195#define seL4_NumASIDPoolsBits 7
196#define seL4_ASIDPoolBits 12
197#define seL4_ASIDPoolIndexBits 9
198#define seL4_IOPageTableBits 12
199#define seL4_WordSizeBits 3
200
201#define seL4_PUDEntryBits 3
202
203#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40)
204/* for a 3 level translation, we skip the PGD */
205#define seL4_PGDBits 0
206#define seL4_PGDEntryBits 0
207#define seL4_PGDIndexBits    0
208
209#define seL4_PUDBits 13
210#define seL4_PUDIndexBits 10
211
212#define seL4_VSpaceBits seL4_PUDBits
213#define seL4_VSpaceIndexBits seL4_PUDIndexBits
214#define seL4_ARM_VSpaceObject seL4_ARM_PageUpperDirectoryObject
215#else
216#define seL4_PGDBits 12
217#define seL4_PGDEntryBits 3
218#define seL4_PGDIndexBits    9
219
220#define seL4_PUDBits 12
221#define seL4_PUDIndexBits 9
222
223#define seL4_VSpaceBits seL4_PGDBits
224#define seL4_VSpaceIndexBits seL4_PGDIndexBits
225#define seL4_ARM_VSpaceObject seL4_ARM_PageGlobalDirectoryObject
226#endif
227
228#define seL4_ARM_VCPUBits   12
229#define seL4_VCPUBits       12
230
231/* word size */
232#define seL4_WordBits (sizeof(seL4_Word) * 8)
233
234/* Untyped size limits */
235#define seL4_MinUntypedBits 4
236#define seL4_MaxUntypedBits 47
237
238#ifndef __ASSEMBLER__
239SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
240SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
241SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
242SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits);
243SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits);
244#endif
245
246#ifdef CONFIG_ENABLE_BENCHMARKS
247/* size of kernel log buffer in bytes */
248#define seL4_LogBufferSize (LIBSEL4_BIT(20))
249#endif /* CONFIG_ENABLE_BENCHMARKS */
250
251#ifdef CONFIG_HARDWARE_DEBUG_API
252#define seL4_FirstBreakpoint (0)
253#define seL4_FirstDualFunctionMonitor (-1)
254#define seL4_NumDualFunctionMonitors (0)
255#endif
256
257#define seL4_FastMessageRegisters 4
258
259/* IPC buffer is 1024 bytes, giving size bits of 10 */
260#define seL4_IPCBufferSizeBits 10
261
262#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
263#ifndef CONFIG_ARM_SMMU
264/* 1 slot at the end of the vspace is used to hold the VMID assigned to the vspace */
265#define seL4_VSpaceReservedSlots 1
266#else /*CONFIG_ARM_SMMU*/
267/* 1 slot at the end of the vspace is used to hold the VMID assigned to the vspace */
268/* 1 slot at the end of the vspace is used to hold the number of SMMU CBs assigned to the vspace */
269#define seL4_VSpaceReservedSlots 2
270#endif /*CONFIG_ARM_SMMU*/
271
272/* The userspace occupies the range 0x0 to 0xfffffffffff.
273 * The stage-1 translation is disabled, and the stage-2
274 * translation input addree size is constrained by the
275 * ID_AA64MMFR0_EL1.PARange which is 44 bits on TX1.
276 * Anything address above the range above triggers an
277 * address size fault.
278 */
279/* First address in the virtual address space that is not accessible to user level */
280#if defined(CONFIG_ARM_PA_SIZE_BITS_44)
281#define seL4_UserTop 0x00000fffffffffff
282#elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
283/* Currently other definitions of seL4_UserTop already have free slots at the end and don't need to subtract for seL4_VSpaceReservedSlots.
284 * Each slot used requires subtracting 1GiB from the top address.
285 */
286#define seL4_UserTop (0x000000ffffffffff - seL4_VSpaceReservedSlots * 0x40000000)
287#else
288#error "Unknown physical address width"
289#endif
290
291#else
292/* First address in the virtual address space that is not accessible to user level */
293#define seL4_UserTop 0x00007fffffffffff
294#endif
295