		Search-engine friendly clone of the ACL2 documentation.

Utils

Structures

x86-specific bit structures.

We define some bit structures using defbitstruct to describe the fields of registers and x86 data structures.

Subtopics

Rflagsbits: An 32-bit unsigned bitstruct type.
Cr4bits: An 26-bit unsigned bitstruct type.
Xcr0bits: An 64-bit unsigned bitstruct type.
Cr0bits: An 32-bit unsigned bitstruct type.
Prefixes: An 52-bit unsigned bitstruct type.
Ia32_eferbits: An 12-bit unsigned bitstruct type.
Evex-byte1: An 8-bit unsigned bitstruct type.
Cr3bits: An 64-bit unsigned bitstruct type.
Evex-byte3: An 8-bit unsigned bitstruct type.
Vex3-byte2: An 8-bit unsigned bitstruct type.
Vex3-byte1: An 8-bit unsigned bitstruct type.
Vex2-byte1: An 8-bit unsigned bitstruct type.
Evex-prefixes: An 32-bit unsigned bitstruct type.
Evex-byte2: An 8-bit unsigned bitstruct type.
Vex-prefixes: An 24-bit unsigned bitstruct type.
Sib: An 8-bit unsigned bitstruct type.
Modr/m-structures: Bitstruct definitions to store a ModR/M byte and its fields.
Vex-prefixes-layout-structures: Functions to decode and collect VEX prefix bytes from an x86 instruction.
Sib-structures: Bitstruct definitions to store a SIB byte and its fields.
Legacy-prefixes-layout-structure: Functions to collect legacy prefix bytes from an x86 instruction.
Evex-prefixes-layout-structures: Functions to decode and collect EVEX prefix bytes from an x86 instruction.
Cr8bits: An 4-bit unsigned bitstruct type.
Opcode-maps-structures: Structures for representing Intel's x86 Opcode Maps in ACL2
Segmentation-bitstructs: Bitstructs related to segmentation, protection, etc.
8bits: An 8-bit unsigned bitstruct type.
2bits: An 2-bit unsigned bitstruct type.
4bits: An 4-bit unsigned bitstruct type.
16bits: An 16-bit unsigned bitstruct type.
Paging-bitstructs: Bitstructs related to the paging data structures
3bits: An 3-bit unsigned bitstruct type.
11bits: An 11-bit unsigned bitstruct type.
40bits: An 40-bit unsigned bitstruct type.
5bits: An 5-bit unsigned bitstruct type.
32bits: An 32-bit unsigned bitstruct type.
19bits: An 19-bit unsigned bitstruct type.
10bits: An 10-bit unsigned bitstruct type.
7bits: An 7-bit unsigned bitstruct type.
64bits: An 64-bit unsigned bitstruct type.
54bits: An 54-bit unsigned bitstruct type.
45bits: An 45-bit unsigned bitstruct type.
36bits: An 36-bit unsigned bitstruct type.
31bits: An 31-bit unsigned bitstruct type.
24bits: An 24-bit unsigned bitstruct type.
22bits: An 22-bit unsigned bitstruct type.
17bits: An 17-bit unsigned bitstruct type.
13bits: An 13-bit unsigned bitstruct type.
12bits: An 12-bit unsigned bitstruct type.
6bits: An 6-bit unsigned bitstruct type.
Vex->x: Get the X field of vex-prefixes for the three-byte form, or 1 for the two-byte form.
Vex->b: Get the B field of vex-prefixes for the three-byte form, or 1 for the two-byte form.
Vex-prefixes-map-p: Returns t if the vex-prefixes, irrespective of whether they are two- or three-byte form, indicate the map that begins with the escape bytes bytes.
Vex-prefixes-byte0-p: Returns t if byte0 of the vex-prefixes structure is either *vex2-byte0* or *vex3-byte0*; returns nil otherwise.
Vex->w: Get the W field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.
Vex->vvvv: Get the VVVV field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.
Vex->r: Get the R field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.
Fp-bitstructs: Bitstructs related to floating-point operations
Cr4bits-debug
Vex->pp: Get the PP field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.
Vex->l: Get the L field of vex-prefixes; cognizant of the two- or three-byte VEX prefixes form.
Rflagsbits-debug
Evex->v-prime: Get the v-prime field of evex-prefixes.
Evex->z: Get the z field (embedded opmask) of evex-prefixes.
Evex->w: Get the W field of evex-prefixes.
Evex->vvvv: Get the VVVV field of evex-prefixes.
Evex->vl/rc: Get the vl/rc field of evex-prefixes.
Evex->pp: Get the PP field of evex-prefixes.
Evex->aaa: Get the aaa field (embedded opmask) of evex-prefixes.
Xcr0bits-debug
Vex3-byte1-equiv-under-mask
Vex3-byte2-equiv-under-mask
Vex2-byte1-equiv-under-mask
Vex-prefixes-equiv-under-mask
Rflagsbits-equiv-under-mask
Ia32_eferbits-equiv-under-mask
Evex-prefixes-equiv-under-mask
Evex-byte3-equiv-under-mask
Evex-byte2-equiv-under-mask
Evex-byte1-equiv-under-mask
Cr0bits-debug
Xcr0bits-equiv-under-mask
Sib-equiv-under-mask
Prefixes-equiv-under-mask
Cr8bits-equiv-under-mask
Cr4bits-equiv-under-mask
Cr3bits-equiv-under-mask
Cr0bits-equiv-under-mask
Vex3-byte1-debug
Prefixes-debug
Ia32_eferbits-debug
Evex-byte1-debug
Vex3-byte2-debug
Vex2-byte1-debug
Vex-prefixes-debug
Evex-prefixes-debug
Evex-byte3-debug
Evex-byte2-debug
Cr3bits-debug
Sib-debug
Cr8bits-debug