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#include <autoconf.h>
10#include <capdl_loader_app/gen_config.h>
11
12#include <sel4/types.h>
13#include <sel4utils/mapping.h>
14#include <limits.h>
15#include <stdbool.h>
16#include <stdlib.h>
17#include <utils/util.h>
18
19#define CDL_VM_CacheEnabled         seL4_ARCH_Default_VMAttributes
20#define CDL_VM_CacheDisabled        seL4_ARCH_Uncached_VMAttributes
21
22#if defined(CONFIG_ARCH_ARM)
23
24/* ARM does not support write through */
25#define CDL_VM_WriteThrough         CDL_VM_CacheDisabled
26/* Note that this is the number of bits translated by the PT
27 * not the size of the actual PT object */
28#elif defined(CONFIG_ARCH_X86)
29
30#define CDL_VM_WriteThrough         seL4_X86_WriteThrough
31
32#endif
33
34/* Binary CapDL representation -- capdl.h */
35
36/* CapRights:  Access rights of capabilities
37 * This type is used internally by capDL, and doesn't
38 * reflect the representation of cap rights in the kernel api.
39 */
40typedef enum {
41    CDL_CanWrite = BIT(0),
42    CDL_CanRead = BIT(1),
43    CDL_CanGrant = BIT(2),
44    CDL_CanGrantReply = BIT(3),
45    CDL_AllRights = (BIT(0) | BIT(1) | BIT(2) | BIT(3)),
46} CDL_CapRights;
47
48/* ObjectID: index into the objects array */
49typedef seL4_Word CDL_ObjID;
50#define INVALID_OBJ_ID ((CDL_ObjID)-1)
51
52/* IRQ number: Hardware IRQ number */
53typedef seL4_Word CDL_IRQ;
54/* Core id */
55typedef seL4_Word CDL_Core;
56
57/* Capability: */
58typedef enum {
59    CDL_NullCap,
60    CDL_UntypedCap,
61    CDL_EPCap,
62    CDL_NotificationCap,
63    CDL_ReplyCap,
64    CDL_MasterReplyCap,
65    CDL_CNodeCap,
66    CDL_TCBCap,
67    CDL_IRQControlCap,
68    CDL_IRQHandlerCap,
69    CDL_FrameCap,
70    CDL_PTCap,
71    CDL_PDCap,
72    CDL_PML4Cap,
73    CDL_PDPTCap,
74    CDL_PUDCap,
75    CDL_PGDCap,
76    CDL_ASIDControlCap,
77    CDL_ASIDPoolCap,
78#if defined(CONFIG_ARCH_X86)
79    CDL_IOPortsCap,
80    CDL_IOSpaceCap,
81#endif
82#if defined(CONFIG_ARCH_ARM)
83    CDL_ARMIOSpaceCap,
84    CDL_SIDCap,
85    CDL_CBCap,
86#endif
87#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
88    CDL_VCPUCap,
89#endif
90    CDL_SCCap,
91    CDL_SchedControlCap,
92    CDL_RTReplyCap,
93    CDL_DomainCap,
94} CDL_CapType;
95
96#define CDL_CapData_Badge 0
97#define CDL_CapData_Guard 1
98#define CDL_CapData_Raw   2
99
100typedef struct {
101    union {
102        struct {
103            seL4_Word guard_bits: 18; /* guards have an 18-bit value */
104seL4_Word guard_size:
105            seL4_WordBits - 18;
106        };
107        seL4_Word badge;
108        seL4_Word data;
109    };
110    unsigned tag: 2; /* One of CDL_CapData_* */
111} PACKED CDL_CapData;
112
113typedef struct {
114    CDL_ObjID obj_id;
115    CDL_CapData data;
116    CDL_IRQ irq;
117    CDL_ObjID mapping_container_id;
118    seL4_Word mapping_slot;
119    seL4_CPtr mapped_frame_cap;
120
121    /* This type tag actually has a more specific type, but we force it to be represented as a
122     * uint8_t to compress the size of this struct in memory.
123     */
124    /* CDL_CapType */ uint8_t type;
125
126    /* The following map to more specific seL4 types, but the seL4 types are padded to word size,
127     * wasting space. This padding is necessary for ABI compatibility, but we have no such
128     * requirements here and can instead reduce the in-memory size of specs by packing these fields
129     * into fewer bits.
130     */
131    /* seL4_ARCH_VMAttributes */ unsigned vm_attribs: 3;
132    /* bool                   */ unsigned is_orig: 1;
133/* seL4_CapRights         */ unsigned rights:
134    seL4_CapRightsBits;
135} PACKED CDL_Cap;
136
137/* CapMap: is just an array of cap slots, position of the slot and cap */
138typedef struct {
139    seL4_Word slot;
140    CDL_Cap cap;
141} PACKED CDL_CapSlot;
142
143typedef struct {
144    seL4_Word num;
145    CDL_CapSlot *slot;
146} CDL_CapMap;
147
148/* ObjMap: is just an array of object slots */
149typedef struct {
150    seL4_Word slot;
151    CDL_ObjID id;
152} CDL_ObjSlot;
153
154typedef struct {
155    seL4_Word num;
156    CDL_ObjSlot *slot;
157} CDL_ObjMap;
158
159/* KernelObject: */
160typedef enum {
161    CDL_Endpoint      = seL4_EndpointObject,
162    CDL_Notification  = seL4_NotificationObject,
163    CDL_TCB           = seL4_TCBObject,
164    CDL_CNode         = seL4_CapTableObject,
165    CDL_Untyped       = seL4_UntypedObject,
166#if defined(CONFIG_ARCH_ARM)
167    CDL_PT            = seL4_ARM_PageTableObject,
168    CDL_PD            = seL4_ARM_PageDirectoryObject,
169    CDL_Frame         = seL4_ARM_SmallPageObject,
170#ifdef CONFIG_ARCH_AARCH64
171    CDL_PUD           = seL4_ARM_PageUpperDirectoryObject,
172    CDL_PGD           = seL4_ARM_PageGlobalDirectoryObject,
173#endif
174#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
175    CDL_VCPU          = seL4_ARM_VCPUObject,
176#endif
177#ifdef CONFIG_VTX
178    CDL_VCPU          = seL4_X86_VCPUObject,
179#endif
180#elif defined(CONFIG_ARCH_X86)
181    CDL_PT            = seL4_X86_PageTableObject,
182    CDL_PD            = seL4_X86_PageDirectoryObject,
183    CDL_Frame         = seL4_X86_4K,
184#ifdef CONFIG_ARCH_X86_64
185    CDL_PML4          = seL4_X64_PML4Object,
186    CDL_PDPT          = seL4_X86_PDPTObject,
187#endif
188#endif
189    CDL_ASIDPool      = seL4_ObjectTypeCount + 1,
190    CDL_Interrupt     = seL4_ObjectTypeCount + 2,
191#if defined(CONFIG_ARCH_X86)
192    CDL_IOPorts       = seL4_ObjectTypeCount + 3,
193    CDL_IODevice      = seL4_ObjectTypeCount + 4,
194#endif
195#ifdef CONFIG_KERNEL_MCS
196    CDL_SchedContext  = seL4_SchedContextObject,
197    CDL_RTReply  = seL4_ReplyObject,
198#else
199    CDL_SchedContext  = seL4_ObjectTypeCount + 5,
200    CDL_RTReply  = seL4_ObjectTypeCount + 6,
201#endif
202#if defined(CONFIG_ARCH_X86)
203    CDL_IOAPICInterrupt = seL4_ObjectTypeCount + 7,
204    CDL_MSIInterrupt = seL4_ObjectTypeCount + 8,
205#endif
206#if defined(CONFIG_ARCH_ARM)
207    CDL_ARMIODevice   = seL4_ObjectTypeCount + 9,
208    CDL_ARMInterrupt = seL4_ObjectTypeCount + 11,
209    CDL_SID = seL4_ObjectTypeCount + 12,
210    CDL_CB = seL4_ObjectTypeCount + 13,
211#endif
212#ifdef CONFIG_ARCH_RISCV
213    CDL_Frame = seL4_RISCV_4K_Page,
214    CDL_PT = seL4_RISCV_PageTableObject,
215    /* We use this hack to distiguish a PageTableObject that is used as a root vspace
216     * as parts of the loader assume that the root vspace object types are unique
217     */
218    CDL_PT_ROOT_ALIAS = seL4_ObjectTypeCount + 10,
219#endif
220} CDL_ObjectType;
221
222#ifdef CONFIG_ARCH_AARCH64
223#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ARM_PA_SIZE_BITS_40)
224#define CDL_TOP_LEVEL_PD         CDL_PUD
225#define CDL_PT_NUM_LEVELS 3
226#else
227#define CDL_TOP_LEVEL_PD         CDL_PGD
228#define CDL_PT_NUM_LEVELS 4
229#define CDL_PT_LEVEL_1_MAP       seL4_ARM_PageUpperDirectory_Map
230#endif
231#define CDL_PT_LEVEL_1_IndexBits seL4_PUDIndexBits
232#define CDL_PT_LEVEL_2_MAP       seL4_ARM_PageDirectory_Map
233#define CDL_PT_LEVEL_2_IndexBits seL4_PageDirIndexBits
234#define CDL_PT_LEVEL_3_MAP       seL4_ARM_PageTable_Map
235#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits
236#elif CONFIG_ARCH_X86_64
237#define CDL_TOP_LEVEL_PD         CDL_PML4
238#define CDL_PT_LEVEL_1_MAP       seL4_X86_PDPT_Map
239#define CDL_PT_LEVEL_1_IndexBits seL4_PDPTIndexBits
240#define CDL_PT_LEVEL_2_MAP       seL4_X86_PageDirectory_Map
241#define CDL_PT_LEVEL_2_IndexBits seL4_PageDirIndexBits
242#define CDL_PT_LEVEL_3_MAP       seL4_X86_PageTable_Map
243#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits
244#define CDL_PT_NUM_LEVELS 4
245#elif CONFIG_ARCH_RISCV
246#define CDL_TOP_LEVEL_PD CDL_PT_ROOT_ALIAS
247#define CDL_PT_LEVEL_0_MAP       seL4_RISCV_PageTable_Map
248#define CDL_PT_LEVEL_0_IndexBits seL4_PageTableIndexBits
249#define CDL_PT_LEVEL_1_MAP       seL4_RISCV_PageTable_Map
250#define CDL_PT_LEVEL_1_IndexBits seL4_PageTableIndexBits
251#define CDL_PT_LEVEL_2_MAP       seL4_RISCV_PageTable_Map
252#define CDL_PT_LEVEL_2_IndexBits seL4_PageTableIndexBits
253#define CDL_PT_LEVEL_3_MAP       seL4_RISCV_PageTable_Map
254#define CDL_PT_LEVEL_3_IndexBits seL4_PageTableIndexBits
255#define CDL_PT_NUM_LEVELS CONFIG_PT_LEVELS
256#else
257#define CDL_TOP_LEVEL_PD         CDL_PD
258#define CDL_PT_NUM_LEVELS 2
259#endif
260
261typedef struct {
262    uint8_t priority;
263    uint8_t max_priority;
264    uint8_t affinity;
265    uint8_t domain;
266    seL4_Word pc;
267    seL4_Word sp;
268    const char *elf_name;
269    const seL4_Word *init;
270    seL4_Word init_sz;
271    seL4_CPtr fault_ep;
272    seL4_Word ipcbuffer_addr;
273    bool resume;
274} CDL_TCBExtraInfo;
275
276typedef struct {
277    uint64_t period;
278    uint64_t budget;
279    seL4_Word data;
280} CDL_SCExtraInfo;
281
282typedef struct {
283    uint8_t bank;
284} CDL_CBExtraInfo;
285
286typedef struct {
287    int ioapic;
288    int ioapic_pin;
289    int level;
290    int polarity;
291} CDL_IOAPICIRQExtraInfo;
292
293typedef struct {
294    int handle;
295    int pci_bus;
296    int pci_dev;
297    int pci_fun;
298} CDL_MSIIRQExtraInfo;
299
300typedef struct {
301    int trigger;
302    int target;
303} CDL_ARMIRQExtraInfo;
304
305typedef enum {
306    CDL_FrameFill_None = 0,
307    CDL_FrameFill_BootInfo,
308    CDL_FrameFill_FileData,
309} CDL_FrameFillType_t;
310
311typedef enum {
312    CDL_FrameFill_BootInfo_Padding = SEL4_BOOTINFO_HEADER_FDT,
313    CDL_FrameFill_BootInfo_X86_VBE = SEL4_BOOTINFO_HEADER_X86_VBE,
314    CDL_FrameFill_BootInfo_X86_MBMMAP = SEL4_BOOTINFO_HEADER_X86_MBMMAP,
315    CDL_FrameFill_BootInfo_X86_ACPI_RSDP = SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP,
316    CDL_FrameFill_BootInfo_X86_Framebuffer = SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER,
317    CDL_FrameFill_BootInfo_X86_TSC_Freq = SEL4_BOOTINFO_HEADER_X86_TSC_FREQ,
318    CDL_FrameFill_BootInfo_FDT = SEL4_BOOTINFO_HEADER_FDT
319} CDL_FrameFill_BootInfoEnum_t;
320
321typedef struct {
322    CDL_FrameFill_BootInfoEnum_t type;
323    size_t src_offset;
324} CDL_FrameFill_BootInfoType_t;
325
326typedef struct {
327    char *filename;
328    size_t file_offset;
329} CDL_FrameFill_FileDataType_t;
330
331typedef struct {
332    CDL_FrameFillType_t type;
333    size_t dest_offset;
334    size_t dest_len;
335    union {
336        CDL_FrameFill_BootInfoType_t bi_type;
337        CDL_FrameFill_FileDataType_t file_data_type;
338    };
339} CDL_FrameFill_Element_t;
340
341typedef struct {
342    CDL_FrameFill_Element_t fill[CONFIG_CAPDL_LOADER_FILLS_PER_FRAME];
343    seL4_Word paddr;
344} CDL_FrameExtraInfo;
345
346typedef struct {
347#ifdef CONFIG_DEBUG_BUILD
348    const char *name; /* textual ObjID from the capDL spec */
349#endif
350
351    CDL_CapMap slots;
352    union {
353        CDL_TCBExtraInfo tcb_extra;
354        CDL_SCExtraInfo sc_extra;
355        CDL_CBExtraInfo cb_extra;
356        CDL_IOAPICIRQExtraInfo ioapicirq_extra;
357        CDL_MSIIRQExtraInfo msiirq_extra;
358        CDL_ARMIRQExtraInfo armirq_extra;
359        CDL_FrameExtraInfo frame_extra;
360        seL4_Word paddr; /* Physical address; only relevant for untyped objects. */
361        seL4_Word asid_high; /* for ASID pools */
362        struct {
363            seL4_Word start;
364            seL4_Word end;
365        };
366    };
367    CDL_ObjectType type;
368    /* The configuration for IO ports on x86 is currently overloaded into the
369     * size_bits parameter. */
370    uint32_t size_bits;
371
372} PACKED CDL_Object;
373
374typedef struct {
375    /* The untyped that the children should be derived from */
376    CDL_ObjID untyped;
377    /* Number of children to derive from this untyped */
378    seL4_Word num;
379    /* Children to derive from this untyped */
380    CDL_ObjID *children;
381} CDL_UntypedDerivation;
382
383/* CapDLModel: is described by a map from ObjectIDs (array index) to Objects */
384typedef struct {
385    seL4_Word num;
386    CDL_Object *objects;
387    seL4_Word num_irqs;
388    CDL_ObjID *irqs;
389
390    seL4_Word num_untyped;
391    CDL_UntypedDerivation *untyped;
392
393    /* Array from ASID slot number to ASID pool object.
394       NB: asid_slots[0] is unused, so the array size is one larger
395           than the number of slots being allocated.
396           Slot 0 is unused because it is the root thread's ASID slot,
397           which the loader uses for loading other component VSpaces. */
398    seL4_Word num_asid_slots;
399    CDL_ObjID *asid_slots;
400} CDL_Model;
401
402/* helper functions ---------------------------------------------------------------------------- */
403
404#define CDL_TCB_CTable_Slot         0
405#define CDL_TCB_VTable_Slot         1
406#define CDL_TCB_Reply_Slot          2
407#define CDL_TCB_Caller_Slot         3
408#define CDL_TCB_IPCBuffer_Slot      4
409#define CDL_TCB_FaultEP_Slot        5
410#define CDL_TCB_SC_Slot             6
411#define CDL_TCB_TemporalFaultEP_Slot   7
412
413#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
414#define CDL_TCB_VCPU_SLOT           8
415#endif
416
417#define CDL_CapData_MakeGuard(x, y) \
418{ .tag = CDL_CapData_Guard, .guard_bits = (y), .guard_size = (x) }
419
420static inline CDL_CapType    CDL_Cap_Type(CDL_Cap *cap)
421{
422    return cap->type;
423}
424static inline CDL_CapData    CDL_Cap_Data(CDL_Cap *cap)
425{
426    return cap->data;
427}
428static inline seL4_ARCH_VMAttributes CDL_Cap_VMAttributes(CDL_Cap *cap)
429{
430    return cap->vm_attribs;
431}
432static inline CDL_ObjID      CDL_Cap_ObjID(CDL_Cap *cap)
433{
434    return cap->obj_id;
435}
436static inline CDL_CapRights  CDL_Cap_Rights(CDL_Cap *cap)
437{
438    return cap->rights;
439}
440static inline CDL_IRQ        CDL_Cap_IRQ(CDL_Cap *cap)
441{
442    return cap->irq;
443}
444static inline bool           CDL_Cap_IsOrig(CDL_Cap *cap)
445{
446    return cap->is_orig;
447}
448
449static inline seL4_Word      CDL_CapSlot_Slot(CDL_CapSlot *cap_slot)
450{
451    return cap_slot->slot;
452}
453static inline CDL_Cap       *CDL_CapSlot_Cap(CDL_CapSlot *cap_slot)
454{
455    return &cap_slot->cap;
456}
457
458static inline seL4_Word      CDL_ObjSlot_Slot(CDL_ObjSlot *obj_slot)
459{
460    return obj_slot->slot;
461}
462static inline CDL_ObjID      CDL_ObjSlot_ObjID(CDL_ObjSlot *obj_slot)
463{
464    return obj_slot->id;
465}
466
467/* Returns the sel4utils representation of a CDL_Cap's rights */
468static inline seL4_CapRights_t CDL_seL4_Cap_Rights(CDL_Cap *cap)
469{
470    return seL4_CapRights_new(!!(cap->rights & CDL_CanGrantReply),
471                              !!(cap->rights & CDL_CanGrant),
472                              !!(cap->rights & CDL_CanRead),
473                              !!(cap->rights & CDL_CanWrite));
474}
475
476static inline const char *CDL_Obj_Name(CDL_Object *obj)
477{
478#ifdef CONFIG_DEBUG_BUILD
479    if (obj->name == NULL) {
480        return "<unnamed>";
481    } else {
482        return obj->name;
483    }
484#else
485    return "<unnamed>";
486#endif
487}
488
489static inline CDL_ObjectType CDL_Obj_Type(CDL_Object *obj)
490{
491    return obj->type;
492}
493static inline seL4_Word      CDL_Obj_SizeBits(CDL_Object *obj)
494{
495    return obj->size_bits;
496}
497
498static inline seL4_Word CDL_Obj_Paddr(CDL_Object *obj)
499{
500    switch (obj->type) {
501    case CDL_Frame:
502        return obj->frame_extra.paddr;
503    case CDL_Untyped:
504        return obj->paddr;
505    default:
506        return 0;
507    }
508}
509
510static inline seL4_Word      CDL_Obj_NumSlots(CDL_Object *obj)
511{
512    return obj->slots.num;
513}
514static inline CDL_CapSlot *CDL_Obj_GetSlot(CDL_Object *obj, seL4_Word i)
515{
516    return &obj->slots.slot[i];
517}
518
519static inline seL4_Word CDL_TCB_IPCBuffer_Addr(CDL_Object *obj)
520{
521    return obj->tcb_extra.ipcbuffer_addr;
522}
523
524static inline uint8_t CDL_TCB_Priority(CDL_Object *obj)
525{
526    return obj->tcb_extra.priority;
527}
528
529static inline uint8_t CDL_CB_Bank(CDL_Object *obj)
530{
531    return obj->cb_extra.bank;
532}
533
534static inline uint8_t CDL_TCB_MaxPriority(CDL_Object *obj)
535{
536    return obj->tcb_extra.max_priority;
537}
538
539static inline uint8_t CDL_TCB_Affinity(CDL_Object *obj)
540{
541    return obj->tcb_extra.affinity;
542}
543
544static inline uint32_t CDL_TCB_Domain(CDL_Object *obj)
545{
546    return obj->tcb_extra.domain;
547}
548
549static inline seL4_Word CDL_TCB_PC(CDL_Object *obj)
550{
551    return obj->tcb_extra.pc;
552}
553
554static inline seL4_Word CDL_TCB_SP(CDL_Object *obj)
555{
556    return obj->tcb_extra.sp;
557}
558
559static inline const char *CDL_TCB_ElfName(CDL_Object *obj)
560{
561    return obj->tcb_extra.elf_name;
562}
563
564static inline uint64_t CDL_SC_Period(CDL_Object *obj)
565{
566    return obj->sc_extra.period;
567}
568
569static inline uint64_t CDL_SC_Budget(CDL_Object *obj)
570{
571    return obj->sc_extra.budget;
572}
573
574static inline seL4_Word CDL_SC_Data(CDL_Object *obj)
575{
576    return obj->sc_extra.data;
577}
578