// InternalRShift64 - addr:0xffdaf459
unsigned __int64 __cdecl InternalRShift64(unsigned __int64 a1)
{
  unsigned int n0x40; // ecx
  int PeiServicesPpi; // eax
  unsigned __int64 v3; // rax
  char n0x40_1; // [esp+0h] [ebp-4h]

  n0x40_1 = n0x40;
  if ( n0x40 >= 0x40 )
  {
    PeiServicesPpi = GetPeiServicesPpi();
    if ( PeiServicesPpi )
      (*(void (__cdecl **)(const char *, int, const char *))(PeiServicesPpi + 4))(
        "e:\\hs\\MdePkg\\Library\\BaseLib\\RShiftU64.c",
        39,
        "Count < 64");
  }
  v3 = HIDWORD(a1);
  if ( (n0x40_1 & 0x20) == 0 )
    v3 = a1;
  return v3 >> (n0x40_1 & 0x1F);
}