libsel4allocman: overflow guards for large UT

seL4 can and does produce Untypeds that reach the end of the address space. Using start + BIT(size) is not overflow safe for these.

Replace this pattern with MASK instead for inclusive-end reasoning, or explicitly use uint64_t where that is too inconvenient.

The latter does rely on the fact that we will not get Untypeds that reach 2^64. It does look like no architecture so far has a full 64-bit physical address space, so this should be impossible.

This is not a full overflow safety survey of all of libsel4allocman, just what I found by searching for “BIT(“ in the untyped allocation path. It at least does fix the errors I was getting for zcu102 which does now produce such an untyped cap.

Signed-off-by: Gerwin Klein gerwin.klein@proofcraft.systems

seL4 Libraries

A collection of libraries for working on seL4.

libsel4allocman: an allocator for managing virtual memory, malloc memory and cspaces.
libsel4bench: a library with utilities for benchmarking on seL4.
libsel4debug: a library with utilities for debugging on seL4. Only useful when debugging a userlevel app; potentially hacky.
libsel4muslcsys: a library to support muslc for the root task.
libsel4platsupport: a wrapper around libplatsupport specificially for seL4.
libsel4simple: an interface which abstracts over the boot environment of a seL4 application.
libsel4simple-default: an implementation of simple for the master branch of the kernel.
libsel4simple-experimental: an implementatoin of simple for the experimental branch of the kernel.
libsel4sync: a synchronisation library that uses notifications to construct basic locks.
libsel4test: a very basic test infrastructure library.
libsel4utils: a library OS - Commonly used stuff, actively maintained: implements threads, processes, elf loading, virtual memory management etc.
libsel4vka: an allocation interface for seL4.
libsel4vspace: a virtual memory management interface for seL4.