• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Instructions
          • X86-modes
          • Segmentation
          • Register-readers-and-writers
            • Zmms-reads-and-writes
            • Gprs-reads-and-writes
              • Wr08
              • Wr16
              • Wr32
              • Rr08
              • !rgfi-size
              • Rgfi-size
              • Rr64
              • Wr64
              • Rr32
              • Rr16
            • Mmx-registers-reads-and-writes
            • Xmms-reads-and-writes
            • Rflags-reads-and-writes
            • Gpr-indices
          • 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
  • Register-readers-and-writers

Gprs-reads-and-writes

Functions to read/write 8/16/32/64 bits into the registers

rr08, rr16, rr32, and rr64 will read the contents of the GPRs as natural numbers. Remember that rgfi will return an i64p value.

Here is an example:


(!rgfi 0 -1 x86) ;; Write -1 to register 0

(rr64 0 x86) returns 18446744073709551615 and (rgfi 0 x86) returns -1. Note that 18446744073709551615 is a bignum in CCL. This is precisely the reason why we declared registers as i64p instead of n64p; -1 would be stored as a bignum if the registers were n64p.

Similarly, wr08, wr16, wr32, and wr64 are used to write natural numbers into the GPRs.

Definitions and Theorems

Function: rr08$inline

(defun
 rr08$inline (reg rex x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 4) reg)
          (type (unsigned-byte 8) rex))
 (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))))
              (n08 qword)))
        (t (let ((qword (the (signed-byte 64)
                             (rgfi (the (unsigned-byte 4) (- reg 4))
                                   x86))))
                (mbe :logic (part-select qword :low 8 :width 8)
                     :exec (n08 (ash qword -8))))))))

Theorem: n08p-rr08

(defthm
 n08p-rr08
 (unsigned-byte-p 8 (rr08 reg rex x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rr08 reg rex x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rr08 reg rex x86))
                   (< (rr08 reg rex x86) 256))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

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

Theorem: loghead-logtail-logext-for-rr08/wr08

(defthm loghead-logtail-logext-for-rr08/wr08
        (implies (integerp x)
                 (equal (loghead 8 (logtail 8 (logext 64 x)))
                        (loghead 8 (logtail 8 x)))))

Theorem: rr08-wr08-same

(defthm rr08-wr08-same
        (equal (rr08 reg rex (wr08 reg rex byte x86))
               (loghead 8 byte)))

Theorem: rr08-wr08-different

(defthm rr08-wr08-different
        (implies (not (equal (nfix reg1) (nfix reg2)))
                 (equal (rr08 reg1 rex1 (wr08 reg2 rex2 byte x86))
                        (rr08 reg1 rex1 x86))))

Function: rr16$inline

(defun rr16$inline (reg x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) reg))
       (n16 (the (signed-byte 64) (rgfi reg x86))))

Theorem: n16p-rr16

(defthm
 n16p-rr16
 (unsigned-byte-p 16 (rr16 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rr16 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rr16 reg x86))
                   (< (rr16 reg x86) 65536))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

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

Theorem: rr16-wr16-same

(defthm rr16-wr16-same
        (equal (rr16 reg (wr16 reg val x86))
               (loghead 16 val)))

Theorem: rr16-wr16-different

(defthm rr16-wr16-different
        (implies (not (equal (nfix reg1) (nfix reg2)))
                 (equal (rr16 reg1 (wr16 reg2 val x86))
                        (rr16 reg1 x86))))

Function: rr32$inline

(defun rr32$inline (reg x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) reg))
       (n32 (the (signed-byte 64) (rgfi reg x86))))

Theorem: n32p-rr32

(defthm
 n32p-rr32
 (unsigned-byte-p 32 (rr32 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rr32 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rr32 reg x86))
                   (< (rr32 reg x86) 4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: wr32$inline

(defun wr32$inline (reg val x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) reg)
                (type (unsigned-byte 32) val))
       (!rgfi reg (mbe :logic (n32 val) :exec val)
              x86))

Theorem: x86p-wr32

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

Theorem: rr32-wr32-same

(defthm rr32-wr32-same
        (equal (rr32 reg (wr32 reg val x86))
               (loghead 32 val)))

Theorem: rr32-wr32-different

(defthm rr32-wr32-different
        (implies (not (equal (nfix reg1) (nfix reg2)))
                 (equal (rr32 reg1 (wr32 reg2 val x86))
                        (rr32 reg1 x86))))

Function: rr64$inline

(defun rr64$inline (reg x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) reg))
       (n64 (the (signed-byte 64) (rgfi reg x86))))

Theorem: n64p-rr64

(defthm
 n64p-rr64
 (unsigned-byte-p 64 (rr64 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rr64 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rr64 reg x86))
                   (< (rr64 reg x86) 18446744073709551616))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: wr64$inline

(defun wr64$inline (reg val x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) reg)
                (type (unsigned-byte 64) val))
       (!rgfi reg (n64-to-i64 val) x86))

Theorem: x86p-wr64

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

Theorem: rr64-wr64-same

(defthm rr64-wr64-same
        (equal (rr64 reg (wr64 reg val x86))
               (loghead 64 val)))

Theorem: rr64-wr64-different

(defthm rr64-wr64-different
        (implies (not (equal (nfix reg1) (nfix reg2)))
                 (equal (rr64 reg1 (wr64 reg2 val x86))
                        (rr64 reg1 x86))))

Function: rgfi-size$inline

(defun rgfi-size$inline (nbytes index rex x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 4) nbytes)
                (type (unsigned-byte 4) index)
                (type (unsigned-byte 8) rex))
       (declare (xargs :guard (and (reg-indexp index rex)
                                   (member nbytes '(1 2 4 8)))))
       (case nbytes (1 (rr08 index rex x86))
             (2 (rr16 index x86))
             (4 (rr32 index x86))
             (8 (rr64 index x86))
             (otherwise 0)))

Theorem: natp-of-rgfi-size

(defthm natp-of-rgfi-size
        (b* ((val (rgfi-size$inline nbytes index rex x86)))
            (natp val))
        :rule-classes :type-prescription)

Function: !rgfi-size$inline

(defun
 !rgfi-size$inline
 (nbytes index val rex x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 4) nbytes)
          (type (unsigned-byte 4) index)
          (type integer val)
          (type (unsigned-byte 8) rex))
 (declare (xargs :guard (and (reg-indexp index rex)
                             (member nbytes '(1 2 4 8))
                             (unsigned-byte-p (ash nbytes 3) val))))
 (case nbytes (1 (wr08 index rex val x86))
       (2 (wr16 index val x86))
       (4 (wr32 index val x86))
       (8 (wr64 index val x86))
       (otherwise x86)))

Theorem: x86p-of-!rgfi-size

(defthm
   x86p-of-!rgfi-size
   (implies (x86p x86)
            (b* ((x86 (!rgfi-size$inline nbytes index val rex x86)))
                (x86p x86)))
   :rule-classes :rewrite)

Subtopics

Wr08
Writing to byte general-purpose registers
Wr16
Write to word general-purpose registers
Wr32
Write to doubleword general-purpose registers
Rr08
Read from byte general-purpose registers
!rgfi-size
Write to byte, word, doubleword, or quadword general-purpose register
Rgfi-size
Read form byte, word, doubleword, or quadword general-purpose register
Rr64
Read from quadword general-purpose registers
Wr64
Write to quadword general-purpose registers
Rr32
Read from doubleword general-purpose registers
Rr16
Read from word general-purpose registers