1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8#include <bootinfo.h>
9#include <arch/bootinfo.h>
10
11#ifndef CONFIG_ARCH_ARM
12#define MAX_NUM_FREEMEM_REG 16
13#else
14/* Modifiers:
15 *  + 1: allow the kernel to release its own boot data region
16 *  + 1: possible gap between ELF images and rootserver objects;
17 *       see arm/arch_init_freemem */
18#define MAX_NUM_FREEMEM_REG (ARRAY_SIZE(avail_p_regs) + MODE_RESERVED + 1 + 1)
19#endif
20
21/*
22 * Resolve naming differences between the abstract specifications
23 * of the bootstrapping phase and the runtime phase of the kernel.
24 */
25typedef cte_t  slot_t;
26typedef cte_t *slot_ptr_t;
27#define SLOT_PTR(pptr, pos) (((slot_ptr_t)(pptr)) + (pos))
28#define pptr_of_cap (pptr_t)cap_get_capPtr
29
30/* (node-local) state accessed only during bootstrapping */
31
32typedef struct ndks_boot {
33    p_region_t reserved[MAX_NUM_RESV_REG];
34    word_t resv_count;
35    region_t   freemem[MAX_NUM_FREEMEM_REG];
36    seL4_BootInfo      *bi_frame;
37    seL4_SlotPos slot_pos_cur;
38    seL4_SlotPos slot_pos_max;
39} ndks_boot_t;
40
41extern ndks_boot_t ndks_boot;
42
43/* function prototypes */
44
45static inline bool_t is_reg_empty(region_t reg)
46{
47    return reg.start == reg.end;
48}
49
50void init_freemem(word_t n_available, const p_region_t *available,
51                  word_t n_reserved, region_t *reserved,
52                  v_region_t it_v_reg, word_t extra_bi_size_bits);
53bool_t reserve_region(p_region_t reg);
54bool_t insert_region(region_t reg);
55void write_slot(slot_ptr_t slot_ptr, cap_t cap);
56cap_t create_root_cnode(void);
57bool_t provide_cap(cap_t root_cnode_cap, cap_t cap);
58cap_t create_it_asid_pool(cap_t root_cnode_cap);
59void write_it_pd_pts(cap_t root_cnode_cap, cap_t it_pd_cap);
60bool_t create_idle_thread(void);
61bool_t create_untypeds_for_region(cap_t root_cnode_cap, bool_t device_memory, region_t reg,
62                                  seL4_SlotPos first_untyped_slot);
63bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before);
64bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg, seL4_SlotPos first_untyped_slot);
65void bi_finalise(void);
66void create_domain_cap(cap_t root_cnode_cap);
67
68cap_t create_ipcbuf_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr);
69word_t calculate_extra_bi_size_bits(word_t extra_size);
70void populate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr,
71                       word_t extra_bi_size_bits);
72void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr);
73
74#ifdef CONFIG_KERNEL_MCS
75bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes);
76#endif
77
78typedef struct create_frames_of_region_ret {
79    seL4_SlotRegion region;
80    bool_t success;
81} create_frames_of_region_ret_t;
82
83create_frames_of_region_ret_t
84create_frames_of_region(
85    cap_t    root_cnode_cap,
86    cap_t    pd_cap,
87    region_t reg,
88    bool_t   do_map,
89    sword_t  pv_offset
90);
91
92cap_t
93create_it_pd_pts(
94    cap_t      root_cnode_cap,
95    v_region_t ui_v_reg,
96    vptr_t     ipcbuf_vptr,
97    vptr_t     bi_frame_vptr
98);
99
100tcb_t *
101create_initial_thread(
102    cap_t  root_cnode_cap,
103    cap_t  it_pd_cap,
104    vptr_t ui_v_entry,
105    vptr_t bi_frame_vptr,
106    vptr_t ipcbuf_vptr,
107    cap_t  ipcbuf_cap
108);
109
110void init_core_state(tcb_t *scheduler_action);
111
112/* state tracking the memory allocated for root server objects */
113typedef struct {
114    pptr_t cnode;
115    pptr_t vspace;
116    pptr_t asid_pool;
117    pptr_t ipc_buf;
118    pptr_t boot_info;
119    pptr_t extra_bi;
120    pptr_t tcb;
121#ifdef CONFIG_KERNEL_MCS
122    pptr_t sc;
123#endif
124    region_t paging;
125} rootserver_mem_t;
126
127extern rootserver_mem_t rootserver;
128
129/* get the number of paging structures required to cover it_v_reg, with
130 * the paging structure covering `bits` of the address range - for a 4k page
131 * `bits` would be 12 */
132static inline BOOT_CODE word_t get_n_paging(v_region_t v_reg, word_t bits)
133{
134    vptr_t start = ROUND_DOWN(v_reg.start, bits);
135    vptr_t end = ROUND_UP(v_reg.end, bits);
136    return (end - start) / BIT(bits);
137}
138
139/* allocate a page table sized structure from rootserver.paging */
140static inline BOOT_CODE pptr_t it_alloc_paging(void)
141{
142    pptr_t allocated = rootserver.paging.start;
143    rootserver.paging.start += BIT(seL4_PageTableBits);
144    assert(rootserver.paging.start <= rootserver.paging.end);
145    return allocated;
146}
147
148/* return the amount of paging structures required to cover v_reg */
149word_t arch_get_n_paging(v_region_t it_veg);
150
151/* Create pptrs for all root server objects, starting at pptr, to cover the
152 * virtual memory region v_reg, and any extra boot info. */
153void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits);
154