• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
            • Ia32e-paging
              • Paging-entry-no-page-fault-p
              • Ia32e-la-to-pa-without-tlb-internal
              • Ia32e-la-to-pa-page-directory
              • Ia32e-la-to-pa-page-dir-ptr-table
              • Ia32e-la-to-pa-page-table
              • Ia32e-la-to-pa-pml4-table
              • Ia32e-la-to-pa-without-tlb
              • Ia32e-la-to-pa
                • Same-page
                • Page-fault-exception
                • Page-dir-ptr-table-entry-addr
                • Page-directory-entry-addr
                • Page-table-entry-addr
                • La-to-pa
                • Paging-entry-no-page-fault-p-did-fault?
                • Pml4-table-entry-addr
                • Same-page-offset
                • Page-user-supervisor
                • Page-execute-disable
                • Set-dirty-bit
                • Set-accessed-bit
                • Page-read-write
                • Page-present
                • Page-fault-err-no
                • Accessed-bit
                • Page-size
                • Find-similar-paging-entries-from-page-present-equality-aux
                • Dirty-bit
                • Good-lin-addr-p
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Ia32e-paging

    Ia32e-la-to-pa

    Signature
    (ia32e-la-to-pa lin-addr r-w-x x86) → (mv * * x86)
    Arguments
    lin-addr — Canonical linear address to be mapped to a physical address.
    r-w-x — Indicates whether this translation is on the behalf of a read, write, or instruction fetch.
    x86 — x86 state.

    Definitions and Theorems

    Function: ia32e-la-to-pa

    (defun ia32e-la-to-pa (lin-addr r-w-x x86)
     (declare (xargs :stobjs (x86)))
     (declare (type (signed-byte 48) lin-addr)
              (type (member :r :w :x) r-w-x))
     (declare (xargs :guard (and (not (app-view x86))
                                 (canonical-address-p lin-addr))))
     (let ((__function__ 'ia32e-la-to-pa))
      (declare (ignorable __function__))
      (if
       (mbt (not (app-view x86)))
       (b*
        ((lin-addr (mbe :logic (logext 48 (loghead 48 lin-addr))
                        :exec lin-addr))
         (r-w-x (mbe :logic (if (member r-w-x '(:r :w :x)) r-w-x :r)
                     :exec r-w-x))
         (implicit-supervisor-access (implicit-supervisor-access x86))
         (cr0 (n32 (ctri *cr0* x86)))
         (cr4 (n22 (ctri *cr4* x86)))
         (cpl (the (unsigned-byte 2)
                   (if implicit-supervisor-access 0
                     (cpl x86))))
         (implicit-supervisor-access
              (the (unsigned-byte 1)
                   (if implicit-supervisor-access 1 0)))
         (ia32-efer (n12 (msri *ia32_efer-idx* x86)))
         (wp (cr0bits->wp cr0))
         (smep (cr4bits->smep cr4))
         (smap (cr4bits->smap cr4))
         (ac (rflagsbits->ac (rflags x86)))
         (nxe (ia32_eferbits->nxe ia32-efer))
         (vpn (logtail 12 (loghead 48 lin-addr)))
         (tlb (tlb x86))
         (tlb-key
             (make-tlb-key-fast
                  :vpn vpn
                  :r-w-x (case r-w-x (:r 0) (:w 1) (:x 2))
                  :wp wp
                  :smep smep
                  :smap smap
                  :ac ac
                  :nxe nxe
                  :implicit-supervisor-access implicit-supervisor-access
                  :cpl cpl))
         (tlb-entry (cdr (hons-get tlb-key tlb)))
         ((when tlb-entry)
          (mv
           nil
           (mbe
               :logic (logapp 12 lin-addr tlb-entry)
               :exec
               (the (unsigned-byte 52)
                    (logapp-inline 12 lin-addr
                                   (the (unsigned-byte 40) tlb-entry))))
           x86))
         ((mv flg phys-addr x86)
          (mbe :exec (ia32e-la-to-pa-without-tlb-internal
                          lin-addr wp smep
                          smap ac nxe implicit-supervisor-access
                          r-w-x cpl x86)
               :logic (ia32e-la-to-pa-without-tlb lin-addr r-w-x x86)))
         ((when flg) (mv flg phys-addr x86))
         (ppn (logtail 12 phys-addr))
         (x86 (!tlb (hons-acons tlb-key ppn tlb)
                    x86)))
        (mv flg phys-addr x86))
       (mv t 0 x86))))

    Theorem: n52p-mv-nth-1-ia32e-la-to-pa

    (defthm n52p-mv-nth-1-ia32e-la-to-pa
     (unsigned-byte-p *physical-address-size*
                      (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86)))
     :rule-classes
     (:rewrite
      (:type-prescription
        :corollary (natp (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86)))
        :hints
        (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
      (:linear
       :corollary
       (and (<= 0
                (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86)))
            (< (mv-nth 1 (ia32e-la-to-pa lin-addr r-w-x x86))
               (expt 2 *physical-address-size*)))
       :hints
       (("Goal"
            :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: x86p-mv-nth-2-ia32e-la-to-pa

    (defthm x86p-mv-nth-2-ia32e-la-to-pa
      (implies (x86p x86)
               (x86p (mv-nth 2
                             (ia32e-la-to-pa lin-addr r-w-x x86)))))

    Theorem: xr-ia32e-la-to-pa

    (defthm xr-ia32e-la-to-pa
     (implies (and (not (equal fld :mem))
                   (not (equal fld :fault))
                   (not (equal fld :tlb)))
              (equal (xr fld index
                         (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))
                     (xr fld index x86))))

    Theorem: xr-fault-ia32e-la-to-pa

    (defthm xr-fault-ia32e-la-to-pa
     (implies (not (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86)))
              (equal (xr :fault index
                         (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))
                     (xr :fault index x86))))

    Theorem: xr-and-ia32e-la-to-pa-in-non-marking-view

    (defthm xr-and-ia32e-la-to-pa-in-non-marking-view
     (implies (and (not (marking-view x86))
                   (not (equal fld :fault))
                   (not (equal fld :tlb)))
              (equal (xr fld index
                         (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))
                     (xr fld index x86))))

    Theorem: ia32e-la-to-pa-xw-values

    (defthm ia32e-la-to-pa-xw-values
     (implies
      (and (not (equal fld :mem))
           (not (equal fld :rflags))
           (not (equal fld :fault))
           (not (equal fld :ctr))
           (not (equal fld :msr))
           (not (equal fld :seg-visible))
           (not (equal fld :app-view))
           (not (equal fld :tlb))
           (not (equal fld :implicit-supervisor-access)))
      (and
         (equal (mv-nth 0
                        (ia32e-la-to-pa lin-addr
                                        r-w-x (xw fld index value x86)))
                (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86)))
         (equal (mv-nth 1
                        (ia32e-la-to-pa lin-addr
                                        r-w-x (xw fld index value x86)))
                (mv-nth 1
                        (ia32e-la-to-pa lin-addr r-w-x x86))))))

    Theorem: ia32e-la-to-pa-xw-rflags-not-ac

    (defthm ia32e-la-to-pa-xw-rflags-not-ac
     (implies
      (equal (rflagsbits->ac value)
             (rflagsbits->ac (rflags x86)))
      (and
       (equal (mv-nth 0
                      (ia32e-la-to-pa lin-addr
                                      r-w-x (xw :rflags nil value x86)))
              (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86)))
       (equal (mv-nth 1
                      (ia32e-la-to-pa lin-addr
                                      r-w-x (xw :rflags nil value x86)))
              (mv-nth 1
                      (ia32e-la-to-pa lin-addr r-w-x x86))))))

    Theorem: ia32e-la-to-pa-xw-state

    (defthm ia32e-la-to-pa-xw-state
     (implies
         (and (not (equal fld :mem))
              (not (equal fld :rflags))
              (not (equal fld :fault))
              (not (equal fld :ctr))
              (not (equal fld :msr))
              (not (equal fld :seg-visible))
              (not (equal fld :app-view))
              (not (equal fld :marking-view))
              (not (equal fld :tlb))
              (not (equal fld :implicit-supervisor-access)))
         (equal (mv-nth 2
                        (ia32e-la-to-pa lin-addr
                                        r-w-x (xw fld index value x86)))
                (xw fld index value
                    (mv-nth 2
                            (ia32e-la-to-pa lin-addr r-w-x x86))))))

    Theorem: ia32e-la-to-pa-xw-rflags-state-not-ac

    (defthm ia32e-la-to-pa-xw-rflags-state-not-ac
     (implies
       (equal (rflagsbits->ac value)
              (rflagsbits->ac (rflags x86)))
       (equal (mv-nth 2
                      (ia32e-la-to-pa lin-addr
                                      r-w-x (xw :rflags nil value x86)))
              (xw :rflags nil value
                  (mv-nth 2
                          (ia32e-la-to-pa lin-addr r-w-x x86))))))

    Theorem: 64-bit-modep-of-ia32e-la-to-pa

    (defthm 64-bit-modep-of-ia32e-la-to-pa
      (equal
           (64-bit-modep (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))
           (64-bit-modep x86)))

    Theorem: x86-operation-mode-of-ia32e-la-to-pa

    (defthm x86-operation-mode-of-ia32e-la-to-pa
      (equal (x86-operation-mode
                  (mv-nth 2 (ia32e-la-to-pa lin-addr r-w-x x86)))
             (x86-operation-mode x86)))

    Theorem: ia32e-la-to-pa-flg-same-if-virt-addr-same-page

    (defthm ia32e-la-to-pa-flg-same-if-virt-addr-same-page
      (implies (same-page lin-addr lin-addr-2)
               (equal (mv-nth 0 (ia32e-la-to-pa lin-addr r-w-x x86))
                      (mv-nth 0
                              (ia32e-la-to-pa lin-addr-2 r-w-x x86))))
      :rule-classes :congruence)

    Theorem: ia32e-la-to-pa-phys-addr-same-if-virt-addr-same-page

    (defthm ia32e-la-to-pa-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 lin-addr r-w-x x86))
                      (mv-nth 1
                              (ia32e-la-to-pa lin-addr-2 r-w-x x86))))
      :rule-classes :congruence)

    Theorem: ia32e-la-to-pa-fixes-address

    (defthm ia32e-la-to-pa-fixes-address
      (implies (not (canonical-address-p lin-addr))
               (equal (ia32e-la-to-pa lin-addr r-w-x x86)
                      (ia32e-la-to-pa (logext 48 lin-addr)
                                      r-w-x x86))))

    Theorem: ia32e-la-to-pa-fixes-perm

    (defthm ia32e-la-to-pa-fixes-perm
      (implies (not (member-p r-w-x '(:r :w :x)))
               (equal (ia32e-la-to-pa lin-addr r-w-x x86)
                      (ia32e-la-to-pa lin-addr :r x86))))