// ReadCpuPciCfg - decompiled from Platform.efi
__int64 __fastcall ReadCpuPciCfg(__int64 a1, char a2, char a3)
{
  _DWORD v4[6]; // [rsp+20h] [rbp-18h] BYREF

  v4[3] = 0; /*0x7ad3*/
  v4[1] = 0; /*0x7adb*/
  v4[2] = 512; /*0x7aec*/
  v4[0] = (a3 & 7 | (8 * (a2 & 0x1F))) << 12; /*0x7af6*/
  return (*(__int64 (__fastcall **)(_DWORD *))(qword_FF00 + 24))(v4); /*0x7b03*/
}