Hello, I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug that occurs when a device physical memory region includes the highest address, i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I create a CAmkES component that uses the highest address, I see the following error. ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..100ac81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[33000..1aefff] vaddr=[8000..183fff] virt_entry=befc Enabling MMU and paging Bootstrapping kernel Booting all finished, dropped to user space <> Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() [Err seL4_NotEnoughMemory]: I have traced this problem to an integer overflow bug in the capdl-loader. The patch below shows how I have addressed this error.

From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001 From: Jeff Kubascik Date: Wed, 27 Sep 2017 13:52:36 -0400 Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a device physical memory region ends at 0xFFFFFFFF

--- capdl-loader-app/src/main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 34eedb0..305da2a 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type, int size_bits, seL4_C /* Assume we are allocating from a device untyped. Do a linear search for it */ for (unsigned int i = 0; i < bootinfo->untyped.end - bootinfo->untyped.start; i++) { if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr && - bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) { + bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits) - 1) { /* just allocate objects until we get the one we want. To do this * correctly we cannot just destroy the cap we allocate, since * if it's the only frame from the untyped this will reset the -- 2.7.4 I have added a -1 to the end address calculations to fix the edge case when bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) is equal to 0x100000000, an integer overflow. The current statement is comparing the address of the next byte past the end of the memory region. My change is comparing the address of the last byte in the memory region. I have tested this fix on the zynq7000 and it works. However, I am not too familiar with the capdl-loader. Are there any problems with this fix that I have not considered? Thanks, Jeff Kubascik