libsel4vka: Fix size bits in vka_untyped_retype for seL4_CapTableObject

[astevins]

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:

  seL4_libs/libsel4vka/include/vka/capops.h

  Line 130 in fcabdef

  size_bits = vka_get_object_size(type, size_bits);

• 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.

[astevins]

Force pushed to adhere to gitlint's commit title length requirement

[lsf37]

I think the question here is more one of what the expected behaviour of this function is -- it currently exports the meaning of size_bits from the seL4 API, which is the size of the object in terms of its native size. I.e. bytes for Untypeds and number of slots for CNodes.

@kent-mcleod do you know what the intention was for this one? For allocators it would make sense to take the size in bytes and translate to object size, but I would assume that there is plenty of other code that assumes the current behaviour (might also be relevant for number of SchedulingContext refills, I guess).

[astevins]

Potentially replacing the vka_get_object_size call with something like get_sel4_object_size is a better approach

seL4_libs/libsel4allocman/include/allocman/utspace/utspace.h

Line 43 in fcabdef

static inline size_t get_sel4_object_size(seL4_Word type, size_t size_bits) {