|
|
|---|
|
|
|
|---|
Read a signed value with the specified number of bytes from memory via an effective address.
(rime-size proc-mode nbytes
eff-addr seg-reg r-x check-alignment?
x86 &key (mem-ptr? 'nil))
→
(mv flg value x86-new)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 riml-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 Atmel manual, Dec'17, Volume 2, Section 4.8.1
Function:
(defun rime-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 8) 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))) (riml-size nbytes lin-addr r-x x86)))
Theorem:
(defthm integerp-of-rime-size.value (implies (integerp nbytes) (b* (((mv ?flg acl2::?value ?x86-new) (rime-size$inline proc-mode nbytes eff-addr seg-reg r-x check-alignment? x86 mem-ptr?))) (integerp value))) :rule-classes :rewrite)
Theorem:
(defthm x86p-of-rime-size.x86-new (implies (x86p x86) (b* (((mv ?flg acl2::?value ?x86-new) (rime-size$inline proc-mode nbytes eff-addr seg-reg r-x check-alignment? x86 mem-ptr?))) (x86p x86-new))) :rule-classes :rewrite)
Theorem:
(defthm rime-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 (rime-size 0 nbytes eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?) (riml-size nbytes eff-addr r-x x86))))
Theorem:
(defthm rime-size-when-64-bit-modep-fs/gs (implies (or (equal seg-reg 4) (equal seg-reg 5)) (equal (rime-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))) (riml-size nbytes lin-addr r-x x86)))))
Theorem:
(defthm rime-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 (rime-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:
(defthm rime-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 (rime-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:
(defthm rime-size-of-1-to-rime08 (equal (rime-size proc-mode 1 eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?) (rime08 proc-mode eff-addr seg-reg r-x x86)))
Theorem:
(defthm rime-size-of-2-to-rime16 (equal (rime-size proc-mode 2 eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?) (rime16 proc-mode eff-addr seg-reg r-x check-alignment? x86)))
Theorem:
(defthm rime-size-of-4-to-rime32 (equal (rime-size proc-mode 4 eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?) (rime32 proc-mode eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?)))
Theorem:
(defthm rime-size-of-8-to-rime64 (equal (rime-size proc-mode 8 eff-addr seg-reg r-x check-alignment? x86 :mem-ptr? mem-ptr?) (rime64 proc-mode eff-addr seg-reg r-x check-alignment? x86)))