allocman: use new vspace ps_map_object
diff --git a/libsel4allocman/CMakeLists.txt b/libsel4allocman/CMakeLists.txt
index 1692376..66e2288 100644
--- a/libsel4allocman/CMakeLists.txt
+++ b/libsel4allocman/CMakeLists.txt
@@ -23,4 +23,4 @@
add_library(sel4allocman STATIC EXCLUDE_FROM_ALL ${deps})
target_include_directories(sel4allocman PUBLIC include "sel4_arch/${KernelSel4Arch}")
target_include_directories(sel4allocman PUBLIC include "arch/${KernelArch}")
-target_link_libraries(sel4allocman Configuration muslc sel4 sel4vka sel4utils)
+target_link_libraries(sel4allocman Configuration muslc sel4 sel4vka sel4utils sel4vspace)
diff --git a/libsel4allocman/arch/arm/allocman/arch/mapping.h b/libsel4allocman/arch/arm/allocman/arch/mapping.h
deleted file mode 100644
index 7c1db87..0000000
--- a/libsel4allocman/arch/arm/allocman/arch/mapping.h
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
- * Copyright 2018, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/sel4_arch/mapping.h>
diff --git a/libsel4allocman/arch/riscv/allocman/arch/mapping.h b/libsel4allocman/arch/riscv/allocman/arch/mapping.h
deleted file mode 100644
index 9747fa6..0000000
--- a/libsel4allocman/arch/riscv/allocman/arch/mapping.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * Copyright 2018, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-#pragma once
-
-#include <allocman/allocman.h>
-
-static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
- /* RISCV has no paging objects beyond the common page table
- * so this function should never get called */
- ZF_LOGF("Invalid lookup level");
- return seL4_InvalidArgument;
-}
-
diff --git a/libsel4allocman/arch/x86/allocman/arch/mapping.h b/libsel4allocman/arch/x86/allocman/arch/mapping.h
deleted file mode 100644
index 7c1db87..0000000
--- a/libsel4allocman/arch/x86/allocman/arch/mapping.h
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
- * Copyright 2018, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/sel4_arch/mapping.h>
diff --git a/libsel4allocman/sel4_arch/aarch32/allocman/sel4_arch/mapping.h b/libsel4allocman/sel4_arch/aarch32/allocman/sel4_arch/mapping.h
deleted file mode 100644
index 23fc274..0000000
--- a/libsel4allocman/sel4_arch/aarch32/allocman/sel4_arch/mapping.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*
- * Copyright 2017, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/allocman.h>
-
-static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
- /* ARM has no paging objects beyond the common page table
- * so this function should never get called */
- ZF_LOGF("Invalid lookup level");
- return seL4_InvalidArgument;
-}
-
diff --git a/libsel4allocman/sel4_arch/aarch64/allocman/sel4_arch/mapping.h b/libsel4allocman/sel4_arch/aarch64/allocman/sel4_arch/mapping.h
deleted file mode 100644
index ed3437b..0000000
--- a/libsel4allocman/sel4_arch/aarch64/allocman/sel4_arch/mapping.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*
- * Copyright 2017, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/allocman.h>
-
-static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
- struct object {
- seL4_Word bits;
- seL4_Word type;
- seL4_Error (*map)(seL4_CPtr, seL4_CPtr, seL4_Word, seL4_Word);
- };
- struct object objects[] = {
- [SEL4_MAPPING_LOOKUP_NO_PT] = {seL4_PageTableBits, seL4_ARM_PageTableObject, seL4_ARM_PageTable_Map},
- [SEL4_MAPPING_LOOKUP_NO_PD] = {seL4_PageDirBits, seL4_ARM_PageDirectoryObject, seL4_ARM_PageDirectory_Map},
- [SEL4_MAPPING_LOOKUP_NO_PUD] = {seL4_PUDBits, seL4_ARM_PageUpperDirectoryObject, seL4_ARM_PageUpperDirectory_Map},
- };
- if (bits >= ARRAY_SIZE(objects) || !objects[bits].map) {
- ZF_LOGF("Unknown lookup bits %d", (int)bits);
- return seL4_InvalidArgument;
- }
- struct object *obj = &objects[bits];
- int error;
- seL4_Word cookie;
- cookie = allocman_utspace_alloc(alloc, obj->bits, obj->type, path, false, &error);
- if (error) {
- ZF_LOGV("Failed to allocate object %d of size %d, got error %d", (int)obj->type, (int)obj->bits, error);
- return seL4_NotEnoughMemory;
- }
- error = obj->map(path->capPtr, vspace_root, (seL4_Word)vaddr, seL4_ARM_Default_VMAttributes);
- if (error) {
- allocman_utspace_free(alloc, cookie, obj->bits);
- }
- return error;
-}
-
diff --git a/libsel4allocman/sel4_arch/ia32/allocman/sel4_arch/mapping.h b/libsel4allocman/sel4_arch/ia32/allocman/sel4_arch/mapping.h
deleted file mode 100644
index 3834db4..0000000
--- a/libsel4allocman/sel4_arch/ia32/allocman/sel4_arch/mapping.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*
- * Copyright 2017, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/allocman.h>
-
-static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
- /* IA32 has no paging objects beyond the common page table
- * so this function should never get called */
- ZF_LOGF("Invalid lookup level");
- return seL4_InvalidArgument;
-}
-
diff --git a/libsel4allocman/sel4_arch/x86_64/allocman/sel4_arch/mapping.h b/libsel4allocman/sel4_arch/x86_64/allocman/sel4_arch/mapping.h
deleted file mode 100644
index 84b88e7..0000000
--- a/libsel4allocman/sel4_arch/x86_64/allocman/sel4_arch/mapping.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*
- * Copyright 2017, Data61
- * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
- * ABN 41 687 119 230.
- *
- * 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(DATA61_BSD)
- */
-
-#pragma once
-
-#include <allocman/allocman.h>
-
-static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
- struct object {
- seL4_Word bits;
- seL4_Word type;
- seL4_Error (*map)(seL4_CPtr, seL4_CPtr, seL4_Word, seL4_Word);
- };
- struct object objects[] = {
- [SEL4_MAPPING_LOOKUP_NO_PT] = {seL4_PageTableBits, seL4_X86_PageTableObject, seL4_X86_PageTable_Map},
- [SEL4_MAPPING_LOOKUP_NO_PD] = {seL4_PageDirBits, seL4_X86_PageDirectoryObject, seL4_X86_PageDirectory_Map},
- [SEL4_MAPPING_LOOKUP_NO_PDPT] = {seL4_PDPTBits, seL4_X86_PDPTObject, seL4_X86_PDPT_Map},
- };
- if (bits >= ARRAY_SIZE(objects) || !objects[bits].map) {
- ZF_LOGF("Unknown lookup bits %d", (int)bits);
- return seL4_InvalidArgument;
- }
- struct object *obj = &objects[bits];
- int error;
- seL4_Word cookie;
- cookie = allocman_utspace_alloc(alloc, obj->bits, obj->type, path, false, &error);
- if (error) {
- ZF_LOGV("Failed to allocate object %d of size %d, got error %d", (int)obj->type, (int)obj->bits, error);
- return seL4_NotEnoughMemory;
- }
- error = obj->map(path->capPtr, vspace_root, (seL4_Word)vaddr, seL4_X86_Default_VMAttributes);
- if (error) {
- allocman_utspace_free(alloc, cookie, obj->bits);
- }
- return error;
-}
-
diff --git a/libsel4allocman/src/mspace/virtual_pool.c b/libsel4allocman/src/mspace/virtual_pool.c
index 02de33e..4280aa1 100644
--- a/libsel4allocman/src/mspace/virtual_pool.c
+++ b/libsel4allocman/src/mspace/virtual_pool.c
@@ -17,10 +17,10 @@
#include <sel4/sel4.h>
#include <sel4utils/mapping.h>
#include <vka/kobject_t.h>
-#include <allocman/arch/mapping.h>
+#include <vspace/mapping.h>
#include <string.h>
-/* This allocator deliberately does not use the vspace library to prevent
+/* This allocator deliberately does not use the vspace library to manage mappings to prevent
* circular dependencies between the vspace library and the allocator */
static int _add_page(allocman_t *alloc, seL4_CPtr pd, void *vaddr)
@@ -48,25 +48,19 @@
break;
}
seL4_Word failed_bits = seL4_MappingFailedLookupLevel();
- /* handle the common case that occurs on all architectures of
- * a page table being missing */
- if (failed_bits == SEL4_MAPPING_LOOKUP_NO_PT) {
- seL4_Word cookie;
- cookie = allocman_utspace_alloc(alloc, seL4_PageTableBits, kobject_get_type(KOBJECT_PAGE_TABLE, 0), &path, false, &error);
- if (error) {
- allocman_cspace_free(alloc, &path);
- ZF_LOGV("Failed to allocate page table");
- break;
- }
- error = seL4_ARCH_PageTable_Map(path.capPtr, pd, (seL4_Word) vaddr,
- seL4_ARCH_Default_VMAttributes);
- if (error != seL4_NoError) {
- allocman_utspace_free(alloc, cookie, seL4_PageTableBits);
- }
- } else {
- error = allocman_sel4_arch_create_object_at_level(alloc, failed_bits, &path, vaddr, pd);
+ vspace_map_obj_t obj;
+ error = vspace_get_map_obj(failed_bits, &obj);
+ assert(error == 0);
+
+ seL4_Word cookie = allocman_utspace_alloc(alloc, obj.size_bits, obj.type, &path, false, &error);
+ if (error) {
+ allocman_cspace_free(alloc, &path);
+ ZF_LOGV("Failed to allocate paging structure");
+ break;
}
+ error = vspace_map_obj(&obj, path.capPtr, pd, (seL4_Word) vaddr, seL4_ARCH_Default_VMAttributes);
if (error != seL4_NoError) {
+ allocman_utspace_free(alloc, cookie, seL4_PageTableBits);
allocman_cspace_free(alloc, &path);
break;
}
