Returns a list of qword addresses of all the active paging structures
(gather-all-paging-structure-qword-addresses x86) → list-of-addresses
Function:
(defun gather-all-paging-structure-qword-addresses (x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard (not (app-view x86)))) (let ((__function__ 'gather-all-paging-structure-qword-addresses)) (declare (ignorable __function__)) (b* ((pml4-table-qword-addresses (gather-pml4-table-qword-addresses x86)) (pdpt-table-qword-addresses (gather-qword-addresses-corresponding-to-entries pml4-table-qword-addresses x86)) (pd-qword-addresses (gather-qword-addresses-corresponding-to-entries pdpt-table-qword-addresses x86)) (pt-qword-addresses (gather-qword-addresses-corresponding-to-entries pd-qword-addresses x86))) (remove-duplicates-equal (append pml4-table-qword-addresses pdpt-table-qword-addresses pd-qword-addresses pt-qword-addresses)))))
Theorem:
(defthm qword-paddr-listp-of-gather-all-paging-structure-qword-addresses (b* ((list-of-addresses (gather-all-paging-structure-qword-addresses x86))) (qword-paddr-listp list-of-addresses)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-gather-all-paging-structure-qword-addresses (b* ((list-of-addresses (gather-all-paging-structure-qword-addresses x86))) (true-listp list-of-addresses)) :rule-classes :rewrite)
Theorem:
(defthm mult-8-qword-paddr-listp-gather-all-paging-structure-qword-addresses (mult-8-qword-paddr-listp (gather-all-paging-structure-qword-addresses x86)))
Theorem:
(defthm no-duplicates-p-gather-all-paging-structure-qword-addresses (no-duplicates-p (gather-all-paging-structure-qword-addresses x86)))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fld!=mem-and-ctr (implies (and (not (equal fld :mem)) (not (equal fld :ctr)) (not (equal fld :app-view))) (equal (gather-all-paging-structure-qword-addresses (xw fld index val x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-ms (equal (gather-all-paging-structure-qword-addresses (xw :ms index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fault (equal (gather-all-paging-structure-qword-addresses (xw :fault index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-env (equal (gather-all-paging-structure-qword-addresses (xw :env index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-undef (equal (gather-all-paging-structure-qword-addresses (xw :undef index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-marking-view (equal (gather-all-paging-structure-qword-addresses (xw :marking-view index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-enable-peripherals (equal (gather-all-paging-structure-qword-addresses (xw :enable-peripherals index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-handle-exceptions (equal (gather-all-paging-structure-qword-addresses (xw :handle-exceptions index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-os-info (equal (gather-all-paging-structure-qword-addresses (xw :os-info index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-rgf (equal (gather-all-paging-structure-qword-addresses (xw :rgf index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-rip (equal (gather-all-paging-structure-qword-addresses (xw :rip index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-rflags (equal (gather-all-paging-structure-qword-addresses (xw :rflags index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-seg-visible (equal (gather-all-paging-structure-qword-addresses (xw :seg-visible index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-seg-hidden-base (equal (gather-all-paging-structure-qword-addresses (xw :seg-hidden-base index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-seg-hidden-limit (equal (gather-all-paging-structure-qword-addresses (xw :seg-hidden-limit index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-seg-hidden-attr (equal (gather-all-paging-structure-qword-addresses (xw :seg-hidden-attr index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-str (equal (gather-all-paging-structure-qword-addresses (xw :str index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-ssr-visible (equal (gather-all-paging-structure-qword-addresses (xw :ssr-visible index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-ssr-hidden-base (equal (gather-all-paging-structure-qword-addresses (xw :ssr-hidden-base index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-ssr-hidden-limit (equal (gather-all-paging-structure-qword-addresses (xw :ssr-hidden-limit index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-ssr-hidden-attr (equal (gather-all-paging-structure-qword-addresses (xw :ssr-hidden-attr index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-dbg (equal (gather-all-paging-structure-qword-addresses (xw :dbg index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-data (equal (gather-all-paging-structure-qword-addresses (xw :fp-data index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-ctrl (equal (gather-all-paging-structure-qword-addresses (xw :fp-ctrl index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-status (equal (gather-all-paging-structure-qword-addresses (xw :fp-status index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-tag (equal (gather-all-paging-structure-qword-addresses (xw :fp-tag index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-last-inst (equal (gather-all-paging-structure-qword-addresses (xw :fp-last-inst index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-last-data (equal (gather-all-paging-structure-qword-addresses (xw :fp-last-data index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fp-opcode (equal (gather-all-paging-structure-qword-addresses (xw :fp-opcode index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-mxcsr (equal (gather-all-paging-structure-qword-addresses (xw :mxcsr index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-opmsk (equal (gather-all-paging-structure-qword-addresses (xw :opmsk index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-zmm (equal (gather-all-paging-structure-qword-addresses (xw :zmm index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-msr (equal (gather-all-paging-structure-qword-addresses (xw :msr index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-inhibit-interrupts-one-instruction (equal (gather-all-paging-structure-qword-addresses (xw :inhibit-interrupts-one-instruction index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-time-stamp-counter (equal (gather-all-paging-structure-qword-addresses (xw :time-stamp-counter index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-last-clock-event (equal (gather-all-paging-structure-qword-addresses (xw :last-clock-event index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-implicit-supervisor-access (equal (gather-all-paging-structure-qword-addresses (xw :implicit-supervisor-access index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-tlb (equal (gather-all-paging-structure-qword-addresses (xw :tlb index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-tty-in (equal (gather-all-paging-structure-qword-addresses (xw :tty-in index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-tty-out (equal (gather-all-paging-structure-qword-addresses (xw :tty-out index val x86)) (gather-all-paging-structure-qword-addresses (double-rewrite x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fld=ctr (implies (not (equal index *cr3*)) (equal (gather-all-paging-structure-qword-addresses (xw :ctr index val x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-xw-fld=mem-disjoint (implies (and (not (member-p index (open-qword-paddr-list (gather-all-paging-structure-qword-addresses x86)))) (physical-address-p index)) (equal (gather-all-paging-structure-qword-addresses (xw :mem index val x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-wm-low-64-disjoint (implies (disjoint-p (addr-range 8 index) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses x86))) (equal (gather-all-paging-structure-qword-addresses (wm-low-64 index val x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-wm-low-64-entry-addr (implies (and (member-p index (gather-all-paging-structure-qword-addresses x86)) (xlate-equiv-entries (double-rewrite val) (rm-low-64 index x86)) (unsigned-byte-p 64 val) (not (xr :app-view nil x86))) (equal (gather-all-paging-structure-qword-addresses (wm-low-64 index val x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-and-wm-low-64-subset-p (implies (and (equal (page-size value) 1) (physical-address-p index) (equal (loghead 3 index) 0) (unsigned-byte-p 64 value) (not (app-view x86))) (subset-p (gather-all-paging-structure-qword-addresses (wm-low-64 index value x86)) (gather-all-paging-structure-qword-addresses x86))))
Theorem:
(defthm gather-all-paging-structure-qword-addresses-and-write-to-physical-memory-subset-p (implies (and (equal p-addrs (addr-range 8 index)) (equal (page-size value) 1) (physical-address-p index) (equal (loghead 3 index) 0) (unsigned-byte-p 64 value) (not (app-view x86))) (subset-p (gather-all-paging-structure-qword-addresses (write-to-physical-memory p-addrs value x86)) (gather-all-paging-structure-qword-addresses x86))))