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
125#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
126#endif /* !__ASSEMBLER__ */
127
128#define seL4_DataFault 0
129#define seL4_InstructionFault 1
130/* object sizes - 2^n */
131#define seL4_PageBits 12
132#define seL4_LargePageBits 16
133#define seL4_SlotBits 4
134
135#if ((defined(CONFIG_DEBUG_BUILD) || CONFIG_MAX_NUM_NODES > 1) && defined(CONFIG_HAVE_FPU) && defined(CONFIG_HARDWARE_DEBUG_API)) \
136    || (defined(CONFIG_HAVE_FPU) && defined(CONFIG_ARM_HYPERVISOR_SUPPORT))
137#define seL4_TCBBits 11
138#elif defined(CONFIG_HAVE_FPU)
139#define seL4_TCBBits 10
140#else
141#define seL4_TCBBits 9
142#endif
143
144#define seL4_EndpointBits 4
145#define seL4_NotificationBits 4
146
147#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
148#define seL4_PageTableBits 12
149#define seL4_PageTableEntryBits 3
150#define seL4_PageTableIndexBits 9
151#define seL4_SectionBits 21
152#define seL4_SuperSectionBits 25
153#define seL4_PGDEntryBits 3
154#define seL4_PGDIndexBits 2
155#define seL4_PGDBits (seL4_PGDIndexBits + seL4_PGDEntryBits)
156#define seL4_PageDirEntryBits 3
157#define seL4_PageDirIndexBits 11
158#define seL4_VCPUBits 12
159#else
160#define seL4_PageTableBits 10
161#define seL4_PageTableEntryBits 2
162#define seL4_PageTableIndexBits 8
163#define seL4_SectionBits 20
164#define seL4_SuperSectionBits 24
165#define seL4_PageDirEntryBits 2
166#define seL4_PageDirIndexBits 12
167#endif
168
169#define seL4_PageDirBits 14
170
171#define seL4_ASIDPoolBits 12
172#define seL4_ASIDPoolIndexBits 10
173#define seL4_ARM_VCPUBits       12
174#define seL4_IOPageTableBits    12
175
176/* bits in a word */
177#define seL4_WordBits (sizeof(seL4_Word) * 8)
178/* log 2 bits in a word */
179#define seL4_WordSizeBits 2
180
181#ifndef __ASSEMBLER__
182SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
183SEL4_SIZE_SANITY(seL4_PageDirEntryBits,   seL4_PageDirIndexBits,   seL4_PageDirBits);
184SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
185#endif
186
187/* Untyped size limits */
188#define seL4_MinUntypedBits 4
189#define seL4_MaxUntypedBits 29
190
191#ifdef CONFIG_ENABLE_BENCHMARKS
192/* size of kernel log buffer in bytes */
193#define seL4_LogBufferSize (LIBSEL4_BIT(20))
194#endif /* CONFIG_ENABLE_BENCHMARKS */
195
196#ifdef CONFIG_HARDWARE_DEBUG_API
197#define seL4_FirstBreakpoint (0)
198#define seL4_FirstDualFunctionMonitor (-1)
199#define seL4_NumDualFunctionMonitors (0)
200#endif
201
202#define seL4_FastMessageRegisters 4
203
204/* IPC buffer is 512 bytes, giving size bits of 9 */
205#define seL4_IPCBufferSizeBits 9
206
207#endif
208