		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__))
    (b* ((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 (b* ((x86 (x86-fetch-decode-execute x86))
                    (n-1 (the (unsigned-byte 59) (1- n))))
                 (x86-run-steps1 n-1 n0 x86)))))))