Permalink
Fetching contributors…
Cannot retrieve contributors at this time
12644 lines (10071 sloc) 591 KB
//! \file
/*
** Copyright (C) - Triton
**
** This program is under the terms of the BSD License.
*/
#include <triton/cpuSize.hpp>
#include <triton/exceptions.hpp>
#include <triton/x86Semantics.hpp>
#include <triton/x86Specifications.hpp>
#include <triton/astContext.hpp>
/*! \page SMT_Semantics_Supported_page SMT Semantics Supported
\brief [**internal**] All information about the supported semantics.
\tableofcontents
\section SMT_Semantics_Supported_description Description
<hr>
Here is the instructions' list of what **Triton** can convert into \ref py_AstNode_page. 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](x86Semantics_8cpp_source.html). Thanks to `wisk` and his
[Medusa project](https://github.com/wisk/medusa/blob/dev/arch/x86.yaml) which has been really useful.
\subsection SMT_Semantics_Supported_x86 x86 and x86-64 SMT semantics supported
Mnemonic | Extensions | Description
-----------------------------|------------|------------
AAA | | ASCII Adjust After Addition
AAD | | ASCII Adjust AX Before Division
AAM | | ASCII Adjust AX After Multiply
AAS | | ASCII Adjust AL After Subtraction
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
WAIT | | Wait
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
*/
namespace triton {
namespace arch {
namespace x86 {
x86Semantics::x86Semantics(triton::arch::Architecture* architecture,
triton::engines::symbolic::SymbolicEngine* symbolicEngine,
triton::engines::taint::TaintEngine* taintEngine,
triton::ast::AstContext& astCtxt) : astCtxt(astCtxt) {
this->architecture = architecture;
this->symbolicEngine = symbolicEngine;
this->taintEngine = taintEngine;
if (architecture == nullptr)
throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The architecture API must be defined.");
if (this->symbolicEngine == nullptr)
throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The symbolic engine API must be defined.");
if (this->taintEngine == nullptr)
throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The taint engines API must be defined.");
}
bool x86Semantics::buildSemantics(triton::arch::Instruction& inst) {
switch (inst.getType()) {
case ID_INS_AAA: this->aaa_s(inst); break;
case ID_INS_AAD: this->aad_s(inst); break;
case ID_INS_AAM: this->aam_s(inst); break;
case ID_INS_AAS: this->aas_s(inst); break;
case ID_INS_ADC: this->adc_s(inst); break;
case ID_INS_ADCX: this->adcx_s(inst); break;
case ID_INS_ADD: this->add_s(inst); break;
case ID_INS_AND: this->and_s(inst); break;
case ID_INS_ANDN: this->andn_s(inst); break;
case ID_INS_ANDNPD: this->andnpd_s(inst); break;
case ID_INS_ANDNPS: this->andnps_s(inst); break;
case ID_INS_ANDPD: this->andpd_s(inst); break;
case ID_INS_ANDPS: this->andps_s(inst); break;
case ID_INS_BEXTR: this->bextr_s(inst); break;
case ID_INS_BLSI: this->blsi_s(inst); break;
case ID_INS_BLSMSK: this->blsmsk_s(inst); break;
case ID_INS_BLSR: this->blsr_s(inst); break;
case ID_INS_BSF: this->bsf_s(inst); break;
case ID_INS_BSR: this->bsr_s(inst); break;
case ID_INS_BSWAP: this->bswap_s(inst); break;
case ID_INS_BT: this->bt_s(inst); break;
case ID_INS_BTC: this->btc_s(inst); break;
case ID_INS_BTR: this->btr_s(inst); break;
case ID_INS_BTS: this->bts_s(inst); break;
case ID_INS_CALL: this->call_s(inst); break;
case ID_INS_CBW: this->cbw_s(inst); break;
case ID_INS_CDQ: this->cdq_s(inst); break;
case ID_INS_CDQE: this->cdqe_s(inst); break;
case ID_INS_CLC: this->clc_s(inst); break;
case ID_INS_CLD: this->cld_s(inst); break;
case ID_INS_CLFLUSH: this->clflush_s(inst); break;
case ID_INS_CLTS: this->clts_s(inst); break;
case ID_INS_CLI: this->cli_s(inst); break;
case ID_INS_CMC: this->cmc_s(inst); break;
case ID_INS_CMOVA: this->cmova_s(inst); break;
case ID_INS_CMOVAE: this->cmovae_s(inst); break;
case ID_INS_CMOVB: this->cmovb_s(inst); break;
case ID_INS_CMOVBE: this->cmovbe_s(inst); break;
case ID_INS_CMOVE: this->cmove_s(inst); break;
case ID_INS_CMOVG: this->cmovg_s(inst); break;
case ID_INS_CMOVGE: this->cmovge_s(inst); break;
case ID_INS_CMOVL: this->cmovl_s(inst); break;
case ID_INS_CMOVLE: this->cmovle_s(inst); break;
case ID_INS_CMOVNE: this->cmovne_s(inst); break;
case ID_INS_CMOVNO: this->cmovno_s(inst); break;
case ID_INS_CMOVNP: this->cmovnp_s(inst); break;
case ID_INS_CMOVNS: this->cmovns_s(inst); break;
case ID_INS_CMOVO: this->cmovo_s(inst); break;
case ID_INS_CMOVP: this->cmovp_s(inst); break;
case ID_INS_CMOVS: this->cmovs_s(inst); break;
case ID_INS_CMP: this->cmp_s(inst); break;
case ID_INS_CMPSB: this->cmpsb_s(inst); break;
case ID_INS_CMPSD: this->cmpsd_s(inst); break;
case ID_INS_CMPSQ: this->cmpsq_s(inst); break;
case ID_INS_CMPSW: this->cmpsw_s(inst); break;
case ID_INS_CMPXCHG: this->cmpxchg_s(inst); break;
case ID_INS_CMPXCHG16B: this->cmpxchg16b_s(inst); break;
case ID_INS_CMPXCHG8B: this->cmpxchg8b_s(inst); break;
case ID_INS_CPUID: this->cpuid_s(inst); break;
case ID_INS_CQO: this->cqo_s(inst); break;
case ID_INS_CWD: this->cwd_s(inst); break;
case ID_INS_CWDE: this->cwde_s(inst); break;
case ID_INS_DEC: this->dec_s(inst); break;
case ID_INS_DIV: this->div_s(inst); break;
case ID_INS_EXTRACTPS: this->extractps_s(inst); break;
case ID_INS_IDIV: this->idiv_s(inst); break;
case ID_INS_IMUL: this->imul_s(inst); break;
case ID_INS_INC: this->inc_s(inst); break;
case ID_INS_INVD: this->invd_s(inst); break;
case ID_INS_INVLPG: this->invlpg_s(inst); break;
case ID_INS_JA: this->ja_s(inst); break;
case ID_INS_JAE: this->jae_s(inst); break;
case ID_INS_JB: this->jb_s(inst); break;
case ID_INS_JBE: this->jbe_s(inst); break;
case ID_INS_JE: this->je_s(inst); break;
case ID_INS_JG: this->jg_s(inst); break;
case ID_INS_JGE: this->jge_s(inst); break;
case ID_INS_JL: this->jl_s(inst); break;
case ID_INS_JLE: this->jle_s(inst); break;
case ID_INS_JMP: this->jmp_s(inst); break;
case ID_INS_JNE: this->jne_s(inst); break;
case ID_INS_JNO: this->jno_s(inst); break;
case ID_INS_JNP: this->jnp_s(inst); break;
case ID_INS_JNS: this->jns_s(inst); break;
case ID_INS_JO: this->jo_s(inst); break;
case ID_INS_JP: this->jp_s(inst); break;
case ID_INS_JS: this->js_s(inst); break;
case ID_INS_LAHF: this->lahf_s(inst); break;
case ID_INS_LDDQU: this->lddqu_s(inst); break;
case ID_INS_LDMXCSR: this->ldmxcsr_s(inst); break;
case ID_INS_LEA: this->lea_s(inst); break;
case ID_INS_LEAVE: this->leave_s(inst); break;
case ID_INS_LFENCE: this->lfence_s(inst); break;
case ID_INS_LODSB: this->lodsb_s(inst); break;
case ID_INS_LODSD: this->lodsd_s(inst); break;
case ID_INS_LODSQ: this->lodsq_s(inst); break;
case ID_INS_LODSW: this->lodsw_s(inst); break;
case ID_INS_MFENCE: this->mfence_s(inst); break;
case ID_INS_MOV: this->mov_s(inst); break;
case ID_INS_MOVABS: this->movabs_s(inst); break;
case ID_INS_MOVAPD: this->movapd_s(inst); break;
case ID_INS_MOVAPS: this->movaps_s(inst); break;
case ID_INS_MOVD: this->movd_s(inst); break;
case ID_INS_MOVDDUP: this->movddup_s(inst); break;
case ID_INS_MOVDQ2Q: this->movdq2q_s(inst); break;
case ID_INS_MOVDQA: this->movdqa_s(inst); break;
case ID_INS_MOVDQU: this->movdqu_s(inst); break;
case ID_INS_MOVHLPS: this->movhlps_s(inst); break;
case ID_INS_MOVHPD: this->movhpd_s(inst); break;
case ID_INS_MOVHPS: this->movhps_s(inst); break;
case ID_INS_MOVLHPS: this->movlhps_s(inst); break;
case ID_INS_MOVLPD: this->movlpd_s(inst); break;
case ID_INS_MOVLPS: this->movlps_s(inst); break;
case ID_INS_MOVMSKPD: this->movmskpd_s(inst); break;
case ID_INS_MOVMSKPS: this->movmskps_s(inst); break;
case ID_INS_MOVNTDQ: this->movntdq_s(inst); break;
case ID_INS_MOVNTI: this->movnti_s(inst); break;
case ID_INS_MOVNTPD: this->movntpd_s(inst); break;
case ID_INS_MOVNTPS: this->movntps_s(inst); break;
case ID_INS_MOVNTQ: this->movntq_s(inst); break;
case ID_INS_MOVQ2DQ: this->movq2dq_s(inst); break;
case ID_INS_MOVQ: this->movq_s(inst); break;
case ID_INS_MOVSB: this->movsb_s(inst); break;
case ID_INS_MOVSD: this->movsd_s(inst); break;
case ID_INS_MOVSHDUP: this->movshdup_s(inst); break;
case ID_INS_MOVSLDUP: this->movsldup_s(inst); break;
case ID_INS_MOVSQ: this->movsq_s(inst); break;
case ID_INS_MOVSW: this->movsw_s(inst); break;
case ID_INS_MOVSX: this->movsx_s(inst); break;
case ID_INS_MOVSXD: this->movsxd_s(inst); break;
case ID_INS_MOVUPD: this->movupd_s(inst); break;
case ID_INS_MOVUPS: this->movups_s(inst); break;
case ID_INS_MOVZX: this->movzx_s(inst); break;
case ID_INS_MUL: this->mul_s(inst); break;
case ID_INS_MULX: this->mulx_s(inst); break;
case ID_INS_NEG: this->neg_s(inst); break;
case ID_INS_NOP: this->nop_s(inst); break;
case ID_INS_NOT: this->not_s(inst); break;
case ID_INS_OR: this->or_s(inst); break;
case ID_INS_ORPD: this->orpd_s(inst); break;
case ID_INS_ORPS: this->orps_s(inst); break;
case ID_INS_PADDB: this->paddb_s(inst); break;
case ID_INS_PADDD: this->paddd_s(inst); break;
case ID_INS_PADDQ: this->paddq_s(inst); break;
case ID_INS_PADDW: this->paddw_s(inst); break;
case ID_INS_PAND: this->pand_s(inst); break;
case ID_INS_PANDN: this->pandn_s(inst); break;
case ID_INS_PAUSE: this->pause_s(inst); break;
case ID_INS_PAVGB: this->pavgb_s(inst); break;
case ID_INS_PAVGW: this->pavgw_s(inst); break;
case ID_INS_PCMPEQB: this->pcmpeqb_s(inst); break;
case ID_INS_PCMPEQD: this->pcmpeqd_s(inst); break;
case ID_INS_PCMPEQW: this->pcmpeqw_s(inst); break;
case ID_INS_PCMPGTB: this->pcmpgtb_s(inst); break;
case ID_INS_PCMPGTD: this->pcmpgtd_s(inst); break;
case ID_INS_PCMPGTW: this->pcmpgtw_s(inst); break;
case ID_INS_PMAXSB: this->pmaxsb_s(inst); break;
case ID_INS_PMAXSD: this->pmaxsd_s(inst); break;
case ID_INS_PMAXSW: this->pmaxsw_s(inst); break;
case ID_INS_PMAXUB: this->pmaxub_s(inst); break;
case ID_INS_PMAXUD: this->pmaxud_s(inst); break;
case ID_INS_PMAXUW: this->pmaxuw_s(inst); break;
case ID_INS_PMINSB: this->pminsb_s(inst); break;
case ID_INS_PMINSD: this->pminsd_s(inst); break;
case ID_INS_PMINSW: this->pminsw_s(inst); break;
case ID_INS_PMINUB: this->pminub_s(inst); break;
case ID_INS_PMINUD: this->pminud_s(inst); break;
case ID_INS_PMINUW: this->pminuw_s(inst); break;
case ID_INS_PMOVMSKB: this->pmovmskb_s(inst); break;
case ID_INS_PMOVSXBD: this->pmovsxbd_s(inst); break;
case ID_INS_PMOVSXBQ: this->pmovsxbq_s(inst); break;
case ID_INS_PMOVSXBW: this->pmovsxbw_s(inst); break;
case ID_INS_PMOVSXDQ: this->pmovsxdq_s(inst); break;
case ID_INS_PMOVSXWD: this->pmovsxwd_s(inst); break;
case ID_INS_PMOVSXWQ: this->pmovsxwq_s(inst); break;
case ID_INS_PMOVZXBD: this->pmovzxbd_s(inst); break;
case ID_INS_PMOVZXBQ: this->pmovzxbq_s(inst); break;
case ID_INS_PMOVZXBW: this->pmovzxbw_s(inst); break;
case ID_INS_PMOVZXDQ: this->pmovzxdq_s(inst); break;
case ID_INS_PMOVZXWD: this->pmovzxwd_s(inst); break;
case ID_INS_PMOVZXWQ: this->pmovzxwq_s(inst); break;
case ID_INS_POP: this->pop_s(inst); break;
case ID_INS_POPAL: this->popal_s(inst); break;
case ID_INS_POPFD: this->popfd_s(inst); break;
case ID_INS_POPFQ: this->popfq_s(inst); break;
case ID_INS_POR: this->por_s(inst); break;
case ID_INS_PREFETCH: this->prefetchx_s(inst); break;
case ID_INS_PREFETCHNTA: this->prefetchx_s(inst); break;
case ID_INS_PREFETCHT0: this->prefetchx_s(inst); break;
case ID_INS_PREFETCHT1: this->prefetchx_s(inst); break;
case ID_INS_PREFETCHT2: this->prefetchx_s(inst); break;
case ID_INS_PREFETCHW: this->prefetchx_s(inst); break;
case ID_INS_PSHUFD: this->pshufd_s(inst); break;
case ID_INS_PSHUFHW: this->pshufhw_s(inst); break;
case ID_INS_PSHUFLW: this->pshuflw_s(inst); break;
case ID_INS_PSHUFW: this->pshufw_s(inst); break;
case ID_INS_PSLLDQ: this->pslldq_s(inst); break;
case ID_INS_PSRLDQ: this->psrldq_s(inst); break;
case ID_INS_PSUBB: this->psubb_s(inst); break;
case ID_INS_PSUBD: this->psubd_s(inst); break;
case ID_INS_PSUBQ: this->psubq_s(inst); break;
case ID_INS_PSUBW: this->psubw_s(inst); break;
case ID_INS_PTEST: this->ptest_s(inst); break;
case ID_INS_PUNPCKHBW: this->punpckhbw_s(inst); break;
case ID_INS_PUNPCKHDQ: this->punpckhdq_s(inst); break;
case ID_INS_PUNPCKHQDQ: this->punpckhqdq_s(inst); break;
case ID_INS_PUNPCKHWD: this->punpckhwd_s(inst); break;
case ID_INS_PUNPCKLBW: this->punpcklbw_s(inst); break;
case ID_INS_PUNPCKLDQ: this->punpckldq_s(inst); break;
case ID_INS_PUNPCKLQDQ: this->punpcklqdq_s(inst); break;
case ID_INS_PUNPCKLWD: this->punpcklwd_s(inst); break;
case ID_INS_PUSH: this->push_s(inst); break;
case ID_INS_PUSHAL: this->pushal_s(inst); break;
case ID_INS_PUSHFD: this->pushfd_s(inst); break;
case ID_INS_PUSHFQ: this->pushfq_s(inst); break;
case ID_INS_PXOR: this->pxor_s(inst); break;
case ID_INS_RCL: this->rcl_s(inst); break;
case ID_INS_RCR: this->rcr_s(inst); break;
case ID_INS_RDTSC: this->rdtsc_s(inst); break;
case ID_INS_RET: this->ret_s(inst); break;
case ID_INS_ROL: this->rol_s(inst); break;
case ID_INS_ROR: this->ror_s(inst); break;
case ID_INS_RORX: this->rorx_s(inst); break;
case ID_INS_SAHF: this->sahf_s(inst); break;
case ID_INS_SAL: this->shl_s(inst); break;
case ID_INS_SAR: this->sar_s(inst); break;
case ID_INS_SARX: this->sarx_s(inst); break;
case ID_INS_SBB: this->sbb_s(inst); break;
case ID_INS_SCASB: this->scasb_s(inst); break;
case ID_INS_SCASD: this->scasd_s(inst); break;
case ID_INS_SCASQ: this->scasq_s(inst); break;
case ID_INS_SCASW: this->scasw_s(inst); break;
case ID_INS_SETA: this->seta_s(inst); break;
case ID_INS_SETAE: this->setae_s(inst); break;
case ID_INS_SETB: this->setb_s(inst); break;
case ID_INS_SETBE: this->setbe_s(inst); break;
case ID_INS_SETE: this->sete_s(inst); break;
case ID_INS_SETG: this->setg_s(inst); break;
case ID_INS_SETGE: this->setge_s(inst); break;
case ID_INS_SETL: this->setl_s(inst); break;
case ID_INS_SETLE: this->setle_s(inst); break;
case ID_INS_SETNE: this->setne_s(inst); break;
case ID_INS_SETNO: this->setno_s(inst); break;
case ID_INS_SETNP: this->setnp_s(inst); break;
case ID_INS_SETNS: this->setns_s(inst); break;
case ID_INS_SETO: this->seto_s(inst); break;
case ID_INS_SETP: this->setp_s(inst); break;
case ID_INS_SETS: this->sets_s(inst); break;
case ID_INS_SFENCE: this->sfence_s(inst); break;
case ID_INS_SHL: this->shl_s(inst); break;
case ID_INS_SHLD: this->shld_s(inst); break;
case ID_INS_SHLX: this->shlx_s(inst); break;
case ID_INS_SHR: this->shr_s(inst); break;
case ID_INS_SHRD: this->shrd_s(inst); break;
case ID_INS_SHRX: this->shrx_s(inst); break;
case ID_INS_STC: this->stc_s(inst); break;
case ID_INS_STD: this->std_s(inst); break;
case ID_INS_STI: this->sti_s(inst); break;
case ID_INS_STMXCSR: this->stmxcsr_s(inst); break;
case ID_INS_STOSB: this->stosb_s(inst); break;
case ID_INS_STOSD: this->stosd_s(inst); break;
case ID_INS_STOSQ: this->stosq_s(inst); break;
case ID_INS_STOSW: this->stosw_s(inst); break;
case ID_INS_SUB: this->sub_s(inst); break;
case ID_INS_SYSCALL: this->syscall_s(inst); break;
case ID_INS_TEST: this->test_s(inst); break;
case ID_INS_TZCNT: this->tzcnt_s(inst); break;
case ID_INS_UNPCKHPD: this->unpckhpd_s(inst); break;
case ID_INS_UNPCKHPS: this->unpckhps_s(inst); break;
case ID_INS_UNPCKLPD: this->unpcklpd_s(inst); break;
case ID_INS_UNPCKLPS: this->unpcklps_s(inst); break;
case ID_INS_VMOVDQA: this->vmovdqa_s(inst); break;
case ID_INS_VMOVDQU: this->vmovdqu_s(inst); break;
case ID_INS_VPAND: this->vpand_s(inst); break;
case ID_INS_VPANDN: this->vpandn_s(inst); break;
case ID_INS_VPOR: this->vpor_s(inst); break;
case ID_INS_VPTEST: this->vptest_s(inst); break;
case ID_INS_VPSHUFD: this->vpshufd_s(inst); break;
case ID_INS_VPXOR: this->vpxor_s(inst); break;
case ID_INS_WAIT: this->wait_s(inst); break;
case ID_INS_WBINVD: this->wbinvd_s(inst); break;
case ID_INS_XADD: this->xadd_s(inst); break;
case ID_INS_XCHG: this->xchg_s(inst); break;
case ID_INS_XOR: this->xor_s(inst); break;
case ID_INS_XORPD: this->xorpd_s(inst); break;
case ID_INS_XORPS: this->xorps_s(inst); break;
default:
return false;
}
return true;
}
triton::uint64 x86Semantics::alignAddStack_s(triton::arch::Instruction& inst, triton::uint32 delta) {
auto dst = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_SP));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->astCtxt.bv(delta, dst.getBitSize());
/* Create the semantics */
auto node = this->astCtxt.bvadd(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "Stack alignment");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Return the new stack value */
return node->evaluate().convert_to<triton::uint64>();
}
triton::uint64 x86Semantics::alignSubStack_s(triton::arch::Instruction& inst, triton::uint32 delta) {
auto dst = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_SP));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->astCtxt.bv(delta, dst.getBitSize());
/* Create the semantics */
auto node = this->astCtxt.bvsub(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "Stack alignment");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Return the new stack value */
return node->evaluate().convert_to<triton::uint64>();
}
void x86Semantics::clearFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
/* Create the semantics */
auto node = this->astCtxt.bv(0, 1);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, flag, comment);
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
}
void x86Semantics::setFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
/* Create the semantics */
auto node = this->astCtxt.bv(1, 1);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, flag, comment);
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
}
void x86Semantics::controlFlow_s(triton::arch::Instruction& inst) {
auto pc = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_IP));
auto counter = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_CX));
auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_ZF));
switch (inst.getPrefix()) {
case triton::arch::x86::ID_PREFIX_REP: {
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
/* Create the semantics for Counter */
auto node1 = this->astCtxt.ite(
this->astCtxt.equal(op1, this->astCtxt.bv(0, counter.getBitSize())),
op1,
this->astCtxt.bvsub(op1, this->astCtxt.bv(1, counter.getBitSize()))
);
/* Create the semantics for PC */
auto node2 = this->astCtxt.ite(
this->astCtxt.equal(node1, this->astCtxt.bv(0, counter.getBitSize())),
this->astCtxt.bv(inst.getNextAddress(), pc.getBitSize()),
this->astCtxt.bv(inst.getAddress(), pc.getBitSize())
);
/* Create symbolic expression */
auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
/* Spread taint for PC */
expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
break;
}
case triton::arch::x86::ID_PREFIX_REPE: {
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
auto op2 = this->symbolicEngine->getOperandAst(inst, zf);
/* Create the semantics for Counter */
auto node1 = this->astCtxt.ite(
this->astCtxt.equal(op1, this->astCtxt.bv(0, counter.getBitSize())),
op1,
this->astCtxt.bvsub(op1, this->astCtxt.bv(1, counter.getBitSize()))
);
/* Create the semantics for PC */
auto node2 = this->astCtxt.ite(
this->astCtxt.lor(
this->astCtxt.equal(node1, this->astCtxt.bv(0, counter.getBitSize())),
this->astCtxt.equal(op2, this->astCtxt.bvfalse())
),
this->astCtxt.bv(inst.getNextAddress(), pc.getBitSize()),
this->astCtxt.bv(inst.getAddress(), pc.getBitSize())
);
/* Create symbolic expression */
auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
break;
}
case triton::arch::x86::ID_PREFIX_REPNE: {
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
auto op2 = this->symbolicEngine->getOperandAst(inst, zf);
/* Create the semantics for Counter */
auto node1 = this->astCtxt.ite(
this->astCtxt.equal(op1, this->astCtxt.bv(0, counter.getBitSize())),
op1,
this->astCtxt.bvsub(op1, this->astCtxt.bv(1, counter.getBitSize()))
);
/* Create the semantics for PC */
auto node2 = this->astCtxt.ite(
this->astCtxt.lor(
this->astCtxt.equal(node1, this->astCtxt.bv(0, counter.getBitSize())),
this->astCtxt.equal(op2, this->astCtxt.bvtrue())
),
this->astCtxt.bv(inst.getNextAddress(), pc.getBitSize()),
this->astCtxt.bv(inst.getAddress(), pc.getBitSize())
);
/* Create symbolic expression */
auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
break;
}
default: {
/* Create the semantics */
auto node = this->astCtxt.bv(inst.getNextAddress(), pc.getBitSize());
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicRegisterExpression(inst, node, this->architecture->getParentRegister(ID_REG_IP), "Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_IP), triton::engines::taint::UNTAINTED);
break;
}
}
}
void x86Semantics::af_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* af = 0x10 == (0x10 & (regDst ^ op1 ^ op2))
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.bv(0x10, bvSize),
this->astCtxt.bvand(
this->astCtxt.bv(0x10, bvSize),
this->astCtxt.bvxor(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bvxor(op1, op2)
)
)
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_AF), "Adjust flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_AF), parent->isTainted);
}
void x86Semantics::afAaa_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = dst.getBitSize();
/*
* Create the semantic.
* af = 1 if ((AL AND 0FH) > 9) or (AF = 1) then 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.lor(
this->astCtxt.bvugt(
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, bvSize)),
this->astCtxt.bv(9, bvSize)
),
this->astCtxt.equal(op3, this->astCtxt.bvtrue())
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_AF), "Adjust flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_AF), parent->isTainted);
}
void x86Semantics::afNeg_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* af = 0x10 == (0x10 & (op1 ^ regDst))
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.bv(0x10, bvSize),
this->astCtxt.bvand(
this->astCtxt.bv(0x10, bvSize),
this->astCtxt.bvxor(
op1,
this->astCtxt.extract(high, low, this->astCtxt.reference(parent))
)
)
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_AF), "Adjust flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_AF), parent->isTainted);
}
void x86Semantics::cfAaa_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = dst.getBitSize();
/*
* Create the semantic.
* cf = 1 if ((AL AND 0FH) > 9) or (AF = 1) then 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.lor(
this->astCtxt.bvugt(
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, bvSize)),
this->astCtxt.bv(9, bvSize)
),
this->astCtxt.equal(op3, this->astCtxt.bvtrue())
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfAdd_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* cf = MSB((op1 & op2) ^ ((op1 ^ op2 ^ parent) & (op1 ^ op2)));
*/
auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
this->astCtxt.bvxor(
this->astCtxt.bvand(op1, op2),
this->astCtxt.bvand(
this->astCtxt.bvxor(
this->astCtxt.bvxor(op1, op2),
this->astCtxt.extract(high, low, this->astCtxt.reference(parent))
),
this->astCtxt.bvxor(op1, op2))
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfBlsi_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* cf = 0 if op1 == 0 else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfBlsmsk_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* cf = 1 if op1 == 0 else 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfBlsr_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* cf = 1 if op1 == 0 else 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfImul_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& res,
bool vol) {
/*
* Create the semantic.
* cf = 0 if sx(dst) == node else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.sx(dst.getBitSize(), op1),
res
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfMul_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* cf = 0 if op1 == 0 else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfNeg_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* cf = 0 if op1 == 0 else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfPtest_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* cf = 0 == regDst
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bv(0, bvSize)
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfRcl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
const triton::ast::SharedAbstractNode& result,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto high = result->getBitvectorSize() - 1;
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(high, high, result)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfRcr_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& result,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto high = result->getBitvectorSize() - 1;
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(high, high, result) /* yes it's should be LSB, but here it's a trick :-) */
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfRol_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(low, low, this->astCtxt.reference(parent))
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfRor_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(high, high, this->astCtxt.reference(parent))
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfSar_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/*
* Create the semantic.
* if op2 != 0:
* if op2 > bvSize:
* cf.id = ((op1 >> (bvSize - 1)) & 1)
* else:
* cf.id = ((op1 >> (op2 - 1)) & 1)
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.ite(
this->astCtxt.bvugt(op2, this->astCtxt.bv(bvSize, bvSize)),
this->astCtxt.extract(0, 0, this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize)))),
this->astCtxt.extract(0, 0, this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(op2, this->astCtxt.bv(1, bvSize))))
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfShl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/*
* Create the semantic.
* cf = (op1 >> ((bvSize - op2) & 1) if op2 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(0, 0,
this->astCtxt.bvlshr(
op1,
this->astCtxt.bvsub(
this->astCtxt.bv(bvSize, bvSize),
op2
)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfShld_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = op3->getBitvectorSize();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/*
* Create the semantic.
* cf = MSB(rol(op3, concat(op2,op1))) if op3 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(
dst.getBitSize(), dst.getBitSize(),
this->astCtxt.bvrol(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfShr_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/*
* Create the semantic.
* cf = ((op1 >> (op2 - 1)) & 1) if op2 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(0, 0,
this->astCtxt.bvlshr(
op1,
this->astCtxt.bvsub(
op2,
this->astCtxt.bv(1, bvSize))
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfShrd_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = op3->getBitvectorSize();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/*
* Create the semantic.
* cf = MSB(ror(op3, concat(op2,op1))) if op3 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, cf),
this->astCtxt.extract(
(dst.getBitSize() * 2)-1, (dst.getBitSize()*2)-1,
this->astCtxt.bvror(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::cfSub_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* cf = extract(bvSize, bvSize (((op1 ^ op2 ^ res) ^ ((op1 ^ res) & (op1 ^ op2)))))
*/
auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
this->astCtxt.bvxor(
this->astCtxt.bvxor(op1, this->astCtxt.bvxor(op2, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))),
this->astCtxt.bvand(
this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent))),
this->astCtxt.bvxor(op1, op2)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_CF), "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_CF), parent->isTainted);
}
void x86Semantics::ofAdd_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* of = MSB((op1 ^ ~op2) & (op1 ^ regDst))
*/
auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
this->astCtxt.bvand(
this->astCtxt.bvxor(op1, this->astCtxt.bvnot(op2)),
this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofImul_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& res,
bool vol) {
/*
* Create the semantic.
* of = 0 if sx(dst) == node else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.sx(dst.getBitSize(), op1),
res
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofMul_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
/*
* Create the semantic.
* of = 0 if up == 0 else 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op1,
this->astCtxt.bv(0, dst.getBitSize())
),
this->astCtxt.bv(0, 1),
this->astCtxt.bv(1, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofNeg_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* of = (res & op1) >> (bvSize - 1) & 1
*/
auto node = this->astCtxt.extract(0, 0,
this->astCtxt.bvlshr(
this->astCtxt.bvand(this->astCtxt.extract(high, low, this->astCtxt.reference(parent)), op1),
this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize))
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofRol_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(1, bvSize)),
this->astCtxt.bvxor(
this->astCtxt.extract(high, high, this->astCtxt.reference(parent)),
this->symbolicEngine->getOperandAst(inst, cf)
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofRor_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(1, bvSize)),
this->astCtxt.bvxor(
this->astCtxt.extract(high, high, this->astCtxt.reference(parent)),
this->astCtxt.extract(high-1, high-1, this->astCtxt.reference(parent))
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofRcr_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = op2->getBitvectorSize();
auto high = dst.getBitSize()-1;
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(1, bvSize)),
this->astCtxt.bvxor(
this->astCtxt.extract(high, high, op1),
this->symbolicEngine->getOperandAst(inst, cf)
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofSar_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
/*
* Create the semantic.
* of = 0 if op2 == 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.land(
this->astCtxt.equal(
/* #672 */
this->astCtxt.reference(parent),
this->astCtxt.reference(parent)
/* ---- */
),
this->astCtxt.equal(
op2,
this->astCtxt.bv(1, bvSize)
)
),
this->astCtxt.bv(0, 1),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofShl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
/*
* Create the semantic.
* of = ((op1 >> (bvSize - 1)) ^ (op1 >> (bvSize - 2))) & 1; if op2 == 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op2,
this->astCtxt.bv(1, bvSize)),
this->astCtxt.extract(0, 0,
this->astCtxt.bvxor(
this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize))),
this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(2, bvSize)))
)
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofShld_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = dst.getBitSize();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
/*
* Create the semantic.
* of = MSB(rol(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.zx(bvSize - op3->getBitvectorSize(), op3),
this->astCtxt.bv(1, bvSize)),
this->astCtxt.bvxor(
this->astCtxt.extract(
dst.getBitSize()-1, dst.getBitSize()-1,
this->astCtxt.bvrol(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
),
this->astCtxt.extract(dst.getBitSize()-1, dst.getBitSize()-1, op1)
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofShr_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
/*
* Create the semantic.
* of = ((op1 >> (bvSize - 1)) & 1) if op2 == 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
op2,
this->astCtxt.bv(1, bvSize)),
this->astCtxt.extract(0, 0, this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize)))),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofShrd_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = dst.getBitSize();
auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_OF));
/*
* Create the semantic.
* of = MSB(ror(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.zx(bvSize - op3->getBitvectorSize(), op3),
this->astCtxt.bv(1, bvSize)),
this->astCtxt.bvxor(
this->astCtxt.extract(
dst.getBitSize()-1, dst.getBitSize()-1,
this->astCtxt.bvror(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
),
this->astCtxt.extract(dst.getBitSize()-1, dst.getBitSize()-1, op1)
),
this->symbolicEngine->getOperandAst(inst, of)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::ofSub_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* of = high:bool((op1 ^ op2) & (op1 ^ regDst))
*/
auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
this->astCtxt.bvand(
this->astCtxt.bvxor(op1, op2),
this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_OF), "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_OF), parent->isTainted);
}
void x86Semantics::pf_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
bool vol) {
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
/*
* Create the semantics.
*
* pf is set to one if there is an even number of bit set to 1 in the least
* significant byte of the result.
*/
auto node = this->astCtxt.bv(1, 1);
for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
node = this->astCtxt.bvxor(
node,
this->astCtxt.extract(0, 0,
this->astCtxt.bvlshr(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bv(counter, BYTE_SIZE_BIT)
)
)
);
}
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_PF), "Parity flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_PF), parent->isTainted);
}
void x86Semantics::pfShl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_PF));
/*
* Create the semantics.
* pf if op2 != 0
*/
auto node1 = this->astCtxt.bv(1, 1);
for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
node1 = this->astCtxt.bvxor(
node1,
this->astCtxt.extract(0, 0,
this->astCtxt.bvlshr(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bv(counter, BYTE_SIZE_BIT)
)
)
);
}
auto node2 = this->astCtxt.ite(
this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, pf),
node1
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node2, this->architecture->getRegister(ID_REG_PF), "Parity flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_PF), parent->isTainted);
}
void x86Semantics::sf_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
bool vol) {
auto bvSize = dst.getBitSize();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* sf = high:bool(regDst)
*/
auto node = this->astCtxt.extract(high, high, this->astCtxt.reference(parent));
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_SF), "Sign flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_SF), parent->isTainted);
}
void x86Semantics::sfShl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_SF));
/*
* Create the semantic.
* sf if op2 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, sf),
this->astCtxt.extract(high, high, this->astCtxt.reference(parent))
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_SF), "Sign flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_SF), parent->isTainted);
}
void x86Semantics::sfShld_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = op3->getBitvectorSize();
auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_SF));
/*
* Create the semantic.
* MSB(rol(op3, concat(op2,op1))) if op3 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, sf),
this->astCtxt.extract(
dst.getBitSize()-1, dst.getBitSize()-1,
this->astCtxt.bvrol(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_SF), "Sign flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_SF), parent->isTainted);
}
void x86Semantics::sfShrd_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op1,
const triton::ast::SharedAbstractNode& op2,
const triton::ast::SharedAbstractNode& op3,
bool vol) {
auto bvSize = op3->getBitvectorSize();
auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_SF));
/*
* Create the semantic.
* MSB(ror(op3, concat(op2,op1))) if op3 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, sf),
this->astCtxt.extract(
dst.getBitSize()-1, dst.getBitSize()-1,
this->astCtxt.bvror(
this->astCtxt.decimal(op3->evaluate()),
this->astCtxt.concat(op2, op1)
)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_SF), "Sign flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_SF), parent->isTainted);
}
void x86Semantics::zf_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
/*
* Create the semantic.
* zf = 0 == regDst
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bv(0, bvSize)
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_ZF), "Zero flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_ZF), parent->isTainted);
}
void x86Semantics::zfBsf_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& src,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
/*
* Create the semantic.
* zf = 1 if op2 == 0 else 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, src.getBitSize())),
this->astCtxt.bvtrue(),
this->astCtxt.bvfalse()
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_ZF), "Zero flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_ZF), parent->isTainted);
}
void x86Semantics::zfShl_s(triton::arch::Instruction& inst,
const triton::engines::symbolic::SharedSymbolicExpression& parent,
triton::arch::OperandWrapper& dst,
const triton::ast::SharedAbstractNode& op2,
bool vol) {
auto bvSize = dst.getBitSize();
auto low = vol ? 0 : dst.getAbstractLow();
auto high = vol ? bvSize-1 : dst.getAbstractHigh();
auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_ZF));
/*
* Create the semantic.
* zf if op2 != 0
*/
auto node = this->astCtxt.ite(
this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(0, bvSize)),
this->symbolicEngine->getOperandAst(inst, zf),
this->astCtxt.ite(
this->astCtxt.equal(
this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
this->astCtxt.bv(0, bvSize)
),
this->astCtxt.bv(1, 1),
this->astCtxt.bv(0, 1)
)
);
/* Create the symbolic expression */
auto expr = this->symbolicEngine->createSymbolicFlagExpression(inst, node, this->architecture->getRegister(ID_REG_ZF), "Zero flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_ZF), parent->isTainted);
}
void x86Semantics::aaa_s(triton::arch::Instruction& inst) {
auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AH));
auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AF));
auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AX));
auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
/* Create the semantics */
auto node = this->astCtxt.ite(
// if
this->astCtxt.lor(
this->astCtxt.bvugt(
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize())),
this->astCtxt.bv(9, src1.getBitSize())
),
this->astCtxt.equal(op3, this->astCtxt.bvtrue())
),
// then
this->astCtxt.concat(
this->astCtxt.bvadd(op2, this->astCtxt.bv(1, src2.getBitSize())),
this->astCtxt.bvand(
this->astCtxt.bvadd(op1, this->astCtxt.bv(6, src1.getBitSize())),
this->astCtxt.bv(0xf, src1.getBitSize())
)
),
// else
this->astCtxt.concat(
op2,
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize()))
)
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAA operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Upate symbolic flags */
this->afAaa_s(inst, expr, dsttmp, op1, op3);
this->cfAaa_s(inst, expr, dsttmp, op1, op3);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::aad_s(triton::arch::Instruction& inst) {
auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D5 0A */
auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AH));
auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AX));
auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
/* D5 ib */
if (inst.operands.size() == 1)
src1 = inst.operands[0];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
/* Create the semantics */
auto node = this->astCtxt.zx(
BYTE_SIZE_BIT,
this->astCtxt.bvadd(
op2,
this->astCtxt.bvmul(op3, op1)
)
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAD operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Upate symbolic flags */
this->pf_s(inst, expr, dsttmp);
this->sf_s(inst, expr, dsttmp);
this->zf_s(inst, expr, dsttmp);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::aam_s(triton::arch::Instruction& inst) {
auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D4 0A */
auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AX));
auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
/* D4 ib */
if (inst.operands.size() == 1)
src1 = inst.operands[0];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
/* Create the semantics */
auto node = this->astCtxt.concat(
this->astCtxt.bvudiv(op2, op1),
this->astCtxt.bvurem(op2, op1)
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAM operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Upate symbolic flags */
this->pf_s(inst, expr, dsttmp);
this->sf_s(inst, expr, dsttmp);
this->zf_s(inst, expr, dsttmp);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::aas_s(triton::arch::Instruction& inst) {
auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AH));
auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AF));
auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AX));
auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AL));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
/* Create the semantics */
auto node = this->astCtxt.ite(
// if
this->astCtxt.lor(
this->astCtxt.bvugt(
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize())),
this->astCtxt.bv(9, src1.getBitSize())
),
this->astCtxt.equal(op3, this->astCtxt.bvtrue())
),
// then
this->astCtxt.concat(
this->astCtxt.bvsub(op2, this->astCtxt.bv(1, src2.getBitSize())),
this->astCtxt.bvand(
this->astCtxt.bvsub(op1, this->astCtxt.bv(6, src1.getBitSize())),
this->astCtxt.bv(0xf, src1.getBitSize())
)
),
// else
this->astCtxt.concat(
op2,
this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize()))
)
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAS operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, dst);
/* Upate symbolic flags */
this->afAaa_s(inst, expr, dsttmp, op1, op3);
this->cfAaa_s(inst, expr, dsttmp, op1, op3);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::adc_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
/* Create the semantics */
auto node = this->astCtxt.bvadd(this->astCtxt.bvadd(op1, op2), this->astCtxt.zx(dst.getBitSize()-1, op3));
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADC operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
expr->isTainted = this->taintEngine->taintUnion(dst, cf);
/* Upate symbolic flags */
this->af_s(inst, expr, dst, op1, op2);
this->cfAdd_s(inst, expr, dst, op1, op2);
this->ofAdd_s(inst, expr, dst, op1, op2);
this->pf_s(inst, expr, dst);
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::adcx_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_CF));
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
/* Create the semantics */
auto node = this->astCtxt.bvadd(this->astCtxt.bvadd(op1, op2), this->astCtxt.zx(dst.getBitSize()-1, op3));
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADCX operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
expr->isTainted = this->taintEngine->taintUnion(dst, cf);
/* Upate symbolic flags */
this->cfAdd_s(inst, expr, dst, op1, op2);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::add_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvadd(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate symbolic flags */
this->af_s(inst, expr, dst, op1, op2);
this->cfAdd_s(inst, expr, dst, op1, op2);
this->ofAdd_s(inst, expr, dst, op1, op2);
this->pf_s(inst, expr, dst);
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::and_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate symbolic flags */
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_CF), "Clears carry flag");
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->pf_s(inst, expr, dst);
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::andn_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src1 = inst.operands[1];
auto& src2 = inst.operands[2];
/* Create symbolic operands */
auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
/* Create the semantics */
auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op2), op3);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDN operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_CF), "Clears carry flag");
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::andnpd_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op1), op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPD operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::andnps_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op1), op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPS operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::andpd_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPD operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::andps_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(op1, op2);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPS operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::bextr_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src1 = inst.operands[1];
auto& src2 = inst.operands[2];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
/* Create the semantics */
auto node = this->astCtxt.bvand(
this->astCtxt.bvlshr(
op1,
this->astCtxt.zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt.extract(7, 0, op2))
),
this->astCtxt.bvsub(
this->astCtxt.bvshl(
this->astCtxt.bv(1, src1.getBitSize()),
this->astCtxt.zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt.extract(15, 8, op2))
),
this->astCtxt.bv(1, src1.getBitSize())
)
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BEXTR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
/* Upate symbolic flags */
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_CF), "Clears carry flag");
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::blsi_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(this->astCtxt.bvneg(op1), op1);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSI operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
/* Upate symbolic flags */
this->cfBlsi_s(inst, expr, src, op1);
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::blsmsk_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvxor(
this->astCtxt.bvsub(op1, this->astCtxt.bv(1, src.getBitSize())),
op1
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSMSK operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
/* Upate symbolic flags */
this->cfBlsmsk_s(inst, expr, src, op1);
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->sf_s(inst, expr, dst);
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_ZF), "Clears zero flag");
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::blsr_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
auto node = this->astCtxt.bvand(
this->astCtxt.bvsub(op1, this->astCtxt.bv(1, src.getBitSize())),
op1
);
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
/* Upate symbolic flags */
this->cfBlsr_s(inst, expr, src, op1);
this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_OF), "Clears overflow flag");
this->sf_s(inst, expr, dst);
this->zf_s(inst, expr, dst);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::bsf_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
auto bvSize1 = dst.getBitSize();
auto bvSize2 = src.getBitSize();
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
triton::ast::SharedAbstractNode node = nullptr;
switch (src.getSize()) {
case BYTE_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))
);
break;
case WORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))))))))))
);
break;
case DWORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))))))))))))))))))))))))))
);
break;
case QWORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(32, 32, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(32, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(33, 33, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(33, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(34, 34, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(34, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(35, 35, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(35, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(36, 36, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(36, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(37, 37, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(37, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(38, 38, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(38, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(39, 39, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(39, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(40, 40, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(40, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(41, 41, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(41, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(42, 42, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(42, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(43, 43, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(43, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(44, 44, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(44, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(45, 45, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(45, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(46, 46, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(46, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(47, 47, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(47, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(48, 48, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(48, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(49, 49, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(49, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(50, 50, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(50, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(51, 51, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(51, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(52, 52, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(52, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(53, 53, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(53, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(54, 54, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(54, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(55, 55, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(55, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(56, 56, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(56, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(57, 57, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(57, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(58, 58, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(58, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(59, 59, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(59, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(60, 60, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(60, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(61, 61, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(61, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(62, 62, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(62, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(63, 63, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(63, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
);
break;
default:
throw triton::exceptions::Semantics("x86Semantics::bsf_s(): Invalid operand size.");
}
/* Create symbolic expression */
auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BSF operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
/* Upate symbolic flags */
this->zfBsf_s(inst, expr, src, op2);
/* Upate the symbolic control flow */
this->controlFlow_s(inst);
}
void x86Semantics::bsr_s(triton::arch::Instruction& inst) {
auto& dst = inst.operands[0];
auto& src = inst.operands[1];
auto bvSize1 = dst.getBitSize();
auto bvSize2 = src.getBitSize();
/* Create symbolic operands */
auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
auto op2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create the semantics */
triton::ast::SharedAbstractNode node = nullptr;
switch (src.getSize()) {
case BYTE_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))
);
break;
case WORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))))))))))
);
break;
case DWORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
this->astCtxt.bv(0, bvSize1)
))))))))))))))))))))))))))))))))
);
break;
case QWORD_SIZE:
node = this->astCtxt.ite(
this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
op1,
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(63, 63, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(63, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(62, 62, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(62, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(61, 61, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(61, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(60, 60, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(60, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(59, 59, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(59, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(58, 58, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(58, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(57, 57, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(57, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(56, 56, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(56, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(55, 55, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(55, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(54, 54, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(54, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(53, 53, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(53, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(52, 52, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(52, bvSize1),
this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(51, 51, op2), this->astCtxt<