Determining access rights and detecting page faults
(paging-entry-no-page-fault-p structure-type 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 flg val x86)
Source for determining the access rights: Section 4.6 in the Intel Manuals, Vol. 3A.
It is important to differentiate between:
These concepts are defined below.
TO-DO: For now, we are treating all supervisor-mode accesses as explicit. We need to detect and then account for implicit accesses.
Function:
(defun paging-entry-no-page-fault-p-did-fault? (u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl) (declare (type (unsigned-byte 1) u/s-all) (type (unsigned-byte 1) r/w-all) (type (unsigned-byte 1) x/d-all) (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 (or (not (equal implicit-supervisor-access 1)) (< cpl 3)))) (let ((__function__ 'paging-entry-no-page-fault-p-did-fault?)) (declare (ignorable __function__)) (or (and (equal r-w-x :r) (if (< cpl 3) (if (equal u/s-all 0) nil (if (equal smap 0) nil (or (equal implicit-supervisor-access 1) (equal ac 0)))) (equal u/s-all 0))) (and (equal r-w-x :w) (if (< cpl 3) (if (equal u/s-all 0) (and (equal wp 1) (equal r/w-all 0)) (if (equal wp 0) (if (equal smap 0) nil (or (equal implicit-supervisor-access 1) (equal ac 0))) (if (equal smap 0) (equal r/w-all 0) (if (and (equal implicit-supervisor-access 0) (equal ac 1)) (equal r/w-all 0) t)))) (or (equal u/s-all 0) (equal r/w-all 0)))) (and (equal r-w-x :x) (if (< cpl 3) (if (equal u/s-all 0) (if (equal nxe 0) nil (equal x/d-all 1)) (if (equal smep 0) (if (equal nxe 0) nil (equal x/d-all 1)) t)) (or (equal u/s-all 0) (and (equal nxe 1) (equal x/d-all 1))))))))
Theorem:
(defthm booleanp-of-paging-entry-no-page-fault-p-did-fault? (b* ((fault? (paging-entry-no-page-fault-p-did-fault? u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl))) (booleanp fault?)) :rule-classes :rewrite)
Function:
(defun paging-entry-no-page-fault-p (structure-type 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) (declare (xargs :stobjs (x86))) (declare (type (unsigned-byte 2) structure-type) (type (signed-byte 48) lin-addr) (type (unsigned-byte 64) entry) (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)) (or (not (equal implicit-supervisor-access 1)) (< cpl 3))))) (let ((__function__ 'paging-entry-no-page-fault-p)) (declare (ignorable __function__)) (b* ((entry (mbe :logic (loghead 64 entry) :exec entry)) (page-present (mbe :logic (page-present entry) :exec (ia32e-page-tablesbits->p entry))) ((when (equal page-present 0)) (let ((err-no (page-fault-err-no page-present r-w-x cpl 0 smep 1 nxe))) (page-fault-exception lin-addr err-no x86))) (read-write (mbe :logic (page-read-write entry) :exec (ia32e-page-tablesbits->r/w entry))) (r/w-all (the (unsigned-byte 1) (logand read-write r/w-acc))) (user-supervisor (mbe :logic (page-user-supervisor entry) :exec (ia32e-page-tablesbits->u/s entry))) (u/s-all (the (unsigned-byte 1) (logand user-supervisor u/s-acc))) (execute-disable (mbe :logic (page-execute-disable entry) :exec (ia32e-page-tablesbits->xd entry))) (x/d-all (the (unsigned-byte 1) (logand execute-disable x/d-acc))) (page-size (mbe :logic (page-size entry) :exec (ia32e-page-tablesbits->ps entry))) (rsvd (mbe :logic (if (or (and (equal structure-type 3) (equal page-size 1)) (and (not (equal structure-type 0)) (not (equal structure-type 3)) (equal page-size 1) (if (equal structure-type 1) (not (equal (part-select entry :low 13 :high 20) 0)) (not (equal (part-select entry :low 13 :high 29) 0)))) (and (equal nxe 0) (not (equal execute-disable 0)))) 1 0) :exec (if (or (and (equal structure-type 3) (equal page-size 1)) (and (not (equal structure-type 0)) (not (equal structure-type 3)) (equal page-size 1) (if (equal structure-type 1) (not (equal (the (unsigned-byte 8) (logand 255 (the (unsigned-byte 51) (ash entry (- 13))))) 0)) (not (equal (the (unsigned-byte 17) (logand 131071 (the (unsigned-byte 51) (ash entry (- 13))))) 0)))) (and (equal nxe 0) (not (equal (ia32e-page-tablesbits->xd entry) 0)))) 1 0))) ((when (equal rsvd 1)) (let ((err-no (page-fault-err-no page-present r-w-x cpl rsvd smep 1 nxe))) (page-fault-exception lin-addr err-no x86))) ((when (paging-entry-no-page-fault-p-did-fault? u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl)) (let ((err-no (page-fault-err-no page-present r-w-x cpl rsvd smep 1 nxe))) (page-fault-exception lin-addr err-no x86)))) (mv nil 0 x86))))
Theorem:
(defthm x86p-of-paging-entry-no-page-fault-p.x86 (implies (x86p x86) (b* (((mv ?flg ?val ?x86) (paging-entry-no-page-fault-p structure-type 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))) (x86p x86))) :rule-classes :rewrite)
Theorem:
(defthm mv-nth-1-paging-entry-no-page-fault-p-value (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type 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)) 0))
Theorem:
(defthm xr-paging-entry-no-page-fault-p (implies (not (equal fld :fault)) (equal (xr fld index (mv-nth 2 (paging-entry-no-page-fault-p structure-type 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))) (xr fld index x86))))
Theorem:
(defthm rm-low-64-paging-entry-no-page-fault-p (equal (rm-low-64 addr (mv-nth 2 (paging-entry-no-page-fault-p structure-type 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))) (rm-low-64 addr x86)))
Theorem:
(defthm paging-entry-no-page-fault-p-xw-values (and (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type lin-addr entry 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 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type lin-addr entry 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 (paging-entry-no-page-fault-p structure-type 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)))))
Theorem:
(defthm paging-entry-no-page-fault-p-xw-state (implies (not (equal fld :fault)) (equal (mv-nth 2 (paging-entry-no-page-fault-p structure-type lin-addr entry 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 (paging-entry-no-page-fault-p structure-type 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))))))
Theorem:
(defthm mv-nth-2-paging-entry-no-page-fault-p-does-not-modify-x86-if-no-fault (implies (not (mv-nth 0 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 2 (paging-entry-no-page-fault-p structure-type 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)) x86)))
Function:
(defun find-similar-paging-entries-from-page-present-equality-aux (index entry-var calls) (declare (xargs :guard (natp index))) (let ((__function__ 'find-similar-paging-entries-from-page-present-equality-aux)) (declare (ignorable __function__)) (if (atom calls) nil (b* ((one-call (car calls)) ((unless (and (true-listp one-call) (true-listp (nth index one-call)) (equal (len (nth index one-call)) 2))) nil)) (cons (list (cons entry-var (nth 1 (nth index one-call)))) (find-similar-paging-entries-from-page-present-equality-aux index entry-var (cdr calls)))))))
Function:
(defun find-similar-paging-entries-from-page-present-equality (bound-entry-val entry-var mfc state) (declare (xargs :stobjs (state)) (ignorable state)) (b* (((mv index calls) (mv 2 (acl2::find-matches-list (cons 'equal (cons (cons 'page-present (cons bound-entry-val 'nil)) '((page-present e)))) (mfc-clause mfc) nil))) ((mv index calls) (if (not calls) (mv 1 (acl2::find-matches-list (cons 'equal (cons '(page-present e) (cons (cons 'page-present (cons bound-entry-val 'nil)) 'nil))) (mfc-clause mfc) nil)) (mv index calls))) ((when (not calls)) nil)) (find-similar-paging-entries-from-page-present-equality-aux index entry-var calls)))
Theorem:
(defthm mv-nth-0-paging-entry-no-page-fault-p-and-similar-entries (implies (and (bind-free (find-similar-paging-entries-from-page-present-equality entry-1 'entry-2 mfc state) (entry-2)) (syntaxp (not (eq entry-1 entry-2))) (equal (page-present entry-1) (page-present entry-2)) (equal (page-read-write entry-1) (page-read-write entry-2)) (equal (page-user-supervisor entry-1) (page-user-supervisor entry-2)) (equal (page-execute-disable entry-1) (page-execute-disable entry-2)) (equal (page-size entry-1) (page-size entry-2)) (if (equal structure-type 1) (equal (part-select entry-1 :low 13 :high 20) (part-select entry-2 :low 13 :high 20)) (if (equal structure-type 2) (equal (part-select entry-1 :low 13 :high 29) (part-select entry-2 :low 13 :high 29)) t)) (unsigned-byte-p 2 structure-type) (unsigned-byte-p 64 entry-1) (unsigned-byte-p 64 entry-2)) (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type lin-addr entry-1 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 (paging-entry-no-page-fault-p structure-type lin-addr entry-2 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-0-paging-entry-no-page-fault-p-is-independent-of-lin-addr (implies (not (mv-nth 0 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type (+ n 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)) nil)))
Theorem:
(defthm 64-bit-modep-of-paging-entry-no-page-fault-p (equal (64-bit-modep (mv-nth 2 (paging-entry-no-page-fault-p structure-type 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))) (64-bit-modep x86)))
Theorem:
(defthm x86-operation-mode-of-paging-entry-no-page-fault-p (equal (x86-operation-mode (mv-nth 2 (paging-entry-no-page-fault-p structure-type 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))) (x86-operation-mode x86)))
Theorem:
(defthm paging-entry-no-page-fault-flg-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type 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 (paging-entry-no-page-fault-p structure-type 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 paging-entry-no-page-fault-val-same-if-virt-addr-same-page (implies (same-page lin-addr lin-addr-2) (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type 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 (paging-entry-no-page-fault-p structure-type 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 paging-entry-no-page-fault-p-invariant-under-paging-entry-no-page-fault-p (and (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (mv-nth 2 (paging-entry-no-page-fault-p structure-type2 lin-addr2 entry2 u/s-acc2 r/w-acc2 x/d-acc2 wp2 smep2 smap2 ac2 nxe2 implicit-supervisor-access2 r-w-x2 cpl2 x86)))) (mv-nth 0 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type lin-addr entry u/s-acc r/w-acc x/d-acc wp smep smap ac nxe implicit-supervisor-access r-w-x cpl (mv-nth 2 (paging-entry-no-page-fault-p structure-type2 lin-addr2 entry2 u/s-acc2 r/w-acc2 x/d-acc2 wp2 smep2 smap2 ac2 nxe2 implicit-supervisor-access2 r-w-x2 cpl2 x86)))) (mv-nth 1 (paging-entry-no-page-fault-p structure-type 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)))))
Theorem:
(defthm paging-entry-no-page-fault-p-invariant-under-setting-dirty-bit (and (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type lin-addr (set-dirty-bit 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 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type lin-addr (set-dirty-bit 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 (paging-entry-no-page-fault-p structure-type 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)))))
Theorem:
(defthm paging-entry-no-page-fault-p-invariant-under-setting-accessed-bit (and (equal (mv-nth 0 (paging-entry-no-page-fault-p structure-type lin-addr (set-accessed-bit 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 (paging-entry-no-page-fault-p structure-type 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))) (equal (mv-nth 1 (paging-entry-no-page-fault-p structure-type lin-addr (set-accessed-bit 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 (paging-entry-no-page-fault-p structure-type 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)))))