1--
2-- Copyright 2014, General Dynamics C4 Systems
3--
4-- SPDX-License-Identifier: GPL-2.0-only
5--
6
7-- Default base size: uint32_t
8base 32
9
10block null_cap {
11    padding 32
12
13    padding 28
14    field capType 4
15}
16
17-- The combination of freeIndex and blockSize must match up with the
18-- definitions of MIN_SIZE_BITS and MAX_SIZE_BITS
19block untyped_cap {
20    field capFreeIndex 26
21    field capIsDevice  1
22    field capBlockSize 5
23
24    field_high capPtr 28
25    field capType     4
26}
27
28block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
29                   capCanReceive, capEPPtr, capType) {
30    field_high capEPPtr 28
31    field capCanGrantReply 1
32    field capCanGrant 1
33    field capCanReceive 1
34    field capCanSend 1
35
36    field capEPBadge 28
37    field capType 4
38}
39
40block notification_cap {
41    field capNtfnBadge 28
42    padding 2
43    field capNtfnCanReceive 1
44    field capNtfnCanSend 1
45
46    field_high capNtfnPtr 28
47    field capType 4
48}
49
50#ifdef CONFIG_KERNEL_MCS
51block reply_cap {
52    field capReplyPtr 32
53
54    padding 27
55    field capReplyCanGrant 1
56    field capType 4
57}
58
59block call_stack {
60    field_high callStackPtr 28
61    padding 3
62    field isHead 1
63}
64#else
65block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
66    padding 32
67
68    field_high capTCBPtr 26
69    field capReplyCanGrant 1
70    field capReplyMaster 1
71    field capType 4
72}
73#endif
74-- The user-visible format of the data word is defined by cnode_capdata, below.
75block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard,
76                capCNodePtr, capType) {
77    padding 4
78    field capCNodeGuardSize 5
79    field capCNodeRadix 5
80    field capCNodeGuard 18
81
82    field_high capCNodePtr 27
83    padding 1
84    field capType 4
85}
86
87block thread_cap {
88    padding              32
89
90    field_high capTCBPtr 28
91    field capType         4
92}
93
94block irq_control_cap {
95    padding       32
96
97    padding       24
98    field capType  8
99}
100
101block irq_handler_cap {
102#ifdef ENABLE_SMP_SUPPORT
103    field capIRQ   32
104#else
105    padding 24
106    field capIRQ 8
107#endif
108
109    padding       24
110    field capType  8
111}
112
113block zombie_cap {
114    field capZombieID     32
115
116    padding               18
117    field capZombieType   6
118    field capType         8
119}
120
121block domain_cap {
122    padding 32
123
124    padding 24
125    field capType 8
126}
127
128#ifdef CONFIG_KERNEL_MCS
129block sched_context_cap {
130    field_high capSCPtr 28
131    padding              4
132
133    padding             18
134    field capSCSizeBits  6
135    field capType        8
136}
137
138block sched_control_cap {
139    field core    32
140
141    padding       24
142    field capType 8
143}
144#endif
145---- Arch-independent object types
146
147-- Endpoint: size = 16 bytes
148block endpoint {
149    padding 64
150
151    field_high epQueue_head 28
152    padding 4
153
154    field_high epQueue_tail 28
155    padding 2
156    field state 2
157}
158
159-- Notification object: size = 16 bytes (32 bytes on mcs)
160block notification {
161#ifdef CONFIG_KERNEL_MCS
162    padding 96
163
164    field_high ntfnSchedContext 28
165    padding 4
166#endif
167
168    field_high ntfnBoundTCB 28
169    padding 4
170
171    field ntfnMsgIdentifier 32
172
173    field_high ntfnQueue_head 28
174    padding 4
175
176    field_high ntfnQueue_tail 28
177    padding 2
178    field state 2
179}
180
181-- Mapping database (MDB) node: size = 8 bytes
182block mdb_node {
183    field_high mdbNext 29
184    padding 1
185    field mdbRevocable 1
186    field mdbFirstBadged 1
187
188    field_high mdbPrev 29
189    padding 3
190}
191
192-- Thread state data
193--
194-- tsType
195-- * Running
196-- * Restart
197-- * Inactive
198-- * BlockedOnReceive
199--   - Endpoint
200--   - CanGrant
201-- * BlockedOnSend
202--   - Endpoint
203--   - CanGrant
204--   - CanGrantReply
205--   - IsCall
206--   - IPCBadge
207--   - Fault
208--     - faultType
209--     * CapFault
210--       - Address
211--       - InReceivePhase
212--       - LookupFailure
213--         - lufType
214--         * InvalidRoot
215--         * MissingCapability
216--           - BitsLeft
217--         * DepthMismatch
218--           - BitsFound
219--           - BitsLeft
220--         * GuardMismatch
221--           - GuardFound
222--           - BitsLeft
223--           - GuardSize
224--     * VMFault
225--       - Address
226--       - FSR
227--       - FaultType
228--     * UnknownSyscall
229--       - Number
230--     * UserException
231--       - Number
232--       - Code
233-- * BlockedOnReply
234-- * BlockedOnFault
235--   - Fault
236-- * BlockedOnNotification
237--   - Notification
238-- * Idle
239
240-- Lookup fault: size = 8 bytes
241block invalid_root {
242    padding 62
243    field lufType 2
244}
245
246block missing_capability {
247    padding 56
248    field bitsLeft 6
249    field lufType 2
250}
251
252block depth_mismatch {
253    padding 50
254    field bitsFound 6
255    field bitsLeft 6
256    field lufType 2
257}
258
259block guard_mismatch {
260    field guardFound 32
261    padding 18
262    field bitsLeft 6
263    field bitsFound 6
264    field lufType 2
265}
266
267tagged_union lookup_fault lufType {
268    tag invalid_root 0
269    tag missing_capability 1
270    tag depth_mismatch 2
271    tag guard_mismatch 3
272}
273
274-- Fault: size = 8 bytes
275block NullFault {
276    padding 60
277    field seL4_FaultType 4
278}
279
280block CapFault {
281    field address 32
282    field inReceivePhase 1
283    padding 27
284    field seL4_FaultType 4
285}
286
287block UnknownSyscall {
288    field syscallNumber 32
289    padding 28
290    field seL4_FaultType 4
291}
292
293block UserException {
294    field number 32
295    field code 28
296    field seL4_FaultType 4
297}
298
299#ifdef CONFIG_HARDWARE_DEBUG_API
300block DebugException {
301    field breakpointAddress 32
302
303    padding 20
304    -- X86 has 4 breakpoints (DR0-3).
305    -- ARM has between 2 and 16 breakpoints
306    --   ( ARM Ref manual, C3.3).
307    -- So we just use 4 bits to cater for both.
308    field breakpointNumber 4
309    field exceptionReason 4
310    field seL4_FaultType 4
311}
312#endif
313
314#ifdef CONFIG_KERNEL_MCS
315block Timeout {
316    field badge 32
317    padding 28
318    field seL4_FaultType 4
319}
320#endif
321
322-- Thread state: size = 12 bytes
323block thread_state(blockingIPCBadge, blockingIPCCanGrant,
324                   blockingIPCCanGrantReply, blockingIPCIsCall,
325                   tcbQueued, blockingObject,
326#ifdef CONFIG_KERNEL_MCS
327                   tcbInReleaseQueue, replyObject,
328#endif
329                   tsType) {
330    field blockingIPCBadge 28
331    field blockingIPCCanGrant 1
332    field blockingIPCCanGrantReply 1
333    field blockingIPCIsCall 1
334    padding 1
335
336    -- this is fastpath-specific. it is useful to be able to write
337    -- tsType and without changing tcbQueued or tcbInReleaseQueue
338#ifdef CONFIG_KERNEL_MCS
339    field_high replyObject 28
340    padding 2
341#else
342    padding 31
343#endif
344    field tcbQueued 1
345#ifdef CONFIG_KERNEL_MCS
346    field tcbInReleaseQueue 1
347#endif
348
349    field_high blockingObject 28
350    field tsType 4
351}
352