		Search-engine friendly clone of the ACL2 documentation.

Instructions

X86-illegal-instruction

Semantic function corresponding to opcodes that Intel deems to be illegal or reserved

Signature
(x86-illegal-instruction message start-rip temp-rip x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Note that the #UD (undefined operation) exception should be thrown here, which is why the fault field is populated with message.

Definitions and Theorems

Function: x86-illegal-instruction

(defun x86-illegal-instruction (message start-rip temp-rip x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) start-rip)
           (type (signed-byte 48) temp-rip))
  (let ((__function__ 'x86-illegal-instruction))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-illegal-instruction)
         (x86 (!rip temp-rip x86)))
      (!!fault-fresh :ud message
                     :instruction-address start-rip))))

Theorem: x86p-of-x86-illegal-instruction

(defthm x86p-of-x86-illegal-instruction
 (implies
   (x86p x86)
   (b*
    ((x86 (x86-illegal-instruction message start-rip temp-rip x86)))
    (x86p x86)))
 :rule-classes :rewrite)