Hello Ben, On 2024-09-05 01:12, Ben McCart wrote:
I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!)
Like the manual mentions, you can use linker symbols to find most virtual addresses. What virtual addresses are used depends on the user image and is defined in the ELF file.
In addition, I like to know the address range used for the stack of the initial thread,
The default root task in most seL4 project use sel4runtime, which uses a static 16kb stack with the C variable name _stack_base and _stack_top, see e.g: https://github.com/seL4/sel4runtime/blob/master/crt/sel4_arch/x86_64/sel4_cr... You can use readelf(1) or objdump(1) on the binary of your userland image to find other symbols. However, the seL4 kernel also supports other user images than those based on sel4runtime, so the seL4 manual can only provide generic information.
as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?)
The reserved virtual address range is platform specific. Usually platforms only support a limited range of virtual address space, e.g. 48 bits out of 64 bits only. The upper bits are set to 1 for kernel virtual addresses and to 0 for user space virtual addresses. I think this is exported by libsel4 as seL4_UserTop. Greetings, Indan