From 2a70716833b2abc02560f0cbbf060bdd87d170e8 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Tue, 3 Oct 2017 16:20:31 +1100 Subject: [PATCH] libsel4: Make guard and badge definitions mode specific The definitions of guard and badge sizes is going to be changed for 64-bit platforms, this change provides an easy way of providing different definitions --- libsel4/CMakeLists.txt | 1 + libsel4/Makefile | 1 + libsel4/include/sel4/types.h | 4 +--- libsel4/mode_include/32/sel4/mode/types.h | 20 ++++++++++++++++++++ libsel4/mode_include/64/sel4/mode/types.h | 20 ++++++++++++++++++++ 5 files changed, 43 insertions(+), 3 deletions(-) create mode 100644 libsel4/mode_include/32/sel4/mode/types.h create mode 100644 libsel4/mode_include/64/sel4/mode/types.h diff --git a/libsel4/CMakeLists.txt b/libsel4/CMakeLists.txt index e952fd0ac..9abbf0f80 100644 --- a/libsel4/CMakeLists.txt +++ b/libsel4/CMakeLists.txt @@ -71,6 +71,7 @@ set(source_header_dirs "${CMAKE_CURRENT_SOURCE_DIR}/arch_include/${KernelArch}" "${CMAKE_CURRENT_SOURCE_DIR}/sel4_arch_include/${KernelSel4Arch}" "${CMAKE_CURRENT_SOURCE_DIR}/sel4_plat_include/${KernelPlatform}" + "${CMAKE_CURRENT_SOURCE_DIR}/mode_include/${KernelWordSize}" ) # Add the include directory of autoconf.h to the cflags for the bitfield generation diff --git a/libsel4/Makefile b/libsel4/Makefile index a07be35cd..d81dc9848 100644 --- a/libsel4/Makefile +++ b/libsel4/Makefile @@ -51,6 +51,7 @@ HDRFILES := \ $(wildcard $(SOURCE_DIR)/arch_include/$(ARCH)/*) \ $(wildcard $(SOURCE_DIR)/sel4_arch_include/$(SEL4_ARCH)/*) \ $(wildcard $(SOURCE_DIR)/sel4_plat_include/$(PLAT)/*) \ + $(wildcard $(SOURCE_DIR)/mode_include/$(TYPE_SUFFIX)/*) \ $(BUILD_DIR)/include/sel4 \ $(BUILD_DIR)/include/interfaces \ $(BUILD_DIR)/sel4_arch_include/$(SEL4_ARCH)/* diff --git a/libsel4/include/sel4/types.h b/libsel4/include/sel4/types.h index 41d5e95f0..2ff1cf9f9 100644 --- a/libsel4/include/sel4/types.h +++ b/libsel4/include/sel4/types.h @@ -29,11 +29,9 @@ #include #include #include +#include #define seL4_UntypedRetypeMaxObjects 256 -#define seL4_GuardSizeBits 5 -#define seL4_GuardBits 18 -#define seL4_BadgeBits 28 typedef seL4_CPtr seL4_CNode; typedef seL4_CPtr seL4_IRQHandler; diff --git a/libsel4/mode_include/32/sel4/mode/types.h b/libsel4/mode_include/32/sel4/mode/types.h new file mode 100644 index 000000000..e51094f0e --- /dev/null +++ b/libsel4/mode_include/32/sel4/mode/types.h @@ -0,0 +1,20 @@ +/* + * 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) + */ + +#ifndef __LIBSEL4_MODE_TYPES_H +#define __LIBSEL4_MODE_TYPES_H + +#define seL4_GuardSizeBits 5 +#define seL4_GuardBits 18 +#define seL4_BadgeBits 28 + +#endif diff --git a/libsel4/mode_include/64/sel4/mode/types.h b/libsel4/mode_include/64/sel4/mode/types.h new file mode 100644 index 000000000..e51094f0e --- /dev/null +++ b/libsel4/mode_include/64/sel4/mode/types.h @@ -0,0 +1,20 @@ +/* + * 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) + */ + +#ifndef __LIBSEL4_MODE_TYPES_H +#define __LIBSEL4_MODE_TYPES_H + +#define seL4_GuardSizeBits 5 +#define seL4_GuardBits 18 +#define seL4_BadgeBits 28 + +#endif