// PopulateDiskInfoRecords - decompiled from Platform.efi
__int64 PopulateDiskInfoRecords()
{
  CHAR16 *ZeroPool_1; // r15
  _BYTE *Node_2; // rdi
  __int64 n310; // rdx
  __int64 result; // rax
  unsigned __int64 v4; // rsi
  __int64 v5; // rax
  const void *Node; // rbx
  const void *i; // rcx
  char n23; // al
  bool v9; // zf
  char n2; // bl
  __int64 v11; // rax
  UINTN AllocationSize; // rcx
  unsigned int n512; // edi
  _WORD *CopyPool; // rax
  _WORD *CopyPool_1; // rsi
  __int64 v16; // rax
  char *Gen1; // rcx
  unsigned __int16 v18; // r11
  unsigned int n0x28; // eax
  __int64 n0x28_1; // r8
  __int64 v21; // r10
  char v22; // r9
  unsigned __int64 v23; // rbx
  unsigned __int64 v24; // rbx
  unsigned __int16 *v25; // r12
  unsigned __int64 n16; // r13
  __int64 n3; // r14
  __int64 v28; // rdi
  unsigned __int64 v29; // rbx
  const __int16 *___ATAPI; // r8
  int n512_1; // [rsp+30h] [rbp-49h] BYREF
  _BYTE v32[4]; // [rsp+34h] [rbp-45h] BYREF
  __int64 v33; // [rsp+38h] [rbp-41h] BYREF
  __int64 v34; // [rsp+40h] [rbp-39h] BYRE... [8524 chars total]