|
|
|---|
|
|
|
|---|
(ia32e-la-to-pa-page-directory
lin-addr base-addr
u/s-acc r/w-acc x/d-acc wp smep
smap ac nxe implicit-supervisor-access
r-w-x cpl x86)
→
(mv * * x86)Function:
(defun ia32e-la-to-pa-page-directory (lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 48) lin-addr) (type (unsigned-byte 52) base-addr) (type (unsigned-byte 1) u/s-acc) (type (unsigned-byte 1) r/w-acc) (type (unsigned-byte 1) x/d-acc) (type (unsigned-byte 1) wp) (type (unsigned-byte 1) smep) (type (unsigned-byte 1) smap) (type (unsigned-byte 1) ac) (type (unsigned-byte 1) nxe) (type (unsigned-byte 1) implicit-supervisor-access) (type (member :r :w :x) r-w-x) (type (unsigned-byte 2) cpl)) (declare (xargs :guard (and (not (app-view x86)) (canonical-address-p lin-addr) (equal (loghead 12 base-addr) 0) (or (not (equal implicit-supervisor-access 1)) (< cpl 3))))) (let ((__function__ 'ia32e-la-to-pa-page-directory)) (declare (ignorable __function__)) (if (mbt (not (app-view x86))) (b* ((lin-addr (mbe :logic (logext 48 (loghead 48 lin-addr)) :exec lin-addr)) (base-addr (mbe :logic (part-install 0 (loghead *physical-address-size* base-addr) :low 0 :width 12) :exec base-addr)) (p-entry-addr (the (unsigned-byte 52) (page-directory-entry-addr lin-addr base-addr))) (entry (the (unsigned-byte 64) (rm-low-64 p-entry-addr x86))) (u/s-all (mbe :logic (logand u/s-acc (page-user-supervisor entry)) :exec (the (unsigned-byte 1) (logand u/s-acc (ia32e-page-tablesbits->u/s entry))))) (r/w-all (mbe :logic (logand r/w-acc (page-read-write entry)) :exec (the (unsigned-byte 1) (logand r/w-acc (ia32e-page-tablesbits->r/w entry))))) (x/d-all (mbe :logic (logand x/d-acc (page-execute-disable entry)) :exec (the (unsigned-byte 1) (logand x/d-acc (ia32e-page-tablesbits->xd entry))))) ((mv fault-flg val x86) (paging-entry-no-page-fault-p 1 lin-addr entry u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (marking-view? (marking-view x86)) ((mv updated? updated-entry) (if (and marking-view? (equal (mbe :logic (page-present entry) :exec (ia32e-page-tablesbits->p entry)) 1)) (b* ((accessed (mbe :logic (accessed-bit entry) :exec (ia32e-page-tablesbits->a entry)))) (if (equal accessed 0) (mv t (mbe :logic (set-accessed-bit entry) :exec (!ia32e-page-tablesbits->a 1 entry))) (mv nil entry))) (mv nil entry))) ((when fault-flg) (b* ((x86 (if updated? (wm-low-64 p-entry-addr updated-entry x86) x86))) (mv 'page-fault val x86)))) (if (mbe :logic (equal (page-size entry) 1) :exec (equal (ia32e-page-tablesbits->ps entry) 1)) (b* (((mv updated? updated-entry) (if marking-view? (b* ((dirty (mbe :logic (dirty-bit entry) :exec (ia32e-page-tablesbits->d entry)))) (if (and (equal dirty 0) (equal r-w-x :w)) (mv t (mbe :logic (set-dirty-bit updated-entry) :exec (!ia32e-page-tablesbits->d 1 updated-entry))) (mv updated? updated-entry))) (mv nil entry))) (x86 (if updated? (wm-low-64 p-entry-addr updated-entry x86) x86))) (mv nil (mbe :logic (part-install (part-select lin-addr :low 0 :high 20) (ash (ia32e-pde-2mb-pagebits->page entry) 21) :low 0 :high 20) :exec (the (unsigned-byte 52) (logior (the (unsigned-byte 52) (logand (the (unsigned-byte 52) (ash (the (unsigned-byte 31) (ia32e-pde-2mb-pagebits->page entry)) 21)) (lognot (1- (ash 1 21))))) (the (unsigned-byte 21) (logand (1- (ash 1 21)) lin-addr))))) x86)) (b* ((page-table-base-addr (ash (ia32e-pde-pg-tablebits->pt entry) 12)) ((mv flag (the (unsigned-byte 52) p-addr) x86) (ia32e-la-to-pa-page-table lin-addr page-table-base-addr u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (entry (rm-low-64 p-entry-addr x86)) (x86 (if marking-view? (b* ((accessed (mbe :logic (accessed-bit entry) :exec (ia32e-page-tablesbits->a entry))) ((unless (equal accessed 0)) x86)) (wm-low-64 p-entry-addr (set-accessed-bit entry) x86)) x86)) ((when flag) (mv flag 0 x86))) (mv nil p-addr x86)))) (mv t 0 x86))))
Theorem:
(defthm n52p-mv-nth-1-ia32e-la-to-pa-page-directory (unsigned-byte-p *physical-address-size* (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (< (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm x86p-mv-nth-2-ia32e-la-to-pa-page-directory (implies (x86p x86) (x86p (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))))
Theorem:
(defthm xr-ia32e-la-to-pa-page-directory (implies (and (not (equal fld :mem)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm xr-fault-ia32e-la-to-pa-page-directory (implies (not (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (xr :fault index (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr :fault index x86))))
Theorem:
(defthm xr-and-ia32e-la-to-pa-page-directory-in-non-marking-view (implies (and (not (marking-view x86)) (not (equal fld :fault))) (equal (xr fld index (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (xr fld index x86))))
Theorem:
(defthm ia32e-la-to-pa-page-directory-xw-values (implies (and (not (equal fld :mem)) (not (equal fld :app-view))) (and (equal (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (equal (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm ia32e-la-to-pa-page-directory-xw-state (implies (and (not (equal fld :mem)) (not (equal fld :fault)) (not (equal fld :app-view)) (not (equal fld :marking-view))) (equal (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (xw fld index value x86))) (xw fld index value (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))))))
Theorem:
(defthm mv-nth-2-ia32e-la-to-pa-page-directory-system-level-non-marking-view (implies (and (not (marking-view x86)) (not (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) (equal (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) x86)))
Theorem:
(defthm 64-bit-modep-of-ia32e-la-to-pa-page-directory (equal (64-bit-modep (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (64-bit-modep x86)))
Theorem:
(defthm x86-operation-mode-of-ia32e-la-to-pa-page-directory (equal (x86-operation-mode (mv-nth 2 (ia32e-la-to-pa-page-directory lin-addr base-addr u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (x86-operation-mode x86)))
Theorem:
(defthm ia32e-la-to-pa-page-directory-same-page-offset (implies (not (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86))) (same-page-offset (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) lin-addr)))
Theorem:
(defthm ia32e-la-to-pa-page-directory-flg-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 0 (ia32e-la-to-pa-page-directory lin-addr-2 entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)
Theorem:
(defthm ia32e-la-to-pa-page-directory-phys-addr-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (same-page (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)) (mv-nth 1 (ia32e-la-to-pa-page-directory lin-addr-2 entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl x86)))) :rule-classes :congruence)