libsel4utils/src/vspace/bootstrap.c - 3p/sel4/sel4_libs - Git at Google

 /*
  * 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 */
	/*
	* 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 4K2 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 */