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