libTriton  version 0.5 build 1357
SMT Semantics Supported

Table of Contents

[internal] All information about the supported semantics.

Description


Here is the instructions' list of what Triton can convert into AST Representations. Please note that our main objective is not to support all semantics right now, we are currently focusing on the design of Triton's engines. When engines will be reliable, we will write the last semantics :-). However, feel free to add your own semantics into the appropriate file. Thanks to wisk and his Medusa project which has been really useful.

x86 and x86-64 SMT semantics supported

Mnemonic Extensions Description
AAD ASCII Adjust AX Before Division
ADC Add with Carry
ADCX adx Unsigned Integer Addition of Two Operands with Carry Flag
ADD Add
AND Logical AND
ANDN bmi1 Logical AND NOT
ANDNPD sse2 Bitwise Logical AND NOT of Packed Double-Precision Floating-Point Values
ANDNPS sse1 Bitwise Logical AND NOT of Packed Single-Precision Floating-Point Values
ANDPD sse2 Bitwise Logical AND of Packed Double-Precision Floating-Point Values
ANDPS sse1 Bitwise Logical AND of Packed Single-Precision Floating-Point Values
BEXTR bmi1/tbm Bit Field Extract
BLSI bmi1 Extract Lowest Set Isolated Bit
BLSMSK bmi1 Get Mask Up to Lowest Set Bit
BLSR bmi1 Reset Lowest Set Bit
BSF Bit Scan Forward
BSR Bit Scan Reverse
BSWAP Byte Swap
BT Bit Test
BTC Bit Test and Complement
BTR Bit Test and Reset
BTS Bit Test and Set
CALL Call Procedure
CBW Convert byte (al) to word (ax)
CDQ Convert dword (eax) to qword (edx:eax)
CDQE Convert dword (eax) to qword (rax)
CLC Clear Carry Flag
CLD Clear Direction Flag
CLFLUSH sse2 Flush Cache Line
CLI Clear Interrupt Flag
CLTS Clear Task-Switched Flag in CR0
CMC Complement Carry Flag
CMOVA Move if not below
CMOVAE Move if not below or equal
CMOVB Move if below
CMOVBE Move if below or equal
CMOVE Move if zero
CMOVG Move if not less
CMOVGE Move if not less or equal
CMOVL Move if less
CMOVLE Move if less or equal
CMOVNE Move if not zero
CMOVNO Move if not overflow
CMOVNP Move if not parity
CMOVNS Move if not sign
CMOVO Move if overflow
CMOVP Move if parity
CMOVS Move if sign
CMP Compare Two Operands
CMPSB Compare byte at address
CMPSD Compare doubleword at address
CMPSQ Compare quadword at address
CMPSW Compare word at address
CMPXCHG Compare and Exchange
CMPXCHG16B Compare and Exchange 16 Bytes
CMPXCHG8B Compare and Exchange 8 Bytes
CPUID CPU Identification
CQO convert qword (rax) to oword (rdx:rax)
CWD Convert word (ax) to dword (dx:ax)
CWDE Convert word (ax) to dword (eax)
DEC Decrement by 1
DIV Unsigned Divide
EXTRACTPS sse4.1 Extract Packed Single Precision Floating-Point Value
IDIV Signed Divide
IMUL Signed Multiply
INC Increment by 1
INVD Invalidate Internal Caches
INVLPG Invalidate TLB Entry
JA Jump if not below (Jump if above)
JAE Jump if not below or equal (Jump if above or equal)
JB Jump if below
JBE Jump if below or equal
JE Jump if zero (Jump if equal)
JG Jump if not less or equal (Jump if greater)
JGE Jump if not less (Jump if not less)
JL Jump if less
JLE Jump if less or equal
JMP Jump
JNE Jump if not equal
JNO Jump if not overflow
JNP Jump if not parity
JNS Jump if not sign
JO Jump if overflow
JP Jump if parity
JS Jump if sign
LAHF Load Status Flags into AH Register
LDDQU sse3 Load Unaligned Integer 128 Bits
LDMXCSR sse1 Load MXCSR Register
LEA Load Effective Address
LEAVE High Level Procedure Exit
LFENCE sse2 Load Fence
LODSB Load byte at address
LODSD Load doubleword at address
LODSQ Load quadword at address
LODSW Load word at address
MFENCE sse2 Memory Fence
MOV Move
MOVABS Move
MOVAPD sse2 Move Aligned Packed Double-Precision Floating-Point Values
MOVAPS sse1 Move Aligned Packed Single-Precision Floating-Point Values
MOVD mmx/sse2 Move Doubleword
MOVDDUP sse3 Move One Double-FP and Duplicate
MOVDQ2Q sse2 Move Quadword from XMM to MMX Technology Register
MOVDQA sse2 Move Aligned Double Quadword
MOVDQU sse2 Move Unaligned Double Quadword
MOVHLPS sse1 Move Packed Single-Precision Floating-Point Values High to Low
MOVHPD sse2 Move High Packed Double-Precision Floating-Point Values
MOVHPS sse1 Move High Packed Single-Precision Floating-Point Values
MOVLHPS sse1 Move Packed Single-Precision Floating-Point Values Low to High
MOVLPD sse2 Move Low Packed Double-Precision Floating-Point Values
MOVLPS sse1 Move Low Packed Single-Precision Floating-Point Values
MOVMSKPD sse2 Extract Packed Double-Precision Floating-Point Sign Mask
MOVMSKPS sse1 Extract Packed Single-Precision Floating-Point Sign Mask
MOVNTDQ sse2 Store Double Quadword Using Non-Temporal Hint
MOVNTI sse2 Store Doubleword Using Non-Temporal Hint
MOVNTPD sse2 Store Packed Double-Precision Floating-Point Values Using Non-Temporal Hint
MOVNTPS sse1 Store Packed Single-Precision Floating-Point Values Using Non-Temporal Hint
MOVNTQ sse1 Store of Quadword Using Non-Temporal Hint
MOVQ mmx/sse2 Move Quadword
MOVQ2DQ sse2 Move Quadword from MMX Technology to XMM Register
MOVSB Move byte at address
MOVSD Move doubleword at address
MOVSHDUP sse3 Move Packed Single-FP High and Duplicate
MOVSLDUP sse3 Move Packed Single-FP Low and Duplicate
MOVSQ Move quadword at address
MOVSW Move word at address
MOVSX Move with Sign-Extension
MOVSXD Move with Sign-Extension
MOVUPD see2 Move Unaligned Packed Double-Precision Floating- Point Values
MOVUPS see1 Move Unaligned Packed Single-Precision Floating- Point Values
MOVZX Move with Zero-Extend
MUL Unsigned Multiply
MULX bmi2 Unsigned Multiply Without Affecting Flags
NEG Two's Complement Negation
NOP No Operation
NOT One's Complement Negation
OR Logical Inclusive OR
ORPD sse2 Bitwise Logical OR of Double-Precision Floating-Point Values
ORPS sse1 Bitwise Logical OR of Single-Precision Floating-Point Values
PADDB mmx/sse2 Add packed byte integers
PADDD mmx/sse2 Add packed doubleword integers
PADDQ mmx/sse2 Add packed quadword integers
PADDW mmx/sse2 Add packed word integers
PAND mmx/sse2 Logical AND
PANDN mmx/sse2 Logical AND NOT
PAUSE sse2 Spin Loop Hint
PAVGB sse1 Average Packed Unsigned Byte Integers
PAVGW sse1 Average Packed Unsigned Word Integers
PCMPEQB mmx/sse2 Compare Packed Data for Equal (bytes)
PCMPEQD mmx/sse2 Compare Packed Data for Equal (dwords)
PCMPEQW mmx/sse2 Compare Packed Data for Equal (words)
PCMPGTB mmx/sse2 Compare Packed Data for Greater Than (bytes)
PCMPGTD mmx/sse2 Compare Packed Data for Greater Than (dwords)
PCMPGTW mmx/sse2 Compare Packed Data for Greater Than (words)
PMAXSB sse4.1 Maximum of Packed Signed Byte Integers
PMAXSD sse4.1 Maximum of Packed Signed Doubleword Integers
PMAXSW sse1 Maximum of Packed Signed Word Integers
PMAXUB sse1 Maximum of Packed Unsigned Byte Integers
PMAXUD sse4.1 Maximum of Packed Unsigned Doubleword Integers
PMAXUW sse4.1 Maximum of Packed Unsigned Word Integers
PMINSB sse4.1 Minimum of Packed Signed Byte Integers
PMINSD sse4.1 Minimum of Packed Signed Doubleword Integers
PMINSW sse1 Minimum of Packed Signed Word Integers
PMINUB sse1 Minimum of Packed Unsigned Byte Integers
PMINUD sse4.1 Minimum of Packed Unsigned Doubleword Integers
PMINUW sse4.1 Minimum of Packed Unsigned Word Integers
PMOVMSKB sse1 Move Byte Mask
PMOVSXBD sse4.1 Sign Extend 4 Packed Signed 8-bit Integers
PMOVSXBQ sse4.1 Sign Extend 2 Packed Signed 8-bit Integers
PMOVSXBW sse4.1 Sign Extend 8 Packed Signed 8-bit Integers
PMOVSXDQ sse4.1 Sign Extend 2 Packed Signed 32-bit Integers
PMOVSXWD sse4.1 Sign Extend 4 Packed Signed 16-bit Integers
PMOVSXWQ sse4.1 Sign Extend 2 Packed Signed 16-bit Integers
PMOVZXBD sse4.1 Zero Extend 4 Packed Signed 8-bit Integers
PMOVZXBQ sse4.1 Zero Extend 2 Packed Signed 8-bit Integers
PMOVZXBW sse4.1 Zero Extend 8 Packed Signed 8-bit Integers
PMOVZXDQ sse4.1 Zero Extend 2 Packed Signed 32-bit Integers
PMOVZXWD sse4.1 Zero Extend 4 Packed Signed 16-bit Integers
PMOVZXWQ sse4.1 Zero Extend 2 Packed Signed 16-bit Integers
POP Pop a Value from the Stack
POPAL/POPAD Pop All General-Purpose Registers
POPFD Pop Stack into EFLAGS Register
POPFQ Pop Stack into RFLAGS Register
POR mmx/sse2 Bitwise Logical OR
PREFETCH 3DNow Move data from m8 closer to the processor without expecting to write back
PREFETCHNTA mmx/sse1 Move data from m8 closer to the processor using NTA hint
PREFETCHT0 mmx/sse1 Move data from m8 closer to the processor using T0 hint
PREFETCHT1 mmx/sse1 Move data from m8 closer to the processor using T1 hint
PREFETCHT2 mmx/sse1 Move data from m8 closer to the processor using T2 hint
PREFETCHW 3DNow Move data from m8 closer to the processor in anticipation of a write
PSHUFD sse2 Shuffle Packed Doublewords
PSHUFHW sse2 Shuffle Packed High Words
PSHUFLW sse2 Shuffle Packed Low Words
PSHUFW sse1 Shuffle Packed Words
PSLLDQ sse2 Shift Double Quadword Left Logical
PSRLDQ sse2 Shift Double Quadword Right Logical
PSUBB mmx/sse2 Subtract packed byte integers
PSUBD mmx/sse2 Subtract packed doubleword integers
PSUBQ mmx/sse2 Subtract packed quadword integers
PSUBW mmx/sse2 Subtract packed word integers
PTEST sse4.1 Logical Compare
PUNPCKHBW mmx,sse2 Unpack High Data (Unpack and interleave high-order bytes)
PUNPCKHDQ mmx,sse2 Unpack High Data (Unpack and interleave high-order doublewords)
PUNPCKHQDQ sse2 Unpack High Data (Unpack and interleave high-order quadwords)
PUNPCKHWD mmx,sse2 Unpack High Data (Unpack and interleave high-order words)
PUNPCKLBW mmx,sse2 Unpack Low Data (Unpack and interleave low-order bytes)
PUNPCKLDQ mmx,sse2 Unpack Low Data (Unpack and interleave low-order doublewords)
PUNPCKLQDQ sse2 Unpack Low Data (Unpack and interleave low-order quadwords)
PUNPCKLWD mmx,sse2 Unpack Low Data (Unpack and interleave low-order words)
PUSH Push a Value onto the Stack
PUSHAL/PUSHAD Push All General-Purpose Registers
PUSHFD Push EFLAGS Register onto the Stack
PUSHFQ Push RFLAGS Register onto the Stack
PXOR mmx/sse2 Logical Exclusive OR
RCL Rotate Left with Carry
RCR Rotate Right with Carry
RDTSC Read Time-Stamp Counter
RET Return from Procedure
ROL Rotate Left
ROR Rotate Right
RORX bmi2 Rotate Right Logical Without Affecting Flags
SAHF Store AH into Flags
SAL Shift Left
SAR Shift Right Signed
SARX bmi2 Shift arithmetic right without affecting flags
SBB Integer Subtraction with Borrow
SCASB Scan byte at address
SCASD Scan doubleword at address
SCASQ Scan quadword at address
SCASW Scan word at address
SETA Set byte if above
SETAE Set byte if above or equal
SETB Set byte if below
SETBE Set byte if below or equal
SETE Set byte if zero
SETG Set byte if greater
SETGE Set byte if greater or equal
SETL Set byte if less
SETLE Set byte if less or equal
SETNE Set byte if not zero
SETNO Set byte if not overflow
SETNP Set byte if not parity
SETNS Set byte if not sign
SETO Set byte if overflow
SETP Set byte if parity
SETS Set byte if sign
SFENCE sse1 Store Fence
SHL Shift Left
SHLD Double-precision Shift Left
SHLX bmi2 Shift Logical Left Without Affecting Flags
SHR Shift Right Unsigned
SHRD Double Precision Shift Right
SHRX bmi2 Shift Logical Right Without Affecting Flags
STC Set Carry Flag
STD Set Direction Flag
STI Set Interrupt Flag
STMXCSR sse1 Store MXCSR Register State
STOSB Store byte at address
STOSD Store doubleword at address
STOSQ Store quadword at address
STOSW Store word at address
SUB Subtract
SYSCALL Fast System Call
TEST Logical Compare
TZCNT bmi1 Count the Number of Trailing Zero Bits
UNPCKHPD sse2 Unpack and Interleave High Packed Double- Precision Floating-Point Values
UNPCKHPS sse1 Unpack and Interleave High Packed Single-Precision Floating-Point Values
UNPCKLPD sse2 Unpack and Interleave Low Packed Double-Precision Floating-Point Values
UNPCKLPS sse1 Unpack and Interleave Low Packed Single-Precision Floating-Point Values
VMOVDQA avx VEX Move aligned packed integer values
VMOVDQU avx VEX Move unaligned packed integer values
VPAND avx/avx2 VEX Logical AND
VPANDN avx/avx2 VEX Logical AND NOT
VPOR avx/avx2 VEX Logical OR
VPSHUFD avx/avx2 VEX Shuffle Packed Doublewords
VPTEST avx VEX Logical Compare
VPXOR avx/avx2 VEX Logical XOR
WBINVD Write Back and Invalidate Cache
XADD Exchange and Add
XCHG Exchange Register/Memory with Register
XOR Logical Exclusive OR
XORPD sse2 Bitwise Logical XOR for Double-Precision Floating-Point Values
XORPS sse1 Bitwise Logical XOR for Single-Precision Floating-Point Values