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 15#include <stdio.h> 16#include <stdlib.h> 17#include <assert.h> 18#include <arch_stdio.h> 19#include <allocman/vka.h> 20#include <allocman/bootstrap.h> 21 22#include <sel4/sel4.h> 23#include <sel4/types.h> 24 25#include <sel4platsupport/timer.h> 26 27#include <sel4utils/util.h> 28#include <sel4utils/mapping.h> 29#include <sel4utils/vspace.h> 30 31#include <sel4test/test.h> 32 33#include <vka/capops.h> 34 35#include "helpers.h" 36#include "test.h" 37#include "init.h" 38 39/* dummy global for libsel4muslcsys */ 40char _cpio_archive[1]; 41char _cpio_archive_end[1]; 42 43/* endpoint to call back to the test driver on */ 44static seL4_CPtr endpoint; 45 46/* global static memory for init */ 47static sel4utils_alloc_data_t alloc_data; 48 49/* dimensions of virtual memory for the allocator to use */ 50#define ALLOCATOR_VIRTUAL_POOL_SIZE ((1 << seL4_PageBits) * 4000) 51 52/* allocator static pool */ 53#define ALLOCATOR_STATIC_POOL_SIZE ((1 << seL4_PageBits) * 20) 54static char allocator_mem_pool[ALLOCATOR_STATIC_POOL_SIZE]; 55 56/* override abort, called by exit (and assert fail) */ 57void abort(void) 58{ 59 /* send back a failure */ 60 seL4_MessageInfo_t info = seL4_MessageInfo_new(seL4_Fault_NullFault, 0, 0, 1); 61 seL4_SetMR(0, -1); 62 seL4_Send(endpoint, info); 63 64 /* we should not get here */ 65 assert(0); 66 while (1); 67} 68 69void __plat_putchar(int c); 70static size_t write_buf(void *data, size_t count) 71{ 72 char *buf = data; 73 for (int i = 0; i < count; i++) { 74 __plat_putchar(buf[i]); 75 } 76 return count; 77} 78 79static testcase_t *find_test(const char *name) 80{ 81 testcase_t *test = sel4test_get_test(name); 82 if (test == NULL) { 83 ZF_LOGF("Failed to find test %s", name); 84 } 85 86 return test; 87} 88 89static void init_allocator(env_t env, test_init_data_t *init_data) 90{ 91 UNUSED int error; 92 UNUSED reservation_t virtual_reservation; 93 94 /* initialise allocator */ 95 allocman_t *allocator = bootstrap_use_current_1level(init_data->root_cnode, 96 init_data->cspace_size_bits, init_data->free_slots.start, 97 init_data->free_slots.end, ALLOCATOR_STATIC_POOL_SIZE, 98 allocator_mem_pool); 99 if (allocator == NULL) { 100 ZF_LOGF("Failed to bootstrap allocator"); 101 } 102 allocman_make_vka(&env->vka, allocator); 103 104 /* fill the allocator with untypeds */ 105 seL4_CPtr slot; 106 unsigned int size_bits_index; 107 size_t size_bits; 108 cspacepath_t path; 109 for (slot = init_data->untypeds.start, size_bits_index = 0; 110 slot <= init_data->untypeds.end; 111 slot++, size_bits_index++) { 112 113 vka_cspace_make_path(&env->vka, slot, &path); 114 /* allocman doesn't require the paddr unless we need to ask for phys addresses, 115 * which we don't. */ 116 size_bits = init_data->untyped_size_bits_list[size_bits_index]; 117 error = allocman_utspace_add_uts(allocator, 1, &path, &size_bits, NULL, 118 ALLOCMAN_UT_KERNEL); 119 if (error) { 120 ZF_LOGF("Failed to add untyped objects to allocator"); 121 } 122 } 123 124 /* add any arch specific objects to the allocator */ 125 arch_init_allocator(env, init_data); 126 127 /* create a vspace */ 128 void *existing_frames[init_data->stack_pages + 2]; 129 existing_frames[0] = (void *) init_data; 130 existing_frames[1] = seL4_GetIPCBuffer(); 131 assert(init_data->stack_pages > 0); 132 for (int i = 0; i < init_data->stack_pages; i++) { 133 existing_frames[i + 2] = init_data->stack + (i * PAGE_SIZE_4K); 134 } 135 136 error = sel4utils_bootstrap_vspace(&env->vspace, &alloc_data, init_data->page_directory, &env->vka, 137 NULL, NULL, existing_frames); 138 139 /* switch the allocator to a virtual memory pool */ 140 void *vaddr; 141 virtual_reservation = vspace_reserve_range(&env->vspace, ALLOCATOR_VIRTUAL_POOL_SIZE, 142 seL4_AllRights, 1, &vaddr); 143 if (virtual_reservation.res == 0) { 144 ZF_LOGF("Failed to switch allocator to virtual memory pool"); 145 } 146 147 bootstrap_configure_virtual_pool(allocator, vaddr, ALLOCATOR_VIRTUAL_POOL_SIZE, 148 env->page_directory); 149 150} 151 152static uint8_t cnode_size_bits(void *data) 153{ 154 test_init_data_t *init = (test_init_data_t *) data; 155 return init->cspace_size_bits; 156} 157 158static seL4_CPtr sched_ctrl(void *data, int core) 159{ 160 return ((test_init_data_t *) data)->sched_ctrl + core; 161} 162 163static int core_count(UNUSED void *data) 164{ 165 return ((test_init_data_t *) data)->cores; 166} 167 168void init_simple(env_t env, test_init_data_t *init_data) 169{ 170 /* minimal simple implementation */ 171 env->simple.data = (void *) init_data; 172 env->simple.arch_simple.data = (void *) init_data; 173 env->simple.init_cap = sel4utils_process_init_cap; 174 env->simple.cnode_size = cnode_size_bits; 175 env->simple.sched_ctrl = sched_ctrl; 176 env->simple.core_count = core_count; 177 178 arch_init_simple(env, &env->simple); 179} 180 181int main(int argc, char **argv) 182{ 183 sel4muslcsys_register_stdio_write_fn(write_buf); 184 185 test_init_data_t *init_data; 186 struct env env; 187 188 /* parse args */ 189 assert(argc == 2); 190 endpoint = (seL4_CPtr) atoi(argv[0]); 191 192 /* read in init data */ 193 init_data = (void *) atol(argv[1]); 194 195 /* configure env */ 196 env.cspace_root = init_data->root_cnode; 197 env.page_directory = init_data->page_directory; 198 env.endpoint = endpoint; 199 env.priority = init_data->priority; 200 env.cspace_size_bits = init_data->cspace_size_bits; 201 env.tcb = init_data->tcb; 202 env.domain = init_data->domain; 203 env.asid_pool = init_data->asid_pool; 204 env.asid_ctrl = init_data->asid_ctrl; 205 env.sched_ctrl = init_data->sched_ctrl; 206#ifdef CONFIG_IOMMU 207 env.io_space = init_data->io_space; 208#endif 209#ifdef CONFIG_TK1_SMMU 210 env.io_space_caps = init_data->io_space_caps; 211#endif 212 env.cores = init_data->cores; 213 env.num_regions = init_data->num_elf_regions; 214 memcpy(env.regions, init_data->elf_regions, sizeof(sel4utils_elf_region_t) * env.num_regions); 215 216 env.timer_notification.cptr = init_data->timer_ntfn; 217 218 env.device_frame = init_data->device_frame_cap; 219 220 /* initialse cspace, vspace and untyped memory allocation */ 221 init_allocator(&env, init_data); 222 223 /* initialise simple */ 224 init_simple(&env, init_data); 225 226 /* initialise rpc client */ 227 sel4rpc_client_init(&env.rpc_client, env.endpoint, SEL4TEST_PROTOBUF_RPC); 228 229 /* find the test */ 230 testcase_t *test = find_test(init_data->name); 231 232 /* run the test */ 233 sel4test_reset(); 234 test_result_t result = SUCCESS; 235 if (test) { 236 printf("Running test %s (%s)\n", test->name, test->description); 237 result = test->function((uintptr_t)&env); 238 } else { 239 result = FAILURE; 240 ZF_LOGF("Cannot find test %s\n", init_data->name); 241 } 242 243 printf("Test %s %s\n", init_data->name, result == SUCCESS ? "passed" : "failed"); 244 /* send our result back */ 245 seL4_MessageInfo_t info = seL4_MessageInfo_new(seL4_Fault_NullFault, 0, 0, 1); 246 seL4_SetMR(0, result); 247 seL4_Send(endpoint, info); 248 249 /* It is expected that we are torn down by the test driver before we are 250 * scheduled to run again after signalling them with the above send. 251 */ 252 assert(!"unreachable"); 253 return 0; 254} 255