Release snapshot
diff --git a/Kbuild b/Kbuild
new file mode 100644
index 0000000..0279788
--- /dev/null
+++ b/Kbuild
@@ -0,0 +1,14 @@
+#
+# 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)
+#
+
+libs-$(CONFIG_LIB_SEL4_UTILS) += libsel4utils
+libsel4vspace-$(CONFIG_LIB_SEL4_VSPACE) := libsel4vspace
+libsel4vka-$(CONFIG_LIB_SEL4_VKA) := libsel4vka
+libsel4utils: $(libsel4vspace-y) $(libsel4vka-y) libutils libelf libcpio libsel4 common $(libc)
diff --git a/Kconfig b/Kconfig
new file mode 100644
index 0000000..d2fcc6b
--- /dev/null
+++ b/Kconfig
@@ -0,0 +1,28 @@
+#
+# 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)
+#
+
+menuconfig LIB_SEL4_UTILS
+ bool "Build sel4utils"
+ depends on LIB_SEL4 && HAVE_LIBC && LIB_ELF && LIB_CPIO && LIB_UTILS
+ select HAVE_SEL4_LIBS
+ default y
+ help
+ A library of utils for building an OS on seL4, including virtual memory and process and thread creation.
+
+if LIB_SEL4_UTILS
+ config SEL4UTILS_STACK_SIZE
+ int "Size of stacks in bytes to allocate if using vspace interface in this library"
+ default 65536
+
+ config SEL4UTILS_CSPACE_SIZE_BITS
+ int "Size of default cspace to spawn processes with"
+ range 2 27
+ default 12
+endif
diff --git a/LICENSE_BSD2.txt b/LICENSE_BSD2.txt
new file mode 100644
index 0000000..85cda3e
--- /dev/null
+++ b/LICENSE_BSD2.txt
@@ -0,0 +1,31 @@
+Files described as being under the "BSD 2-Clause" license fall under the
+following license.
+
+-----------------------------------------------------------------------
+
+Copyright (c) 2014 National ICT Australia and other contributors.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
+
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..ab9fd59
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,23 @@
+#
+# 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)
+#
+
+# Targets
+TARGETS := libsel4utils.a
+
+# Source files required to build the target
+CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/*.c))
+CFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/vspace/*.c))
+
+# Header files/directories this library provides
+HDRFILES := $(wildcard $(SOURCE_DIR)/include/*)
+HDRFILES += $(wildcard $(SOURCE_DIR)/arch_include/$(ARCH)/*)
+
+include $(SEL4_COMMON)/common.mk
+
diff --git a/arch_include/arm/sel4utils/arch/util.h b/arch_include/arm/sel4utils/arch/util.h
new file mode 100644
index 0000000..d8dc118
--- /dev/null
+++ b/arch_include/arm/sel4utils/arch/util.h
@@ -0,0 +1,56 @@
+/*
+ * 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)
+ */
+#ifndef _SEL4UTILS_ARCH_UTIL_H
+#define _SEL4UTILS_ARCH_UTIL_H
+
+#include <sel4/sel4.h>
+#include <sel4/arch/pfIPC.h>
+#include <sel4/arch/exIPC.h>
+
+#define EXCEPT_IPC_SYS_MR_IP EXCEPT_IPC_SYS_MR_PC
+
+static inline int
+sel4utils_is_read_fault(void)
+{
+ seL4_Word fsr = seL4_GetMR(SEL4_PFIPC_FSR);
+#if defined(ARM_HYP)
+ return (fsr & (1 << 6)) == 0;
+#else
+ return (fsr & (1 << 11)) == 0;
+#endif
+}
+
+
+static inline void
+sel4utils_set_instruction_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->pc = value;
+}
+
+static inline seL4_Word
+sel4utils_get_instruction_pointer(seL4_UserContext regs)
+{
+ return regs.pc;
+}
+
+static inline void
+sel4utils_set_stack_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->sp = value;
+}
+
+static inline void
+sel4utils_set_arg0(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->r0 = value;
+}
+#endif /* _SEL4UTILS_ARCH_UTIL_H */
+
+
diff --git a/arch_include/ia32/sel4utils/arch/util.h b/arch_include/ia32/sel4utils/arch/util.h
new file mode 100644
index 0000000..21faac1
--- /dev/null
+++ b/arch_include/ia32/sel4utils/arch/util.h
@@ -0,0 +1,53 @@
+/*
+ * 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)
+ */
+#ifndef _SEL4UTILS_ARCH_UTIL_H
+#define _SEL4UTILS_ARCH_UTIL_H
+
+#include <sel4/sel4.h>
+#include <sel4/arch/pfIPC.h>
+#include <sel4/arch/exIPC.h>
+
+#define EXCEPT_IPC_SYS_MR_IP EXCEPT_IPC_SYS_MR_EIP
+
+
+static inline int
+sel4utils_is_read_fault(void)
+{
+ seL4_Word fsr = seL4_GetMR(SEL4_PFIPC_FSR);
+ return (fsr & (1 << 1)) == 0;
+}
+
+
+static inline void
+sel4utils_set_instruction_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->eip = value;
+}
+
+static inline seL4_Word
+sel4utils_get_instruction_pointer(seL4_UserContext regs)
+{
+ return regs.eip;
+}
+
+static inline void
+sel4utils_set_stack_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->esp = value;
+}
+
+static inline void
+sel4utils_set_arg0(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->eip = value;
+}
+#endif /* _SEL4UTILS_ARCH_UTIL_H */
+
+
diff --git a/arch_include/ia64/sel4utils/arch/util.h b/arch_include/ia64/sel4utils/arch/util.h
new file mode 100644
index 0000000..90714bc
--- /dev/null
+++ b/arch_include/ia64/sel4utils/arch/util.h
@@ -0,0 +1,52 @@
+/*
+ * 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)
+ */
+#ifndef _SEL4UTILS_ARCH_UTIL_H
+#define _SEL4UTILS_ARCH_UTIL_H
+
+#include <sel4/sel4.h>
+#include <sel4/arch/pfIPC.h>
+#include <sel4/arch/exIPC.h>
+
+#define EXCEPT_IPC_SYS_MR_IP EXCEPT_IPC_RIP
+
+static inline int
+sel4utils_is_read_fault(void)
+{
+ seL4_Word fsr = seL4_GetMR(SEL4_PFIPC_FSR);
+ return (fsr & (1 << 1)) == 0;
+}
+
+
+static inline void
+sel4utils_set_instruction_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->rip = value;
+}
+
+static inline seL4_Word
+sel4utils_get_instruction_pointer(seL4_UserContext regs)
+{
+ return regs.rip;
+}
+
+static inline void
+sel4utils_set_stack_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->rsp = value;
+}
+
+static inline void
+sel4utils_set_arg0(seL4_UserContext *regs, seL4_Word value)
+{
+ regs->rdi = value;
+}
+#endif /* _SEL4UTILS_ARCH_UTIL_H */
+
+
diff --git a/include/sel4utils/client_server_vspace.h b/include/sel4utils/client_server_vspace.h
new file mode 100644
index 0000000..de1561d
--- /dev/null
+++ b/include/sel4utils/client_server_vspace.h
@@ -0,0 +1,71 @@
+/*
+ * 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)
+ */
+
+/*
+ * This implements a virtual address space that proxies calls two different
+ * vspaces to ensure that pages in one are mapped into the other. This allows
+ * a server to efficiently read/write memory from a client. No attempt is made
+ * to construct contiguous regions in the server when contiguous regions are
+ * created in the client.
+ * Currently cannot correctly handle stacks (since their size is unknown to us)
+ * and cacheability attributes (currently assume all cached mappings)
+ */
+#ifndef _UTILS_CLIENT_SERVER_VSPACE_H
+#define _UTILS_CLIENT_SERVER_VSPACE_H
+
+#include <autoconf.h>
+
+#if defined CONFIG_LIB_SEL4_VSPACE && defined CONFIG_LIB_SEL4_VKA
+
+#include <vspace/vspace.h>
+#include <vka/vka.h>
+
+/**
+ * Initialize a new client server vspace
+ *
+ * @param vspace vspace struct to initialize
+ * @param vka vka for future allocations
+ * @param server vspace to duplicate all mappings into
+ * @param client vspace to directly proxy calls to
+ *
+ * @return 0 on success
+ */
+int sel4utils_get_cs_vspace(vspace_t *vspace, vka_t *vka, vspace_t *server, vspace_t *client);
+
+/**
+ * Translate virtual address in client to one in the server.
+ * This is only for that address! Pages are not contiguous
+ *
+ * @param vspace vspace to do translation with
+ * @param addr addr to lookup in the client
+ *
+ * @return Address in the server vspace, or NULL if not found
+ */
+void *sel4utils_cs_vspace_translate(vspace_t *vspace, void *addr);
+
+/**
+ * Perform a callback for every contiguous range of bytes in the server vspace
+ * for the range provided in the client vspace
+ *
+ * @param vspace vspace to do translation in
+ * @param addr Address in the client to start translation from
+ * @param len length of the range in the client
+ * @param proc Callback function that will be called back with ranges of address in the server after
+ * page boundary splits. If non zero is returned the loop is stopped and the error returned
+ * @param cookie Cookie to be passed to the callback function
+ *
+ * @return Result of callback if non zero occured, internal error code if mapping not found, zero otherwise
+ */
+int sel4utils_cs_vspace_for_each(vspace_t *vspace, void *addr, uint32_t len,
+ int (*proc)(void* addr, uint32_t len, void *cookie),
+ void *cookie);
+
+#endif /* CONFIG_LIB_SEL4_VSPACE && CONFIG_LIB_SEL4_VKA */
+#endif /* _UTILS_CLIENT_SERVER_VSPACE_H */
diff --git a/include/sel4utils/elf.h b/include/sel4utils/elf.h
new file mode 100644
index 0000000..2348bc1
--- /dev/null
+++ b/include/sel4utils/elf.h
@@ -0,0 +1,100 @@
+/*
+ * 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)
+ */
+#ifndef SEL4UTILS_ELF_H
+#define SEL4UTILS_ELF_H
+
+#include <autoconf.h>
+
+#if (defined CONFIG_LIB_SEL4_VKA && defined CONFIG_LIB_SEL4_VSPACE)
+
+#include <vka/vka.h>
+
+#include <vspace/vspace.h>
+
+typedef struct sel4utils_elf_region {
+ seL4_CapRights rights;
+ /* These two vstarts may differ if the elf was not mapped 1to1. Such an elf is not
+ * runnable, but allows it to be loaded into a vspace where it is not intended to be run */
+ void *elf_vstart;
+ void *reservation_vstart;
+ uint32_t size;
+ reservation_t *reservation;
+ int cacheable;
+} sel4utils_elf_region_t;
+
+/**
+ * Load an elf file into a vspace.
+ *
+ * The loader vspace and vka allocation will be preserved (no extra cslots or objects or vaddrs
+ * will leak from this function), even in the case of an error.
+ *
+ * The loadee vspace and vka will alter: cslots will be allocated for each frame to be
+ * mapped into the address space and frames will be allocated. In case of failure the entire
+ * virtual address space is left in the state where it failed.
+ *
+ * @param loadee the vspace to load the elf file into
+ * @param loader the vspace we are loading from
+ * @param loadee_vka allocator to use for allocation in the loadee vspace
+ * @param loader_vka allocator to use for loader vspace. Can be the same as loadee_vka.
+ * @param image_name name of the image in the cpio archive to load.
+ * @param regions Optional array for list of regions to be placed. Assumed to be the correct
+ size as reported by a call to sel4utils_elf_num_regions
+ * @param mapanywhere If true allows the elf to be loaded anywhere in the vspace. Regions will
+ still be contiguous
+ *
+ * @return The entry point of the new process, NULL on error
+ */
+void *
+sel4utils_elf_load_record_regions(vspace_t *loadee, vspace_t *loader, vka_t *loadee_vka,
+ vka_t *loader_vka, char *image_name, sel4utils_elf_region_t *regions, int mapanywhere);
+
+/**
+ * Wrapper for sel4utils_elf_load_record_regions. Does not record/perform resevations and
+ * maps into the correct virtual addresses
+ *
+ * @param loadee the vspace to load the elf file into
+ * @param loader the vspace we are loading from
+ * @param loadee_vka allocator to use for allocation in the loadee vspace
+ * @param loader_vka allocator to use for loader vspace. Can be the same as loadee_vka.
+ * @param image_name name of the image in the cpio archive to load.
+ *
+ * @return The entry point of the new process, NULL on error
+ */
+void *
+sel4utils_elf_load(vspace_t *loadee, vspace_t *loader, vka_t *loadee_vka,
+ vka_t *loader_vka, char *image_name);
+
+/**
+ * Parses an elf file but does not actually load it. Merely reserves the regions in the vspace
+ * for where the elf segments would go. This is used for lazy loading / copy on write
+
+ * @param loadee the vspace to reserve the elf regions in
+ * @param image_name name of the image in the cpio archive to parse.
+ * @param regions Array for list of regions to be placed. Assumed to be the correct
+ size as reported by a call to sel4utils_elf_num_regions
+ *
+ * @return The entry point of the elf, NULL on error
+ */
+void *
+sel4utils_elf_reserve(vspace_t *loadee, char *image_name, sel4utils_elf_region_t *regions);
+
+/**
+ * Parses an elf file and returns the number of loadable regions. The result of this
+ * is used to calculate the number of regions to pass to sel4utils_elf_reserve and
+ * sel4utils_elf_load_record_regions
+ *
+ * @param image_name name of the image in the cpio archive to inspect
+ * @return Number of loadable regions in the elf
+ */
+int
+sel4utils_elf_num_regions(char *image_name);
+
+#endif /* (defined CONFIG_LIB_SEL4_VKA && defined CONFIG_LIB_SEL4_VSPACE) */
+#endif /* SEL4UTILS_ELF_H */
diff --git a/include/sel4utils/mapping.h b/include/sel4utils/mapping.h
new file mode 100644
index 0000000..f0b967b
--- /dev/null
+++ b/include/sel4utils/mapping.h
@@ -0,0 +1,124 @@
+/*
+ * 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)
+ */
+
+#ifndef _UTILS_MAPPING_H_
+#define _UTILS_MAPPING_H_
+
+#include <utils/util.h>
+#include <sel4/sel4.h>
+#include <autoconf.h>
+
+
+#if defined(CONFIG_ARCH_ARM)
+
+/* sizes (in bits) of pages supported by sel4 in ascending order */
+#if defined(ARM_HYP)
+static int UNUSED sel4_supported_page_sizes[] = {12, 16, 21, 25};
+#else
+static int UNUSED sel4_supported_page_sizes[] = {12, 16, 20, 24};
+#endif
+
+#define seL4_ARCH_Uncached_VMAttributes 0
+
+#define seL4_ARCH_Page_Map seL4_ARM_Page_Map
+#define seL4_ARCH_Page_Unmap seL4_ARM_Page_Unmap
+#define seL4_ARCH_PageTable_Map seL4_ARM_PageTable_Map
+#define seL4_ARCH_ASIDPool_Assign seL4_ARM_ASIDPool_Assign
+#define seL4_ARCH_PageTableObject seL4_ARM_PageTableObject
+#define seL4_ARCH_PageDirectoryObject seL4_ARM_PageDirectoryObject
+#define seL4_ARCH_Default_VMAttributes seL4_ARM_Default_VMAttributes
+#define seL4_ARCH_VMAttributes seL4_ARM_VMAttributes
+#define seL4_ARCH_4KPage seL4_ARM_SmallPageObject
+
+#elif defined(CONFIG_X86_64)
+
+/* sizes (in bits) of pages supported by sel4 in ascending order */
+static int UNUSED sel4_supported_page_sizes[] = {12, 21};
+
+#define seL4_ARCH_Page_Unmap seL4_X64_Page_Unmap
+#define seL4_ARCH_Page_Map seL4_X64_Page_Map
+#define seL4_ARCH_PageTable_Map seL4_X64_PageTable_Map
+#define seL4_ARCH_PageDirectory_Map seL4_X64_PageDirectory_Map
+#define seL4_ARCH_PageDirectoryPointerTable_Map seL4_X64_PageDirectoryPointerTable_Map
+#define seL4_CapInitThreadPD seL4_CapInitThreadPML4
+#define seL4_ARCH_VMAttributes seL4_IA32_VMAttributes
+#define seL4_ARCH_4KPage seL4_X64_4K
+#define seL4_ARCH_Default_VMAttributes seL4_IA32_Default_VMAttributes
+
+#elif defined(CONFIG_ARCH_IA32) /* CONFIG_ARCH_ARM */
+
+/* sizes (in bits) of pages supported by sel4 in ascending order */
+static int UNUSED sel4_supported_page_sizes[] = {12, 22};
+
+#define seL4_ARCH_Page_Map seL4_IA32_Page_Map
+#define seL4_ARCH_Page_Unmap seL4_IA32_Page_Unmap
+#define seL4_ARCH_PageTable_Map seL4_IA32_PageTable_Map
+#define seL4_ARCH_ASIDPool_Assign seL4_IA32_ASIDPool_Assign
+#define seL4_ARCH_PageTableObject seL4_IA32_PageTableObject
+#define seL4_ARCH_PageDirectoryObject seL4_IA32_PageDirectoryObject
+#define seL4_ARCH_Default_VMAttributes seL4_IA32_Default_VMAttributes
+#define seL4_ARCH_VMAttributes seL4_IA32_VMAttributes
+#define seL4_ARCH_4KPage seL4_IA32_4K
+#define seL4_ARCH_Uncached_VMAttributes 0
+
+#endif /* CONFIG_ARCH_IA32 */
+
+#define NUM_SEL4_PAGE_SIZES ((int) ARRAY_SIZE(sel4_supported_page_sizes))
+
+#ifdef CONFIG_LIB_SEL4_VKA
+
+#include <vka/vka.h>
+#include <vka/object.h>
+
+/* Map a page to a virtual address, allocating a page table if neccessary.
+*
+*
+* @param vka a vka compliant allocator
+* @param pd page directory to map the page into
+* @param page capability to the page to map in
+* @param vaddr unmapped virutal address to map the page into
+* @param rights permissions to map the page with
+* @param cacheable 1 if the page should be cached (0 if it is for DMA)
+* @param pagetable empty vka_object_t structure to be populated with page table
+* info if one is allocated
+*
+* @return error sel4 error code or -1 if allocation failed.
+*/
+int sel4utils_map_page(vka_t *vka, seL4_CPtr pd, seL4_CPtr frame, void *vaddr,
+ seL4_CapRights rights, int cacheable, vka_object_t *pagetable);
+
+/** convenient wrapper this if you don't want to track allocated page tables */
+static inline int sel4utils_map_page_leaky(vka_t *vka, seL4_CPtr pd, seL4_CPtr frame, void *vaddr,
+ seL4_CapRights rights, int cacheable)
+{
+ vka_object_t pagetable;
+ return sel4utils_map_page(vka, pd, frame, vaddr, rights, cacheable, &pagetable);
+}
+
+#endif /* CONFIG_LIB_SEL4_VKA */
+
+#ifdef CONFIG_ARCH_IA32
+
+#ifdef CONFIG_IOMMU
+int sel4utils_map_iospace_page(vka_t *vka, seL4_CPtr iospace, seL4_CPtr frame, seL4_Word vaddr,
+ seL4_CapRights rights, int cacheable, seL4_Word size_bits,
+ vka_object_t *pts, int *num_pts);
+#endif
+
+#ifdef CONFIG_VTX
+int sel4utils_map_ept_page(vka_t *vka, seL4_CPtr pd, seL4_CPtr frame, seL4_Word vaddr,
+ seL4_CapRights rights, int cacheable, seL4_Word size_bits, vka_object_t *pagetable, vka_object_t *pagedir);
+
+#endif
+#endif
+
+
+
+#endif /* UTILS_MAPPING_H_ */
diff --git a/include/sel4utils/process.h b/include/sel4utils/process.h
new file mode 100644
index 0000000..4e0d909
--- /dev/null
+++ b/include/sel4utils/process.h
@@ -0,0 +1,242 @@
+/*
+ * 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)
+ */
+#ifndef SEL4UTILS_PROCESS_H
+#define SEL4UTILS_PROCESS_H
+
+#include <autoconf.h>
+
+#if (defined CONFIG_LIB_SEL4_VSPACE && defined CONFIG_LIB_SEL4_VKA)
+
+#include <vka/vka.h>
+#include <vspace/vspace.h>
+
+#include <sel4utils/thread.h>
+#include <sel4utils/vspace.h>
+#include <sel4utils/elf.h>
+
+typedef struct object_node object_node_t;
+
+struct object_node {
+ vka_object_t object;
+ object_node_t *next;
+};
+
+typedef struct {
+ vka_object_t pd;
+ vspace_t vspace;
+ sel4utils_alloc_data_t data;
+ vka_object_t cspace;
+ uint32_t cspace_size;
+ uint32_t cspace_next_free;
+ sel4utils_thread_t thread;
+ vka_object_t fault_endpoint;
+ void *entry_point;
+ object_node_t *allocated_object_list_head;
+ /* if the elf wasn't loaded into the address space, this describes the regions.
+ * this permits lazy loading / copy on write / page sharing / whatever crazy thing
+ * you want to implement */
+ int num_elf_regions;
+ sel4utils_elf_region_t *elf_regions;
+} sel4utils_process_t;
+
+/* sel4utils processes start with some caps in their cspace.
+ * These are the caps
+ */
+enum sel4utils_cspace_layout {
+ /*
+ * The root cnode (with appropriate guard)
+ */
+ SEL4UTILS_CNODE_SLOT = 1,
+ /* The slot on the cspace that fault_endpoint is put if
+ * sel4utils_configure_process is used.
+ */
+ SEL4UTILS_ENDPOINT_SLOT = 2,
+};
+
+typedef struct {
+ /* should we handle elf logic at all? */
+ bool is_elf;
+ /* if so what is the image name? */
+ char *image_name;
+ /* Do you want the elf image preloaded? */
+ bool do_elf_load;
+
+ /* otherwise what is the entry point? */
+ void *entry_point;
+
+ /* should we create a default single level cspace? */
+ bool create_cspace;
+ /* if so how big ? */
+ int one_level_cspace_size_bits;
+
+ /* otherwise what is the root cnode ?*/
+ /* Note if you use a custom cspace then
+ * sel4utils_copy_cap_to_process etc will not work */
+ vka_object_t cnode;
+
+ /* do you want us to create a vspace for you? */
+ bool create_vspace;
+ /* if not what is the page dir, and what is the vspace */
+ vspace_t *vspace;
+ vka_object_t page_dir;
+
+ /* if so, is there a regions you want left clear?*/
+ sel4utils_elf_region_t *reservations;
+ int num_reservations;
+
+ /* do you want a fault endpoint created? */
+ bool create_fault_endpoint;
+ /* otherwise what is it */
+ vka_object_t fault_endpoint;
+
+ int priority;
+#ifndef CONFIG_KERNEL_STABLE
+ seL4_CPtr asid_pool;
+#endif
+} sel4utils_process_config_t;
+
+/**
+ * Copy data from one vspace to another. Data is in POSIX standard argc, argv style.
+ *
+ * This is intented to use when loading applications of the format:
+ *
+ * int main(int argc, char **argv) { };
+ *
+ *
+ * @param current the vspace we are loading the arguments from
+ * @param target the vspace we are loading the arguments to
+ * @param vka the vka allocation interface to use when allocating pages.
+ * the pages will first be mapped into the current vspace, then unmapped and
+ * mapped into the target vspace, and left that way.
+ * @param argc the number of strings
+ * @param argv an array of c strings.
+ *
+ * @return NULL on failure, otherwise a pointer in the target address space where argv has
+ * been written.
+ */
+void *sel4utils_copy_args(vspace_t *current, vspace_t *target, vka_t *vka,
+ int argc, char *argv[]);
+
+/**
+ * Start a process, and copy arguments into the processes address space.
+ *
+ * This is intented to use when loading applications of the format:
+ *
+ * int main(int argc, char **argv) { };
+ *
+ * The third argument (in r2 for arm, on stack for ia32) will be the address of the ipc buffer.
+ * This is intended to be loaded by the crt into the data word of the ipc buffer,
+ * or you can just add it to your function prototype.
+ *
+ * Add the following to your crt to use it this way:
+ *
+ * arm: str r2, [r2, #484]
+ * ia32: popl %ebp
+ * movl %ebp, 484(%ebp)
+ *
+ * @param process initialised sel4utils process struct.
+ * @param vka vka interface to use for allocation of frames.
+ * @param vspace the current vspace.
+ * @param argc the number of arguments.
+ * @param argv a pointer to an array of strings in the current vspace.
+ * @param resume 1 to start the process, 0 to leave suspended.
+ *
+ * @return -1 on error, 0 on success.
+ *
+ */
+int sel4utils_spawn_process(sel4utils_process_t *process, vka_t *vka, vspace_t *vspace,
+ int argc, char *argv[], int resume);
+
+/**
+ * This is the function to use if you just want to set up a process as fast as possible.
+ * It creates a simple cspace and vspace for you, allocates a fault endpoint and puts
+ * it into the new cspace.
+ *
+ * It loads the elf file into the new vspace, parses the elf file and stores the entry point
+ * into process->entry_point.
+ *
+ * It uses the same vka for both allocations - the new process will not have an allocator.
+ *
+ * The process will have just one thread.
+ *
+ * Otherwise, use it as a model for loading processes and use the elf_load.
+ *
+ * WARNING: when launching processes on ia32 please ensure your calling convention
+ * matches that documented in sel4utils_start_thread. Otherwise your arguments
+ * won't come through correctly.
+ *
+ * @param process uninitialised process struct.
+ * @param vka allocator to use to allocate objects.
+ * @param vspace vspace allocator for the current vspace.
+ * @param priority priority to configure the process to run as.
+ * @param image_name name of the elf image to load from the cpio archive.
+ *
+ * @return 0 on success, -1 on error.
+ */
+int sel4utils_configure_process(sel4utils_process_t *process, vka_t *vka, vspace_t *vspace,
+ uint8_t priority, char *image_name);
+
+/**
+ * Configure a process with more customisations (Create your own vspace, customise cspace size).
+ *
+ * @param process uninitliased process struct
+ * @param vka allocator to use to allocate objects.
+ * @param spawner_vspace vspace to use to allocate virtual memory in the current address space.
+ * @param config process config.
+ *
+ * @return 0 on success, -1 on error.
+ */
+int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka,
+ vspace_t *spawner_vspace, sel4utils_process_config_t config);
+
+/**
+ * Copy a cap into a process' cspace.
+ *
+ * This will only work if you configured the process using one of the above functions, or
+ * have mimiced their functionality.
+ *
+ * @param process process to copy the cap to
+ * @param src path in the current cspace to copy the cap from
+ *
+ * @return 0 on failure, otherwise the slot in the processes cspace.
+ */
+seL4_CPtr sel4utils_copy_cap_to_process(sel4utils_process_t *process, cspacepath_t src);
+
+/**
+ *
+ * Mint a cap into a process' cspace.
+ *
+ * As above, except mint the cap with rights and data.
+ *
+ * @return 0 on failure, otherwise the slot in the cspace where the new cap is.
+ */
+seL4_CPtr sel4utils_mint_cap_to_process(sel4utils_process_t *process, cspacepath_t src, seL4_CapRights rights, seL4_CapData_t data);
+
+/**
+ * Destroy a process.
+ *
+ * This will free everything possible associated with a process and teardown the vspace.
+ *
+ * @param process process to destroy
+ * @param vka allocator used to allocate objects for this process
+ */
+void sel4utils_destroy_process(sel4utils_process_t *process, vka_t *vka);
+
+
+/*
+ * sel4utils default allocated object function for vspaces.
+ *
+ * Stores a list of allocated objects in the process struct and frees them
+ * when sel4utils_destroy_process is called.
+ */
+void sel4utils_allocated_object(void *cookie, vka_object_t object);
+
+#endif /* (defined CONFIG_LIB_SEL4_VSPACE && defined CONFIG_LIB_SEL4_VKA) */
+#endif /* SEL4UTILS_PROCESS_H */
diff --git a/include/sel4utils/profile.h b/include/sel4utils/profile.h
new file mode 100644
index 0000000..07ad529
--- /dev/null
+++ b/include/sel4utils/profile.h
@@ -0,0 +1,79 @@
+/*
+ * 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)
+ */
+
+#ifndef _UTILS_PROFILE_H_
+#define _UTILS_PROFILE_H_
+
+#include <sel4utils/util.h>
+#include <stdint.h>
+
+#define PROFILE_VAR_TYPE_INT32 1
+#define PROFILE_VAR_TYPE_INT64 2
+
+typedef struct profile_var {
+ int type;
+ void *var;
+ const char *varname;
+ const char *description;
+} profile_var_t;
+
+#define __WATCH_VAR(_type, _var, _description, _unique) \
+ static profile_var_t profile_##_unique \
+ __attribute__((used)) __attribute__((section("_profile_var"))) \
+ = {.type = _type, .var = &_var, .varname = #_var, .description = _description}
+
+#define _WATCH_VAR32(var, description, unique) \
+ compile_time_assert(profile_size_##unique, sizeof(var) == 4); \
+ __WATCH_VAR(PROFILE_VAR_TYPE_INT32, var, description, unique)
+
+#define WATCH_VAR32(var, description) \
+ _WATCH_VAR32(var, description, __LINE__)
+
+#define _WATCH_VAR64(var, description, unique) \
+ compile_time_assert(profile_size_##unique, sizeof(var) == 8); \
+ __WATCH_VAR(PROFILE_VAR_TYPE_INT64, var, description, unique)
+
+#define WATCH_VAR64(var, description) \
+ _WATCH_VAR64(var, description, __LINE__)
+
+typedef void (*profile_callback32)(uint32_t value, const char *varname, const char *descrption, void *cookie);
+typedef void (*profile_callback64)(uint64_t value, const char *varname, const char *descrption, void *cookie);
+
+/* Sample functions that just output the vars using printf. cookie is ignored */
+void profile_print32(uint32_t value, const char *varname, const char *description, void *cookie);
+void profile_print64(uint64_t value, const char *varname, const char *description, void *cookie);
+
+/* Iterates over all profile variables and calls back the specified function(s)
+ * with the current value. */
+void profile_scrape(profile_callback32 callback32, profile_callback64 callback64, void *cookie);
+
+#define _PSTART_TIME(x) uint32_t __begin_time##x = read_ccnt()
+#define _PEND_TIME(x) uint32_t __end_time##x = read_ccnt()
+#define _PTIME_DIFF(x) (__end_time##x - __begin_time##x)
+#define PINC(name) PADD(name, 1)
+#define PADDTIMEDIFF(name) PADD(name, PTIMEDIFF(name))
+#define PADDTIME(name) PEND_TIME(name); PADDTIMEDIFF(name)
+#define PTIMEDIFF(x) _PTIME_DIFF(x)
+
+#ifdef PROFILE
+#define PVARUINT32(name, desc) static uint32_t name = 0; WATCH_VAR32(name, desc);
+#define PVARUINT64(name, desc) static uint64_t name = 0; WATCH_VAR64(name, desc);
+#define PADD(name, x) do {name += (x); } while(0)
+#define PSTART_TIME(x) _PSTART_TIME(x)
+#define PEND_TIME(x) _PEND_TIME(x)
+#else
+#define PVARUINT32(name, desc)
+#define PVARUINT64(name, desc)
+#define PADD(name, x) do { } while(0)
+#define PSTART_TIME(x) do { } while(0)
+#define PEND_TIME(x) do { } while(0)
+#endif
+
+#endif
diff --git a/include/sel4utils/sel4_debug.h b/include/sel4utils/sel4_debug.h
new file mode 100644
index 0000000..e1358c4
--- /dev/null
+++ b/include/sel4utils/sel4_debug.h
@@ -0,0 +1,31 @@
+/*
+ * 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)
+ */
+
+/*
+ Authors: Cristan Szmajda, Ben Leslie
+ Description:
+ Program diagnostics as per 7.2
+ Status: Complete.
+*/
+
+/*
+ * <assert.h> may safely be included multiple times with or without NDEBUG
+ */
+#undef sel4_error
+
+#define sel4_error(e, str) ((e == seL4_NoError) ? (void)0 : __sel4_error(e, __FILE__, __func__, __LINE__, str))
+
+/* Implemented in src/assert.c */
+#ifndef _SEL4_DEBUG_H_
+#define _SEL4_DEBUG_H_
+
+void __sel4_error(int, const char *, const char *, int, char *);
+
+#endif /* _SEL4_DEBUG_ */
diff --git a/include/sel4utils/stack.h b/include/sel4utils/stack.h
new file mode 100644
index 0000000..02e639e
--- /dev/null
+++ b/include/sel4utils/stack.h
@@ -0,0 +1,27 @@
+/*
+ * 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)
+ */
+#ifndef __SEL4UTILS_STACK_H
+#define __SEL4UTILS_STACK_H
+
+#include <vspace/vspace.h>
+
+/**
+ * Allocate a new stack and start running func on it.
+ * If func returns, you will be back on the old stack.
+ *
+ * @param vspace interface to allocate stack with
+ * @param func to jump to with the new stack.
+ * @ret the return value of func. -1 if stack allocation fails.
+ * Note: it would be unwise to write func such that it returns -1.
+ *
+ */
+int sel4utils_run_on_stack(vspace_t *vspace, int (*func)(void));
+
+#endif /* __SEL4UTILS_STACK_H */
diff --git a/include/sel4utils/thread.h b/include/sel4utils/thread.h
new file mode 100644
index 0000000..0f665a8
--- /dev/null
+++ b/include/sel4utils/thread.h
@@ -0,0 +1,154 @@
+/*
+ * 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)
+ */
+
+/**
+ *
+ * Provides basic thread configuration/starting/cleanup functions.
+ *
+ * Any other operations (start, stop, resume) should use the seL4 API directly on
+ * sel4utils_thread_t->tcb.cptr.
+ *
+ */
+#ifndef _SEL4UTILS_THREAD_H
+#define _SEL4UTILS_THREAD_H
+
+#include <autoconf.h>
+
+#ifdef CONFIG_LIB_SEL4_VSPACE
+
+#include <sel4/sel4.h>
+
+#include <vka/vka.h>
+
+#include <vspace/vspace.h>
+
+typedef struct sel4utils_thread {
+ vka_object_t tcb;
+ void *stack_top;
+ seL4_CPtr ipc_buffer;
+ seL4_Word ipc_buffer_addr;
+} sel4utils_thread_t;
+
+/**
+ * Configure a thread, allocating any resources required.
+ *
+ * @param vka initialised vka to allocate objects with
+ * @param alloc initialised vspace structure to allocate virtual memory with
+ * @param fault_endpoint endpoint to set as the threads fault endpoint. Can be 0.
+ * @param priority seL4 priority for the thread to be scheduled with.
+ * @param cspace the root of the cspace to start the thread in
+ * @param cspace_root_data data for cspace access
+ * @param res an uninitialised sel4utils_thread_t data structure that will be initialised
+ * after this operation.
+ *
+ * @return 0 on success, -1 on failure. Use CONFIG_DEBUG to see error messages.
+ */
+int sel4utils_configure_thread(vka_t *vka, vspace_t *alloc, seL4_CPtr fault_endpoint,
+ uint8_t priority, seL4_CNode cspace, seL4_CapData_t cspace_root_data,
+ sel4utils_thread_t *res);
+
+/**
+ * Start a thread, allocating any resources required.
+ * The third argument to the thread (in r2 for arm, on stack for ia32) will be the
+ * address of the ipc buffer.
+ *
+ * @param thread thread data structure that has been initialised with sel4utils_configure_thread
+ * @param entry_point the address that the thread will start at
+ *
+ * NOTE: In order for the on-stack argument passing to work for ia32,
+ * entry points must be functions.
+ *
+ * ie. jumping to this start symbol will work:
+ *
+ * void _start(int argc, char **argv) {
+ * int ret = main(argc, argv);
+ * exit(ret);
+ * }
+ *
+ *
+ * However, jumping to a start symbol like this:
+ *
+ * _start:
+ * call main
+ *
+ * will NOT work, as call pushes an extra value (the return value)
+ * onto the stack. If you really require an assembler stub, it should
+ * decrement the stack value to account for this.
+ *
+ * ie.
+ *
+ * _start:
+ * popl %eax
+ * call main
+ *
+ * This does not apply for arm, as arguments are passed in registers.
+ *
+ *
+ * @param arg0 a pointer to the arguments for this thread. User decides the protocol.
+ * @param arg1 another pointer. User decides the protocol. Note that there are two args here
+ * to easily support C standard: int main(int argc, char **argv).
+ * @param resume 1 to start the thread immediately, 0 otherwise.
+ *
+ * @return 0 on success, -1 on failure.
+ */
+int sel4utils_start_thread(sel4utils_thread_t *thread, void *entry_point, void *arg0, void *arg1,
+ int resume);
+
+/**
+ * Release any resources used by this thread. The thread data structure will not be usable
+ * until sel4utils_thread_configure is called again.
+ *
+ * @param vka the vka interface that this thread was initialised with
+ * @param alloc the allocation interface that this thread was initialised with
+ * @param thread the thread structure that was returned when the thread started
+ */
+void sel4utils_clean_up_thread(vka_t *vka, vspace_t *alloc, sel4utils_thread_t *thread);
+
+/**
+ * Start a fault handling thread that will print the name of the thread that faulted
+ * as well as debugging information.
+ *
+ * @param fault_endpoint the fault_endpoint to wait on
+ * @param vka allocator
+ * @param vspace vspace (this library must be mapped into that vspace).
+ * @param prio the priority to run the thread at (recommend highest possible)
+ * @param cspace the cspace that the fault_endpoint is in
+ * @param data the cspace_data for that cspace (with correct guard)
+ * @param name the name of the thread to print if it faults
+ * @param thread the thread data structure to populate
+ *
+ * @return 0 on success.
+ */
+int sel4utils_start_fault_handler(seL4_CPtr fault_endpoint, vka_t *vka, vspace_t *vspace,
+ uint8_t prio, seL4_CPtr cspace, seL4_CapData_t data, char *name, sel4utils_thread_t *res);
+
+
+/**
+ * Pretty print a fault messge.
+ *
+ * @param tag the message info tag delivered by the fault.
+ * @param name thread name
+ */
+void sel4utils_print_fault_message(seL4_MessageInfo_t tag, char *name);
+
+static inline seL4_TCB
+sel4utils_get_tcb(sel4utils_thread_t *thread)
+{
+ return thread->tcb.cptr;
+}
+
+static inline int
+sel4utils_suspend_thread(sel4utils_thread_t *thread)
+{
+ return seL4_TCB_Suspend(thread->tcb.cptr);
+}
+
+#endif /* CONFIG_LIB_SEL4_VSPACE */
+#endif /* _SEL4UTILS_THREAD_H */
diff --git a/include/sel4utils/util.h b/include/sel4utils/util.h
new file mode 100644
index 0000000..a6a59d4
--- /dev/null
+++ b/include/sel4utils/util.h
@@ -0,0 +1,20 @@
+/*
+ * 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)
+ */
+
+#ifndef _SEL4_UTILS_UTIL_H_
+#define _SEL4_UTILS_UTIL_H_
+
+#include <autoconf.h>
+#include <assert.h>
+#include <stdint.h>
+
+#include <utils/util.h>
+
+#endif
diff --git a/include/sel4utils/vspace.h b/include/sel4utils/vspace.h
new file mode 100644
index 0000000..252e635
--- /dev/null
+++ b/include/sel4utils/vspace.h
@@ -0,0 +1,279 @@
+/*
+ * 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)
+ */
+
+/*
+ * An implementation of the vspace virtual memory allocation interface, using a two
+ * level page table.
+ *
+ * This implementation expects malloc to work, although it only uses it for small amounts of
+ * memory.
+ *
+ * Stack size is constant and be configured in menuconfig.
+ *
+ * Stacks are allocated with 1 guard page between them, but they are continguous in the vmem
+ * region.
+ *
+ * Allocation starts at 0x00001000.
+ *
+ * This library will allow you to map over anything that it doesn't know about, so
+ * make sure you tell it if you do any external mapping.
+ *
+ */
+#ifndef _UTILS_VSPACE_H
+#define _UTILS_VSPACE_H
+
+#include <autoconf.h>
+
+#if defined CONFIG_LIB_SEL4_VSPACE && defined CONFIG_LIB_SEL4_VKA
+
+#include <vspace/vspace.h>
+#include <vka/vka.h>
+#include <sel4utils/util.h>
+
+/* These definitions are only here so that you can take the size of them.
+ * TOUCHING THESE DATA STRUCTURES IN ANY WAY WILL BREAK THE WORLD
+ * */
+#ifdef CONFIG_X86_64
+#define VSPACE_LEVEL_BITS 9
+#else
+#define VSPACE_LEVEL_BITS 10
+#endif
+
+#define VSPACE_LEVEL_SIZE BIT(VSPACE_LEVEL_BITS)
+
+typedef struct bottom_level {
+ seL4_CPtr bottom_level[VSPACE_LEVEL_SIZE];
+} bottom_level_t;
+
+typedef int(*sel4utils_map_page_fn)(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights, int cacheable, size_t size_bits);
+
+typedef struct sel4utils_alloc_data {
+ vka_t *vka;
+ bottom_level_t **top_level;
+ void *next_bottom_level_vaddr;
+ void *last_allocated;
+ vspace_t *bootstrap;
+ sel4utils_map_page_fn map_page;
+} sel4utils_alloc_data_t;
+
+struct reservation {
+ void *start;
+ void *end;
+ seL4_CapRights rights;
+ int cacheable;
+};
+
+/**
+ * This is a mostly internal function for constructing a vspace. Allows a vspace to be created
+ * with an arbitrary function to invoke for the mapping of pages. This is useful if you want
+ * a vspace manager, but you do not want to use seL4 page directories
+ *
+ * @param loader vspace of the current process, used to allocate
+ * virtual memory book keeping.
+ * @param new_vspace uninitialised vspace struct to populate.
+ * @param data uninitialised vspace data struct to populate.
+ * @param vka initialised vka that this virtual memory allocator will use to
+ * allocate pages and pagetables. This allocator will never invoke free.
+ * @param page_directory page directory for the new vspace.
+ * @param allocated_object_fn function to call when objects are allocated. Can be null.
+ * @param allocated_object_cookie cookie passed when the above function is called. Can be null.
+ * @param map_page Function that will be called to map seL4 pages
+ *
+ * @return 0 on success.
+ */
+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);
+
+/**
+ * Initialise a vspace allocator for a new address space (not the current one).
+ *
+ * @param loader vspace of the current process, used to allocate
+ * virtual memory book keeping.
+ * @param new_vspace uninitialised vspace struct to populate.
+ * @param data uninitialised vspace data struct to populate.
+ * @param vka initialised vka that this virtual memory allocator will use to
+ * allocate pages and pagetables. This allocator will never invoke free.
+ * @param page_directory page directory for the new vspace.
+ * @param allocated_object_fn function to call when objects are allocated. Can be null.
+ * @param allocated_object_cookie cookie passed when the above function is called. Can be null.
+ *
+ * @return 0 on success.
+ */
+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);
+
+#ifdef CONFIG_VTX
+/**
+ * Initialise a vspace allocator for an EPT address space
+ *
+ * @param loader vspace of the current process, used to allocate
+ * virtual memory book keeping.
+ * @param new_vspace uninitialised vspace struct to populate.
+ * @param vka initialised vka that this virtual memory allocator will use to
+ * allocate pages and pagetables. This allocator will never invoke free.
+ * @param ept EPT page directory for the new vspace.
+ * @param allocated_object_fn function to call when objects are allocated. Can be null.
+ * @param allocated_object_cookie cookie passed when the above function is called. Can be null.
+ *
+ * @return 0 on success.
+ */
+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);
+#endif /* CONFIG_VTX */
+
+/**
+ * Initialise a vspace allocator for the current address space (this is intended
+ * for use a task that is not the root task but has no vspace, ie one loaded by the capDL loader).
+ *
+ * @param vspace uninitialised vspace struct to populate.
+ * @param data uninitialised vspace data struct to populate.
+ * @param vka initialised vka that this virtual memory allocator will use to
+ * allocate pages and pagetables. This allocator will never invoke free.
+ * @param page_directory page directory for the new vspace.
+ * @param allocated_object_fn function to call when objects are allocated. Can be null.
+ * @param allocated_object_cookie cookie passed when the above function is called. Can be null.
+ * @param existing_frames a NULL terminated list of virtual addresses for 4K frames that are
+ * already allocated. For larger frames, just pass in the virtual
+ * address range in 4K addresses. This will prevent the allocator
+ * from overriding these frames.
+ *
+ * @return 0 on succes.
+ *
+ */
+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 *allocated_object_cookie,
+ void *existing_frames[]);
+
+/**
+ * Initialise a vspace allocator for the current address space (this is intended
+ * for use by the root task). Take details of existing frames from bootinfo.
+ *
+ * @param vspace uninitialised vspace struct to populate.
+ * @param data uninitialised vspace data struct to populate.
+ * @param vka initialised vka that this virtual memory allocator will use to
+ * allocate pages and pagetables. This allocator will never invoke free.
+ * @param info seL4 boot info
+ * @param page_directory page directory for the new vspace.
+ * @param allocated_object_fn function to call when objects are allocated. Can be null.
+ * @param allocated_object_cookie cookie passed when the above function is called. Can be null.
+ *
+ * @return 0 on succes.
+ *
+ */
+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);
+
+/* Wrapper function that configures a vspaceator such that all allocated objects are not
+ * tracked.
+ */
+static inline int
+sel4utils_get_vspace_leaky(vspace_t *loader, vspace_t *new_vspace, sel4utils_alloc_data_t *data,
+ vka_t *vka, seL4_CPtr page_directory)
+{
+ return sel4utils_get_vspace(loader, new_vspace, data, vka, page_directory,
+ (vspace_allocated_object_fn) NULL, NULL);
+}
+
+#ifdef CONFIG_VTX
+static inline int
+sel4utils_get_vspace_ept_leaky(vspace_t *loader, vspace_t *new_vspace,
+ vka_t *vka, seL4_CPtr page_directory)
+{
+ return sel4utils_get_vspace_ept(loader, new_vspace, vka, page_directory,
+ (vspace_allocated_object_fn) NULL, NULL);
+}
+#endif /* CONFIG_VTX */
+
+static inline int
+sel4utils_bootstrap_vspace_with_bootinfo_leaky(vspace_t *vspace, sel4utils_alloc_data_t *data, seL4_CPtr page_directory,
+ vka_t *vka, seL4_BootInfo *info)
+{
+ return sel4utils_bootstrap_vspace_with_bootinfo(vspace, data, page_directory, vka, info, NULL, NULL);
+}
+
+static inline int
+sel4utils_bootstrap_vspace_leaky(vspace_t *vspace, sel4utils_alloc_data_t *data, seL4_CPtr page_directory, vka_t *vka,
+ void *existing_frames[])
+{
+ return sel4utils_bootstrap_vspace(vspace, data, page_directory, vka, NULL, NULL, existing_frames);
+}
+
+/**
+ * Attempts to create a new vspace reservation. Function behaves similarly to vspace_reserve_range
+ * except a reservation struct is passed in, instead of being malloc'ed. This is intended to be
+ * used during bootstrapping where malloc has not yet been setup.
+ * Reservations created with this function should *only* be freed with sel4utils_reserve_range_at_no_alloc
+ *
+ * @param vspace the virtual memory allocator to use.
+ * @param reservation Allocated reservation struct to fill out
+ * @param bytes the size in bytes to map.
+ * @param rights the rights to map the pages in with in this reservation
+ * @param cacheable 1 if the pages should be mapped with cacheable attributes. 0 for DMA.
+ * @param vaddr the virtual address of the reserved range will be returned here.
+ *
+ * @param Returns 0 on success
+ */
+int sel4utils_reserve_range_no_alloc(vspace_t *vspace, reservation_t *reservation, size_t size,
+ seL4_CapRights rights, int cacheable, void **result);
+
+/**
+ * Attempts to create a new vspace reservation. Function behaves similarly to vspace_reserve_range_at
+ * except a reservation struct is passed in, instead of being malloc'ed. This is intended to be
+ * used during bootstrapping where malloc has not yet been setup.
+ * Reservations created with this function should *only* be freed with sel4utils_reserve_range_at_no_alloc
+ *
+ * @param vspace the virtual memory allocator to use.
+ * @param reservation Allocated reservation struct to fill out
+ * @param vaddr the virtual address to start the range at.
+ * @param bytes the size in bytes to map.
+ * @param rights the rights to map the pages in with in this reservatio
+ * @param cacheable 1 if the pages should be mapped with cacheable attributes. 0 for DMA.
+ *
+ * @param Returns 0 on success
+ */
+int sel4utils_reserve_range_at_no_alloc(vspace_t *vspace, reservation_t *reservation, void *vaddr,
+ size_t size, seL4_CapRights rights, int cacheable);
+
+/**
+ * Frees a reservation. Function behaves similarly to vspace_free_reservation, except
+ * it should only be called on reservations that were created with sel4utils_reserve_range_no_alloc
+ * and sel4utils_reserve_range_at_no_alloc
+ * @param vspace the virtual memory allocator to use.
+ * @param reservation the reservation to free.
+ */
+void sel4utils_free_reservation_no_alloc(vspace_t *vspace, reservation_t *reservation);
+
+/*
+ * Copy the code and data segment (the image effectively) from current vspace
+ * into clone vspace. The clone vspace should be initialised.
+ *
+ * @param current the vspace to copy from.
+ * @param clone the vspace to copy to.
+ * @param reservation the previously established reservation in clone to copy.
+ * @return 0 on success.
+ */
+int sel4utils_bootstrap_clone_into_vspace(vspace_t *current, vspace_t *clone, reservation_t *reserve);
+
+/**
+ * Get the bounds of _executable_start and _end.
+ *
+ * @param va_start return va_start.
+ * @param va_end return va_end.
+ */
+void sel4utils_get_image_region(seL4_Word *va_start, seL4_Word *va_end);
+
+#endif /* CONFIG_LIB_SEL4_VSPACE && CONFIG_LIB_SEL4_VKA */
+#endif /* _UTILS_VSPACE_H */
diff --git a/include/sel4utils/vspace_internal.h b/include/sel4utils/vspace_internal.h
new file mode 100644
index 0000000..f1b78b2
--- /dev/null
+++ b/include/sel4utils/vspace_internal.h
@@ -0,0 +1,217 @@
+/*
+ * 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)
+ */
+
+#ifndef __SEL4UILS_VSPACE_PRIVATE_H
+#define __SEL4UILS_VSPACE_PRIVATE_H
+
+#include <vka/vka.h>
+#include <vspace/vspace.h>
+
+#include <sel4utils/util.h>
+#include <sel4utils/mapping.h>
+#include <sel4utils/vspace.h>
+
+#define KERNEL_RESERVED_START 0xE0000000
+#define KERNEL_RESERVED_END 0xFFFFF000
+
+#define RESERVED 0xFFFFFFFF
+#define EMPTY 0
+
+/* Bits to remove to get to the start of the second level translation bits. There are
+ * many implicit assumptions in the code that this is actually 12 bits and hence
+ * translation addresses can be stepped using the PAGE_SIZE_4K constant. */
+#ifdef CONFIG_X86_64
+#define BOTTOM_LEVEL_BITS_OFFSET (30 - 2 * VSPACE_LEVEL_BITS)
+#else
+#define BOTTOM_LEVEL_BITS_OFFSET (seL4_WordBits - 2 * VSPACE_LEVEL_BITS)
+#endif
+
+/* Bits to remove to get to the start of the first level translation bits */
+#ifdef CONFIG_X86_64
+#define TOP_LEVEL_BITS_OFFSET (30 - VSPACE_LEVEL_BITS)
+#else
+#define TOP_LEVEL_BITS_OFFSET (seL4_WordBits - VSPACE_LEVEL_BITS)
+#endif
+
+#define LEVEL_MASK MASK_UNSAFE(VSPACE_LEVEL_BITS)
+
+#define BOTTOM_LEVEL_INDEX(x) ((((uint32_t) ((seL4_Word)(x))) >> BOTTOM_LEVEL_BITS_OFFSET) & LEVEL_MASK)
+#define TOP_LEVEL_INDEX(x) ((((uint32_t) ((seL4_Word)(x))) >> TOP_LEVEL_BITS_OFFSET) & LEVEL_MASK)
+
+int assure_level(vspace_t *vspace, void *vaddr);
+int bootstrap_create_level(vspace_t *vspace, void *vaddr);
+
+static inline sel4utils_alloc_data_t *
+get_alloc_data(vspace_t *vspace)
+{
+ return (sel4utils_alloc_data_t *) vspace->data;
+}
+
+static inline int
+update_entry(vspace_t *vspace, void *vaddr, seL4_CPtr page)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ if (assure_level(vspace, vaddr) != seL4_NoError) {
+ return -1;
+ }
+
+ assert(data->top_level[TOP_LEVEL_INDEX(vaddr)] != (void *) RESERVED);
+ assert(data->top_level[TOP_LEVEL_INDEX(vaddr)] != NULL);
+ data->top_level[TOP_LEVEL_INDEX(vaddr)]->bottom_level[BOTTOM_LEVEL_INDEX(vaddr)] = page;
+
+ return seL4_NoError;
+}
+
+static inline int
+update(vspace_t *vspace, void *vaddr, seL4_CPtr page)
+{
+
+#if 0
+ if (page == RESERVED) {
+ LOG_ERROR("Cap %x cannot be used!", RESERVED);
+ return -1;
+ }
+#endif
+ assert(page != 0);
+ assert(get_alloc_data(vspace)->top_level[TOP_LEVEL_INDEX(vaddr)] != (void *) RESERVED);
+ return update_entry(vspace, vaddr, page);
+}
+
+static inline int
+reserve(vspace_t *vspace, void *vaddr)
+{
+ assert(get_alloc_data(vspace)->top_level[TOP_LEVEL_INDEX(vaddr)] != (void *) RESERVED);
+ return update_entry(vspace, vaddr, RESERVED);
+}
+
+static inline void
+clear(vspace_t *vspace, void *vaddr)
+{
+ /* if we are clearing an entry it should have been allocated before */
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ assert(data->top_level[TOP_LEVEL_INDEX(vaddr)] != NULL);
+ assert(data->top_level[TOP_LEVEL_INDEX(vaddr)] != (void *) RESERVED);
+
+ update_entry(vspace, vaddr, 0);
+ if (vaddr < data->last_allocated) {
+ data->last_allocated = vaddr;
+ }
+}
+
+static inline seL4_CPtr
+get_entry(bottom_level_t *top[], void *vaddr)
+{
+ if (top[TOP_LEVEL_INDEX(vaddr)] == NULL) {
+ return 0;
+ }
+
+ return top[TOP_LEVEL_INDEX(vaddr)]->bottom_level[BOTTOM_LEVEL_INDEX(vaddr)];
+}
+
+/* update entry in page table and handle large pages */
+static inline int
+update_entries(vspace_t *vspace, void *vaddr, seL4_CPtr cap, size_t size_bits)
+{
+ int error = seL4_NoError;
+ for (int i = 0; i < (1 << size_bits) && error == seL4_NoError; i += PAGE_SIZE_4K) {
+ error = update(vspace, vaddr + i, cap);
+ }
+
+ return error;
+}
+
+/* reserve entry in page table and handle large pages */
+static inline int
+reserve_entries(vspace_t *vspace, void *vaddr, size_t size_bits)
+{
+ int error = seL4_NoError;
+ for (int i = 0; i < (1 << size_bits) && error == seL4_NoError; i += PAGE_SIZE_4K) {
+ error = reserve(vspace, vaddr + i);
+ }
+
+ return error;
+}
+
+/* clear an entry in the page table and handle large pages */
+static inline void
+clear_entries(vspace_t *vspace, void *vaddr, size_t size_bits)
+{
+ assert( ((uintptr_t)vaddr & ((1 << size_bits) - 1)) == 0);
+ for (int i = 0; i < (1 << size_bits); i += PAGE_SIZE_4K) {
+ clear(vspace, vaddr + i);
+ }
+}
+
+static inline int
+is_available(bottom_level_t *top_level[VSPACE_LEVEL_SIZE], void *vaddr)
+{
+ /* if there is no bottom level page table then this entry is available */
+ if (top_level[TOP_LEVEL_INDEX(vaddr)] == NULL) {
+ return 1;
+ /* otherwise check the entry explicitly */
+ } else if (top_level[TOP_LEVEL_INDEX(vaddr)] == (void *) RESERVED) {
+ return 0;
+ }
+
+ return top_level[TOP_LEVEL_INDEX(vaddr)]->bottom_level[BOTTOM_LEVEL_INDEX(vaddr)] == 0;
+}
+
+static inline int
+is_reserved(bottom_level_t *top_level[VSPACE_LEVEL_SIZE], void *vaddr)
+{
+ if (top_level[TOP_LEVEL_INDEX(vaddr)] == (void *) RESERVED) {
+ return 1;
+ }
+
+ if (top_level[TOP_LEVEL_INDEX(vaddr)] == NULL) {
+ return 0;
+ }
+#if 0
+ printf("is reserved vaddr 0x%x 0x%x \n",vaddr, top_level[TOP_LEVEL_INDEX(vaddr)]->bottom_level[BOTTOM_LEVEL_INDEX(vaddr)]);
+#endif
+ return top_level[TOP_LEVEL_INDEX(vaddr)]->bottom_level[BOTTOM_LEVEL_INDEX(vaddr)] == RESERVED;
+}
+
+/* Internal interface functions */
+int sel4utils_map_page_pd(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights, int cacheable, size_t size_bits);
+#ifdef CONFIG_VTX
+int sel4utils_map_page_ept(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights, int cacheable, size_t size_bits);
+#endif /* CONFIG_VTX */
+
+/* interface functions */
+int sel4utils_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], void *vaddr,
+ size_t num_pages, size_t size_bits, reservation_t *reservation);
+seL4_CPtr sel4utils_get_cap(vspace_t *vspace, void *vaddr);
+void *sel4utils_map_pages(vspace_t *vspace, seL4_CPtr caps[], seL4_CapRights rights,
+ size_t num_pages, size_t size_bits, int cacheable);
+void sel4utils_unmap_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits);
+
+int sel4utils_unmap_reserved_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits, reservation_t *reservation);
+
+int sel4utils_new_pages_at_vaddr(vspace_t *vspace, void *vaddr, size_t num_pages,
+ size_t size_bits, reservation_t *reservation);
+void *sel4utils_new_pages(vspace_t *vspace, seL4_CapRights rights, size_t num_pages,
+ size_t size_bits);
+void sel4utils_free_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits);
+
+void *sel4utils_new_stack(vspace_t *vspace);
+void sel4utils_free_stack(vspace_t *vspace, void *stack_top);
+
+void * sel4utils_new_ipc_buffer(vspace_t *vspace, seL4_CPtr *page);
+void sel4utils_free_ipc_buffer(vspace_t *vspace, void *vaddr);
+
+reservation_t *sel4utils_reserve_range(vspace_t *vspace, size_t size, seL4_CapRights rights,
+ int cacheable, void **vaddr);
+reservation_t *sel4utils_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size,
+ seL4_CapRights rights, int cacheable);
+void sel4utils_free_reservation(vspace_t *vspace, reservation_t *reservation);
+
+#endif /* __SEL4UILS_VSPACE_PRIVATE_H */
diff --git a/src/elf.c b/src/elf.c
new file mode 100644
index 0000000..734439f
--- /dev/null
+++ b/src/elf.c
@@ -0,0 +1,303 @@
+/*
+ * 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_VKA && defined CONFIG_LIB_SEL4_VSPACE)
+
+#include <string.h>
+#include <sel4/sel4.h>
+#include <elf/elf.h>
+#include <cpio/cpio.h>
+#include <vka/capops.h>
+#include <sel4utils/thread.h>
+#include <sel4utils/util.h>
+#include <sel4utils/mapping.h>
+#include <sel4utils/elf.h>
+
+#ifdef CONFIG_X86_64
+#define SZFMT "%ld"
+#else
+#define SZFMT "%u"
+#endif
+
+/* This library works with our cpio set up in the build system */
+extern char _cpio_archive[];
+
+/*
+ * Convert ELF permissions into seL4 permissions.
+ *
+ * @param permissions elf permissions
+ * @return seL4 permissions
+ */
+static inline seL4_CapRights
+rights_from_elf(unsigned long permissions)
+{
+ seL4_CapRights result = 0;
+
+ if (permissions & PF_R || permissions & PF_X) {
+ result |= seL4_CanRead;
+ }
+
+ if (permissions & PF_W) {
+ result |= seL4_CanWrite;
+ }
+
+ return result;
+}
+
+static int
+load_segment(vspace_t *loadee_vspace, vspace_t *loader_vspace,
+ vka_t *loadee_vka, vka_t *loader_vka,
+ char *src, size_t segment_size, size_t file_size, uint32_t dst,
+ reservation_t *reservation)
+{
+ int error = seL4_NoError;
+
+ if (file_size > segment_size) {
+ LOG_ERROR("Error, file_size "SZFMT" > segment_size "SZFMT, file_size, segment_size);
+ return seL4_InvalidArgument;
+ }
+
+ /* create a slot to map a page into the loader address space */
+ seL4_CPtr loader_slot;
+ cspacepath_t loader_frame_cap;
+
+ error = vka_cspace_alloc(loader_vka, &loader_slot);
+ if (error) {
+ LOG_ERROR("Failed to allocate cslot by loader vka: %d", error);
+ return error;
+ }
+ vka_cspace_make_path(loader_vka, loader_slot, &loader_frame_cap);
+
+ /* We work a page at a time */
+ unsigned int pos = 0;
+ while (pos < segment_size && error == seL4_NoError) {
+ void *loader_vaddr = 0;
+ void *loadee_vaddr = (void *) ((seL4_Word)ROUND_DOWN(dst, PAGE_SIZE_4K));
+
+ /* create and map the frame in the loadee address space */
+ error = vspace_new_pages_at_vaddr(loadee_vspace, loadee_vaddr, 1, seL4_PageBits, reservation);
+ if (error != seL4_NoError) {
+ LOG_ERROR("ERROR: failed to allocate frame by loadee vka: %d", error);
+ continue;
+ }
+
+ /* copy the frame cap to map into the loader address space */
+ cspacepath_t loadee_frame_cap;
+
+ vka_cspace_make_path(loadee_vka, vspace_get_cap(loadee_vspace, loadee_vaddr),
+ &loadee_frame_cap);
+ error = vka_cnode_copy(&loader_frame_cap, &loadee_frame_cap, seL4_AllRights);
+ if (error != seL4_NoError) {
+ LOG_ERROR("ERROR: failed to copy frame cap into loader cspace: %d", error);
+ continue;
+ }
+
+ /* map the frame into the loader address space */
+ loader_vaddr = vspace_map_pages(loader_vspace, &loader_frame_cap.capPtr, seL4_AllRights,
+ 1, seL4_PageBits, 1);
+ if (loader_vaddr == NULL) {
+ LOG_ERROR("failed to map frame into loader vspace.");
+ error = -1;
+ continue;
+ }
+
+ /* finally copy the data */
+ int nbytes = PAGE_SIZE_4K - (dst & PAGE_MASK_4K);
+ if (pos < file_size) {
+ memcpy(loader_vaddr + (dst % PAGE_SIZE_4K), (void*)src, MIN(nbytes, file_size - pos));
+ }
+ /* Note that we don't need to explicitly zero frames as seL4 gives us zero'd frames */
+
+#ifdef CONFIG_ARCH_ARM
+ /* Flush the caches */
+ seL4_ARM_Page_Unify_Instruction(loader_frame_cap.capPtr,0, PAGE_SIZE_4K);
+ seL4_ARM_Page_Unify_Instruction(loadee_frame_cap.capPtr,0, PAGE_SIZE_4K);
+#endif /* CONFIG_ARCH_ARM */
+
+ /* now unmap the page in the loader address space */
+ vspace_unmap_pages(loader_vspace, (void *) loader_vaddr, 1, seL4_PageBits);
+ vka_cnode_delete(&loader_frame_cap);
+
+ pos += nbytes;
+ dst += nbytes;
+ src += nbytes;
+ }
+
+ /* clear the cslot */
+ vka_cspace_free(loader_vka, loader_frame_cap.capPtr);
+
+ return error;
+}
+
+int
+sel4utils_elf_num_regions(char *image_name)
+{
+ int i;
+ unsigned long elf_size;
+ char *elf_file;
+ assert(image_name);
+ elf_file = cpio_get_file(_cpio_archive, image_name, &elf_size);
+ if (elf_file == NULL) {
+ LOG_ERROR("ERROR: failed to load elf file %s", image_name);
+ return 0;
+ }
+
+ int num_headers = elf_getNumProgramHeaders(elf_file);
+ int loadable_headers = 0;
+
+ for (i = 0; i < num_headers; i++) {
+ /* Skip non-loadable segments (such as debugging data). */
+ if (elf_getProgramHeaderType(elf_file, i) == PT_LOAD) {
+ loadable_headers++;
+ }
+ }
+ return loadable_headers;
+}
+
+static int
+make_region(vspace_t *loadee, unsigned long flags, unsigned long segment_size,
+ unsigned long vaddr, sel4utils_elf_region_t *region, int anywhere)
+{
+ region->cacheable = 1;
+ region->rights = rights_from_elf(flags);
+ region->elf_vstart = (void*)PAGE_ALIGN_4K(vaddr);
+ region->size = PAGE_ALIGN_4K(vaddr + segment_size - 1) + PAGE_SIZE_4K - (uint32_t)((seL4_Word)region->elf_vstart);
+
+ if (loadee) {
+ if (anywhere) {
+ region->reservation = vspace_reserve_range(loadee, region->size, region->rights, 1, (void**)®ion->reservation_vstart);
+ } else {
+ region->reservation_vstart = region->elf_vstart;
+ region->reservation = vspace_reserve_range_at(loadee,
+ region->elf_vstart,
+ region->size,
+ region->rights,
+ 1);
+ }
+ return !region->reservation;
+ }
+
+ return 0;
+}
+
+void *
+sel4utils_elf_reserve(vspace_t *loadee, char *image_name, sel4utils_elf_region_t *regions)
+{
+ unsigned long elf_size;
+ char *elf_file = cpio_get_file(_cpio_archive, image_name, &elf_size);
+ if (elf_file == NULL) {
+ LOG_ERROR("ERROR: failed to load elf file %s", image_name);
+ return NULL;
+ }
+
+ int num_headers = elf_getNumProgramHeaders(elf_file);
+ int region = 0;
+
+ for (int i = 0; i < num_headers; i++) {
+ unsigned long flags, segment_size, vaddr;
+
+ /* Skip non-loadable segments (such as debugging data). */
+ if (elf_getProgramHeaderType(elf_file, i) == PT_LOAD) {
+ /* Fetch information about this segment. */
+ segment_size = elf_getProgramHeaderMemorySize(elf_file, i);
+ vaddr = elf_getProgramHeaderVaddr(elf_file, i);
+ flags = elf_getProgramHeaderFlags(elf_file, i);
+ if (make_region(loadee, flags, segment_size, vaddr, ®ions[region], 0)) {
+ for (region--; region >= 0; region--) {
+ vspace_free_reservation(loadee, regions[region].reservation);
+ regions[region].reservation = NULL;
+ }
+ LOG_ERROR("Failed to create reservation");
+ return NULL;
+ }
+ region++;
+ }
+ }
+
+ uint64_t entry_point = elf_getEntryPoint(elf_file);
+ if ((uint32_t) (entry_point >> 32) != 0) {
+ LOG_ERROR("ERROR: this code hasn't been tested for 64bit!");
+ return NULL;
+ }
+ assert(entry_point != 0);
+ return (void*)(seL4_Word)entry_point;
+}
+
+void *
+sel4utils_elf_load_record_regions(vspace_t *loadee, vspace_t *loader, vka_t *loadee_vka, vka_t *loader_vka, char *image_name, sel4utils_elf_region_t *regions, int mapanywhere)
+{
+ unsigned long elf_size;
+ char *elf_file = cpio_get_file(_cpio_archive, image_name, &elf_size);
+ if (elf_file == NULL) {
+ LOG_ERROR("ERROR: failed to load elf file %s", image_name);
+ return NULL;
+ }
+
+ int num_headers = elf_getNumProgramHeaders(elf_file);
+ int error = seL4_NoError;
+ int region_count = 0;
+
+ uint64_t entry_point = elf_getEntryPoint(elf_file);
+ if ((uint32_t) (entry_point >> 32) != 0) {
+ LOG_ERROR("ERROR: this code hasn't been tested for 64bit!");
+ return NULL;
+ }
+ assert(entry_point != 0);
+
+ for (int i = 0; i < num_headers; i++) {
+ char *source_addr;
+ unsigned long flags, file_size, segment_size, vaddr;
+
+ /* Skip non-loadable segments (such as debugging data). */
+ if (elf_getProgramHeaderType(elf_file, i) == PT_LOAD) {
+ /* Fetch information about this segment. */
+ source_addr = elf_file + elf_getProgramHeaderOffset(elf_file, i);
+ file_size = elf_getProgramHeaderFileSize(elf_file, i);
+ segment_size = elf_getProgramHeaderMemorySize(elf_file, i);
+ vaddr = elf_getProgramHeaderVaddr(elf_file, i);
+ flags = elf_getProgramHeaderFlags(elf_file, i);
+ /* make reservation */
+ sel4utils_elf_region_t region;
+ error = make_region(loadee, flags, segment_size, vaddr, ®ion, mapanywhere);
+ if (error) {
+ LOG_ERROR("Failed to reserve region");
+ break;
+ }
+ unsigned long offset = vaddr - PAGE_ALIGN_4K(vaddr);
+ /* Copy it across to the vspace */
+ LOG_INFO(" * Loading segment %08x-->%08x", (int)vaddr, (int)(vaddr + segment_size));
+ error = load_segment(loadee, loader, loadee_vka, loader_vka, source_addr,
+ segment_size, file_size, offset + (uint32_t)((seL4_Word)region.reservation_vstart), region.reservation);
+ if (error) {
+ LOG_ERROR("Failed to load segment");
+ break;
+ }
+ /* record the region if requested */
+ if (regions) {
+ regions[region_count] = region;
+ } else {
+ vspace_free_reservation(loadee, region.reservation);
+ }
+ /* increment the count of the number of loaded regions */
+ region_count++;
+ }
+ }
+
+ return error == seL4_NoError ? (void*)(seL4_Word)entry_point : NULL;
+}
+
+void *
+sel4utils_elf_load(vspace_t *loadee, vspace_t *loader, vka_t *loadee_vka, vka_t *loader_vka, char *image_name)
+{
+ return sel4utils_elf_load_record_regions(loadee, loader, loadee_vka, loader_vka, image_name, NULL, 0);
+}
+
+#endif /* (defined CONFIG_LIB_SEL4_VKA && defined CONFIG_LIB_SEL4_VSPACE) */
diff --git a/src/helpers.h b/src/helpers.h
new file mode 100644
index 0000000..d9d02da
--- /dev/null
+++ b/src/helpers.h
@@ -0,0 +1,23 @@
+/*
+ * 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)
+ */
+
+#ifndef SEL4UTILS_HELPERS_H
+#define SEL4UTILS_HELPERS_H
+/**
+ * Start a thread.
+ *
+ * @param stack_top address of the stack in the current vspace.
+ * Other parameters see sel4utils_start_thread.
+ */
+int sel4utils_internal_start_thread(sel4utils_thread_t *thread, void *entry_point, void *arg0,
+ void *arg1, int resume, void *stack_top);
+
+
+#endif /* SEL4UTILS_HELPERS_H */
diff --git a/src/mapping.c b/src/mapping.c
new file mode 100644
index 0000000..fe97abf
--- /dev/null
+++ b/src/mapping.c
@@ -0,0 +1,263 @@
+/*
+ * 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>
+
+#ifdef CONFIG_LIB_SEL4_VKA
+
+#include <sel4/sel4.h>
+#include <vka/object.h>
+#include <sel4utils/mapping.h>
+#include <sel4utils/util.h>
+
+#ifndef DFMT
+#ifdef CONFIG_X86_64
+#define DFMT "%lld"
+#else
+#define DFMT "%d"
+#endif
+#endif
+
+int
+sel4utils_map_page(vka_t *vka, seL4_CPtr pd, seL4_CPtr frame, void *vaddr,
+ seL4_CapRights rights, int cacheable, vka_object_t *pagetable)
+{
+ assert(vka != NULL);
+ assert(pd != 0);
+ assert(frame != 0);
+ assert(vaddr != 0);
+ assert(rights != 0);
+ assert(pagetable != NULL);
+
+ seL4_ARCH_VMAttributes attr = 0;
+
+#ifdef CONFIG_ARCH_IA32
+ if (!cacheable) {
+ attr = seL4_IA32_CacheDisabled;
+ }
+#elif CONFIG_ARCH_ARM /* CONFIG_ARCH_IA32 */
+ if (cacheable) {
+ attr = seL4_ARM_PageCacheable;
+ }
+#endif /* CONFIG_ARCH_ARM */
+ int error = seL4_ARCH_Page_Map(frame, pd, (seL4_Word) vaddr, rights, attr);
+
+#ifdef CONFIG_X86_64
+
+page_map_retry:
+
+ if (error == seL4_FailedLookupPDPT) {
+ error = vka_alloc_page_directory_pointer_table(vka, pagetable);
+ if (!error) {
+ error = seL4_ARCH_PageDirectoryPointerTable_Map(pagetable->cptr, pd, (seL4_Word)vaddr,
+ seL4_ARCH_Default_VMAttributes);
+ } else {
+ LOG_ERROR("Page directory pointer table allocation failed %d", error);
+ }
+
+ if (!error) {
+ error = seL4_ARCH_Page_Map(frame, pd, (seL4_Word)vaddr, rights, attr);
+ if (error != seL4_NoError) {
+ goto page_map_retry;
+ }
+ } else {
+ LOG_ERROR("Page directory pointer table mapping failed %d\n", error);
+ }
+ }
+
+ if (error == seL4_FailedLookupPD) {
+ error = vka_alloc_page_directory(vka, pagetable);
+ if (!error) {
+ error = seL4_ARCH_PageDirectory_Map(pagetable->cptr, pd, (seL4_Word)vaddr,
+ seL4_ARCH_Default_VMAttributes);
+ } else {
+ LOG_ERROR("Page direcotry allocation failed %d\n", error);
+ }
+
+ if (!error) {
+ error = seL4_ARCH_Page_Map(frame, pd, (seL4_Word)vaddr, rights, attr);
+ if (error != seL4_NoError) {
+ goto page_map_retry;
+ }
+
+ } else {
+ LOG_ERROR("Page directory mapping failed %d\n", error);
+ }
+ }
+
+#endif
+
+ if (error == seL4_FailedLookup) {
+ /* need a page table, allocate one */
+ error = vka_alloc_page_table(vka, pagetable);
+
+ /* map in the page table */
+ if (!error) {
+ error = seL4_ARCH_PageTable_Map(pagetable->cptr, pd, (seL4_Word) vaddr,
+ seL4_ARCH_Default_VMAttributes);
+ } else {
+ LOG_ERROR("Page table allocation failed, %d", error);
+ }
+
+ /* now map in the frame again, if pagetable allocation was successful */
+ if (!error) {
+ error = seL4_ARCH_Page_Map(frame, pd, (seL4_Word) vaddr, rights, attr);
+ } else {
+ LOG_ERROR("Page table mapping failed, %d", error);
+ }
+ }
+
+ if (error != seL4_NoError) {
+ LOG_ERROR("Failed to map page at address %p with cap "DFMT", error: %d", vaddr, frame, error);
+ }
+
+ return error;
+}
+
+#ifdef CONFIG_ARCH_IA32
+
+#ifdef CONFIG_IOMMU
+int
+sel4utils_map_iospace_page(vka_t *vka, seL4_CPtr iospace, seL4_CPtr frame, seL4_Word vaddr,
+ seL4_CapRights rights, int cacheable, seL4_Word size_bits,
+ vka_object_t *pts, int *num_pts)
+{
+ int error;
+ int num;
+ assert(vka);
+ assert(iospace);
+ assert(frame);
+ assert(cacheable);
+ assert(size_bits == seL4_PageBits);
+ /* Start mapping in pages and page tables until it bloody well works */
+ num = 0;
+ while ( (error = seL4_IA32_Page_MapIO(frame, iospace, rights, vaddr)) == seL4_FailedLookup && error != seL4_NoError) {
+ /* Need a page table? */
+ vka_object_t pt;
+ error = vka_alloc_io_page_table(vka, &pt);
+ if (error) {
+ return error;
+ }
+ if (pts) {
+ pts[num] = pt;
+ num++;
+ assert(num_pts);
+ *num_pts = num;
+ }
+ error = seL4_IA32_IOPageTable_Map(pt.cptr, iospace, vaddr);
+ if (error != seL4_NoError) {
+ return error;
+ }
+ }
+ return error;
+}
+
+#endif
+
+#ifdef CONFIG_VTX
+
+/*map a frame into guest os's physical address space*/
+int
+sel4utils_map_ept_page(vka_t *vka, seL4_CPtr pd, seL4_CPtr frame, seL4_Word vaddr,
+ seL4_CapRights rights, int cacheable, seL4_Word size_bits,
+ vka_object_t *pagetable, vka_object_t *pagedir)
+{
+ int ret;
+
+ assert(vka);
+ assert(pd);
+ assert(frame);
+ assert(rights);
+ assert(size_bits);
+ assert(pagetable);
+ assert(pagedir);
+
+ seL4_ARCH_VMAttributes attr = 0;
+
+ if (!cacheable) {
+ attr = seL4_IA32_CacheDisabled;
+ }
+
+ /* Try map into EPT directory first. */
+ ret = seL4_IA32_Page_Map(frame, pd, vaddr, rights, attr);
+ if (ret == seL4_NoError) {
+ /* Successful! */
+ return ret;
+ }
+ if (ret != seL4_FailedLookup) {
+ LOG_ERROR("Failed to map page, error: %d", ret);
+ return ret;
+ }
+
+ if (size_bits == seL4_4MBits) {
+ /* Allocate a directory table for a 4M entry. */
+ ret = vka_alloc_ept_page_directory(vka, pagedir);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("Allocation of EPT page directory failed, error: %d", ret);
+ return ret;
+ }
+
+ /* Map in the page directory. */
+ ret = seL4_IA32_EPTPageDirectory_Map(pagedir->cptr, pd, vaddr, attr);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("Failed to map EPT PD, error: %d", ret);
+ return ret;
+ }
+ } else {
+ /* Allocate an EPT page table for a 4K entry. */
+ ret = vka_alloc_ept_page_table(vka, pagetable);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("allocating ept page table failed\n");
+ return ret;
+ }
+
+ /* Map in the EPT page table. */
+ ret = seL4_IA32_EPTPageTable_Map(pagetable->cptr, pd, vaddr, attr);
+
+ /* Mapping could fail due to missing PD. In this case, we map the PD and try again. */
+ if (ret == seL4_FailedLookup) {
+ /* Allocate an EPT page directory for the page table. */
+ ret = vka_alloc_ept_page_directory(vka, pagedir);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("Allocating EPT page directory failed\n");
+ return ret;
+ }
+
+ /* Map the EPT page directory in. */
+ ret = seL4_IA32_EPTPageDirectory_Map(pagedir->cptr, pd, vaddr, attr);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("Failed to map EPT PD, error: %d", ret);
+ return ret;
+ }
+
+ /* Try to map the page table again. */
+ ret = seL4_IA32_EPTPageTable_Map(pagetable->cptr, pd, vaddr, attr);
+ if (ret != seL4_NoError) {
+ LOG_ERROR("Second attempt at mapping EPT PT failed, error: %d", ret);
+ return ret;
+ }
+ } else if (ret) {
+ LOG_ERROR("EPT PT failed to map, error: %d", ret);
+ return ret;
+ }
+ }
+
+ if (ret != seL4_NoError) {
+ return ret;
+ }
+
+ /* Try to map the frame again. */
+ return seL4_IA32_Page_Map(frame, pd, vaddr, rights, attr);
+}
+
+
+#endif
+#endif
+#endif /* CONFIG_LIB_SEL4_VKA */
diff --git a/src/process.c b/src/process.c
new file mode 100644
index 0000000..2d4ce98
--- /dev/null
+++ b/src/process.c
@@ -0,0 +1,565 @@
+/*
+ * 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_VKA && defined CONFIG_LIB_SEL4_VSPACE)
+
+#include <stdlib.h>
+#include <string.h>
+#include <stdio.h>
+#include <sel4/sel4.h>
+#include <vka/object.h>
+#include <vka/capops.h>
+#include <sel4utils/vspace.h>
+#include <sel4utils/process.h>
+#include <sel4utils/util.h>
+#include <sel4utils/elf.h>
+#include <sel4utils/mapping.h>
+#include "helpers.h"
+
+static size_t
+compute_length(int argc, char **argv)
+{
+ size_t length = 0;
+
+ assert(argv != NULL);
+ for (int i = 0; i < argc; i++) {
+ assert(argv[i] != NULL);
+ length += strlen(argv[i]) + 1;
+ }
+
+ return length;
+}
+
+static int recurse = 0;
+
+void
+sel4utils_allocated_object(void *cookie, vka_object_t object)
+{
+ if (recurse == 1) {
+ assert(!"VSPACE RECURSION ON MALLOC, YOU ARE DEAD\n");
+ }
+ recurse = 1;
+
+ sel4utils_process_t *process = (sel4utils_process_t *) cookie;
+
+ object_node_t *node = (object_node_t *) malloc(sizeof(object_node_t));
+ assert(node != NULL);
+ node->object = object;
+
+ node->next = process->allocated_object_list_head;
+ process->allocated_object_list_head = node;
+
+ recurse = 0;
+}
+
+static void
+clear_objects(sel4utils_process_t *process, vka_t *vka)
+{
+ assert(process != NULL);
+ assert(vka != NULL);
+
+ while (process->allocated_object_list_head != NULL) {
+ object_node_t *prev = process->allocated_object_list_head;
+
+ process->allocated_object_list_head = prev->next;
+
+ vka_free_object(vka, &prev->object);
+ free(prev);
+ }
+}
+
+static int
+next_free_slot(sel4utils_process_t *process, cspacepath_t *dest)
+{
+ if (process->cspace_next_free >= (1 << process->cspace_size)) {
+ LOG_ERROR("Can't allocate slot, cspace is full.\n");
+ return -1;
+ }
+
+ dest->root = process->cspace.cptr;
+ dest->capPtr = process->cspace_next_free;
+ dest->capDepth = process->cspace_size;
+
+ return 0;
+}
+
+static void
+allocate_next_slot(sel4utils_process_t *process)
+{
+ assert(process->cspace_next_free < (1 << process->cspace_size));
+ process->cspace_next_free++;
+}
+
+
+seL4_CPtr
+sel4utils_mint_cap_to_process(sel4utils_process_t *process, cspacepath_t src, seL4_CapRights rights, seL4_CapData_t data)
+{
+ cspacepath_t dest;
+ if (next_free_slot(process, &dest) == -1) {
+ return 0;
+ }
+
+ int error = vka_cnode_mint(&dest, &src, rights, data);
+ if (error != seL4_NoError) {
+ LOG_ERROR("Failed to mint cap\n");
+ return 0;
+ }
+
+ /* success */
+ allocate_next_slot(process);
+ return dest.capPtr;
+}
+
+seL4_CPtr
+sel4utils_copy_cap_to_process(sel4utils_process_t *process, cspacepath_t src)
+{
+ cspacepath_t dest;
+ if (next_free_slot(process, &dest) == -1) {
+ return 0;
+ }
+
+ int error = vka_cnode_copy(&dest, &src, seL4_AllRights);
+ if (error != seL4_NoError) {
+ LOG_ERROR("Failed to copy cap\n");
+ return 0;
+ }
+
+ /* success */
+ allocate_next_slot(process);
+ return dest.capPtr;
+}
+
+void *
+sel4utils_copy_args(vspace_t *current_vspace, vspace_t *target_vspace,
+ vka_t *vka, int argc, char *argv[])
+{
+ assert(current_vspace != target_vspace);
+
+ size_t length = compute_length(argc, argv);
+ size_t npages UNUSED = BYTES_TO_4K_PAGES(length);
+ //TODO handle multiple pages of args. Implement this if you need it.
+ assert(npages == 1);
+
+ /* allocate pages in the target address space */
+ vka_object_t target_page = {0};
+ cspacepath_t target_cap = {0};
+ cspacepath_t current_cap = {0};
+ void *target_vaddr = NULL;
+ void *current_vaddr = NULL;
+ seL4_CPtr slot = 0;
+
+ int error = vka_alloc_frame(vka, seL4_PageBits, &target_page);
+ vka_cspace_make_path(vka, target_page.cptr, &target_cap);
+ if (error) {
+ target_page.cptr = 0;
+ LOG_ERROR("Failed to allocate frame\n");
+ goto error;
+ }
+
+ error = vka_cspace_alloc(vka, &slot);
+ if (error) {
+ slot = 0;
+ LOG_ERROR("Failed to allocate cslot\n");
+ goto error;
+ }
+
+ vka_cspace_make_path(vka, slot, ¤t_cap);
+ error = vka_cnode_copy(¤t_cap, &target_cap, seL4_AllRights);
+ if (error) {
+ LOG_ERROR("Failed to make a copy of frame cap\n");
+ current_cap.capPtr = 0;
+ goto error;
+ }
+
+ /* map the pages */
+ current_vaddr = vspace_map_pages(current_vspace, ¤t_cap.capPtr,
+ seL4_AllRights, 1, seL4_PageBits, 1);
+ if (current_vaddr == NULL) {
+ LOG_ERROR("Failed to map page into current address space\n");
+ goto error;
+ }
+
+ target_vaddr = vspace_map_pages(target_vspace, &target_cap.capPtr, seL4_CanRead,
+ 1, seL4_PageBits, 1);
+ if (target_vaddr == NULL) {
+ LOG_ERROR("Failed to map page into target address space\n");
+ goto error;
+ }
+
+ /* we aren't bailing now - inform caller we allocated a frame */
+ vspace_maybe_call_allocated_object(current_vspace, target_page);
+
+ /* do the copy */
+ char **current_argv = current_vaddr;
+ char *strings = current_vaddr + (argc * sizeof(char*));
+
+ for (int i = 0; i < argc; i++) {
+ current_argv[i] = target_vaddr + ((uint32_t) ((seL4_Word)strings) % PAGE_SIZE_4K);
+ strncpy(strings, argv[i], strlen(argv[i]) + 1);
+ strings += strlen(argv[i]) + 1;
+ }
+
+ /* flush & unmap */
+#ifdef CONFIG_ARCH_ARM
+ seL4_ARM_Page_Unify_Instruction(current_cap.capPtr, 0, PAGE_SIZE_4K);
+ seL4_ARM_Page_Unify_Instruction(target_cap.capPtr, 0, PAGE_SIZE_4K);
+#endif /* CONFIG_ARCH_ARM */
+
+ vspace_unmap_pages(current_vspace, current_vaddr, 1, seL4_PageBits);
+
+ vka_cnode_delete(¤t_cap);
+ vka_cspace_free(vka, slot);
+
+ return target_vaddr;
+
+error:
+ if (current_vaddr != NULL) {
+ vspace_unmap_pages(current_vspace, current_vaddr, 1, seL4_PageBits);
+ }
+
+ if (current_cap.capPtr != 0) {
+ vka_cnode_delete(¤t_cap);
+ }
+
+ if (slot != 0) {
+ vka_cspace_free(vka, slot);
+ }
+
+ if (target_page.cptr != 0) {
+ vka_free_object(vka, &target_page);
+ }
+
+ return NULL;
+}
+
+int
+sel4utils_spawn_process(sel4utils_process_t *process, vka_t *vka, vspace_t *vspace, int argc,
+ char *argv[], int resume)
+{
+ char **new_process_argv = NULL;
+ if (argc > 0) {
+ new_process_argv = sel4utils_copy_args(vspace, &process->vspace, vka, argc, argv);
+ if (new_process_argv == NULL) {
+ return -1;
+ }
+ }
+
+ /* On arm we write the arguments to registers */
+#ifdef CONFIG_ARCH_IA32
+ /* map in the first page of the stack for this thread */
+ seL4_CPtr page_cap = vspace_get_cap(&process->vspace, process->thread.stack_top - PAGE_SIZE_4K);
+
+ /* make a copy of the cap */
+ seL4_CPtr page_cap_copy;
+ int error = vka_cspace_alloc(vka, &page_cap_copy);
+ if (error) {
+ LOG_ERROR("Failed to allocate cslot\n");
+ return error;
+ }
+
+ cspacepath_t src, dest;
+
+ vka_cspace_make_path(vka, page_cap, &src);
+ vka_cspace_make_path(vka, page_cap_copy, &dest);
+
+ error = vka_cnode_copy(&dest, &src, seL4_AllRights);
+ if (error) {
+ LOG_ERROR("Failed to copy cap of stack page, error: %d\n", error);
+ vka_cspace_free(vka, page_cap_copy);
+ return error;
+ }
+
+ /* map the page in */
+ void *stack = vspace_map_pages(vspace, &page_cap_copy, seL4_AllRights, 1, seL4_PageBits, 1);
+
+ if (stack == NULL) {
+ LOG_ERROR("Failed to map stack page into process loading vspace\n");
+ vka_cspace_free(vka, page_cap_copy);
+ return -1;
+ }
+
+ error = sel4utils_internal_start_thread(&process->thread, process->entry_point,
+ (void *) ((seL4_Word)argc), (void *) new_process_argv, resume, stack + PAGE_SIZE_4K);
+
+ /* unmap it */
+ vspace_free_pages(vspace, stack, 1, seL4_PageBits);
+ vka_cnode_delete(&dest);
+ vka_cspace_free(vka, page_cap_copy);
+#elif CONFIG_ARCH_ARM
+ int error = sel4utils_internal_start_thread(&process->thread, process->entry_point,
+ (void *) argc, (void *) new_process_argv, resume, process->thread.stack_top);
+#endif /* CONFIG_ARCH_IA32 */
+
+ return error;
+}
+
+int
+sel4utils_configure_process(sel4utils_process_t *process, vka_t *vka,
+ vspace_t *vspace, uint8_t priority, char *image_name)
+{
+ sel4utils_process_config_t config = {
+ .is_elf = true,
+ .image_name = image_name,
+ .do_elf_load = true,
+ .create_cspace = true,
+ .one_level_cspace_size_bits = CONFIG_SEL4UTILS_CSPACE_SIZE_BITS,
+ .create_vspace = true,
+ .create_fault_endpoint = true,
+ .priority = priority,
+#ifndef CONFIG_KERNEL_STABLE
+ .asid_pool = seL4_CapInitThreadASIDPool,
+#endif
+ };
+
+ return sel4utils_configure_process_custom(process, vka, vspace, config);
+}
+
+static int
+create_reservations(vspace_t *vspace, int num, sel4utils_elf_region_t regions[])
+{
+ for (int i = 0; i < num; i++) {
+ sel4utils_elf_region_t *region = ®ions[i];
+ region->reservation = vspace_reserve_range_at(vspace, region->elf_vstart,
+ region->size, region->rights, region->cacheable);
+ if (region == NULL) {
+ LOG_ERROR("Failed to create region\n");
+ for (int j = i - 1; j >= 0; j--) {
+ free(regions[i].reservation);
+ }
+ return -1;
+ }
+ }
+
+ return 0;
+}
+
+#ifndef CONFIG_KERNEL_STABLE
+static int
+assign_asid_pool(seL4_CPtr asid_pool, seL4_CPtr pd) {
+
+ int error;
+
+ if (asid_pool == 0) {
+ LOG_INFO("This method will fail if run in a thread that is not in the root server cspace\n");
+ asid_pool = seL4_CapInitThreadASIDPool;
+ }
+
+ error = seL4_ARCH_ASIDPool_Assign(asid_pool, pd);
+ if (error) {
+ LOG_ERROR("Failed to assign asid pool\n");
+ }
+
+ return error;
+}
+#endif
+
+static int
+create_cspace(vka_t *vka, int size_bits, sel4utils_process_t *process,
+ seL4_CapData_t cspace_root_data) {
+ int error;
+
+ /* create a cspace */
+ error = vka_alloc_cnode_object(vka, size_bits, &process->cspace);
+ if (error) {
+ LOG_ERROR("Failed to create cspace: %d\n", error);
+ return error;
+ }
+
+ process->cspace_size = size_bits;
+ /* first slot is always 1, never allocate 0 as a cslot */
+ process->cspace_next_free = 1;
+
+ /* mint the cnode cap into the process cspace */
+ cspacepath_t src;
+ vka_cspace_make_path(vka, process->cspace.cptr, &src);
+ error = sel4utils_mint_cap_to_process(process, src, seL4_AllRights, cspace_root_data);
+ assert(error == SEL4UTILS_CNODE_SLOT);
+
+ return 0;
+}
+
+static int
+create_fault_endpoint(vka_t *vka, sel4utils_process_t *process)
+{
+ /* create a fault endpoint and put it into the cspace */
+ int error = vka_alloc_endpoint(vka, &process->fault_endpoint);
+ if (error) {
+ LOG_ERROR("Failed to allocate fault endpoint: %d\n", error);
+ return error;
+ }
+
+ cspacepath_t src;
+ vka_cspace_make_path(vka, process->fault_endpoint.cptr, &src);
+ error = sel4utils_copy_cap_to_process(process, src);
+
+ if (error == 0) {
+ LOG_ERROR("Failed to move allocated endpoint: %d\n", error);
+ return error;
+ }
+ assert(error == SEL4UTILS_ENDPOINT_SLOT);
+
+ return 0;
+}
+
+
+int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *vka,
+ vspace_t *spawner_vspace, sel4utils_process_config_t config)
+{
+ int error;
+ sel4utils_alloc_data_t * data = NULL;
+ memset(process, 0, sizeof(sel4utils_process_t));
+ seL4_CapData_t cspace_root_data = seL4_CapData_Guard_new(0,
+ seL4_WordBits - config.one_level_cspace_size_bits);
+
+ /* create a page directory */
+ if (config.create_vspace) {
+ error = vka_alloc_page_directory(vka, &process->pd);
+ if (error) {
+ LOG_ERROR("Failed to allocate page directory for new process: %d\n", error);
+ goto error;
+ }
+
+#ifndef CONFIG_KERNEL_STABLE
+#ifndef CONFIG_X86_64
+ /* assign an asid pool */
+ if (assign_asid_pool(config.asid_pool, process->pd.cptr) != seL4_NoError) {
+ goto error;
+ }
+#endif /* end of !CONFIG_X86_64 */
+#endif /* CONFIG_KERNEL_STABLE */
+ } else {
+ process->pd = config.page_dir;
+ }
+
+ if (config.create_cspace) {
+ if (create_cspace(vka, config.one_level_cspace_size_bits, process, cspace_root_data) != 0) {
+ goto error;
+ }
+ } else {
+ process->cspace = config.cnode;
+ }
+
+ if (config.create_fault_endpoint) {
+ if (create_fault_endpoint(vka, process) != 0) {
+ goto error;
+ }
+ } else {
+ process->fault_endpoint = config.fault_endpoint;
+ }
+
+ /* create a vspace */
+ if (config.create_vspace) {
+ sel4utils_get_vspace(spawner_vspace, &process->vspace, &process->data, vka, process->pd.cptr,
+ sel4utils_allocated_object, (void *) process);
+
+ if (config.num_reservations > 0) {
+ if (create_reservations(&process->vspace, config.num_reservations,
+ config.reservations)) {
+ goto error;
+ }
+ }
+ } else {
+ memcpy(&process->vspace, config.vspace, sizeof(process->vspace));
+ }
+
+ /* finally elf load */
+ if (config.is_elf) {
+ if (config.do_elf_load) {
+ process->entry_point = sel4utils_elf_load(&process->vspace, spawner_vspace, vka, vka, config.image_name);
+ } else {
+ process->num_elf_regions = sel4utils_elf_num_regions(config.image_name);
+ process->elf_regions = calloc(process->num_elf_regions, sizeof(*process->elf_regions));
+ if (!process->elf_regions) {
+ LOG_ERROR("Failed to allocate memory for elf region information");
+ goto error;
+ }
+ process->entry_point = sel4utils_elf_reserve(&process->vspace, config.image_name, process->elf_regions);
+ }
+
+ if (process->entry_point == NULL) {
+ LOG_ERROR("Failed to load elf file\n");
+ goto error;
+ }
+ } else {
+ process->entry_point = config.entry_point;
+ }
+
+ /* create the thread, do this *after* elf-loading so that we don't clobber
+ * the required virtual memory*/
+ error = sel4utils_configure_thread(vka, &process->vspace, SEL4UTILS_ENDPOINT_SLOT,
+ config.priority, process->cspace.cptr, cspace_root_data, &process->thread);
+
+ if (error) {
+ LOG_ERROR("ERROR: failed to configure thread for new process %d\n", error);
+ goto error;
+ }
+
+ return 0;
+
+error:
+ /* try to clean up */
+ if (config.create_fault_endpoint && process->fault_endpoint.cptr != 0) {
+ vka_free_object(vka, &process->fault_endpoint);
+ }
+
+ if (config.create_cspace && process->cspace.cptr != 0) {
+ vka_free_object(vka, &process->cspace);
+ }
+
+ if (config.create_vspace && process->pd.cptr != 0) {
+ vka_free_object(vka, &process->pd);
+ if (process->vspace.page_directory != 0) {
+ LOG_ERROR("Could not clean up vspace\n");
+ }
+ }
+
+ if (process->elf_regions) {
+ free(process->elf_regions);
+ }
+
+ if (data != NULL) {
+ free(data);
+ }
+
+ return -1;
+}
+
+void
+sel4utils_destroy_process(sel4utils_process_t *process, vka_t *vka)
+{
+ /* delete all of the caps in the cspace */
+ for (int i = 1; i < process->cspace_next_free; i++) {
+ cspacepath_t path;
+ path.root = process->cspace.cptr;
+ path.capPtr = i;
+ path.capDepth = process->cspace_size;
+ vka_cnode_delete(&path);
+ }
+
+ /* destroy the thread */
+ sel4utils_clean_up_thread(vka, &process->vspace, &process->thread);
+
+ /* destroy the cnode */
+ vka_free_object(vka, &process->cspace);
+
+ /* free any objects created by the vspace */
+ clear_objects(process, vka);
+
+ /* destroy the endpoint */
+ if (process->fault_endpoint.cptr != 0) {
+ vka_free_object(vka, &process->fault_endpoint);
+ }
+
+ /* destroy the page directory */
+ vka_free_object(vka, &process->pd);
+}
+
+#endif /*(defined CONFIG_LIB_SEL4_VKA && defined CONFIG_LIB_SEL4_VSPACE)*/
diff --git a/src/profile.c b/src/profile.c
new file mode 100644
index 0000000..fb2dac8
--- /dev/null
+++ b/src/profile.c
@@ -0,0 +1,46 @@
+/*
+ * 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 <sel4utils/profile.h>
+#include <stdio.h>
+
+/*
+ * __start_SECTION_NAME and __stop_SECTION_NAME are magic symbols inserted by the gcc
+ * linker
+ */
+extern profile_var_t __start__profile_var[];
+extern profile_var_t __stop__profile_var[];
+
+void profile_print32(uint32_t value, const char *varname, const char *description, void *cookie)
+{
+ printf("%s: %u %s\n", varname, value, description);
+}
+void profile_print64(uint64_t value, const char *varname, const char *description, void *cookie)
+{
+ printf("%s: %llu %s\n", varname, value, description);
+}
+
+void profile_scrape(profile_callback32 callback32, profile_callback64 callback64, void *cookie)
+{
+ profile_var_t *i;
+ for (i = __start__profile_var; i < __stop__profile_var; i++) {
+ switch (i->type) {
+ case PROFILE_VAR_TYPE_INT32:
+ callback32(*(uint32_t*)i->var, i->varname, i->description, cookie);
+ break;
+ case PROFILE_VAR_TYPE_INT64:
+ callback64(*(uint64_t*)i->var, i->varname, i->description, cookie);
+ break;
+ default:
+ LOG_ERROR("Unknown profile var. Probable memory corruption or linker failure!");
+ break;
+ }
+ }
+}
diff --git a/src/sel4_debug.c b/src/sel4_debug.c
new file mode 100644
index 0000000..da8ac35
--- /dev/null
+++ b/src/sel4_debug.c
@@ -0,0 +1,41 @@
+/*
+ * 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)
+ */
+
+/*
+ Authors: Kevin Elphinstone
+*/
+
+#include <stdio.h> /* For fprintf() */
+#include <stdlib.h> /* For abort() */
+#include <sel4utils/sel4_debug.h>
+
+char *sel4_errlist[] = {
+ "seL4_NoError",
+ "seL4_InvalidArgument",
+ "seL4_InvalidCapability",
+ "seL4_IllegalOperation",
+ "seL4_RangeError",
+ "seL4_AlignmentError",
+ "seL4_FailedLookup",
+ "seL4_TruncatedMessage",
+ "seL4_DeleteFirst",
+ "seL4_RevokeFirst",
+ "seL4_NotEnoughMemory"
+};
+
+void
+__sel4_error(int sel4_error, const char *file,
+ const char *function, int line, char * str)
+{
+ fprintf(stderr, "seL4 Error: %s, function %s, file %s, line %d: %s\n",
+ sel4_errlist[sel4_error],
+ function, file, line, str);
+ abort();
+}
diff --git a/src/stack.c b/src/stack.c
new file mode 100644
index 0000000..7fca7a7
--- /dev/null
+++ b/src/stack.c
@@ -0,0 +1,27 @@
+/*
+ * 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 <errno.h>
+#include <vspace/vspace.h>
+#include <sel4utils/stack.h>
+#include <sel4utils/util.h>
+#include <utils/stack.h>
+
+int
+sel4utils_run_on_stack(vspace_t *vspace, int (*func)(void))
+{
+ void *stack_top = vspace_new_stack(vspace);
+ if (stack_top == NULL) {
+ LOG_ERROR("Failed to allocate new stack\n");
+ return -1;
+ }
+
+ return utils_run_on_stack(stack_top, func);
+}
diff --git a/src/thread.c b/src/thread.c
new file mode 100644
index 0000000..c0f998f
--- /dev/null
+++ b/src/thread.c
@@ -0,0 +1,223 @@
+/*
+ * 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>
+
+#ifdef CONFIG_LIB_SEL4_VSPACE
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include <sel4/sel4.h>
+#include <vka/vka.h>
+#include <vka/object.h>
+#include <vspace/vspace.h>
+#include <sel4utils/thread.h>
+#include <sel4utils/util.h>
+#include <sel4utils/arch/util.h>
+
+#include "helpers.h"
+
+int
+sel4utils_configure_thread(vka_t *vka, vspace_t *alloc, seL4_CPtr fault_endpoint,
+ uint8_t priority, seL4_CNode cspace, seL4_CapData_t cspace_root_data,
+ sel4utils_thread_t *res)
+{
+ memset(res, 0, sizeof(sel4utils_thread_t));
+
+ int error = vka_alloc_tcb(vka, &res->tcb);
+ if (error == -1) {
+ LOG_ERROR("vka_alloc tcb failed");
+ sel4utils_clean_up_thread(vka, alloc, res);
+ return -1;
+ }
+
+ res->ipc_buffer_addr = (seL4_Word) vspace_new_ipc_buffer(alloc, &res->ipc_buffer);
+
+ if (res->ipc_buffer_addr == 0) {
+ LOG_ERROR("ipc buffer allocation failed");
+ return -1;
+ }
+
+ seL4_CapData_t null_cap_data = {{0}};
+ error = seL4_TCB_Configure(res->tcb.cptr, fault_endpoint, priority, cspace, cspace_root_data,
+ vspace_get_root(alloc), null_cap_data,
+ res->ipc_buffer_addr, res->ipc_buffer);
+
+ if (error != seL4_NoError) {
+ LOG_ERROR("TCB configure failed with seL4 error code %d", error);
+ sel4utils_clean_up_thread(vka, alloc, res);
+ return -1;
+ }
+
+ res->stack_top = vspace_new_stack(alloc);
+
+ if (res->stack_top == NULL) {
+ LOG_ERROR("Stack allocation failed!");
+ sel4utils_clean_up_thread(vka, alloc, res);
+ return -1;
+ }
+
+ return 0;
+}
+
+int
+sel4utils_internal_start_thread(sel4utils_thread_t *thread, void *entry_point, void *arg0,
+ void *arg1, int resume, void *stack_top)
+{
+ seL4_UserContext context = {0};
+ size_t context_size = sizeof(seL4_UserContext) / sizeof(seL4_Word);
+ int error;
+
+#ifdef ARCH_IA32
+
+#ifdef CONFIG_X86_64
+ context.rdi = (seL4_Word)arg0;
+ context.rsi = (seL4_Word)arg1;
+ context.rdx = (seL4_Word)thread->ipc_buffer_addr;
+ context.rsp = (seL4_Word) thread->stack_top;
+ context.gs = IPCBUF_GDT_SELECTOR;
+ context.rip = (seL4_Word)entry_point;
+#else
+ seL4_Word *stack_ptr = (seL4_Word *) stack_top;
+ stack_ptr[-5] = (seL4_Word) arg0;
+ stack_ptr[-4] = (seL4_Word) arg1;
+ stack_ptr[-3] = (seL4_Word) thread->ipc_buffer_addr;
+ context.esp = (seL4_Word) (thread->stack_top - 24);
+ context.gs = IPCBUF_GDT_SELECTOR;
+ context.eip = (seL4_Word)entry_point;
+#endif
+
+ /* check that stack is aligned correctly */
+ assert((seL4_Word) thread->stack_top % (sizeof(seL4_Word) * 2) == 0);
+ error = seL4_TCB_WriteRegisters(thread->tcb.cptr, resume, 0, context_size, &context);
+#elif ARCH_ARM /* ARCH_IA32 */
+ context.pc = (seL4_Word) entry_point;
+ context.sp = (seL4_Word) thread->stack_top;
+ context.r0 = (seL4_Word) arg0;
+ context.r1 = (seL4_Word) arg1;
+ context.r2 = (seL4_Word) thread->ipc_buffer_addr;
+
+ /* check that stack is aligned correctly */
+ assert((uint32_t) thread->stack_top % (sizeof(seL4_Word) * 2) == 0);
+ error = seL4_TCB_WriteRegisters(thread->tcb.cptr, resume, 0, context_size, &context);
+#endif /* ARCH_ARM */
+
+ if (error) {
+ LOG_ERROR("seL4_TCB_WriteRegisters failed with error %d", error);
+ return -1;
+ }
+
+ return 0;
+}
+
+
+int
+sel4utils_start_thread(sel4utils_thread_t *thread, void *entry_point, void *arg0, void *arg1,
+ int resume)
+{
+ return sel4utils_internal_start_thread(thread, entry_point, arg0, arg1, resume, thread->stack_top);
+}
+
+void
+sel4utils_clean_up_thread(vka_t *vka, vspace_t *alloc, sel4utils_thread_t *thread)
+{
+ if (thread->tcb.cptr != 0) {
+ vka_free_object(vka, &thread->tcb);
+ }
+
+ if (thread->ipc_buffer_addr != 0) {
+ vspace_free_ipc_buffer(alloc, (seL4_Word *) thread->ipc_buffer_addr);
+ }
+
+ if (thread->stack_top != 0) {
+ vspace_free_stack(alloc, thread->stack_top);
+ }
+
+ memset(thread, 0, sizeof(sel4utils_thread_t));
+}
+
+void
+sel4utils_print_fault_message(seL4_MessageInfo_t tag, char *thread_name)
+{
+ switch (seL4_MessageInfo_get_label(tag)) {
+ case SEL4_PFIPC_LABEL:
+ assert(seL4_MessageInfo_get_length(tag) == SEL4_PFIPC_LENGTH);
+ printf("%sPagefault from [%s]: %s %s at PC: 0x"XFMT" vaddr: 0x"XFMT"%s\n",
+ COLOR_ERROR,
+ thread_name,
+ sel4utils_is_read_fault() ? "read" : "write",
+ seL4_GetMR(SEL4_PFIPC_PREFETCH_FAULT) ? "prefetch fault" : "fault",
+ seL4_GetMR(SEL4_PFIPC_FAULT_IP),
+ seL4_GetMR(SEL4_PFIPC_FAULT_ADDR),
+ COLOR_NORMAL);
+ break;
+
+ case SEL4_EXCEPT_IPC_LABEL:
+ assert(seL4_MessageInfo_get_length(tag) == SEL4_EXCEPT_IPC_LENGTH);
+ printf("%sBad syscall from [%s]: scno "DFMT" at PC: 0x"XFMT"%s\n",
+ COLOR_ERROR,
+ thread_name,
+ seL4_GetMR(EXCEPT_IPC_SYS_MR_SYSCALL),
+ seL4_GetMR(EXCEPT_IPC_SYS_MR_IP),
+ COLOR_NORMAL
+ );
+
+ break;
+
+ case SEL4_USER_EXCEPTION_LABEL:
+ assert(seL4_MessageInfo_get_length(tag) == SEL4_USER_EXCEPTION_LENGTH);
+ printf("%sInvalid instruction from [%s] at PC: 0x"XFMT"%s\n",
+ COLOR_ERROR,
+ thread_name,
+ seL4_GetMR(0),
+ COLOR_NORMAL);
+ break;
+
+ default:
+ /* What? Why are we here? What just happened? */
+ printf("Unknown fault from [%s]: "DFMT" (length = "DFMT")\n", thread_name, seL4_MessageInfo_get_label(tag), seL4_MessageInfo_get_length(tag));
+ break;
+ }
+}
+
+
+static int
+fault_handler(char *name, seL4_CPtr endpoint) {
+ seL4_Word badge;
+ seL4_MessageInfo_t info = seL4_Wait(endpoint, &badge);
+
+ sel4utils_print_fault_message(info, name);
+
+ /* go back to sleep so other things can run */
+ seL4_Wait(endpoint, &badge);
+
+ return 0;
+}
+
+int
+sel4utils_start_fault_handler(seL4_CPtr fault_endpoint, vka_t *vka, vspace_t *vspace,
+ uint8_t prio, seL4_CPtr cspace, seL4_CapData_t cap_data, char *name,
+ sel4utils_thread_t *res)
+{
+ int error = sel4utils_configure_thread(vka, vspace, 0, prio, cspace,
+ cap_data, res);
+
+ if (error) {
+ LOG_ERROR("Failed to configure fault handling thread\n");
+ return -1;
+ }
+
+ return sel4utils_start_thread(res, fault_handler, (void *) name,
+ (void *) fault_endpoint, 1);
+}
+
+#endif /* CONFIG_LIB_SEL4_VSPACE */
diff --git a/src/vspace/bootstrap.c b/src/vspace/bootstrap.c
new file mode 100644
index 0000000..243b82b
--- /dev/null
+++ b/src/vspace/bootstrap.c
@@ -0,0 +1,451 @@
+/*
+ * 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
+ * 0xdfc00000 ↓
+ * 0xdfbfffff ↑
+ * | top level page table
+ * 0xdfbff000 ↓
+ * 0xdfbfefff ↑
+ * | 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)
+/* reserve the first page to catch null pointer dereferences */
+#define FIRST_VADDR (0 + PAGE_SIZE_4K)
+
+/* sanity checks - check our constants above are what we say they are */
+#ifndef CONFIG_X86_64
+compile_time_assert(sel4utils_vspace_1, TOP_LEVEL_INDEX(TOP_LEVEL_PAGE_TABLE_VADDR) == 894);
+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) == 895);
+compile_time_assert(sel4utils_vspace_4, BOTTOM_LEVEL_INDEX(FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR) == 0);
+#endif
+
+/* check our data structures are 4K page sized like the rest of the code assumes they are */
+compile_time_assert(bottom_level_4k, sizeof(bottom_level_t) == PAGE_SIZE_4K);
+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 = (void *) 0x10000000;
+
+ vspace->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 useable */
+ vspace->new_stack = sel4utils_new_stack;
+ vspace->free_stack = sel4utils_free_stack;
+
+ vspace->new_ipc_buffer = sel4utils_new_ipc_buffer;
+ vspace->free_ipc_buffer = sel4utils_free_ipc_buffer;
+
+ vspace->new_pages = sel4utils_new_pages;
+ vspace->new_pages_at_vaddr = sel4utils_new_pages_at_vaddr;
+ vspace->free_pages = sel4utils_free_pages;
+
+ vspace->map_pages = sel4utils_map_pages;
+ vspace->map_pages_at_vaddr = sel4utils_map_pages_at_vaddr;
+ vspace->unmap_pages = sel4utils_unmap_pages;
+ vspace->unmap_reserved_pages = sel4utils_unmap_reserved_pages;
+
+ vspace->reserve_range = sel4utils_reserve_range;
+ vspace->reserve_range_at = sel4utils_reserve_range_at;
+ vspace->free_reservation = sel4utils_free_reservation;
+
+ vspace->get_cap = sel4utils_get_cap;
+}
+
+static int
+reserve_range(vspace_t *vspace, void *start, void *end)
+{
+ int pages = BYTES_TO_4K_PAGES(ROUND_UP((uint32_t) ((seL4_Word)end), PAGE_SIZE_4K) -
+ ROUND_DOWN((uint32_t) ((seL4_Word)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 %p and %p", 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(seL4_Word *va_start, seL4_Word *va_end) {
+ extern char __executable_start[];
+ extern char _end[];
+
+ *va_start = (seL4_Word) __executable_start;
+ *va_end = (seL4_Word) _end;
+ *va_end = (seL4_Word) (seL4_Word)ROUND_UP((uint32_t) ((seL4_Word)va_end), (uint32_t) PAGE_SIZE_4K);
+}
+
+
+static int
+reserve_initial_task_regions(vspace_t *vspace, void *existing_frames[])
+{
+
+ /* mark the code and data segments as used */
+ seL4_Word 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, (void *) va_start, (void *) 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, existing_frames[i], 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 pagetable = {0};
+
+ error = sel4utils_map_page(data->vka, vspace->page_directory, frame->cptr, vaddr,
+ seL4_AllRights, 1, &pagetable);
+
+ if (error) {
+ LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error);
+ return error;
+ }
+
+ /* Zero the memory */
+ memset(vaddr, 0, PAGE_SIZE_4K);
+
+ if (pagetable.cptr != 0) {
+ vspace_maybe_call_allocated_object(vspace, pagetable);
+ }
+
+ return seL4_NoError;
+}
+
+int
+bootstrap_create_level(vspace_t *vspace, void *vaddr)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ vka_object_t bottom_level = {0};
+ if (alloc_and_map_bootstrap_frame(vspace, &bottom_level,
+ data->next_bottom_level_vaddr) != seL4_NoError) {
+ return -1;
+ }
+
+ int error __attribute__((unused)) = update(vspace, data->next_bottom_level_vaddr, bottom_level.cptr);
+ /* this cannot fail */
+ assert(error == seL4_NoError);
+
+ data->top_level[TOP_LEVEL_INDEX(vaddr)] = (bottom_level_t *) data->next_bottom_level_vaddr;
+
+ data->next_bottom_level_vaddr += PAGE_SIZE_4K;
+
+ 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;
+ }
+
+ /* The top level page table vaddr is the last entry in the second last bottom level
+ * page table - create that level and map it in*/
+ vka_object_t first_bottom_level = {0};
+ if (alloc_and_map_bootstrap_frame(vspace, &first_bottom_level,
+ (void *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR)) {
+ return -1;
+ }
+
+ /* The level we just created is the first entry in the last bottom level page table -
+ * create that level and map it in */
+ vka_object_t second_bottom_level = {0};
+ if (alloc_and_map_bootstrap_frame(vspace, &second_bottom_level,
+ (void *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR + PAGE_SIZE_4K)) {
+ return -1;
+ }
+
+ /* set up the pointers to our new page tables */
+ data->top_level = (bottom_level_t **) TOP_LEVEL_PAGE_TABLE_VADDR;
+ data->top_level[TOP_LEVEL_INDEX(TOP_LEVEL_PAGE_TABLE_VADDR)] =
+ (bottom_level_t *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR;
+ data->top_level[TOP_LEVEL_INDEX(FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR)] =
+ (bottom_level_t *) (FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR + 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. */
+ int error = update(vspace, (void *) TOP_LEVEL_PAGE_TABLE_VADDR, top_level.cptr);
+ (void)error;
+ assert(error == seL4_NoError);
+ error = update(vspace, (void *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR, first_bottom_level.cptr);
+ assert(error == seL4_NoError);
+ error = update(vspace, (void *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR + PAGE_SIZE_4K,
+ second_bottom_level.cptr);
+ assert(error == seL4_NoError);
+
+ /* Finally reserve the rest of the entries for the rest of the bottom level page tables */
+ void *vaddr = (void *) FIRST_BOTTOM_LEVEL_PAGE_TABLE_VADDR;
+ data->next_bottom_level_vaddr = vaddr + (2 * PAGE_SIZE_4K);
+ for (int i = 2; i < VSPACE_LEVEL_SIZE; i++) {
+ error = reserve(vspace, vaddr + (i * PAGE_SIZE_4K));
+ assert(error == seL4_NoError);
+ }
+
+ 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)
+{
+ 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 (void *page = image->start; page < image->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 */
+ int error = vspace_new_pages_at_vaddr(clone, page, 1, seL4_PageBits, image);
+ if (error) {
+ /* vspace will be left inconsistent */
+ LOG_ERROR("Error %d while trying to map page at %p\n", error, page);
+ }
+
+ seL4_CPtr cap = vspace_get_cap(clone, 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, 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, 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);
+ 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 */
diff --git a/src/vspace/client_server_vspace.c b/src/vspace/client_server_vspace.c
new file mode 100644
index 0000000..689acc8
--- /dev/null
+++ b/src/vspace/client_server_vspace.c
@@ -0,0 +1,393 @@
+/*
+ * 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_VKA && defined CONFIG_LIB_SEL4_VSPACE
+
+#include <sel4utils/client_server_vspace.h>
+#include <vka/capops.h>
+#include <sel4utils/mapping.h>
+#include <sel4utils/util.h>
+#include <stdlib.h>
+#include <sel4utils/vspace.h>
+#include <sel4utils/vspace_internal.h>
+
+#define OFFSET(x) ( ((uint32_t)((seL4_Word)(x))) & MASK(BOTTOM_LEVEL_BITS_OFFSET) )
+#define ADDR(start, page) ( (start) + (page) * PAGE_SIZE_4K )
+
+typedef struct client_server_vspace {
+ /* vspace of the server. we also use this to request memory for metadata */
+ vspace_t *server;
+ /* vspace of the client we are proxying calls for */
+ vspace_t *client;
+ vka_t *vka;
+ /* a fake sel4utils vspace that acts as a translation layer */
+ vspace_t translation;
+ sel4utils_alloc_data_t translation_data;
+} client_server_vspace_t;
+
+static void unmap(client_server_vspace_t *cs_vspace, void *caddr, size_t size_bits)
+{
+ /* determine the virtual address of the start */
+ void *saddr = (void*)get_entry(cs_vspace->translation_data.top_level, caddr);
+ assert(saddr);
+ /* get the cap from the server vspace */
+ seL4_CPtr cap = vspace_get_cap(cs_vspace->server, saddr);
+ assert(cap);
+ /* unmap */
+ vspace_unmap_pages(cs_vspace->server, saddr, 1, size_bits);
+ /* delete and free the cap */
+ cspacepath_t cap_path;
+ vka_cspace_make_path(cs_vspace->vka, cap, &cap_path);
+ vka_cnode_delete(&cap_path);
+ vka_cspace_free(cs_vspace->vka, cap);
+ /* remove our translation */
+ clear_entries(&cs_vspace->translation, caddr, size_bits);
+}
+
+static void unmap_many(client_server_vspace_t *cs_vspace, void *caddr, size_t num_pages, size_t size_bits)
+{
+ int i;
+ for (i = 0; i < num_pages; i++) {
+ unmap(cs_vspace, caddr + BIT(size_bits) * i, size_bits);
+ }
+}
+
+static int dup_and_map(client_server_vspace_t *cs_vspace, seL4_CPtr cap, void *caddr, size_t size_bits)
+{
+ /* duplicate the cap */
+ seL4_CPtr server_cap;
+ cspacepath_t cap_path, server_cap_path;
+ int error = vka_cspace_alloc(cs_vspace->vka, &server_cap);
+ if (error) {
+ LOG_ERROR("Failed to allocate cslot");
+ return error;
+ }
+ vka_cspace_make_path(cs_vspace->vka, cap, &cap_path);
+ vka_cspace_make_path(cs_vspace->vka, server_cap, &server_cap_path);
+ error = vka_cnode_copy(&server_cap_path, &cap_path, seL4_AllRights);
+ if (error != seL4_NoError) {
+ LOG_ERROR("Error copying frame cap");
+ vka_cspace_free(cs_vspace->vka, server_cap);
+ return -1;
+ }
+ /* map it into the server */
+ void *saddr = vspace_map_pages(cs_vspace->server, &server_cap_path.capPtr, seL4_AllRights, 1, size_bits, 1);
+ if (!saddr) {
+ LOG_ERROR("Error mapping frame into server vspace");
+ vka_cnode_delete(&server_cap_path);
+ vka_cspace_free(cs_vspace->vka, server_cap);
+ return -1;
+ }
+ /* update our translation */
+ int i;
+ uint32_t pages = BYTES_TO_4K_PAGES(BIT(size_bits));
+ for (i = 0; i < pages; i++) {
+ if (update_entry(&cs_vspace->translation, ADDR(caddr, i), (seL4_CPtr)ADDR(saddr, i))) {
+ /* remove the entries we already put in. we can't call
+ * clear_entries because the portion to remove is not
+ * a power of two size */
+ for (i--; i >= 0; i--) {
+ clear(&cs_vspace->translation, ADDR(caddr, i));
+ }
+ vka_cnode_delete(&server_cap_path);
+ vka_cspace_free(cs_vspace->vka, server_cap);
+ return -1;
+ }
+ }
+ return 0;
+}
+
+static int dup_and_map_many(client_server_vspace_t *cs_vspace, seL4_CPtr *caps, void *caddr, size_t num_pages, size_t size_bits)
+{
+ int i;
+ for (i = 0; i < num_pages; i++) {
+ int error = dup_and_map(cs_vspace, caps[i], caddr + BIT(size_bits) * i, size_bits);
+ if (error) {
+ unmap_many(cs_vspace, caddr, i - 1, size_bits);
+ return error;
+ }
+ }
+ return 0;
+}
+
+static int find_dup_and_map_many(client_server_vspace_t *cs_vspace, void *caddr, size_t num_pages, size_t size_bits)
+{
+ int i;
+ seL4_CPtr caps[num_pages];
+ for (i = 0; i < num_pages; i++) {
+ caps[i] = vspace_get_cap(cs_vspace->client, caddr + BIT(size_bits) * i);
+ assert(caps[i]);
+ }
+ return dup_and_map_many(cs_vspace, caps, caddr, num_pages, size_bits);
+}
+
+static void *cs_new_stack(vspace_t *vspace)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* we do not know how much stack will get mapped. so just proxy the call
+ * and hope we do not want to inspect their stack */
+ return vspace_new_stack(cs_vspace->client);
+}
+
+static void cs_free_stack(vspace_t *vspace, void *stack_top)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ vspace_free_stack(cs_vspace->client, stack_top);
+}
+
+static void *cs_new_ipc_buffer(vspace_t *vspace, seL4_CPtr *page)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* it makes no sense to want to inspect their IPC buffer. so this call can
+ * just be proxied */
+ return vspace_new_ipc_buffer(cs_vspace->client, page);
+}
+
+static void cs_free_ipc_buffer(vspace_t *vspace, void *vaddr)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ vspace_free_ipc_buffer(cs_vspace->client, vaddr);
+}
+
+static reservation_t *cs_reserve_range(vspace_t *vspace, size_t size, seL4_CapRights rights,
+ int cacheable, void **result)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ assert(cacheable);
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* we are not interested in client reservations, just proxy */
+ return vspace_reserve_range(cs_vspace->client, size, rights, cacheable, result);
+}
+
+static reservation_t *cs_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size, seL4_CapRights
+ rights, int cacheable)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ assert(cacheable);
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* we are not interested in client reservations, just proxy */
+ return vspace_reserve_range_at(cs_vspace->client, vaddr, size, rights, cacheable);
+}
+
+static void cs_free_reservation(vspace_t *vspace, reservation_t *reservation)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ vspace_free_reservation(cs_vspace->client, reservation);
+}
+
+static int cs_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], void *vaddr,
+ size_t num_pages, size_t size_bits, reservation_t *reservation)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ assert(size_bits >= 12);
+ /* first map all the pages into the client */
+ int result = vspace_map_pages_at_vaddr(cs_vspace->client, caps, vaddr, num_pages, size_bits, reservation);
+ if (result) {
+ LOG_ERROR("Error mapping pages into client vspace");
+ /* some error, propogate up */
+ return result;
+ }
+ /* now map them all into the server */
+ result = dup_and_map_many(cs_vspace, caps, vaddr, num_pages, size_bits);
+ if (result) {
+ /* unmap */
+ LOG_ERROR("Error mapping pages into server vspace");
+ vspace_unmap_pages(cs_vspace->client, vaddr, num_pages, size_bits);
+ return result;
+ }
+ return 0;
+}
+
+static seL4_CPtr cs_get_cap(vspace_t *vspace, void *vaddr)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* return the client cap */
+ return vspace_get_cap(cs_vspace->client, vaddr);
+}
+
+static void *cs_map_pages(vspace_t *vspace, seL4_CPtr caps[], seL4_CapRights rights,
+ size_t num_pages, size_t size_bits, int cacheable)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ assert(size_bits >= 12);
+ assert(cacheable);
+ /* first map all the pages into the client */
+ void *result = vspace_map_pages(cs_vspace->client, caps, rights, num_pages, size_bits, cacheable);
+ if (!result) {
+ LOG_ERROR("Error mapping pages into client vspace");
+ return result;
+ }
+ /* now map them all into the server */
+ int error = dup_and_map_many(cs_vspace, caps, result, num_pages, size_bits);
+ if (error) {
+ /* unmap */
+ LOG_ERROR("Error mapping pages into server vspace");
+ vspace_unmap_pages(cs_vspace->client, result, num_pages, size_bits);
+ return NULL;
+ }
+ return result;
+}
+
+static void cs_unmap_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* remove our mappings */
+ unmap_many(cs_vspace, vaddr, num_pages, size_bits);
+ /* unmap from the client */
+ vspace_unmap_pages(cs_vspace->client, vaddr, num_pages, size_bits);
+}
+
+static int cs_new_pages_at_vaddr(vspace_t *vspace, void *vaddr, size_t num_pages,
+ size_t size_bits, reservation_t *reservation)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ assert(size_bits >= 12);
+ /* create new pages in the client first */
+ int result = vspace_new_pages_at_vaddr(cs_vspace->client, vaddr, num_pages, size_bits, reservation);
+ if (result) {
+ LOG_ERROR("Error creating pages in client vspace");
+ return result;
+ }
+ result = find_dup_and_map_many(cs_vspace, vaddr, num_pages, size_bits);
+ if (result) {
+ LOG_ERROR("Error mapping new page in server vspace");
+ assert(!"Cannot delete pages we created in client vspace");
+ return -1;
+ }
+ return 0;
+}
+
+static void *cs_new_pages(vspace_t *vspace, seL4_CapRights rights, size_t num_pages,
+ size_t size_bits)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ assert(size_bits >= 12);
+ void *vaddr = vspace_new_pages(cs_vspace->client, rights, num_pages, size_bits);
+ if (!vaddr) {
+ LOG_ERROR("Error creating new pages in client vspace");
+ return NULL;
+ }
+ int result = find_dup_and_map_many(cs_vspace, vaddr, num_pages, size_bits);
+ if (result) {
+ LOG_ERROR("Error mapping new page in server vspace");
+ assert(!"Cannot delete pages we created in client vspace");
+ return NULL;
+ }
+ return vaddr;
+}
+
+static void cs_free_pages(vspace_t *vspace, void *vaddr, size_t num_pages,
+ size_t size_bits)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+ cs_vspace->client->page_directory = vspace->page_directory;
+ /* remove our mappings */
+ unmap_many(cs_vspace, vaddr, num_pages, size_bits);
+ /* free in client */
+ vspace_free_pages(cs_vspace->client, vaddr, num_pages, size_bits);
+}
+
+int sel4utils_get_cs_vspace(vspace_t *vspace, vka_t *vka, vspace_t *server, vspace_t *client)
+{
+ int error;
+ client_server_vspace_t *cs_vspace = malloc(sizeof(*cs_vspace));
+ cs_vspace->server = server;
+ cs_vspace->client = client;
+ cs_vspace->vka = vka;
+
+ error = sel4utils_get_vspace(server, &cs_vspace->translation, &cs_vspace->translation_data,
+ vka, 0, NULL, NULL);
+ if (error) {
+ LOG_ERROR("Failed to create translation vspace");
+ free(cs_vspace);
+ return error;
+ }
+
+ vspace->data = cs_vspace;
+
+ vspace->new_stack = cs_new_stack;
+ vspace->free_stack = cs_free_stack;
+
+ vspace->new_ipc_buffer = cs_new_ipc_buffer;
+ vspace->free_ipc_buffer = cs_free_ipc_buffer;
+
+ vspace->new_pages = cs_new_pages;
+ vspace->new_pages_at_vaddr = cs_new_pages_at_vaddr;
+ vspace->free_pages = cs_free_pages;
+
+ vspace->map_pages = cs_map_pages;
+ vspace->map_pages_at_vaddr = cs_map_pages_at_vaddr;
+ vspace->unmap_pages = cs_unmap_pages;
+
+ vspace->reserve_range = cs_reserve_range;
+ vspace->reserve_range_at = cs_reserve_range_at;
+ vspace->free_reservation = cs_free_reservation;
+
+ vspace->get_cap = cs_get_cap;
+
+ vspace->allocated_object = NULL;
+ vspace->allocated_object_cookie = NULL;
+
+ /* we always pretend to be the client. due to api limitations
+ * we need to constatly reset the clients page directory to ours
+ * in case ours was modified as a result of process loading */
+ vspace->page_directory = client->page_directory;
+
+ return 0;
+}
+
+void *sel4utils_cs_vspace_translate(vspace_t *vspace, void *addr)
+{
+ client_server_vspace_t *cs_vspace = (client_server_vspace_t*)vspace->data;
+
+ seL4_CPtr translation_result = get_entry(cs_vspace->translation_data.top_level, addr);
+
+ /* the translation will through away any non aligned bits, if we got a successful
+ * translation then add the offset back onto the result */
+ return translation_result == 0 ? NULL : ((void*)translation_result) + OFFSET(addr);
+}
+
+int sel4utils_cs_vspace_for_each(vspace_t *vspace, void *addr, uint32_t len,
+ int (*proc)(void* addr, uint32_t len, void *cookie),
+ void *cookie)
+{
+ uint32_t current_addr;
+ uint32_t next_addr;
+ uint32_t end_addr = (uint32_t)(addr + len);
+ for (current_addr = (uint32_t)addr; current_addr < end_addr; current_addr = next_addr) {
+ uint32_t current_aligned = PAGE_ALIGN_4K(current_addr);
+ uint32_t next_page_start = current_aligned + PAGE_SIZE_4K;
+ next_addr = MIN(end_addr, next_page_start);
+ void *saddr = sel4utils_cs_vspace_translate(vspace, (void*)current_aligned);
+ if (!saddr) {
+ return -1;
+ }
+ int result = proc((void*)(saddr + (current_addr - current_aligned)), next_addr - current_addr, cookie);
+ if (result) {
+ return result;
+ }
+ }
+ return 0;
+}
+
+#endif
diff --git a/src/vspace/vspace.c b/src/vspace/vspace.c
new file mode 100644
index 0000000..c8b8a16
--- /dev/null
+++ b/src/vspace/vspace.c
@@ -0,0 +1,566 @@
+/*
+ * 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)
+ */
+
+/* see sel4utils/vspace.h for details */
+#include <autoconf.h>
+
+#if defined CONFIG_LIB_SEL4_VKA && defined CONFIG_LIB_SEL4_VSPACE
+
+#include <stdlib.h>
+#include <string.h>
+
+#include <sel4utils/vspace.h>
+
+#include <sel4utils/vspace_internal.h>
+
+#include <utils/util.h>
+
+/* see comment in vspace_internal for why these checks exist */
+compile_time_assert(pages_are_4k1, BOTTOM_LEVEL_BITS_OFFSET == seL4_PageBits);
+compile_time_assert(pages_are_4k2, BIT(BOTTOM_LEVEL_BITS_OFFSET) == PAGE_SIZE_4K);
+
+static int
+create_level(vspace_t *vspace, void* vaddr)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ /* We need a level in the bootstrapper vspace */
+ if (data->bootstrap == NULL) {
+ return bootstrap_create_level(vspace, vaddr);
+ }
+
+ /* Otherwise we allocate our level out of the bootstrapper vspace -
+ * which is where bookkeeping is mapped */
+ bottom_level_t *bottom_level = vspace_new_pages(data->bootstrap, seL4_AllRights, 1, seL4_PageBits);
+ if (bottom_level == NULL) {
+ return -1;
+ }
+ memset(bottom_level, 0, BIT(seL4_PageBits));
+
+ data->top_level[TOP_LEVEL_INDEX(vaddr)] = bottom_level;
+
+ return 0;
+}
+
+int
+assure_level(vspace_t *vspace, void *vaddr)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ assert(data->top_level != NULL);
+ assert(data->top_level != (void *) RESERVED);
+
+ if (data->top_level[TOP_LEVEL_INDEX(vaddr)] == NULL) {
+ int error = create_level(vspace, vaddr);
+ if (error) {
+ return -1;
+ }
+ }
+
+ return 0;
+}
+
+static int
+check_empty_range(bottom_level_t *top_level[], void *vaddr, size_t num_pages, size_t size_bits)
+{
+ int result = 1;
+ int num_4k_pages = BYTES_TO_4K_PAGES(num_pages * (1 << size_bits));
+ for (int i = 0; i < num_4k_pages && result; i++) {
+ /* a range is empty if it does not have a mapped cap and it isn't reserved */
+ result = is_available(top_level, vaddr + (i * PAGE_SIZE_4K))
+ && !is_reserved(top_level, vaddr + (i * PAGE_SIZE_4K));
+ }
+
+ return result;
+}
+
+/* check a range of pages is all reserved */
+static int
+check_reserved_range(bottom_level_t *top_level[], void *vaddr, size_t num_pages, size_t size_bits)
+{
+ int result = 1;
+ int num_4k_pages = BYTES_TO_4K_PAGES(num_pages * (1 << size_bits));
+ for (int i = 0; i < num_4k_pages && result; i++) {
+ /* a range is empty if it does not have a mapped cap and it isn't reserved */
+ result = is_reserved(top_level, vaddr + (i * PAGE_SIZE_4K));
+
+ }
+
+ return result;
+}
+
+/* check that vaddr is actually in the reservation */
+static int
+check_reservation_bounds(reservation_t *reservation, void *vaddr, size_t num_pages, size_t size_bits)
+{
+ return (vaddr >= reservation->start) &&
+ (vaddr + (num_pages * (1 << size_bits))) <= reservation->end;
+}
+
+static int
+check_reservation(bottom_level_t *top_level[], reservation_t *reservation, void *vaddr,
+ size_t num_pages, size_t size_bits)
+{
+ return check_reservation_bounds(reservation, vaddr, num_pages, size_bits) &
+ check_reserved_range(top_level, vaddr, num_pages, size_bits);
+}
+
+static void
+perform_reservation(vspace_t *vspace, reservation_t *reservation, void *vaddr, size_t bytes,
+ seL4_CapRights rights, int cacheable)
+{
+ reservation->start = (void *) (seL4_Word)ROUND_DOWN((uint32_t) ((seL4_Word)vaddr), PAGE_SIZE_4K);
+ reservation->end = (void *) (seL4_Word)ROUND_UP((uint32_t) ((seL4_Word)vaddr) + bytes, PAGE_SIZE_4K);
+
+ reservation->rights = rights;
+ reservation->cacheable = cacheable;
+
+ int error = seL4_NoError;
+ void *v = reservation->start;
+
+ for (v = reservation->start; v < reservation->end &&
+ error == seL4_NoError; v += PAGE_SIZE_4K) {
+ error = reserve(vspace, v);
+ }
+
+ /* return the amount we sucessfully reserved */
+ reservation->end = v;
+}
+
+int
+sel4utils_map_page_pd(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights,
+ int cacheable, size_t size_bits)
+{
+ vka_object_t pagetable = {0};
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ int error = sel4utils_map_page(data->vka, vspace->page_directory, cap, vaddr,
+ rights, cacheable, &pagetable);
+ if (error) {
+ /* everything has gone to hell. Do no clean up. */
+ LOG_ERROR("Error mapping pages, bailing: %d", error);
+ return -1;
+ }
+
+ if (pagetable.cptr != 0) {
+ vspace_maybe_call_allocated_object(vspace, pagetable);
+ }
+ pagetable.cptr = 0;
+
+ return seL4_NoError;
+}
+
+#ifdef CONFIG_VTX
+int
+sel4utils_map_page_ept(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights,
+ int cacheable, size_t size_bits)
+{
+ struct sel4utils_alloc_data *data = get_alloc_data(vspace);
+ vka_object_t pagetable = {0};
+ vka_object_t pagedir = {0};
+
+ int error = sel4utils_map_ept_page(data->vka, vspace->page_directory, cap,
+ (seL4_Word) vaddr, rights, cacheable, size_bits, &pagetable, &pagedir);
+ if (error) {
+ LOG_ERROR("Error mapping pages, bailing\n");
+ return -1;
+ }
+
+ if (pagetable.cptr != 0) {
+ vspace_maybe_call_allocated_object(vspace, pagetable);
+ pagetable.cptr = 0;
+ }
+
+ if (pagedir.cptr != 0) {
+ vspace_maybe_call_allocated_object(vspace, pagedir);
+ pagedir.cptr = 0;
+ }
+
+ return seL4_NoError;
+}
+#endif /* CONFIG_VTX */
+
+static int
+map_page(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights rights,
+ int cacheable, size_t size_bits)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ return data->map_page(vspace, cap, vaddr, rights, cacheable, size_bits);
+}
+
+static void *
+find_range(sel4utils_alloc_data_t *data, size_t num_pages, size_t size_bits)
+{
+ /* look for a contiguous range that is free.
+ * We use first-fit with the optimisation that we store
+ * a pointer to the last thing we freed/allocated */
+ int num_4k_pages = BYTES_TO_4K_PAGES(num_pages * (1 << size_bits));
+ void *current = data->last_allocated;
+ size_t contiguous = 0;
+ void *start = data->last_allocated;
+ while (contiguous < num_4k_pages) {
+
+ if (is_available(data->top_level, current) && IS_ALIGNED((uint32_t)((seL4_Word)start), size_bits)) {
+ contiguous++;
+ } else {
+ start = current + PAGE_SIZE_4K;
+ contiguous = 0;
+ }
+
+ current += PAGE_SIZE_4K;
+
+ if (current >= (void *) KERNEL_RESERVED_START) {
+ LOG_ERROR("Out of virtual memory");
+ return NULL;
+ }
+
+ }
+
+ data->last_allocated = current;
+
+ return start;
+}
+
+static int
+alloc_pages(vspace_t *vspace, seL4_CPtr pages[], size_t num_pages, size_t size_bits)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ for (int i = 0; i < num_pages; i++) {
+ vka_object_t object;
+ if (vka_alloc_frame(data->vka, size_bits, &object) != 0) {
+ /* abort! */
+ LOG_ERROR("Failed to allocate page");
+ return -1;
+ }
+
+ vspace_maybe_call_allocated_object(vspace, object);
+ pages[i] = object.cptr;
+ }
+
+ return 0;
+}
+
+static int
+map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], void *vaddr, size_t num_pages,
+ size_t size_bits, seL4_CapRights rights, int cacheable)
+{
+ int error = seL4_NoError;
+ for (int i = 0; i < num_pages && error == seL4_NoError; i++) {
+ assert(caps[i] != 0);
+ error = map_page(vspace, caps[i], vaddr, rights, cacheable, size_bits);
+
+ if (error == seL4_NoError) {
+ error = update_entries(vspace, vaddr, caps[i], size_bits);
+ vaddr += (1 << size_bits);
+ }
+ }
+ return error;
+}
+
+static int
+new_pages_at_vaddr(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits,
+ seL4_CapRights rights, int cacheable)
+{
+ seL4_CPtr pages[num_pages];
+
+ int error = alloc_pages(vspace, pages, num_pages, size_bits);
+ if (error == 0) {
+ error = map_pages_at_vaddr(vspace, pages, vaddr, num_pages, size_bits, rights, cacheable);
+ }
+
+ return error;
+}
+
+/* VSPACE INTERFACE FUNCTIONS */
+
+int
+sel4utils_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], void *vaddr,
+ size_t num_pages, size_t size_bits, reservation_t *reservation)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ if (!check_reservation(data->top_level, reservation, vaddr, num_pages, size_bits)) {
+ return -1;
+ }
+
+ return map_pages_at_vaddr(vspace, caps, vaddr, num_pages, size_bits,
+ reservation->rights, reservation->cacheable);
+}
+
+seL4_CPtr
+sel4utils_get_cap(vspace_t *vspace, void *vaddr)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ seL4_CPtr entry = get_entry(data->top_level, vaddr);
+
+ if (entry == RESERVED) {
+ entry = 0;
+ }
+ return entry;
+}
+
+void *
+sel4utils_map_pages(vspace_t *vspace, seL4_CPtr caps[], seL4_CapRights rights,
+ size_t num_pages, size_t size_bits, int cacheable)
+{
+ struct sel4utils_alloc_data *data = get_alloc_data(vspace);
+ void *vaddr = find_range(data, num_pages, size_bits);
+
+ if (vaddr == NULL) {
+ return NULL;
+ }
+
+ int error = map_pages_at_vaddr(vspace, caps, vaddr, num_pages, size_bits, rights,
+ cacheable);
+ if (error == seL4_NoError) {
+ return vaddr;
+ } else {
+ return NULL;
+ }
+}
+
+
+int sel4utils_unmap_reserved_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits, reservation_t *reservation) {
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+
+ if (!check_reservation_bounds(reservation, vaddr, num_pages, size_bits)) {
+ printf("check reservation failed vaddr %p\n", vaddr);
+ return -1;
+ }
+ for (int i = 0; i < num_pages; i++) {
+ seL4_CPtr cap = sel4utils_get_cap(vspace, vaddr);
+
+ if (cap != 0) {
+ int error = seL4_ARCH_Page_Unmap(get_entry(data->top_level, vaddr));
+ if (error != seL4_NoError) {
+ LOG_ERROR("Failed to unmap page at vaddr %p", vaddr);
+ }
+
+ /*update entires*/
+ update_entries(vspace, vaddr, RESERVED, size_bits);
+ }
+
+ vaddr += (1 << size_bits);
+ }
+
+ return 0;
+}
+
+void
+sel4utils_unmap_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ for (int i = 0; i < num_pages; i++) {
+ seL4_CPtr cap = sel4utils_get_cap(vspace, vaddr);
+
+ if (cap != 0) {
+ int error = seL4_ARCH_Page_Unmap(get_entry(data->top_level, vaddr));
+ if (error != seL4_NoError) {
+ LOG_ERROR("Failed to unmap page at vaddr %p", vaddr);
+ }
+ }
+
+ vaddr += (1 << size_bits);
+ }
+}
+
+int
+sel4utils_new_pages_at_vaddr(vspace_t *vspace, void *vaddr, size_t num_pages,
+ size_t size_bits, reservation_t *reservation)
+{
+ struct sel4utils_alloc_data *data = get_alloc_data(vspace);
+
+ if (!check_reservation(data->top_level, reservation, vaddr, num_pages, size_bits)) {
+ LOG_ERROR("Range for vaddr %p with "DFMT" 4k pages not reserved!", vaddr, num_pages);
+ return -1;
+ }
+
+ return new_pages_at_vaddr(vspace, vaddr, num_pages, size_bits,
+ reservation->rights, reservation->cacheable);
+}
+
+void *
+sel4utils_new_pages(vspace_t *vspace, seL4_CapRights rights, size_t num_pages,
+ size_t size_bits)
+{
+ struct sel4utils_alloc_data *data = get_alloc_data(vspace);
+
+ void *vaddr = find_range(data, num_pages, size_bits);
+ if (vaddr == NULL) {
+ return NULL;
+ }
+
+ int error = new_pages_at_vaddr(vspace, vaddr, num_pages, size_bits, rights, 1);
+ if (error == seL4_NoError) {
+ return vaddr;
+ } else {
+ return NULL;
+ }
+}
+
+void
+sel4utils_free_pages(vspace_t *vspace, void *vaddr, size_t num_pages,
+ size_t size_bits)
+{
+ /* first unmap the pages */
+ sel4utils_unmap_pages(vspace, vaddr, num_pages, size_bits);
+
+ /* now mark them all as free */
+ for (int i = 0; i < num_pages; i++) {
+ clear_entries(vspace, vaddr, size_bits);
+ vaddr += PAGE_SIZE_4K;
+ }
+}
+
+void *
+sel4utils_new_stack(vspace_t *vspace)
+{
+ /* this implementation allocates stacks with small pages. */
+ int num_pages = BYTES_TO_4K_PAGES(CONFIG_SEL4UTILS_STACK_SIZE);
+ struct sel4utils_alloc_data *data = get_alloc_data(vspace);
+
+ void *vaddr = find_range(data, num_pages + 1, seL4_PageBits);
+
+ /* reserve the first page as the guard */
+ int error = reserve(vspace, vaddr);
+ if (error) {
+ return NULL;
+ }
+
+ void *stack_bottom = vaddr + PAGE_SIZE_4K;
+ error = new_pages_at_vaddr(vspace, stack_bottom, num_pages, seL4_PageBits,
+ seL4_AllRights, 1);
+
+ /* abort */
+ if (error != seL4_NoError) {
+ clear(vspace, vaddr);
+ return NULL;
+ }
+
+ /* return a pointer to the TOP of the stack */
+ return stack_bottom + CONFIG_SEL4UTILS_STACK_SIZE;
+}
+
+void
+sel4utils_free_stack(vspace_t *vspace, void *stack_top)
+{
+ int num_pages = BYTES_TO_4K_PAGES(CONFIG_SEL4UTILS_STACK_SIZE);
+
+ sel4utils_free_pages(vspace, stack_top - CONFIG_SEL4UTILS_STACK_SIZE,
+ num_pages, seL4_PageBits);
+
+ /* unreserve the guard page */
+ clear(vspace, stack_top - CONFIG_SEL4UTILS_STACK_SIZE - PAGE_SIZE_4K);
+}
+
+void *
+sel4utils_new_ipc_buffer(vspace_t *vspace, seL4_CPtr *page)
+{
+ void *vaddr = sel4utils_new_pages(vspace, seL4_AllRights, 1, seL4_PageBits);
+ if (vaddr == NULL) {
+ LOG_ERROR("Failed to create ipc buffer");
+ return NULL;
+ }
+
+ *page = sel4utils_get_cap(vspace, vaddr);
+
+ return vaddr;
+}
+
+void
+sel4utils_free_ipc_buffer(vspace_t *vspace, void *vaddr)
+{
+ sel4utils_free_pages(vspace, vaddr, 1, seL4_PageBits);
+}
+
+
+int sel4utils_reserve_range_no_alloc(vspace_t *vspace, reservation_t *reservation, size_t size,
+ seL4_CapRights rights, int cacheable, void **result)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ void *vaddr = find_range(data, BYTES_TO_4K_PAGES(size), seL4_PageBits);
+
+ if (vaddr == NULL) {
+ return -1;
+ }
+
+ *result = vaddr;
+ perform_reservation(vspace, reservation, vaddr, size, rights, cacheable);
+ return 0;
+}
+
+reservation_t *
+sel4utils_reserve_range(vspace_t *vspace, size_t size, seL4_CapRights rights,
+ int cacheable, void **result)
+{
+ reservation_t *reservation = malloc(sizeof(struct reservation));
+ if (reservation == NULL) {
+ LOG_ERROR("Malloc failed");
+ return NULL;
+ }
+
+ int error = sel4utils_reserve_range_no_alloc(vspace, reservation, size, rights, cacheable, result);
+ if (error) {
+ free(reservation);
+ return NULL;
+ }
+
+ return reservation;
+}
+
+int sel4utils_reserve_range_at_no_alloc(vspace_t *vspace, reservation_t *reservation, void *vaddr,
+ size_t size, seL4_CapRights rights, int cacheable)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ if (!check_empty_range(data->top_level, vaddr, BYTES_TO_4K_PAGES(size),
+ seL4_PageBits)) {
+ LOG_ERROR("Range not available at %p, size 0x"XFMT"", vaddr, size);
+ return -1;
+ }
+ perform_reservation(vspace, reservation, vaddr, size, rights, cacheable);
+ return 0;
+}
+
+reservation_t *
+sel4utils_reserve_range_at(vspace_t *vspace, void *vaddr, size_t size, seL4_CapRights
+ rights, int cacheable)
+{
+ reservation_t *reservation = malloc(sizeof(struct reservation));
+ if (reservation == NULL) {
+ LOG_ERROR("Malloc failed");
+ return NULL;
+ }
+
+ int error = sel4utils_reserve_range_at_no_alloc(vspace, reservation, vaddr, size, rights, cacheable);
+ if (error) {
+ free(reservation);
+ return NULL;
+ }
+ return reservation;
+}
+
+void sel4utils_free_reservation_no_alloc(vspace_t *vspace, reservation_t *reservation)
+{
+ sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+ for (void *current = reservation->start; current < reservation->end; current += PAGE_SIZE_4K) {
+ if (get_entry(data->top_level, current) == RESERVED) {
+ clear(vspace, current);
+ }
+ }
+}
+
+void
+sel4utils_free_reservation(vspace_t *vspace, reservation_t *reservation)
+{
+ sel4utils_free_reservation_no_alloc(vspace, reservation);
+ free(reservation);
+}
+
+#endif /* CONFIG_LIB_SEL4_VKA && CONFIG_LIB_SEL4_VSPACE */
