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#ifdef CONFIG_KERNEL_GLOBALS_FRAME
15enum {
16    seL4_GlobalsFrame = 0xffffc000,
17};
18#endif /* CONFIG_KERNEL_GLOBALS_FRAME */
19
20/* format of an unknown syscall message */
21typedef enum {
22    seL4_UnknownSyscall_R0,
23    seL4_UnknownSyscall_R1,
24    seL4_UnknownSyscall_R2,
25    seL4_UnknownSyscall_R3,
26    seL4_UnknownSyscall_R4,
27    seL4_UnknownSyscall_R5,
28    seL4_UnknownSyscall_R6,
29    seL4_UnknownSyscall_R7,
30    seL4_UnknownSyscall_FaultIP,
31    seL4_UnknownSyscall_SP,
32    seL4_UnknownSyscall_LR,
33    seL4_UnknownSyscall_CPSR,
34    seL4_UnknownSyscall_Syscall,
35    /* length of an unknown syscall message */
36    seL4_UnknownSyscall_Length,
37    SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
38} seL4_UnknownSyscall_Msg;
39
40/* format of a user exception message */
41typedef enum {
42    seL4_UserException_FaultIP,
43    seL4_UserException_SP,
44    seL4_UserException_CPSR,
45    seL4_UserException_Number,
46    seL4_UserException_Code,
47    /* length of a user exception */
48    seL4_UserException_Length,
49    SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
50} seL4_UserException_Msg;
51
52/* format of a vm fault message */
53typedef enum {
54    seL4_VMFault_IP,
55    seL4_VMFault_Addr,
56    seL4_VMFault_PrefetchFault,
57    seL4_VMFault_FSR,
58    seL4_VMFault_Length,
59    SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
60} seL4_VMFault_Msg;
61
62#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
63typedef enum {
64    seL4_VGICMaintenance_IDX,
65    seL4_VGICMaintenance_Length,
66    SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg),
67} seL4_VGICMaintenance_Msg;
68
69typedef enum {
70    seL4_VPPIEvent_IRQ,
71    SEL4_FORCE_LONG_ENUM(seL4_VPPIEvent_Msg),
72} seL4_VPPIEvent_Msg;
73
74typedef enum {
75    seL4_VCPUFault_HSR,
76    seL4_VCPUFault_Length,
77    SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg),
78} seL4_VCPUFault_Msg;
79
80typedef enum {
81    seL4_VCPUReg_SCTLR = 0,
82    seL4_VCPUReg_ACTLR,
83    seL4_VCPUReg_TTBCR,
84    seL4_VCPUReg_TTBR0,
85    seL4_VCPUReg_TTBR1,
86    seL4_VCPUReg_DACR,
87    seL4_VCPUReg_DFSR,
88    seL4_VCPUReg_IFSR,
89    seL4_VCPUReg_ADFSR,
90    seL4_VCPUReg_AIFSR,
91    seL4_VCPUReg_DFAR,
92    seL4_VCPUReg_IFAR,
93    seL4_VCPUReg_PRRR,
94    seL4_VCPUReg_NMRR,
95    seL4_VCPUReg_CIDR,
96    seL4_VCPUReg_TPIDRPRW,
97    seL4_VCPUReg_FPEXC,
98    seL4_VCPUReg_LRsvc,
99    seL4_VCPUReg_SPsvc,
100    seL4_VCPUReg_LRabt,
101    seL4_VCPUReg_SPabt,
102    seL4_VCPUReg_LRund,
103    seL4_VCPUReg_SPund,
104    seL4_VCPUReg_LRirq,
105    seL4_VCPUReg_SPirq,
106    seL4_VCPUReg_LRfiq,
107    seL4_VCPUReg_SPfiq,
108    seL4_VCPUReg_R8fiq,
109    seL4_VCPUReg_R9fiq,
110    seL4_VCPUReg_R10fiq,
111    seL4_VCPUReg_R11fiq,
112    seL4_VCPUReg_R12fiq,
113#if  CONFIG_MAX_NUM_NODES > 1
114    seL4_VCPUReg_VMPIDR,
115#endif /* CONFIG_MAX_NUM_NODES > 1 */
116    seL4_VCPUReg_SPSRsvc,
117    seL4_VCPUReg_SPSRabt,
118    seL4_VCPUReg_SPSRund,
119    seL4_VCPUReg_SPSRirq,
120    seL4_VCPUReg_SPSRfiq,
121    seL4_VCPUReg_CNTV_CTL,
122    seL4_VCPUReg_CNTV_CVALhigh,
123    seL4_VCPUReg_CNTV_CVALlow,
124    seL4_VCPUReg_CNTVOFFhigh,
125    seL4_VCPUReg_CNTVOFFlow,
126    seL4_VCPUReg_Num,
127} seL4_VCPUReg;
128#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
129
130#ifdef CONFIG_KERNEL_MCS
131typedef enum {
132    seL4_Timeout_Data,
133    /* consumed is 64 bits */
134    seL4_Timeout_Consumed_HighBits,
135    seL4_Timeout_Consumed_LowBits,
136    seL4_Timeout_Length,
137    SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg)
138} seL4_TimeoutMsg;
139
140typedef enum {
141    seL4_TimeoutReply_FaultIP,
142    seL4_TimeoutReply_SP,
143    seL4_TimeoutReply_CPSR,
144    seL4_TimeoutReply_R0,
145    seL4_TimeoutReply_R1,
146    seL4_TimeoutReply_R8,
147    seL4_TimeoutReply_R9,
148    seL4_TimeoutReply_R10,
149    seL4_TimeoutReply_R11,
150    seL4_TimeoutReply_R12,
151    seL4_TimeoutReply_R2,
152    seL4_TimeoutReply_R3,
153    seL4_TimeoutReply_R4,
154    seL4_TimeoutReply_R5,
155    seL4_TimeoutReply_R6,
156    seL4_TimeoutReply_R7,
157    seL4_TimeoutReply_R14,
158    seL4_TimeoutReply_Length,
159    SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
160} seL4_TimeoutReply_Msg;
161#endif /* CONFIG_KERNEL_MCS */
162#endif /* !__ASSEMBLER__ */
163
164#define seL4_DataFault 0
165#define seL4_InstructionFault 1
166/* object sizes - 2^n */
167#define seL4_PageBits 12
168#define seL4_LargePageBits 16
169#define seL4_SlotBits 4
170
171#if ( \
172    defined(CONFIG_HAVE_FPU) && ( \
173        (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE)) || \
174        defined(CONFIG_HARDWARE_DEBUG_API) \
175    ) \
176)
177#define seL4_TCBBits 11
178#elif ( \
179    defined(CONFIG_HAVE_FPU) || \
180    (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE)) || \
181    defined(CONFIG_HARDWARE_DEBUG_API) \
182)
183#define seL4_TCBBits 10
184#else
185#define seL4_TCBBits 9
186#endif
187
188#define seL4_EndpointBits 4
189#ifdef CONFIG_KERNEL_MCS
190#define seL4_NotificationBits 5
191#define seL4_ReplyBits 4
192#else
193#define seL4_NotificationBits 4
194#endif
195
196#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
197#define seL4_PageTableBits 12
198#define seL4_PageTableEntryBits 3
199#define seL4_PageTableIndexBits 9
200#define seL4_SectionBits 21
201#define seL4_SuperSectionBits 25
202#define seL4_PageDirEntryBits 3
203#define seL4_PageDirIndexBits 11
204#define seL4_VCPUBits 12
205#else
206#define seL4_PageTableBits 10
207#define seL4_PageTableEntryBits 2
208#define seL4_PageTableIndexBits 8
209#define seL4_SectionBits 20
210#define seL4_SuperSectionBits 24
211#define seL4_PageDirEntryBits 2
212#define seL4_PageDirIndexBits 12
213#endif
214
215#define seL4_PageDirBits 14
216#define seL4_VSpaceBits seL4_PageDirBits
217
218#ifdef CONFIG_TK1_SMMU
219#define seL4_NumASIDPoolsBits 6
220#else
221#define seL4_NumASIDPoolsBits 7
222#endif
223#define seL4_ASIDPoolBits 12
224#define seL4_ASIDPoolIndexBits 10
225#define seL4_ARM_VCPUBits       12
226#define seL4_IOPageTableBits    12
227
228/* bits in a word */
229#define seL4_WordBits (sizeof(seL4_Word) * 8)
230/* log 2 bits in a word */
231#define seL4_WordSizeBits 2
232
233#ifndef __ASSEMBLER__
234SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
235SEL4_SIZE_SANITY(seL4_PageDirEntryBits,   seL4_PageDirIndexBits,   seL4_PageDirBits);
236SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
237#ifdef seL4_PGDBits
238SEL4_SIZE_SANITY(seL4_PGDEntryBits, seL4_PGDIndexBits, seL4_PGDBits);
239#endif
240#endif
241
242/* Untyped size limits */
243#define seL4_MinUntypedBits 4
244#define seL4_MaxUntypedBits 29
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 512 bytes, giving size bits of 9 */
260#define seL4_IPCBufferSizeBits 9
261
262