• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Program-at-alt
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • 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
              • All-mem-except-paging-structures-equal
              • Gather-qword-addresses-corresponding-to-1-entry
              • Xlation-governing-entries-paddrs
              • Xlate-equiv-structures
              • Xlation-governing-entries-paddrs-for-page-dir-ptr-table
              • Xlation-governing-entries-paddrs-for-page-directory
              • All-xlation-governing-entries-paddrs
              • Xlation-governing-entries-paddrs-for-pml4-table
              • Xlation-governing-entries-paddrs-for-page-table
              • Gather-pml4-table-qword-addresses
              • 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
          • Phys-mem-values-same
        • 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
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Gather-paging-structures

Xlation-governing-entries-paddrs

Signature

(xlation-governing-entries-paddrs lin-addr x86) → *

Arguments

lin-addr — Canonical linear address to be mapped to a physical address.

x86 — x86 state.

xlation-governing-entries-paddrs returns a true-listp of physical addresses that govern the translation of a linear address lin-addr to its corresponding physical address p-addr. Addresses that can be a part of the output (depending on the page configurations, i.e., 4K, 2M, or 1G pages) include:

1. The addresses of the relevant PML4 entry
2. The addresses of the relevant PDPT entry
3. The addresses of the relevant PD entry
4. The addresses of the relevant PT entry

Definitions and Theorems

Function: xlation-governing-entries-paddrs

(defun xlation-governing-entries-paddrs (lin-addr x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr))
  (declare (xargs :guard (not (app-view x86))))
  (let ((__function__ 'xlation-governing-entries-paddrs))
    (declare (ignorable __function__))
    (if (mbt (not (app-view x86)))
        (b* ((cr3 (ctri *cr3* x86))
             (pml4-base-addr (ash (cr3bits->pdb cr3) 12)))
          (xlation-governing-entries-paddrs-for-pml4-table
               lin-addr pml4-base-addr x86))
      nil)))

Theorem: xlation-governing-entries-paddrs-and-xw-not-mem

(defthm xlation-governing-entries-paddrs-and-xw-not-mem
  (implies (and (not (equal fld :mem))
                (not (equal fld :ctr))
                (not (equal fld :app-view)))
           (equal (xlation-governing-entries-paddrs
                       lin-addr (xw fld index value x86))
                  (xlation-governing-entries-paddrs
                       lin-addr (double-rewrite x86)))))

Theorem: xlation-governing-entries-paddrs-and-xw-mem-not-member

(defthm xlation-governing-entries-paddrs-and-xw-mem-not-member
  (implies (not (member-p index
                          (xlation-governing-entries-paddrs
                               lin-addr (double-rewrite x86))))
           (equal (xlation-governing-entries-paddrs
                       lin-addr (xw :mem index value x86))
                  (xlation-governing-entries-paddrs
                       lin-addr (double-rewrite x86)))))

Theorem: ia32e-la-to-pa-values-and-xw-mem-not-member

(defthm ia32e-la-to-pa-values-and-xw-mem-not-member
 (implies
  (and (not (member-p index
                      (xlation-governing-entries-paddrs
                           lin-addr (double-rewrite x86))))
       (canonical-address-p lin-addr))
  (and
   (equal
    (mv-nth
       0
       (ia32e-la-to-pa-without-tlb lin-addr
                                   r-w-x (xw :mem index value x86)))
    (mv-nth 0
            (ia32e-la-to-pa-without-tlb
                 lin-addr r-w-x (double-rewrite x86))))
   (equal
    (mv-nth
       1
       (ia32e-la-to-pa-without-tlb lin-addr
                                   r-w-x (xw :mem index value x86)))
    (mv-nth
        1
        (ia32e-la-to-pa-without-tlb lin-addr
                                    r-w-x (double-rewrite x86)))))))

Theorem: xlation-governing-entries-paddrs-and-write-to-physical-memory-disjoint

(defthm
 xlation-governing-entries-paddrs-and-write-to-physical-memory-disjoint
 (implies
  (and
   (disjoint-p
    (xlation-governing-entries-paddrs lin-addr (double-rewrite x86))
    p-addrs)
   (physical-address-listp p-addrs))
  (equal (xlation-governing-entries-paddrs
              lin-addr
              (write-to-physical-memory p-addrs bytes x86))
         (xlation-governing-entries-paddrs
              lin-addr (double-rewrite x86)))))