// VariableServicesInit - decompiled from Platform.efi
__int64 VariableServicesInit()
{
  __int64 v0; // rax
  __int64 n64; // rdx
  __int64 v2; // rax
  __int64 v3; // rax
  __int64 n64_1; // rdx
  __int64 v5; // rax
  __int64 v6; // rax
  __int64 v7; // rbx
  __int64 v8; // rax
  __int64 v9; // rbx
  __int64 v10; // rax
  __int64 v11; // rbx
  __int64 Value; // rbx
  int n7777; // r9d
  unsigned int *v14; // rcx
  __int64 v15; // r8
  unsigned int *v16; // rdx
  __int64 v17; // rax
  __int64 v18; // rdi
  unsigned int *v19; // rcx
  __int64 v20; // r10
  __int64 v21; // r9
  unsigned int *v22; // rdx
  __int64 v23; // r8
  int n7777_1; // r11d
  __int64 v25; // rax
  __int64 n64_2; // rdx
  __int64 v27; // rax
  __int64 v28; // rax
  __int64 n64_3; // rdx
  __int64 v30; // rax
  __int64 Buffer; // rax
  __int64 v32; // [rsp+30h] [rbp-30h] BYREF
  char v33[8]; // [rsp+38h] [rbp-28h] BYREF
  _DWORD Port[4]; // [rsp+40h] [rbp-20h] BYREF
  _DWORD Port_1[4]; // [rsp+50h] [rbp-10h] BYREF
  char v36; // [rsp+A0h] [rbp+40h] BYREF
  __int64 v37; ... [9418 chars total]