Module X86Types

module X86Types: sig .. end

The X86 machine language

Register sets

type reg8 =

`\|`	`AL`
`\|`	`CL`
`\|`	`DL`
`\|`	`BL`
`\|`	`AH`
`\|`	`CH`
`\|`	`DH`
`\|`	`BH`

General-purpose 8-bit registers

type reg16 =

`\|`	`AX`
`\|`	`CX`
`\|`	`DX`
`\|`	`BX`
`\|`	`SP`
`\|`	`BP`
`\|`	`SI`
`\|`	`DI`

General-purpose 16-bit registers

type reg32 =

`\|`	`EAX`
`\|`	`ECX`
`\|`	`EDX`
`\|`	`EBX`
`\|`	`ESP`
`\|`	`EBP`
`\|`	`ESI`
`\|`	`EDI`

General-purpose 32-bit registers

val nRegs32 : int

Number of 32-bit registers

type segment_reg =

`\|`	`ES`
`\|`	`CS`
`\|`	`SS`
`\|`	`DS`
`\|`	`FS`
`\|`	`GS`

Segment registers

type float_reg =

`\|`	`ST0`
`\|`	`ST1`
`\|`	`ST2`
`\|`	`ST3`
`\|`	`ST4`
`\|`	`ST5`
`\|`	`ST6`
`\|`	`ST7`

Floating-point registers

type mmx_reg =

`\|`	`MM0`
`\|`	`MM1`
`\|`	`MM2`
`\|`	`MM3`
`\|`	`MM4`
`\|`	`MM5`
`\|`	`MM6`
`\|`	`MM7`

MMX registers

type control_reg =

`\|`	`CR0`
`\|`	`CR2`
`\|`	`CR3`
`\|`	`CR4`

Control registers

type debug_reg =

`\|`	`DR0`
`\|`	`DR1`
`\|`	`DR2`
`\|`	`DR3`
`\|`	`DR6`
`\|`	`DR7`

Debug registers

type test_reg =

`\|`	`TR3`
`\|`	`TR4`
`\|`	`TR5`
`\|`	`TR6`
`\|`	`TR7`

Test registers

Flags

Condition codes

type flag =

`\|`	`ID`
`\|`	`VIP`
`\|`	`VIF`
`\|`	`AC`
`\|`	`VM`
`\|`	`RF`
`\|`	`NT`
`\|`	`IOPL`
`\|`	`OF`
`\|`	`DF`
`\|`	`IF_flag`
`\|`	`TF`
`\|`	`SF`
`\|`	`ZF`
`\|`	`AF`
`\|`	`PF`
`\|`	`CF`

Flags

type condition =

`\|`	`O`
`\|`	`B`
`\|`	`Z`
`\|`	`BE`
`\|`	`S`
`\|`	`P`
`\|`	`L`
`\|`	`LE`

Basic conditions

type ('a, 'b) prod =

`\|`	`Pair of 'a * 'b`

A normal type for pairs, since Coq extraction can't seem to produce code that uses built-in tuple types.

type cc = (bool, condition) prod

A condition code is a pair of a basic condition and a boolean indicating whether that condition is true.

val nCcs : int

Number of distinct condition codes

SSE

type sse =

`\|`	`SseEQ`
`\|`	`SseLT`
`\|`	`SseLE`
`\|`	`SseUNORD`
`\|`	`SseNEQ`
`\|`	`SseNLT`
`\|`	`SseNLE`
`\|`	`SseORD`

SSE tests

Addresses

type scale =

`\|`	`Scale1`
`\|`	`Scale2`
`\|`	`Scale4`
`\|`	`Scale8`

Scales for integer operations

type address = {

`addrDisp : int64;`	`(*`	Constant displacement	`*)`
`addrBase : reg32 option;`	`(*`	Optional base register	`*)`
`addrIndex : (scale, reg32) prod option;`	`(*`	Optional index register, along with a scaling factor by which to multiply it	`*)`

}

The memory address format supported by the machine language

Operands

type 'a genop =

`\|`	`Imm of int64`	`(*`	A constant machine integer	`*)`
`\|`	`Reg of 'a`	`(*`	A register	`*)`
`\|`	`Address of address`	`(*`	A memory dereference	`*)`

Generic instruction operands, indexed by the relevant register set

type genop32 = reg32 genop

type genop8 = reg8 genop

Specializations to particular register sets

Operations

type arith_op =

`\|`	`Add`
`\|`	`And`
`\|`	`Or`
`\|`	`Sub`

Arithmetic operations

type shift_op =

`\|`	`Shl`
`\|`	`Shr`

Bitwise shift operations

Instructions

type instr =

`\|`	`Arith of arith_op * genop32 * genop32`
`\|`	`Arithb of arith_op * genop8 * genop8`
`\|`	`Call of genop32`
`\|`	`Cmp of genop32 * genop32`
`\|`	`Inc of genop32`
`\|`	`Jcc of cc * int64`
`\|`	`Jmp of int64`
`\|`	`Lea of reg32 * address`
`\|`	`Leave`
`\|`	`Mov of genop32 * genop32`
`\|`	`Movb of genop8 * genop8`
`\|`	`Pop of genop32`
`\|`	`Push of genop32`
`\|`	`Ret`
`\|`	`Shift of shift_op * genop32 * genop8`

The actual instructions. These follow the standard x86 instruction set.