		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-run-steps1

Signature
(x86-run-steps1 n n0 x86) → (mv * x86)

Definitions and Theorems

Function: x86-run-steps1

(defun
   x86-run-steps1 (n n0 x86)
   (declare (xargs :stobjs (x86)))
   (declare (type (unsigned-byte 59) n)
            (type (unsigned-byte 59) n0))
   (declare (xargs :guard (and (natp n) (natp n0) (<= n n0))))
   (let ((__function__ 'x86-run-steps1))
        (declare (ignorable __function__))
        (let* ((diff (the (unsigned-byte 59) (- n0 n))))
              (cond ((ms x86) (mv diff x86))
                    ((fault x86) (mv diff x86))
                    ((zp n)
                     (let* ((ctx 'x86-run)
                            (x86 (!!ms-fresh :timeout t)))
                           (mv diff x86)))
                    (t (let* ((x86 (x86-fetch-decode-execute x86))
                              (n-1 (the (unsigned-byte 59) (1- n))))
                             (x86-run-steps1 n-1 n0 x86)))))))