• 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
      • Booting-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

Wr16

Write to word general-purpose registers

Signature

(wr16 reg val 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.

This function is used both in 64-bit mode and in 32-bit mode. 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: wr16$inline

(defun wr16$inline (reg val x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 4) reg)
          (type (unsigned-byte 16) val))
 (let ((qword (the (signed-byte 64) (rgfi reg x86))))
  (!rgfi
   reg
   (n64-to-i64
    (mbe
       :logic (part-install val (part-select qword :low 0 :width 64)
                            :low 0
                            :width 16)
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand qword 18446744073709486080))
                          val))))
   x86)))

Theorem: x86p-wr16

(defthm x86p-wr16
  (implies (x86p x86)
           (x86p (wr16 reg val x86))))