• 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

Rme-size

Read an unsigned value with the specified number of bytes from memory via an effective address.

Signature

(rme-size proc-mode nbytes 
          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 (natp value).

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

The effective address 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 rml-size 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 Intel manual, Dec'17, Volume 2, Section 4.8.1

Definitions and Theorems

Function: rme-size$inline

(defun rme-size$inline (proc-mode nbytes eff-addr seg-reg
                                  r-x check-alignment? x86 mem-ptr?)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (member 1 2 4 6 8 10 16 32)
                nbytes)
          (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 nbytes x86))
   ((when flg) (mv flg 0 x86))
   ((unless (or (not check-alignment?)
                (address-aligned-p lin-addr nbytes mem-ptr?)))
    (mv (list :unaligned-linear-address lin-addr)
        0 x86)))
  (rml-size nbytes lin-addr r-x x86)))

Theorem: natp-of-rme-size.value

(defthm natp-of-rme-size.value
  (b* (((mv ?flg acl2::?value ?x86-new)
        (rme-size$inline proc-mode nbytes eff-addr seg-reg
                         r-x check-alignment? x86 mem-ptr?)))
    (natp value))
  :rule-classes (:rewrite :type-prescription))

Theorem: x86p-of-rme-size.x86-new

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

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

(defthm rme-size-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 nbytes mem-ptr?)))
           (equal (rme-size 0 nbytes eff-addr
                            seg-reg r-x check-alignment? x86
                            :mem-ptr? mem-ptr?)
                  (rml-size nbytes eff-addr r-x x86))))

Theorem: rme-size-when-64-bit-modep-fs/gs

(defthm rme-size-when-64-bit-modep-fs/gs
 (implies
  (or (equal seg-reg 4) (equal seg-reg 5))
  (equal
    (rme-size 0 nbytes 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 nbytes mem-ptr?)))
          (mv (list :unaligned-linear-address lin-addr)
              0 x86)))
      (rml-size nbytes lin-addr r-x x86)))))

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

(defthm rme-size-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 nbytes mem-ptr?)))
            (canonical-address-p eff-addr))
       (equal (rme-size 0 nbytes eff-addr
                        seg-reg r-x check-alignment? x86
                        :mem-ptr? mem-ptr?)
              (list (list :unaligned-linear-address eff-addr)
                    0 x86))))

Theorem: rme-size-non-canonical-when-64-bit-modep-and-not-fs/gs

(defthm rme-size-non-canonical-when-64-bit-modep-and-not-fs/gs
  (implies (and (not (equal seg-reg 4))
                (not (equal seg-reg 5))
                (not (canonical-address-p eff-addr)))
           (equal (rme-size 0 nbytes eff-addr
                            seg-reg r-x check-alignment? x86
                            :mem-ptr? mem-ptr?)
                  (list (list :non-canonical-address eff-addr)
                        0 x86))))

Theorem: rme-size-of-1-to-rme08

(defthm rme-size-of-1-to-rme08
  (equal (rme-size proc-mode 1 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme08 proc-mode eff-addr seg-reg r-x x86)))

Theorem: rme-size-of-2-to-rme16

(defthm rme-size-of-2-to-rme16
  (equal (rme-size proc-mode 2 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme16 proc-mode eff-addr
                seg-reg r-x check-alignment? x86)))

Theorem: rme-size-of-4-to-rme32

(defthm rme-size-of-4-to-rme32
  (equal (rme-size proc-mode 4 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme32 proc-mode eff-addr
                seg-reg r-x check-alignment? x86
                :mem-ptr? mem-ptr?)))

Theorem: rme-size-of-6-to-rme48

(defthm rme-size-of-6-to-rme48
  (equal (rme-size proc-mode 6 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme48 proc-mode eff-addr
                seg-reg r-x check-alignment? x86)))

Theorem: rme-size-of-8-to-rme64

(defthm rme-size-of-8-to-rme64
  (equal (rme-size proc-mode 8 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme64 proc-mode eff-addr
                seg-reg r-x check-alignment? x86)))

Theorem: rme-size-of-10-to-rme64

(defthm rme-size-of-10-to-rme64
  (equal (rme-size proc-mode 10 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme80 proc-mode eff-addr
                seg-reg r-x check-alignment? x86)))

Theorem: rme-size-of-16-to-rme128

(defthm rme-size-of-16-to-rme128
  (equal (rme-size proc-mode 16 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme128 proc-mode eff-addr
                 seg-reg r-x check-alignment? x86)))

Theorem: rme-size-of-32-to-rme256

(defthm rme-size-of-32-to-rme256
  (equal (rme-size proc-mode 32 eff-addr
                   seg-reg r-x check-alignment? x86
                   :mem-ptr? mem-ptr?)
         (rme256 proc-mode eff-addr
                 seg-reg r-x check-alignment? x86)))