		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)