Adrian, That is great to hear. Thanks for the feedback.
Jeff Kubascik On 9/28/2017 12:24 AM, [email protected] wrote: > Hi Jeff, > > The change looks good to me. Have applied it internally and will let it go > through CI. > > Thanks! > Adrian > > On Thu 28-Sep-2017 6:08 AM, Jeff Kubascik wrote: >> 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 >> <<seL4(CPU 0) [decodeUntypedInvocation/210 T0xffdfd100 "rootserver" @8fa8]: >> Untyped Retype: Insufficient memory (1 * 4096 bytes needed, 0 bytes >> available).>> >> >> 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 <[email protected]> >> 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 _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
