From 343f9c77d146ec999e44fc812ab5b9317adc3133 Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Wed, 30 Aug 2023 22:26:13 +1000 Subject: [PATCH 1/4] Remove seL4_lib dependencies from generated C spec The capdl_spec.c file is generated by capDL-tool and is compiled into the capdl-loader-app program to define the system that the loader will load. The file is supposed to only be a C-language representation of the capDL spec for a particular system. Currently, the header files required to compile this spec file introduces dependencies on a C library, and libraries from seL4/util_libs and seL4/sel4_libs including libsel4utils and libutils (and any libraries they depend on). The spec itself doesn't inherently require any type definitions other than what's provided by libsel4, and so it shouldn't require these additional dependencies. Signed-off-by: Kent McLeod --- capDL-tool/CapDL/PrintC.hs | 6 +-- capdl-loader-app/include/capdl.h | 83 ++++++++++++++++++-------------- 2 files changed, 50 insertions(+), 39 deletions(-) diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 4d71ee9b..99c4bb03 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" ++ diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index 32d46253..4e15fb6a 100644 --- a/capdl-loader-app/include/capdl.h +++ b/capdl-loader-app/include/capdl.h @@ -9,15 +9,26 @@ #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 PACKED __attribute__((__packed__)) + +#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 +133,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 +278,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 +289,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 +339,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 +386,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 +444,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 +460,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 +492,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 +503,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 +548,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 +588,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; } From 8139b5b6946627a679074a3f8fd99de8751fb5ed Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Fri, 1 Sep 2023 23:23:16 +1000 Subject: [PATCH 2/4] capdl-loader-app: Introduce custom error checks Instead of ZF_LOG* framework functions, we introduce our own layering of functions that directly output to seL4_DebugPutChar() when the debug syscall is present and outputs nothing when it isn't. This implementation allows using a minimal amount of the muslc stdio implementation for string formatting and bypasses the need for malloc or any syscalls to be supported. This will make it easier to refactor capdl-loader-app to be more freestanding (minimal runtime dependencies) in upcoming commits. Signed-off-by: Kent McLeod --- capdl-loader-app/CMakeLists.txt | 5 +- capdl-loader-app/src/check.c | 48 +++++ capdl-loader-app/src/check.h | 52 ++++++ capdl-loader-app/src/main.c | 313 ++++++++++++++++---------------- 4 files changed, 261 insertions(+), 157 deletions(-) create mode 100644 capdl-loader-app/src/check.c create mode 100644 capdl-loader-app/src/check.h diff --git a/capdl-loader-app/CMakeLists.txt b/capdl-loader-app/CMakeLists.txt index ed2d54bb..0d6cc2eb 100644 --- a/capdl-loader-app/CMakeLists.txt +++ b/capdl-loader-app/CMakeLists.txt @@ -95,10 +95,13 @@ add_config_library(capdl_loader_app "${configure_string}") # 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") +get_target_property(MUSL_SOURCE_DIR muslc_gen SOURCE_DIR) +set_property(TARGET capdl_app_properties PROPERTY C_FILES "${CMAKE_CURRENT_SOURCE_DIR}/src/main.c" "${CMAKE_CURRENT_SOURCE_DIR}/src/check.c") set_property( TARGET capdl_app_properties 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) diff --git a/capdl-loader-app/src/check.c b/capdl-loader-app/src/check.c new file mode 100644 index 00000000..ad55f72f --- /dev/null +++ b/capdl-loader-app/src/check.c @@ -0,0 +1,48 @@ +/* + * 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; +} + 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/main.c b/capdl-loader-app/src/main.c index e3a5c380..db0c1414 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -29,6 +29,7 @@ #include #include #endif +#include "check.h" #include "capdl_spec.h" @@ -102,7 +103,7 @@ static seL4_CPtr get_free_slot(void) 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 +162,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 +186,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 +197,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 +209,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 +224,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 +241,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 +265,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 +289,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 +323,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 +331,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 +360,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 +376,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 +400,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 +423,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 +436,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 +465,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 +475,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 +517,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 +537,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, 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 +596,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); @@ -628,7 +629,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 +637,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 +651,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 +673,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 +713,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 +729,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 +741,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 +751,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 +761,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 +787,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 +808,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 +824,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 +832,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 +840,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 +850,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 +897,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 +931,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 +949,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 +985,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 +993,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 +1004,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 +1044,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 +1099,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 +1122,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 +1144,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 +1153,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 +1184,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 +1203,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 +1215,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 +1247,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 +1255,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 +1264,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 +1311,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 +1323,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 +1362,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 +1383,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 +1404,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 +1436,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 +1446,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 +1455,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 +1485,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 +1514,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 +1603,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 +1613,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 +1639,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 +1675,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 +1692,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 +1812,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 +1845,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 +1863,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 +1877,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 +1896,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 +1943,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 +1996,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_len > max, "Bad spec, fill frame with len larger than frame size"); /* Check for which type */ switch (frame_fill.type) { @@ -2009,12 +2010,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 +2033,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 +2055,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; } } @@ -2105,7 +2106,7 @@ 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); @@ -2134,8 +2135,8 @@ static void CONSTRUCTOR(MUSLCSYS_WITH_VSYSCALL_PRIORITY) init_bootinfo(void) int main(void) { - ZF_LOGI("Starting CapDL Loader..."); + LOGI("Starting CapDL Loader..."); init_system(&capdl_spec); - ZF_LOGI(A_RESET A_FG_G "CapDL Loader done, suspending..." A_RESET ""); + LOGI("CapDL Loader done, suspending..."); seL4_TCB_Suspend(seL4_CapInitThreadTCB); } From ab39b65a1f6912d6e4737164735cadcdf88ab43d Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Fri, 1 Sep 2023 23:41:27 +1000 Subject: [PATCH 3/4] capdl-loader-app: Remove seL4_libs dependencies Refactor the remainder of the implementation of capdl-loader-app to remove seL4_libs dependencies. This is achieved by mostly using similar basic constructions inline rather than relying on them being provided by the external libs: - Create inline definitions of seL4_ARCH_{invocation} for the arch being built, - implement get_frame_object_type() which returns the correct object type for page sizes of the current architecture, - provide a few macro definitions for basic definitions - remove platsupport_serial_setup code as seL4_DebugPutchar() will be used for any console output for this app. (The loader doesn't safely handle accessing physical serial device untyped without potentially conflicting with resource requests of the system being loaded. - remove malloc initialization as it is no longer required. Signed-off-by: Kent McLeod --- capdl-loader-app/helpers.cmake | 7 +- capdl-loader-app/include/capdl.h | 3 + capdl-loader-app/src/check.c | 1 - capdl-loader-app/src/main.c | 166 +++++++++++++++++++++---------- 4 files changed, 121 insertions(+), 56 deletions(-) diff --git a/capdl-loader-app/helpers.cmake b/capdl-loader-app/helpers.cmake index d8cbf1da..0a538fc7 100644 --- a/capdl-loader-app/helpers.cmake +++ b/capdl-loader-app/helpers.cmake @@ -77,14 +77,11 @@ function(BuildCapDLApplication) sel4runtime sel4 cpio - sel4platsupport - sel4utils capdl_loader_app_Config sel4_autoconf + muslc ) - 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 4e15fb6a..e7be7f1f 100644 --- a/capdl-loader-app/include/capdl.h +++ b/capdl-loader-app/include/capdl.h @@ -12,7 +12,10 @@ #include #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 diff --git a/capdl-loader-app/src/check.c b/capdl-loader-app/src/check.c index ad55f72f..d7826a7f 100644 --- a/capdl-loader-app/src/check.c +++ b/capdl-loader-app/src/check.c @@ -45,4 +45,3 @@ int _printf(const char *restrict fmt, ...) va_end(ap); return ret; } - diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index db0c1414..e51d3a9c 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -4,37 +4,111 @@ * 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 #include -#include -#include "capdl.h" +#include +#include -#ifdef CONFIG_DEBUG_BUILD -#include -#include +#include +#ifdef CONFIG_ARCH_ARM +#include #endif #include "check.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 @@ -100,6 +174,21 @@ static seL4_CPtr get_free_slot(void) return free_slot_start; } +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++; @@ -542,7 +631,7 @@ static int find_device_object(seL4_Word paddr, seL4_Word type, int size_bits, se 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); ABORT_IFERR(error, ""); addr = seL4_ARCH_Page_GetAddress(free_slot + 2); @@ -613,7 +702,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; @@ -621,7 +710,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 @@ -1998,8 +2087,8 @@ static void init_frame(CDL_Model *spec, CDL_ObjID obj_id, CDL_FrameFill_Element_ } ABORT_IFERR(error, ""); - ssize_t max = BIT(spec->objects[obj_id].size_bits) - frame_fill.dest_offset; - ABORT_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) { @@ -2069,16 +2158,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); @@ -2113,30 +2198,11 @@ static void init_system(CDL_Model *spec) } -#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) -{ - /* Init memory area for musl. */ - morecore_area = debug_libc_morecore_area; - morecore_size = sizeof(debug_libc_morecore_area); - - /* Allow us to print via seL4_Debug_PutChar. */ - platsupport_serial_setup_bootinfo_failsafe(); -} -#endif int main(void) { LOGI("Starting CapDL Loader..."); - init_system(&capdl_spec); + init_system(&capdl_spec, sel4runtime_bootinfo()); LOGI("CapDL Loader done, suspending..."); seL4_TCB_Suspend(seL4_CapInitThreadTCB); } From 7ced9b3c2cf5eaa8b8cb2bf5da30a909cad4b1ff Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Fri, 1 Sep 2023 23:16:47 +1000 Subject: [PATCH 4/4] capdl-loader-app: Refactor two-phase build design The capdl-loader-app has previously used a non-conventional CMake pattern for building. As the app is built with the capDL spec and ELF files for any program data the loader is required to load, the actual CMake target definitions are deferred until the targets for generating the capDL spec are known as well as the ELF targets. These are then used to declare a capdl-loader-app target. Instead this change uses a different approach: - It compiles and links the program code leaving the symbols for the capDL spec and CPIO archive containing the ELF files unresolved, while still producing a base object file "capdl-loader.o". - Later on, a complete image can be created by taking the CapDL C spec and an object file containing a CPIO archive of ELF files and compiling these with the "capdl-loader.o" file. This compilation can be done outside of a CMake build as only access to libsel4 and capdl-loader-app header files are required to compile the CapDL C spec. - The helpers.cmake file that declares BuildCapDLApplication now builds the rootimage from within a custom command that performs the external call to a compiler with the required include paths and input files. - the sel4runtime dependency is removed as the loader app doesn't require thread-local storage and basic entry point assembly code is provided by "entry.h" which sets up a stack and then directly calls main() as the kernel places the bootinfo pointer in the first argument register and this is all the capdl-loader program needs to bootstrap. - As there is only one thread in the loader app, use global allocation instead of thread-local allocation for thread variables such as the pointer for the seL4 IPC buffer used by libsel4. Signed-off-by: Kent McLeod --- capDL-tool/CapDL/PrintC.hs | 1 + capdl-loader-app/CMakeLists.txt | 120 ++++++++++++++++++++++++--- capdl-loader-app/helpers.cmake | 75 ++++++----------- capdl-loader-app/src/check.c | 16 ++++ capdl-loader-app/src/entry.h | 140 ++++++++++++++++++++++++++++++++ capdl-loader-app/src/main.c | 58 ++++++++++++- 6 files changed, 348 insertions(+), 62 deletions(-) create mode 100644 capdl-loader-app/src/entry.h diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 99c4bb03..9db5dbf9 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -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 0d6cc2eb..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,19 +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) + +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) -set_property(TARGET capdl_app_properties PROPERTY C_FILES "${CMAKE_CURRENT_SOURCE_DIR}/src/main.c" "${CMAKE_CURRENT_SOURCE_DIR}/src/check.c") + +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 0a538fc7..17031836 100644 --- a/capdl-loader-app/helpers.cmake +++ b/capdl-loader-app/helpers.cmake @@ -26,60 +26,37 @@ 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() - - 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() + 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 - # 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 - capdl_loader_app_Config - sel4_autoconf - muslc + 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}" ) endfunction(BuildCapDLApplication) diff --git a/capdl-loader-app/src/check.c b/capdl-loader-app/src/check.c index d7826a7f..e8dbc109 100644 --- a/capdl-loader-app/src/check.c +++ b/capdl-loader-app/src/check.c @@ -45,3 +45,19 @@ int _printf(const char *restrict fmt, ...) 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/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 e51d3a9c..63f0936e 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -12,9 +12,9 @@ #include #include +#define __thread #include #include -#include #include #ifdef CONFIG_ARCH_ARM @@ -22,6 +22,8 @@ #endif #include "check.h" +#include "entry.h" + #include "capdl.h" #include "capdl_spec.h" @@ -129,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]; @@ -174,6 +178,52 @@ 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) { @@ -2199,10 +2249,12 @@ static void init_system(CDL_Model *spec, seL4_BootInfo *bootinfo) } -int main(void) +int main(seL4_BootInfo *boot_info) { + __sel4_ipc_buffer = boot_info->ipcBuffer; + LOGI("Starting CapDL Loader..."); - init_system(&capdl_spec, sel4runtime_bootinfo()); + init_system(&capdl_spec, boot_info); LOGI("CapDL Loader done, suspending..."); seL4_TCB_Suspend(seL4_CapInitThreadTCB); }