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#include <autoconf.h>
14#include <sel4/types.h>
15#include <sel4/sel4.h>
16#include <stdio.h>
17#include <allocman/allocman.h>
18#include <allocman/cspace/simple1level.h>
19#include <allocman/mspace/fixed_pool.h>
20#include <allocman/utspace/twinkle.h>
21#include <allocman/cspace/two_level.h>
22#include <allocman/mspace/virtual_pool.h>
23#include <allocman/utspace/trickle.h>
24#include <allocman/bootstrap.h>
25#include <allocman/cspaceops.h>
26#include <string.h>
27#include <sel4utils/vspace.h>
28#include <allocman/vka.h>
29
30#define VIRTUAL_START 0xA0000000
31
32#define MEM_POOL_SIZE (1*1024*1024)
33
34static char initial_mem_pool[MEM_POOL_SIZE];
35
36allocman_t *test_use_current_cspace_bootinfo() {
37    int error;
38    allocman_t *allocman;
39    vspace_alloc_t vspace;
40    vka_t *vka;
41    allocman = bootstrap_use_bootinfo(seL4_GetBootInfo(), sizeof(initial_mem_pool), initial_mem_pool);
42    assert(allocman);
43    vka = allocman_mspace_alloc(allocman, sizeof(*vka), &error);
44    assert(!error);
45    allocman_make_vka(vka, allocman);
46    sel4util_get_vspace_alloc_leaky(&vspace, seL4_CapInitThreadPD, vka, seL4_GetBootInfo());
47
48    reservation_t *reservation = vspace_reserve_range_at(&vspace, VIRTUAL_START, MEM_POOL_SIZE, seL4_AllRights, 1);
49    assert(reservation);
50
51    bootstrap_configure_virtual_pool(allocman, VIRTUAL_START, MEM_POOL_SIZE, seL4_CapInitThreadPD);
52    error = allocman_fill_reserves(allocman);
53    assert(!error);
54    return allocman;
55}
56
57void test_use_current_1level_cspace() {
58    int error;
59    seL4_CPtr i;
60    allocman_t *allocman;
61    seL4_BootInfo *bi = seL4_GetBootInfo();
62    allocman = bootstrap_use_current_1level(seL4_CapInitThreadCNode, bi->initThreadCNodeSizeBits, bi->empty.start, bi->empty.end, sizeof(initial_mem_pool), initial_mem_pool);
63    assert(allocman);
64    /* have to add all our resources manually */
65    for (i = bi->untyped.start; i < bi->untyped.end; i++) {
66        cspacepath_t slot = allocman_cspace_make_path(allocman, i);
67        uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start];
68        uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start];
69        error = allocman_utspace_add_uts(allocman, 1, &slot, &size_bits, &paddr);
70        assert(!error);
71    }
72    error = allocman_fill_reserves(allocman);
73    assert(!error);
74}
75
76void test_use_current_cspace() {
77    int error;
78    seL4_CPtr i;
79    allocman_t *allocman;
80    cspace_single_level_t *cspace;
81    utspace_trickle_t *utspace;
82    seL4_BootInfo *bi = seL4_GetBootInfo();
83    allocman = bootstrap_create_allocman(sizeof(initial_mem_pool), initial_mem_pool);
84    assert(allocman);
85    /* construct a description of our current cspace */
86    cspace = allocman_mspace_alloc(allocman, sizeof(*cspace), &error);
87    assert(!error);
88    error = cspace_single_level_create(allocman, cspace, (struct cspace_single_level_config) {
89        .cnode = seL4_CapInitThreadCNode,
90        .cnode_size_bits = bi->initThreadCNodeSizeBits,
91        .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits,
92        .first_slot = bi->empty.start,
93        .end_slot = bi->empty.end
94    });
95    assert(!error);
96
97    error = allocman_attach_cspace(allocman, cspace_single_level_make_interface(cspace));
98    assert(!error);
99
100    utspace = allocman_mspace_alloc(allocman, sizeof(*utspace), &error);
101    assert(!error);
102    error = allocman_attach_utspace(allocman, utspace_trickle_make_interface(utspace));
103    assert(!error);
104
105    /* have to add all our resources manually */
106    for (i = bi->untyped.start; i < bi->untyped.end; i++) {
107        cspacepath_t slot = allocman_cspace_make_path(allocman, i);
108        uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start];
109        uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start];
110        error = allocman_utspace_add_uts(allocman, 1, &slot, &size_bits);
111        assert(!error);
112    }
113    error = allocman_fill_reserves(allocman);
114    assert(!error);
115}
116
117void test_new_1level_cspace_bootinfo() {
118    int error;
119    allocman_t *allocman;
120    cspace_simple1level_t *boot_cspace;
121    cspacepath_t new_path;
122    allocman = bootstrap_new_1level_bootinfo(seL4_GetBootInfo(), 14, sizeof(initial_mem_pool), initial_mem_pool, &boot_cspace);
123    assert(allocman);
124    error = allocman_fill_reserves(allocman);
125    assert(!error);
126    /* test we can easily use our old cspace */
127    error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(boot_cspace), seL4_CapInitThreadTCB, &new_path);
128    assert(!error);
129    /* drop our priority */
130    error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100);
131    assert(error == seL4_NoError);
132    /* no longer need that boot cspace information */
133    allocman_mspace_free(allocman, boot_cspace, sizeof(*boot_cspace));
134}
135
136void test_new_1level_cspace() {
137    bootstrap_info_t *bootstrap;
138    seL4_BootInfo *bi = seL4_GetBootInfo();
139    cspace_simple1level_t boot_cspace;
140    allocman_t *allocman;
141    cspacepath_t oldroot;
142    cspacepath_t currentroot;
143    cspacepath_t new_path;
144    cspacepath_t tcb;
145    cspacepath_t pd;
146    seL4_CPtr i;
147    int error;
148    bootstrap = bootstrap_create_info(sizeof(initial_mem_pool), initial_mem_pool);
149    assert(bootstrap);
150    /* describe the current cspace */
151    cspace_simple1level_create(&boot_cspace, (struct cspace_simple1level_config){
152        .cnode = seL4_CapInitThreadCNode,
153        .cnode_size_bits = bi->initThreadCNodeSizeBits,
154        .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits,
155        .first_slot = bi->empty.start,
156        .end_slot = bi->empty.end - 1
157    });
158    /* pass to the boot strapper */
159    currentroot = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadCNode);
160    bootstrap_set_boot_cspace(bootstrap, cspace_simple1level_make_interface(&boot_cspace), currentroot);
161    /* give the untypeds to the bootstrapper */
162    for (i = bi->untyped.start; i < bi->untyped.end; i++) {
163        cspacepath_t slot = _cspace_simple1level_make_path(&boot_cspace, i);
164        uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start];
165        uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start];
166        error = bootstrap_add_untypeds(bootstrap, 1, &slot, &size_bits, &paddr);
167        assert(!error);
168    }
169    /* bootstrapper has enough information to create */
170    tcb = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadTCB);
171    pd = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadPD);
172    allocman = bootstrap_new_1level(bootstrap, 14, tcb, pd, &oldroot);
173    assert(allocman);
174    /* take advantage of knowledge of simple1level cspace and just shift its root :) */
175    assert(oldroot.capDepth == 32);
176    boot_cspace.config.cnode = oldroot.capPtr;
177    /* now test we can use it */
178    error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(&boot_cspace), seL4_CapInitThreadTCB, &new_path);
179    assert(!error);
180    /* drop our priority */
181    error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100);
182    assert(error == seL4_NoError);
183}
184
185void test_new_2level_cspace_bootinfo() {
186    int error;
187    allocman_t *allocman;
188    cspace_simple1level_t *boot_cspace;
189    cspacepath_t new_path;
190    allocman = bootstrap_new_2level_bootinfo(seL4_GetBootInfo(), 6,10, sizeof(initial_mem_pool), initial_mem_pool, &boot_cspace);
191    assert(allocman);
192    error = allocman_fill_reserves(allocman);
193    assert(!error);
194    /* test we can easily use our old cspace */
195    error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(boot_cspace), seL4_CapInitThreadTCB, &new_path);
196    assert(!error);
197    /* drop our priority */
198    error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100);
199    assert(error == seL4_NoError);
200    /* no longer need that boot cspace information */
201    allocman_mspace_free(allocman, boot_cspace, sizeof(*boot_cspace));
202}
203
204void test_new_2level_cspace() {
205    bootstrap_info_t *bootstrap;
206    seL4_BootInfo *bi = seL4_GetBootInfo();
207    cspace_simple1level_t boot_cspace;
208    allocman_t *allocman;
209    cspacepath_t oldroot;
210    cspacepath_t currentroot;
211    cspacepath_t new_path;
212    cspacepath_t tcb;
213    cspacepath_t pd;
214    seL4_CPtr i;
215    int error;
216    bootstrap = bootstrap_create_info(sizeof(initial_mem_pool), initial_mem_pool);
217    assert(bootstrap);
218    /* describe the current cspace */
219    cspace_simple1level_create(&boot_cspace, (struct cspace_simple1level_config){
220        .cnode = seL4_CapInitThreadCNode,
221        .cnode_size_bits = bi->initThreadCNodeSizeBits,
222        .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits,
223        .first_slot = bi->empty.start,
224        .end_slot = bi->empty.end - 1
225    });
226    /* pass to the boot strapper */
227    currentroot = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadCNode);
228    bootstrap_set_boot_cspace(bootstrap, cspace_simple1level_make_interface(&boot_cspace), currentroot);
229    /* give the untypeds to the bootstrapper */
230    for (i = bi->untyped.start; i < bi->untyped.end; i++) {
231        cspacepath_t slot = _cspace_simple1level_make_path(&boot_cspace, i);
232        uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start];
233        uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start];
234        error = bootstrap_add_untypeds(bootstrap, 1, &slot, &size_bits, &paddr);
235        assert(!error);
236    }
237    /* bootstrapper has enough information to create */
238    tcb = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadTCB);
239    pd = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadPD);
240    allocman = bootstrap_new_2level(bootstrap, 6, 10, tcb, pd, &oldroot);
241    assert(allocman);
242    /* take advantage of knowledge of simple1level cspace and just shift its root :) */
243    assert(oldroot.capDepth == 32);
244    boot_cspace.config.cnode = oldroot.capPtr;
245    /* now test we can use it */
246    error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(&boot_cspace), seL4_CapInitThreadTCB, &new_path);
247    assert(!error);
248    /* drop our priority */
249    error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100);
250    assert(error == seL4_NoError);
251}
252
253int main(void) {
254    allocman_t *alloc;
255    alloc = test_use_current_cspace_bootinfo();
256//    test_use_current_1level_cspace();
257//    test_use_current_cspace();
258//    test_new_1level_cspace_bootinfo();
259//    test_new_1level_cspace();
260//    test_new_2level_cspace_bootinfo();
261//    test_new_2level_cspace();
262    printf("All is well in the universe.\n");
263    while(1);
264}
265