Merge pull request #66 in SEL4/sel4_libs from ~MFERNANDEZ/sel4_libs:aeeb7e68-c2e2-43c6-8d72-bd94b55363c7 to master * commit 'a7e6e0557ff787c458ed6e941ec925040bd7dbad': libsel4utils: Mark some strings as const. libsel4test: Mark some char * parameters as const. libsel4allocman: Fix missing initialised field.
diff --git a/libsel4allocman/include/allocman/bootstrap.h b/libsel4allocman/include/allocman/bootstrap.h index 30f95b0..9c0dcba 100644 --- a/libsel4allocman/include/allocman/bootstrap.h +++ b/libsel4allocman/include/allocman/bootstrap.h
@@ -57,7 +57,6 @@ #include <allocman/mspace/fixed_pool.h> #include <allocman/mspace/virtual_pool.h> #include <allocman/utspace/twinkle.h> -#include <allocman/utspace/trickle.h> #include <vspace/vspace.h> #include <simple/simple.h> /**
diff --git a/libsel4allocman/include/allocman/utspace/trickle.h b/libsel4allocman/include/allocman/utspace/trickle.h deleted file mode 100644 index 8fa6dda..0000000 --- a/libsel4allocman/include/allocman/utspace/trickle.h +++ /dev/null
@@ -1,61 +0,0 @@ -/* - * 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 _ALLOCMAN_UTSPACE_TRICKLE_H_ -#define _ALLOCMAN_UTSPACE_TRICKLE_H_ - -#include <autoconf.h> -#include <sel4/types.h> -#include <allocman/utspace/utspace.h> -#include <assert.h> - -#ifdef CONFIG_KERNEL_STABLE - -struct utspace_trickle_node { - cspacepath_t *ut; - size_t offset; - seL4_Word parent_cookie; - size_t bitmap_bits; - size_t bitmap; - struct utspace_trickle_node *next, *prev; - size_t padding; - uintptr_t paddr; -}; - -compile_time_assert(trickle_struct_size32, sizeof(struct utspace_trickle_node) == 36 || sizeof(size_t) == 8); -compile_time_assert(trickle_struct_size64, sizeof(struct utspace_trickle_node) == 72 || sizeof(size_t) == 4); - -typedef struct utspace_trickle { - struct utspace_trickle_node *heads[CONFIG_WORD_SIZE]; -} utspace_trickle_t; - -void utspace_trickle_create(utspace_trickle_t *trickle); - -int _utspace_trickle_add_uts(struct allocman *alloc, void *_trickle, size_t num, const cspacepath_t *uts, size_t *size_bits, uintptr_t *paddr); - -seL4_Word _utspace_trickle_alloc(struct allocman *alloc, void *_trickle, size_t size_bits, seL4_Word type, const cspacepath_t *slot, int *error); -void _utspace_trickle_free(struct allocman *alloc, void *_trickle, seL4_Word cookie, size_t size_bits); - -uintptr_t _utspace_trickle_paddr(void *_trickle, seL4_Word cookie, size_t size_bits); - -static inline utspace_interface_t utspace_trickle_make_interface(utspace_trickle_t *trickle) { - return (utspace_interface_t) { - .alloc = _utspace_trickle_alloc, - .free = _utspace_trickle_free, - .add_uts = _utspace_trickle_add_uts, - .paddr = _utspace_trickle_paddr, - .properties = ALLOCMAN_DEFAULT_PROPERTIES, - .utspace = trickle - }; -} - -#endif /* CONFIG_KERNEL_STABLE */ - -#endif
diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c index 9f06f08..9debfa2 100644 --- a/libsel4allocman/src/bootstrap.c +++ b/libsel4allocman/src/bootstrap.c
@@ -15,7 +15,6 @@ #include <allocman/cspace/simple1level.h> #include <allocman/cspace/two_level.h> #include <allocman/mspace/dual_pool.h> -#include <allocman/utspace/trickle.h> #include <allocman/utspace/split.h> #include <allocman/bootstrap.h> #include <allocman/sel4_arch/reservation.h> @@ -28,11 +27,7 @@ #include <utils/arith.h> /* configure the choice of boot strapping allocators */ -#if defined(CONFIG_KERNEL_STABLE) -#define UTMAN trickle -#else #define UTMAN split -#endif /*do some nasty macro expansion to get the string substitution to happen how we want */ #define CON2(a, b,c) a##b##c @@ -275,37 +270,6 @@ return 0; } -#if defined(CONFIG_KERNEL_STABLE) - -static int _split_ut(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t p1, cspacepath_t p2, size_t size) { - int error; - error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_UntypedObject, 0, size, p1.root, p1.dest, p1.destDepth, p1.offset, 1); - if (error != seL4_NoError) { - LOG_ERROR("Failed to split untyped"); - return 1; - } - error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_UntypedObject, BIT(size), size, - p2.root, p2.dest, p2.destDepth, p2.offset, 1); - if (error != seL4_NoError) { - LOG_ERROR("Failed to allocate second half of split untyped"); - return 1; - } - return 0; -} - -static int _retype_cnode(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t cnode, seL4_Word sel4_size) { - int error; - error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_CapTableObject, 0, sel4_size, - cnode.root, cnode.dest, cnode.destDepth, cnode.offset, 1); - if (error != seL4_NoError) { - LOG_ERROR("Failed to retype a cnode"); - return 1; - } - return 0; -} - -#else - static int _split_ut(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t p1, cspacepath_t p2, size_t size) { int error; error = seL4_Untyped_Retype(ut.capPtr, seL4_UntypedObject, size, p1.root, p1.dest, p1.destDepth, p1.offset, 1); @@ -329,8 +293,6 @@ return 0; } -#endif - static int bootstrap_allocate_cnode(bootstrap_info_t *bs, size_t size, cspacepath_t *slot) { size_t ut_size; int i;
diff --git a/libsel4allocman/src/utspace/split.c b/libsel4allocman/src/utspace/split.c index 416348c..b255d8d 100644 --- a/libsel4allocman/src/utspace/split.c +++ b/libsel4allocman/src/utspace/split.c
@@ -135,11 +135,7 @@ return 1; } /* perform the first retype */ -#if defined(CONFIG_KERNEL_STABLE) - sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, seL4_UntypedObject, 0, size_bits, left->ut.root, left->ut.dest, left->ut.destDepth, left->ut.offset, 1); -#else sel4_error = seL4_Untyped_Retype(node->ut.capPtr, seL4_UntypedObject, size_bits, left->ut.root, left->ut.dest, left->ut.destDepth, left->ut.offset, 1); -#endif if (sel4_error != seL4_NoError) { _delete_node(alloc, left); _delete_node(alloc, right); @@ -147,11 +143,7 @@ return 1; } /* perform the second retype */ -#if defined(CONFIG_KERNEL_STABLE) - sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, seL4_UntypedObject, BIT(size_bits), size_bits, right->ut.root, right->ut.dest, right->ut.destDepth, right->ut.offset, 1); -#else sel4_error = seL4_Untyped_Retype(node->ut.capPtr, seL4_UntypedObject, size_bits, right->ut.root, right->ut.dest, right->ut.destDepth, right->ut.offset, 1); -#endif if (sel4_error != seL4_NoError) { vka_cnode_delete(&left->ut); _delete_node(alloc, left); @@ -199,11 +191,7 @@ /* use the first node for lack of a better one */ node = split->heads[size_bits]; /* Perform the untyped retype */ -#if defined(CONFIG_KERNEL_STABLE) - sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, type, 0, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1); -#else sel4_error = seL4_Untyped_Retype(node->ut.capPtr, type, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1); -#endif if (sel4_error != seL4_NoError) { /* Well this shouldn't happen */ SET_ERROR(error, 1);
diff --git a/libsel4allocman/src/utspace/trickle.c b/libsel4allocman/src/utspace/trickle.c deleted file mode 100644 index 80e039e..0000000 --- a/libsel4allocman/src/utspace/trickle.c +++ /dev/null
@@ -1,251 +0,0 @@ -/* - * 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> -#include <allocman/utspace/trickle.h> -#include <allocman/allocman.h> -#include <allocman/util.h> -#include <sel4/sel4.h> - -#include <vka/object.h> - -#ifdef CONFIG_KERNEL_STABLE - -static inline size_t _make_bitmap(size_t bits) { - /* avoid shift by int max in BIT/MASK code */ - if (BIT(bits - 1) == CONFIG_WORD_SIZE) { - return -1; - } else { - /* shift the result up so that the high bits are set */ - return MASK(BIT(bits - 1)) << (CONFIG_WORD_SIZE - BIT(bits - 1)); - } -} - -static inline void _insert_node(struct utspace_trickle_node **head, struct utspace_trickle_node *node) -{ - if (*head) { - (*head)->prev = node; - } - node->next = *head; - node->prev = NULL; - *head = node; -} - -static inline void _remove_node(struct utspace_trickle_node **head, struct utspace_trickle_node *node) -{ - if (node->next) { - node->next->prev = node->prev; - } - if (node->prev) { - node->prev->next = node->next; - } else { - *head = node->next; - } -} - -static inline seL4_Word _make_cookie(struct utspace_trickle_node *node, size_t offset) -{ - size_t int_node = (size_t) node; - assert( (int_node % (CONFIG_WORD_SIZE)) == 0); - assert(offset < CONFIG_WORD_SIZE); - return int_node | offset; -} - -static inline struct utspace_trickle_node *_cookie_to_node(seL4_Word cookie) { - cookie -= cookie % (CONFIG_WORD_SIZE); - return (struct utspace_trickle_node*)cookie; -} - -static inline size_t _cookie_to_offset(seL4_Word cookie) -{ - return cookie % (CONFIG_WORD_SIZE); -} - -static inline struct utspace_trickle_node *_make_node(struct allocman *alloc, int *error) { - uintptr_t addr = (uintptr_t)allocman_mspace_alloc(alloc, sizeof(struct utspace_trickle_node) * 2 - sizeof(size_t), error); - struct utspace_trickle_node *node; - if (*error) { - return NULL; - } - node = _cookie_to_node(addr + CONFIG_WORD_SIZE); - node->padding = addr; - return node; -} - -static inline void _free_node(struct allocman *alloc, struct utspace_trickle_node *node) -{ - allocman_mspace_free(alloc, (void*)node->padding, sizeof(struct utspace_trickle_node) * 2 - sizeof(size_t)); -} - -int _utspace_trickle_add_uts(allocman_t *alloc, void *_trickle, size_t num, const cspacepath_t *uts, size_t *size_bits, uintptr_t *paddr) { - utspace_trickle_t *trickle = (utspace_trickle_t*) _trickle; - struct utspace_trickle_node *nodes[num]; - cspacepath_t *uts_copy[num]; - int error; - size_t i; - for (i = 0; i < num; i++) { - nodes[i] = _make_node(alloc, &error); - if (error) { - for (i--; i >= 0; i--) { - _free_node(alloc, nodes[i]); - allocman_mspace_free(alloc, uts_copy[i], sizeof(cspacepath_t)); - } - return error; - } - uts_copy[i] = allocman_mspace_alloc(alloc, sizeof(cspacepath_t), &error); - if (error) { - _free_node(alloc, nodes[i]); - for (i--; i >= 0; i--) { - _free_node(alloc, nodes[i]); - allocman_mspace_free(alloc, uts_copy[i], sizeof(cspacepath_t)); - } - } - } - for (i = 0; i < num; i++) { - *uts_copy[i] = uts[i]; - nodes[i]->ut = uts_copy[i]; - nodes[i]->offset = 0; - nodes[i]->paddr = paddr[i]; - nodes[i]->parent_cookie = 0; - nodes[i]->next = nodes[i]->prev = NULL; - /* Start with only 1 thing free */ - nodes[i]->bitmap = BIT(31); - nodes[i]->bitmap_bits = 1; - _insert_node(&trickle->heads[size_bits[i]], nodes[i]); - } - return 0; -} - -void utspace_trickle_create(utspace_trickle_t *trickle) -{ - uint32_t i; - for (i = 0; i < CONFIG_WORD_SIZE; i++) { - trickle->heads[i] = NULL; - } -} - -static int _refill_pool(struct allocman *alloc, utspace_trickle_t *trickle, size_t size_bits) -{ - size_t i; - int error; - struct utspace_trickle_node *node; - seL4_Word cookie; - node = _make_node(alloc, &error); - if (error) { - return error; - } - /* Check if there are untypeds >= 5 size_bits from us */ - for (i = size_bits + 5 > CONFIG_WORD_SIZE - 1 ? CONFIG_WORD_SIZE - 1 : size_bits + 5; i < CONFIG_WORD_SIZE; i++) { - if (trickle->heads[i]) { - i = size_bits + 5; - break; - } - } - if (i == CONFIG_WORD_SIZE) { - /* Search for the biggest one near us */ - for (i = size_bits + 5 > CONFIG_WORD_SIZE - 1 ? CONFIG_WORD_SIZE - 1 : size_bits + 5; i > size_bits; i--) { - if (trickle->heads[i]) { - break; - } - } - } - if (i != size_bits) { - cookie = _utspace_trickle_alloc(alloc, trickle, i, seL4_UntypedObject, NULL, &error); - if (!error) { - struct utspace_trickle_node *parent = _cookie_to_node(cookie); - size_t offset = _cookie_to_offset(cookie); - node->ut = parent->ut; - node->offset = parent->offset + (offset << (i)); - if (parent->paddr) { - node->paddr = parent->paddr + (offset << (i)); - } else { - node->paddr = 0; - } - node->parent_cookie = cookie; - node->bitmap_bits = i - size_bits + 1; - node->bitmap = _make_bitmap(node->bitmap_bits); - node->next = node->prev = NULL; - _insert_node(&trickle->heads[size_bits], node); - return 0; - } - } - _free_node(alloc, node); - return 1; -} - -seL4_Word _utspace_trickle_alloc(struct allocman *alloc, void *_trickle, size_t size_bits, seL4_Word type, const cspacepath_t *slot, int *error) -{ - size_t sel4_size_bits; - int _error; - utspace_trickle_t *trickle = (utspace_trickle_t*)_trickle; - struct utspace_trickle_node *node; - size_t offset; - size_t mem_offset; - /* get size of untyped call */ - sel4_size_bits = get_sel4_object_size(type, size_bits); - if (size_bits != vka_get_object_size(type, sel4_size_bits) || size_bits == 0) { - SET_ERROR(error, 1); - return 0; - } - assert(size_bits < CONFIG_WORD_SIZE); - if (!trickle->heads[size_bits]) { - _error = _refill_pool(alloc, trickle, size_bits); - if (_error) { - SET_ERROR(error, _error); - return 0; - } - } - node = trickle->heads[size_bits]; - offset = CLZL(node->bitmap); - mem_offset = node->offset + (offset << size_bits); - if (slot) { - _error = seL4_Untyped_RetypeAtOffset(node->ut->capPtr, type, mem_offset, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1); - if (_error != seL4_NoError) { - SET_ERROR(error, 1); - return 0; - } - } - node->bitmap &= ~BIT(CONFIG_WORD_SIZE - 1 - offset); - if (node->bitmap == 0) { - _remove_node(&trickle->heads[size_bits], node); - } - SET_ERROR(error, 0); - return _make_cookie(node, offset); -} - -void _utspace_trickle_free(struct allocman *alloc, void *_trickle, seL4_Word cookie, size_t size_bits) -{ - utspace_trickle_t *trickle = (utspace_trickle_t*)_trickle; - struct utspace_trickle_node *node = _cookie_to_node(cookie); - size_t offset = _cookie_to_offset(cookie); - int in_list = !(node->bitmap == 0); - node->bitmap |= BIT(CONFIG_WORD_SIZE - 1 - offset); - if (node->bitmap == _make_bitmap(node->bitmap_bits)) { - if (node->parent_cookie) { - if (in_list) { - _remove_node(&trickle->heads[size_bits], node); - } - _utspace_trickle_free(alloc, trickle, node->parent_cookie, size_bits + node->bitmap_bits - 1); - _free_node(alloc, node); - } else if (!in_list) { - _insert_node(&trickle->heads[size_bits], node); - } - } else if (!in_list) { - _insert_node(&trickle->heads[size_bits], node); - } -} - -uintptr_t _utspace_trickle_paddr(void *_trickle, seL4_Word cookie, size_t size_bits) { - struct utspace_trickle_node *node = _cookie_to_node(cookie); - size_t offset = _cookie_to_offset(cookie); - return node->paddr + (offset << size_bits); -} - -#endif
diff --git a/libsel4allocman/src/utspace/twinkle.c b/libsel4allocman/src/utspace/twinkle.c index 908e763..7e3681f 100644 --- a/libsel4allocman/src/utspace/twinkle.c +++ b/libsel4allocman/src/utspace/twinkle.c
@@ -82,15 +82,10 @@ i = j; } } - /* Perform the untyped retype */ -#if defined(CONFIG_KERNEL_STABLE) - sel4_error = seL4_Untyped_RetypeAtOffset(twinkle->uts[i].path.capPtr, type, _round_up(twinkle->uts[i].offset, size_bits), sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1); -#else /* if using inc retype then our offset calculation is effectively emulating the kernels calculations. This * means we track the free space of the untyped correctly, and since we are not going to try and free then * allocate again, this allocator can be used with either allocation scheme */ sel4_error = seL4_Untyped_Retype(twinkle->uts[i].path.capPtr, type, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1); -#endif if (sel4_error != seL4_NoError) { /* Well this shouldn't happen */ SET_ERROR(error, 1);
diff --git a/libsel4bench/Makefile b/libsel4bench/Makefile index ebd6d43..49752a5 100644 --- a/libsel4bench/Makefile +++ b/libsel4bench/Makefile
@@ -14,7 +14,9 @@ # Source files required to build the target CFILES := \ $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/*.c)) \ - $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/arch-$(ARCH)/*.c)) + $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/arch-$(ARCH)/*.c)) \ + $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/arch-$(ARCH)/armv/$(ARMV)/*.c)) \ + $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/arch-$(ARCH)/cpu/$(CPU)/*.c)) # Header files/directories this library provides # Note: sel4_client.h may not have been built at the time this is evaluated.
diff --git a/libsel4bench/src/arch-arm/event_counters_armv7a.c b/libsel4bench/src/arch-arm/armv/armv7-a/event_counters_armv7a.c similarity index 97% rename from libsel4bench/src/arch-arm/event_counters_armv7a.c rename to libsel4bench/src/arch-arm/armv/armv7-a/event_counters_armv7a.c index 5ae1544..5b5b0d7 100644 --- a/libsel4bench/src/arch-arm/event_counters_armv7a.c +++ b/libsel4bench/src/arch-arm/armv/armv7-a/event_counters_armv7a.c
@@ -8,11 +8,9 @@ * @TAG(NICTA_BSD) */ -#if defined(ARMV7_A) - #include <utils/util.h> -#include "event_counters.h" +#include "../../event_counters.h" #define NAME_EVENT(id, name) EVENT_COUNTER_FORMAT(SEL4BENCH_ARMV7A_EVENT_##id, name) @@ -58,5 +56,3 @@ { return ARRAY_SIZE(sel4bench_arch_event_counter_data); } - -#endif /* defined(ARMV7_A) */
diff --git a/libsel4bench/src/arch-arm/event_counters_arm1136.c b/libsel4bench/src/arch-arm/cpu/arm1136jf-s/event_counters_arm1136.c similarity index 93% rename from libsel4bench/src/arch-arm/event_counters_arm1136.c rename to libsel4bench/src/arch-arm/cpu/arm1136jf-s/event_counters_arm1136.c index 44a9870..0ef3948 100644 --- a/libsel4bench/src/arch-arm/event_counters_arm1136.c +++ b/libsel4bench/src/arch-arm/cpu/arm1136jf-s/event_counters_arm1136.c
@@ -8,11 +8,9 @@ * @TAG(NICTA_BSD) */ -#if defined(ARM1136J_S) || defined(ARM1136JF_S) - #include <utils/util.h> -#include "event_counters.h" +#include "../../event_counters.h" #define NAME_EVENT(id, name) EVENT_COUNTER_FORMAT(SEL4BENCH_ARM1136_EVENT_##id, name) @@ -54,5 +52,3 @@ { return ARRAY_SIZE(sel4bench_cpu_event_counter_data); } - -#endif /* defined(ARM1136J_S) || defined(ARM1136JF_S) */
diff --git a/libsel4bench/src/arch-arm/event_counters_cortexa15.c b/libsel4bench/src/arch-arm/cpu/cortex-a15/event_counters_cortexa15.c similarity index 96% rename from libsel4bench/src/arch-arm/event_counters_cortexa15.c rename to libsel4bench/src/arch-arm/cpu/cortex-a15/event_counters_cortexa15.c index 396625c..565daf5 100644 --- a/libsel4bench/src/arch-arm/event_counters_cortexa15.c +++ b/libsel4bench/src/arch-arm/cpu/cortex-a15/event_counters_cortexa15.c
@@ -8,11 +8,7 @@ * @TAG(NICTA_BSD) */ -#include <autoconf.h> - -#if defined(CONFIG_ARM_CORTEX_A15) - -#include "event_counters.h" +#include "../../event_counters.h" #define NAME_EVENT(id, name) EVENT_COUNTER_FORMAT(SEL4BENCH_CORTEXA15_EVENT_##id, name) @@ -67,5 +63,3 @@ { return ARRAY_SIZE(sel4bench_cpu_event_counter_data); } - -#endif /* defined(CONFIG_ARM_CORTEX_A15) */
diff --git a/libsel4bench/src/arch-arm/event_counters_cortexa8.c b/libsel4bench/src/arch-arm/cpu/cortex-a8/event_counters_cortexa8.c similarity index 94% rename from libsel4bench/src/arch-arm/event_counters_cortexa8.c rename to libsel4bench/src/arch-arm/cpu/cortex-a8/event_counters_cortexa8.c index 58bfa26..2b0f53c 100644 --- a/libsel4bench/src/arch-arm/event_counters_cortexa8.c +++ b/libsel4bench/src/arch-arm/cpu/cortex-a8/event_counters_cortexa8.c
@@ -8,11 +8,7 @@ * @TAG(NICTA_BSD) */ -#include <autoconf.h> - -#if defined(CONFIG_ARM_CORTEX_A8) - -#include "event_counters.h" +#include "../../event_counters.h" #define NAME_EVENT(id, name) EVENT_COUNTER_FORMAT(SEL4BENCH_CORTEXA8_EVENT_##id, name) @@ -54,5 +50,3 @@ { return ARRAY_SIZE(sel4bench_cpu_event_counter_data); } - -#endif /* defined(CONFIG_ARM_CORTEX_A8) */
diff --git a/libsel4bench/src/arch-arm/event_counters_cortexa9.c b/libsel4bench/src/arch-arm/cpu/cortex-a9/event_counters_cortexa9.c similarity index 95% rename from libsel4bench/src/arch-arm/event_counters_cortexa9.c rename to libsel4bench/src/arch-arm/cpu/cortex-a9/event_counters_cortexa9.c index d8e3a41..c25db15 100644 --- a/libsel4bench/src/arch-arm/event_counters_cortexa9.c +++ b/libsel4bench/src/arch-arm/cpu/cortex-a9/event_counters_cortexa9.c
@@ -8,11 +8,7 @@ * @TAG(NICTA_BSD) */ -#include <autoconf.h> - -#if defined(CONFIG_ARM_CORTEX_A9) - -#include "event_counters.h" +#include "../../event_counters.h" #define NAME_EVENT(id, name) EVENT_COUNTER_FORMAT(SEL4BENCH_CORTEXA9_EVENT_##id, name) @@ -63,5 +59,3 @@ { return ARRAY_SIZE(sel4bench_cpu_event_counter_data); } - -#endif /* defined(CONFIG_ARM_CORTEX_A9) */
diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index a0f9616..ec55b9b 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c
@@ -49,19 +49,6 @@ } } - /* mainline and experimental treat device regions differently*/ -#ifdef CONFIG_KERNEL_STABLE - ZF_LOGI("device untypeds: [%u --> %u)", info->deviceUntyped.start, info->deviceUntyped.end); - ZF_LOGI("List of device untypes"); - ZF_LOGI("Paddr | Size "); - int start = info->untyped.end - info->untyped.start; - int size = info->deviceUntyped.end - info->deviceUntyped.start; - for (int i = start; i < start + size; i++) { - if (info->untypedPaddrList[i] != 0) { - ZF_LOGI("0x%08x | %u", info->untypedPaddrList[i], info->untypedSizeBitsList[i]); - } - } -#else ZF_LOGI("DeviceRegions: %u\n", info->numDeviceRegions); printf("List of deviceRegions\n"); printf("Paddr | Size | Slot Region\n"); @@ -71,7 +58,6 @@ info->deviceRegions[i].frames.start, info->deviceRegions[i].frames.end); } -#endif /* CONFIG_KERNEL_STABLE */ }
diff --git a/libsel4utils/include/sel4utils/process.h b/libsel4utils/include/sel4utils/process.h index 1699864..03ab1b8 100644 --- a/libsel4utils/include/sel4utils/process.h +++ b/libsel4utils/include/sel4utils/process.h
@@ -118,9 +118,7 @@ vka_object_t fault_endpoint; int priority; -#ifndef CONFIG_KERNEL_STABLE seL4_CPtr asid_pool; -#endif } sel4utils_process_config_t; /**
diff --git a/libsel4utils/src/page_dma.c b/libsel4utils/src/page_dma.c index 0ece05e..75193f2 100644 --- a/libsel4utils/src/page_dma.c +++ b/libsel4utils/src/page_dma.c
@@ -112,11 +112,7 @@ if (error) { goto handle_error; } -#ifdef CONFIG_KERNEL_STABLE - error = seL4_Untyped_RetypeAtOffset(ut.cptr, kobject_get_type(KOBJECT_FRAME, PAGE_BITS_4K), PAGE_SIZE_4K * i, size_bits, frames[i].root, frames[i].dest, frames[i].destDepth, frames[i].offset, 1); -#else error = seL4_Untyped_Retype(ut.cptr, kobject_get_type(KOBJECT_FRAME, PAGE_BITS_4K), size_bits, frames[i].root, frames[i].dest, frames[i].destDepth, frames[i].offset, 1); -#endif if (error != seL4_NoError) { goto handle_error; }
diff --git a/libsel4utils/src/process.c b/libsel4utils/src/process.c index d6fd828..ed2fb3a 100644 --- a/libsel4utils/src/process.c +++ b/libsel4utils/src/process.c
@@ -369,9 +369,7 @@ .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); @@ -459,7 +457,7 @@ slot = sel4utils_copy_cap_to_process(process, src); assert(slot == SEL4UTILS_PD_SLOT); - if (!(config_set(CONFIG_KERNEL_STABLE) || config_set(CONFIG_X86_64))) { + if (!config_set(CONFIG_X86_64)) { vka_cspace_make_path(vka, get_asid_pool(asid_pool), &src); slot = sel4utils_copy_cap_to_process(process, src); assert(slot == SEL4UTILS_ASID_POOL_SLOT); @@ -501,7 +499,7 @@ } /* assign an asid pool */ - if (!(config_set(CONFIG_KERNEL_STABLE) || config_set(CONFIG_X86_64)) && + if (!config_set(CONFIG_X86_64) && assign_asid_pool(config.asid_pool, process->pd.cptr) != seL4_NoError) { goto error; }
diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c index 95ae31f..868e934 100644 --- a/libsel4utils/src/vspace/bootstrap.c +++ b/libsel4utils/src/vspace/bootstrap.c
@@ -19,10 +19,6 @@ #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. @@ -373,9 +369,6 @@ { void *existing_frames[] = { (void *) info, -#if defined(CONFIG_ARCH_X86) && 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(((seL4_Word)(info->ipcBuffer)), PAGE_SIZE_4K), NULL
diff --git a/libsel4vka/include/vka/capops.h b/libsel4vka/include/vka/capops.h index 98b377b..736c0f0 100644 --- a/libsel4vka/include/vka/capops.h +++ b/libsel4vka/include/vka/capops.h
@@ -131,17 +131,6 @@ //TODO: implement rotate -#ifdef CONFIG_KERNEL_STABLE -inline static int -vka_untyped_retypeAtOffset(vka_object_t *untyped, int type, int offset, int size_bits, - int num_objects, const cspacepath_t *dest) -{ - size_bits = vka_get_object_size(type, size_bits); - return seL4_Untyped_RetypeAtOffset(untyped->cptr, type, offset, size_bits, - dest->root, dest->dest, dest->destDepth, dest->offset, num_objects); -} - -#else /** * Retype num_objects objects from untyped into type starting from destination slot dest. * @@ -153,6 +142,5 @@ size_bits = vka_get_object_size(type, size_bits); return seL4_Untyped_Retype(untyped->cptr, type, size_bits, dest->root, dest->dest, dest->destDepth, dest->offset, num_objects); } -#endif #endif /* VKA_CAPOPS_H */
diff --git a/libsel4vspace/src/vspace.c b/libsel4vspace/src/vspace.c index ee15e5a..fd5ae50 100644 --- a/libsel4vspace/src/vspace.c +++ b/libsel4vspace/src/vspace.c
@@ -1,3 +1,12 @@ +/* + * Copyright 2016, 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> #include <vspace/vspace.h>