• 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

Rime08

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

Signature

(rime08 proc-mode eff-addr seg-reg r-x x86) 
  → 
(mv flg value x86-new)

Returns

value — Type (signed-byte-p 8 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 riml08 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: rime08$inline

(defun rime08$inline (proc-mode eff-addr seg-reg r-x 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))
 (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 1 x86))
   ((when flg) (mv flg 0 x86)))
  (riml08 lin-addr r-x x86)))

Theorem: return-type-of-rime08.value

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

Theorem: x86p-of-rime08.x86-new

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

Theorem: i08p-of-mv-nth-1-rime08

(defthm i08p-of-mv-nth-1-rime08
 (signed-byte-p
      8
      (mv-nth 1
              (rime08 proc-mode eff-addr seg-reg r-x x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary
     (integerp (mv-nth 1
                       (rime08 proc-mode eff-addr seg-reg r-x x86)))
     :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
    :corollary
    (and (<= -128
             (mv-nth 1
                     (rime08 proc-mode eff-addr seg-reg r-x x86)))
         (< (mv-nth 1
                    (rime08 proc-mode eff-addr seg-reg r-x x86))
            128))
    :hints
    (("Goal"
          :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

Theorem: rime08-value-when-error

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

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

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

Theorem: xr-rime08-state-app-view

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

Theorem: xr-rime08-state-sys-view

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

Theorem: rime08-xw-app-view

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

Theorem: rime08-xw-sys-view

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

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

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

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

(defthm rime08-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))
           (equal (rime08 0 eff-addr seg-reg r-x x86)
                  (riml08 eff-addr r-x x86))))

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

(defthm rime08-when-64-bit-modep-and-fs/gs
  (implies
       (or (equal seg-reg 4) (equal seg-reg 5))
       (equal (rime08 0 eff-addr seg-reg r-x 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)))
                (riml08 lin-addr r-x x86)))))