/* x86_cpuid2() writes four 32bit values, %eax, %ebx, %ecx and %edx */