// Decompiled: 0xffe0757c
// Function: ReadMsr64
// Module: TxtPei.efi (TXTPEI)

int __fastcall ReadMsr64(unsigned int a1)
{
  unsigned int v1; // esi
  int n0x400000; // edi
  int v3; // ebx
  int v4; // eax
  int result; // eax
  int v6; // [esp-4h] [ebp-14h]

  v1 = a1 >> 22; /*0xffe07589*/
  n0x400000 = a1 & 0x3FFFFF; /*0xffe0758c*/
  do /*0xffe075c0*/
  {
    v3 = n0x400000 + PsfRegisterRead(1288, a1); /*0xffe0759a*/
    n0x400000 = 0x400000; /*0xffe0759d*/
    while ( 1 ) /*0xffe075a9*/
    {
      v4 = PsfRegisterRead(1288, v6); /*0xffe075a9*/
      a1 = v3 - v4; /*0xffe075b1*/
      if ( ((v3 - v4) & 0x800000) != 0 ) /*0xffe075b9*/
        break; /*0xffe075b9*/
      _mm_pause(); /*0xffe075a4*/
      v6 = v3 - v4; /*0xffe075a6*/
    }
    result = v1--; /*0xffe075bb*/
  }
  while ( result ); /*0xffe075c0*/
  return result; /*0xffe075c2*/
}