• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Program-at-alt
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
            • Create-qword-address-list
            • Mult-8-qword-paddr-listp
            • Gather-paging-structures
              • Gather-all-paging-structure-qword-addresses
                • Gather-qword-addresses-corresponding-to-entries
              • All-mem-except-paging-structures-equal
              • Gather-qword-addresses-corresponding-to-1-entry
              • Xlation-governing-entries-paddrs
              • Xlation-governing-entries-paddrs-for-page-dir-ptr-table
              • Xlate-equiv-structures
              • Xlation-governing-entries-paddrs-for-page-directory
              • All-xlation-governing-entries-paddrs
              • Xlation-governing-entries-paddrs-for-pml4-table
              • Gather-pml4-table-qword-addresses
              • Xlation-governing-entries-paddrs-for-page-table
              • Xlate-equiv-memory
              • Open-qword-paddr-list
            • Qword-paddr-listp
            • Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
            • Find-first-arg-of-disjoint-p$-candidates
            • Paging-basics
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-paging-structures

Gather-all-paging-structure-qword-addresses

Returns a list of qword addresses of all the active paging structures

Signature

(gather-all-paging-structure-qword-addresses x86) 
  → 
list-of-addresses

Returns

list-of-addresses — Type (qword-paddr-listp list-of-addresses).

Definitions and Theorems

Function: gather-all-paging-structure-qword-addresses

(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: qword-paddr-listp-of-gather-all-paging-structure-qword-addresses

(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: true-listp-of-gather-all-paging-structure-qword-addresses

(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: mult-8-qword-paddr-listp-gather-all-paging-structure-qword-addresses

(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: no-duplicates-p-gather-all-paging-structure-qword-addresses

(defthm no-duplicates-p-gather-all-paging-structure-qword-addresses
  (no-duplicates-p
       (gather-all-paging-structure-qword-addresses x86)))

Theorem: gather-all-paging-structure-qword-addresses-xw-fld!=mem-and-ctr

(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: gather-all-paging-structure-qword-addresses-xw-doc

(defthm gather-all-paging-structure-qword-addresses-xw-doc
  (equal (gather-all-paging-structure-qword-addresses
              (xw :doc index val x86))
         (gather-all-paging-structure-qword-addresses
              (double-rewrite x86))))

Theorem: gather-all-paging-structure-qword-addresses-xw-ms

(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: gather-all-paging-structure-qword-addresses-xw-fault

(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: gather-all-paging-structure-qword-addresses-xw-env

(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: gather-all-paging-structure-qword-addresses-xw-undef

(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: gather-all-paging-structure-qword-addresses-xw-marking-view

(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: gather-all-paging-structure-qword-addresses-xw-os-info

(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: gather-all-paging-structure-qword-addresses-xw-rgf

(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: gather-all-paging-structure-qword-addresses-xw-rip

(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: gather-all-paging-structure-qword-addresses-xw-rflags

(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: gather-all-paging-structure-qword-addresses-xw-seg-visible

(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: gather-all-paging-structure-qword-addresses-xw-seg-hidden-base

(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: gather-all-paging-structure-qword-addresses-xw-seg-hidden-limit

(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: gather-all-paging-structure-qword-addresses-xw-seg-hidden-attr

(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: gather-all-paging-structure-qword-addresses-xw-str

(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: gather-all-paging-structure-qword-addresses-xw-ssr-visible

(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: gather-all-paging-structure-qword-addresses-xw-ssr-hidden-base

(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: gather-all-paging-structure-qword-addresses-xw-ssr-hidden-limit

(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: gather-all-paging-structure-qword-addresses-xw-ssr-hidden-attr

(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: gather-all-paging-structure-qword-addresses-xw-dbg

(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: gather-all-paging-structure-qword-addresses-xw-fp-data

(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: gather-all-paging-structure-qword-addresses-xw-fp-ctrl

(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: gather-all-paging-structure-qword-addresses-xw-fp-status

(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: gather-all-paging-structure-qword-addresses-xw-fp-tag

(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: gather-all-paging-structure-qword-addresses-xw-fp-last-inst

(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: gather-all-paging-structure-qword-addresses-xw-fp-last-data

(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: gather-all-paging-structure-qword-addresses-xw-fp-opcode

(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: gather-all-paging-structure-qword-addresses-xw-mxcsr

(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: gather-all-paging-structure-qword-addresses-xw-opmsk

(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: gather-all-paging-structure-qword-addresses-xw-zmm

(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: gather-all-paging-structure-qword-addresses-xw-msr

(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: gather-all-paging-structure-qword-addresses-xw-fld=ctr

(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: gather-all-paging-structure-qword-addresses-xw-fld=mem-disjoint

(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: gather-all-paging-structure-qword-addresses-wm-low-64-disjoint

(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: gather-all-paging-structure-qword-addresses-wm-low-64-entry-addr

(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: gather-all-paging-structure-qword-addresses-and-wm-low-64-subset-p

(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: gather-all-paging-structure-qword-addresses-and-write-to-physical-memory-subset-p

(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))))

Subtopics

Gather-qword-addresses-corresponding-to-entries

Returns a list --- with no duplicates --- of qword addresses of inferior paging structures referred by the entries located at addresses superior-structure-paddrs of a given superior structure