#include <stdio.h>
#include <stdint.h>

int main() {
    uint32_t eax, ebx, ecx, edx;

    eax = 0x80000008;

    __asm__ __volatile__ (
        "cpuid"
        : "=a" (eax), "=b" (ebx), "=c" (ecx), "=d" (edx)
        : "a" (eax)
    );

    printf("EBX: 0x%x\n", ebx);

    if (ebx & (1 << 3)) {
        printf("CPU supports INVLPGB\n");
    } else {
        printf("CPU does not support INVLPGB\n");
    }

    return 0;
}