• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
          • Get-prefixes
          • Vex-0f3a-execute
          • Vex-0f38-execute
          • Vex-0f-execute
          • Two-byte-opcode-execute
          • Second-three-byte-opcode-execute
          • One-byte-opcode-execute
          • First-three-byte-opcode-execute
          • Evex-0f3a-execute
          • Evex-0f38-execute
          • Evex-0f-execute
          • X86-fetch-decode-execute
          • Vex-decode-and-execute
          • Evex-decode-and-execute
          • Opcode-maps
          • X86-run
          • Implemented-opcodes
          • Three-byte-opcode-decode-and-execute
          • X86-run-halt-count
          • Two-byte-opcode-decode-and-execute
          • X86-run-steps
          • X86-fetch-decode-execute-halt
          • X86-run-halt
          • X86-run-steps1
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• X86-decoder

First-three-byte-opcode-execute

First three-byte opcode dispatch function.

Signature

(first-three-byte-opcode-execute proc-mode start-rip 
                                 temp-rip prefixes mandatory-prefix 
                                 rex-byte opcode modr/m sib x86) 
 
  → 
x86

first-three-byte-opcode-execute is the doorway to the first three-byte opcode map, i.e., to all three-byte opcodes whose first two opcode bytes are 0F 38.

Definitions and Theorems

Function: first-three-byte-opcode-execute

