• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Ethereum
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • App-view
          • Top-level-memory
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
            • Read-operands-and-write-results
            • Effective-address-computations
            • Select-operand-size
            • Instruction-pointer-operations
            • Stack-pointer-operations
            • Select-segment-register
            • Prefix-modrm-sib-decoding
            • Select-address-size
            • Rex-byte-from-vex-prefixes
            • Check-instruction-length
            • Error-objects
            • Rip-guard-okp
            • Sib-decoding
          • Instructions
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Sha-2
      • Yul
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Axe
      • Poseidon
      • Where-do-i-place-my-book
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Machine

Decoding-and-spec-utils

Miscellaneous utilities for instruction decoding and for writing instruction specification functions

Subtopics

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.
Effective-address-computations
Computing effective address using ModR/M, SIB bytes, and displacement bytes present in the instruction
Select-operand-size
Selecting the operand size for general-purpose instructions
Instruction-pointer-operations
Operations to manipulate instruction pointers.
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.
Rex-byte-from-vex-prefixes
Calculate a REX byte from a VEX prefix.
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