• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
          • Effective-address-computations
          • Read-operands-and-write-results
            • X86-operand-from-modr/m-and-sib-bytes
            • Alignment-checking-enabled-p
            • X86-operand-to-reg/mem
            • X86-operand-to-xmm/mem
          • Instruction-pointer-operations
          • Select-operand-size
          • Stack-pointer-operations
          • Select-segment-register
          • Prefix-modrm-sib-decoding
          • Select-address-size
          • Check-instruction-length
          • Error-objects
          • Rip-guard-okp
          • Sib-decoding
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Decoding-and-spec-utils

Read-operands-and-write-results

Functions to fetch and read operands from an instruction, and to write results to appropriate registers/memory locations, based on ModR/M, SIB, immediate, and/or displacement bytes.

Definitions and Theorems

Function: alignment-checking-enabled-p

(defun alignment-checking-enabled-p (x86)
       (declare (xargs :stobjs (x86)))
       (declare (xargs :guard t))
       (let ((__function__ 'alignment-checking-enabled-p))
            (declare (ignorable __function__))
            (b* ((cr0 (the (unsigned-byte 32)
                           (n32 (ctri 0 x86))))
                 (am (cr0bits->am cr0))
                 (ac (flgi :ac x86))
                 (cpl (cpl x86)))
                (and (equal am 1)
                     (equal ac 1)
                     (equal cpl 3)))))

Theorem: booleanp-of-alignment-checking-enabled-p

(defthm booleanp-of-alignment-checking-enabled-p
        (b* ((enabled (alignment-checking-enabled-p x86)))
            (booleanp enabled))
        :rule-classes :type-prescription)

Theorem: alignment-checking-enabled-p-and-xw

(defthm
   alignment-checking-enabled-p-and-xw
   (implies
        (and (not (equal fld :ctr))
             (not (equal fld :seg-visible))
             (not (equal fld :rflags)))
        (equal (alignment-checking-enabled-p (xw fld index val x86))
               (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-ctr

(defthm
 alignment-checking-enabled-p-and-xw-ctr
 (implies
   (case-split (or (not (equal (nfix index) *cr0*))
                   (and (equal (nfix index) *cr0*)
                        (equal (cr0bits->am (loghead 32 val))
                               (cr0bits->am (xr :ctr *cr0* x86))))))
   (equal (alignment-checking-enabled-p (xw :ctr index val x86))
          (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-rflags

(defthm
 alignment-checking-enabled-p-and-xw-rflags
 (implies
      (equal (rflagsbits->ac val)
             (rflagsbits->ac (xr :rflags nil x86)))
      (equal (alignment-checking-enabled-p (xw :rflags nil val x86))
             (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-seg-visible

(defthm
 alignment-checking-enabled-p-and-xw-seg-visible
 (implies
  (case-split
   (or
    (not (equal index 1))
    (and (equal index 1)
         (equal (segment-selectorbits->rpl val)
                (segment-selectorbits->rpl (seg-visiblei 1 x86))))))
  (equal
      (alignment-checking-enabled-p (xw :seg-visible index val x86))
      (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-mv-nth-1-wb

(defthm
 alignment-checking-enabled-p-and-mv-nth-1-wb
 (equal
     (alignment-checking-enabled-p (mv-nth 1 (wb n addr w val x86)))
     (alignment-checking-enabled-p x86)))

Theorem: alignment-checking-enabled-p-and-mv-nth-2-rb

(defthm
  alignment-checking-enabled-p-and-mv-nth-2-rb
  (equal
       (alignment-checking-enabled-p (mv-nth 2 (rb n addr r-x x86)))
       (alignment-checking-enabled-p x86)))

Theorem: alignment-checking-enabled-p-and-mv-nth-2-las-to-pas

(defthm alignment-checking-enabled-p-and-mv-nth-2-las-to-pas
        (equal (alignment-checking-enabled-p
                    (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
               (alignment-checking-enabled-p x86)))

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 (unsigned-byte 1) reg-type)
          (type (member 1 2 4 6 8 10 16)
                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)
                        (cond ((equal reg-type 0)
                               (member operand-size '(1 2 4 8)))
                              (t (member operand-size '(4 8 16))))
                        (member operand-size
                                '(member 1 2 4 6 8 10 16)))))
 (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)
      (if (int= reg-type 0)
          (mv nil
              (rgfi-size operand-size (reg-index r/m rex-byte 0)
                         rex-byte x86)
              x86)
          (mv nil
              (xmmi-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))
          (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))
                    (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))
            (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))
          (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)))))))

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

Function: x86-operand-to-xmm/mem

(defun
 x86-operand-to-xmm/mem
 (proc-mode operand-size inst-ac? operand
            seg-reg addr rex-byte r/m mod x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (member 4 8 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?)
           (integer-range-p 0
                            *segment-register-names-len* seg-reg))))
 (declare (xargs :guard (unsigned-byte-p (ash operand-size 3)
                                         operand)))
 (let
  ((__function__ 'x86-operand-to-xmm/mem))
  (declare (ignorable __function__))
  (b*
   (((when (equal mod 3))
     (let* ((x86 (!xmmi-size operand-size (reg-index r/m rex-byte 0)
                             operand 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? nil)))
   (mv flg x86))))

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

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

Subtopics

X86-operand-from-modr/m-and-sib-bytes

Read an operand from memory or a register.

Alignment-checking-enabled-p

Checking if alignment is enabled

X86-operand-to-reg/mem

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

X86-operand-to-xmm/mem

Write an operand to memory or an XMM register.