		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-endbr32/endbr64

Terminate indirect branch.

Signature
(x86-endbr32/endbr64 proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

For now we model ENDBR32 and ENDBR64 as no-ops, effectively assuming no CET support (see Intel manual Volume 1 Chapter 17 of Dec 2023). In the future, we will add proper support (conditional under CPU features).

These are instructions with two-byte opcodes, according to their specification in Intel manual Volume 2 of Dec 2023. However, Table A-3 of the same manual shows "Reserved-NOP" for F3 0F 1E. Perhaps that table has not been updated yet, but note that the `NOP' is consistent with the fact that ENDBR32 and ENDBR64 are no-ops in legacy platforms. It seems that the FB (for ENDBR32) and FA (for ENDBR64) are opcode extensions, which differentiate between the two.

This ACL2 function is called when the bytes 0F 1E are encountered during decoding, possibly with prefixes. Since the F3 prefix is mandatory for these instructions, in this ACL2 function we check that it is present.

It is not clear whether the presence of other prefixes is allowed. For now we allow and ignore them, but we may revise this

Then we ensure that there is at least one more byte, which must be either FB or FA. Otherwise, the throw a #UD, which seems appropriate, although it is not immediately clear from the Intel manual whether there are other instructions that also start with F3 0F 1E. Also this may be revised in the future.

It is not clear from the Intel manual what should happen if ENDBR32 is used in 64-bit mode or ENDBR64 is used in 32-bit mode. For now, we allow them, since we treat them as no-op anyhow.

For generality, we may want to rename this ACL2 function to something like x86-reserved-nop-1e, so that it can accommodate potentially other (future?) instructions besides ENDBR32 and ENDBR64.

Definitions and Theorems

Function: x86-endbr32/endbr64

(defun x86-endbr32/endbr64
       (proc-mode start-rip temp-rip
                  prefixes 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) rex-byte)
          (type (unsigned-byte 8) opcode)
          (type (unsigned-byte 8) modr/m)
          (type (unsigned-byte 8) sib))
 (declare (ignorable proc-mode start-rip temp-rip
                     prefixes rex-byte opcode modr/m sib))
 (declare (xargs :guard (and (prefixes-p prefixes)
                             (modr/m-p modr/m)
                             (sib-p sib)
                             (rip-guard-okp proc-mode temp-rip))))
 (let ((__function__ 'x86-endbr32/endbr64))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-endbr32/endbr64)
       (?r/m (the (unsigned-byte 3)
                  (modr/m->r/m modr/m)))
       (?mod (the (unsigned-byte 2)
                  (modr/m->mod modr/m)))
       (?reg (the (unsigned-byte 3)
                  (modr/m->reg modr/m))))
   (b*
    ((p1 (prefixes->rep prefixes))
     ((unless (= p1 243))
      (!!fault-fresh :ud nil :no-mandatory-f3))
     (p2 (prefixes->seg prefixes))
     (p4? (equal 103 (prefixes->adr prefixes)))
     (seg-reg
         (select-segment-register proc-mode p2 p4? mod r/m sib x86))
     ((mv flg next-byte x86)
      (rme08 proc-mode temp-rip seg-reg
             :x x86))
     ((when flg)
      (!!ms-fresh :no-next-byte-in-instruction))
     ((unless (or (= next-byte 251)
                  (= next-byte 250)))
      (!!fault-fresh :ud nil :no-following-fb-or-fa))
     ((mv flg temp-rip)
      (add-to-*ip proc-mode temp-rip 1 x86))
     ((when flg)
      (!!ms-fresh :add-to-*ip temp-rip))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-endbr32/endbr64

(defthm x86p-of-x86-endbr32/endbr64
 (implies
   (x86p x86)
   (b*
    ((x86 (x86-endbr32/endbr64 proc-mode start-rip temp-rip prefixes
                               rex-byte opcode modr/m sib x86)))
    (x86p x86)))
 :rule-classes :rewrite)