		Search-engine friendly clone of the ACL2 documentation.

System-level-marking-view-proof-utilities

Las-to-pas-two-n-ind-hint

Signature
(las-to-pas-two-n-ind-hint n-1 n-2 lin-addr r-w-x x86) → (mv * * x86)
Arguments: n-1 — Guard (natp n-1).; n-2 — Guard (natp n-2).; lin-addr — Guard (integerp lin-addr).

Definitions and Theorems

Function: las-to-pas-two-n-ind-hint

(defun las-to-pas-two-n-ind-hint (n-1 n-2 lin-addr r-w-x x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (member :r :w :x) r-w-x))
  (declare (xargs :guard (and (natp n-1)
                              (natp n-2)
                              (integerp lin-addr))))
  (let ((__function__ 'las-to-pas-two-n-ind-hint))
    (declare (ignorable __function__))
    (if (or (zp n-1) (zp n-2))
        (mv nil nil x86)
      (b* (((unless (canonical-address-p lin-addr))
            (mv t nil x86))
           ((mv flg p-addr x86)
            (ia32e-la-to-pa lin-addr r-w-x x86))
           ((when flg) (mv flg nil x86))
           ((mv flgs p-addrs x86)
            (las-to-pas-two-n-ind-hint (1- n-1)
                                       (1- n-2)
                                       (1+ lin-addr)
                                       r-w-x x86)))
        (mv flgs (if flgs nil (cons p-addr p-addrs))
            x86)))))