• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
        • App-view
        • Top-level-memory
        • 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
            • X86-operand-to-mmx/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-from-modr/m-and-sib-bytes

Read an operand from memory or a register.

Signature

(x86-operand-from-modr/m-and-sib-bytes 
     proc-mode reg-type operand-size inst-ac? 
     memory-ptr? seg-reg p4? temp-rip 
     rex-byte r/m mod sib num-imm-bytes x86) 
 
  → 
(mv flg operand increment-rip-by addr x86)

Arguments

reg-type — reg-type is *gpr-access* for GPRs, *xmm-access* for XMMs (non-VEX-encoded), *vex-xmm-access* for XMMs (VEX-encoded), *ymm-access* for YMMs, and *mmx-access*) or MMXs. (@('*zmm-access*, for ZMMs, is not yet supported.

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).

p4? — Address-Size Override Prefix Present?.

Returns

operand — Type (natp operand).

x86 — Type (x86p x86), given (force (x86p x86)).

Based on the ModR/M byte, the operand is read from either a register or memory. In the latter case, we calculate the effective address and then we read the operand from it. Besides returning the operand, we also return the calculated effective address. This is useful for instructions that modify the operand after reading it (e.g. the source/destination operand of ADD), which pass the effective address calculated by this function to x86-operand-to-reg/mem (which writes the result to memory).

Definitions and Theorems

Function: x86-operand-from-modr/m-and-sib-bytes

(defun x86-operand-from-modr/m-and-sib-bytes
       (proc-mode reg-type operand-size inst-ac?
                  memory-ptr? seg-reg p4? temp-rip
                  rex-byte r/m mod sib num-imm-bytes x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (member 0 1 2 3 5) reg-type)
          (type (member 1 2 4 6 8 10 16 32)
                operand-size)
          (type (or t nil) p4?)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 3) r/m)
          (type (unsigned-byte 2) mod)
          (type (unsigned-byte 8) sib)
          (type (unsigned-byte 3) num-imm-bytes))
 (declare
  (xargs
      :guard
      (and (booleanp inst-ac?)
           (booleanp memory-ptr?)
           (integer-range-p 0
                            *segment-register-names-len* seg-reg))))
 (declare (xargs :guard
                 (if (equal mod 3)
                     (case reg-type
                       (0 (member operand-size '(1 2 4 8)))
                       (1 (member operand-size '(4 8 16)))
                       (2 (member operand-size '(4 8 16)))
                       (3 (member operand-size '(4 8 16 32)))
                       (5 (equal operand-size 8))
                       (t t))
                   (member operand-size
                           '(member 1 2 4 6 8 10 16 32)))))
 (let ((__function__ 'x86-operand-from-modr/m-and-sib-bytes))
  (declare (ignorable __function__))
  (b*
   (((mv ?flg0 (the (signed-byte 64) addr)
         (the (integer 0 4) increment-rip-by)
         x86)
     (if (equal mod 3)
         (mv nil 0 0 x86)
       (x86-effective-addr proc-mode p4? temp-rip rex-byte
                           r/m mod sib num-imm-bytes x86)))
    ((when flg0)
     (mv (cons 'x86-effective-addr-error flg0)
         0 0 0 x86))
    ((mv ?flg2 operand x86)
     (if (equal mod 3)
         (case reg-type
           (0 (mv nil
                  (rgfi-size operand-size (reg-index r/m rex-byte 0)
                             rex-byte x86)
                  x86))
           (5 (mv nil (mmx r/m x86) x86))
           (1 (mv nil
                  (xmmi-size operand-size (reg-index r/m rex-byte 0)
                             x86)
                  x86))
           (t (mv nil
                  (zmmi-size operand-size (reg-index r/m rex-byte 0)
                             x86)
                  x86)))
      (b*
       ((check-alignment? (and inst-ac?
                               (alignment-checking-enabled-p x86))))
       (rme-size-opt proc-mode operand-size
                     addr seg-reg :r check-alignment? x86
                     :mem-ptr? memory-ptr?
                     :check-canonicity t))))
    ((when flg2)
     (mv (cons 'rm-size-error flg2)
         0 0 0 x86)))
   (mv nil
       operand increment-rip-by addr x86))))

Theorem: natp-of-x86-operand-from-modr/m-and-sib-bytes.operand

(defthm natp-of-x86-operand-from-modr/m-and-sib-bytes.operand
  (b* (((mv ?flg
            ?operand ?increment-rip-by ?addr ?x86)
        (x86-operand-from-modr/m-and-sib-bytes
             proc-mode reg-type
             operand-size inst-ac? memory-ptr?
             seg-reg p4? temp-rip rex-byte
             r/m mod sib num-imm-bytes x86)))
    (natp operand))
  :rule-classes :type-prescription)

Theorem: x86p-of-x86-operand-from-modr/m-and-sib-bytes.x86

(defthm x86p-of-x86-operand-from-modr/m-and-sib-bytes.x86
  (implies (force (x86p x86))
           (b* (((mv ?flg
                     ?operand ?increment-rip-by ?addr ?x86)
                 (x86-operand-from-modr/m-and-sib-bytes
                      proc-mode reg-type
                      operand-size inst-ac? memory-ptr?
                      seg-reg p4? temp-rip rex-byte
                      r/m mod sib num-imm-bytes x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Theorem: bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand

(defthm
    bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand
 (implies
     (and (equal bound (ash operand-size 3))
          (member operand-size '(1 2 4 8 16 32))
          (or (not (equal reg-type 5))
              (equal operand-size 8))
          (x86p x86))
     (unsigned-byte-p bound
                      (mv-nth 1
                              (x86-operand-from-modr/m-and-sib-bytes
                                   proc-mode reg-type
                                   operand-size inst-ac? memory-ptr?
                                   seg-reg p4? temp-rip rex-byte
                                   r/m mod sib num-imm-bytes x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (and (equal bound (ash operand-size 3))
                    (member operand-size '(1 2 4 8 16 32))
                    (or (not (equal reg-type 5))
                        (equal operand-size 8))
                    (x86p x86))
               (natp (mv-nth 1
                             (x86-operand-from-modr/m-and-sib-bytes
                                  proc-mode reg-type
                                  operand-size inst-ac? memory-ptr?
                                  seg-reg p4? temp-rip rex-byte
                                  r/m mod sib num-imm-bytes x86))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies
       (and (equal bound (ash operand-size 3))
            (member operand-size '(1 2 4 8 16 32))
            (or (not (equal reg-type 5))
                (equal operand-size 8))
            (x86p x86))
       (and (<= 0
                (mv-nth 1
                        (x86-operand-from-modr/m-and-sib-bytes
                             proc-mode reg-type
                             operand-size inst-ac? memory-ptr?
                             seg-reg p4? temp-rip rex-byte
                             r/m mod sib num-imm-bytes x86)))
            (< (mv-nth 1
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4? temp-rip
                            rex-byte r/m mod sib num-imm-bytes x86))
               (expt 2 bound))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: bigger-bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand

(defthm
 bigger-bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand
 (implies
     (and (<= (ash operand-size 3) bound)
          (member operand-size '(1 2 4 8 16 32))
          (or (not (equal reg-type 5))
              (equal operand-size 8))
          (integerp bound)
          (x86p x86))
     (unsigned-byte-p bound
                      (mv-nth 1
                              (x86-operand-from-modr/m-and-sib-bytes
                                   proc-mode reg-type
                                   operand-size inst-ac? memory-ptr?
                                   seg-reg p4? temp-rip rex-byte
                                   r/m mod sib num-imm-bytes x86))))
 :rule-classes (:rewrite))

Theorem: bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand-6-and-10-bytes-read

(defthm
 bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand-6-and-10-bytes-read
 (implies
     (and (equal bound (ash operand-size 3))
          (member operand-size '(6 10))
          (not (equal mod 3))
          (x86p x86))
     (unsigned-byte-p bound
                      (mv-nth 1
                              (x86-operand-from-modr/m-and-sib-bytes
                                   proc-mode reg-type
                                   operand-size inst-ac? memory-ptr?
                                   seg-reg p4? temp-rip rex-byte
                                   r/m mod sib num-imm-bytes x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (and (equal bound (ash operand-size 3))
                    (member operand-size '(6 10))
                    (not (equal mod 3))
                    (x86p x86))
               (natp (mv-nth 1
                             (x86-operand-from-modr/m-and-sib-bytes
                                  proc-mode reg-type
                                  operand-size inst-ac? memory-ptr?
                                  seg-reg p4? temp-rip rex-byte
                                  r/m mod sib num-imm-bytes x86))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies
       (and (equal bound (ash operand-size 3))
            (member operand-size '(6 10))
            (not (equal mod 3))
            (x86p x86))
       (and (<= 0
                (mv-nth 1
                        (x86-operand-from-modr/m-and-sib-bytes
                             proc-mode reg-type
                             operand-size inst-ac? memory-ptr?
                             seg-reg p4? temp-rip rex-byte
                             r/m mod sib num-imm-bytes x86)))
            (< (mv-nth 1
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4? temp-rip
                            rex-byte r/m mod sib num-imm-bytes x86))
               (expt 2 bound))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: integerp-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-type-prescription

(defthm
 integerp-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-type-prescription
 (implies
      (force (x86p x86))
      (natp (mv-nth 2
                    (x86-operand-from-modr/m-and-sib-bytes
                         proc-mode reg-type operand-size inst-ac?
                         memory-ptr? seg-reg p4 temp-rip rex-byte
                         r/m mod sib num-imm-bytes x86))))
 :rule-classes :type-prescription)

Theorem: mv-nth-2-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-linear<=4

(defthm
 mv-nth-2-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-linear<=4
 (implies (x86p x86)
          (<= (mv-nth 2
                      (x86-operand-from-modr/m-and-sib-bytes
                           proc-mode reg-type operand-size
                           inst-ac? memory-ptr? seg-reg p4 temp-rip
                           rex-byte r/m mod sib num-imm-bytes x86))
              4))
 :rule-classes :linear)

Theorem: i48p-x86-operand-from-modr/m-and-sib-bytes

(defthm i48p-x86-operand-from-modr/m-and-sib-bytes
 (implies (forced-and (x86p x86))
          (signed-byte-p
               48
               (mv-nth 2
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (implies
     (forced-and (x86p x86))
     (integerp (mv-nth 2
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86))))
   :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
   :corollary
   (implies
      (forced-and (x86p x86))
      (and (<= -140737488355328
               (mv-nth 2
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86)))
           (< (mv-nth 2
                      (x86-operand-from-modr/m-and-sib-bytes
                           proc-mode reg-type operand-size
                           inst-ac? memory-ptr? seg-reg p4 temp-rip
                           rex-byte r/m mod sib num-imm-bytes x86))
              140737488355328)))
   :hints
   (("Goal"
         :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

Theorem: i64p-x86-operand-from-modr/m-and-sib-bytes

(defthm i64p-x86-operand-from-modr/m-and-sib-bytes
 (implies (forced-and (x86p x86))
          (signed-byte-p
               64
               (mv-nth 3
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (implies
     (forced-and (x86p x86))
     (integerp (mv-nth 3
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86))))
   :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
   :corollary
   (implies
      (forced-and (x86p x86))
      (and (<= -9223372036854775808
               (mv-nth 3
                       (x86-operand-from-modr/m-and-sib-bytes
                            proc-mode reg-type operand-size inst-ac?
                            memory-ptr? seg-reg p4 temp-rip rex-byte
                            r/m mod sib num-imm-bytes x86)))
           (< (mv-nth 3
                      (x86-operand-from-modr/m-and-sib-bytes
                           proc-mode reg-type operand-size
                           inst-ac? memory-ptr? seg-reg p4 temp-rip
                           rex-byte r/m mod sib num-imm-bytes x86))
              9223372036854775808)))
   :hints
   (("Goal"
         :in-theory '(signed-byte-p integer-range-p (:e expt)))))))