• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
          • Rme32
          • Rime32
          • Gen-read-function
          • Rme80
          • Rme64
          • Rme48
          • Rme256
          • Rme16
          • Rme128
          • Rime64
          • Rime16
          • Gen-write-function
          • Rme-size
          • Rme08
          • Rime08
          • Rime-size
          • Wme-size
          • Wime-size
          • Wme32
          • Wime32
          • Wme80
          • Wme64
          • Wme48
          • Wme256
          • Wme16
          • Wme128
          • Wime64
          • Wime16
          • Address-aligned-p
          • Wme08
          • Wime08
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • 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

• Top-level-memory

Rime32

Read a signed 32-bit value from memory via an effective address.

Signature

(rime32 proc-mode 
        eff-addr seg-reg r-x check-alignment? 
        x86 &key (mem-ptr? 'nil)) 
 
  → 
(mv flg value x86-new)

Arguments

check-alignment? — Guard (booleanp check-alignment?).

mem-ptr? — Guard (booleanp mem-ptr?).

Returns

value — Type (signed-byte-p 32 value), given (x86p x86).

x86-new — Type (x86p x86-new), given (x86p x86).

The effective address eff-addr is translated to a canonical linear address using ea-to-la. If this translation is successful and no other errors (like alignment errors) occur, then riml32 is called.

Prior to the effective address translation, we check whether read access is allowed. The only case in which it is not allowed is when a read access is attempted on an execute-only code segment, in 32-bit mode. In 64-bit mode, the R bit of the code segment descriptor is ignored (see Atmel manual, Dec'17, Volume 2, Section 4.8.1).

Definitions and Theorems

Function: rime32$inline

(defun rime32$inline (proc-mode eff-addr seg-reg
                                r-x check-alignment? x86 mem-ptr?)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 64) eff-addr)
          (type (integer 0 5) seg-reg)
          (type (member :r :x) r-x))
 (declare (xargs :guard (and (booleanp check-alignment?)
                             (booleanp mem-ptr?))))
 (b*
  (((when
     (and (/= proc-mode 0)
          (= seg-reg 1)
          (eq r-x :r)
          (b* ((attr (loghead 16 (seg-hidden-attri seg-reg x86)))
               (r (code-segment-descriptor-attributesbits->r attr)))
            (= r 0))))
    (mv (list :execute-only-code-segment eff-addr)
        0 x86))
   ((mv flg lin-addr)
    (ea-to-la proc-mode eff-addr seg-reg 4 x86))
   ((when flg) (mv flg 0 x86))
   ((unless (or (not check-alignment?)
                (address-aligned-p lin-addr 4 mem-ptr?)))
    (mv (list :unaligned-linear-address lin-addr)
        0 x86)))
  (riml32 lin-addr r-x x86)))

Theorem: return-type-of-rime32.value

(defthm return-type-of-rime32.value
  (implies (x86p x86)
           (b* (((mv ?flg acl2::?value ?x86-new)
                 (rime32$inline proc-mode eff-addr seg-reg
                                r-x check-alignment? x86 mem-ptr?)))
             (signed-byte-p 32 value)))
  :rule-classes :rewrite)

Theorem: x86p-of-rime32.x86-new

(defthm x86p-of-rime32.x86-new
  (implies (x86p x86)
           (b* (((mv ?flg acl2::?value ?x86-new)
                 (rime32$inline proc-mode eff-addr seg-reg
                                r-x check-alignment? x86 mem-ptr?)))
             (x86p x86-new)))
  :rule-classes :rewrite)

Theorem: i32p-of-mv-nth-1-rime32

