• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Introduction
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • Syscalls
          • Cpuid
          • X86isa-state
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
            • Effective-address-computations
            • Read-operands-and-write-results
            • Instruction-pointer-operations
            • Select-operand-size
            • Stack-pointer-operations
            • Select-segment-register
            • Prefix-modrm-sib-decoding
            • Select-address-size
            • Check-instruction-length
            • Error-objects
            • Rip-guard-okp
            • Sib-decoding
          • Instructions
          • X86-modes
          • Segmentation
          • Register-readers-and-writers
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • Proof-utilities
        • To-do
        • Concrete-simulation-examples
        • Model-validation
        • Utils
        • Debugging-code-proofs
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • Machine

Decoding-and-spec-utils

Miscellaneous utilities for instruction decoding and for writing instruction specification functions

Subtopics

Effective-address-computations
Computing effective address using ModR/M, SIB bytes, and displacement bytes present in the instruction
Read-operands-and-write-results
Functions to fetch and read operands from an instruction, and to write results to appropriate registers/memory locations, based on ModR/M, SIB, immediate, and/or displacement bytes.
Instruction-pointer-operations
Operations to manipulate instruction pointers.
Select-operand-size
Selecting the operand size for general-purpose instructions
Stack-pointer-operations
Operations to manipulate stack pointers.
Select-segment-register
Segment register to use for an instruction operand in memory.
Prefix-modrm-sib-decoding
Decoding utilities for the prefixes, ModR/M, and SIB bytes
Select-address-size
Address size of an instruction, in bytes.
Check-instruction-length
Check if the length of an instruction exceeds 15 bytes.
Error-objects
Utilities trafficking in erp objects
Rip-guard-okp
Size constraints on a memory address of some instruction byte
Sib-decoding
Functions to detect and decode SIB bytes