		Search-engine friendly clone of the ACL2 documentation.

Instructions

Two-byte-opcodes

Instruction semantic functions for Intel's instructions with two-byte opcodes

Subtopics

X86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex: VEX-encoded logical instructions.
X86-endbr32/endbr64: Terminate indirect branch.
X86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm: Add/Sub/Mul/Div/Max/Min scalar single/double precision floating-point values
X86-push-segment-register: PUSH Segment Register
X86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm
X86-addps/subps/mulps/divps/maxps/minps-op/en-rm: Add/Sub/Mul/Div/Max/Min packed single-precision floating-point values
X86-lldt
X86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm: Add/Sub/Mul/Div/Max/Min packed double-precision floating-point values
X86-cmovcc
X86-two-byte-jcc
X86-setcc
X86-cvts?2si/cvtts?2si-op/en-rm: Convert scalar single/double precision FP value to integer
X86-comis?/ucomis?-op/en-rm: Order/Unordered compare scalar single/double precision floating-point values and set EFLAGS
X86-cmpps-op/en-rmi: Compare packed single-precision floating-point values
X86-vpsubb/vpsubw/vpsubd/vpsubq-vex: Subtract packed integers (VEX variants).
X86-vpaddb/vpaddw/vpaddd/vpaddq-vex: Add packed integers (VEX variants).
X86-movups/movupd/movdqu-op/en-rm
X86-sysret: Return from fast system call to user code at privilege level 3
X86-pmovmskb-op/en-rm: Move byte mask
X86-unpck?ps-op/en-rm: Unpack and interleave low/high packed single-precision floating-point values
X86-lidt
X86-lgdt
X86-cmppd-op/en-rmi: Compare packed double-precision floating-point values
X86-sqrtps-op/en-rm: Square roots of packed single-precision floating-point values
X86-rdrand
X86-vmovups-vex-b: VMOVUPS: Move Unaligned Packed Single Precision Floating-Point Values (VEX encoding, Op/En B)
X86-unpck?pd-op/en-rm: Unpack and interleave low/high packed double-precision floating-point values
X86-cvtsi2s?-op/en-rm: Convert integer to scalar single/double precision FP value
X86-cmpss/cmpsd-op/en-rmi: Compare scalar single/double precision floating-point values
X86-vmovups-vex-a: VMOVUPS: Move Unaligned Packed Single Precision Floating-Point Values (VEX encoding, Op/En A)
X86-shufps-op/en-rmi: Shuffle packed single-precision floating-point values
X86-fxsave/fxsave64
X86-fxrstor/fxrstor64
X86-cvtpd2ps-op/en-rm: Convert packed double-precision FP values to packed single-precision FP values
X86-btr-0f-b3
X86-bt-0f-ba
X86-bt-0f-ab
X86-sqrtpd-op/en-rm: Square roots packed double-precision floating-point values
X86-cvts?2s?-op/en-rm: Convert scalar single/double precision FP value to scalar double/single FP value
X86-vzeroupper: VZEROUPPER: Zero Upper Bits of YMM and ZMM Registers
X86-two-byte-nop
X86-sgdt
X86-psubb/psubw/psubd/psubq-sse: Subtract packed integers (SSE variants).
X86-paddb/paddw/paddd/paddq-sse: Add packed integers (SSE variants).
X86-movups/movupd/movdqu-op/en-mr
X86-cvtps2pd-op/en-rm: Convert packed single-precision FP values to packed double-precision FP values
X86-sqrts?-op/en-rm: Square root of scalar single/double precision floating-point value
X86-imul-op/en-rm
X86-bt-0f-a3
X86-syscall
X86-shufpd-op/en-rmi: Shuffle packed double-precision floating-point values
X86-punpckh-sse
X86-movss/movsd-op/en-rm: Move scalar single/double precision floating-point values
X86-movss/movsd-op/en-mr: Move scalar single/double precision floating-point values
X86-movhps/movhpd-op/en-mr: Move high packed single/double precision floating-point values
X86-movaps/movapd-op/en-mr: Move aligned packed single/double precision floating-point values
X86-cmpxchg8b/16b
X86-bswap
X86-punpckl-sse
X86-movlps/movlpd-op/en-rm: Move low packed single/double precision floating-point values
X86-movlps/movlpd-op/en-mr: Move low packed single/double precision floating-point values
X86-movhps/movhpd-op/en-rm: Move high packed single/double precision floating-point values
X86-movaps/movapd-op/en-rm: Move aligned packed single/double precision floating-point values
X86-ldmxcsr/stmxcsr-op/en-m: Load/Store MXCSR register
X86-bsf-op/en-rm: Bit scan forward
X86-syscall-app-view
X86-psrl-xmm-sse
X86-psll-xmm-sse
X86-movsx
X86-cmpxchg
X86-pcmpgt-sse
X86-pcmpeq-sse
X86-movhlps-sse: Move Packed Single Precision Floating-Point Values High to Low
X86-psrl-imm-sse
X86-psra-xmm-sse
X86-psll-imm-sse
X86-pslldq/psrldq: Shift double quadword left/right logical (SSE variant).
X86-movzx
X86-tzcnt
X86-psra-imm-sse
X86-pshuflw
X86-pshufhw
X86-pshufd
X86-movd/movq-from-xmm
X86-movdqa-from-xmm: Move aligned packed integer values.
X86-ltr
X86-bsr
X86-popcnt
X86-packuswb-sse
X86-movq-to-xmm/mem
X86-movdqa-to-xmm: Move aligned packed integer values.
X86-movq-from-xmm/mem
X86-movd/movq-to-xmm
X86-mov-control-regs-op/en-rm
X86-mov-control-regs-op/en-mr
X86-invlpg
X86-cpuid
X86-wrmsr
X86-syscall-both-views
X86-rdmsr
X86-one-byte-nop