seL4_libs
seL4_libs copied to clipboard
libsel4vka: Fix size bits in vka_untyped_retype for seL4_CapTableObject
The size bits for a untyped retype to seL4_CapTableObject
are calculated incorrectly when using vka_untyped_retype
-
seL4_SlotBits
is added once in vka: https://github.com/seL4/seL4_libs/blob/fcabdef37016cd568a40c82e0d97a264b86ee6d4/libsel4vka/include/vka/capops.h#L130 - And it is added again during the syscall: https://github.com/seL4/seL4/blob/c679fe77d6441cd412dd253d953ee833dd25d740/src/object/untyped.c#L75
The result is that seL4_SlotBits
is added twice, causing the UntypedRetype operation to fail with "Insufficient memory" for this simple test:
int test_retype_cap_table_object(env_t env)
{
int error;
size_t cspace_size_bits = 17;
vka_object_t untyped;
error = vka_alloc_untyped(&env->vka, cspace_size_bits + seL4_SlotBits, &untyped);
test_error_eq(error, 0);
cspacepath_t cnode_dest;
error = vka_cspace_alloc_path(&env->vka, &cnode_dest);
test_error_eq(error, 0);
error = vka_untyped_retype(&untyped, seL4_CapTableObject, cspace_size_bits, 1, &cnode_dest);
test_error_eq(error, 0);
}
A simple solution is to subtract seL4_SlotBits before calling seL4_Untyped_Retype
.