CoqToLeanAsm: x86 Macro Assembler in Lean 4

8.2. ModR/M byte in Detail

The ModR/M byte is the key to understanding x86 encoding. It packs three fields into a single byte:

 7   6   5   4   3   2   1   0
+---+---+---+---+---+---+---+---+
|  mod  |   reg/op  |    r/m    |
+---+---+---+---+---+---+---+---+

mod (bits 7-6) specifies the addressing modes:

  • 00 = Memory, no displacement (except special cases)

  • 01 = Memory + 8-bit signed displacement

  • 10 = Memory + 32-bit displacement

  • 11 = Register-to-register (no memory access)

reg/op (bits 5-3) holds either:

  • A register number (0-7) for two-operand instructions

  • An opcode extension for single-operand instructions (like INC, DEC, PUSH)

r/m (bits 2-0) specifies the destination:

  • With mod=11: register number (0-7)

  • With mod≠11: addressing mode (100=SIB follows, 101=disp32 with mod=00)

8.2.1. Register Encoding Table

| Register | Encoding | As r/m with mod=11 | |----------|----------|-------------------| | EAX/AX/AL | 000 (0) | Direct register | | ECX/CX/CL | 001 (1) | Direct register | | EDX/DX/DL | 010 (2) | Direct register | | EBX/BX/BL | 011 (3) | Direct register | | ESP/SP/AH | 100 (4) | SIB byte follows | | EBP/BP/CH | 101 (5) | disp32 if mod=00 | | ESI/SI/DH | 110 (6) | Direct register | | EDI/DI/BH | 111 (7) | Direct register |

8.2.2. Example: MOV EAX, EBX (0x89 0xD8)

[137#8, 216#8]#eval encode 0 (Instr.MOVOP OpSize.Op32 (DstSrc.RR EAX EBX))

Breaking down 0xD8:

  • Binary: 11 011 000

  • mod = 11 (register-to-register)

  • reg = 011 (EBX = 3, the source)

  • r/m = 000 (EAX = 0, the destination)

8.2.3. Example: MOV EBX, EAX (0x89 0xC3)

[137#8, 195#8]#eval encode 0 (Instr.MOVOP OpSize.Op32 (DstSrc.RR EBX EAX))

Breaking down 0xC3:

  • Binary: 11 000 011

  • mod = 11 (register-to-register)

  • reg = 000 (EAX = 0, the source)

  • r/m = 011 (EBX = 3, the destination)