• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-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
          • Rme256
          • Rme128
          • Rime64
          • Rime16
          • Rme80
          • Rme64
          • Rme48
          • Rme16
          • 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
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Top-level-memory

Rme256

Read an unsigned 256-bit value from memory via an effective address.

Signature

(rme256 proc-mode eff-addr seg-reg r-x check-alignment? x86) 
  → 
(mv flg value x86-new)

Arguments

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

Returns

value — Type (unsigned-byte-p 256 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 rml256 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: rme256$inline

(defun rme256$inline (proc-mode eff-addr
                                seg-reg r-x check-alignment? x86)
 (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 (booleanp check-alignment?)))
 (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 32 x86))
   ((when flg) (mv flg 0 x86))
   ((unless (or (not check-alignment?)
                (address-aligned-p lin-addr 32 nil)))
    (mv (list :unaligned-linear-address lin-addr)
        0 x86)))
  (rml256 lin-addr r-x x86)))

Theorem: return-type-of-rme256.value

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

Theorem: x86p-of-rme256.x86-new

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

Theorem: n256p-of-mv-nth-1-rme256

(defthm n256p-of-mv-nth-1-rme256
 (unsigned-byte-p
      256
      (mv-nth 1
              (rme256 proc-mode eff-addr
                      seg-reg r-x check-alignment? x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (natp (mv-nth 1
                    (rme256 proc-mode eff-addr
                            seg-reg r-x check-alignment? x86)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
    (<= 0
        (mv-nth 1
                (rme256 proc-mode eff-addr
                        seg-reg r-x check-alignment? x86)))
    (<
     (mv-nth 1
             (rme256 proc-mode eff-addr
                     seg-reg r-x check-alignment? x86))
     115792089237316195423570985008687907853269984665640564039457584007913129639936))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: rme256-value-when-error

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

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

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

Theorem: xr-rme256-state-app-view

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

Theorem: xr-rme256-state-sys-view

(defthm xr-rme256-state-sys-view
 (implies
      (and (not (equal fld :mem))
           (not (equal fld :fault))
           (not (equal fld :tlb)))
      (equal (xr fld index
                 (mv-nth 2
                         (rme256 proc-mode eff-addr
                                 seg-reg r-x check-alignment? x86)))
             (xr fld index x86))))

Theorem: rme256-xw-app-view

(defthm rme256-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
                      (rme256 proc-mode
                              eff-addr seg-reg r-x check-alignment?
                              (xw fld index value x86)))
              (mv-nth 0
                      (rme256 proc-mode eff-addr
                              seg-reg r-x check-alignment? x86)))
       (equal (mv-nth 1
                      (rme256 proc-mode
                              eff-addr seg-reg r-x check-alignment?
                              (xw fld index value x86)))
              (mv-nth 1
                      (rme256 proc-mode eff-addr
                              seg-reg r-x check-alignment? x86))))))

Theorem: rme256-xw-sys-view

(defthm rme256-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
                   (rme256 proc-mode
                           eff-addr seg-reg r-x check-alignment?
                           (xw fld index value x86)))
           (mv-nth 0
                   (rme256 proc-mode eff-addr
                           seg-reg r-x check-alignment? x86)))
    (equal (mv-nth 1
                   (rme256 proc-mode
                           eff-addr seg-reg r-x check-alignment?
                           (xw fld index value x86)))
           (mv-nth 1
                   (rme256 proc-mode eff-addr
                           seg-reg r-x check-alignment? x86)))
    (equal
         (mv-nth 2
                 (rme256 proc-mode
                         eff-addr seg-reg r-x check-alignment?
                         (xw fld index value x86)))
         (xw fld index value
             (mv-nth 2
                     (rme256 proc-mode eff-addr
                             seg-reg r-x check-alignment? x86)))))))

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

(defthm rme256-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
                   (rme256 proc-mode
                           eff-addr seg-reg r-x check-alignment?
                           (xw :rflags nil value x86)))
           (mv-nth 0
                   (rme256 proc-mode eff-addr
                           seg-reg r-x check-alignment? x86)))
    (equal (mv-nth 1
                   (rme256 proc-mode
                           eff-addr seg-reg r-x check-alignment?
                           (xw :rflags nil value x86)))
           (mv-nth 1
                   (rme256 proc-mode eff-addr
                           seg-reg r-x check-alignment? x86)))
    (equal
         (mv-nth 2
                 (rme256 proc-mode
                         eff-addr seg-reg r-x check-alignment?
                         (xw :rflags nil value x86)))
         (xw :rflags nil value
             (mv-nth 2
                     (rme256 proc-mode eff-addr
                             seg-reg r-x check-alignment? x86)))))))

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

(defthm rme256-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 32 nil)))
           (equal (rme256 0 eff-addr
                          seg-reg r-x check-alignment? x86)
                  (rml256 eff-addr r-x x86))))

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

(defthm rme256-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 32 nil)))
                (canonical-address-p eff-addr))
           (equal (rme256 0 eff-addr
                          seg-reg r-x check-alignment? x86)
                  (list (list :unaligned-linear-address eff-addr)
                        0 x86))))

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

(defthm rme256-when-64-bit-modep-and-fs/gs
 (implies
      (or (equal seg-reg 4) (equal seg-reg 5))
      (equal (rme256 0 eff-addr
                     seg-reg r-x check-alignment? x86)
             (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 32 nil)))
                   (mv (list :unaligned-linear-address lin-addr)
                       0 x86)))
               (rml256 lin-addr r-x x86)))))