6.1. General Purpose Registers

The eight 32-bit general purpose registers (GPRs) are defined by Reg:

X86.EAX : Reg#check EAX  -- Accumulator (encoding 0)
X86.ECX : Reg#check ECX  -- Counter (encoding 1)
X86.EDX : Reg#check EDX  -- Data (encoding 2)
X86.EBX : Reg#check EBX  -- Base (encoding 3)
X86.ESP : Reg#check ESP  -- Stack Pointer (encoding 4)
X86.EBP : Reg#check EBP  -- Base Pointer (encoding 5)
X86.ESI : Reg#check ESI  -- Source Index (encoding 6)
X86.EDI : Reg#check EDI  -- Destination Index (encoding 7)

The NonSPReg type excludes ESP, which cannot be used as an index in SIB byte addressing.

Each register's encoding is accessed via Reg.toNat:

0#eval EAX.toNat  -- 0
1#eval ECX.toNat  -- 1
4#eval ESP.toNat  -- 4