[patches-axel]

.github/workflows/sel4test-sim.yml

@@ -22,7 +22,7 @@ concurrency:
   cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 jobs:
-  cparser:
+  simulation:
     name: Simulation
     runs-on: ubuntu-latest
     strategy:

libsel4allocman/src/bootstrap.c

@@ -227,13 +227,19 @@ int bootstrap_add_untypeds_from_bootinfo(bootstrap_info_t *bs, seL4_BootInfo *bi
 
 static int bootstrap_add_untypeds_from_simple(bootstrap_info_t *bs, simple_t *simple) {
     int error;
-    int i;
     /* if we do not have a boot cspace, or we have added some uts that aren't in the
      * current space then just bail */
     if (!bs->have_boot_cspace || (bs->uts && !bs->uts_in_current_cspace)) {
         return 1;
     }
-    for (i = 0; i < simple_get_untyped_count(simple); i++) {
+
+    int cnt = simple_get_untyped_count(simple);
+    if (cnt < 0) {
+        ZF_LOGW("Could not get untyped count (%d)", cnt);
+        return 1;
+    }
+
+    for (int i = 0; i < cnt; i++) {
         size_t size_bits;
         uintptr_t paddr;
         bool device;
@@ -1005,10 +1011,7 @@ static int handle_device_untyped_cap(add_untypeds_state_t *state, uintptr_t padd
     bool cap_tainted = false;
     int error;
     uintptr_t ut_end = paddr + BIT(size_bits);
-    int num_regions = 0;
-    if (state != NULL) {
-        num_regions = state->num_regions;
-    }
+    int num_regions = state ? state->num_regions : 0;
     for (int i = 0; i < num_regions; i++) {
         pmem_region_t *region = &state->regions[i];
         uint64_t region_end = region->base_addr + region->length;
@@ -1111,23 +1114,25 @@ int allocman_add_simple_untypeds_with_regions(allocman_t *alloc, simple_t *simpl
     int error = prepare_handle_device_untyped_cap(alloc, simple, &state, num_regions, region_list);
     ZF_LOGF_IF(error, "bootstrap_prepare_handle_device_untyped_cap Failed");
 
-    size_t i;
-    size_t total_untyped = simple_get_untyped_count(simple);
+    int total_untyped = simple_get_untyped_count(simple);
+    if (total_untyped < 0) {
+        ZF_LOGW("Could not get untyped count (%d)", total_untyped);
+        return 0; /* don't report an error, just do nothing */
+    }
 
-    for(i = 0; i < total_untyped; i++) {
+    for(int i = 0; i < total_untyped; i++) {
         size_t size_bits;
         uintptr_t paddr;
         bool device;
         cspacepath_t path = allocman_cspace_make_path(alloc, simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device));
-        int dev_type = device ? ALLOCMAN_UT_DEV : ALLOCMAN_UT_KERNEL;
-        // If it is regular UT memory, then we add cap and move on.
-        if (dev_type == ALLOCMAN_UT_KERNEL) {
-            error = allocman_utspace_add_uts(alloc, 1, &path, &size_bits, &paddr, dev_type);
-            ZF_LOGF_IF(error, "Could not add kernel untyped.");
-        } else {
-            // Otherwise we are Device untyped.
+        if (device) {
+            // Separates device RAM memory into separate untyped caps
             error = handle_device_untyped_cap(state, paddr, size_bits, &path, alloc);
-            ZF_LOGF_IF(error, "bootstrap_arch_handle_device_untyped_cap failed.");
+            ZF_LOGF_IF(error, "handle_device_untyped_cap failed (%d).", error);
+        } else {
+            // for regular UT memory we add cap
+            error = allocman_utspace_add_uts(alloc, 1, &path, &size_bits, &paddr, ALLOCMAN_UT_KERNEL);
+            ZF_LOGF_IF(error, "Could not add kernel untyped (%d).", error);
         }
     }
     if (state) {

libsel4debug/src/bootinfo.c

@@ -8,41 +8,95 @@
 #include <sel4debug/gen_config.h>
 
 #include <stdio.h>
+#include <assert.h>
 
 #include <sel4/sel4.h>
 #include <utils/util.h>
 
+static void print_slot_reg_info(char const *descr, seL4_SlotRegion *reg)
+{
+    if (reg->end == reg->start) {
+        printf("%snone\n", descr);
+    } else {
+        printf("%s[%"SEL4_PRIu_word" --> %"SEL4_PRIu_word")\n",
+               descr, reg->start, reg->end);
+    }
+}
+
 void debug_print_bootinfo(seL4_BootInfo *info)
 {
+    printf("Node:                      %"SEL4_PRIu_word" of %"SEL4_PRIu_word"\n",
+           info->nodeID, info->numNodes);
+    printf("Domain:                    %"SEL4_PRIu_word"\n",
+           info->initThreadDomain);
+    printf("IPC buffer:                %p\n", info->ipcBuffer);
+    printf("IO-MMU page table levels:  %"SEL4_PRIu_word"\n",
+           info->numIOPTLevels);
+    printf("Root cnode size:           2^%"SEL4_PRIu_word" (%lu)\n",
+           info->initThreadCNodeSizeBits,
+           LIBSEL4_BIT(info->initThreadCNodeSizeBits));
+    print_slot_reg_info("Shared pages:              ", &info->sharedFrames);
+    print_slot_reg_info("User image MMU tables:     ", &info->userImagePaging);
+    print_slot_reg_info("Extra boot info pages:     ", &info->extraBIPages);
+    print_slot_reg_info("User image pages:          ", &info->userImageFrames);
+    print_slot_reg_info("Untyped memory:            ", &info->untyped);
+    print_slot_reg_info("Empty slots:               ", &info->empty);
 
-    printf("Node %lu of %lu\n", (long)info->nodeID, (long)info->numNodes);
-    printf("IOPT levels:     %u\n", (int)info->numIOPTLevels);
-    printf("IPC buffer:      %p\n", info->ipcBuffer);
-    printf("Empty slots:     [%lu --> %lu)\n", (long)info->empty.start, (long)info->empty.end);
-    printf("sharedFrames:    [%lu --> %lu)\n", (long)info->sharedFrames.start, (long)info->sharedFrames.end);
-    printf("userImageFrames: [%lu --> %lu)\n", (long)info->userImageFrames.start, (long)info->userImageFrames.end);
-    printf("userImagePaging: [%lu --> %lu)\n", (long)info->userImagePaging.start, (long)info->userImagePaging.end);
-    printf("untypeds:        [%lu --> %lu)\n", (long)info->untyped.start, (long)info->untyped.end);
-    printf("Initial thread domain: %u\n", (int)info->initThreadDomain);
-    printf("Initial thread cnode size: %u\n", (int)info->initThreadCNodeSizeBits);
-    printf("List of untypeds\n");
-    printf("------------------\n");
-    printf("Paddr    | Size   | Device\n");
-
-    int sizes[CONFIG_WORD_SIZE] = {0};
-    for (int i = 0; i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS && i < (info->untyped.end - info->untyped.start); i++) {
-        int index = info->untypedList[i].sizeBits;
-        assert(index < ARRAY_SIZE(sizes));
-        sizes[index]++;
-        printf("%p | %zu | %d\n", (void *)info->untypedList[i].paddr, (size_t)info->untypedList[i].sizeBits,
-               (int)info->untypedList[i].isDevice);
+    printf("Extra boot info blobs:\n");
+    seL4_Word offs = 0;
+    while (offs < info->extraLen) {
+        seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + seL4_BootInfoFrameSize + offs);
+        printf("    type: %"SEL4_PRIu_word", offset: %"SEL4_PRIu_word", len: %"SEL4_PRIu_word"\n",
+               h->id, offs, h->len);
+        offs += h->len;
     }
 
-    printf("Untyped summary\n");
-    for (int i = 0; i < ARRAY_SIZE(sizes); i++) {
-        if (sizes[i] != 0) {
-            printf("%d untypeds of size %d\n", sizes[i], i);
+    seL4_Word numUntypeds = info->untyped.end - info->untyped.start;
+    printf("Used bootinfo untyped descriptors: %"SEL4_PRIu_word" of %d\n",
+           numUntypeds, CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS);
+    /* Sanity check that the boot info is consistent. */
+    assert(info->empty.end == LIBSEL4_BIT(info->initThreadCNodeSizeBits));
+    assert(numUntypeds < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS);
+    assert(info->extraLen <= (LIBSEL4_BIT(seL4_PageBits) * (info->extraBIPages.end - info->extraBIPages.start)));
+
+    printf("Physical memory map with available untypeds:\n");
+    printf("---------------------+------+----------+-------\n");
+    printf(" Phys Addr           | Size | Type     | Slot\n");
+    printf("---------------------+------+----------+-------\n");
+
+    for (seL4_Word pos = 0; pos < (seL4_Word)(-1); pos++) {
+        /* Find the next descriptor according to our current position. */
+        seL4_UntypedDesc *d = NULL;
+        int idx = -1;
+        for (int i = 0; i < numUntypeds; i++) {
+            seL4_UntypedDesc *d_tmp = &info->untypedList[i];
+            if (d_tmp->paddr < pos) {
+                continue;
+            }
+            if (d && (d_tmp->paddr >= d->paddr)) {
+                /* Two  descriptors for the same region are not allowed. */
+                assert(d_tmp->paddr != d->paddr);
+                continue;
+            }
+            d = d_tmp; /* Found a better match. */
+            idx = i;
         }
+        /* No adjacent descriptor found means there is reserved space. */
+        if ((!d) || (pos < d->paddr)) {
+            printf("  %#*"SEL4_PRIx_word" | -    | reserved | -\n",
+                   2 + (CONFIG_WORD_SIZE / 4), pos);
+            if (!d) {
+                break; /* No descriptors found at all means we are done. */
+            }
+        }
+        printf("  %#*"SEL4_PRIx_word" | 2^%-2u | %s | %"SEL4_PRIu_word"\n",
+               2 + (CONFIG_WORD_SIZE / 4),
+               d->paddr,
+               d->sizeBits,
+               d->isDevice ? "device  " : "free    ",
+               info->untyped.start + idx);
+        seL4_Word pos_new = d->paddr + LIBSEL4_BIT(d->sizeBits) - 1;
+        assert(pos_new >= pos); /* Regions must not overflow. */
+        pos = pos_new;
     }
 }
-

libsel4muslcsys/src/sys_morecore.c

@@ -68,6 +68,11 @@ long sys_mmap_impl(void *addr, size_t length, int prot, int flags, int fd, off_t
         if (length > morecore_top - morecore_base) {
             return -ENOMEM;
         }
+
+        ZF_LOGI(
+            "morecore %p - %p, len %#x, return address: 0x%"PRIxPTR,
+            morecore_base, morecore_top, length, morecore_top-length);
+
         /* Steal from the top */
         morecore_top -= length;
         return morecore_top;
@@ -116,6 +121,8 @@ static void init_morecore_region(void)
         morecore_base = (uintptr_t) morecore_area;
         morecore_top = (uintptr_t) &morecore_area[morecore_size];
     }
+
+    ZF_LOGI("morecore %p - %p (%#zd)", morecore_base, morecore_top, morecore_size);
 }
 
 static long sys_brk_static(va_list ap)
@@ -199,8 +206,16 @@ static long sys_mmap_impl_static(void *addr, size_t length, int prot, int flags,
         if (base < morecore_base) {
             return -ENOMEM;
         }
+        ZF_LOGF_IF(
+            (base % 0x1000) != 0,
+            "morecore %p - %p, len %#zx, return address: %p (not 4 KiB aligned)",
+            (void*)morecore_base, (void*)morecore_top, length, (void*)base);
+
+        ZF_LOGI(
+            "morecore %p - %p, len %#zx, return address: %p",
+            (void*)morecore_base, (void*)morecore_top, length, (void*)base);
+
         morecore_top = base;
-        ZF_LOGF_IF((base % 0x1000) != 0, "return address: 0x%"PRIxPTR" requires alignment: 0x%x ", base, 0x1000);
         return base;
     }
     assert(!"not implemented");