(defthm i32p-of-mv-nth-1-rime32
 (signed-byte-p 32
                (mv-nth 1
                        (rime32 proc-mode eff-addr
                                seg-reg r-x check-alignment? x86
                                :mem-ptr? mem-ptr?)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (integerp (mv-nth 1
                        (rime32 proc-mode eff-addr
                                seg-reg r-x check-alignment? x86
                                :mem-ptr? mem-ptr?)))
      :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
    :corollary
    (and (<= -2147483648
             (mv-nth 1
                     (rime32 proc-mode eff-addr
                             seg-reg r-x check-alignment? x86
                             :mem-ptr? mem-ptr?)))
         (< (mv-nth 1
                    (rime32 proc-mode eff-addr
                            seg-reg r-x check-alignment? x86
                            :mem-ptr? mem-ptr?))
            2147483648))
    :hints
    (("Goal"
          :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

Theorem: rime32-value-when-error

(defthm rime32-value-when-error
  (implies (mv-nth 0
                   (rime32 proc-mode eff-addr
                           seg-reg r-x check-alignment? x86
                           :mem-ptr? mem-ptr?))
           (equal (mv-nth 1
                          (rime32 proc-mode eff-addr
                                  seg-reg r-x check-alignment? x86
                                  :mem-ptr? mem-ptr?))
                  0)))

Theorem: rime32-does-not-affect-state-in-app-view

(defthm rime32-does-not-affect-state-in-app-view
  (implies (app-view x86)
           (equal (mv-nth 2
                          (rime32 proc-mode eff-addr
                                  seg-reg r-x check-alignment? x86
                                  :mem-ptr? mem-ptr?))
                  x86)))

Theorem: xr-rime32-state-app-view

(defthm xr-rime32-state-app-view
  (implies
       (app-view x86)
       (equal (xr fld index
                  (mv-nth 2
                          (rime32 proc-mode eff-addr
                                  seg-reg r-x check-alignment? x86
                                  :mem-ptr? mem-ptr?)))
              (xr fld index x86))))

Theorem: xr-rime32-state-sys-view

(defthm xr-rime32-state-sys-view
  (implies
       (and (not (app-view x86))
            (not (equal fld :mem))
            (not (equal fld :fault))
            (not (equal fld :tlb))
            (member-equal fld *x86-field-names-as-keywords*))
       (equal (xr fld index
                  (mv-nth 2
                          (rime32 proc-mode eff-addr
                                  seg-reg r-x check-alignment? x86
                                  :mem-ptr? mem-ptr?)))
              (xr fld index x86))))

Theorem: rime32-xw-app-view

(defthm rime32-xw-app-view
 (implies
   (and (app-view x86)
        (not (equal fld :mem))
        (not (equal fld :app-view))
        (not (equal fld :seg-hidden-base))
        (not (equal fld :seg-hidden-limit))
        (not (equal fld :seg-hidden-attr))
        (not (equal fld :seg-visible))
        (not (equal fld :msr)))
   (and (equal (mv-nth 0
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw fld index value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 0
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?)))
        (equal (mv-nth 1
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw fld index value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 1
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?))))))

Theorem: rime32-xw-sys-view

(defthm rime32-xw-sys-view
 (implies
   (and (not (app-view x86))
        (not (equal fld :fault))
        (not (equal fld :seg-visible))
        (not (equal fld :seg-hidden-base))
        (not (equal fld :seg-hidden-limit))
        (not (equal fld :seg-hidden-attr))
        (not (equal fld :mem))
        (not (equal fld :ctr))
        (not (equal fld :msr))
        (not (equal fld :rflags))
        (not (equal fld :app-view))
        (not (equal fld :tlb))
        (not (equal fld :marking-view))
        (not (equal fld :implicit-supervisor-access))
        (member-equal fld *x86-field-names-as-keywords*))
   (and (equal (mv-nth 0
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw fld index value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 0
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?)))
        (equal (mv-nth 1
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw fld index value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 1
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?)))
        (equal (mv-nth 2
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw fld index value x86)
                               :mem-ptr? mem-ptr?))
               (xw fld index value
                   (mv-nth 2
                           (rime32 proc-mode eff-addr
                                   seg-reg r-x check-alignment? x86
                                   :mem-ptr? mem-ptr?)))))))

Theorem: rime32-xw-sys-view-rflags-not-ac

(defthm rime32-xw-sys-view-rflags-not-ac
 (implies
   (and (not (app-view x86))
        (equal (rflagsbits->ac value)
               (rflagsbits->ac (rflags x86))))
   (and (equal (mv-nth 0
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw :rflags nil value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 0
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?)))
        (equal (mv-nth 1
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw :rflags nil value x86)
                               :mem-ptr? mem-ptr?))
               (mv-nth 1
                       (rime32 proc-mode eff-addr
                               seg-reg r-x check-alignment? x86
                               :mem-ptr? mem-ptr?)))
        (equal (mv-nth 2
                       (rime32 proc-mode
                               eff-addr seg-reg r-x check-alignment?
                               (xw :rflags nil value x86)
                               :mem-ptr? mem-ptr?))
               (xw :rflags nil value
                   (mv-nth 2
                           (rime32 proc-mode eff-addr
                                   seg-reg r-x check-alignment? x86
                                   :mem-ptr? mem-ptr?)))))))

Theorem: rime32-when-64-bit-modep-and-not-fs/gs

(defthm rime32-when-64-bit-modep-and-not-fs/gs
  (implies (and (not (equal seg-reg 4))
                (not (equal seg-reg 5))
                (canonical-address-p eff-addr)
                (or (not check-alignment?)
                    (address-aligned-p eff-addr 4 mem-ptr?)))
           (equal (rime32 0 eff-addr
                          seg-reg r-x check-alignment? x86
                          :mem-ptr? mem-ptr?)
                  (riml32 eff-addr r-x x86))))

Theorem: rime32-unaligned-when-64-bit-modep-and-not-fs/gs

(defthm rime32-unaligned-when-64-bit-modep-and-not-fs/gs
  (implies (and (not (equal seg-reg 4))
                (not (equal seg-reg 5))
                (not (or (not check-alignment?)
                         (address-aligned-p eff-addr 4 mem-ptr?)))
                (canonical-address-p eff-addr))
           (equal (rime32 0 eff-addr
                          seg-reg r-x check-alignment? x86
                          :mem-ptr? mem-ptr?)
                  (list (list :unaligned-linear-address eff-addr)
                        0 x86))))

Theorem: rime32-when-64-bit-modep-and-fs/gs

(defthm rime32-when-64-bit-modep-and-fs/gs
 (implies
  (or (equal seg-reg 4) (equal seg-reg 5))
  (equal (rime32 0 eff-addr
                 seg-reg r-x check-alignment? x86
                 :mem-ptr? mem-ptr?)
         (b* (((mv flg lin-addr)
               (b* (((mv base & &)
                     (segment-base-and-bounds 0 seg-reg x86))
                    (lin-addr (i64 (+ base (n64 eff-addr)))))
                 (if (canonical-address-p lin-addr)
                     (mv nil lin-addr)
                   (mv (list :non-canonical-address lin-addr)
                       0))))
              ((when flg) (mv flg 0 x86))
              ((unless (or (not check-alignment?)
                           (address-aligned-p lin-addr 4 mem-ptr?)))
               (mv (list :unaligned-linear-address lin-addr)
                   0 x86)))
           (riml32 lin-addr r-x x86)))))