| /* | |
| * Copyright 2014, NICTA | |
| * | |
| * This software may be distributed and modified according to the terms of | |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. | |
| * See "LICENSE_BSD2.txt" for details. | |
| * | |
| * @TAG(NICTA_BSD) | |
| */ | |
| #include <autoconf.h> | |
| #if defined CONFIG_LIB_SEL4_VSPACE && defined CONFIG_LIB_SEL4_VKA | |
| #include <stdlib.h> | |
| #include <string.h> | |
| #include <vka/vka.h> | |
| #include <vka/capops.h> | |
| #include <sel4utils/vspace.h> | |
| #include <sel4utils/vspace_internal.h> | |
| #ifdef CONFIG_KERNEL_STABLE | |
| #include <sel4/arch/bootinfo.h> | |
| #endif | |
| /* For the initial vspace, we must always guarantee we have virtual memory available | |
| * for each bottom level page table. Future vspaces can then use the initial vspace | |
| * to allocate bottom level page tables until memory runs out. | |
| * | |
| * The initial vspace then looks like this: | |
| * 0xffffffff ↑ | |
| * | kernel code | |
| * 0xe0000000 ↓ | |
| * 0xdfffffff ↑ | |
| * | bottom level page tables | |
| * 0xdf800000 ↓ | |
| * 0xdf7fffff ↑ | |
| * | top level page table | |
| * 0xdf7ff000 ↓ | |
| * 0xdf7fefff ↑ | |
| * | available address space | |
| * 0x00001000 ↓ | |
| * 0x00000fff ↑ | |
| * | reserved (null page) | |
| * 0x00000000 ↓ | |
| * | |
| * The following constants come from the above layout. | |
| */ | |
| /* reserve enough virtual memory just below the kernel window such that there is enough | |
| * space to create all possible bottom level structures. This amount of memory is therefore | |
| * size of second level structure * number of second level structures | |
| * where number of second level structures is equivalent to number of bits in the top level translation */ | |
| #define FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR (KERNEL_RESERVED_START - sizeof(bottom_level_t) * VSPACE_LEVEL_SIZE) | |
| /* we also need some memory for top level structure. place that just below all our bottom | |
| level page tables. no good way of specifying the size, will assume one page */ | |
| #define TOP_LEVEL_PAGE_TABLE_VADDR (FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR - PAGE_SIZE_4K) | |
| /* when bootstrapping we need to allocate 1 bottom level page table to store the top level page table | |
| * index in, and enough bottom levels to store indexes of all possible bottom levels */ | |
| #define INITIAL_BOTTOM_LEVEL_PAGES 6 | |
| #define INITIAL_BOTTOM_LEVEL_TABLES (INITIAL_BOTTOM_LEVEL_PAGES / PAGES_FOR_BOTTOM_LEVEL) | |
| /* sanity checks - check our constants above are what we say they are */ | |
| #if !defined(CONFIG_X86_64) && !defined(CONFIG_PAE_PAGING) | |
| compile_time_assert(sel4utils_vspace_1, TOP_LEVEL_INDEX(TOP_LEVEL_PAGE_TABLE_VADDR) == 893); | |
| compile_time_assert(sel4utils_vspace_2, BOTTOM_LEVEL_INDEX(TOP_LEVEL_PAGE_TABLE_VADDR) == 1023); | |
| compile_time_assert(sel4utils_vspace_3, TOP_LEVEL_INDEX(FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR) == 894); | |
| compile_time_assert(sel4utils_vspace_4, BOTTOM_LEVEL_INDEX(FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR) == 0); | |
| #endif | |
| /* check our data structures are 4K*2 page sized like the rest of the code assumes they are */ | |
| compile_time_assert(bottom_level_8k, sizeof(bottom_level_t) == (PAGE_SIZE_4K * 2)); | |
| compile_time_assert(top_level_4k, sizeof(bottom_level_t *) * VSPACE_LEVEL_SIZE == PAGE_SIZE_4K); | |
| static int | |
| common_init(vspace_t *vspace, vka_t *vka, seL4_CPtr page_directory, | |
| vspace_allocated_object_fn allocated_object_fn, void *cookie) | |
| { | |
| sel4utils_alloc_data_t *data = get_alloc_data(vspace); | |
| data->vka = vka; | |
| data->last_allocated = 0x10000000; | |
| data->reservation_head = NULL; | |
| data->page_directory = page_directory; | |
| vspace->allocated_object = allocated_object_fn; | |
| vspace->allocated_object_cookie = cookie; | |
| return 0; | |
| } | |
| static void | |
| common_init_post_bootstrap(vspace_t *vspace, sel4utils_map_page_fn map_page) | |
| { | |
| sel4utils_alloc_data_t *data = get_alloc_data(vspace); | |
| /* reserve the kernel region, we do this by marking the | |
| * top level entry as RESERVED */ | |
| for (int i = TOP_LEVEL_INDEX(KERNEL_RESERVED_START); | |
| i <= TOP_LEVEL_INDEX(KERNEL_RESERVED_END); i++) { | |
| data->top_level[i] = (bottom_level_t *) RESERVED; | |
| } | |
| data->map_page = map_page; | |
| /* initialise the rest of the functions now that they are usable */ | |
| vspace->new_pages_at_vaddr = sel4utils_new_pages_at_vaddr; | |
| vspace->map_pages_at_vaddr = sel4utils_map_pages_at_vaddr; | |
| vspace->unmap_pages = sel4utils_unmap_pages; | |
| vspace->reserve_range_aligned = sel4utils_reserve_range_aligned; | |
| vspace->reserve_range_at = sel4utils_reserve_range_at; | |
| vspace->free_reservation = sel4utils_free_reservation; | |
| vspace->free_reservation_by_vaddr = sel4utils_free_reservation_by_vaddr; | |
| vspace->get_cap = sel4utils_get_cap; | |
| vspace->get_cookie = sel4utils_get_cookie; | |
| vspace->get_root = sel4utils_get_root; | |
| vspace->tear_down = sel4utils_tear_down; | |
| vspace->share_mem_at_vaddr = sel4utils_share_mem_at_vaddr; | |
| } | |
| static int | |
| reserve_range(vspace_t *vspace, uintptr_t start, uintptr_t end) | |
| { | |
| int pages = BYTES_TO_4K_PAGES(ROUND_UP(end, PAGE_SIZE_4K) - | |
| ROUND_DOWN(start, PAGE_SIZE_4K)); | |
| int error = 0; | |
| for (int i = 0; i < pages && error == 0; i++) { | |
| error = reserve_entries(vspace, start + (i * PAGE_SIZE_4K) , seL4_PageBits); | |
| } | |
| if (error) { | |
| LOG_ERROR("Error reserving range between %"PRIuPTR" and %"PRIuPTR, start, end); | |
| } | |
| return error; | |
| } | |
| /** | |
| * Symbols in this function need to be provided by your | |
| * crt0.S or your linker script, such that we can figure out | |
| * what virtual addresses are taken up by the current task | |
| */ | |
| void | |
| sel4utils_get_image_region(uintptr_t *va_start, uintptr_t *va_end) | |
| { | |
| extern char __executable_start[]; | |
| extern char _end[]; | |
| *va_start = (uintptr_t) __executable_start; | |
| *va_end = (uintptr_t) _end; | |
| *va_end = (uintptr_t) ROUND_UP(*va_end, PAGE_SIZE_4K); | |
| } | |
| static int | |
| reserve_initial_task_regions(vspace_t *vspace, void *existing_frames[]) | |
| { | |
| /* mark the code and data segments as used */ | |
| uintptr_t va_start, va_end; | |
| sel4utils_get_image_region(&va_start, &va_end); | |
| /* this is the scope of the virtual memory used by the image, including | |
| * data, text and stack */ | |
| if (reserve_range(vspace, va_start, va_end)) { | |
| LOG_ERROR("Error reserving code/data segment"); | |
| return -1; | |
| } | |
| /* mark boot info as used */ | |
| if (existing_frames != NULL) { | |
| for (int i = 0; existing_frames[i] != NULL; i++) { | |
| if (reserve_range(vspace, (uintptr_t) existing_frames[i], (uintptr_t) existing_frames[i] | |
| + PAGE_SIZE_4K)) { | |
| LOG_ERROR("Error reserving frame at %p", existing_frames[i]); | |
| return -1; | |
| } | |
| } | |
| } | |
| return 0; | |
| } | |
| static int | |
| alloc_and_map_bootstrap_frame(vspace_t *vspace, vka_object_t *frame, void *vaddr) | |
| { | |
| sel4utils_alloc_data_t *data = get_alloc_data(vspace); | |
| int error = vka_alloc_frame(data->vka, seL4_PageBits, frame); | |
| if (error) { | |
| LOG_ERROR("Failed to allocate bootstrap frame, error: %d", error); | |
| return error; | |
| } | |
| vka_object_t objects[3]; | |
| int num = 3; | |
| error = sel4utils_map_page(data->vka, data->page_directory, frame->cptr, vaddr, | |
| seL4_AllRights, 1, objects, &num); | |
| if (error) { | |
| vka_free_object(data->vka, frame); | |
| LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error); | |
| return error; | |
| } | |
| /* Zero the memory */ | |
| memset(vaddr, 0, PAGE_SIZE_4K); | |
| for (int i = 0; i < num; i++) { | |
| vspace_maybe_call_allocated_object(vspace, objects[i]); | |
| } | |
| return seL4_NoError; | |
| } | |
| int | |
| bootstrap_create_level(vspace_t *vspace, uintptr_t vaddr) | |
| { | |
| sel4utils_alloc_data_t *data = get_alloc_data(vspace); | |
| UNUSED int error; | |
| uintptr_t pt_vaddr = data->next_bottom_level_vaddr; | |
| for (int i = 0; i < PAGES_FOR_BOTTOM_LEVEL; i++) { | |
| vka_object_t bottom_level = {0}; | |
| if (alloc_and_map_bootstrap_frame(vspace, &bottom_level, (void *) pt_vaddr) != seL4_NoError) { | |
| LOG_ERROR("Failed to bootstrap a level, everything is broken."); | |
| /* leak memory, can't really recover */ | |
| return -1; | |
| } | |
| error = update(vspace, pt_vaddr, bottom_level.cptr, bottom_level.ut); | |
| /* this cannot fail */ | |
| assert(error == seL4_NoError); | |
| pt_vaddr += PAGE_SIZE_4K; | |
| } | |
| data->top_level[TOP_LEVEL_INDEX(vaddr)] = (bottom_level_t *) data->next_bottom_level_vaddr; | |
| data->next_bottom_level_vaddr = pt_vaddr; | |
| return 0; | |
| } | |
| static int | |
| bootstrap_page_table(vspace_t *vspace) | |
| { | |
| sel4utils_alloc_data_t *data = get_alloc_data(vspace); | |
| /* First we allocate a page for the top level page table to live in */ | |
| vka_object_t top_level = {0}; | |
| if (alloc_and_map_bootstrap_frame(vspace, &top_level, (void *) TOP_LEVEL_PAGE_TABLE_VADDR)) { | |
| return -1; | |
| } | |
| /* set up the pointer to top level page table */ | |
| data->top_level = (bottom_level_t **) TOP_LEVEL_PAGE_TABLE_VADDR; | |
| vka_object_t bottom_levels[INITIAL_BOTTOM_LEVEL_PAGES]; | |
| uintptr_t vaddr = FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR; | |
| for (int i = 0; i < INITIAL_BOTTOM_LEVEL_PAGES; i++) { | |
| if (alloc_and_map_bootstrap_frame(vspace, &bottom_levels[i], (void *) vaddr)) { | |
| return -1; | |
| } | |
| vaddr += PAGE_SIZE_4K; | |
| } | |
| /* set up pointers to bottom level page tables */ | |
| vaddr = FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR; | |
| for (int i = 0; i < INITIAL_BOTTOM_LEVEL_TABLES; i++) { | |
| data->top_level[TOP_LEVEL_INDEX(TOP_LEVEL_PAGE_TABLE_VADDR) + i] = (void *) vaddr; | |
| vaddr += (PAGES_FOR_BOTTOM_LEVEL * PAGE_SIZE_4K); | |
| } | |
| /* now update those entries in our new page tables */ | |
| /* these cannot fail - failure is only caused by lack of a bottom level page table, | |
| * and we just allocated them. */ | |
| UNUSED int error = update(vspace, TOP_LEVEL_PAGE_TABLE_VADDR, top_level.cptr, top_level.ut); | |
| assert(error == seL4_NoError); | |
| vaddr = FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR; | |
| for (int i = 0; i < INITIAL_BOTTOM_LEVEL_PAGES; i++) { | |
| error = update(vspace, vaddr, bottom_levels[i].cptr, bottom_levels[i].ut); | |
| assert(error == seL4_NoError); | |
| vaddr += PAGE_SIZE_4K; | |
| } | |
| vaddr = FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR + (INITIAL_BOTTOM_LEVEL_PAGES * PAGE_SIZE_4K); | |
| data->next_bottom_level_vaddr = vaddr; | |
| /* reserve the rest of them */ | |
| for (int i = INITIAL_BOTTOM_LEVEL_PAGES; i < VSPACE_LEVEL_SIZE * PAGES_FOR_BOTTOM_LEVEL; i++) { | |
| assert(data->top_level[TOP_LEVEL_INDEX(vaddr)] != NULL); | |
| error = reserve(vspace, vaddr); | |
| assert(error == seL4_NoError); | |
| vaddr += PAGE_SIZE_4K; | |
| } | |
| return 0; | |
| } | |
| /* Interface functions */ | |
| int | |
| sel4utils_get_vspace_with_map(vspace_t *loader, vspace_t *new_vspace, sel4utils_alloc_data_t *data, | |
| vka_t *vka, seL4_CPtr page_directory, | |
| vspace_allocated_object_fn allocated_object_fn, void *allocated_object_cookie, sel4utils_map_page_fn map_page) | |
| { | |
| new_vspace->data = (void *) data; | |
| if (common_init(new_vspace, vka, page_directory, allocated_object_fn, allocated_object_cookie)) { | |
| return -1; | |
| } | |
| data->bootstrap = loader; | |
| /* create the top level page table from the loading vspace */ | |
| data->top_level = (bottom_level_t **) vspace_new_pages(loader, seL4_AllRights, 1, seL4_PageBits); | |
| if (data->top_level == NULL) { | |
| return -1; | |
| } | |
| common_init_post_bootstrap(new_vspace, map_page); | |
| return 0; | |
| } | |
| int | |
| sel4utils_get_vspace(vspace_t *loader, vspace_t *new_vspace, sel4utils_alloc_data_t *data, | |
| vka_t *vka, seL4_CPtr page_directory, | |
| vspace_allocated_object_fn allocated_object_fn, void *allocated_object_cookie) | |
| { | |
| return sel4utils_get_vspace_with_map(loader, new_vspace, data, vka, page_directory, allocated_object_fn, allocated_object_cookie, sel4utils_map_page_pd); | |
| } | |
| #ifdef CONFIG_VTX | |
| int sel4utils_get_vspace_ept(vspace_t *loader, vspace_t *new_vspace, vka_t *vka, | |
| seL4_CPtr ept, vspace_allocated_object_fn allocated_object_fn, void *allocated_object_cookie) | |
| { | |
| sel4utils_alloc_data_t *data = malloc(sizeof(*data)); | |
| if (!data) { | |
| return -1; | |
| } | |
| return sel4utils_get_vspace_with_map(loader, new_vspace, data, vka, ept, allocated_object_fn, allocated_object_cookie, sel4utils_map_page_ept); | |
| } | |
| #endif /* CONFIG_VTX */ | |
| int | |
| sel4utils_bootstrap_vspace(vspace_t *vspace, sel4utils_alloc_data_t *data, | |
| seL4_CPtr page_directory, vka_t *vka, | |
| vspace_allocated_object_fn allocated_object_fn, void *cookie, void *existing_frames[]) | |
| { | |
| vspace->data = (void *) data; | |
| if (common_init(vspace, vka, page_directory, allocated_object_fn, cookie)) { | |
| return -1; | |
| } | |
| data->bootstrap = NULL; | |
| if (bootstrap_page_table(vspace)) { | |
| return -1; | |
| } | |
| reserve_initial_task_regions(vspace, existing_frames); | |
| common_init_post_bootstrap(vspace, sel4utils_map_page_pd); | |
| return 0; | |
| } | |
| int | |
| sel4utils_bootstrap_vspace_with_bootinfo(vspace_t *vspace, sel4utils_alloc_data_t *data, | |
| seL4_CPtr page_directory, | |
| vka_t *vka, seL4_BootInfo *info, vspace_allocated_object_fn allocated_object_fn, | |
| void *allocated_object_cookie) | |
| { | |
| void *existing_frames[] = { | |
| (void *) info, | |
| #if defined(CONFIG_ARCH_IA32) && defined(CONFIG_KERNEL_STABLE) | |
| (void *) seL4_IA32_GetBootInfo(), | |
| #endif | |
| /* We assume the IPC buffer is less than a page and fits into one page */ | |
| (void *) (seL4_Word)ROUND_DOWN((uint32_t) ((seL4_Word)(info->ipcBuffer)), PAGE_SIZE_4K), | |
| NULL | |
| }; | |
| return sel4utils_bootstrap_vspace(vspace, data, page_directory, vka, allocated_object_fn, | |
| allocated_object_cookie, existing_frames); | |
| } | |
| int | |
| sel4utils_bootstrap_clone_into_vspace(vspace_t *current, vspace_t *clone, reservation_t image) | |
| { | |
| sel4utils_res_t *res = reservation_to_res(image); | |
| seL4_CPtr slot; | |
| int error = vka_cspace_alloc(get_alloc_data(current)->vka, &slot); | |
| if (error) { | |
| return -1; | |
| } | |
| cspacepath_t dest; | |
| vka_cspace_make_path(get_alloc_data(current)->vka, slot, &dest); | |
| for (uintptr_t page = res->start; page < res->end - 1; page += PAGE_SIZE_4K) { | |
| /* we don't know if the current vspace has caps to its mappings - | |
| * it probably doesn't. | |
| * | |
| * So we map the page in and copy the data across instead :( */ | |
| /* create the page in the clone vspace */ | |
| error = vspace_new_pages_at_vaddr(clone, (void *) page, 1, seL4_PageBits, image); | |
| if (error) { | |
| /* vspace will be left inconsistent */ | |
| LOG_ERROR("Error %d while trying to map page at %"PRIuPTR, error, page); | |
| } | |
| seL4_CPtr cap = vspace_get_cap(clone, (void *) page); | |
| /* copy the cap */ | |
| cspacepath_t src; | |
| vka_cspace_make_path(get_alloc_data(clone)->vka, cap, &src); | |
| error = vka_cnode_copy(&dest, &src, seL4_AllRights); | |
| assert(error == 0); | |
| /* map a copy of it the current vspace */ | |
| void *dest_addr = vspace_map_pages(current, &dest.capPtr, NULL, seL4_AllRights, | |
| 1, seL4_PageBits, 1); | |
| if (dest_addr == NULL) { | |
| /* vspace will be left inconsistent */ | |
| LOG_ERROR("Error! Vspace mapping failed, bailing\n"); | |
| return -1; | |
| } | |
| /* copy the data */ | |
| memcpy(dest_addr, (void *) page, PAGE_SIZE_4K); | |
| #ifdef CONFIG_ARCH_ARM | |
| seL4_ARM_Page_Unify_Instruction(dest.capPtr, 0, PAGE_SIZE_4K); | |
| seL4_ARM_Page_Unify_Instruction(cap, 0, PAGE_SIZE_4K); | |
| #endif /* CONFIG_ARCH_ARM */ | |
| /* unmap our copy */ | |
| vspace_unmap_pages(current, dest_addr, 1, seL4_PageBits, VSPACE_PRESERVE); | |
| vka_cnode_delete(&dest); | |
| } | |
| /* TODO swap out fault handler temporarily to ignore faults here */ | |
| vka_cspace_free(get_alloc_data(current)->vka, slot); | |
| return 0; | |
| } | |
| #endif /* CONFIG_LIB_SEL4_VSPACE && CONFIG_LIB_SEL4_VKA */ |