		Search-engine friendly clone of the ACL2 documentation.

X86-decoder

X86-fetch-decode-execute-halt

Alternative version of x86-fetch-decode-execute that sets the MS field if rip is equal to halt-address

Signature
(x86-fetch-decode-execute-halt halt-address x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Definitions and Theorems

Function: x86-fetch-decode-execute-halt$inline

(defun x86-fetch-decode-execute-halt$inline (halt-address x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) halt-address))
  (if (equal (the (signed-byte 48) (rip x86))
             halt-address)
      (b* ((ctx 'x86-fetch-decode-execute-halt))
        (!!ms-fresh))
    (x86-fetch-decode-execute x86)))

Theorem: x86p-of-x86-fetch-decode-execute-halt

(defthm x86p-of-x86-fetch-decode-execute-halt
 (implies
   (x86p x86)
   (b*
     ((x86 (x86-fetch-decode-execute-halt$inline halt-address x86)))
     (x86p x86)))
 :rule-classes :rewrite)