diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 4d71ee9b..9db5dbf9 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -142,7 +142,7 @@ showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ = ", .is_orig = " ++ is_orig ++ ", .rights = " ++ showRights rights ++ ", .vm_attribs = " ++ - (if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++ + (if cached then "CDL_VM_CacheEnabled" else "CDL_VM_CacheDisabled") ++ ", .mapping_container_id = " ++ (case maybe_mapping of Just (mapping_container, _) -> showObjID objs mapping_container; @@ -220,7 +220,7 @@ showSlots objs obj_id (x:xs) irqNode cdt ms = where index = fst x slot = showCap objs (snd x) irqNode is_orig ms - is_orig = if Map.notMember (obj_id, index) cdt then "true" else "false" + is_orig = if Map.notMember (obj_id, index) cdt then "1" else "0" memberSlots :: Map ObjID Int -> ObjID -> CapMap Word -> IRQMap -> CDT -> ObjMap Word -> String memberSlots objs obj_id slots irqNode cdt ms = @@ -447,7 +447,7 @@ showUntypedDerivations :: AllocationType -> Map ObjID Int -> CoverMap -> String showUntypedDerivations DynamicAlloc{} _ untypedCovers | all null (Map.elems untypedCovers) = ".num_untyped = 0," +++ - ".untyped = NULL," + ".untyped = 0," | otherwise = error $ "refusing to generate spec for dynamic allocation because the " ++ "following untypeds already have children:\n" ++ @@ -500,6 +500,7 @@ printC allocType (Model arch objs irqNode cdt untypedCovers) _ _ = text $ "/* Generated file. Your changes will be overwritten. */" +++ "" +++ + "#define __thread" +++ "#include " +++ "#include " +++ "" +++ diff --git a/capdl-loader-app/CMakeLists.txt b/capdl-loader-app/CMakeLists.txt index ed2d54bb..0ad9ed84 100644 --- a/capdl-loader-app/CMakeLists.txt +++ b/capdl-loader-app/CMakeLists.txt @@ -30,6 +30,14 @@ config_string( UNQUOTE ) +config_string( + CapDLLoaderRootStack + CAPDL_LOADER_ROOT_STACK + "Size of the initial stack for the root task" + DEFAULT + 16384 +) + config_string( CapDLLoaderFillsPerFrame CAPDL_LOADER_FILLS_PER_FRAME @@ -89,16 +97,111 @@ config_option( add_config_library(capdl_loader_app "${configure_string}") -# The capdl-loader-app requires outside configuration in order to build. To achieve this -# we just declare a target here with custom properties for describing the source and headers. -# This is done here as at this point we know the source directory and can construct these things. -# Later on the user will construct a rule for actually generating the capdl executable from a -# different project directory -add_custom_target(capdl_app_properties) -set_property(TARGET capdl_app_properties PROPERTY C_FILES "${CMAKE_CURRENT_SOURCE_DIR}/src/main.c") + +if(DEFINED platform_yaml) + + find_file(PLATFORM_SIFT platform_sift.py PATHS ${CMAKE_MODULE_PATH} NO_CMAKE_FIND_ROOT_PATH) + mark_as_advanced(FORCE PLATFORM_SIFT) + if("${PLATFORM_SIFT}" STREQUAL "PLATFORM_SIFT-NOTFOUND") + message( + FATAL_ERROR + "Failed to find platform_sift.py. Consider using -DPLATFORM_SIFT=/path/to/file" + ) + endif() + + set( + MEMORY_REGIONS + "${CMAKE_BINARY_DIR}/capdl/capdl-loader-app/gen_config/capdl_loader_app/platform_info.h" + ) + add_custom_command( + COMMAND ${PLATFORM_SIFT} --emit-c-syntax ${platform_yaml} > ${MEMORY_REGIONS} + OUTPUT ${MEMORY_REGIONS} + ) + add_custom_target(mem_regions DEPENDS ${platform_yaml} ${PLATFORM_SIFT} ${MEMORY_REGIONS}) + set_property( + SOURCE ${CMAKE_CURRENT_SOURCE_DIR}/capdl/capdl-loader-app/src/main.c + PROPERTY OBJECT_DEPENDS mem_regions + ) +endif() + +get_target_property(MUSL_SOURCE_DIR muslc_gen SOURCE_DIR) + +if(KernelDebugBuild) + set(print_sources + # Debug sources for printing + src/check.c + ${MUSL_SOURCE_DIR}/src/stdio/vfprintf.c + ${MUSL_SOURCE_DIR}/src/stdio/fwrite.c + ${MUSL_SOURCE_DIR}/src/stdio/__towrite.c + ${MUSL_SOURCE_DIR}/src/multibyte/wctomb.c + ${MUSL_SOURCE_DIR}/src/multibyte/wcrtomb.c + ${MUSL_SOURCE_DIR}/src/math/__signbitl.c + ${MUSL_SOURCE_DIR}/src/math/__fpclassifyl.c + ${MUSL_SOURCE_DIR}/src/math/frexpl.c + ${MUSL_SOURCE_DIR}/src/string/strnlen.c + ${MUSL_SOURCE_DIR}/src/string/memchr.c + ) +endif() + + +# Build the application +add_library(capdl_base OBJECT EXCLUDE_FROM_ALL + src/main.c + # Add implementations of memset and memcpy from lib musl + ${MUSL_SOURCE_DIR}/src/string/memset.c + ${MUSL_SOURCE_DIR}/src/string/memcpy.c + + ${print_sources} + ) + +target_include_directories( + capdl_base + PRIVATE + "${CMAKE_CURRENT_SOURCE_DIR}/include" + ${MUSL_SOURCE_DIR}/src/internal + ${MUSL_SOURCE_DIR}/arch/aarch64 +) +target_link_libraries( + capdl_base + PRIVATE + sel4 + cpio + capdl_loader_app_Config + sel4_autoconf + muslc +) + +if(DEFINED platform_yaml) + add_dependencies("capdl_base" mem_regions) +endif() + +separate_arguments( + cmake_c_flags_sep NATIVE_COMMAND "${CMAKE_C_FLAGS}" +) +add_custom_command( + OUTPUT capdl-loader.o + COMMAND + ${CMAKE_C_COMPILER} ${cmake_c_flags_sep} -static -nostdlib -z max-page-size=0x1000 -Wl,-r + $ + $ + -o capdl-loader.o + DEPENDS $ $ COMMAND_EXPAND_LISTS +) + +add_custom_target( + capdl_loader_precompile + DEPENDS capdl-loader.o +) + +add_library(capdl_loader_base STATIC IMPORTED GLOBAL) +set_property(TARGET capdl_loader_base PROPERTY IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/capdl-loader.o") set_property( - TARGET capdl_app_properties + TARGET capdl_loader_base PROPERTY INCLUDE_DIRS "${CMAKE_CURRENT_SOURCE_DIR}/include" + "${MUSL_SOURCE_DIR}/src/internal" + "${MUSL_SOURCE_DIR}/arch/aarch64" ) - -RequireFile(CAPDL_LOADER_BUILD_HELPERS helpers.cmake) +add_library(capdl_loader INTERFACE) +add_dependencies(capdl_loader capdl_loader_base) +set_property(TARGET capdl_loader PROPERTY INTERFACE_LINK_LIBRARIES capdl_loader_base) +target_include_directories(capdl_loader INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}/include") diff --git a/capdl-loader-app/helpers.cmake b/capdl-loader-app/helpers.cmake index d8cbf1da..17031836 100644 --- a/capdl-loader-app/helpers.cmake +++ b/capdl-loader-app/helpers.cmake @@ -26,65 +26,39 @@ function(BuildCapDLApplication) CPIO_SYMBOL _capdl_archive ) + separate_arguments( + cmake_c_flags_sep NATIVE_COMMAND "${CMAKE_C_FLAGS}" + ) - if(DEFINED platform_yaml) - - find_file(PLATFORM_SIFT platform_sift.py PATHS ${CMAKE_MODULE_PATH} NO_CMAKE_FIND_ROOT_PATH) - mark_as_advanced(FORCE PLATFORM_SIFT) - if("${PLATFORM_SIFT}" STREQUAL "PLATFORM_SIFT-NOTFOUND") - message( - FATAL_ERROR - "Failed to find platform_sift.py. Consider using -DPLATFORM_SIFT=/path/to/file" - ) - endif() + add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT}.bin + BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT} + COMMAND_EXPAND_LISTS + COMMAND ${CMAKE_C_COMPILER} ${cmake_c_flags_sep} -static -nostdlib -z max-page-size=0x1000 - set( - MEMORY_REGIONS - "${CMAKE_BINARY_DIR}/capdl/capdl-loader-app/gen_config/capdl_loader_app/platform_info.h" - ) - add_custom_command( - COMMAND ${PLATFORM_SIFT} --emit-c-syntax ${platform_yaml} > ${MEMORY_REGIONS} - OUTPUT ${MEMORY_REGIONS} - ) - add_custom_target(mem_regions DEPENDS ${platform_yaml} ${PLATFORM_SIFT} ${MEMORY_REGIONS}) - set_property( - SOURCE ${CMAKE_CURRENT_SOURCE_DIR}/capdl/capdl-loader-app/src/main.c - PROPERTY OBJECT_DEPENDS mem_regions - ) - endif() - - # Build the application - add_executable( - "${CAPDL_BUILD_APP_OUTPUT}" - EXCLUDE_FROM_ALL - $ - ${CAPDL_LOADER_APP_C_FILES} - ${CAPDL_BUILD_APP_OUTPUT}_archive.o - ${CAPDL_BUILD_APP_C_SPEC} + "-I$,;-I>" + "-I$,;-I>" + "-I$,;-I>" + -I$ + $ + ${CAPDL_BUILD_APP_OUTPUT}_archive.o + ${CAPDL_BUILD_APP_C_SPEC} + -lgcc + -o ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT} + COMMAND cp ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT} ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT}.bin + DEPENDS ${CAPDL_BUILD_APP_OUTPUT}_archive.o capdl_loader $ + "${CAPDL_BUILD_APP_ELF}" + ${CAPDL_BUILD_APP_DEPENDS} ) - if(DEFINED platform_yaml) - add_dependencies("${CAPDL_BUILD_APP_OUTPUT}" mem_regions) - endif() + add_custom_target("${CAPDL_BUILD_APP_OUTPUT}-custom" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT}.bin) - add_dependencies("${CAPDL_BUILD_APP_OUTPUT}" ${CAPDL_BUILD_APP_DEPENDS}) - target_include_directories( - "${CAPDL_BUILD_APP_OUTPUT}" - PRIVATE $ - ) - target_link_libraries( - "${CAPDL_BUILD_APP_OUTPUT}" - sel4runtime - sel4 - cpio - sel4platsupport - sel4utils - capdl_loader_app_Config - sel4_autoconf + add_library("${CAPDL_BUILD_APP_OUTPUT}" STATIC IMPORTED GLOBAL) + add_dependencies("${CAPDL_BUILD_APP_OUTPUT}" "${CAPDL_BUILD_APP_OUTPUT}-custom") + set_property( + TARGET "${CAPDL_BUILD_APP_OUTPUT}" + PROPERTY IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/${CAPDL_BUILD_APP_OUTPUT}" ) - if(KernelDebugBuild) - target_link_libraries("${CAPDL_BUILD_APP_OUTPUT}" sel4muslcsys) - endif() + endfunction(BuildCapDLApplication) # Hook for CAmkES build system. This allows CAmkES projects to diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index 32d46253..e7be7f1f 100644 --- a/capdl-loader-app/include/capdl.h +++ b/capdl-loader-app/include/capdl.h @@ -9,15 +9,29 @@ #include #include -#include -#include -#include -#include -#include -#include +#include -#define CDL_VM_CacheEnabled seL4_ARCH_Default_VMAttributes -#define CDL_VM_CacheDisabled seL4_ARCH_Uncached_VMAttributes +#define BIT(n) (1ul<<(n)) +#define MASK(n) (BIT(n) - 1ul) + +#define PACKED __attribute__((__packed__)) +#define UNUSED __attribute__((__unused__)) + +#if defined(CONFIG_ARCH_ARM) +#define CDL_VM_CacheEnabled seL4_ARM_Default_VMAttributes +#define CDL_VM_CacheDisabled 0 + +#elif defined (CONFIG_ARCH_X86) +#define CDL_VM_CacheEnabled seL4_X86_Default_VMAttributes +#define CDL_VM_CacheDisabled seL4_X86_CacheDisabled + +#elif defined (CONFIG_ARCH_RISCV) +#define CDL_VM_CacheEnabled seL4_RISCV_Default_VMAttributes +#define CDL_VM_CacheDisabled 0 + +#else +#error "Unsupported architecture" +#endif #if defined(CONFIG_ARCH_ARM) @@ -122,17 +136,17 @@ typedef struct { seL4_CPtr mapped_frame_cap; /* This type tag actually has a more specific type, but we force it to be represented as a - * uint8_t to compress the size of this struct in memory. + * seL4_Uint8 to compress the size of this struct in memory. */ - /* CDL_CapType */ uint8_t type; + /* CDL_CapType */ seL4_Uint8 type; /* The following map to more specific seL4 types, but the seL4 types are padded to word size, * wasting space. This padding is necessary for ABI compatibility, but we have no such * requirements here and can instead reduce the in-memory size of specs by packing these fields * into fewer bits. */ - /* seL4_ARCH_VMAttributes */ unsigned vm_attribs: 3; - /* bool */ unsigned is_orig: 1; + /* unsigned */ unsigned vm_attribs: 3; + /* seL4_Bool */ unsigned is_orig: 1; /* seL4_CapRights */ unsigned rights: seL4_CapRightsBits; } PACKED CDL_Cap; @@ -267,10 +281,10 @@ typedef enum { #endif typedef struct { - uint8_t priority; - uint8_t max_priority; - uint8_t affinity; - uint8_t domain; + seL4_Uint8 priority; + seL4_Uint8 max_priority; + seL4_Uint8 affinity; + seL4_Uint8 domain; seL4_Word pc; seL4_Word sp; const char *elf_name; @@ -278,17 +292,17 @@ typedef struct { seL4_Word init_sz; seL4_CPtr fault_ep; seL4_Word ipcbuffer_addr; - bool resume; + seL4_Bool resume; } CDL_TCBExtraInfo; typedef struct { - uint64_t period; - uint64_t budget; + seL4_Uint64 period; + seL4_Uint64 budget; seL4_Word data; } CDL_SCExtraInfo; typedef struct { - uint8_t bank; + seL4_Uint8 bank; } CDL_CBExtraInfo; typedef struct { @@ -328,18 +342,18 @@ typedef enum { typedef struct { CDL_FrameFill_BootInfoEnum_t type; - size_t src_offset; + seL4_Word src_offset; } CDL_FrameFill_BootInfoType_t; typedef struct { char *filename; - size_t file_offset; + seL4_Word file_offset; } CDL_FrameFill_FileDataType_t; typedef struct { CDL_FrameFillType_t type; - size_t dest_offset; - size_t dest_len; + seL4_Word dest_offset; + seL4_Word dest_len; union { CDL_FrameFill_BootInfoType_t bi_type; CDL_FrameFill_FileDataType_t file_data_type; @@ -375,7 +389,7 @@ typedef struct { CDL_ObjectType type; /* The configuration for IO ports on x86 is currently overloaded into the * size_bits parameter. */ - uint32_t size_bits; + seL4_Uint32 size_bits; } PACKED CDL_Object; @@ -433,7 +447,7 @@ static inline CDL_CapData CDL_Cap_Data(CDL_Cap *cap) { return cap->data; } -static inline seL4_ARCH_VMAttributes CDL_Cap_VMAttributes(CDL_Cap *cap) +static inline unsigned CDL_Cap_VMAttributes(CDL_Cap *cap) { return cap->vm_attribs; } @@ -449,7 +463,7 @@ static inline CDL_IRQ CDL_Cap_IRQ(CDL_Cap *cap) { return cap->irq; } -static inline bool CDL_Cap_IsOrig(CDL_Cap *cap) +static inline seL4_Bool CDL_Cap_IsOrig(CDL_Cap *cap) { return cap->is_orig; } @@ -481,7 +495,7 @@ static inline seL4_CapRights_t CDL_seL4_Cap_Rights(CDL_Cap *cap) !!(cap->rights & CDL_CanWrite)); } -static inline uint32_t CONST seL4_CapRights_get_capAllowAllRights(seL4_CapRights_t seL4_CapRights) +static inline seL4_Uint32 CONST seL4_CapRights_get_capAllowAllRights(seL4_CapRights_t seL4_CapRights) { return (seL4_CapRights_get_capAllowRead(seL4_CapRights) && seL4_CapRights_get_capAllowWrite(seL4_CapRights) && @@ -492,7 +506,7 @@ static inline uint32_t CONST seL4_CapRights_get_capAllowAllRights(seL4_CapRights static inline const char *CDL_Obj_Name(CDL_Object *obj) { #ifdef CONFIG_DEBUG_BUILD - if (obj->name == NULL) { + if (obj->name == seL4_Null) { return ""; } else { return obj->name; @@ -537,27 +551,27 @@ static inline seL4_Word CDL_TCB_IPCBuffer_Addr(CDL_Object *obj) return obj->tcb_extra.ipcbuffer_addr; } -static inline uint8_t CDL_TCB_Priority(CDL_Object *obj) +static inline seL4_Uint8 CDL_TCB_Priority(CDL_Object *obj) { return obj->tcb_extra.priority; } -static inline uint8_t CDL_CB_Bank(CDL_Object *obj) +static inline seL4_Uint8 CDL_CB_Bank(CDL_Object *obj) { return obj->cb_extra.bank; } -static inline uint8_t CDL_TCB_MaxPriority(CDL_Object *obj) +static inline seL4_Uint8 CDL_TCB_MaxPriority(CDL_Object *obj) { return obj->tcb_extra.max_priority; } -static inline uint8_t CDL_TCB_Affinity(CDL_Object *obj) +static inline seL4_Uint8 CDL_TCB_Affinity(CDL_Object *obj) { return obj->tcb_extra.affinity; } -static inline uint32_t CDL_TCB_Domain(CDL_Object *obj) +static inline seL4_Uint32 CDL_TCB_Domain(CDL_Object *obj) { return obj->tcb_extra.domain; } @@ -577,12 +591,12 @@ static inline const char *CDL_TCB_ElfName(CDL_Object *obj) return obj->tcb_extra.elf_name; } -static inline uint64_t CDL_SC_Period(CDL_Object *obj) +static inline seL4_Uint64 CDL_SC_Period(CDL_Object *obj) { return obj->sc_extra.period; } -static inline uint64_t CDL_SC_Budget(CDL_Object *obj) +static inline seL4_Uint64 CDL_SC_Budget(CDL_Object *obj) { return obj->sc_extra.budget; } diff --git a/capdl-loader-app/src/check.c b/capdl-loader-app/src/check.c new file mode 100644 index 00000000..e8dbc109 --- /dev/null +++ b/capdl-loader-app/src/check.c @@ -0,0 +1,63 @@ +/* + * Copyright 2023, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include "stdio_impl.h" + +#include + +static size_t sn_write(FILE *f, const unsigned char *s, size_t l) +{ + size_t k = f->wpos - f->wbase; + for (size_t i = 0; i < k; i++) { + seL4_DebugPutChar(f->wbase[i]); + } + size_t t = k; + k = l; + + for (size_t i = 0; i < k; i++) { + seL4_DebugPutChar(s[i]); + } + f->wpos = f->wbase = f->buf; + return t + k; +} + + +int _printf(const char *restrict fmt, ...) +{ + int ret; + va_list ap; + va_start(ap, fmt); + unsigned char buf[1]; + FILE f = { + .lbf = EOF, + .write = sn_write, + .lock = -1, + .buf = buf, + .cookie = NULL, + }; + + ret = vfprintf(&f, fmt, ap); + + va_end(ap); + return ret; +} + + +int __lockfile(FILE *f) { + abort(); +} + +void __unlockfile(FILE *f) { + abort(); +} +_Thread_local int errno; +char *strerror(int e) +{ + abort(); +} + +void __stdio_exit_needed(void){} diff --git a/capdl-loader-app/src/check.h b/capdl-loader-app/src/check.h new file mode 100644 index 00000000..b2f46aa6 --- /dev/null +++ b/capdl-loader-app/src/check.h @@ -0,0 +1,52 @@ +#ifndef CONFIG_DEBUG_BUILD + +#define _printf(...) +#else + +int _printf(const char *restrict fmt, ...); + +#endif /* CONFIG_DEBUG_BUILD */ + +#ifdef NDEBUG +#define assert(x) (void)0 +#else +#define assert(x) ((void)((x) || (__assert_fail(#x, __FILE__, __LINE__, __func__),0))) +#endif + +#define LOG_LEVEL_F 0 +#define LOG_LEVEL_E 1 +#define LOG_LEVEL_W 2 +#define LOG_LEVEL_I 3 +#define LOG_LEVEL_D 4 +#define LOG_LEVEL_V 5 + +#define LOG_LEVEL LOG_LEVEL_V + +#define LOG(lvl, ...) do {if (LOG_LEVEL >= lvl) {_printf(__VA_ARGS__); _printf("\n");}} while(0) +#define LOGF(...) LOG(LOG_LEVEL_F, __VA_ARGS__) +#define LOGE(...) LOG(LOG_LEVEL_E, __VA_ARGS__) +#define LOGW(...) LOG(LOG_LEVEL_W, __VA_ARGS__) +#define LOGI(...) LOG(LOG_LEVEL_I, __VA_ARGS__) +#define LOGD(...) LOG(LOG_LEVEL_D, __VA_ARGS__) +#define LOGV(...) LOG(LOG_LEVEL_V, __VA_ARGS__) + + +#define LOGE_IFERR(err, fmt, ...) \ + if ((err) != seL4_NoError) \ + { LOGE("[Err %d]:\n\t" fmt, err, ## __VA_ARGS__); } + +#define LOGD_IF(cond, fmt, ...) \ + if (cond) { LOGD("[Cond failed: %s]\n\t" fmt, #cond, ## __VA_ARGS__); } + +static inline void ABORT_IF(int predicate, const char *const fmt, ...) { + assert(!predicate); +} + +static inline void ABORT_IFERR(int predicate, const char *const fmt, ...) { + assert(predicate == seL4_NoError); +} + +static inline void ABORT(const char *const fmt, ...) { + assert(0); +} + diff --git a/capdl-loader-app/src/entry.h b/capdl-loader-app/src/entry.h new file mode 100644 index 00000000..31215572 --- /dev/null +++ b/capdl-loader-app/src/entry.h @@ -0,0 +1,140 @@ +/* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + */ + + +/** + * Define entry points for all supported architectures. + * + * _start is used as the entry point symbol. A stack is set + * from an object declared in .bss and then control is jumped to + * main(). + * + */ + +#ifdef CONFIG_ARCH_AARCH64 +__asm__ ( + ".section .text ; " + ".global _start ; " + "_start: ; " + " ldr x19, =__stack_top ; " + " add sp, x19, #0 ; " + " bl main ; " + /* should not return */ + "1: ; " + " b 1b ; " +); + +#elif CONFIG_ARCH_AARCH32 + +__asm__ ( + ".section .text ; " + ".global _start ; " + ".type _start, %function ; " + "_start: ; " + " adr r1, LC2 ; " + " ldr sp, [r1] ;" + " bl main ; " + /* should not return */ + "1: ; " + " b 1b ; " + ".size _start, .-_start ;" + ".type LC2, #object ; " + "LC2: ; " + ".word __stack_top ; " + ".size LC2, . - LC2 ; " + +); + +#elif CONFIG_ARCH_IA32 +__asm__ ( + ".section .text ; " + ".global _start ; " + "_start: ; " + " leal __stack_top, %esp ; " + " mov %esp, %ebp ; " + /* + * GCC expects that a C function is always entered via a call + * instruction and that the stack is 16-byte aligned before such an + * instruction (leaving it 16-byte aligned + 1 word from the + * implicit push when the function is entered). + * + * If additional items are pushed onto the stack, the stack must be + * manually re-aligned before before pushing the arguments for the + * call instruction to main. + */ + " sub $0x8, %esp ; " + " push %ebp ; " + " push %ebx ; " + " call main ; " + + /* should not return */ + "1: ; " + " jmp 1b ; " +); + + +#elif CONFIG_ARCH_X86_64 +__asm__ ( + + ".section .text ; " + ".global _start ; " + "_start: ; " + " leaq __stack_top, %rsp ; " + " movq %rsp, %rbp ; " + /* + * GCC expects that a C function is always entered via a call + * instruction and that the stack is 16-byte aligned before such an + * instruction (leaving it 16-byte aligned + 1 word from the + * implicit push when the function is entered). + * + * If additional items are pushed onto the stack, the stack must be + * manually re-aligned before the call instruction to + * main. + */ + " subq $0x8, %rsp ; " + " push %rbp ; " + " call main ; " + + /* should not return */ + "1: ; " + " jmp 1b ; " +); + +#elif CONFIG_ARCH_RISCV +__asm ( + + ".section .text ; " + ".global _start ; " + "_start: ; " + + /* Set gp for relaxation. See + * https://www.sifive.com/blog/2017/08/28/all-aboard-part-3-linker-relaxation-in-riscv-toolchain/ + */ + ".option push ; " + ".option norelax ; " + "1:auipc gp, %pcrel_hi(__global_pointer$) ; " + " addi gp, gp, %pcrel_lo(1b) ; " + ".option pop ; " + + " la sp, __stack_top ; " + " jal main ; " + /* should not return */ + "1: ; " + " j 1b ; " + + ); + +#else + +#error "Unsupported architecture" +#endif +__asm__ ( + ".section .bss ; " + "__stack_base: ; " + ".align 16 ; " + ".space " CONFIG_CAPDL_LOADER_ROOT_STACK ";" + "__stack_top: ; " + ); diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index e3a5c380..63f0936e 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -4,36 +4,113 @@ * SPDX-License-Identifier: BSD-2-Clause */ -#include -#include - -#include -#include -#include -#include -#include #include -#include -#include -#include -#include +#include +#include +#include +#include +#include -#include -#include +#define __thread #include -#include -#include "capdl.h" +#include -#ifdef CONFIG_DEBUG_BUILD -#include -#include +#include +#ifdef CONFIG_ARCH_ARM +#include #endif +#include "check.h" + +#include "entry.h" +#include "capdl.h" #include "capdl_spec.h" + +#define CHAR_BIT 8 + +/* Evaluate a Kconfig-provided configuration setting at compile-time. */ +#define config_set(macro) _is_set_(macro) +#define _macrotest_1 , +#define _is_set_(value) _is_set__(_macrotest_##value) +#define _is_set__(comma) _is_set___(comma 1, 0) +#define _is_set___(_, v, ...) v + +#define MIN(a,b) (((a)<(b))?(a):(b)) +#define MAX(a,b) (((a)>(b))?(a):(b)) + +#define PAGE_SIZE_4K 4096 +#define ROUND_UP(n, b) \ + ({ typeof (n) _n = (n); \ + typeof (b) _b = (b); \ + (_n + (_n % _b == 0 ? 0 : (_b - (_n % _b)))); \ + }) + #ifdef CONFIG_ARCH_ARM -#include +#define ARCH ARM +#define seL4_ARCH_SmallPageObject seL4_ARM_SmallPageObject +#elif CONFIG_ARCH_X86 +#define ARCH X86 +#define seL4_ARCH_SmallPageObject seL4_X86_4K +#elif CONFIG_ARCH_RISCV +#define ARCH RISCV +#define seL4_ARCH_SmallPageObject seL4_RISCV_4K_Page +#else +#error "Unsupported architecture" +#endif + +#define SEL4_ARCH_DEF_XX(symbol, arch) seL4_##arch##_##symbol +#define SEL4_ARCH_DEF_X(symbol, arch) SEL4_ARCH_DEF_XX(symbol, arch) +#define SEL4_ARCH_DEF(symbol) SEL4_ARCH_DEF_X(symbol, ARCH) + +#define seL4_ARCH_Page_GetAddress_t SEL4_ARCH_DEF(Page_GetAddress_t) +#define seL4_ARCH_Page_Unmap SEL4_ARCH_DEF(Page_Unmap) +#define seL4_ARCH_Page_GetAddress SEL4_ARCH_DEF(Page_GetAddress) +#define seL4_ARCH_ASIDPool_Assign SEL4_ARCH_DEF(ASIDPool_Assign) +#define seL4_ARCH_ASIDControl_MakePool SEL4_ARCH_DEF(ASIDControl_MakePool) +#define seL4_ARCH_VMAttributes SEL4_ARCH_DEF(VMAttributes) +#define seL4_ARCH_Default_VMAttributes SEL4_ARCH_DEF(Default_VMAttributes) +#define seL4_ARCH_PageTable_Map SEL4_ARCH_DEF(PageTable_Map) +#define seL4_ARCH_Page_Map SEL4_ARCH_DEF(Page_Map) + +#ifdef CONFIG_ARCH_AARCH32 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_ARM_SmallPageObject) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_ARM_LargePageObject) \ + X_PAGE_SIZES(seL4_SectionBits, seL4_ARM_SectionObject) \ + X_PAGE_SIZES(seL4_SuperSectionBits, seL4_ARM_SuperSectionObject) + +#elif CONFIG_ARCH_AARCH64 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_ARM_SmallPageObject) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_ARM_LargePageObject) \ + X_PAGE_SIZES(seL4_HugePageBits, seL4_ARM_HugePageObject) +#elif CONFIG_ARCH_IA32 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_X86_4K) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_X86_LargePageObject) + +#elif CONFIG_ARCH_X86_64 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_X86_4K) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_X86_LargePageObject) \ + X_PAGE_SIZES(seL4_HugePageBits, seL4_X64_HugePageObject) + +#elif CONFIG_ARCH_RISCV32 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_RISCV_4K_Page) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_RISCV_Mega_Page) + +#elif CONFIG_ARCH_RISCV64 +#define PAGE_SIZES \ + X_PAGE_SIZES(seL4_PageBits, seL4_RISCV_4K_Page) \ + X_PAGE_SIZES(seL4_LargePageBits, seL4_RISCV_Mega_Page) \ + X_PAGE_SIZES(seL4_HugePageBits, seL4_RISCV_Giga_Page) \ + X_PAGE_SIZES(seL4_TeraPageBits, seL4_RISCV_Tera_Page) + +#else +#error "Unsupported architecture" #endif #ifdef CONFIG_ARCH_RISCV @@ -54,6 +131,8 @@ #define MAX_STREAM_IDS 60 +seL4_IPCBuffer *__sel4_ipc_buffer; + static seL4_CPtr capdl_to_sel4_orig[CONFIG_CAPDL_LOADER_MAX_OBJECTS]; static seL4_CPtr capdl_to_sel4_copy[CONFIG_CAPDL_LOADER_MAX_OBJECTS]; static seL4_CPtr capdl_to_sel4_irq[CONFIG_CAPDL_LOADER_MAX_OBJECTS]; @@ -99,10 +178,71 @@ static seL4_CPtr get_free_slot(void) return free_slot_start; } +char *strcpy(char *dest, const char *src) { + size_t i; + if (!dest) { + return dest; + } + for (i = 0; src && src[i] != 0; i++) { + dest[i] = src[i]; + } + dest[i] = '\0'; + + return dest; +} + +char *strncpy(char *dest, const char *src, size_t n) { + size_t i; + if (!dest) { + return dest; + } + for (i = 0; i < n && src && src[i] != 0; i++) { + dest[i] = src[i]; + } + while (i < n) { + dest[i] = '\0'; + i++; + } + + return dest; + +} + +int raise(int sig) { + abort(); + +} + +_Noreturn void abort(void) { + seL4_TCB_Suspend(seL4_CapInitThreadTCB); + while(1); +} + +_Noreturn void __assert_fail(const char *expr, const char *file, int line, const char *func) +{ + LOGF("Assertion failed: %s (%s: %s: %d)\n", expr, file, func, line); + abort(); +} + +seL4_Word get_frame_object_type(seL4_Word object_size) { + switch (object_size) { + +#define X_PAGE_SIZES(bits, object_type) \ + case bits: \ + return object_type; + + PAGE_SIZES +#undef X_PAGE_SIZES + default: + return -1; + } + +} + static void next_free_slot(void) { free_slot_start++; - ZF_LOGF_IF(free_slot_start >= free_slot_end, "Ran out of free slots!"); + ABORT_IF(free_slot_start >= free_slot_end, "Ran out of free slots!"); } typedef enum {MOVE, COPY} init_cnode_mode; @@ -161,7 +301,7 @@ static seL4_Word get_capData(CDL_CapData d) case CDL_CapData_Raw: return d.data; default: - ZF_LOGF("invalid cap data"); + ABORT("invalid cap data"); return seL4_NilData; } } @@ -185,7 +325,7 @@ static CDL_Cap *get_cdl_frame_pdpt(CDL_ObjID root, uintptr_t vaddr, CDL_Model *s CDL_Object *cdl_pml4 = get_spec_object(spec, root); CDL_Cap *pdpt_cap = get_cap_at(cdl_pml4, PML4_SLOT(vaddr)); if (pdpt_cap == NULL) { - ZF_LOGF("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pml4), (int)PML4_SLOT(vaddr)); + ABORT("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pml4), (int)PML4_SLOT(vaddr)); } return pdpt_cap; } @@ -196,7 +336,7 @@ static CDL_Cap *get_cdl_frame_pd(CDL_ObjID root, uintptr_t vaddr, CDL_Model *spe CDL_Object *cdl_pdpt = get_spec_object(spec, CDL_Cap_ObjID(pdpt_cap)); CDL_Cap *pd_cap = get_cap_at(cdl_pdpt, PDPT_SLOT(vaddr)); if (pd_cap == NULL) { - ZF_LOGF("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pdpt), (int)PDPT_SLOT(vaddr)); + ABORT("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pdpt), (int)PDPT_SLOT(vaddr)); } return pd_cap; } @@ -208,7 +348,7 @@ static CDL_Cap *get_cdl_frame_pud(CDL_ObjID root, uintptr_t vaddr, CDL_Model *sp CDL_Object *cdl_pgd = get_spec_object(spec, root); CDL_Cap *pud_cap = get_cap_at(cdl_pgd, PGD_SLOT(vaddr)); if (pud_cap == NULL) { - ZF_LOGF("Could not find PUD cap %s[%d]", CDL_Obj_Name(cdl_pgd), (int)PGD_SLOT(vaddr)); + ABORT("Could not find PUD cap %s[%d]", CDL_Obj_Name(cdl_pgd), (int)PGD_SLOT(vaddr)); } return pud_cap; } @@ -223,7 +363,7 @@ static CDL_Cap *get_cdl_frame_pd(CDL_ObjID root, uintptr_t vaddr, CDL_Model *spe #endif CDL_Cap *pd_cap = get_cap_at(cdl_pud, PUD_SLOT(vaddr)); if (pd_cap == NULL) { - ZF_LOGF("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pud), (int)PUD_SLOT(vaddr)); + ABORT("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pud), (int)PUD_SLOT(vaddr)); } return pd_cap; } @@ -240,7 +380,7 @@ static CDL_Cap *get_cdl_frame_pt(CDL_ObjID pd, uintptr_t vaddr, CDL_Model *spec) #endif CDL_Cap *pt_cap = get_cap_at(cdl_pd, PD_SLOT(vaddr)); if (pt_cap == NULL) { - ZF_LOGF("Could not find PT cap %s[%d]", CDL_Obj_Name(cdl_pd), (int)PD_SLOT(vaddr)); + ABORT("Could not find PT cap %s[%d]", CDL_Obj_Name(cdl_pd), (int)PD_SLOT(vaddr)); } return pt_cap; } @@ -264,7 +404,7 @@ static CDL_Cap *get_cdl_frame_pt_recurse(CDL_ObjID root, uintptr_t vaddr, CDL_Mo } CDL_Cap *pt_cap_ret = get_cap_at(cdl_pt, PT_LEVEL_SLOT(vaddr, level)); if (pt_cap_ret == NULL) { - ZF_LOGF("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pt), (int)PT_LEVEL_SLOT(vaddr, level)); + ABORT("Could not find PD cap %s[%d]", CDL_Obj_Name(cdl_pt), (int)PT_LEVEL_SLOT(vaddr, level)); } return pt_cap_ret; } @@ -288,7 +428,7 @@ static CDL_Cap *get_cdl_frame_cap(CDL_ObjID pd, uintptr_t vaddr, CDL_Model *spec CDL_Object *cdl_pt = get_spec_object(spec, CDL_Cap_ObjID(pt_cap)); CDL_Cap *frame_cap = get_cap_at(cdl_pt, PT_SLOT(vaddr)); if (frame_cap == NULL) { - ZF_LOGF("Could not find frame cap %s[%d]", CDL_Obj_Name(cdl_pt), (int)PT_SLOT(vaddr)); + ABORT("Could not find frame cap %s[%d]", CDL_Obj_Name(cdl_pt), (int)PT_SLOT(vaddr)); } return frame_cap; @@ -322,7 +462,7 @@ void init_copy_frame(seL4_BootInfo *bootinfo) (uintptr_t)&__executable_start) / PAGE_SIZE_4K; if (num_user_image_frames_reported < num_user_image_frames_measured) { - ZF_LOGE("Too few frames caps in bootinfo to back user image"); + LOGE("Too few frames caps in bootinfo to back user image"); return; } @@ -330,7 +470,7 @@ void init_copy_frame(seL4_BootInfo *bootinfo) (num_user_image_frames_reported - num_user_image_frames_measured) * PAGE_SIZE_4K; if (additional_user_image_bytes > (uintptr_t)&__executable_start) { - ZF_LOGE("User image padding too high to fit before start symbol"); + LOGE("User image padding too high to fit before start symbol"); return; } @@ -359,7 +499,7 @@ void init_copy_frame(seL4_BootInfo *bootinfo) for (int i = 0; i < sizeof(copy_addr_with_pt) / PAGE_SIZE_4K; i++) { error = seL4_ARCH_Page_Unmap(copy_addr_frame + i); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } @@ -375,7 +515,7 @@ static unsigned int sort_untypeds(seL4_BootInfo *bootinfo) seL4_CPtr untyped_start = bootinfo->untyped.start; seL4_CPtr untyped_end = bootinfo->untyped.end; - ZF_LOGD("Sorting untypeds..."); + LOGD("Sorting untypeds..."); seL4_Word count[CONFIG_WORD_SIZE] = {0}; @@ -399,12 +539,12 @@ static unsigned int sort_untypeds(seL4_BootInfo *bootinfo) // Store untypeds in untyped_cptrs array. for (seL4_Word untyped_index = 0; untyped_index != untyped_end - untyped_start; untyped_index++) { if (bootinfo->untypedList[untyped_index].isDevice) { - ZF_LOGD("Untyped %3d (cptr=%p) (addr=%p) is of size %2d. Skipping as it is device", + LOGD("Untyped %3d (cptr=%p) (addr=%p) is of size %2d. Skipping as it is device", untyped_index, (void *)(untyped_start + untyped_index), (void *)bootinfo->untypedList[untyped_index].paddr, bootinfo->untypedList[untyped_index].sizeBits); } else { - ZF_LOGD("Untyped %3d (cptr=%p) (addr=%p) is of size %2d. Placing in slot %d...", + LOGD("Untyped %3d (cptr=%p) (addr=%p) is of size %2d. Placing in slot %d...", untyped_index, (void *)(untyped_start + untyped_index), (void *)bootinfo->untypedList[untyped_index].paddr, bootinfo->untypedList[untyped_index].sizeBits, @@ -422,7 +562,7 @@ static unsigned int sort_untypeds(seL4_BootInfo *bootinfo) static void parse_bootinfo(seL4_BootInfo *bootinfo, CDL_Model *spec) { - ZF_LOGD("Parsing bootinfo..."); + LOGD("Parsing bootinfo..."); free_slot_start = bootinfo->empty.start; free_slot_end = bootinfo->empty.end; @@ -435,7 +575,7 @@ static void parse_bootinfo(seL4_BootInfo *bootinfo, CDL_Model *spec) */ free_slot_start += 16; - ZF_LOGD(" %ld free cap slots, from %ld to %ld", + LOGD(" %ld free cap slots, from %ld to %ld", (long)(free_slot_end - free_slot_start), (long)free_slot_start, (long)free_slot_end); @@ -464,7 +604,7 @@ static void parse_bootinfo(seL4_BootInfo *bootinfo, CDL_Model *spec) seL4_Word ut_paddr = bootinfo->untypedList[i].paddr; if (bootinfo->untypedList[i].paddr == ut->paddr) { seL4_Uint8 ut_size = bootinfo->untypedList[i].sizeBits; - ZF_LOGF_IF(ut_size != ut->size_bits, + ABORT_IF(ut_size != ut->size_bits, "Ut at %p in incorrect size, expected %u got %u", ut->paddr, ut->size_bits, ut_size); untyped_cptrs[u] = bootinfo->untyped.start + i; @@ -474,26 +614,26 @@ static void parse_bootinfo(seL4_BootInfo *bootinfo, CDL_Model *spec) } } } - ZF_LOGF_IF(!found, "Failed to find ut for %p", ut->paddr); + ABORT_IF(!found, "Failed to find ut for %p", ut->paddr); } #else /* Probably an inconsistency in the build configuration, so fail now. */ - ZF_LOGF_IF(spec->num_untyped, "spec has static alloc, but loader is compiled for dynamic"); + ABORT_IF(spec->num_untyped, "spec has static alloc, but loader is compiled for dynamic"); #endif #if CONFIG_CAPDL_LOADER_PRINT_UNTYPEDS int num_untyped = bootinfo->untyped.end - bootinfo->untyped.start; - ZF_LOGD(" Untyped memory (%d)", num_untyped); + LOGD(" Untyped memory (%d)", num_untyped); for (int i = 0; i < num_untyped; i++) { uintptr_t ut_paddr = bootinfo->untypedList[i].paddr; uintptr_t ut_size = bootinfo->untypedList[i].sizeBits; bool ut_isDevice = bootinfo->untypedList[i].isDevice; - ZF_LOGD(" 0x%016" PRIxPTR " - 0x%016" PRIxPTR " (%s)", ut_paddr, + LOGD(" 0x%016" PRIxPTR " - 0x%016" PRIxPTR " (%s)", ut_paddr, ut_paddr + BIT(ut_size), ut_isDevice ? "device" : "memory"); } #endif - ZF_LOGD("Loader is running in domain %d", bootinfo->initThreadDomain); + LOGD("Loader is running in domain %d", bootinfo->initThreadDomain); first_arm_iospace = bootinfo->ioSpaceCaps.start; } @@ -516,7 +656,7 @@ static int find_device_object(seL4_Word paddr, seL4_Word type, int size_bits, se /* Attempt to copy the cap */ error = seL4_CNode_Copy(seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE, seL4_CapInitThreadCNode, orig_caps(prev), CONFIG_WORD_SIZE, seL4_AllRights); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); return 0; } } @@ -536,41 +676,41 @@ static int find_device_object(seL4_Word paddr, seL4_Word type, int size_bits, se while (1) { error = seL4_Untyped_Retype(bootinfo->untyped.start + i, type, size_bits, seL4_CapInitThreadCNode, 0, 0, free_slot, 1); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); seL4_ARCH_Page_GetAddress_t addr; if (type == seL4_UntypedObject) { /* if it's an untyped, create a temporary frame in it * to get the address from */ - error = seL4_Untyped_Retype(free_slot, arch_kobject_get_type(KOBJECT_FRAME, seL4_PageBits), seL4_PageBits, + error = seL4_Untyped_Retype(free_slot, seL4_ARCH_SmallPageObject, seL4_PageBits, seL4_CapInitThreadCNode, 0, 0, free_slot + 2, 1); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); addr = seL4_ARCH_Page_GetAddress(free_slot + 2); error = seL4_CNode_Delete(seL4_CapInitThreadCNode, free_slot + 2, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { addr = seL4_ARCH_Page_GetAddress(free_slot); } - ZF_LOGF_IFERR(addr.error, "Could not get address for untyped cap."); + ABORT_IFERR(addr.error, "Could not get address for untyped cap."); if (addr.paddr == (uintptr_t)paddr) { /* nailed it */ /* delete any holding cap */ if (hold_slot) { error = seL4_CNode_Delete(seL4_CapInitThreadCNode, hold_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } return 0; } - ZF_LOGF_IF(addr.paddr > (uintptr_t)paddr, "device frames probably not ordered by physical address"); + ABORT_IF(addr.paddr > (uintptr_t)paddr, "device frames probably not ordered by physical address"); /* if we are currently using a hold slot we can just delete the cap, otherwise start the hold */ if (hold_slot) { error = seL4_CNode_Delete(seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { hold_slot = free_slot + 1; error = seL4_CNode_Move(seL4_CapInitThreadCNode, hold_slot, CONFIG_WORD_SIZE, seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } } @@ -595,7 +735,7 @@ static int retype_untyped(seL4_CPtr free_slot, seL4_CPtr free_untyped, int no_objects = 1; - ZF_LOGF_IF(object_type >= seL4_ObjectTypeCount, + ABORT_IF(object_type >= seL4_ObjectTypeCount, "Invalid object type %zu size %zu", (size_t) object_type, (size_t) object_size); @@ -612,7 +752,7 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ switch (CDL_Obj_Type(obj)) { case CDL_Frame: - obj_type = kobject_get_type(KOBJECT_FRAME, obj_size); + obj_type = get_frame_object_type(obj_size); break; case CDL_ASIDPool: obj_type = CDL_Untyped; @@ -620,7 +760,7 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ break; #ifdef CONFIG_KERNEL_MCS case CDL_SchedContext: - obj_size = kobject_get_size(KOBJECT_SCHED_CONTEXT, obj_size); + obj_size = obj_size > seL4_MinSchedContextBits ? obj_size : seL4_MinSchedContextBits; obj_type = (seL4_ArchObjectType) CDL_Obj_Type(obj); break; #endif @@ -628,7 +768,7 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ obj_type = (seL4_ArchObjectType) CDL_Obj_Type(obj); } - ZF_LOGD_IF(CDL_Obj_Type(obj) == CDL_CNode, " (CNode of size %d bits)", obj_size); + LOGD_IF(CDL_Obj_Type(obj) == CDL_CNode, " (CNode of size %d bits)", obj_size); seL4_Error err = seL4_NoError; @@ -636,7 +776,7 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ if (CDL_Obj_Type(obj) == CDL_IOPorts) { err = seL4_X86_IOPortControl_Issue(seL4_CapIOPortControl, obj->start, obj->end, seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate IOPort for range [%d,%d]", (int)obj->start, (int)obj->end); + ABORT_IF(err != seL4_NoError, "Failed to allocate IOPort for range [%d,%d]", (int)obj->start, (int)obj->end); return seL4_NoError; } #endif @@ -650,14 +790,14 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ if (CDL_Obj_Type(obj) == CDL_SID) { err = seL4_ARM_SIDControl_GetSID(seL4_CapSMMUSIDControl, sid_number, seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate SID cap"); + ABORT_IF(err != seL4_NoError, "Failed to allocate SID cap"); sid_number++; - ZF_LOGF_IF(sid_number > MAX_STREAM_IDS, "Stream ID numbers exhausted"); + ABORT_IF(sid_number > MAX_STREAM_IDS, "Stream ID numbers exhausted"); return seL4_NoError; } else if (CDL_Obj_Type(obj) == CDL_CB) { err = seL4_ARM_CBControl_GetCB(seL4_CapSMMUCBControl, CDL_CB_Bank(obj), seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate CB cap"); + ABORT_IF(err != seL4_NoError, "Failed to allocate CB cap"); sid_number = 0; //(1***) return seL4_NoError; } @@ -672,11 +812,11 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ #if !CONFIG_CAPDL_LOADER_STATIC_ALLOC if (isDeviceObject(obj)) { seL4_Word paddr = CDL_Obj_Paddr(obj); - ZF_LOGD(" device frame/untyped, paddr = %p, size = %d bits", (void *) paddr, obj_size); + LOGD(" device frame/untyped, paddr = %p, size = %d bits", (void *) paddr, obj_size); /* This is a device object. Look for it in bootinfo. */ err = find_device_object(paddr, obj_type, obj_size, free_slot, id, info, spec); - ZF_LOGF_IF(err != seL4_NoError, "Failed to find device frame/untyped at paddr = %p", (void *) paddr); + ABORT_IF(err != seL4_NoError, "Failed to find device frame/untyped at paddr = %p", (void *) paddr); return seL4_NoError; } #endif @@ -712,7 +852,7 @@ static int requires_creation(CDL_ObjectType type) */ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) { - ZF_LOGD("Creating objects..."); + LOGD("Creating objects..."); unsigned int free_slot_index = 0; @@ -728,10 +868,10 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) CDL_Object *obj = &spec->objects[obj_id]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); - ZF_LOGV("Creating object %s in slot %ld, from untyped %lx...", + LOGV("Creating object %s in slot %ld, from untyped %lx...", CDL_Obj_Name(obj), (long)free_slot, (long)untyped_cptr); - ZF_LOGF_IF(!requires_creation(capdl_obj_type), + ABORT_IF(!requires_creation(capdl_obj_type), "object %s is in static allocation, but requires_creation is false", CDL_Obj_Name(obj)); seL4_Error err = create_object(spec, obj, obj_id, bootinfo, untyped_cptr, free_slot); @@ -740,7 +880,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) free_slot_index++; } else { /* Exit with failure. */ - ZF_LOGF_IFERR(err, "Untyped retype failed with unexpected error"); + ABORT_IFERR(err, "Untyped retype failed with unexpected error"); } } } @@ -750,7 +890,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) inside the kernel's ASID table, which ensures consistency with verification models. */ if (spec->num_asid_slots > 1) { - ZF_LOGD("Creating ASID pools..."); + LOGD("Creating ASID pools..."); } for (seL4_Word asid_high = 1; asid_high < spec->num_asid_slots; asid_high++) { CDL_ObjID obj_id = spec->asid_slots[asid_high]; @@ -760,7 +900,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) seL4_Error err = seL4_ARCH_ASIDControl_MakePool(seL4_CapASIDControl, asidpool_ut, seL4_CapInitThreadCNode, asidpool_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(err, "Failed to create ASID pool #%d from ut slot %ld into slot %ld", + ABORT_IFERR(err, "Failed to create ASID pool #%d from ut slot %ld into slot %ld", (int)asid_high, (long)asidpool_ut, (long)asidpool_slot); // update to point to our new ASID pool @@ -786,7 +926,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) /* Sort untypeds from largest to smallest. */ unsigned int num_normal_untypes = sort_untypeds(bootinfo); - ZF_LOGD("Creating objects..."); + LOGD("Creating objects..."); /* First, allocate most objects and update the spec database with the cslot locations. The exception is ASIDPools, where @@ -807,8 +947,8 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) CDL_Object *obj = &spec->objects[obj_id_index]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); - ZF_LOGV("Creating object %s in slot %ld, from untyped %lx...", CDL_Obj_Name(obj), (long)free_slot, - (long)untyped_cptr); + LOGV("Creating object %s in slot %ld, from untyped %lx...", CDL_Obj_Name(obj), (long)free_slot, + (long)untyped_cptr); if (requires_creation(capdl_obj_type)) { /* at this point we are definitely creating an object - figure out what it is */ @@ -823,7 +963,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) obj_id_index--; } else { /* Exit with failure. */ - ZF_LOGF_IFERR(err, "Untyped retype failed with unexpected error"); + ABORT_IFERR(err, "Untyped retype failed with unexpected error"); } } obj_id_index++; @@ -831,7 +971,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) if (obj_id_index != spec->num) { /* We didn't iterate through all the objects. */ - ZF_LOGF("Ran out of untyped memory while creating objects."); + ABORT("Ran out of untyped memory while creating objects."); } /* Now, we turn the backing untypeds into ASID pools, in the order @@ -839,7 +979,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) inside the kernel's ASID table, which ensures consistency with verification models. */ if (spec->num_asid_slots > 1) { - ZF_LOGD("Creating ASID pools..."); + LOGD("Creating ASID pools..."); } for (seL4_Word asid_high = 1; asid_high < spec->num_asid_slots; asid_high++) { CDL_ObjID obj_id = spec->asid_slots[asid_high]; @@ -849,7 +989,7 @@ static void create_objects(CDL_Model *spec, seL4_BootInfo *bootinfo) seL4_Error err = seL4_ARCH_ASIDControl_MakePool(seL4_CapASIDControl, asid_ut, seL4_CapInitThreadCNode, asid_slot, CONFIG_WORD_SIZE); - ZF_LOGF_IFERR(err, "Failed to create asid pool"); + ABORT_IFERR(err, "Failed to create asid pool"); // update to point to our new ASID pool add_sel4_cap(obj_id, ORIG, asid_slot); @@ -896,19 +1036,19 @@ static void create_irq_cap(CDL_IRQ irq, CDL_Object *obj, seL4_CPtr free_slot) default: error = seL4_IRQControl_Get(seL4_CapIRQControl, irq, root, index, depth); } - ZF_LOGF_IFERR(error, "Failed to create irq cap"); + ABORT_IFERR(error, "Failed to create irq cap"); add_sel4_cap(irq, IRQ, index); } static void create_irq_caps(CDL_Model *spec) { - ZF_LOGD("Creating irq handler caps..."); + LOGD("Creating irq handler caps..."); for (CDL_IRQ irq = 0; irq < spec->num_irqs; irq++) { if (spec->irqs[irq] != INVALID_OBJ_ID) { seL4_CPtr free_slot = get_free_slot(); - ZF_LOGD(" Creating irq handler cap for IRQ %d...", irq); + LOGD(" Creating irq handler cap for IRQ %d...", irq); create_irq_cap(irq, &spec->objects[spec->irqs[irq]], free_slot); next_free_slot(); } @@ -930,7 +1070,7 @@ static void mint_cap(CDL_ObjID object_id, int free_slot, seL4_Word badge, seL4_C int error = seL4_CNode_Mint(dest_root, dest_index, dest_depth, src_root, src_index, src_depth, rights, badge); - ZF_LOGF_IF(error, "Failed to mint cap"); + ABORT_IF(error, "Failed to mint cap"); } /* Duplicate capabilities */ @@ -948,17 +1088,17 @@ static void duplicate_cap(CDL_ObjID object_id, int free_slot) int error = seL4_CNode_Copy(dest_root, dest_index, dest_depth, src_root, src_index, src_depth, rights); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); add_sel4_cap(object_id, DUP, dest_index); } static void duplicate_caps(CDL_Model *spec) { - ZF_LOGD("Duplicating CNodes..."); + LOGD("Duplicating CNodes..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_CNode || spec->objects[obj_id].type == CDL_TCB) { - ZF_LOGD(" Duplicating %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Duplicating %s...", CDL_Obj_Name(&spec->objects[obj_id])); int free_slot = get_free_slot(); duplicate_cap(obj_id, free_slot); next_free_slot(); @@ -984,7 +1124,7 @@ static void init_sc(CDL_Model *spec, CDL_ObjID sc, CDL_Core affinity) uint64_t UNUSED period = CDL_SC_Period(cdl_sc); seL4_Word UNUSED data = CDL_SC_Data(cdl_sc); - ZF_LOGD("budget: %llu, period: %llu, data: %u", budget, period, data); + LOGD("budget: %llu, period: %llu, data: %u", budget, period, data); seL4_CPtr UNUSED seL4_sc = orig_caps(sc); seL4_CPtr UNUSED sched_control = sched_ctrl_caps(affinity); @@ -992,7 +1132,7 @@ static void init_sc(CDL_Model *spec, CDL_ObjID sc, CDL_Core affinity) /* Assign the sched context to run on the CPU that the root task runs on. */ int error = seL4_SchedControl_Configure(sched_control, seL4_sc, budget, period, 0, data); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); #endif } @@ -1003,15 +1143,15 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) CDL_Cap *cdl_cspace_root = get_cap_at(cdl_tcb, CDL_TCB_CTable_Slot); if (cdl_cspace_root == NULL) { - ZF_LOGD("Could not find CSpace cap for %s", CDL_Obj_Name(cdl_tcb)); + LOGD("Could not find CSpace cap for %s", CDL_Obj_Name(cdl_tcb)); } CDL_Cap *cdl_vspace_root = get_cap_at(cdl_tcb, CDL_TCB_VTable_Slot); if (cdl_vspace_root == NULL) { - ZF_LOGD("Could not find VSpace cap for %s", CDL_Obj_Name(cdl_tcb)); + LOGD("Could not find VSpace cap for %s", CDL_Obj_Name(cdl_tcb)); } CDL_Cap *cdl_ipcbuffer = get_cap_at(cdl_tcb, CDL_TCB_IPCBuffer_Slot); if (cdl_ipcbuffer == NULL) { - ZF_LOGD(" Warning: TCB has no IPC buffer"); + LOGD(" Warning: TCB has no IPC buffer"); } #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX) CDL_Cap *cdl_vcpu = get_cap_at(cdl_tcb, CDL_TCB_VCPU_SLOT); @@ -1043,12 +1183,12 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) CDL_Cap *cdl_fault_ep = get_cap_at(cdl_tcb, CDL_TCB_FaultEP_Slot); if (cdl_fault_ep == NULL) { - ZF_LOGW(" Warning: TCB has no fault endpoint"); + LOGW(" Warning: TCB has no fault endpoint"); } CDL_Cap *cdl_tempfault_ep = get_cap_at(cdl_tcb, CDL_TCB_TemporalFaultEP_Slot); if (cdl_tempfault_ep == NULL) { - ZF_LOGW(" Warning: TCB has no temporal fault endpoint"); + LOGW(" Warning: TCB has no temporal fault endpoint"); } sel4_fault_ep = cdl_fault_ep ? orig_caps(CDL_Cap_ObjID(cdl_fault_ep)) : 0; @@ -1098,21 +1238,21 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) sel4_cspace_root, sel4_cspace_root_data, sel4_vspace_root, sel4_vspace_root_data, ipcbuffer_addr, sel4_ipcbuffer); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { - ZF_LOGE_IFERR(cdl_cspace_root || cdl_vspace_root || sel4_ipcbuffer, + LOGE_IFERR(cdl_cspace_root || cdl_vspace_root || sel4_ipcbuffer, "Could not call seL4_TCB_Configure as not all required objects provided: " "VSpace: %p, CSpace: %p, IPC Buffer: %"SEL4_PRIx_word, cdl_vspace_root, cdl_cspace_root, sel4_ipcbuffer); if (sel4_ipcbuffer) { error = seL4_TCB_SetIPCBuffer(sel4_tcb, ipcbuffer_addr, sel4_ipcbuffer); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } error = seL4_TCB_SetSchedParams(sel4_tcb, seL4_CapInitThreadTCB, max_priority, priority, sel4_sc, sel4_fault_ep); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); error = seL4_TCB_SetTimeoutEndpoint(sel4_tcb, sel4_tempfault_ep); #else @@ -1121,21 +1261,21 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) sel4_cspace_root, sel4_cspace_root_data, sel4_vspace_root, sel4_vspace_root_data, ipcbuffer_addr, sel4_ipcbuffer); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { - ZF_LOGE_IFERR(cdl_cspace_root || cdl_vspace_root || sel4_ipcbuffer, + LOGE_IFERR(cdl_cspace_root || cdl_vspace_root || sel4_ipcbuffer, "Could not call seL4_TCB_Configure as not all required objects provided: " "VSpace: %p, CSpace: %p, IPC Buffer: %"SEL4_PRIx_word, cdl_vspace_root, cdl_cspace_root, sel4_ipcbuffer); if (sel4_ipcbuffer) { error = seL4_TCB_SetIPCBuffer(sel4_tcb, ipcbuffer_addr, sel4_ipcbuffer); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } error = seL4_TCB_SetSchedParams(sel4_tcb, seL4_CapInitThreadTCB, max_priority, priority); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); #if CONFIG_MAX_NUM_NODES > 1 error = seL4_TCB_SetAffinity(sel4_tcb, affinity); @@ -1143,7 +1283,7 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) #endif - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX) if (sel4_vcpu) { @@ -1152,7 +1292,7 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb) #else //CONFIG_VTX int error = seL4_X86_VCPU_SetTCB(sel4_vcpu, sel4_tcb); #endif - ZF_LOGF_IFERR(error, "Failed to bind TCB %s to VCPU %s", + ABORT_IFERR(error, "Failed to bind TCB %s to VCPU %s", CDL_Obj_Name(cdl_tcb), CDL_Obj_Name(get_spec_object(spec, CDL_Cap_ObjID(cdl_vcpu)))); } #endif @@ -1183,7 +1323,7 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) uintptr_t sp = CDL_TCB_SP(cdl_tcb); if (sp % (sizeof(uintptr_t) * 2) != 0) { - ZF_LOGF("TCB %s's stack pointer is not dword-aligned", CDL_Obj_Name(&spec->objects[tcb])); + ABORT("TCB %s's stack pointer is not dword-aligned", CDL_Obj_Name(&spec->objects[tcb])); } int reg_args = 0; #if defined(CONFIG_ARCH_ARM) @@ -1202,7 +1342,7 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) if (argc > reg_args) { #ifdef CONFIG_CAPDL_LOADER_CC_REGISTERS - ZF_LOGF("TCB %s has more than four arguments, which is not supported using" + ABORT("TCB %s has more than four arguments, which is not supported using" " the register calling convention", CDL_Obj_Name(&spec->objects[tcb])); #else //!CONFIG_CAPDL_LOADER_CC_REGISTERS /* We need to map the TCB's stack into our address space because there @@ -1214,7 +1354,7 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) CDL_ObjID pd = CDL_Cap_ObjID(cdl_vspace_root); if (STACK_ALIGNMENT_BYTES % sizeof(*argv)) { - ZF_LOGF("Stack alignment requirement not evenly divisible by argument size"); + ABORT("Stack alignment requirement not evenly divisible by argument size"); } /* The stack pointer of new threads will initially be aligned to @@ -1246,7 +1386,7 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) #endif int error = seL4_ARCH_Page_Map(frame, seL4_CapInitThreadPD, (seL4_Word)copy_addr_with_pt, seL4_ReadWrite, attribs); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); /* Write all necessary arguments to the TCB's stack. */ for (int i = argc - 1; i >= 0 && i >= reg_args; i--) { @@ -1254,7 +1394,7 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) /* We could support this case with more complicated logic, but * choose not to. */ - ZF_LOGF("TCB %s's initial arguments cause its stack to cross a page boundary", + ABORT("TCB %s's initial arguments cause its stack to cross a page boundary", CDL_Obj_Name(&spec->objects[tcb])); } sp -= sizeof(seL4_Word); @@ -1263,10 +1403,10 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) #ifdef CONFIG_ARCH_ARM error = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); #endif //CONFIG_ARCH_ARM error = seL4_ARCH_Page_Unmap(frame); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); #endif //CONFIG_CAPDL_LOADER_CC_REGISTERS } @@ -1310,11 +1450,11 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) .a3 = argc > 3 ? argv[3] : 0, #endif }; - ZF_LOGD(" Setting up _start()"); - ZF_LOGD(" pc = %p", (void *)pc); - ZF_LOGD(" sp = %p", (void *)sp); + LOGD(" Setting up _start()"); + LOGD(" pc = %p", (void *)pc); + LOGD(" sp = %p", (void *)sp); for (int i = 0; i < argc; i++) { - ZF_LOGD(" arg%d = %p", i, (void *)argv[i]); + LOGD(" arg%d = %p", i, (void *)argv[i]); } global_user_context = regs; @@ -1322,23 +1462,23 @@ static void configure_tcb(CDL_Model *spec, CDL_ObjID tcb) int error = seL4_TCB_WriteRegisters(sel4_tcb, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &global_user_context); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); uint32_t UNUSED domain = CDL_TCB_Domain(cdl_tcb); - ZF_LOGD(" Assigning thread to domain %u...", domain); + LOGD(" Assigning thread to domain %u...", domain); error = seL4_DomainSet_Set(seL4_CapDomain, domain, sel4_tcb); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } static void init_tcbs(CDL_Model *spec) { - ZF_LOGD("Initialising TCBs..."); + LOGD("Initialising TCBs..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_TCB) { - ZF_LOGD(" Initialising %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Initialising %s...", CDL_Obj_Name(&spec->objects[obj_id])); init_tcb(spec, obj_id); - ZF_LOGD(" Configuring %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Configuring %s...", CDL_Obj_Name(&spec->objects[obj_id])); configure_tcb(spec, obj_id); } } @@ -1361,10 +1501,10 @@ static void init_irq(CDL_Model *spec, CDL_IRQ irq_no) #endif if (cdl_irq->size_bits != 0) { - ZF_LOGF("Misconfigured IRQ; an IRQ must have a size of 0."); + ABORT("Misconfigured IRQ; an IRQ must have a size of 0."); } if (cdl_irq->slots.num > 1) { - ZF_LOGF("Misconfigured IRQ; an IRQ cannot have more than one assigned endpoint."); + ABORT("Misconfigured IRQ; an IRQ cannot have more than one assigned endpoint."); } if (cdl_irq->slots.num == 1) { @@ -1382,17 +1522,17 @@ static void init_irq(CDL_Model *spec, CDL_IRQ irq_no) } int error = seL4_IRQHandler_SetNotification(irq_handler_cap, endpoint_cptr); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } static void init_irqs(CDL_Model *spec) { - ZF_LOGD("Initialising IRQ handler caps..."); + LOGD("Initialising IRQ handler caps..."); for (CDL_IRQ irq = 0; irq < spec->num_irqs; irq++) { if (spec->irqs[irq] != INVALID_OBJ_ID) { - ZF_LOGD(" Initialising handler for IRQ %d...", irq); + LOGD(" Initialising handler for IRQ %d...", irq); init_irq(spec, irq); } } @@ -1403,17 +1543,17 @@ static void set_asid(CDL_Model *spec UNUSED, CDL_ObjID page) { seL4_CPtr sel4_page = orig_caps(page); int error = seL4_ARCH_ASIDPool_Assign(seL4_CapInitThreadASIDPool, sel4_page); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } static void init_pd_asids(CDL_Model *spec) { - ZF_LOGD("Initialising Page Directory ASIDs..."); + LOGD("Initialising Page Directory ASIDs..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { CDL_ObjectType type = CDL_TOP_LEVEL_PD; if (spec->objects[obj_id].type == type) { - ZF_LOGD(" Initialising pd/pml4 ASID %s...", + LOGD(" Initialising pd/pml4 ASID %s...", CDL_Obj_Name(&spec->objects[obj_id])); set_asid(spec, obj_id); } @@ -1435,7 +1575,7 @@ static void map_page(CDL_Model *spec UNUSED, CDL_Cap *page_cap, CDL_ObjID pd_id, } #endif seL4_ARCH_VMAttributes vm_attribs = CDL_Cap_VMAttributes(page_cap); - ZF_LOGD(" Mapping %s into %s with rights={G: %d, R: %d, W: %d}, vaddr=0x%x, vm_attribs=0x%x", + LOGD(" Mapping %s into %s with rights={G: %d, R: %d, W: %d}, vaddr=0x%x, vm_attribs=0x%x", CDL_Obj_Name(&spec->objects[page]), CDL_Obj_Name(&spec->objects[pd_id]), seL4_CapRights_get_capAllowGrant(rights), @@ -1445,7 +1585,7 @@ static void map_page(CDL_Model *spec UNUSED, CDL_Cap *page_cap, CDL_ObjID pd_id, if (CDL_Cap_Type(page_cap) == CDL_PTCap) { int error = seL4_ARCH_PageTable_Map(sel4_page, sel4_pd, vaddr, vm_attribs); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else if (CDL_Cap_Type(page_cap) == CDL_FrameCap) { #ifdef CAPDL_SHARED_FRAMES @@ -1454,7 +1594,7 @@ static void map_page(CDL_Model *spec UNUSED, CDL_Cap *page_cap, CDL_ObjID pd_id, int error_0 = seL4_CNode_Copy(seL4_CapInitThreadCNode, dest_index, CONFIG_WORD_SIZE, seL4_CapInitThreadCNode, sel4_page, CONFIG_WORD_SIZE, seL4_AllRights); - ZF_LOGF_IFERR(error_0, ""); + ABORT_IFERR(error_0, ""); next_free_slot(); sel4_page = dest_index; @@ -1484,15 +1624,15 @@ static void map_page(CDL_Model *spec UNUSED, CDL_Cap *page_cap, CDL_ObjID pd_id, /* Try and retrieve some useful information to help the user * diagnose the error. */ - ZF_LOGE("Failed to map frame "); + LOGE("Failed to map frame "); seL4_ARCH_Page_GetAddress_t addr UNUSED = seL4_ARCH_Page_GetAddress(sel4_page); if (addr.error) { - ZF_LOGE("", addr.error); + LOGE("", addr.error); } else { - ZF_LOGE("%p", (void *)addr.paddr); + LOGE("%p", (void *)addr.paddr); } - ZF_LOGE(" -> %p (error = %d)", (void *)vaddr, error); - ZF_LOGF_IFERR(error, ""); + LOGE(" -> %p (error = %d)", (void *)vaddr, error); + ABORT_IFERR(error, ""); } #ifdef CONFIG_ARCH_ARM /* When seL4 creates a new frame object it zeroes the associated memory @@ -1513,17 +1653,17 @@ static void map_page(CDL_Model *spec UNUSED, CDL_Cap *page_cap, CDL_ObjID pd_id, if (addr.paddr >= memory_region[0].start && addr.paddr <= memory_region[0].end) { if (!(vm_attribs & seL4_ARM_PageCacheable) && CDL_Obj_Paddr(&spec->objects[page]) == 0) { error = seL4_ARM_Page_CleanInvalidate_Data(sel4_page, 0, BIT(size_bits)); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } if (seL4_CapRights_get_capAllowGrant(rights)) { error = seL4_ARM_Page_Unify_Instruction(sel4_page, 0, BIT(size_bits)); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } #endif } else { - ZF_LOGF("attempt to map something that is not a frame or PT"); + ABORT("attempt to map something that is not a frame or PT"); } } @@ -1602,7 +1742,7 @@ static void init_level_0(CDL_Model *spec, CDL_ObjID level_0_obj, uintptr_t level CDL_PT_LEVEL_1_MAP(orig_caps(level_1_obj), orig_caps(level_0_obj), base, vm_attribs); init_level_1(spec, level_0_obj, base, level_1_obj); #else - ZF_LOGF("CDL_PT_LEVEL_1_MAP is not defined"); + ABORT("CDL_PT_LEVEL_1_MAP is not defined"); #endif } } @@ -1612,7 +1752,7 @@ static void init_level_0(CDL_Model *spec, CDL_ObjID level_0_obj, uintptr_t level static void map_page_directory_slot(CDL_Model *spec UNUSED, CDL_ObjID pd_id, CDL_CapSlot *pd_slot) { - ZF_LOGD(" Mapping slot %d in %s", pd_slot->slot, CDL_Obj_Name(&spec->objects[pd_id])); + LOGD(" Mapping slot %d in %s", pd_slot->slot, CDL_Obj_Name(&spec->objects[pd_id])); CDL_Cap *page_cap = CDL_CapSlot_Cap(pd_slot); seL4_Word page_vaddr = CDL_CapSlot_Slot(pd_slot) << (seL4_PageTableIndexBits + seL4_PageBits); @@ -1638,7 +1778,7 @@ static void map_page_table_slot(CDL_Model *spec UNUSED, CDL_ObjID pd, CDL_ObjID seL4_Word page_vaddr = pt_vaddr + (CDL_CapSlot_Slot(pt_slot) << seL4_PageBits); seL4_CapRights_t page_rights = CDL_seL4_Cap_Rights(page_cap); - ZF_LOGD(" Mapping %s into %s[%d] with rights={G: %d, R: %d, W: %d}, vaddr=0x%" PRIxPTR "", + LOGD(" Mapping %s into %s[%d] with rights={G: %d, R: %d, W: %d}, vaddr=0x%" PRIxPTR "", CDL_Obj_Name(&spec->objects[pt]), CDL_Obj_Name(&spec->objects[pd]), pt_slot->slot, seL4_CapRights_get_capAllowGrant(page_rights), seL4_CapRights_get_capAllowRead(page_rights), @@ -1674,16 +1814,16 @@ static void map_page_directory_page_tables(CDL_Model *spec, CDL_ObjID pd) static void init_vspace(CDL_Model *spec) { - ZF_LOGD("Initialising VSpaces..."); + LOGD("Initialising VSpaces..."); #if defined(CONFIG_ARCH_X86_64) || defined(CONFIG_ARCH_AARCH64) || defined(CONFIG_ARCH_RISCV) /* Have no understanding of the logic of model of whatever the hell the other code in this function is doing as it is pure gibberish. For x86_64 and aarch64 we will just do the obvious recursive initialization */ - ZF_LOGD("================================"); + LOGD("================================"); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_TOP_LEVEL_PD) { - ZF_LOGD(" Initialising top level %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Initialising top level %s...", CDL_Obj_Name(&spec->objects[obj_id])); #if (CDL_PT_NUM_LEVELS == 4) init_level_0(spec, obj_id, 0, obj_id); #elif (CDL_PT_NUM_LEVELS == 3) @@ -1691,26 +1831,26 @@ static void init_vspace(CDL_Model *spec) #elif (CDL_PT_NUM_LEVELS == 2) init_level_2(spec, obj_id, 0, obj_id); #else - ZF_LOGF("Unsupported CDL_PT_NUM_LEVELS value: \"%d\"", CDL_PT_NUM_LEVELS); + ABORT("Unsupported CDL_PT_NUM_LEVELS value: \"%d\"", CDL_PT_NUM_LEVELS); #endif } } #else - ZF_LOGD("================================"); - ZF_LOGD("Initialising page directories..."); + LOGD("================================"); + LOGD("Initialising page directories..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_PD) { - ZF_LOGD(" Initialising page directory %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Initialising page directory %s...", CDL_Obj_Name(&spec->objects[obj_id])); map_page_directory(spec, obj_id); } } - ZF_LOGD("==========================="); - ZF_LOGD("Initialising page tables..."); + LOGD("==========================="); + LOGD("Initialising page tables..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_PD) { - ZF_LOGD(" Initialising page tables in %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Initialising page tables in %s...", CDL_Obj_Name(&spec->objects[obj_id])); map_page_directory_page_tables(spec, obj_id); } } @@ -1811,19 +1951,19 @@ static void init_cnode_slot(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cno if (mode == MOVE && move_cap) { if (is_ep_cap || is_irq_handler_cap) { - ZF_LOGD("moving..."); + LOGD("moving..."); int error = seL4_CNode_Move(dest_root, dest_index, dest_depth, src_root, src_index, src_depth); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { - ZF_LOGD("mutating (with badge/guard %p)...", (void *)target_cap_data); + LOGD("mutating (with badge/guard %p)...", (void *)target_cap_data); int error = seL4_CNode_Mutate(dest_root, dest_index, dest_depth, src_root, src_index, src_depth, target_cap_data); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } else if (mode == COPY && !move_cap) { if (is_frame_cap && target_cap->mapping_container_id != INVALID_OBJ_ID) { - ZF_LOGD("moving mapped..."); + LOGD("moving mapped..."); /* The spec requires the frame cap in the current slot be the same one * used to perform the mapping of the frame in some container (either * a page table or page directory). */ @@ -1844,15 +1984,15 @@ static void init_cnode_slot(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cno /* Move the cap to the frame used for the mapping into the destination slot. */ int error = seL4_CNode_Move(dest_root, dest_index, dest_depth, src_root, mapped_frame_cap, src_depth); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } else { - ZF_LOGD("minting (with badge/guard %p)...", (void *)target_cap_data); + LOGD("minting (with badge/guard %p)...", (void *)target_cap_data); int error = seL4_CNode_Mint(dest_root, dest_index, dest_depth, src_root, src_index, src_depth, target_cap_rights, target_cap_data); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } else { - ZF_LOGV("skipping"); + LOGV("skipping"); } } @@ -1862,11 +2002,11 @@ static void init_cnode(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cnode) for (unsigned int slot_index = 0; slot_index < CDL_Obj_NumSlots(cdl_cnode); slot_index++) { if (CDL_Obj_GetSlot(cdl_cnode, slot_index)->cap.type == CDL_IRQHandlerCap) { CDL_IRQ UNUSED irq = CDL_Obj_GetSlot(cdl_cnode, slot_index)->cap.irq; - ZF_LOGD(" Populating slot %d with cap to IRQ %d, name %s...", + LOGD(" Populating slot %d with cap to IRQ %d, name %s...", CDL_Obj_GetSlot(cdl_cnode, slot_index)->slot, irq, CDL_Obj_Name(&spec->objects[spec->irqs[irq]])); } else { - ZF_LOGD(" Populating slot %d with cap to %s...", + LOGD(" Populating slot %d with cap to %s...", CDL_Obj_GetSlot(cdl_cnode, slot_index)->slot, CDL_Obj_Name(&spec->objects[CDL_Obj_GetSlot(cdl_cnode, slot_index)->cap.obj_id])); } @@ -1876,18 +2016,18 @@ static void init_cnode(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cnode) static void init_cspace(CDL_Model *spec) { - ZF_LOGD("Copying Caps..."); + LOGD("Copying Caps..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_CNode) { - ZF_LOGD(" Copying into %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Copying into %s...", CDL_Obj_Name(&spec->objects[obj_id])); init_cnode(spec, COPY, obj_id); } } - ZF_LOGD("Moving Caps..."); + LOGD("Moving Caps..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_CNode) { - ZF_LOGD(" Moving into %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Moving into %s...", CDL_Obj_Name(&spec->objects[obj_id])); init_cnode(spec, MOVE, obj_id); } } @@ -1895,13 +2035,13 @@ static void init_cspace(CDL_Model *spec) static void start_threads(CDL_Model *spec) { - ZF_LOGD("Starting threads..."); + LOGD("Starting threads..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_TCB && spec->objects[obj_id].tcb_extra.resume) { - ZF_LOGD(" Starting %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Starting %s...", CDL_Obj_Name(&spec->objects[obj_id])); seL4_CPtr tcb = orig_caps(obj_id); int error = seL4_TCB_Resume(tcb); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } } } @@ -1942,7 +2082,7 @@ static void fill_frame_with_bootinfo(uintptr_t base, CDL_FrameFill_Element_t fra case CDL_FrameFill_BootInfo_FDT: break; default: - ZF_LOGF("Unable to parse extra information for \"bootinfo\", given \"%d\"", + ABORT("Unable to parse extra information for \"bootinfo\", given \"%d\"", bi_type); } @@ -1995,10 +2135,10 @@ static void init_frame(CDL_Model *spec, CDL_ObjID obj_id, CDL_FrameFill_Element_ error = seL4_ARCH_Page_Map(cap, seL4_CapInitThreadPD, (seL4_Word)copy_addr_with_pt, seL4_ReadWrite, seL4_ARCH_Default_VMAttributes); } - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); - ssize_t max = BIT(spec->objects[obj_id].size_bits) - frame_fill.dest_offset; - ZF_LOGF_IF(frame_fill.dest_len > max, "Bad spec, fill frame with len larger than frame size"); + ABORT_IF(frame_fill.dest_offset + frame_fill.dest_len > BIT(spec->objects[obj_id].size_bits), + "Bad spec, fill frame with len larger than frame size"); /* Check for which type */ switch (frame_fill.type) { @@ -2009,12 +2149,12 @@ static void init_frame(CDL_Model *spec, CDL_ObjID obj_id, CDL_FrameFill_Element_ fill_frame_with_filedata(base, frame_fill); break; default: - ZF_LOGF("Unsupported frame fill type %u", frame_fill.type); + ABORT("Unsupported frame fill type %u", frame_fill.type); } /* Unmap the frame */ error = seL4_ARCH_Page_Unmap(cap); - ZF_LOGF_IFERR(error, ""); + ABORT_IFERR(error, ""); } static void init_frames(CDL_Model *spec) @@ -2032,10 +2172,10 @@ static void init_frames(CDL_Model *spec) static void init_scs(CDL_Model *spec) { - ZF_LOGD(" Initialising SCs"); + LOGD(" Initialising SCs"); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { if (spec->objects[obj_id].type == CDL_SchedContext) { - ZF_LOGD(" Initialising %s...", CDL_Obj_Name(&spec->objects[obj_id])); + LOGD(" Initialising %s...", CDL_Obj_Name(&spec->objects[obj_id])); /* all scs get configured on core 0, any scs that should be bound to a tcb will be reconfigured for the correct core in init_tcbs */ init_sc(spec, obj_id, 0); @@ -2054,13 +2194,13 @@ static void init_scs(CDL_Model *spec) */ static void mark_vspace_roots(CDL_Model *spec) { - ZF_LOGD("Marking top level PageTables as CDL_PT_ROOT_ALIAS..."); + LOGD("Marking top level PageTables as CDL_PT_ROOT_ALIAS..."); for (CDL_ObjID obj_id = 0; obj_id < spec->num; obj_id++) { CDL_ObjectType type = CDL_TCB; if (spec->objects[obj_id].type == type) { CDL_ObjID root = CDL_Cap_ObjID(get_cap_at(get_spec_object(spec, obj_id), CDL_TCB_VTable_Slot)); - ZF_LOGD(" Updating vspace_root: %d", root); + LOGD(" Updating vspace_root: %d", root); spec->objects[root].type = CDL_PT_ROOT_ALIAS; } } @@ -2068,16 +2208,12 @@ static void mark_vspace_roots(CDL_Model *spec) #endif -static void init_system(CDL_Model *spec) +static void init_system(CDL_Model *spec, seL4_BootInfo *bootinfo) { - seL4_BootInfo *bootinfo = platsupport_get_bootinfo(); - simple_t simple; cache_extended_bootinfo_headers(bootinfo); init_copy_addr(bootinfo); - simple_default_init_bootinfo(&simple, bootinfo); - init_copy_frame(bootinfo); parse_bootinfo(bootinfo, spec); @@ -2105,37 +2241,20 @@ static void init_system(CDL_Model *spec) init_cspace(spec); start_threads(spec); - ZF_LOGD("%d of %d CSlots used (%.2LF%%)", get_free_slot(), + LOGD("%d of %d CSlots used (%.2LF%%)", get_free_slot(), BIT(CONFIG_ROOT_CNODE_SIZE_BITS), ((long double)get_free_slot() / BIT(CONFIG_ROOT_CNODE_SIZE_BITS)) * 100); } -#ifdef CONFIG_DEBUG_BUILD -/* We need to give malloc enough memory for musllibc to allocate memory - * for stdin, stdout, and stderr. The heap pool base address and size is - * expected to be page aligned. - */ -extern char *morecore_area; -extern size_t morecore_size; -static char ALIGN(PAGE_SIZE_4K) debug_libc_morecore_area[PAGE_SIZE_4K]; -static void CONSTRUCTOR(MUSLCSYS_WITH_VSYSCALL_PRIORITY) init_bootinfo(void) +int main(seL4_BootInfo *boot_info) { - /* Init memory area for musl. */ - morecore_area = debug_libc_morecore_area; - morecore_size = sizeof(debug_libc_morecore_area); + __sel4_ipc_buffer = boot_info->ipcBuffer; - /* Allow us to print via seL4_Debug_PutChar. */ - platsupport_serial_setup_bootinfo_failsafe(); -} -#endif - -int main(void) -{ - ZF_LOGI("Starting CapDL Loader..."); - init_system(&capdl_spec); - ZF_LOGI(A_RESET A_FG_G "CapDL Loader done, suspending..." A_RESET ""); + LOGI("Starting CapDL Loader..."); + init_system(&capdl_spec, boot_info); + LOGI("CapDL Loader done, suspending..."); seL4_TCB_Suspend(seL4_CapInitThreadTCB); }