search

seL4 / util_libs

Other
55 stars 83 forks source link

libutils: add kernel word size related CTZ macro #176

Closed colorglass closed 8 months ago

colorglass commented 8 months ago

Add kernel word size related macros CxZ_WORD() for ctz and clz builtin func. And also add CxZLL() macro for 64bits data size. And for the macro CTZL(), which is used for unsigned long type, I found a error use in sel4test timer dirver: https://github.com/seL4/sel4test/blob/0a488b92bc7a08acc14d49524d1f22656f286627/apps/sel4test-driver/src/timer.c#L53

......
void handle_timer_interrupts(driver_env_t env, seL4_Word badge)
{
    int error = 0;
    while (badge) {
        seL4_Word badge_bit = CTZL(badge);
......

The seL4_Word type can be 64bits, but CTZL() recives unsigned long argument. It can be changed to CTZ_WORD() to fix the problom.

colorglass commented 8 months ago

Thanks for your attention.

I searched C99 standard ISO/IEC 9899:1999, and didn't find the size define of long, only got some information indicates that it should hold the number limits defined in limits.h.

And I find that the size of long in gcc was defined by a internal macro LONG_TYPE_SIZE Layout of Source Language Data Types, which defines that long type in gcc has the default one word size.

Finally I write the simple test file to print the result of sizeof(long), compile and run and get the result is 4 within my visual studio 2019.

So I can confirm that the practical size of the long is depended on the compiler itself. The most generally used compiler is gcc and one word size long becomes a de facto standard.

Please forgive my attention to details, and since there is no builtin_ctz() function in msvc, we can just apply CTZL() to word size variable with no change to this file.

axel-h commented 8 months ago

See explanation here: https://en.m.wikipedia.org/wiki/64-bit_computing Seems LLP64 support for userland is currently not planned then.