		Search-engine friendly clone of the ACL2 documentation.

Ia32e-paging

La-to-pa

Top-level page translation function

Signature
(la-to-pa lin-addr r-w-x x86) → (mv * * x86)
Arguments: 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: la-to-pa$inline

(defun la-to-pa$inline (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 (not (app-view x86))))
 (if (mbt (and (canonical-address-p lin-addr)
               (not (app-view x86))))
     (ia32e-la-to-pa lin-addr r-w-x x86)
   (mv (list :ia32e-paging-invalid-linear-address-or-not-in-sys-view
             lin-addr)
       0 x86)))