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
