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>
