• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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

Wr08

Writing to byte general-purpose registers

Signature

(wr08 reg rex byte x86) → x86

Note Intel Vol. 1 Sec. 3.4.1.1 p. 3-17, which says the following about 64-bit mode:

8-bit and 16-bit operands generate an 8-bit or 16-bit result. The upper 56 or 48 bits (respectively) of the destination general-purpose register are not modified by the operation.

This is also confirmed by AMD manual, Jun'15, Vol. 3, App. B.1, under ‘No Extension of 8-Bit and 16-Bit Results’.

In 32-bit mode, the upper 32 bits are undefined, as specified by the following quote from the same page as above:

Because the upper 32 bits of 64-bit general-purpose registers are undefined in 32-bit modes, the upper 32 bits of any general-purpose register are not preserved when switching from 64-bit mode to a 32-bit mode (to protected mode or compatibility mode). Software must not depend on these bits to maintain a value after a 64-bit to 32-bit mode switch.

In 32-bit mode, this function is called with 0 as REX. Since in 32-bit mode the high 32 bits of general-purpose registers are not accessible, it is fine for this function to leave those bits unchanged, as opposed to, for example, setting them to undefined values as done by the semantic functions of certain instructions for certain flags. The switching from 32-bit mode to 64-bit mode (when modeled) will set the high 32 bits of general-purpose registers to undefined values.

Definitions and Theorems

Function: wr08$inline

(defun wr08$inline (reg rex byte x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 4) reg)
          (type (unsigned-byte 8) rex)
          (type (unsigned-byte 8) byte))
 (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))))
     (!rgfi
      reg
      (n64-to-i64
       (mbe
        :logic (part-install byte
                             (part-select qword :low 0 :width 64)
                             :low 0
                             :width 8)
        :exec (the (unsigned-byte 64)
                   (logior (the (unsigned-byte 64)
                                (logand 18446744073709551360 qword))
                           byte))))
      x86)))
   (t
    (let* ((index (the (unsigned-byte 4)
                       (- (the (unsigned-byte 4) reg) 4)))
           (qword (the (signed-byte 64)
                       (rgfi index x86))))
     (!rgfi
      index
      (n64-to-i64
       (mbe
        :logic (part-install byte
                             (part-select qword :low 0 :width 64)
                             :low 8
                             :width 8)
        :exec (the (unsigned-byte 64)
                   (logior (the (unsigned-byte 64)
                                (logand 18446744073709486335 qword))
                           (the (unsigned-byte 16)
                                (ash byte 8))))))
      x86))))))

Theorem: x86p-wr08

(defthm x86p-wr08
  (implies (x86p x86)
           (x86p (wr08 reg rex byte x86))))