(x86-run-steps1 n n0 x86) → (mv * x86)
Function:
(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)))))))