• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • 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
      • Proof-utilities
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 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))
  (b* ((x86 (!rgfi reg (n64-to-i64 val) x86)))
    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

Rr08

Read from byte general-purpose registers

Wr32

Write to doubleword 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