• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • 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
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
            • Zmms-reads-and-writes
            • Gprs-reads-and-writes
              • Wr08
              • Wr16
              • Rr08
                • Wr32
                • !rgfi-size
                • Rgfi-size
                • Rr64
                • Wr64
                • Rr32
                • Rr16
              • Mmx-registers-reads-and-writes
              • Xmms-reads-and-writes
              • Rflags-reads-and-writes
              • Gpr-indices
              • Vex-vvvv-reg-index
              • Msr-reads-and-writes
              • Ctr-reads-and-writes
            • 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
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Gprs-reads-and-writes

    Rr08

    Read from byte general-purpose registers

    Signature
    (rr08 reg rex x86) → *

    Source: Intel Manuals, Vol. 1, Section 3.4.1.1 (General-Purpose Registers in 64-bit Mode)

    In 64-bit mode, there are limitations on accessing byte registers. An instruction cannot reference legacy high-bytes (for example: AH, BH, CH, DH) and one of the new byte registers at the same time (for example: the low byte of the RAX register). However, instructions may reference legacy low-bytes (for example: AL, BL, CL or DL) and new byte registers at the same time (for example: the low byte of the R8 register, or R8L). The architecture enforces this limitation by changing high-byte references (AH, BH, CH, DH) to low byte references (BPL, SPL, DIL, SIL: the low 8 bits for RBP, RSP, RDI and RSI) for instructions using a REX prefix.

    In other words, without the REX prefix, indices 0-7 refer to byte registers AL, CL, DL, BL, AH, CH, DH, and BH, whereas with the REX prefix, indices 0-15 refer to AL, CL, DL, BL, SPL, BPL, SIL, DIL, R8L, R9L, R10L, R11L, R12L, R13L, R14L, R15L. This applies to 64-bit mode.

    In 32-bit mode, this function is called with 0 as REX.

    Definitions and Theorems

    Function: rr08$inline

    (defun rr08$inline (reg rex x86)
     (declare (xargs :stobjs (x86)))
     (declare (type (unsigned-byte 4) reg)
              (type (unsigned-byte 8) rex))
     (declare (xargs :guard (reg-indexp reg rex)))
     (b* ((reg (mbe :logic (nfix reg) :exec reg)))
      (cond ((or (not (eql rex 0)) (< reg 4))
             (let ((qword (the (signed-byte 64) (rgfi reg x86))))
               (n08 qword)))
            (t (let ((qword (the (signed-byte 64)
                                 (rgfi (the (unsigned-byte 4) (- reg 4))
                                       x86))))
                 (mbe :logic (part-select qword :low 8 :width 8)
                      :exec (n08 (ash qword -8))))))))

    Theorem: n08p-rr08

    (defthm n08p-rr08
     (unsigned-byte-p 8 (rr08 reg rex x86))
     :rule-classes
     (:rewrite
      (:type-prescription
          :corollary (natp (rr08 reg rex x86))
          :hints
          (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
      (:linear
       :corollary (and (<= 0 (rr08 reg rex x86))
                       (< (rr08 reg rex x86) 256))
       :hints
       (("Goal"
            :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))