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_BOOTINFO_TYPES_H
14#define __LIBSEL4_BOOTINFO_TYPES_H
15
16/* caps with fixed slot positions in the root CNode */
17
18enum {
19    seL4_CapNull                =  0, /* null cap */
20    seL4_CapInitThreadTCB       =  1, /* initial thread's TCB cap */
21    seL4_CapInitThreadCNode     =  2, /* initial thread's root CNode cap */
22    seL4_CapInitThreadVSpace    =  3, /* initial thread's VSpace cap */
23    seL4_CapIRQControl          =  4, /* global IRQ controller cap */
24    seL4_CapASIDControl         =  5, /* global ASID controller cap */
25    seL4_CapInitThreadASIDPool  =  6, /* initial thread's ASID pool cap */
26    seL4_CapIOPortControl       =  7, /* global IO port control cap (null cap if not supported) */
27    seL4_CapIOSpace             =  8, /* global IO space cap (null cap if no IOMMU support) */
28    seL4_CapBootInfoFrame       =  9, /* bootinfo frame cap */
29    seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
30    seL4_CapDomain              = 11, /* global domain controller cap */
31    seL4_NumInitialCaps         = 12
32};
33
34/* Legacy code will have assumptions on the vspace root being a Page Directory
35 * type, so for now we define one to the other */
36#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
37
38/* types */
39typedef seL4_Word seL4_SlotPos;
40
41typedef struct {
42    seL4_SlotPos start; /* first CNode slot position OF region */
43    seL4_SlotPos end;   /* first CNode slot position AFTER region */
44} seL4_SlotRegion;
45
46typedef struct {
47    seL4_Word  paddr;   /* physical address of untyped cap  */
48    seL4_Uint8 padding1;
49    seL4_Uint8 padding2;
50    seL4_Uint8 sizeBits;/* size (2^n) bytes of each untyped */
51    seL4_Uint8 isDevice;/* whether the untyped is a device  */
52} seL4_UntypedDesc;
53
54typedef struct {
55    seL4_Word         extraLen;        /* length of any additional bootinfo information */
56    seL4_NodeId       nodeID;          /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
57    seL4_Word         numNodes;        /* number of seL4 nodes (1 if uniprocessor) */
58    seL4_Word         numIOPTLevels;   /* number of IOMMU PT levels (0 if no IOMMU support) */
59    seL4_IPCBuffer*   ipcBuffer;       /* pointer to initial thread's IPC buffer */
60    seL4_SlotRegion   empty;           /* empty slots (null caps) */
61    seL4_SlotRegion   sharedFrames;    /* shared-frame caps (shared between seL4 nodes) */
62    seL4_SlotRegion   userImageFrames; /* userland-image frame caps */
63    seL4_SlotRegion   userImagePaging; /* userland-image paging structure caps */
64    seL4_SlotRegion   ioSpaceCaps;     /* IOSpace caps for ARM SMMU */
65    seL4_SlotRegion   extraBIPages;    /* caps for any pages used to back the additional bootinfo information */
66    seL4_Word         initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
67    seL4_Domain       initThreadDomain; /* Initial thread's domain ID */
68    seL4_SlotRegion   untyped;         /* untyped-object caps (untyped caps) */
69    seL4_UntypedDesc  untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* information about each untyped */
70    /* the untypedList should be the last entry in this struct, in order
71     * to make this struct easier to represent in other languages */
72} seL4_BootInfo;
73
74/* If extraLen > 0 then 4K after the start of bootinfo is a region of extraLen additional
75 * bootinfo structures. Bootinfo structures are arch/platform specific and may or may not
76 * exist in any given execution. */
77typedef struct {
78    /* identifier of the following chunk. IDs are arch/platform specific */
79    seL4_Word id;
80    /* length of the chunk, including this header */
81    seL4_Word len;
82} seL4_BootInfoHeader;
83
84/* Bootinfo identifiers share a global namespace, even if they are arch or platform specific
85 * and are enumerated here */
86#define SEL4_BOOTINFO_HEADER_PADDING 0
87#define SEL4_BOOTINFO_HEADER_X86_VBE 1
88#define SEL4_BOOTINFO_HEADER_X86_MBMMAP 2
89#define SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP 3
90#define SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER 4
91#define SEL4_BOOTINFO_HEADER_X86_TSC_FREQ 5 // frequency is in mhz
92
93#endif // __LIBSEL4_BOOTINFO_TYPES_H
94