		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-run-halt-count

A combination in functionality of x86-run-steps and x86-run-halt

Signature
(x86-run-halt-count halt-address n x86 n0) → (mv steps x86)
Returns: steps — Type (natp steps), given (and (natp n0) (natp n)).; x86 — Type (x86p x86), given (x86p x86).

Run n instructions or till halt-address is reached, whichever comes first. This function also returns the number of times x86-fetch-decode-execute-halt is executed. Note that x86-fetch-decode-execute-halt is executed one more time than x86-fetch-decode-execute --- i.e., when rip == halt-address.

Definitions and Theorems

Function: x86-run-halt-count

(defun x86-run-halt-count (halt-address n x86 n0)
 (declare (xargs :stobjs (x86)))
 (declare (type (signed-byte 48) halt-address)
          (type (unsigned-byte 59) n)
          (type (unsigned-byte 59) n0))
 (declare (xargs :guard (<= n n0)))
 (let ((__function__ 'x86-run-halt-count))
  (declare (ignorable __function__))
  (if
   (mbt (<= n n0))
   (cond
    ((or (fault x86)
         (ms x86)
         (mbe :logic (zp n) :exec (equal 0 n)))
     (mv (the (unsigned-byte 59) (- n0 n))
         x86))
    (t (let* ((x86 (x86-fetch-decode-execute-halt halt-address x86))
              (n (the (unsigned-byte 59) (1- n))))
         (x86-run-halt-count halt-address n x86 n0))))
   (mv 0 x86))))

Theorem: natp-of-x86-run-halt-count.steps

(defthm natp-of-x86-run-halt-count.steps
  (implies (and (natp n0) (natp n))
           (b* (((mv ?steps ?x86)
                 (x86-run-halt-count halt-address n x86 n0)))
             (natp steps)))
  :rule-classes :type-prescription)

Theorem: x86p-of-x86-run-halt-count.x86

(defthm x86p-of-x86-run-halt-count.x86
  (implies (x86p x86)
           (b* (((mv ?steps ?x86)
                 (x86-run-halt-count halt-address n x86 n0)))
             (x86p x86)))
  :rule-classes :rewrite)