(defun
 first-three-byte-opcode-execute
 (proc-mode start-rip
            temp-rip prefixes mandatory-prefix
            rex-byte opcode modr/m sib x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) start-rip)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8)
                mandatory-prefix)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 8) opcode)
          (type (unsigned-byte 8) modr/m)
          (type (unsigned-byte 8) sib))
 (case
  opcode
  (0
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (1
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (2
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (3
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (4
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (5
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (6
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (7
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (8
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (9
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (10
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (11
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (16
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (20
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (21
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (23
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (28
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (29
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (30
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:ssse3)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:ssse3))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (32
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (33
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (34
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (35
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (36
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-5 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-5 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (37
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-5 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-5 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (40
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (41
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (42
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-1 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0)
                             (ud-modr/m.mod-indicates-register))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (43
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (48
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (49
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (50
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (51
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (52
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (53
   (cond
    ((and (not (equal (modr/m->mod modr/m) 3))
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    ((and (equal (modr/m->mod modr/m) 3)
          (equal mandatory-prefix 102))
     (let
      ((fault-var (let ((chk-ex (or (chk-exc :type-5 (:avx2)))))
                       (or chk-ex nil))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (55
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.2)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.2))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (56
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (57
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (58
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse2)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse2))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (59
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (60
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (61
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (62
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (63
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (64
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (65
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
            (let ((chk-ex (or (chk-exc :type-4 (:sse4.1)))))
                 (or chk-ex
                     (if (or (equal (feature-flags-macro '(:sse4.1))
                                    0))
                         ':ud
                         nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (128
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (ud-not-in-prot-or-64-mode)
                          (ud-not-in-vmx-operation)
                          (ud-invept-not-supported)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      (if (or (gp-cpl-not-0)) ':gp nil))))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (:gp (x86-general-protection "#GP Encountered!"
                                           start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (129
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (ud-not-in-prot-or-64-mode)
                          (ud-not-in-vmx-operation)
                          (ud-invvpid-not-supported)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      (if (or (gp-cpl-not-0)) ':gp nil))))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (:gp (x86-general-protection "#GP Encountered!"
                                           start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (130
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (ud-lock-used)
                          (ud-invpcid-not-supported)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      (if (or (gp-cpl-not-0)) ':gp nil))))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (:gp (x86-general-protection "#GP Encountered!"
                                           start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (200
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (201
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (202
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (203
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (204
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (205
   (let
    ((fault-var
          (let ((chk-ex (or (chk-exc :type-4 (:sha)))))
               (or chk-ex
                   (if (or (equal (feature-flags-macro '(:sha)) 0))
                       ':ud
                       nil)))))
    (if
     fault-var
     (case
      fault-var
      (:ud (x86-illegal-instruction "#UD Encountered!"
                                    start-rip temp-rip x86))
      (:gp (x86-general-protection "#GP Encountered!"
                                   start-rip temp-rip x86))
      (:nm (x86-device-not-available "#NM Encountered!"
                                     start-rip temp-rip x86))
      (t
        (x86-step-unimplemented "Unimplemented exception in x86isa!"
                                x86)))
     (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                             x86))))
  (219
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
           (let ((chk-ex (or (chk-exc :type-4 (:aes)))))
                (or chk-ex
                    (if (or (equal (feature-flags-macro '(:aes)) 0))
                        ':ud
                        nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (220
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
           (let ((chk-ex (or (chk-exc :type-4 (:aes)))))
                (or chk-ex
                    (if (or (equal (feature-flags-macro '(:aes)) 0))
                        ':ud
                        nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (221
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
           (let ((chk-ex (or (chk-exc :type-4 (:aes)))))
                (or chk-ex
                    (if (or (equal (feature-flags-macro '(:aes)) 0))
                        ':ud
                        nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (222
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
           (let ((chk-ex (or (chk-exc :type-4 (:aes)))))
                (or chk-ex
                    (if (or (equal (feature-flags-macro '(:aes)) 0))
                        ':ud
                        nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (223
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var
           (let ((chk-ex (or (chk-exc :type-4 (:aes)))))
                (or chk-ex
                    (if (or (equal (feature-flags-macro '(:aes)) 0))
                        ':ud
                        nil)))))
      (if
       fault-var
       (case fault-var
             (:ud (x86-illegal-instruction "#UD Encountered!"
                                           start-rip temp-rip x86))
             (:gp (x86-general-protection "#GP Encountered!"
                                          start-rip temp-rip x86))
             (:nm (x86-device-not-available "#NM Encountered!"
                                            start-rip temp-rip x86))
             (t (x86-step-unimplemented
                     "Unimplemented exception in x86isa!"
                     x86)))
       (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                               x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (240
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:movbe))
                                 0)
                          (ud-lock-used)
                          (ud-repne-f2-v86-cpuid-case)
                          (ud-rep-f3-used)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:movbe))
                                 0)
                          (ud-lock-used)
                          (ud-repne-f2-v86-cpuid-case)
                          (ud-rep-f3-used)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    ((equal mandatory-prefix 242)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:sse4.2))
                                 0)
                          (ud-lock-used))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (241
   (cond
    ((equal mandatory-prefix 0)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:movbe))
                                 0)
                          (ud-lock-used)
                          (ud-repne-f2-v86-cpuid-case)
                          (ud-rep-f3-used)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:movbe))
                                 0)
                          (ud-lock-used)
                          (ud-repne-f2-v86-cpuid-case)
                          (ud-rep-f3-used)
                          (ud-modr/m.mod-indicates-register))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    ((equal mandatory-prefix 242)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:sse4.2))
                                 0)
                          (ud-lock-used))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (246
   (cond
    ((equal mandatory-prefix 102)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:adx)) 0)
                          (ud-lock-used))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    ((equal mandatory-prefix 243)
     (let
      ((fault-var (if (or (equal (feature-flags-macro '(:adx)) 0)
                          (ud-lock-used))
                      ':ud
                      nil)))
      (if
        fault-var
        (case fault-var
              (:ud (x86-illegal-instruction "#UD Encountered!"
                                            start-rip temp-rip x86))
              (t (x86-step-unimplemented
                      "Unimplemented exception in x86isa!"
                      x86)))
        (x86-step-unimplemented "Opcode Unimplemented in x86isa!"
                                x86))))
    (t (x86-illegal-instruction "#UD Encountered!"
                                start-rip temp-rip x86))))
  (t (x86-illegal-instruction "#UD Encountered!"
                              start-rip temp-rip x86))))

Theorem: x86p-first-three-byte-opcode-execute

(defthm x86p-first-three-byte-opcode-execute
        (implies (x86p x86)
                 (x86p (first-three-byte-opcode-execute
                            proc-mode start-rip
                            temp-rip prefixes mandatory-prefix
                            rex-byte opcode modr/m sib x86))))