• 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
          • Read-operands-and-write-results
            • X86-operand-from-modr/m-and-sib-bytes
            • Alignment-checking-enabled-p
            • X86-operand-to-zmm/mem
            • X86-operand-to-reg/mem
            • X86-operand-to-xmm/mem
          • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Read-operands-and-write-results

X86-operand-to-reg/mem

Write an operand to memory or a general-purpose register.

Signature

(x86-operand-to-reg/mem proc-mode operand-size 
                        inst-ac? memory-ptr? operand 
                        seg-reg addr rex-byte r/m mod x86) 
 
  → 
(mv * x86)

Arguments

inst-ac? — t if instruction does alignment checking, nil otherwise.
    Guard (booleanp inst-ac?).

memory-ptr? — t if the operand is a memory operand of the form m16:16, m16:32, or m16:64.
    Guard (booleanp memory-ptr?).

seg-reg — Register of the segment to read the operand from (when reading the operand from memory).
    Guard (integer-range-p 0 *segment-register-names-len* seg-reg).

Based on the ModR/M byte, the operand is written to either a register or memory. The address argument of this function is often the effective address calculated and returned by x86-operand-from-modr/m-and-sib-bytes.

Definitions and Theorems

Function: x86-operand-to-reg/mem

(defun x86-operand-to-reg/mem
       (proc-mode operand-size
                  inst-ac? memory-ptr? operand
                  seg-reg addr rex-byte r/m mod x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (member 1 2 4 6 8 10 16)
                operand-size)
          (type (integer 0 *) operand)
          (type (signed-byte 64) addr)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 3) r/m)
          (type (unsigned-byte 2) mod))
 (declare
  (xargs
      :guard
      (and (booleanp inst-ac?)
           (booleanp memory-ptr?)
           (integer-range-p 0
                            *segment-register-names-len* seg-reg))))
 (declare
      (xargs :guard (and (unsigned-byte-p (ash operand-size 3)
                                          operand)
                         (if (equal mod 3)
                             (member operand-size '(member 1 2 4 8))
                           (member operand-size
                                   '(member 1 2 4 6 8 10 16))))))
 (let ((__function__ 'x86-operand-to-reg/mem))
  (declare (ignorable __function__))
  (b*
   (((when (equal mod 3))
     (let* ((x86 (!rgfi-size operand-size (reg-index r/m rex-byte 0)
                             operand rex-byte x86)))
       (mv nil x86)))
    (check-alignment? (and inst-ac?
                           (alignment-checking-enabled-p x86)))
    ((mv flg x86)
     (wme-size proc-mode operand-size addr
               seg-reg operand check-alignment? x86
               :mem-ptr? memory-ptr?)))
   (mv flg x86))))

Theorem: x86p-x86-operand-to-reg/mem

(defthm x86p-x86-operand-to-reg/mem
 (implies
  (force (x86p x86))
  (x86p
   (mv-nth
      1
      (x86-operand-to-reg/mem proc-mode operand-size
                              inst-ac? memory-ptr? operand
                              addr seg-reg rex-byte r/m mod x86)))))