1 //! \file
2 /*
3 **  Copyright (C) - Triton
4 **
5 **  This program is under the terms of the Apache License 2.0.
6 */
7 
8 #include <utility>
9 #include <triton/aarch64Semantics.hpp>
10 #include <triton/aarch64Specifications.hpp>
11 #include <triton/astContext.hpp>
12 #include <triton/cpuSize.hpp>
13 #include <triton/exceptions.hpp>
14 
15 
16 
17 /*! \page SMT_aarch64_Semantics_Supported_page AArch64 SMT semantics supported
18     \brief [**internal**] List of the supported semantics for the AArch64 architecture.
19 
20 
21 Mnemonic                      | Description
22 ------------------------------|------------
23 ADC                           | Add with Carry
24 ADD (extended register)       | Add (extended register)
25 ADD (immediate)               | Add (immediate)
26 ADD (shifted register)        | Add (shifted register)
27 ADDS (extended register)      | Add (extended register), setting flags
28 ADDS (immediate)              | Add (immediate), setting flags
29 ADDS (shifted register)       | Add (shifted register), setting flags
30 ADR                           | Form PC-relative address
31 ADRP                          | Form PC-relative address to 4KB page
32 AND (immediate)               | Bitwise AND (immediate)
33 AND (shifted register)        | Bitwise AND (shifted register)
34 ANDS (immediate)              | Bitwise AND (immediate), setting flags
35 ANDS (shifted register)       | Bitwise AND (shifted register), setting flags
36 ASR (immediate)               | Arithmetic Shift Right (immediate): an alias of SBFM
37 ASR (register)                | Arithmetic Shift Right (register): an alias of ASRV
38 B                             | Branch
39 BFI                           | Bit Field Insert
40 BIC                           | Bitwise Bit Clear
41 BL                            | Branch with Link
42 BLR                           | Branch with Link to Register
43 BR                            | Branch to Register
44 CBNZ                          | Compare and Branch on Nonzero
45 CBZ                           | Compare and Branch on Zero
46 CCMP (immediate)              | Conditional Compare (immediate)
47 CCMP (register)               | Conditional Compare (register)
48 CINC                          | Conditional Increment: an alias of CSINC
49 CLZ                           | Count Leading Zeros
50 CMN (extended register)       | Compare Negative (extended register): an alias of ADDS (extended register)
51 CMN (immediate)               | Compare Negative (immediate): an alias of ADDS (immediate)
52 CMN (shifted register)        | Compare Negative (shifted register): an alias of ADDS (shifted register)
53 CMP (extended register)       | Compare (extended register): an alias of SUBS (extended register)
54 CMP (immediate)               | Compare (immediate): an alias of SUBS (immediate)
55 CMP (shifted register)        | Compare (shifted register): an alias of SUBS (shifted register)
56 CSEL                          | Conditional Select
57 CSET                          | Conditional Set: an alias of CSINC
58 CSINC                         | Conditional Select Increment
59 CSNEG                         | Conditional Select Negation
60 EON (shifted register)        | Bitwise Exclusive OR NOT (shifted register)
61 EOR (immediate)               | Bitwise Exclusive OR (immediate)
62 EOR (shifted register)        | Bitwise Exclusive OR (shifted register)
63 EXTR                          | EXTR: Extract register
64 LDAR                          | Load-Acquire Register
65 LDARB                         | Load-Acquire Register Byte
66 LDARH                         | Load-Acquire Register Halfword
67 LDAXR                         | Load-Acquire Exclusive Register
68 LDAXRB                        | Load-Acquire Exclusive Register Byte
69 LDAXRH                        | Load-Acquire Exclusive Register Halfword
70 LDP                           | Load Pair of Registers
71 LDR (immediate)               | Load Register (immediate)
72 LDR (literal)                 | Load Register (literal)
73 LDR (register)                | Load Register (register)
74 LDRB (immediate)              | Load Register Byte (immediate)
75 LDRB (register)               | Load Register Byte (register)
76 LDRH (immediate)              | Load Register Halfword (immediate)
77 LDRH (register)               | Load Register Halfword (register)
78 LDRSB (immediate)             | Load Register Signed Byte (immediate)
79 LDRSB (register)              | Load Register Signed Byte (register)
80 LDRSH (immediate)             | Load Register Signed Halfword (immediate)
81 LDRSH (register)              | Load Register Signed Halfword (register)
82 LDRSW (immediate)             | Load Register Signed Word (immediate)
83 LDRSW (literal)               | Load Register Signed Word (literal)
84 LDRSW (register)              | Load Register Signed Word (register)
85 LDUR                          | Load Register (unscaled)
86 LDURB                         | Load Register Byte (unscaled)
87 LDURH                         | Load Register Halfword (unscaled)
88 LDURSB                        | Load Register Signed Byte (unscaled)
89 LDURSH                        | Load Register Signed Halfword (unscaled)
90 LDURSW                        | Load Register Signed Word (unscaled)
91 LDXR                          | Load Exclusive Register
92 LDXRB                         | Load Exclusive Register Byte
93 LDXRH                         | Load Exclusive Register Halfword
94 LSL (immediate)               | Logical Shift Left (immediate): an alias of UBFM
95 LSL (register)                | Logical Shift Left (register): an alias of LSLV
96 LSR (immediate)               | Logical Shift Right (immediate): an alias of UBFM
97 LSR (register)                | Logical Shift Right (register): an alias of LSRV
98 MADD                          | Multiply-Add
99 MNEG                          | Multiply-Negate: an alias of MSUB
100 MOV (bitmask immediate)       | Move (bitmask immediate): an alias of ORR (immediate)
101 MOV (register)                | Move (register): an alias of ORR (shifted register)
102 MOV (to/from SP)              | Move between register and stack pointer: an alias of ADD (immediate)
103 MOVK                          | Move wide with keep
104 MOVN                          | Move wide with NOT
105 MOVZ                          | Move shifted 16-bit immediate to register
106 MSUB                          | Multiply-Subtract
107 MUL                           | Multiply: an alias of MADD
108 MVN                           | Bitwise NOT: an alias of ORN (shifted register)
109 NEG (shifted register)        | Negate (shifted register): an alias of SUB (shifted register)
110 NOP                           | No Operation
111 ORN                           | Bitwise OR NOT (shifted register)
112 ORR (immediate)               | Bitwise OR (immediate)
113 ORR (shifted register)        | Bitwise OR (shifted register)
114 RBIT                          | Reverse Bits
115 RET                           | Return from subroutine
116 REV                           | Reverse Bytes
117 REV16                         | Reverse bytes in 16-bit halfwords
118 REV32                         | Reverse bytes in 32-bit words
119 REV64                         | Reverse Bytes: an alias of REV
120 ROR (immediate)               | Rotate right (immediate): an alias of EXTR
121 ROR (register)                | Rotate Right (register): an alias of RORV
122 RORV                          | Rotate Right Variable
123 SBFX                          | Signed Bitfield Extract: an alias of SBFM
124 SDIV                          | Signed Divide
125 SMADDL                        | Signed Multiply-Add Long
126 SMSUBL                        | Signed Multiply-Subtract Long
127 SMULH                         | Signed Multiply High
128 SMULL                         | Signed Multiply Long: an alias of SMADDL
129 STLR                          | Store-Release Register
130 STLRB                         | Store-Release Register Byte
131 STLRH                         | Store-Release Register Halfword
132 STP                           | Store Pair of Registers
133 STR (immediate)               | Store Register (immediate)
134 STR (register)                | Store Register (register)
135 STRB (immediate)              | Store Register Byte (immediate)
136 STRB (register)               | Store Register Byte (register)
137 STRH (immediate)              | Store Register Halfword (immediate)
138 STRH (register)               | Store Register Halfword (register)
139 STUR                          | Store Register (unscaled)
140 STURB                         | Store Register Byte (unscaled)
141 STURH                         | Store Register Halfword (unscaled)
142 SUB (extended register)       | Subtract (extended register)
143 SUB (immediate)               | Subtract (immediate)
144 SUB (shifted register)        | Subtract (shifted register)
145 SUBS (extended register)      | Subtract (extended register), setting flags
146 SUBS (immediate)              | Subtract (immediate), setting flags
147 SUBS (shifted register)       | Subtract (shifted register), setting flags
148 SVC                           | Supervisor Call
149 SXTB                          | Signed Extend Byte: an alias of SBFM
150 SXTH                          | Sign Extend Halfword: an alias of SBFM
151 SXTW                          | Sign Extend Word: an alias of SBFM
152 TST (immediate)               | Test bits (immediate): an alias of ANDS (immediate)
153 TST (shifted register)        | Test (shifted register): an alias of ANDS (shifted register)
154 UBFIZ                         | Unsigned Bitfield Insert in Zero: an alias of UBFM
155 UBFX                          | Unsigned Bitfield Extract: an alias of UBFM
156 UDIV                          | Unsigned Divide
157 UMADDL                        | Unsigned Multiply-Add Long
158 UMNEGL                        | Unsigned Multiply-Negate Long: an alias of UMSUBL
159 UMSUBL                        | Unsigned Multiply-Subtract Long
160 UMULH                         | Unsigned Multiply High
161 UMULL                         | Unsigned Multiply Long: an alias of UMADDL
162 UXTB                          | Unsigned Extend Byte: an alias of UBFM
163 UXTH                          | Unsigned Extend Halfword: an alias of UBFM
164 
165 */
166 
167 
168 namespace triton {
169   namespace arch {
170     namespace arm {
171       namespace aarch64 {
172 
AArch64Semantics(triton::arch::Architecture * architecture,triton::engines::symbolic::SymbolicEngine * symbolicEngine,triton::engines::taint::TaintEngine * taintEngine,const triton::ast::SharedAstContext & astCtxt)173         AArch64Semantics::AArch64Semantics(triton::arch::Architecture* architecture,
174                                            triton::engines::symbolic::SymbolicEngine* symbolicEngine,
175                                            triton::engines::taint::TaintEngine* taintEngine,
176                                            const triton::ast::SharedAstContext& astCtxt) {
177 
178           this->architecture    = architecture;
179           this->astCtxt         = astCtxt;
180           this->symbolicEngine  = symbolicEngine;
181           this->taintEngine     = taintEngine;
182 
183           if (architecture == nullptr)
184             throw triton::exceptions::Semantics("AArch64Semantics::AArch64Semantics(): The architecture API must be defined.");
185 
186           if (this->symbolicEngine == nullptr)
187             throw triton::exceptions::Semantics("AArch64Semantics::AArch64Semantics(): The symbolic engine API must be defined.");
188 
189           if (this->taintEngine == nullptr)
190             throw triton::exceptions::Semantics("AArch64Semantics::AArch64Semantics(): The taint engines API must be defined.");
191         }
192 
193 
buildSemantics(triton::arch::Instruction & inst)194         bool AArch64Semantics::buildSemantics(triton::arch::Instruction& inst) {
195           switch (inst.getType()) {
196             case ID_INS_ADC:       this->adc_s(inst);           break;
197             case ID_INS_ADD:       this->add_s(inst);           break;
198             case ID_INS_ADR:       this->adr_s(inst);           break;
199             case ID_INS_ADRP:      this->adrp_s(inst);          break;
200             case ID_INS_AND:       this->and_s(inst);           break;
201             case ID_INS_ASR:       this->asr_s(inst);           break;
202             case ID_INS_B:         this->b_s(inst);             break;
203             case ID_INS_BFI:       this->bfi_s(inst);           break;
204             case ID_INS_BIC:       this->bic_s(inst);           break;
205             case ID_INS_BL:        this->bl_s(inst);            break;
206             case ID_INS_BLR:       this->blr_s(inst);           break;
207             case ID_INS_BR:        this->br_s(inst);            break;
208             case ID_INS_CBNZ:      this->cbnz_s(inst);          break;
209             case ID_INS_CBZ:       this->cbz_s(inst);           break;
210             case ID_INS_CCMP:      this->ccmp_s(inst);          break;
211             case ID_INS_CINC:      this->cinc_s(inst);          break;
212             case ID_INS_CLZ:       this->clz_s(inst);           break;
213             case ID_INS_CMN:       this->cmn_s(inst);           break;
214             case ID_INS_CMP:       this->cmp_s(inst);           break;
215             case ID_INS_CSEL:      this->csel_s(inst);          break;
216             case ID_INS_CSET:      this->cset_s(inst);          break;
217             case ID_INS_CSINC:     this->csinc_s(inst);         break;
218             case ID_INS_CSNEG:     this->csneg_s(inst);         break;
219             case ID_INS_EON:       this->eon_s(inst);           break;
220             case ID_INS_EOR:       this->eor_s(inst);           break;
221             case ID_INS_EXTR:      this->extr_s(inst);          break;
222             case ID_INS_LDAR:      this->ldar_s(inst);          break;
223             case ID_INS_LDARB:     this->ldarb_s(inst);         break;
224             case ID_INS_LDARH:     this->ldarh_s(inst);         break;
225             case ID_INS_LDAXR:     this->ldaxr_s(inst);         break;
226             case ID_INS_LDAXRB:    this->ldaxrb_s(inst);        break;
227             case ID_INS_LDAXRH:    this->ldaxrh_s(inst);        break;
228             case ID_INS_LDP:       this->ldp_s(inst);           break;
229             case ID_INS_LDR:       this->ldr_s(inst);           break;
230             case ID_INS_LDRB:      this->ldrb_s(inst);          break;
231             case ID_INS_LDRH:      this->ldrh_s(inst);          break;
232             case ID_INS_LDRSB:     this->ldrsb_s(inst);         break;
233             case ID_INS_LDRSH:     this->ldrsh_s(inst);         break;
234             case ID_INS_LDRSW:     this->ldrsw_s(inst);         break;
235             case ID_INS_LDUR:      this->ldur_s(inst);          break;
236             case ID_INS_LDURB:     this->ldurb_s(inst);         break;
237             case ID_INS_LDURH:     this->ldurh_s(inst);         break;
238             case ID_INS_LDURSB:    this->ldursb_s(inst);        break;
239             case ID_INS_LDURSH:    this->ldursh_s(inst);        break;
240             case ID_INS_LDURSW:    this->ldursw_s(inst);        break;
241             case ID_INS_LDXR:      this->ldxr_s(inst);          break;
242             case ID_INS_LDXRB:     this->ldxrb_s(inst);         break;
243             case ID_INS_LDXRH:     this->ldxrh_s(inst);         break;
244             case ID_INS_LSL:       this->lsl_s(inst);           break;
245             case ID_INS_LSR:       this->lsr_s(inst);           break;
246             case ID_INS_MADD:      this->madd_s(inst);          break;
247             case ID_INS_MNEG:      this->mneg_s(inst);          break;
248             case ID_INS_MOV:       this->mov_s(inst);           break;
249             case ID_INS_MOVK:      this->movk_s(inst);          break;
250             case ID_INS_MOVN:      this->movn_s(inst);          break;
251             case ID_INS_MOVZ:      this->movz_s(inst);          break;
252             case ID_INS_MSUB:      this->msub_s(inst);          break;
253             case ID_INS_MUL:       this->mul_s(inst);           break;
254             case ID_INS_MVN:       this->mvn_s(inst);           break;
255             case ID_INS_NEG:       this->neg_s(inst);           break;
256             case ID_INS_NOP:       this->nop_s(inst);           break;
257             case ID_INS_ORN:       this->orn_s(inst);           break;
258             case ID_INS_ORR:       this->orr_s(inst);           break;
259             case ID_INS_RBIT:      this->rbit_s(inst);          break;
260             case ID_INS_RET:       this->ret_s(inst);           break;
261             case ID_INS_REV16:     this->rev16_s(inst);         break;
262             case ID_INS_REV32:     this->rev32_s(inst);         break;
263             case ID_INS_REV64:     this->rev_s(inst);           break;
264             case ID_INS_REV:       this->rev_s(inst);           break;
265             case ID_INS_ROR:       this->ror_s(inst);           break;
266             case ID_INS_SBFX:      this->sbfx_s(inst);          break;
267             case ID_INS_SDIV:      this->sdiv_s(inst);          break;
268             case ID_INS_SMADDL:    this->smaddl_s(inst);        break;
269             case ID_INS_SMSUBL:    this->smsubl_s(inst);        break;
270             case ID_INS_SMULH:     this->smulh_s(inst);         break;
271             case ID_INS_SMULL:     this->smull_s(inst);         break;
272             case ID_INS_STLR:      this->stlr_s(inst);          break;
273             case ID_INS_STLRB:     this->stlrb_s(inst);         break;
274             case ID_INS_STLRH:     this->stlrh_s(inst);         break;
275             case ID_INS_STP:       this->stp_s(inst);           break;
276             case ID_INS_STR:       this->str_s(inst);           break;
277             case ID_INS_STRB:      this->strb_s(inst);          break;
278             case ID_INS_STRH:      this->strh_s(inst);          break;
279             case ID_INS_STUR:      this->stur_s(inst);          break;
280             case ID_INS_STURB:     this->sturb_s(inst);         break;
281             case ID_INS_STURH:     this->sturh_s(inst);         break;
282             case ID_INS_SUB:       this->sub_s(inst);           break;
283             case ID_INS_SVC:       this->svc_s(inst);           break;
284             case ID_INS_SXTB:      this->sxtb_s(inst);          break;
285             case ID_INS_SXTH:      this->sxth_s(inst);          break;
286             case ID_INS_SXTW:      this->sxtw_s(inst);          break;
287             case ID_INS_TBNZ:      this->tbnz_s(inst);          break;
288             case ID_INS_TBZ:       this->tbz_s(inst);           break;
289             case ID_INS_TST:       this->tst_s(inst);           break;
290             case ID_INS_UBFIZ:     this->ubfiz_s(inst);         break;
291             case ID_INS_UBFX:      this->ubfx_s(inst);          break;
292             case ID_INS_UDIV:      this->udiv_s(inst);          break;
293             case ID_INS_UMADDL:    this->umaddl_s(inst);        break;
294             case ID_INS_UMNEGL:    this->umnegl_s(inst);        break;
295             case ID_INS_UMSUBL:    this->umsubl_s(inst);        break;
296             case ID_INS_UMULH:     this->umulh_s(inst);         break;
297             case ID_INS_UMULL:     this->umull_s(inst);         break;
298             case ID_INS_UXTB:      this->uxtb_s(inst);          break;
299             case ID_INS_UXTH:      this->uxth_s(inst);          break;
300             default:
301               return false;
302           }
303           return true;
304         }
305 
306 
controlFlow_s(triton::arch::Instruction & inst)307         void AArch64Semantics::controlFlow_s(triton::arch::Instruction& inst) {
308           auto pc = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_AARCH64_PC));
309 
310           /* Create the semantics */
311           auto node = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
312 
313           /* Create symbolic expression */
314           auto expr = this->symbolicEngine->createSymbolicRegisterExpression(inst, node, this->architecture->getParentRegister(ID_REG_AARCH64_PC), "Program Counter");
315 
316           /* Spread taint */
317           expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_AARCH64_PC), triton::engines::taint::UNTAINTED);
318         }
319 
320 
getCodeConditionAst(triton::arch::Instruction & inst,triton::ast::SharedAbstractNode & thenNode,triton::ast::SharedAbstractNode & elseNode)321         triton::ast::SharedAbstractNode AArch64Semantics::getCodeConditionAst(triton::arch::Instruction& inst,
322                                                                               triton::ast::SharedAbstractNode& thenNode,
323                                                                               triton::ast::SharedAbstractNode& elseNode) {
324 
325           switch (inst.getCodeCondition()) {
326             // Always. Any flags. This suffix is normally omitted.
327             case triton::arch::arm::ID_CONDITION_AL: {
328               return thenNode;
329             }
330 
331             // Equal. Z set.
332             case triton::arch::arm::ID_CONDITION_EQ: {
333               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
334               auto node = this->astCtxt->ite(
335                           this->astCtxt->equal(z, this->astCtxt->bvtrue()),
336                           thenNode,
337                           elseNode);
338               return node;
339             }
340 
341             // Signed >=. N and V the same.
342             case triton::arch::arm::ID_CONDITION_GE: {
343               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
344               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
345               auto node = this->astCtxt->ite(
346                           this->astCtxt->equal(n, v),
347                           thenNode,
348                           elseNode);
349               return node;
350             }
351 
352             // Signed >. Z clear, N and V the same.
353             case triton::arch::arm::ID_CONDITION_GT: {
354               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
355               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
356               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
357               auto node = this->astCtxt->ite(
358                           this->astCtxt->land(
359                             this->astCtxt->equal(z, this->astCtxt->bvfalse()),
360                             this->astCtxt->equal(n, v)
361                           ),
362                           thenNode,
363                           elseNode);
364               return node;
365             }
366 
367             // Higher (unsigned >). C set and Z clear.
368             case triton::arch::arm::ID_CONDITION_HI: {
369               auto c = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C)));
370               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
371               auto node = this->astCtxt->ite(
372                           this->astCtxt->land(
373                             this->astCtxt->equal(c, this->astCtxt->bvtrue()),
374                             this->astCtxt->equal(z, this->astCtxt->bvfalse())
375                           ),
376                           thenNode,
377                           elseNode);
378               return node;
379             }
380 
381             // Higher or same (unsigned >=). C set.
382             case triton::arch::arm::ID_CONDITION_HS: {
383               auto c = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C)));
384               auto node = this->astCtxt->ite(
385                           this->astCtxt->equal(c, this->astCtxt->bvtrue()),
386                           thenNode,
387                           elseNode);
388               return node;
389             }
390 
391             // Signed <=. Z set or N and V differ.
392             case triton::arch::arm::ID_CONDITION_LE: {
393               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
394               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
395               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
396               auto node = this->astCtxt->ite(
397                           this->astCtxt->lor(
398                             this->astCtxt->equal(z, this->astCtxt->bvtrue()),
399                             this->astCtxt->lnot(this->astCtxt->equal(n, v))
400                           ),
401                           thenNode,
402                           elseNode);
403               return node;
404             }
405 
406             // Lower (unsigned <). C clear.
407             case triton::arch::arm::ID_CONDITION_LO: {
408               auto c = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C)));
409               auto node = this->astCtxt->ite(
410                           this->astCtxt->equal(c, this->astCtxt->bvfalse()),
411                           thenNode,
412                           elseNode);
413               return node;
414             }
415 
416             // Lower or same (unsigned <=). C clear or Z set.
417             case triton::arch::arm::ID_CONDITION_LS: {
418               auto c = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C)));
419               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
420               auto node = this->astCtxt->ite(
421                           this->astCtxt->lor(
422                             this->astCtxt->equal(c, this->astCtxt->bvfalse()),
423                             this->astCtxt->equal(z, this->astCtxt->bvtrue())
424                           ),
425                           thenNode,
426                           elseNode);
427               return node;
428             }
429 
430             // Signed <. N and V differ.
431             case triton::arch::arm::ID_CONDITION_LT: {
432               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
433               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
434               auto node = this->astCtxt->ite(
435                           this->astCtxt->lnot(this->astCtxt->equal(n, v)),
436                           thenNode,
437                           elseNode);
438               return node;
439             }
440 
441             // Negative. N set.
442             case triton::arch::arm::ID_CONDITION_MI: {
443               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
444               auto node = this->astCtxt->ite(
445                           this->astCtxt->equal(n, this->astCtxt->bvtrue()),
446                           thenNode,
447                           elseNode);
448               return node;
449             }
450 
451             // Not equal. Z clear.
452             case triton::arch::arm::ID_CONDITION_NE: {
453               auto z = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z)));
454               auto node = this->astCtxt->ite(
455                           this->astCtxt->equal(z, this->astCtxt->bvfalse()),
456                           thenNode,
457                           elseNode);
458               return node;
459             }
460 
461             // Positive or zero. N clear.
462             case triton::arch::arm::ID_CONDITION_PL: {
463               auto n = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N)));
464               auto node = this->astCtxt->ite(
465                           this->astCtxt->equal(n, this->astCtxt->bvfalse()),
466                           thenNode,
467                           elseNode);
468               return node;
469             }
470 
471             // No overflow. V clear.
472             case triton::arch::arm::ID_CONDITION_VC: {
473               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
474               auto node = this->astCtxt->ite(
475                           this->astCtxt->equal(v, this->astCtxt->bvfalse()),
476                           thenNode,
477                           elseNode);
478               return node;
479             }
480 
481             // Overflow. V set.
482             case triton::arch::arm::ID_CONDITION_VS: {
483               auto v = this->symbolicEngine->getOperandAst(inst, triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V)));
484               auto node = this->astCtxt->ite(
485                           this->astCtxt->equal(v, this->astCtxt->bvtrue()),
486                           thenNode,
487                           elseNode);
488               return node;
489             }
490 
491             default:
492               /* The instruction don't use condition, so just return the 'then' node */
493               return thenNode;
494           }
495         }
496 
497 
getCodeConditionTainteSate(const triton::arch::Instruction & inst)498         bool AArch64Semantics::getCodeConditionTainteSate(const triton::arch::Instruction& inst) {
499           switch (inst.getCodeCondition()) {
500             // Always. Any flags. This suffix is normally omitted.
501             case triton::arch::arm::ID_CONDITION_AL: {
502               return false;
503             }
504 
505             // Equal. Z set.
506             // Not equal. Z clear.
507             case triton::arch::arm::ID_CONDITION_EQ:
508             case triton::arch::arm::ID_CONDITION_NE: {
509               auto z = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z));
510               return this->taintEngine->isTainted(z);
511             }
512 
513             // Signed >=. N and V the same.
514             // Signed <. N and V differ.
515             case triton::arch::arm::ID_CONDITION_GE:
516             case triton::arch::arm::ID_CONDITION_LT: {
517               auto n = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N));
518               auto v = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V));
519               return this->taintEngine->isTainted(n) | this->taintEngine->isTainted(v);
520             }
521 
522             // Signed >. Z clear, N and V the same.
523             // Signed <=. Z set, N and V differ.
524             case triton::arch::arm::ID_CONDITION_GT:
525             case triton::arch::arm::ID_CONDITION_LE: {
526               auto z = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z));
527               auto n = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N));
528               auto v = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V));
529               return this->taintEngine->isTainted(z) | this->taintEngine->isTainted(n) | this->taintEngine->isTainted(v);
530             }
531 
532             // Higher (unsigned >). C set and Z clear.
533             // Lower or same (unsigned <=). C clear or Z set.
534             case triton::arch::arm::ID_CONDITION_HI:
535             case triton::arch::arm::ID_CONDITION_LS: {
536               auto c = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C));
537               auto z = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_Z));
538               return this->taintEngine->isTainted(c) | this->taintEngine->isTainted(z);
539             }
540 
541             // Higher or same (unsigned >=). C set.
542             // Lower (unsigned <). C clear.
543             case triton::arch::arm::ID_CONDITION_HS:
544             case triton::arch::arm::ID_CONDITION_LO: {
545               auto c = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C));
546               return this->taintEngine->isTainted(c);
547             }
548 
549             // Negative. N set.
550             // Positive or zero. N clear.
551             case triton::arch::arm::ID_CONDITION_MI:
552             case triton::arch::arm::ID_CONDITION_PL: {
553               auto n = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_N));
554               return this->taintEngine->isTainted(n);
555             }
556 
557             // No overflow. V clear.
558             // Overflow. V set.
559             case triton::arch::arm::ID_CONDITION_VC:
560             case triton::arch::arm::ID_CONDITION_VS: {
561               auto v = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_V));
562               return this->taintEngine->isTainted(v);
563             }
564 
565             default:
566               return false;
567           }
568         }
569 
570 
clearFlag_s(triton::arch::Instruction & inst,const triton::arch::Register & flag,std::string comment)571         void AArch64Semantics::clearFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
572           /* Create the semantics */
573           auto node = this->astCtxt->bv(0, 1);
574 
575           /* Create symbolic expression */
576           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
577 
578           /* Spread taint */
579           expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
580         }
581 
582 
setFlag_s(triton::arch::Instruction & inst,const triton::arch::Register & flag,std::string comment)583         void AArch64Semantics::setFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
584           /* Create the semantics */
585           auto node = this->astCtxt->bv(1, 1);
586 
587           /* Create symbolic expression */
588           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
589 
590           /* Spread taint */
591           expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
592         }
593 
594 
nf_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst)595         void AArch64Semantics::nf_s(triton::arch::Instruction& inst,
596                                     const triton::engines::symbolic::SharedSymbolicExpression& parent,
597                                     triton::arch::OperandWrapper& dst) {
598 
599           auto nf   = this->architecture->getRegister(ID_REG_AARCH64_N);
600           auto high = dst.getHigh();
601 
602           /*
603            * Create the semantic.
604            * nf = MSB(result)
605            */
606           auto node = this->astCtxt->extract(high, high, this->astCtxt->reference(parent));
607 
608           /* Create the symbolic expression */
609           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, nf, "Negative flag");
610 
611           /* Spread the taint from the parent to the child */
612           expr->isTainted = this->taintEngine->setTaintRegister(nf, parent->isTainted);
613         }
614 
615 
nfCcmp_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & nzcv)616         void AArch64Semantics::nfCcmp_s(triton::arch::Instruction& inst,
617                                         const triton::engines::symbolic::SharedSymbolicExpression& parent,
618                                         triton::arch::OperandWrapper& dst,
619                                         triton::ast::SharedAbstractNode& nzcv) {
620 
621           auto nf   = this->architecture->getRegister(ID_REG_AARCH64_N);
622           auto high = dst.getHigh();
623 
624           /*
625            * Create the semantic.
626            * nf = MSB(result) if cond == true else NF(nzcv)
627            */
628           auto node1 = this->astCtxt->extract(high, high, this->astCtxt->reference(parent));
629           auto node2 = this->astCtxt->extract(3, 3, nzcv);
630           auto node3 = this->getCodeConditionAst(inst, node1, node2);
631 
632           /* Create the symbolic expression */
633           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, nf, "Negative flag");
634 
635           /* Spread the taint from the parent to the child */
636           expr->isTainted = this->taintEngine->setTaintRegister(nf, parent->isTainted);
637         }
638 
639 
zf_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst)640         void AArch64Semantics::zf_s(triton::arch::Instruction& inst,
641                                     const triton::engines::symbolic::SharedSymbolicExpression& parent,
642                                     triton::arch::OperandWrapper& dst) {
643 
644           auto zf     = this->architecture->getRegister(ID_REG_AARCH64_Z);
645           auto bvSize = dst.getBitSize();
646           auto low    = dst.getLow();
647           auto high   = dst.getHigh();
648 
649           /*
650            * Create the semantic.
651            * zf = 0 == result
652            */
653           auto node = this->astCtxt->ite(
654                         this->astCtxt->equal(
655                           this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
656                           this->astCtxt->bv(0, bvSize)
657                         ),
658                         this->astCtxt->bv(1, 1),
659                         this->astCtxt->bv(0, 1)
660                       );
661 
662           /* Create the symbolic expression */
663           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, zf, "Zero flag");
664 
665           /* Spread the taint from the parent to the child */
666           expr->isTainted = this->taintEngine->setTaintRegister(zf, parent->isTainted);
667         }
668 
669 
zfCcmp_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & nzcv)670         void AArch64Semantics::zfCcmp_s(triton::arch::Instruction& inst,
671                                         const triton::engines::symbolic::SharedSymbolicExpression& parent,
672                                         triton::arch::OperandWrapper& dst,
673                                         triton::ast::SharedAbstractNode& nzcv) {
674 
675           auto zf     = this->architecture->getRegister(ID_REG_AARCH64_Z);
676           auto bvSize = dst.getBitSize();
677           auto low    = dst.getLow();
678           auto high   = dst.getHigh();
679 
680           /*
681            * Create the semantic.
682            * zf = 0 == result if cond == true else ZF(nzcv)
683            */
684           auto node1 = this->astCtxt->ite(
685                          this->astCtxt->equal(
686                            this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
687                            this->astCtxt->bv(0, bvSize)
688                          ),
689                          this->astCtxt->bv(1, 1),
690                          this->astCtxt->bv(0, 1)
691                        );
692           auto node2 = this->astCtxt->extract(2, 2, nzcv);
693           auto node3 = this->getCodeConditionAst(inst, node1, node2);
694 
695           /* Create the symbolic expression */
696           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, zf, "Zero flag");
697 
698           /* Spread the taint from the parent to the child */
699           expr->isTainted = this->taintEngine->setTaintRegister(zf, parent->isTainted);
700         }
701 
702 
cfAdd_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2)703         void AArch64Semantics::cfAdd_s(triton::arch::Instruction& inst,
704                                        const triton::engines::symbolic::SharedSymbolicExpression& parent,
705                                        triton::arch::OperandWrapper& dst,
706                                        triton::ast::SharedAbstractNode& op1,
707                                        triton::ast::SharedAbstractNode& op2) {
708 
709           auto cf     = this->architecture->getRegister(ID_REG_AARCH64_C);
710           auto bvSize = dst.getBitSize();
711           auto low    = dst.getLow();
712           auto high   = dst.getHigh();
713 
714           /*
715            * Create the semantic.
716            * cf = MSB((op1 & op2) ^ ((op1 ^ op2 ^ result) & (op1 ^ op2)));
717            */
718           auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
719                         this->astCtxt->bvxor(
720                           this->astCtxt->bvand(op1, op2),
721                           this->astCtxt->bvand(
722                             this->astCtxt->bvxor(
723                               this->astCtxt->bvxor(op1, op2),
724                               this->astCtxt->extract(high, low, this->astCtxt->reference(parent))
725                             ),
726                           this->astCtxt->bvxor(op1, op2))
727                         )
728                       );
729 
730           /* Create the symbolic expression */
731           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf, "Carry flag");
732 
733           /* Spread the taint from the parent to the child */
734           expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
735         }
736 
737 
cfSub_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2)738         void AArch64Semantics::cfSub_s(triton::arch::Instruction& inst,
739                                        const triton::engines::symbolic::SharedSymbolicExpression& parent,
740                                        triton::arch::OperandWrapper& dst,
741                                        triton::ast::SharedAbstractNode& op1,
742                                        triton::ast::SharedAbstractNode& op2) {
743 
744           auto cf     = this->architecture->getRegister(ID_REG_AARCH64_C);
745           auto bvSize = dst.getBitSize();
746           auto low    = dst.getLow();
747           auto high   = dst.getHigh();
748 
749           /*
750            * Create the semantic.
751            * cf = (MSB(((op1 ^ op2 ^ result) ^ ((op1 ^ result) & (op1 ^ op2))))) ^ 1
752            */
753           auto node = this->astCtxt->bvxor(
754                         this->astCtxt->extract(bvSize-1, bvSize-1,
755                           this->astCtxt->bvxor(
756                             this->astCtxt->bvxor(op1, this->astCtxt->bvxor(op2, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))),
757                             this->astCtxt->bvand(
758                               this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent))),
759                               this->astCtxt->bvxor(op1, op2)
760                             )
761                           )
762                         ),
763                         this->astCtxt->bvtrue()
764                       );
765 
766           /* Create the symbolic expression */
767           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf, "Carry flag");
768 
769           /* Spread the taint from the parent to the child */
770           expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
771         }
772 
773 
cfCcmp_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2,triton::ast::SharedAbstractNode & nzcv)774         void AArch64Semantics::cfCcmp_s(triton::arch::Instruction& inst,
775                                         const triton::engines::symbolic::SharedSymbolicExpression& parent,
776                                         triton::arch::OperandWrapper& dst,
777                                         triton::ast::SharedAbstractNode& op1,
778                                         triton::ast::SharedAbstractNode& op2,
779                                         triton::ast::SharedAbstractNode& nzcv) {
780 
781           auto cf     = this->architecture->getRegister(ID_REG_AARCH64_C);
782           auto bvSize = dst.getBitSize();
783           auto low    = dst.getLow();
784           auto high   = dst.getHigh();
785 
786           /*
787            * Create the semantic.
788            * if cond == true:
789            *   cf = (MSB(((op1 ^ op2 ^ result) ^ ((op1 ^ result) & (op1 ^ op2))))) ^ 1
790            * else
791            *   cf = CF(nzcv)
792            */
793           auto node1 = this->astCtxt->bvxor(
794                          this->astCtxt->extract(bvSize-1, bvSize-1,
795                            this->astCtxt->bvxor(
796                              this->astCtxt->bvxor(op1, this->astCtxt->bvxor(op2, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))),
797                              this->astCtxt->bvand(
798                                this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent))),
799                                this->astCtxt->bvxor(op1, op2)
800                              )
801                            )
802                          ),
803                          this->astCtxt->bvtrue()
804                        );
805           auto node2 = this->astCtxt->extract(1, 1, nzcv);
806           auto node3 = this->getCodeConditionAst(inst, node1, node2);
807 
808           /* Create the symbolic expression */
809           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, cf, "Carry flag");
810 
811           /* Spread the taint from the parent to the child */
812           expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
813         }
814 
815 
vfAdd_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2)816         void AArch64Semantics::vfAdd_s(triton::arch::Instruction& inst,
817                                        const triton::engines::symbolic::SharedSymbolicExpression& parent,
818                                        triton::arch::OperandWrapper& dst,
819                                        triton::ast::SharedAbstractNode& op1,
820                                        triton::ast::SharedAbstractNode& op2) {
821 
822           auto vf     = this->architecture->getRegister(ID_REG_AARCH64_V);
823           auto bvSize = dst.getBitSize();
824           auto low    = dst.getLow();
825           auto high   = dst.getHigh();
826 
827           /*
828            * Create the semantic.
829            * vf = MSB((op1 ^ ~op2) & (op1 ^ result))
830            */
831           auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
832                         this->astCtxt->bvand(
833                           this->astCtxt->bvxor(op1, this->astCtxt->bvnot(op2)),
834                           this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))
835                         )
836                       );
837 
838           /* Create the symbolic expression */
839           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, vf, "Overflow flag");
840 
841           /* Spread the taint from the parent to the child */
842           expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
843         }
844 
845 
vfSub_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2)846         void AArch64Semantics::vfSub_s(triton::arch::Instruction& inst,
847                                        const triton::engines::symbolic::SharedSymbolicExpression& parent,
848                                        triton::arch::OperandWrapper& dst,
849                                        triton::ast::SharedAbstractNode& op1,
850                                        triton::ast::SharedAbstractNode& op2) {
851 
852           auto vf     = this->architecture->getRegister(ID_REG_AARCH64_V);
853           auto bvSize = dst.getBitSize();
854           auto low    = dst.getLow();
855           auto high   = dst.getHigh();
856 
857           /*
858            * Create the semantic.
859            * vf = MSB((op1 ^ op2) & (op1 ^ result))
860            */
861           auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
862                         this->astCtxt->bvand(
863                           this->astCtxt->bvxor(op1, op2),
864                           this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))
865                         )
866                       );
867 
868           /* Create the symbolic expression */
869           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, vf, "Overflow flag");
870 
871           /* Spread the taint from the parent to the child */
872           expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
873         }
874 
875 
vfCcmp_s(triton::arch::Instruction & inst,const triton::engines::symbolic::SharedSymbolicExpression & parent,triton::arch::OperandWrapper & dst,triton::ast::SharedAbstractNode & op1,triton::ast::SharedAbstractNode & op2,triton::ast::SharedAbstractNode & nzcv)876         void AArch64Semantics::vfCcmp_s(triton::arch::Instruction& inst,
877                                         const triton::engines::symbolic::SharedSymbolicExpression& parent,
878                                         triton::arch::OperandWrapper& dst,
879                                         triton::ast::SharedAbstractNode& op1,
880                                         triton::ast::SharedAbstractNode& op2,
881                                         triton::ast::SharedAbstractNode& nzcv) {
882 
883           auto vf     = this->architecture->getRegister(ID_REG_AARCH64_V);
884           auto bvSize = dst.getBitSize();
885           auto low    = dst.getLow();
886           auto high   = dst.getHigh();
887 
888           /*
889            * Create the semantic.
890            * if cond == true:
891            *   vf = MSB((op1 ^ op2) & (op1 ^ result))
892            * else:
893            *   vf = VF(nzcv)
894            */
895           auto node1 = this->astCtxt->extract(bvSize-1, bvSize-1,
896                          this->astCtxt->bvand(
897                            this->astCtxt->bvxor(op1, op2),
898                            this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))
899                          )
900                        );
901           auto node2 = this->astCtxt->extract(0, 0, nzcv);
902           auto node3 = this->getCodeConditionAst(inst, node1, node2);
903 
904           /* Create the symbolic expression */
905           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, vf, "Overflow flag");
906 
907           /* Spread the taint from the parent to the child */
908           expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
909         }
910 
911 
adc_s(triton::arch::Instruction & inst)912         void AArch64Semantics::adc_s(triton::arch::Instruction& inst) {
913           auto& dst  = inst.operands[0];
914           auto& src1 = inst.operands[1];
915           auto& src2 = inst.operands[2];
916           auto  cf   = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_C));
917 
918           /* Create symbolic operands */
919           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
920           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
921           auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
922 
923           /* Create the semantics */
924           auto node = this->astCtxt->bvadd(this->astCtxt->bvadd(op1, op2), this->astCtxt->zx(dst.getBitSize()-1, op3));
925 
926           /* Create symbolic expression */
927           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADC operation");
928 
929           /* Spread taint */
930           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(cf));
931 
932           /* Update the symbolic control flow */
933           this->controlFlow_s(inst);
934         }
935 
936 
add_s(triton::arch::Instruction & inst)937         void AArch64Semantics::add_s(triton::arch::Instruction& inst) {
938           auto& dst  = inst.operands[0];
939           auto& src1 = inst.operands[1];
940           auto& src2 = inst.operands[2];
941 
942           /* Create symbolic operands */
943           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
944           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
945 
946           /* Create the semantics */
947           auto node = this->astCtxt->bvadd(op1, op2);
948 
949           /* Create symbolic expression */
950           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD(S) operation");
951 
952           /* Spread taint */
953           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
954 
955           /* Update symbolic flags */
956           if (inst.isUpdateFlag() == true) {
957             this->cfAdd_s(inst, expr, dst, op1, op2);
958             this->nf_s(inst, expr, dst);
959             this->vfAdd_s(inst, expr, dst, op1, op2);
960             this->zf_s(inst, expr, dst);
961           }
962 
963           /* Update the symbolic control flow */
964           this->controlFlow_s(inst);
965         }
966 
967 
adr_s(triton::arch::Instruction & inst)968         void AArch64Semantics::adr_s(triton::arch::Instruction& inst) {
969           auto& dst = inst.operands[0];
970           auto& src = inst.operands[1];
971           auto  pc  = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_AARCH64_PC));
972 
973           /*
974            * Note: Capstone already encodes the result into the source operand. We don't have
975            * to compute the add operation but do we lose the symbolic?
976            */
977           /* Create symbolic semantics */
978           auto node = this->symbolicEngine->getOperandAst(inst, src);
979 
980           /* Create symbolic expression */
981           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADR operation");
982 
983           /* Spread taint */
984           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src) | this->taintEngine->isTainted(pc));
985 
986           /* Update the symbolic control flow */
987           this->controlFlow_s(inst);
988         }
989 
990 
adrp_s(triton::arch::Instruction & inst)991         void AArch64Semantics::adrp_s(triton::arch::Instruction& inst) {
992           auto& dst = inst.operands[0];
993           auto& src = inst.operands[1];
994           auto  pc  = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_AARCH64_PC));
995 
996           /*
997            * Note: Capstone already encodes the result into the source operand. We don't have
998            * to compute the add operation but do we lose the symbolic?
999            */
1000           /* Create symbolic semantics */
1001           auto node = this->symbolicEngine->getOperandAst(inst, src);
1002 
1003           /* Create symbolic expression */
1004           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADRP operation");
1005 
1006           /* Spread taint */
1007           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src) | this->taintEngine->isTainted(pc));
1008 
1009           /* Update the symbolic control flow */
1010           this->controlFlow_s(inst);
1011         }
1012 
1013 
and_s(triton::arch::Instruction & inst)1014         void AArch64Semantics::and_s(triton::arch::Instruction& inst) {
1015           auto& dst  = inst.operands[0];
1016           auto& src1 = inst.operands[1];
1017           auto& src2 = inst.operands[2];
1018 
1019           /* Create symbolic operands */
1020           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1021           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1022 
1023           /* Create the semantics */
1024           auto node = this->astCtxt->bvand(op1, op2);
1025 
1026           /* Create symbolic expression */
1027           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND(S) operation");
1028 
1029           /* Spread taint */
1030           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1031 
1032           /* Update symbolic flags */
1033           if (inst.isUpdateFlag() == true) {
1034             this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_AARCH64_C), "Clears carry flag");
1035             this->nf_s(inst, expr, dst);
1036             this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_AARCH64_V), "Clears overflow flag");
1037             this->zf_s(inst, expr, dst);
1038           }
1039 
1040           /* Update the symbolic control flow */
1041           this->controlFlow_s(inst);
1042         }
1043 
1044 
asr_s(triton::arch::Instruction & inst)1045         void AArch64Semantics::asr_s(triton::arch::Instruction& inst) {
1046           auto& dst  = inst.operands[0];
1047           auto& src1 = inst.operands[1];
1048           auto& src2 = inst.operands[2];
1049 
1050           /* Create symbolic operands */
1051           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1052           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1053 
1054           /* Create the semantics */
1055           auto node = this->astCtxt->bvashr(op1, op2);
1056 
1057           /* Create symbolic expression */
1058           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ASR operation");
1059 
1060           /* Spread taint */
1061           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1062 
1063           /* Update the symbolic control flow */
1064           this->controlFlow_s(inst);
1065         }
1066 
1067 
b_s(triton::arch::Instruction & inst)1068         void AArch64Semantics::b_s(triton::arch::Instruction& inst) {
1069           auto  dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1070           auto& src = inst.operands[0];
1071 
1072           /* Create symbolic operands */
1073           auto op1 = this->symbolicEngine->getOperandAst(inst, src);
1074           auto op2 = this->astCtxt->bv(inst.getNextAddress(), dst.getBitSize());
1075 
1076           /* Create the semantics */
1077           auto node = this->getCodeConditionAst(inst, op1, op2);
1078 
1079           /* Create symbolic expression */
1080           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "B operation - Program Counter");
1081 
1082           /* Spread taint */
1083           expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
1084 
1085           /* Set condition flag */
1086           if (node->getType() == triton::ast::ITE_NODE) {
1087             if (!(node->getChildren()[0]->evaluate().is_zero())) {
1088               inst.setConditionTaken(true);
1089             }
1090           }
1091 
1092           /* Create the path constraint */
1093           this->symbolicEngine->pushPathConstraint(inst, expr);
1094         }
1095 
1096 
bfi_s(triton::arch::Instruction & inst)1097         void AArch64Semantics::bfi_s(triton::arch::Instruction& inst) {
1098           auto& dst   = inst.operands[0]; // Reg
1099           auto& src1  = inst.operands[1]; // Reg
1100           auto& src2  = inst.operands[2]; // Imm (Lsb)
1101           auto& src3  = inst.operands[3]; // Imm (Width)
1102 
1103           auto  lsb   = src2.getImmediate().getValue();
1104           auto  width = src3.getImmediate().getValue();
1105 
1106           if (lsb + width > dst.getBitSize())
1107             throw triton::exceptions::Semantics("AArch64Semantics::bfi_s(): Invalid lsb and width.");
1108 
1109           /* Create symbolic operands */
1110           auto op    = this->symbolicEngine->getOperandAst(inst, src1);
1111           auto opDst = this->symbolicEngine->getOperandAst(inst, dst);
1112 
1113           /* Create the semantics */
1114           std::vector<triton::ast::SharedAbstractNode> chunks;
1115           chunks.reserve(3);
1116 
1117           if (lsb + width < dst.getBitSize()) {
1118             chunks.push_back(this->astCtxt->extract(dst.getBitSize() - 1, lsb + width, /* src */ opDst));
1119           }
1120           chunks.push_back(this->astCtxt->extract(width - 1, 0, /* src */ op));
1121           chunks.push_back(this->astCtxt->extract(lsb - 1, 0, /* dst */ opDst));
1122 
1123           auto node = this->astCtxt->concat(chunks);
1124 
1125           /* Create symbolic expression */
1126           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BFI operation");
1127 
1128           /* Spread taint */
1129           expr->isTainted = this->taintEngine->taintUnion(dst, src1);
1130 
1131           /* Update the symbolic control flow */
1132           this->controlFlow_s(inst);
1133         }
1134 
1135 
bic_s(triton::arch::Instruction & inst)1136         void AArch64Semantics::bic_s(triton::arch::Instruction& inst) {
1137           auto& dst  = inst.operands[0]; // Reg
1138           auto& src1 = inst.operands[1]; // Reg
1139           auto& src2 = inst.operands[2]; // Reg + [Shift]
1140 
1141           /* Create symbolic operands */
1142           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1143           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1144 
1145           /* Create the semantics */
1146           auto node = this->astCtxt->bvand(op1, this->astCtxt->bvnot(op2));
1147 
1148           /* Create symbolic expression */
1149           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BIC operation");
1150 
1151           /* Spread taint */
1152           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1153 
1154           /* Update the symbolic control flow */
1155           this->controlFlow_s(inst);
1156         }
1157 
1158 
bl_s(triton::arch::Instruction & inst)1159         void AArch64Semantics::bl_s(triton::arch::Instruction& inst) {
1160           auto  dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_X30));
1161           auto  dst2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1162           auto& src  = inst.operands[0];
1163 
1164           /* Create the semantics */
1165           auto node1 = this->astCtxt->bv(inst.getNextAddress(), dst1.getBitSize());
1166           auto node2 = this->symbolicEngine->getOperandAst(inst, src);
1167 
1168           /* Create symbolic expression */
1169           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "BL operation - Link Register");
1170           auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BL operation - Program Counter");
1171 
1172           /* Spread taint */
1173           expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
1174           expr2->isTainted = this->taintEngine->taintAssignment(dst2, src);
1175 
1176           /* Set condition flag */
1177           inst.setConditionTaken(true);
1178 
1179           /* Create the path constraint */
1180           this->symbolicEngine->pushPathConstraint(inst, expr2);
1181         }
1182 
1183 
blr_s(triton::arch::Instruction & inst)1184         void AArch64Semantics::blr_s(triton::arch::Instruction& inst) {
1185           auto  dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_X30));
1186           auto  dst2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1187           auto& src  = inst.operands[0];
1188 
1189           /* Create the semantics */
1190           auto node1 = this->astCtxt->bv(inst.getNextAddress(), dst1.getBitSize());
1191           auto node2 = this->symbolicEngine->getOperandAst(inst, src);
1192 
1193           /* Create symbolic expression */
1194           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "BLR operation - Link Register");
1195           auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BLR operation - Program Counter");
1196 
1197           /* Spread taint */
1198           expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
1199           expr2->isTainted = this->taintEngine->taintAssignment(dst2, src);
1200 
1201           /* Set condition flag */
1202           inst.setConditionTaken(true);
1203 
1204           /* Create the path constraint */
1205           this->symbolicEngine->pushPathConstraint(inst, expr2);
1206         }
1207 
1208 
br_s(triton::arch::Instruction & inst)1209         void AArch64Semantics::br_s(triton::arch::Instruction& inst) {
1210           auto  dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1211           auto& src = inst.operands[0];
1212 
1213           /* Create the semantics */
1214           auto node = this->symbolicEngine->getOperandAst(inst, src);
1215 
1216           /* Create symbolic expression */
1217           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BR operation - Program Counter");
1218 
1219           /* Spread taint */
1220           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1221 
1222           /* Set condition flag */
1223           inst.setConditionTaken(true);
1224 
1225           /* Create the path constraint */
1226           this->symbolicEngine->pushPathConstraint(inst, expr);
1227         }
1228 
1229 
cbnz_s(triton::arch::Instruction & inst)1230         void AArch64Semantics::cbnz_s(triton::arch::Instruction& inst) {
1231           auto  dst  = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1232           auto& src1 = inst.operands[0];
1233           auto& src2 = inst.operands[1];
1234 
1235           /* Create symbolic operands */
1236           auto op1 = this->astCtxt->zx(dst.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
1237           auto op2 = this->astCtxt->zx(dst.getBitSize() - src2.getBitSize(), this->symbolicEngine->getOperandAst(inst, src2));
1238 
1239           /* Create the semantics */
1240           auto node = this->astCtxt->ite(
1241                         this->astCtxt->lnot(this->astCtxt->equal(op1, this->astCtxt->bv(0, op1->getBitvectorSize()))),
1242                         op2,
1243                         this->astCtxt->bv(inst.getNextAddress(), dst.getBitSize())
1244                       );
1245 
1246           /* Create symbolic expression */
1247           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBNZ operation - Program Counter");
1248 
1249           /* Spread taint */
1250           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1251 
1252           /* Set condition flag */
1253           if (op1->evaluate() != 0)
1254             inst.setConditionTaken(true);
1255 
1256           /* Create the path constraint */
1257           this->symbolicEngine->pushPathConstraint(inst, expr);
1258         }
1259 
1260 
cbz_s(triton::arch::Instruction & inst)1261         void AArch64Semantics::cbz_s(triton::arch::Instruction& inst) {
1262           auto  dst  = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
1263           auto& src1 = inst.operands[0];
1264           auto& src2 = inst.operands[1];
1265 
1266           /* Create symbolic operands */
1267           auto op1 = this->astCtxt->zx(dst.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
1268           auto op2 = this->astCtxt->zx(dst.getBitSize() - src2.getBitSize(), this->symbolicEngine->getOperandAst(inst, src2));
1269 
1270           /* Create the semantics */
1271           auto node = this->astCtxt->ite(
1272                         this->astCtxt->equal(op1, this->astCtxt->bv(0, op1->getBitvectorSize())),
1273                         op2,
1274                         this->astCtxt->bv(inst.getNextAddress(), dst.getBitSize())
1275                       );
1276 
1277           /* Create symbolic expression */
1278           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBZ operation - Program Counter");
1279 
1280           /* Spread taint */
1281           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1282 
1283           /* Set condition flag */
1284           if (op1->evaluate() == 0)
1285             inst.setConditionTaken(true);
1286 
1287           /* Create the path constraint */
1288           this->symbolicEngine->pushPathConstraint(inst, expr);
1289         }
1290 
1291 
ccmp_s(triton::arch::Instruction & inst)1292         void AArch64Semantics::ccmp_s(triton::arch::Instruction& inst) {
1293           auto& src1  = inst.operands[0];
1294           auto& src2  = inst.operands[1];
1295           auto& src3  = inst.operands[2];
1296 
1297           /* Create symbolic operands */
1298           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1299           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1300           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
1301 
1302           /* Create the semantics */
1303           auto node = this->astCtxt->bvsub(op1, op2);
1304 
1305           /* Create symbolic expression */
1306           auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "CCMP temporary operation");
1307 
1308           /* Spread taint */
1309           expr->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2);
1310 
1311           /* Update symbolic flags */
1312           this->cfCcmp_s(inst, expr, src1, op1, op2, op3);
1313           this->nfCcmp_s(inst, expr, src1, op3);
1314           this->vfCcmp_s(inst, expr, src1, op1, op2, op3);
1315           this->zfCcmp_s(inst, expr, src1, op3);
1316 
1317           /* Update the symbolic control flow */
1318           this->controlFlow_s(inst);
1319         }
1320 
1321 
cinc_s(triton::arch::Instruction & inst)1322         void AArch64Semantics::cinc_s(triton::arch::Instruction& inst) {
1323           auto& dst = inst.operands[0];
1324           auto& src = inst.operands[1];
1325 
1326           /* Create symbolic operands */
1327           auto op1 = this->symbolicEngine->getOperandAst(inst, src);
1328           auto op2 = this->astCtxt->bvadd(op1, this->astCtxt->bv(1, src.getBitSize()));
1329 
1330           /* Create the semantics */
1331           auto node = this->getCodeConditionAst(inst, op2, op1);
1332 
1333           /* Create symbolic expression */
1334           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CINC operation");
1335 
1336           /* Spread taint */
1337           expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
1338 
1339           /* Update the symbolic control flow */
1340           this->controlFlow_s(inst);
1341         }
1342 
1343 
clz_s(triton::arch::Instruction & inst)1344         void AArch64Semantics::clz_s(triton::arch::Instruction& inst) {
1345           auto& dst     = inst.operands[0];
1346           auto& src     = inst.operands[1];
1347           auto  bvSize  = dst.getBitSize();
1348 
1349           /* Create symbolic operands */
1350           auto op = this->symbolicEngine->getOperandAst(inst, src);
1351 
1352           /* Create the semantics */
1353           triton::ast::SharedAbstractNode node = nullptr;
1354           switch (src.getSize()) {
1355             case triton::size::dword:
1356               node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize),
1357                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize),
1358                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize),
1359                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize),
1360                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize),
1361                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize),
1362                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize),
1363                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize),
1364                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize),
1365                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize),
1366                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize),
1367                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize),
1368                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize),
1369                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize),
1370                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize),
1371                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize),
1372                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize),
1373                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize),
1374                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize),
1375                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize),
1376                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize),
1377                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize),
1378                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(22, bvSize),
1379                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(23, bvSize),
1380                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(24, bvSize),
1381                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(25, bvSize),
1382                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(26, bvSize),
1383                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(27, bvSize),
1384                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(28, bvSize),
1385                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(29, bvSize),
1386                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(30, bvSize),
1387                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op), this->astCtxt->bvtrue()),   this->astCtxt->bv(31, bvSize),
1388                      this->astCtxt->bv(32, bvSize)
1389                      ))))))))))))))))))))))))))))))));
1390               break;
1391 
1392             case triton::size::qword:
1393               node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(63, 63, op), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize),
1394                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(62, 62, op), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize),
1395                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(61, 61, op), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize),
1396                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(60, 60, op), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize),
1397                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(59, 59, op), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize),
1398                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(58, 58, op), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize),
1399                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(57, 57, op), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize),
1400                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(56, 56, op), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize),
1401                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(55, 55, op), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize),
1402                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(54, 54, op), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize),
1403                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(53, 53, op), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize),
1404                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(52, 52, op), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize),
1405                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(51, 51, op), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize),
1406                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(50, 50, op), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize),
1407                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(49, 49, op), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize),
1408                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(48, 48, op), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize),
1409                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(47, 47, op), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize),
1410                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(46, 46, op), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize),
1411                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(45, 45, op), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize),
1412                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(44, 44, op), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize),
1413                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(43, 43, op), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize),
1414                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(42, 42, op), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize),
1415                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(41, 41, op), this->astCtxt->bvtrue()), this->astCtxt->bv(22, bvSize),
1416                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(40, 40, op), this->astCtxt->bvtrue()), this->astCtxt->bv(23, bvSize),
1417                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(39, 39, op), this->astCtxt->bvtrue()), this->astCtxt->bv(24, bvSize),
1418                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(38, 38, op), this->astCtxt->bvtrue()), this->astCtxt->bv(25, bvSize),
1419                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(37, 37, op), this->astCtxt->bvtrue()), this->astCtxt->bv(26, bvSize),
1420                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(36, 36, op), this->astCtxt->bvtrue()), this->astCtxt->bv(27, bvSize),
1421                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(35, 35, op), this->astCtxt->bvtrue()), this->astCtxt->bv(28, bvSize),
1422                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(34, 34, op), this->astCtxt->bvtrue()), this->astCtxt->bv(29, bvSize),
1423                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(33, 33, op), this->astCtxt->bvtrue()), this->astCtxt->bv(30, bvSize),
1424                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(32, 32, op), this->astCtxt->bvtrue()), this->astCtxt->bv(31, bvSize),
1425                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op), this->astCtxt->bvtrue()), this->astCtxt->bv(32, bvSize),
1426                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op), this->astCtxt->bvtrue()), this->astCtxt->bv(33, bvSize),
1427                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op), this->astCtxt->bvtrue()), this->astCtxt->bv(34, bvSize),
1428                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op), this->astCtxt->bvtrue()), this->astCtxt->bv(35, bvSize),
1429                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op), this->astCtxt->bvtrue()), this->astCtxt->bv(36, bvSize),
1430                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op), this->astCtxt->bvtrue()), this->astCtxt->bv(37, bvSize),
1431                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op), this->astCtxt->bvtrue()), this->astCtxt->bv(38, bvSize),
1432                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op), this->astCtxt->bvtrue()), this->astCtxt->bv(39, bvSize),
1433                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op), this->astCtxt->bvtrue()), this->astCtxt->bv(40, bvSize),
1434                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op), this->astCtxt->bvtrue()), this->astCtxt->bv(41, bvSize),
1435                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op), this->astCtxt->bvtrue()), this->astCtxt->bv(42, bvSize),
1436                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op), this->astCtxt->bvtrue()), this->astCtxt->bv(43, bvSize),
1437                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op), this->astCtxt->bvtrue()), this->astCtxt->bv(44, bvSize),
1438                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op), this->astCtxt->bvtrue()), this->astCtxt->bv(45, bvSize),
1439                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op), this->astCtxt->bvtrue()), this->astCtxt->bv(46, bvSize),
1440                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op), this->astCtxt->bvtrue()), this->astCtxt->bv(47, bvSize),
1441                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op), this->astCtxt->bvtrue()), this->astCtxt->bv(48, bvSize),
1442                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op), this->astCtxt->bvtrue()), this->astCtxt->bv(49, bvSize),
1443                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op), this->astCtxt->bvtrue()), this->astCtxt->bv(50, bvSize),
1444                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op), this->astCtxt->bvtrue()), this->astCtxt->bv(51, bvSize),
1445                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op), this->astCtxt->bvtrue()), this->astCtxt->bv(52, bvSize),
1446                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op), this->astCtxt->bvtrue()), this->astCtxt->bv(53, bvSize),
1447                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(54, bvSize),
1448                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(55, bvSize),
1449                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(56, bvSize),
1450                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(57, bvSize),
1451                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(58, bvSize),
1452                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(59, bvSize),
1453                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(60, bvSize),
1454                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(61, bvSize),
1455                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(62, bvSize),
1456                      this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op),   this->astCtxt->bvtrue()), this->astCtxt->bv(63, bvSize),
1457                      this->astCtxt->bv(64, bvSize)
1458                      ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1459               break;
1460 
1461             default:
1462               throw triton::exceptions::Semantics("AArch64Semantics::clz_s(): Invalid operand size.");
1463           }
1464 
1465           /* Create symbolic expression */
1466           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CLZ operation");
1467 
1468           /* Spread taint */
1469           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1470 
1471           /* Update the symbolic control flow */
1472           this->controlFlow_s(inst);
1473         }
1474 
1475 
cmn_s(triton::arch::Instruction & inst)1476         void AArch64Semantics::cmn_s(triton::arch::Instruction& inst) {
1477           auto& src1 = inst.operands[0];
1478           auto& src2 = inst.operands[1];
1479 
1480           /* Create symbolic operands */
1481           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1482           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1483 
1484           /* Create the semantics */
1485           auto node = this->astCtxt->bvadd(op1, op2);
1486 
1487           /* Create symbolic expression */
1488           auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "CMN operation");
1489 
1490           /* Spread taint */
1491           expr->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2);
1492 
1493           /* Update symbolic flags */
1494           this->cfAdd_s(inst, expr, src1, op1, op2);
1495           this->nf_s(inst, expr, src1);
1496           this->vfAdd_s(inst, expr, src1, op1, op2);
1497           this->zf_s(inst, expr, src1);
1498 
1499           /* Update the symbolic control flow */
1500           this->controlFlow_s(inst);
1501         }
1502 
1503 
cmp_s(triton::arch::Instruction & inst)1504         void AArch64Semantics::cmp_s(triton::arch::Instruction& inst) {
1505           auto& src1 = inst.operands[0];
1506           auto& src2 = inst.operands[1];
1507 
1508           /* Create symbolic operands */
1509           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1510           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1511 
1512           /* Create the semantics */
1513           auto node = this->astCtxt->bvsub(op1, op2);
1514 
1515           /* Create symbolic expression */
1516           auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "CMP operation");
1517 
1518           /* Spread taint */
1519           expr->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2);
1520 
1521           /* Update symbolic flags */
1522           this->cfSub_s(inst, expr, src1, op1, op2);
1523           this->nf_s(inst, expr, src1);
1524           this->vfSub_s(inst, expr, src1, op1, op2);
1525           this->zf_s(inst, expr, src1);
1526 
1527           /* Update the symbolic control flow */
1528           this->controlFlow_s(inst);
1529         }
1530 
1531 
csel_s(triton::arch::Instruction & inst)1532         void AArch64Semantics::csel_s(triton::arch::Instruction& inst) {
1533           auto& dst  = inst.operands[0];
1534           auto& src1 = inst.operands[1];
1535           auto& src2 = inst.operands[2];
1536 
1537           /* Create symbolic operands */
1538           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1539           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1540 
1541           /* Create the semantics */
1542           auto node = this->getCodeConditionAst(inst, op1, op2);
1543 
1544           /* Create symbolic expression */
1545           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSEL operation");
1546 
1547           /* Spread taint */
1548           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1549 
1550           /* Update the symbolic control flow */
1551           this->controlFlow_s(inst);
1552         }
1553 
1554 
cset_s(triton::arch::Instruction & inst)1555         void AArch64Semantics::cset_s(triton::arch::Instruction& inst) {
1556           auto& dst = inst.operands[0];
1557 
1558           /* Create symbolic operands */
1559           auto op1 = this->astCtxt->bv(1, dst.getBitSize());
1560           auto op2 = this->astCtxt->bv(0, dst.getBitSize());
1561 
1562           /* Create the semantics */
1563           auto node = this->getCodeConditionAst(inst, op1, op2);
1564 
1565           /* Create symbolic expression */
1566           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSET operation");
1567 
1568           /* Spread taint */
1569           expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
1570 
1571           /* Update the symbolic control flow */
1572           this->controlFlow_s(inst);
1573         }
1574 
1575 
csinc_s(triton::arch::Instruction & inst)1576         void AArch64Semantics::csinc_s(triton::arch::Instruction& inst) {
1577           auto& dst  = inst.operands[0];
1578           auto& src1 = inst.operands[1];
1579           auto& src2 = inst.operands[2];
1580 
1581           /* Create symbolic operands */
1582           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1583           auto op2 = this->astCtxt->bvadd(
1584                        this->symbolicEngine->getOperandAst(inst, src2),
1585                        this->astCtxt->bv(1, src2.getBitSize())
1586                      );
1587 
1588           /* Create the semantics */
1589           auto node = this->getCodeConditionAst(inst, op1, op2);
1590 
1591           /* Create symbolic expression */
1592           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSINC operation");
1593 
1594           /* Spread taint */
1595           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1596 
1597           /* Update the symbolic control flow */
1598           this->controlFlow_s(inst);
1599         }
1600 
1601 
csneg_s(triton::arch::Instruction & inst)1602         void AArch64Semantics::csneg_s(triton::arch::Instruction& inst) {
1603           auto& dst  = inst.operands[0];
1604           auto& src1 = inst.operands[1];
1605           auto& src2 = inst.operands[2];
1606 
1607           /* Create symbolic operands */
1608           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1609           auto op2 = this->astCtxt->bvneg(this->symbolicEngine->getOperandAst(inst, src2));
1610 
1611           /* Create the semantics */
1612           auto node = this->getCodeConditionAst(inst, op1, op2);
1613 
1614           /* Create symbolic expression */
1615           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSNEG operation");
1616 
1617           /* Spread taint */
1618           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1619 
1620           /* Update the symbolic control flow */
1621           this->controlFlow_s(inst);
1622         }
1623 
1624 
eon_s(triton::arch::Instruction & inst)1625         void AArch64Semantics::eon_s(triton::arch::Instruction& inst) {
1626           auto& dst  = inst.operands[0];
1627           auto& src1 = inst.operands[1];
1628           auto& src2 = inst.operands[2];
1629 
1630           /* Create symbolic operands */
1631           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1632           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1633 
1634           /* Create the semantics */
1635           auto node = this->astCtxt->bvxnor(op1, op2);
1636 
1637           /* Create symbolic expression */
1638           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EON operation");
1639 
1640           /* Spread taint */
1641           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1642 
1643           /* Update the symbolic control flow */
1644           this->controlFlow_s(inst);
1645         }
1646 
1647 
eor_s(triton::arch::Instruction & inst)1648         void AArch64Semantics::eor_s(triton::arch::Instruction& inst) {
1649           auto& dst  = inst.operands[0];
1650           auto& src1 = inst.operands[1];
1651           auto& src2 = inst.operands[2];
1652 
1653           /* Create symbolic operands */
1654           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1655           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1656 
1657           /* Create the semantics */
1658           auto node = this->astCtxt->bvxor(op1, op2);
1659 
1660           /* Create symbolic expression */
1661           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EOR operation");
1662 
1663           /* Spread taint */
1664           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1665 
1666           /* Update the symbolic control flow */
1667           this->controlFlow_s(inst);
1668         }
1669 
1670 
extr_s(triton::arch::Instruction & inst)1671         void AArch64Semantics::extr_s(triton::arch::Instruction& inst) {
1672           auto& dst  = inst.operands[0];
1673           auto& src1 = inst.operands[1];
1674           auto& src2 = inst.operands[2];
1675           auto& src3 = inst.operands[3];
1676           auto  lsb  = src3.getImmediate().getValue();
1677 
1678           /* Create symbolic operands */
1679           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1680           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1681 
1682           /* Create the semantics */
1683           auto node = this->astCtxt->extract(lsb + dst.getBitSize() - 1, lsb, this->astCtxt->concat(op1, op2));
1684 
1685           /* Create symbolic expression */
1686           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EXTR operation");
1687 
1688           /* Spread taint */
1689           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
1690 
1691           /* Update the symbolic control flow */
1692           this->controlFlow_s(inst);
1693         }
1694 
1695 
ldar_s(triton::arch::Instruction & inst)1696         void AArch64Semantics::ldar_s(triton::arch::Instruction& inst) {
1697           triton::arch::OperandWrapper& dst = inst.operands[0];
1698           triton::arch::OperandWrapper& src = inst.operands[1];
1699 
1700           /* Create the semantics of the LOAD */
1701           auto node = this->symbolicEngine->getOperandAst(inst, src);
1702 
1703           /* Create symbolic expression */
1704           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAR operation - LOAD access");
1705 
1706           /* Spread taint */
1707           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1708 
1709           /* Update the symbolic control flow */
1710           this->controlFlow_s(inst);
1711         }
1712 
1713 
ldarb_s(triton::arch::Instruction & inst)1714         void AArch64Semantics::ldarb_s(triton::arch::Instruction& inst) {
1715           triton::arch::OperandWrapper& dst = inst.operands[0];
1716           triton::arch::OperandWrapper& src = inst.operands[1];
1717 
1718           /* Special behavior: Define that the size of the memory access is 8 bits */
1719           src.getMemory().setPair(std::make_pair(7, 0));
1720 
1721           /* Create the semantics of the LOAD */
1722           auto node = this->symbolicEngine->getOperandAst(inst, src);
1723 
1724           /* Create symbolic expression */
1725           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDARB operation - LOAD access");
1726 
1727           /* Spread taint */
1728           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1729 
1730           /* Update the symbolic control flow */
1731           this->controlFlow_s(inst);
1732         }
1733 
1734 
ldarh_s(triton::arch::Instruction & inst)1735         void AArch64Semantics::ldarh_s(triton::arch::Instruction& inst) {
1736           triton::arch::OperandWrapper& dst = inst.operands[0];
1737           triton::arch::OperandWrapper& src = inst.operands[1];
1738 
1739           /* Special behavior: Define that the size of the memory access is 16 bits */
1740           src.getMemory().setPair(std::make_pair(15, 0));
1741 
1742           /* Create the semantics of the LOAD */
1743           auto node = this->symbolicEngine->getOperandAst(inst, src);
1744 
1745           /* Create symbolic expression */
1746           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDARH operation - LOAD access");
1747 
1748           /* Spread taint */
1749           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1750 
1751           /* Update the symbolic control flow */
1752           this->controlFlow_s(inst);
1753         }
1754 
1755 
ldaxr_s(triton::arch::Instruction & inst)1756         void AArch64Semantics::ldaxr_s(triton::arch::Instruction& inst) {
1757           triton::arch::OperandWrapper& dst = inst.operands[0];
1758           triton::arch::OperandWrapper& src = inst.operands[1];
1759 
1760           /* Create the semantics of the LOAD */
1761           auto node = this->symbolicEngine->getOperandAst(inst, src);
1762 
1763           /* Create symbolic expression */
1764           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXR operation - LOAD access");
1765 
1766           /* Spread taint */
1767           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1768 
1769           /* Update the symbolic control flow */
1770           this->controlFlow_s(inst);
1771         }
1772 
1773 
ldaxrb_s(triton::arch::Instruction & inst)1774         void AArch64Semantics::ldaxrb_s(triton::arch::Instruction& inst) {
1775           triton::arch::OperandWrapper& dst = inst.operands[0];
1776           triton::arch::OperandWrapper& src = inst.operands[1];
1777 
1778           /* Special behavior: Define that the size of the memory access is 8 bits */
1779           src.getMemory().setPair(std::make_pair(7, 0));
1780 
1781           /* Create the semantics of the LOAD */
1782           auto node = this->symbolicEngine->getOperandAst(inst, src);
1783 
1784           /* Create symbolic expression */
1785           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXRB operation - LOAD access");
1786 
1787           /* Spread taint */
1788           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1789 
1790           /* Update the symbolic control flow */
1791           this->controlFlow_s(inst);
1792         }
1793 
1794 
ldaxrh_s(triton::arch::Instruction & inst)1795         void AArch64Semantics::ldaxrh_s(triton::arch::Instruction& inst) {
1796           triton::arch::OperandWrapper& dst = inst.operands[0];
1797           triton::arch::OperandWrapper& src = inst.operands[1];
1798 
1799           /* Special behavior: Define that the size of the memory access is 16 bits */
1800           src.getMemory().setPair(std::make_pair(15, 0));
1801 
1802           /* Create the semantics of the LOAD */
1803           auto node = this->symbolicEngine->getOperandAst(inst, src);
1804 
1805           /* Create symbolic expression */
1806           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXRH operation - LOAD access");
1807 
1808           /* Spread taint */
1809           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1810 
1811           /* Update the symbolic control flow */
1812           this->controlFlow_s(inst);
1813         }
1814 
1815 
ldp_s(triton::arch::Instruction & inst)1816         void AArch64Semantics::ldp_s(triton::arch::Instruction& inst) {
1817           triton::arch::OperandWrapper& dst1 = inst.operands[0];
1818           triton::arch::OperandWrapper& dst2 = inst.operands[1];
1819           triton::arch::OperandWrapper& src  = inst.operands[2];
1820 
1821           /* Special behavior: Define that the size of the memory access is dst1.size + dst2.size */
1822           src.getMemory().setPair(std::make_pair((dst1.getBitSize() + dst2.getBitSize()) - 1, 0));
1823 
1824           /* Create symbolic operands */
1825           auto op = this->symbolicEngine->getOperandAst(inst, src);
1826 
1827           /* Create the semantics */
1828           auto node1 = this->astCtxt->extract((dst1.getBitSize() - 1), 0, op);
1829           auto node2 = this->astCtxt->extract((dst1.getBitSize() + dst2.getBitSize()) - 1, dst1.getBitSize(), op);
1830 
1831           /* Create symbolic expression */
1832           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "LDP operation - LOAD access");
1833           auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "LDP operation - LOAD access");
1834 
1835           /* Spread taint */
1836           expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
1837           expr2->isTainted = this->taintEngine->taintAssignment(dst2, src);
1838 
1839           /* Optional behavior. Post computation of the base register */
1840           /* LDP <Xt1>, <Xt2>, [<Xn|SP>], #<imm> */
1841           if (inst.operands.size() == 4) {
1842             triton::arch::Immediate& imm = inst.operands[3].getImmediate();
1843             triton::arch::Register& base = src.getMemory().getBaseRegister();
1844 
1845             /* Create symbolic operands of the post computation */
1846             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
1847             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
1848 
1849             /* Create the semantics of the base register */
1850             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
1851 
1852             /* Create symbolic expression */
1853             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDP operation - Base register computation");
1854 
1855             /* Spread taint */
1856             expr2->isTainted = this->taintEngine->isTainted(base);
1857           }
1858 
1859           /* LDP <Xt1>, <Xt2>, [<Xn|SP>, #<imm>]! */
1860           else if (inst.operands.size() == 3 && inst.isWriteBack() == true) {
1861             triton::arch::Register& base = src.getMemory().getBaseRegister();
1862 
1863             /* Create the semantics of the base register */
1864             auto node3 = src.getMemory().getLeaAst();
1865 
1866             /* Create symbolic expression */
1867             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDP operation - Base register computation");
1868 
1869             /* Spread taint */
1870             expr3->isTainted = this->taintEngine->isTainted(base);
1871           }
1872 
1873           /* Update the symbolic control flow */
1874           this->controlFlow_s(inst);
1875         }
1876 
1877 
ldr_s(triton::arch::Instruction & inst)1878         void AArch64Semantics::ldr_s(triton::arch::Instruction& inst) {
1879           triton::arch::OperandWrapper& dst = inst.operands[0];
1880           triton::arch::OperandWrapper& src = inst.operands[1];
1881 
1882           /* Create the semantics of the LOAD */
1883           auto node1 = this->symbolicEngine->getOperandAst(inst, src);
1884 
1885           /* Create symbolic expression */
1886           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDR operation - LOAD access");
1887 
1888           /* Spread taint */
1889           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
1890 
1891           /* Optional behavior. Post computation of the base register */
1892           /* LDR <Xt>, [<Xn|SP>], #<simm> */
1893           if (inst.operands.size() == 3) {
1894             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
1895             triton::arch::Register& base = src.getMemory().getBaseRegister();
1896 
1897             /* Create symbolic operands of the post computation */
1898             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
1899             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
1900 
1901             /* Create the semantics of the base register */
1902             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
1903 
1904             /* Create symbolic expression */
1905             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDR operation - Base register computation");
1906 
1907             /* Spread taint */
1908             expr2->isTainted = this->taintEngine->isTainted(base);
1909           }
1910 
1911           /* LDR <Xt>, [<Xn|SP>, #<simm>]! */
1912           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
1913             triton::arch::Register& base = src.getMemory().getBaseRegister();
1914 
1915             /* Create the semantics of the base register */
1916             auto node3 = src.getMemory().getLeaAst();
1917 
1918             /* Create symbolic expression */
1919             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDR operation - Base register computation");
1920 
1921             /* Spread taint */
1922             expr3->isTainted = this->taintEngine->isTainted(base);
1923           }
1924 
1925           /* Update the symbolic control flow */
1926           this->controlFlow_s(inst);
1927         }
1928 
1929 
ldrb_s(triton::arch::Instruction & inst)1930         void AArch64Semantics::ldrb_s(triton::arch::Instruction& inst) {
1931           triton::arch::OperandWrapper& dst = inst.operands[0];
1932           triton::arch::OperandWrapper& src = inst.operands[1];
1933 
1934           /* Special behavior: Define that the size of the memory access is 8 bits */
1935           src.getMemory().setPair(std::make_pair(7, 0));
1936 
1937           /* Create the semantics of the LOAD */
1938           auto node1 = this->symbolicEngine->getOperandAst(inst, src);
1939 
1940           /* Create symbolic expression */
1941           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRB operation - LOAD access");
1942 
1943           /* Spread taint */
1944           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
1945 
1946           /* Optional behavior. Post computation of the base register */
1947           /* LDRB <Xt>, [<Xn|SP>], #<simm> */
1948           if (inst.operands.size() == 3) {
1949             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
1950             triton::arch::Register& base = src.getMemory().getBaseRegister();
1951 
1952             /* Create symbolic operands of the post computation */
1953             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
1954             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
1955 
1956             /* Create the semantics of the base register */
1957             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
1958 
1959             /* Create symbolic expression */
1960             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRB operation - Base register computation");
1961 
1962             /* Spread taint */
1963             expr2->isTainted = this->taintEngine->isTainted(base);
1964           }
1965 
1966           /* LDRB <Xt>, [<Xn|SP>, #<simm>]! */
1967           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
1968             triton::arch::Register& base = src.getMemory().getBaseRegister();
1969 
1970             /* Create the semantics of the base register */
1971             auto node3 = src.getMemory().getLeaAst();
1972 
1973             /* Create symbolic expression */
1974             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRB operation - Base register computation");
1975 
1976             /* Spread taint */
1977             expr3->isTainted = this->taintEngine->isTainted(base);
1978           }
1979 
1980           /* Update the symbolic control flow */
1981           this->controlFlow_s(inst);
1982         }
1983 
1984 
ldrh_s(triton::arch::Instruction & inst)1985         void AArch64Semantics::ldrh_s(triton::arch::Instruction& inst) {
1986           triton::arch::OperandWrapper& dst = inst.operands[0];
1987           triton::arch::OperandWrapper& src = inst.operands[1];
1988 
1989           /* Special behavior: Define that the size of the memory access is 16 bits */
1990           src.getMemory().setPair(std::make_pair(15, 0));
1991 
1992           /* Create the semantics of the LOAD */
1993           auto node1 = this->symbolicEngine->getOperandAst(inst, src);
1994 
1995           /* Create symbolic expression */
1996           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRH operation - LOAD access");
1997 
1998           /* Spread taint */
1999           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
2000 
2001           /* Optional behavior. Post computation of the base register */
2002           /* LDRH <Xt>, [<Xn|SP>], #<simm> */
2003           if (inst.operands.size() == 3) {
2004             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
2005             triton::arch::Register& base = src.getMemory().getBaseRegister();
2006 
2007             /* Create symbolic operands of the post computation */
2008             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
2009             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
2010 
2011             /* Create the semantics of the base register */
2012             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
2013 
2014             /* Create symbolic expression */
2015             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRH operation - Base register computation");
2016 
2017             /* Spread taint */
2018             expr2->isTainted = this->taintEngine->isTainted(base);
2019           }
2020 
2021           /* LDRH <Xt>, [<Xn|SP>, #<simm>]! */
2022           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
2023             triton::arch::Register& base = src.getMemory().getBaseRegister();
2024 
2025             /* Create the semantics of the base register */
2026             auto node3 = src.getMemory().getLeaAst();
2027 
2028             /* Create symbolic expression */
2029             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRH operation - Base register computation");
2030 
2031             /* Spread taint */
2032             expr3->isTainted = this->taintEngine->isTainted(base);
2033           }
2034 
2035           /* Update the symbolic control flow */
2036           this->controlFlow_s(inst);
2037         }
2038 
2039 
ldrsb_s(triton::arch::Instruction & inst)2040         void AArch64Semantics::ldrsb_s(triton::arch::Instruction& inst) {
2041           triton::arch::OperandWrapper& dst = inst.operands[0];
2042           triton::arch::OperandWrapper& src = inst.operands[1];
2043 
2044           /* Special behavior: Define that the size of the memory access is 8 bits */
2045           src.getMemory().setPair(std::make_pair(7, 0));
2046 
2047           /* Create symbolic operands */
2048           auto op = this->symbolicEngine->getOperandAst(inst, src);
2049 
2050           /* Create the semantics of the LOAD */
2051           auto node1 = this->astCtxt->sx(dst.getBitSize() - 8, op);
2052 
2053           /* Create symbolic expression */
2054           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSB operation - LOAD access");
2055 
2056           /* Spread taint */
2057           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
2058 
2059           /* Optional behavior. Post computation of the base register */
2060           /* LDRSB <Xt>, [<Xn|SP>], #<simm> */
2061           if (inst.operands.size() == 3) {
2062             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
2063             triton::arch::Register& base = src.getMemory().getBaseRegister();
2064 
2065             /* Create symbolic operands of the post computation */
2066             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
2067             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
2068 
2069             /* Create the semantics of the base register */
2070             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
2071 
2072             /* Create symbolic expression */
2073             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSB operation - Base register computation");
2074 
2075             /* Spread taint */
2076             expr2->isTainted = this->taintEngine->isTainted(base);
2077           }
2078 
2079           /* LDRSB <Xt>, [<Xn|SP>, #<simm>]! */
2080           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
2081             triton::arch::Register& base = src.getMemory().getBaseRegister();
2082 
2083             /* Create the semantics of the base register */
2084             auto node3 = src.getMemory().getLeaAst();
2085 
2086             /* Create symbolic expression */
2087             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSB operation - Base register computation");
2088 
2089             /* Spread taint */
2090             expr3->isTainted = this->taintEngine->isTainted(base);
2091           }
2092 
2093           /* Update the symbolic control flow */
2094           this->controlFlow_s(inst);
2095         }
2096 
2097 
ldrsh_s(triton::arch::Instruction & inst)2098         void AArch64Semantics::ldrsh_s(triton::arch::Instruction& inst) {
2099           triton::arch::OperandWrapper& dst = inst.operands[0];
2100           triton::arch::OperandWrapper& src = inst.operands[1];
2101 
2102           /* Special behavior: Define that the size of the memory access is 16 bits */
2103           src.getMemory().setPair(std::make_pair(15, 0));
2104 
2105           /* Create symbolic operands */
2106           auto op = this->symbolicEngine->getOperandAst(inst, src);
2107 
2108           /* Create the semantics of the LOAD */
2109           auto node1 = this->astCtxt->sx(dst.getBitSize() - 16, op);
2110 
2111           /* Create symbolic expression */
2112           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSH operation - LOAD access");
2113 
2114           /* Spread taint */
2115           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
2116 
2117           /* Optional behavior. Post computation of the base register */
2118           /* LDRSH <Xt>, [<Xn|SP>], #<simm> */
2119           if (inst.operands.size() == 3) {
2120             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
2121             triton::arch::Register& base = src.getMemory().getBaseRegister();
2122 
2123             /* Create symbolic operands of the post computation */
2124             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
2125             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
2126 
2127             /* Create the semantics of the base register */
2128             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
2129 
2130             /* Create symbolic expression */
2131             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSH operation - Base register computation");
2132 
2133             /* Spread taint */
2134             expr2->isTainted = this->taintEngine->isTainted(base);
2135           }
2136 
2137           /* LDRSH <Xt>, [<Xn|SP>, #<simm>]! */
2138           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
2139             triton::arch::Register& base = src.getMemory().getBaseRegister();
2140 
2141             /* Create the semantics of the base register */
2142             auto node3 = src.getMemory().getLeaAst();
2143 
2144             /* Create symbolic expression */
2145             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSH operation - Base register computation");
2146 
2147             /* Spread taint */
2148             expr3->isTainted = this->taintEngine->isTainted(base);
2149           }
2150 
2151           /* Update the symbolic control flow */
2152           this->controlFlow_s(inst);
2153         }
2154 
2155 
ldrsw_s(triton::arch::Instruction & inst)2156         void AArch64Semantics::ldrsw_s(triton::arch::Instruction& inst) {
2157           triton::arch::OperandWrapper& dst = inst.operands[0];
2158           triton::arch::OperandWrapper& src = inst.operands[1];
2159 
2160           /* Special behavior: Define that the size of the memory access is 32 bits */
2161           src.getMemory().setPair(std::make_pair(31, 0));
2162 
2163           /* Create symbolic operands */
2164           auto op = this->symbolicEngine->getOperandAst(inst, src);
2165 
2166           /* Create the semantics of the LOAD */
2167           auto node1 = this->astCtxt->sx(dst.getBitSize() - 32, op);
2168 
2169           /* Create symbolic expression */
2170           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSW operation - LOAD access");
2171 
2172           /* Spread taint */
2173           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
2174 
2175           /* Optional behavior. Post computation of the base register */
2176           /* LDRSW <Xt>, [<Xn|SP>], #<simm> */
2177           if (inst.operands.size() == 3) {
2178             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
2179             triton::arch::Register& base = src.getMemory().getBaseRegister();
2180 
2181             /* Create symbolic operands of the post computation */
2182             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
2183             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
2184 
2185             /* Create the semantics of the base register */
2186             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
2187 
2188             /* Create symbolic expression */
2189             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSW operation - Base register computation");
2190 
2191             /* Spread taint */
2192             expr2->isTainted = this->taintEngine->isTainted(base);
2193           }
2194 
2195           /* LDRSW <Xt>, [<Xn|SP>, #<simm>]! */
2196           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
2197             triton::arch::Register& base = src.getMemory().getBaseRegister();
2198 
2199             /* Create the semantics of the base register */
2200             auto node3 = src.getMemory().getLeaAst();
2201 
2202             /* Create symbolic expression */
2203             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSW operation - Base register computation");
2204 
2205             /* Spread taint */
2206             expr3->isTainted = this->taintEngine->isTainted(base);
2207           }
2208 
2209           /* Update the symbolic control flow */
2210           this->controlFlow_s(inst);
2211         }
2212 
2213 
ldur_s(triton::arch::Instruction & inst)2214         void AArch64Semantics::ldur_s(triton::arch::Instruction& inst) {
2215           triton::arch::OperandWrapper& dst = inst.operands[0];
2216           triton::arch::OperandWrapper& src = inst.operands[1];
2217 
2218           /* Create the semantics of the LOAD */
2219           auto node = this->symbolicEngine->getOperandAst(inst, src);
2220 
2221           /* Create symbolic expression */
2222           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDUR operation");
2223 
2224           /* Spread taint */
2225           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2226 
2227           /* Update the symbolic control flow */
2228           this->controlFlow_s(inst);
2229         }
2230 
2231 
ldurb_s(triton::arch::Instruction & inst)2232         void AArch64Semantics::ldurb_s(triton::arch::Instruction& inst) {
2233           triton::arch::OperandWrapper& dst = inst.operands[0];
2234           triton::arch::OperandWrapper& src = inst.operands[1];
2235 
2236           /* Special behavior: Define that the size of the memory access is 8 bits */
2237           src.getMemory().setPair(std::make_pair(7, 0));
2238 
2239           /* Create symbolic operands */
2240           auto op = this->symbolicEngine->getOperandAst(inst, src);
2241 
2242           /* Create the semantics */
2243           auto node = this->astCtxt->zx(dst.getBitSize() - 8, op);
2244 
2245           /* Create symbolic expression */
2246           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURB operation");
2247 
2248           /* Spread taint */
2249           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2250 
2251           /* Update the symbolic control flow */
2252           this->controlFlow_s(inst);
2253         }
2254 
2255 
ldurh_s(triton::arch::Instruction & inst)2256         void AArch64Semantics::ldurh_s(triton::arch::Instruction& inst) {
2257           triton::arch::OperandWrapper& dst = inst.operands[0];
2258           triton::arch::OperandWrapper& src = inst.operands[1];
2259 
2260           /* Special behavior: Define that the size of the memory access is 16 bits */
2261           src.getMemory().setPair(std::make_pair(15, 0));
2262 
2263           /* Create symbolic operands */
2264           auto op = this->symbolicEngine->getOperandAst(inst, src);
2265 
2266           /* Create the semantics */
2267           auto node = this->astCtxt->zx(dst.getBitSize() - 16, op);
2268 
2269           /* Create symbolic expression */
2270           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURH operation");
2271 
2272           /* Spread taint */
2273           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2274 
2275           /* Update the symbolic control flow */
2276           this->controlFlow_s(inst);
2277         }
2278 
2279 
ldursb_s(triton::arch::Instruction & inst)2280         void AArch64Semantics::ldursb_s(triton::arch::Instruction& inst) {
2281           triton::arch::OperandWrapper& dst = inst.operands[0];
2282           triton::arch::OperandWrapper& src = inst.operands[1];
2283 
2284           /* Special behavior: Define that the size of the memory access is 8 bits */
2285           src.getMemory().setPair(std::make_pair(7, 0));
2286 
2287           /* Create symbolic operands */
2288           auto op = this->symbolicEngine->getOperandAst(inst, src);
2289 
2290           /* Create the semantics */
2291           auto node = this->astCtxt->sx(dst.getBitSize() - 8, op);
2292 
2293           /* Create symbolic expression */
2294           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSB operation");
2295 
2296           /* Spread taint */
2297           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2298 
2299           /* Update the symbolic control flow */
2300           this->controlFlow_s(inst);
2301         }
2302 
2303 
ldursh_s(triton::arch::Instruction & inst)2304         void AArch64Semantics::ldursh_s(triton::arch::Instruction& inst) {
2305           triton::arch::OperandWrapper& dst = inst.operands[0];
2306           triton::arch::OperandWrapper& src = inst.operands[1];
2307 
2308           /* Special behavior: Define that the size of the memory access is 16 bits */
2309           src.getMemory().setPair(std::make_pair(15, 0));
2310 
2311           /* Create symbolic operands */
2312           auto op = this->symbolicEngine->getOperandAst(inst, src);
2313 
2314           /* Create the semantics */
2315           auto node = this->astCtxt->sx(dst.getBitSize() - 16, op);
2316 
2317           /* Create symbolic expression */
2318           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSH operation");
2319 
2320           /* Spread taint */
2321           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2322 
2323           /* Update the symbolic control flow */
2324           this->controlFlow_s(inst);
2325         }
2326 
2327 
ldursw_s(triton::arch::Instruction & inst)2328         void AArch64Semantics::ldursw_s(triton::arch::Instruction& inst) {
2329           triton::arch::OperandWrapper& dst = inst.operands[0];
2330           triton::arch::OperandWrapper& src = inst.operands[1];
2331 
2332           /* Special behavior: Define that the size of the memory access is 32 bits */
2333           src.getMemory().setPair(std::make_pair(31, 0));
2334 
2335           /* Create symbolic operands */
2336           auto op = this->symbolicEngine->getOperandAst(inst, src);
2337 
2338           /* Create the semantics */
2339           auto node = this->astCtxt->sx(dst.getBitSize() - 32, op);
2340 
2341           /* Create symbolic expression */
2342           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSW operation");
2343 
2344           /* Spread taint */
2345           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2346 
2347           /* Update the symbolic control flow */
2348           this->controlFlow_s(inst);
2349         }
2350 
2351 
ldxr_s(triton::arch::Instruction & inst)2352         void AArch64Semantics::ldxr_s(triton::arch::Instruction& inst) {
2353           triton::arch::OperandWrapper& dst = inst.operands[0];
2354           triton::arch::OperandWrapper& src = inst.operands[1];
2355 
2356           /* Create the semantics of the LOAD */
2357           auto node = this->symbolicEngine->getOperandAst(inst, src);
2358 
2359           /* Create symbolic expression */
2360           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXR operation");
2361 
2362           /* Spread taint */
2363           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2364 
2365           /* Update the symbolic control flow */
2366           this->controlFlow_s(inst);
2367         }
2368 
2369 
ldxrb_s(triton::arch::Instruction & inst)2370         void AArch64Semantics::ldxrb_s(triton::arch::Instruction& inst) {
2371           triton::arch::OperandWrapper& dst = inst.operands[0];
2372           triton::arch::OperandWrapper& src = inst.operands[1];
2373 
2374           /* Special behavior: Define that the size of the memory access is 8 bits */
2375           src.getMemory().setPair(std::make_pair(7, 0));
2376 
2377           /* Create symbolic operands */
2378           auto op = this->symbolicEngine->getOperandAst(inst, src);
2379 
2380           /* Create the semantics */
2381           auto node = this->astCtxt->zx(dst.getBitSize() - 8, op);
2382 
2383           /* Create symbolic expression */
2384           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXRB operation");
2385 
2386           /* Spread taint */
2387           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2388 
2389           /* Update the symbolic control flow */
2390           this->controlFlow_s(inst);
2391         }
2392 
2393 
ldxrh_s(triton::arch::Instruction & inst)2394         void AArch64Semantics::ldxrh_s(triton::arch::Instruction& inst) {
2395           triton::arch::OperandWrapper& dst = inst.operands[0];
2396           triton::arch::OperandWrapper& src = inst.operands[1];
2397 
2398           /* Special behavior: Define that the size of the memory access is 16 bits */
2399           src.getMemory().setPair(std::make_pair(15, 0));
2400 
2401           /* Create symbolic operands */
2402           auto op = this->symbolicEngine->getOperandAst(inst, src);
2403 
2404           /* Create the semantics */
2405           auto node = this->astCtxt->zx(dst.getBitSize() - 16, op);
2406 
2407           /* Create symbolic expression */
2408           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXRH operation");
2409 
2410           /* Spread taint */
2411           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2412 
2413           /* Update the symbolic control flow */
2414           this->controlFlow_s(inst);
2415         }
2416 
2417 
lsl_s(triton::arch::Instruction & inst)2418         void AArch64Semantics::lsl_s(triton::arch::Instruction& inst) {
2419           auto& dst  = inst.operands[0];
2420           auto& src1 = inst.operands[1];
2421           auto& src2 = inst.operands[2];
2422           auto  size = src2.getBitSize();
2423 
2424           /* Create symbolic operands */
2425           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2426           auto op2 = this->astCtxt->bvand(
2427                        this->symbolicEngine->getOperandAst(inst, src2),
2428                        this->astCtxt->bv(size - 1,  size)
2429                      );
2430 
2431           /* Create the semantics */
2432           auto node = this->astCtxt->bvshl(op1, op2);
2433 
2434           /* Create symbolic expression */
2435           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LSL operation");
2436 
2437           /* Spread taint */
2438           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2439 
2440           /* Update the symbolic control flow */
2441           this->controlFlow_s(inst);
2442         }
2443 
2444 
lsr_s(triton::arch::Instruction & inst)2445         void AArch64Semantics::lsr_s(triton::arch::Instruction& inst) {
2446           auto& dst  = inst.operands[0];
2447           auto& src1 = inst.operands[1];
2448           auto& src2 = inst.operands[2];
2449           auto  size = src2.getBitSize();
2450 
2451           /* Create symbolic operands */
2452           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2453           auto op2 = this->astCtxt->bvand(
2454                        this->symbolicEngine->getOperandAst(inst, src2),
2455                        this->astCtxt->bv(size - 1,  size)
2456                      );
2457 
2458           /* Create the semantics */
2459           auto node = this->astCtxt->bvlshr(op1, op2);
2460 
2461           /* Create symbolic expression */
2462           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LSR operation");
2463 
2464           /* Spread taint */
2465           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2466 
2467           /* Update the symbolic control flow */
2468           this->controlFlow_s(inst);
2469         }
2470 
2471 
madd_s(triton::arch::Instruction & inst)2472         void AArch64Semantics::madd_s(triton::arch::Instruction& inst) {
2473           auto& dst  = inst.operands[0];
2474           auto& src1 = inst.operands[1];
2475           auto& src2 = inst.operands[2];
2476           auto& src3 = inst.operands[3];
2477 
2478           /* Create symbolic operands */
2479           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2480           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2481           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2482 
2483           /* Create the semantics */
2484           auto node = this->astCtxt->bvadd(op3, this->astCtxt->bvmul(op1, op2));
2485 
2486           /* Create symbolic expression */
2487           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MADD operation");
2488 
2489           /* Spread taint */
2490           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
2491 
2492           /* Update the symbolic control flow */
2493           this->controlFlow_s(inst);
2494         }
2495 
2496 
mneg_s(triton::arch::Instruction & inst)2497         void AArch64Semantics::mneg_s(triton::arch::Instruction& inst) {
2498           auto& dst  = inst.operands[0];
2499           auto& src1 = inst.operands[1];
2500           auto& src2 = inst.operands[2];
2501 
2502           /* Create symbolic operands */
2503           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2504           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2505 
2506           /* Create the semantics */
2507           auto node = this->astCtxt->bvneg(this->astCtxt->bvmul(op1, op2));
2508 
2509           /* Create symbolic expression */
2510           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MNEG operation");
2511 
2512           /* Spread taint */
2513           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2514 
2515           /* Update the symbolic control flow */
2516           this->controlFlow_s(inst);
2517         }
2518 
2519 
mov_s(triton::arch::Instruction & inst)2520         void AArch64Semantics::mov_s(triton::arch::Instruction& inst) {
2521           auto& dst = inst.operands[0];
2522           auto& src = inst.operands[1];
2523 
2524           /* Create the semantics */
2525           auto node = this->symbolicEngine->getOperandAst(inst, src);
2526 
2527           /* Create symbolic expression */
2528           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOV operation");
2529 
2530           /* Spread taint */
2531           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2532 
2533           /* Update the symbolic control flow */
2534           this->controlFlow_s(inst);
2535         }
2536 
2537 
movk_s(triton::arch::Instruction & inst)2538         void AArch64Semantics::movk_s(triton::arch::Instruction& inst) {
2539           auto& dst = inst.operands[0];
2540           auto& src = inst.operands[1];
2541           auto  pos = src.getImmediate().getShiftImmediate(); // 0 by default.
2542 
2543           /* Create symbolic operands */
2544           auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2545           auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2546 
2547           /* Create the semantics */
2548           std::vector<triton::ast::SharedAbstractNode> bits;
2549           bits.reserve(10);
2550 
2551           switch (pos) {
2552             case 0:
2553               // [------------------------------------------------xxxxxxxxxxxxxxxx]
2554               bits.push_back(this->astCtxt->extract(dst.getHigh(), 16, op1));
2555               bits.push_back(this->astCtxt->extract(15, 0, op2));
2556               break;
2557 
2558             case 16:
2559               // [--------------------------------xxxxxxxxxxxxxxxx----------------]
2560               if (dst.getBitSize() == 64) {
2561                 /*
2562                  * The case where the instruction is: MOVK <Xd>, #<imm>{, LSL #<shift>}.
2563                  * Otherwise if the instruction is: MOVK <Wd>, #<imm>{, LSL #<shift>}, just
2564                  * skip this extract.
2565                  */
2566                 bits.push_back(this->astCtxt->extract(dst.getHigh(), 32, op1));
2567               }
2568               bits.push_back(this->astCtxt->extract(31, 16, op2));
2569               bits.push_back(this->astCtxt->extract(15, 0, op1));
2570               break;
2571 
2572             case 32:
2573               // [----------------xxxxxxxxxxxxxxxx--------------------------------]
2574               bits.push_back(this->astCtxt->extract(dst.getHigh(), 48, op1));
2575               bits.push_back(this->astCtxt->extract(47, 32, op2));
2576               bits.push_back(this->astCtxt->extract(31, 0, op1));
2577               break;
2578 
2579             case 48:
2580               // [xxxxxxxxxxxxxxxx------------------------------------------------]
2581               bits.push_back(this->astCtxt->extract(63, 48, op2));
2582               bits.push_back(this->astCtxt->extract(47, 0, op1));
2583               break;
2584 
2585             default:
2586               throw triton::exceptions::Semantics("AArch64Semantics::movk_s(): Invalid pos (hw field) encoding.");
2587           }
2588 
2589           auto node = this->astCtxt->concat(bits);
2590 
2591           /* Create symbolic expression */
2592           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVK operation");
2593 
2594           /* Spread taint */
2595           expr->isTainted = this->taintEngine->taintUnion(dst, src);
2596 
2597           /* Update the symbolic control flow */
2598           this->controlFlow_s(inst);
2599         }
2600 
2601 
movn_s(triton::arch::Instruction & inst)2602         void AArch64Semantics::movn_s(triton::arch::Instruction& inst) {
2603           auto& dst = inst.operands[0];
2604           auto& src = inst.operands[1];
2605 
2606           /* Create symbolic operands */
2607           auto op = this->symbolicEngine->getOperandAst(inst, src);
2608 
2609           /* Create the semantics */
2610           auto node = this->astCtxt->bvnot(op);
2611 
2612           /* Create symbolic expression */
2613           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVN operation");
2614 
2615           /* Spread taint */
2616           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2617 
2618           /* Update the symbolic control flow */
2619           this->controlFlow_s(inst);
2620         }
2621 
2622 
movz_s(triton::arch::Instruction & inst)2623         void AArch64Semantics::movz_s(triton::arch::Instruction& inst) {
2624           auto& dst = inst.operands[0];
2625           auto& src = inst.operands[1];
2626 
2627           /* Create the semantics */
2628           auto node = this->symbolicEngine->getOperandAst(inst, src);
2629 
2630           /* Create symbolic expression */
2631           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVZ operation");
2632 
2633           /* Spread taint */
2634           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2635 
2636           /* Update the symbolic control flow */
2637           this->controlFlow_s(inst);
2638         }
2639 
2640 
msub_s(triton::arch::Instruction & inst)2641         void AArch64Semantics::msub_s(triton::arch::Instruction& inst) {
2642           auto& dst  = inst.operands[0];
2643           auto& src1 = inst.operands[1];
2644           auto& src2 = inst.operands[2];
2645           auto& src3 = inst.operands[3];
2646 
2647           /* Create symbolic operands */
2648           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2649           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2650           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2651 
2652           /* Create the semantics */
2653           auto node = this->astCtxt->bvsub(op3, this->astCtxt->bvmul(op1, op2));
2654 
2655           /* Create symbolic expression */
2656           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MSUB operation");
2657 
2658           /* Spread taint */
2659           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
2660 
2661           /* Update the symbolic control flow */
2662           this->controlFlow_s(inst);
2663         }
2664 
2665 
mul_s(triton::arch::Instruction & inst)2666         void AArch64Semantics::mul_s(triton::arch::Instruction& inst) {
2667           auto& dst  = inst.operands[0];
2668           auto& src1 = inst.operands[1];
2669           auto& src2 = inst.operands[2];
2670 
2671           /* Create symbolic operands */
2672           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2673           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2674 
2675           /* Create the semantics */
2676           auto node = this->astCtxt->bvmul(op1, op2);
2677 
2678           /* Create symbolic expression */
2679           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MUL operation");
2680 
2681           /* Spread taint */
2682           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2683 
2684           /* Update the symbolic control flow */
2685           this->controlFlow_s(inst);
2686         }
2687 
2688 
mvn_s(triton::arch::Instruction & inst)2689         void AArch64Semantics::mvn_s(triton::arch::Instruction& inst) {
2690           auto& dst = inst.operands[0];
2691           auto& src = inst.operands[1];
2692 
2693           /* Create symbolic operands */
2694           auto op = this->symbolicEngine->getOperandAst(inst, src);
2695 
2696           /* Create the semantics */
2697           auto node = this->astCtxt->bvnot(op);
2698 
2699           /* Create symbolic expression */
2700           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MVN operation");
2701 
2702           /* Spread taint */
2703           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2704 
2705           /* Update the symbolic control flow */
2706           this->controlFlow_s(inst);
2707         }
2708 
2709 
neg_s(triton::arch::Instruction & inst)2710         void AArch64Semantics::neg_s(triton::arch::Instruction& inst) {
2711           auto& dst = inst.operands[0];
2712           auto& src = inst.operands[1];
2713 
2714           /* Create symbolic operands */
2715           auto op = this->symbolicEngine->getOperandAst(inst, src);
2716 
2717           /* Create the semantics */
2718           auto node = this->astCtxt->bvneg(op);
2719 
2720           /* Create symbolic expression */
2721           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MEG operation");
2722 
2723           /* Spread taint */
2724           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2725 
2726           /* Update the symbolic control flow */
2727           this->controlFlow_s(inst);
2728         }
2729 
2730 
nop_s(triton::arch::Instruction & inst)2731         void AArch64Semantics::nop_s(triton::arch::Instruction& inst) {
2732           /* Update the symbolic control flow */
2733           this->controlFlow_s(inst);
2734         }
2735 
2736 
orn_s(triton::arch::Instruction & inst)2737         void AArch64Semantics::orn_s(triton::arch::Instruction& inst) {
2738           auto& dst  = inst.operands[0];
2739           auto& src1 = inst.operands[1];
2740           auto& src2 = inst.operands[2];
2741 
2742           /* Create symbolic operands */
2743           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2744           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2745 
2746           /* Create the semantics */
2747           auto node = this->astCtxt->bvor(op1, this->astCtxt->bvnot(op2));
2748 
2749           /* Create symbolic expression */
2750           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ORN operation");
2751 
2752           /* Spread taint */
2753           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2754 
2755           /* Update the symbolic control flow */
2756           this->controlFlow_s(inst);
2757         }
2758 
2759 
orr_s(triton::arch::Instruction & inst)2760         void AArch64Semantics::orr_s(triton::arch::Instruction& inst) {
2761           auto& dst  = inst.operands[0];
2762           auto& src1 = inst.operands[1];
2763           auto& src2 = inst.operands[2];
2764 
2765           /* Create symbolic operands */
2766           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2767           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2768 
2769           /* Create the semantics */
2770           auto node = this->astCtxt->bvor(op1, op2);
2771 
2772           /* Create symbolic expression */
2773           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ORR operation");
2774 
2775           /* Spread taint */
2776           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2777 
2778           /* Update the symbolic control flow */
2779           this->controlFlow_s(inst);
2780         }
2781 
2782 
rbit_s(triton::arch::Instruction & inst)2783         void AArch64Semantics::rbit_s(triton::arch::Instruction& inst) {
2784           auto& dst = inst.operands[0];
2785           auto& src = inst.operands[1];
2786 
2787           /* Create symbolic operands */
2788           auto op = this->symbolicEngine->getOperandAst(inst, src);
2789 
2790           /* Create the semantics */
2791           std::vector<triton::ast::SharedAbstractNode> bits;
2792           bits.reserve(src.getBitSize());
2793 
2794           for (triton::uint32 index = 0; index < src.getBitSize(); index++) {
2795             bits.push_back(this->astCtxt->extract(index, index, op));
2796           }
2797 
2798           auto node = this->astCtxt->concat(bits);
2799 
2800           /* Create symbolic expression */
2801           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "RBIT operation");
2802 
2803           /* Spread taint */
2804           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2805 
2806           /* Update the symbolic control flow */
2807           this->controlFlow_s(inst);
2808         }
2809 
2810 
ret_s(triton::arch::Instruction & inst)2811         void AArch64Semantics::ret_s(triton::arch::Instruction& inst) {
2812           auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
2813           auto src = ((inst.operands.size() == 1) ? inst.operands[0] : triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_X30)));
2814 
2815           /* Create the semantics */
2816           auto node = this->symbolicEngine->getOperandAst(inst, src);
2817 
2818           /* Create symbolic expression */
2819           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "RET operation - Program Counter");
2820 
2821           /* Spread taint */
2822           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2823         }
2824 
2825 
rev_s(triton::arch::Instruction & inst)2826         void AArch64Semantics::rev_s(triton::arch::Instruction& inst) {
2827           auto& dst = inst.operands[0];
2828           auto& src = inst.operands[1];
2829 
2830           /* Create symbolic operands */
2831           auto op = this->symbolicEngine->getOperandAst(inst, src);
2832 
2833           /* Create the semantics */
2834           std::list<triton::ast::SharedAbstractNode> bits;
2835 
2836           switch(src.getSize()) {
2837             case triton::size::qword:
2838                 bits.push_front(this->astCtxt->extract(63, 56, op));
2839                 bits.push_front(this->astCtxt->extract(55, 48, op));
2840                 bits.push_front(this->astCtxt->extract(47, 40, op));
2841                 bits.push_front(this->astCtxt->extract(39, 32, op));
2842             case triton::size::dword:
2843                 bits.push_front(this->astCtxt->extract(31, 24, op));
2844                 bits.push_front(this->astCtxt->extract(23, 16, op));
2845                 bits.push_front(this->astCtxt->extract(15, 8,  op));
2846                 bits.push_front(this->astCtxt->extract(7,  0,  op));
2847               break;
2848 
2849             default:
2850               throw triton::exceptions::Semantics("AArch64Semantics::rev_s(): Invalid operand size.");
2851           }
2852 
2853           auto node = this->astCtxt->concat(bits);
2854 
2855           /* Create symbolic expression */
2856           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV operation");
2857 
2858           /* Spread taint */
2859           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2860 
2861           /* Update the symbolic control flow */
2862           this->controlFlow_s(inst);
2863         }
2864 
2865 
rev16_s(triton::arch::Instruction & inst)2866         void AArch64Semantics::rev16_s(triton::arch::Instruction& inst) {
2867           auto& dst = inst.operands[0];
2868           auto& src = inst.operands[1];
2869 
2870           /* Create symbolic operands */
2871           auto op = this->symbolicEngine->getOperandAst(inst, src);
2872 
2873           /* Create the semantics */
2874           std::vector<triton::ast::SharedAbstractNode> bits;
2875           bits.reserve(8);
2876 
2877           switch(src.getSize()) {
2878             case triton::size::qword:
2879                 bits.push_back(this->astCtxt->extract(55, 48, op));
2880                 bits.push_back(this->astCtxt->extract(63, 56, op));
2881                 bits.push_back(this->astCtxt->extract(39, 32, op));
2882                 bits.push_back(this->astCtxt->extract(47, 40, op));
2883             case triton::size::dword:
2884                 bits.push_back(this->astCtxt->extract(23, 16, op));
2885                 bits.push_back(this->astCtxt->extract(31, 24, op));
2886                 bits.push_back(this->astCtxt->extract(7,  0,  op));
2887                 bits.push_back(this->astCtxt->extract(15, 8,  op));
2888               break;
2889 
2890             default:
2891               throw triton::exceptions::Semantics("AArch64Semantics::rev16_s(): Invalid operand size.");
2892           }
2893 
2894           auto node = this->astCtxt->concat(bits);
2895 
2896           /* Create symbolic expression */
2897           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV16 operation");
2898 
2899           /* Spread taint */
2900           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2901 
2902           /* Update the symbolic control flow */
2903           this->controlFlow_s(inst);
2904         }
2905 
2906 
rev32_s(triton::arch::Instruction & inst)2907         void AArch64Semantics::rev32_s(triton::arch::Instruction& inst) {
2908           auto& dst = inst.operands[0];
2909           auto& src = inst.operands[1];
2910 
2911           /* Create symbolic operands */
2912           auto op = this->symbolicEngine->getOperandAst(inst, src);
2913 
2914           /* Create the semantics */
2915           std::vector<triton::ast::SharedAbstractNode> bits;
2916           bits.reserve(8);
2917 
2918           bits.push_back(this->astCtxt->extract(39, 32, op));
2919           bits.push_back(this->astCtxt->extract(47, 40, op));
2920           bits.push_back(this->astCtxt->extract(55, 48, op));
2921           bits.push_back(this->astCtxt->extract(63, 56, op));
2922           bits.push_back(this->astCtxt->extract(7,  0,  op));
2923           bits.push_back(this->astCtxt->extract(15, 8,  op));
2924           bits.push_back(this->astCtxt->extract(23, 16, op));
2925           bits.push_back(this->astCtxt->extract(31, 24, op));
2926 
2927           auto node = this->astCtxt->concat(bits);
2928 
2929           /* Create symbolic expression */
2930           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV32 operation");
2931 
2932           /* Spread taint */
2933           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2934 
2935           /* Update the symbolic control flow */
2936           this->controlFlow_s(inst);
2937         }
2938 
2939 
ror_s(triton::arch::Instruction & inst)2940         void AArch64Semantics::ror_s(triton::arch::Instruction& inst) {
2941           auto& dst  = inst.operands[0];
2942           auto& src1 = inst.operands[1];
2943           auto& src2 = inst.operands[2];
2944 
2945           /* Create symbolic operands */
2946           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2947           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2948 
2949           /* Create the semantics */
2950           auto node = this->astCtxt->bvror(op1, op2);
2951 
2952           /* Create symbolic expression */
2953           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ROR operation");
2954 
2955           /* Spread taint */
2956           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2957 
2958           /* Update the symbolic control flow */
2959           this->controlFlow_s(inst);
2960         }
2961 
2962 
sbfx_s(triton::arch::Instruction & inst)2963         void AArch64Semantics::sbfx_s(triton::arch::Instruction& inst) {
2964           auto& dst   = inst.operands[0];
2965           auto& src1  = inst.operands[1];
2966           auto& src2  = inst.operands[2];
2967           auto& src3  = inst.operands[3];
2968           auto  lsb   = src2.getImmediate().getValue();
2969           auto  width = src3.getImmediate().getValue();
2970 
2971           if (lsb + width > dst.getBitSize())
2972             throw triton::exceptions::Semantics("AArch64Semantics::sbfx_s(): Invalid lsb and width.");
2973 
2974           /* Create symbolic operands */
2975           auto op = this->symbolicEngine->getOperandAst(inst, src1);
2976 
2977           /* Create the semantics */
2978           auto node = this->astCtxt->sx(dst.getBitSize() - width, this->astCtxt->extract(lsb+width-1, lsb, op));
2979 
2980           /* Create symbolic expression */
2981           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SBFX operation");
2982 
2983           /* Spread taint */
2984           expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
2985 
2986           /* Update the symbolic control flow */
2987           this->controlFlow_s(inst);
2988         }
2989 
2990 
sdiv_s(triton::arch::Instruction & inst)2991         void AArch64Semantics::sdiv_s(triton::arch::Instruction& inst) {
2992           auto& dst  = inst.operands[0];
2993           auto& src1 = inst.operands[1];
2994           auto& src2 = inst.operands[2];
2995 
2996           /* Create symbolic operands */
2997           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2998           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2999 
3000           /* Create the semantics */
3001           auto node = this->astCtxt->ite(
3002                         this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
3003                         this->astCtxt->bv(0, dst.getBitSize()),
3004                         this->astCtxt->bvsdiv(op1, op2)
3005                       );
3006 
3007           /* Create symbolic expression */
3008           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SDIV operation");
3009 
3010           /* Spread taint */
3011           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3012 
3013           /* Update the symbolic control flow */
3014           this->controlFlow_s(inst);
3015         }
3016 
3017 
smaddl_s(triton::arch::Instruction & inst)3018         void AArch64Semantics::smaddl_s(triton::arch::Instruction& inst) {
3019           auto& dst  = inst.operands[0];
3020           auto& src1 = inst.operands[1];
3021           auto& src2 = inst.operands[2];
3022           auto& src3 = inst.operands[3];
3023 
3024           /* Create symbolic operands */
3025           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3026           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3027           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
3028 
3029           /* Create the semantics */
3030           auto node = this->astCtxt->bvadd(
3031                         op3,
3032                         this->astCtxt->bvmul(
3033                           this->astCtxt->sx(triton::bitsize::dword, op1),
3034                           this->astCtxt->sx(triton::bitsize::dword, op2)
3035                         )
3036                       );
3037 
3038           /* Create symbolic expression */
3039           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMADDL operation");
3040 
3041           /* Spread taint */
3042           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
3043 
3044           /* Update the symbolic control flow */
3045           this->controlFlow_s(inst);
3046         }
3047 
3048 
smsubl_s(triton::arch::Instruction & inst)3049         void AArch64Semantics::smsubl_s(triton::arch::Instruction& inst) {
3050           auto& dst  = inst.operands[0];
3051           auto& src1 = inst.operands[1];
3052           auto& src2 = inst.operands[2];
3053           auto& src3 = inst.operands[3];
3054 
3055           /* Create symbolic operands */
3056           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3057           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3058           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
3059 
3060           /* Create the semantics */
3061           auto node = this->astCtxt->bvsub(
3062                         op3,
3063                         this->astCtxt->bvmul(
3064                           this->astCtxt->sx(triton::bitsize::dword, op1),
3065                           this->astCtxt->sx(triton::bitsize::dword, op2)
3066                         )
3067                       );
3068 
3069           /* Create symbolic expression */
3070           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMSUBL operation");
3071 
3072           /* Spread taint */
3073           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
3074 
3075           /* Update the symbolic control flow */
3076           this->controlFlow_s(inst);
3077         }
3078 
3079 
smulh_s(triton::arch::Instruction & inst)3080         void AArch64Semantics::smulh_s(triton::arch::Instruction& inst) {
3081           auto& dst  = inst.operands[0];
3082           auto& src1 = inst.operands[1];
3083           auto& src2 = inst.operands[2];
3084 
3085           /* Create symbolic operands */
3086           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3087           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3088 
3089           /* Create the semantics */
3090           auto node = this->astCtxt->extract(
3091                         triton::bitsize::dqword-1,
3092                         triton::bitsize::qword,
3093                         this->astCtxt->bvmul(
3094                           this->astCtxt->sx(triton::bitsize::qword, op1),
3095                           this->astCtxt->sx(triton::bitsize::qword, op2)
3096                         )
3097                       );
3098 
3099           /* Create symbolic expression */
3100           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMULH operation");
3101 
3102           /* Spread taint */
3103           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3104 
3105           /* Update the symbolic control flow */
3106           this->controlFlow_s(inst);
3107         }
3108 
3109 
smull_s(triton::arch::Instruction & inst)3110         void AArch64Semantics::smull_s(triton::arch::Instruction& inst) {
3111           auto& dst  = inst.operands[0];
3112           auto& src1 = inst.operands[1];
3113           auto& src2 = inst.operands[2];
3114 
3115           /* Create symbolic operands */
3116           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3117           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3118 
3119           /* Create the semantics */
3120           auto node = this->astCtxt->bvmul(
3121                         this->astCtxt->sx(triton::bitsize::dword, op1),
3122                         this->astCtxt->sx(triton::bitsize::dword, op2)
3123                       );
3124 
3125           /* Create symbolic expression */
3126           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMULL operation");
3127 
3128           /* Spread taint */
3129           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3130 
3131           /* Update the symbolic control flow */
3132           this->controlFlow_s(inst);
3133         }
3134 
3135 
stlr_s(triton::arch::Instruction & inst)3136         void AArch64Semantics::stlr_s(triton::arch::Instruction& inst) {
3137           triton::arch::OperandWrapper& src = inst.operands[0];
3138           triton::arch::OperandWrapper& dst = inst.operands[1];
3139 
3140           /* Create the semantics of the STORE */
3141           auto node = this->symbolicEngine->getOperandAst(inst, src);
3142 
3143           /* Create symbolic expression */
3144           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLR operation - STORE access");
3145 
3146           /* Spread taint */
3147           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3148 
3149           /* Update the symbolic control flow */
3150           this->controlFlow_s(inst);
3151         }
3152 
3153 
stlrb_s(triton::arch::Instruction & inst)3154         void AArch64Semantics::stlrb_s(triton::arch::Instruction& inst) {
3155           triton::arch::OperandWrapper& src = inst.operands[0];
3156           triton::arch::OperandWrapper& dst = inst.operands[1];
3157 
3158           /* Create the semantics of the STORE */
3159           auto node = this->symbolicEngine->getOperandAst(inst, src);
3160 
3161           /* Special behavior: Define that the size of the memory access is 8 bits */
3162           dst.getMemory().setPair(std::make_pair(7, 0));
3163 
3164           /* Create symbolic expression */
3165           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLRB operation - STORE access");
3166 
3167           /* Spread taint */
3168           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3169 
3170           /* Update the symbolic control flow */
3171           this->controlFlow_s(inst);
3172         }
3173 
3174 
stlrh_s(triton::arch::Instruction & inst)3175         void AArch64Semantics::stlrh_s(triton::arch::Instruction& inst) {
3176           triton::arch::OperandWrapper& src = inst.operands[0];
3177           triton::arch::OperandWrapper& dst = inst.operands[1];
3178 
3179           /* Create the semantics of the STORE */
3180           auto node = this->symbolicEngine->getOperandAst(inst, src);
3181 
3182           /* Special behavior: Define that the size of the memory access is 16 bits */
3183           dst.getMemory().setPair(std::make_pair(15, 0));
3184 
3185           /* Create symbolic expression */
3186           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLRH operation - STORE access");
3187 
3188           /* Spread taint */
3189           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3190 
3191           /* Update the symbolic control flow */
3192           this->controlFlow_s(inst);
3193         }
3194 
3195 
stp_s(triton::arch::Instruction & inst)3196         void AArch64Semantics::stp_s(triton::arch::Instruction& inst) {
3197           triton::arch::OperandWrapper& src1 = inst.operands[0];
3198           triton::arch::OperandWrapper& src2 = inst.operands[1];
3199           triton::arch::OperandWrapper& dst  = inst.operands[2];
3200 
3201           /* Create symbolic operands */
3202           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3203           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3204 
3205           /* Create the semantics */
3206           auto node = this->astCtxt->concat(op2, op1);
3207 
3208           /* Special behavior: Define that the size of the memory access is src1.size + src2.size */
3209           dst.getMemory().setPair(std::make_pair(node->getBitvectorSize()-1, 0));
3210 
3211           /* Create symbolic expression */
3212           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STP operation - STORE access");
3213 
3214           /* Spread taint */
3215           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3216 
3217           /* Optional behavior. Post computation of the base register */
3218           /* STP <Xt1>, <Xt2>, [<Xn|SP>], #<imm> */
3219           if (inst.operands.size() == 4) {
3220             triton::arch::Immediate& imm = inst.operands[3].getImmediate();
3221             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3222 
3223             /* Create symbolic operands of the post computation */
3224             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
3225             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
3226 
3227             /* Create the semantics of the base register */
3228             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
3229 
3230             /* Create symbolic expression */
3231             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STP operation - Base register computation");
3232 
3233             /* Spread taint */
3234             expr2->isTainted = this->taintEngine->isTainted(base);
3235           }
3236 
3237           /* STP <Xt1>, <Xt2>, [<Xn|SP>, #<imm>]! */
3238           else if (inst.operands.size() == 3 && inst.isWriteBack() == true) {
3239             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3240 
3241             /* Create the semantics of the base register */
3242             auto node3 = dst.getMemory().getLeaAst();
3243 
3244             /* Create symbolic expression */
3245             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STP operation - Base register computation");
3246 
3247             /* Spread taint */
3248             expr3->isTainted = this->taintEngine->isTainted(base);
3249           }
3250 
3251           /* Update the symbolic control flow */
3252           this->controlFlow_s(inst);
3253         }
3254 
3255 
str_s(triton::arch::Instruction & inst)3256         void AArch64Semantics::str_s(triton::arch::Instruction& inst) {
3257           triton::arch::OperandWrapper& src = inst.operands[0];
3258           triton::arch::OperandWrapper& dst = inst.operands[1];
3259 
3260           /* Create the semantics of the STORE */
3261           auto node1 = this->symbolicEngine->getOperandAst(inst, src);
3262 
3263           /* Create symbolic expression */
3264           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STR operation - STORE access");
3265 
3266           /* Spread taint */
3267           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
3268 
3269           /* Optional behavior. Post computation of the base register */
3270           /* STR <Xt>, [<Xn|SP>], #<simm> */
3271           if (inst.operands.size() == 3) {
3272             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
3273             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3274 
3275             /* Create symbolic operands of the post computation */
3276             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
3277             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
3278 
3279             /* Create the semantics of the base register */
3280             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
3281 
3282             /* Create symbolic expression */
3283             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STR operation - Base register computation");
3284 
3285             /* Spread taint */
3286             expr2->isTainted = this->taintEngine->isTainted(base);
3287           }
3288 
3289           /* STR <Xt>, [<Xn|SP>, #<simm>]! */
3290           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
3291             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3292 
3293             /* Create the semantics of the base register */
3294             auto node3 = dst.getMemory().getLeaAst();
3295 
3296             /* Create symbolic expression */
3297             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STR operation - Base register computation");
3298 
3299             /* Spread taint */
3300             expr3->isTainted = this->taintEngine->isTainted(base);
3301           }
3302 
3303           /* Update the symbolic control flow */
3304           this->controlFlow_s(inst);
3305         }
3306 
3307 
strb_s(triton::arch::Instruction & inst)3308         void AArch64Semantics::strb_s(triton::arch::Instruction& inst) {
3309           triton::arch::OperandWrapper& src = inst.operands[0];
3310           triton::arch::OperandWrapper& dst = inst.operands[1];
3311 
3312           /* Create symbolic operands */
3313           auto op = this->symbolicEngine->getOperandAst(inst, src);
3314 
3315           /* Create the semantics */
3316           auto node1 = this->astCtxt->extract(7, 0, op);
3317 
3318           /* Special behavior: Define that the size of the memory access is 8 bits */
3319           dst.getMemory().setPair(std::make_pair(7, 0));
3320 
3321           /* Create symbolic expression */
3322           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STRB operation - STORE access");
3323 
3324           /* Spread taint */
3325           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
3326 
3327           /* Optional behavior. Post computation of the base register */
3328           /* STRB <Wt>, [<Xn|SP>], #<simm> */
3329           if (inst.operands.size() == 3) {
3330             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
3331             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3332 
3333             /* Create symbolic operands of the post computation */
3334             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
3335             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
3336 
3337             /* Create the semantics of the base register */
3338             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
3339 
3340             /* Create symbolic expression */
3341             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STRB operation - Base register computation");
3342 
3343             /* Spread taint */
3344             expr2->isTainted = this->taintEngine->isTainted(base);
3345           }
3346 
3347           /* STRB <Wt>, [<Xn|SP>, #<simm>]! */
3348           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
3349             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3350 
3351             /* Create the semantics of the base register */
3352             auto node3 = dst.getMemory().getLeaAst();
3353 
3354             /* Create symbolic expression */
3355             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STRB operation - Base register computation");
3356 
3357             /* Spread taint */
3358             expr3->isTainted = this->taintEngine->isTainted(base);
3359           }
3360 
3361           /* Update the symbolic control flow */
3362           this->controlFlow_s(inst);
3363         }
3364 
3365 
strh_s(triton::arch::Instruction & inst)3366         void AArch64Semantics::strh_s(triton::arch::Instruction& inst) {
3367           triton::arch::OperandWrapper& src = inst.operands[0];
3368           triton::arch::OperandWrapper& dst = inst.operands[1];
3369 
3370           /* Create symbolic operands */
3371           auto op = this->symbolicEngine->getOperandAst(inst, src);
3372 
3373           /* Create the semantics */
3374           auto node1 = this->astCtxt->extract(15, 0, op);
3375 
3376           /* Special behavior: Define that the size of the memory access is 16 bits */
3377           dst.getMemory().setPair(std::make_pair(15, 0));
3378 
3379           /* Create symbolic expression */
3380           auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STRH operation - STORE access");
3381 
3382           /* Spread taint */
3383           expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
3384 
3385           /* Optional behavior. Post computation of the base register */
3386           /* STRH <Wt>, [<Xn|SP>], #<simm> */
3387           if (inst.operands.size() == 3) {
3388             triton::arch::Immediate& imm = inst.operands[2].getImmediate();
3389             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3390 
3391             /* Create symbolic operands of the post computation */
3392             auto baseNode = this->symbolicEngine->getOperandAst(inst, base);
3393             auto immNode  = this->symbolicEngine->getOperandAst(inst, imm);
3394 
3395             /* Create the semantics of the base register */
3396             auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
3397 
3398             /* Create symbolic expression */
3399             auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STRH operation - Base register computation");
3400 
3401             /* Spread taint */
3402             expr2->isTainted = this->taintEngine->isTainted(base);
3403           }
3404 
3405           /* STRH <Wt>, [<Xn|SP>, #<simm>]! */
3406           else if (inst.operands.size() == 2 && inst.isWriteBack() == true) {
3407             triton::arch::Register& base = dst.getMemory().getBaseRegister();
3408 
3409             /* Create the semantics of the base register */
3410             auto node3 = dst.getMemory().getLeaAst();
3411 
3412             /* Create symbolic expression */
3413             auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STRH operation - Base register computation");
3414 
3415             /* Spread taint */
3416             expr3->isTainted = this->taintEngine->isTainted(base);
3417           }
3418 
3419           /* Update the symbolic control flow */
3420           this->controlFlow_s(inst);
3421         }
3422 
3423 
stur_s(triton::arch::Instruction & inst)3424         void AArch64Semantics::stur_s(triton::arch::Instruction& inst) {
3425           triton::arch::OperandWrapper& src = inst.operands[0];
3426           triton::arch::OperandWrapper& dst = inst.operands[1];
3427 
3428           /* Create the semantics of the STORE */
3429           auto node = this->symbolicEngine->getOperandAst(inst, src);
3430 
3431           /* Create symbolic expression */
3432           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STUR operation");
3433 
3434           /* Spread taint */
3435           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3436 
3437           /* Update the symbolic control flow */
3438           this->controlFlow_s(inst);
3439         }
3440 
3441 
sturb_s(triton::arch::Instruction & inst)3442         void AArch64Semantics::sturb_s(triton::arch::Instruction& inst) {
3443           triton::arch::OperandWrapper& src = inst.operands[0];
3444           triton::arch::OperandWrapper& dst = inst.operands[1];
3445 
3446           /* Create symbolic operands */
3447           auto op = this->symbolicEngine->getOperandAst(inst, src);
3448 
3449           /* Create the semantics */
3450           auto node = this->astCtxt->extract(7, 0, op);
3451 
3452           /* Special behavior: Define that the size of the memory access is 8 bits */
3453           dst.getMemory().setPair(std::make_pair(7, 0));
3454 
3455           /* Create symbolic expression */
3456           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STURB operation");
3457 
3458           /* Spread taint */
3459           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3460 
3461           /* Update the symbolic control flow */
3462           this->controlFlow_s(inst);
3463         }
3464 
3465 
sturh_s(triton::arch::Instruction & inst)3466         void AArch64Semantics::sturh_s(triton::arch::Instruction& inst) {
3467           triton::arch::OperandWrapper& src = inst.operands[0];
3468           triton::arch::OperandWrapper& dst = inst.operands[1];
3469 
3470           /* Create symbolic operands */
3471           auto op = this->symbolicEngine->getOperandAst(inst, src);
3472 
3473           /* Create the semantics */
3474           auto node = this->astCtxt->extract(15, 0, op);
3475 
3476           /* Special behavior: Define that the size of the memory access is 16 bits */
3477           dst.getMemory().setPair(std::make_pair(15, 0));
3478 
3479           /* Create symbolic expression */
3480           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STURH operation");
3481 
3482           /* Spread taint */
3483           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3484 
3485           /* Update the symbolic control flow */
3486           this->controlFlow_s(inst);
3487         }
3488 
3489 
sub_s(triton::arch::Instruction & inst)3490         void AArch64Semantics::sub_s(triton::arch::Instruction& inst) {
3491           auto& dst  = inst.operands[0];
3492           auto& src1 = inst.operands[1];
3493           auto& src2 = inst.operands[2];
3494 
3495           /* Create symbolic operands */
3496           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3497           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3498 
3499           /* Create the semantics */
3500           auto node = this->astCtxt->bvsub(op1, op2);
3501 
3502           /* Create symbolic expression */
3503           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SUB(S) operation");
3504 
3505           /* Spread taint */
3506           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3507 
3508           /* Update symbolic flags */
3509           if (inst.isUpdateFlag() == true) {
3510             this->cfSub_s(inst, expr, dst, op1, op2);
3511             this->nf_s(inst, expr, dst);
3512             this->vfSub_s(inst, expr, dst, op1, op2);
3513             this->zf_s(inst, expr, dst);
3514           }
3515 
3516           /* Update the symbolic control flow */
3517           this->controlFlow_s(inst);
3518         }
3519 
3520 
svc_s(triton::arch::Instruction & inst)3521         void AArch64Semantics::svc_s(triton::arch::Instruction& inst) {
3522           auto& src = inst.operands[0];
3523 
3524           /* Link the immediate to the instruction */
3525           this->symbolicEngine->getOperandAst(inst, src);
3526 
3527           /* Update the symbolic control flow */
3528           this->controlFlow_s(inst);
3529         }
3530 
3531 
sxtb_s(triton::arch::Instruction & inst)3532         void AArch64Semantics::sxtb_s(triton::arch::Instruction& inst) {
3533           auto& dst = inst.operands[0];
3534           auto& src = inst.operands[1];
3535 
3536           /* Create symbolic operands */
3537           auto op = this->symbolicEngine->getOperandAst(inst, src);
3538 
3539           /* Create the semantics */
3540           auto node = this->astCtxt->sx(dst.getBitSize() - 8, this->astCtxt->extract(7, 0, op));
3541 
3542           /* Create symbolic expression */
3543           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTB operation");
3544 
3545           /* Spread taint */
3546           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3547 
3548           /* Update the symbolic control flow */
3549           this->controlFlow_s(inst);
3550         }
3551 
3552 
sxth_s(triton::arch::Instruction & inst)3553         void AArch64Semantics::sxth_s(triton::arch::Instruction& inst) {
3554           auto& dst = inst.operands[0];
3555           auto& src = inst.operands[1];
3556 
3557           /* Create symbolic operands */
3558           auto op = this->symbolicEngine->getOperandAst(inst, src);
3559 
3560           /* Create the semantics */
3561           auto node = this->astCtxt->sx(dst.getBitSize() - 16, this->astCtxt->extract(15, 0, op));
3562 
3563           /* Create symbolic expression */
3564           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTH operation");
3565 
3566           /* Spread taint */
3567           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3568 
3569           /* Update the symbolic control flow */
3570           this->controlFlow_s(inst);
3571         }
3572 
3573 
sxtw_s(triton::arch::Instruction & inst)3574         void AArch64Semantics::sxtw_s(triton::arch::Instruction& inst) {
3575           auto& dst = inst.operands[0];
3576           auto& src = inst.operands[1];
3577 
3578           /* Create symbolic operands */
3579           auto op = this->symbolicEngine->getOperandAst(inst, src);
3580 
3581           /* Create the semantics */
3582           auto node = this->astCtxt->sx(dst.getBitSize() - 32, this->astCtxt->extract(31, 0, op));
3583 
3584           /* Create symbolic expression */
3585           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTW operation");
3586 
3587           /* Spread taint */
3588           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3589 
3590           /* Update the symbolic control flow */
3591           this->controlFlow_s(inst);
3592         }
3593 
3594 
tbnz_s(triton::arch::Instruction & inst)3595         void AArch64Semantics::tbnz_s(triton::arch::Instruction& inst) {
3596           auto  dst  = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
3597           auto& src1 = inst.operands[0];
3598           auto& src2 = inst.operands[1];
3599           auto& src3 = inst.operands[2];
3600 
3601           /* Create symbolic operands */
3602           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3603           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3604           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
3605 
3606           /* Create the semantics */
3607           auto node = this->astCtxt->ite(
3608                         this->astCtxt->equal(
3609                           this->astCtxt->extract(0, 0, this->astCtxt->bvlshr(op1, op2)),
3610                           this->astCtxt->bvtrue()
3611                         ),
3612                         op3,
3613                         this->astCtxt->bv(inst.getNextAddress(), dst.getBitSize())
3614                       );
3615 
3616           /* Create symbolic expression */
3617           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "TBNZ operation - Program Counter");
3618 
3619           /* Spread taint */
3620           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3621         }
3622 
3623 
tbz_s(triton::arch::Instruction & inst)3624         void AArch64Semantics::tbz_s(triton::arch::Instruction& inst) {
3625           auto  dst  = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_AARCH64_PC));
3626           auto& src1 = inst.operands[0];
3627           auto& src2 = inst.operands[1];
3628           auto& src3 = inst.operands[2];
3629 
3630           /* Create symbolic operands */
3631           auto op1 = this->astCtxt->zx(dst.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
3632           auto op2 = this->astCtxt->zx(dst.getBitSize() - src2.getBitSize(), this->symbolicEngine->getOperandAst(inst, src2));
3633           auto op3 = this->astCtxt->zx(dst.getBitSize() - src3.getBitSize(), this->symbolicEngine->getOperandAst(inst, src3));
3634 
3635           /* Create the semantics */
3636           auto node = this->astCtxt->ite(
3637                         this->astCtxt->equal(
3638                           this->astCtxt->extract(0, 0, this->astCtxt->bvlshr(op1, op2)),
3639                           this->astCtxt->bvfalse()
3640                         ),
3641                         op3,
3642                         this->astCtxt->bv(inst.getNextAddress(), dst.getBitSize())
3643                       );
3644 
3645           /* Create symbolic expression */
3646           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "TBZ operation - Program Counter");
3647 
3648           /* Spread taint */
3649           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3650         }
3651 
3652 
tst_s(triton::arch::Instruction & inst)3653         void AArch64Semantics::tst_s(triton::arch::Instruction& inst) {
3654           auto& src1 = inst.operands[0];
3655           auto& src2 = inst.operands[1];
3656 
3657           /* Create symbolic operands */
3658           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3659           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3660 
3661           /* Create the semantics */
3662           auto node = this->astCtxt->bvand(op1, op2);
3663 
3664           /* Create symbolic expression */
3665           auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "TST operation");
3666 
3667           /* Spread taint */
3668           expr->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2);
3669 
3670           /* Update symbolic flags */
3671           if (inst.isUpdateFlag() == true) {
3672             this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_AARCH64_C), "Clears carry flag");
3673             this->nf_s(inst, expr, src1);
3674             this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_AARCH64_V), "Clears overflow flag");
3675             this->zf_s(inst, expr, src1);
3676           }
3677 
3678           /* Update the symbolic control flow */
3679           this->controlFlow_s(inst);
3680         }
3681 
3682 
ubfiz_s(triton::arch::Instruction & inst)3683         void AArch64Semantics::ubfiz_s(triton::arch::Instruction& inst) {
3684           auto& dst   = inst.operands[0];
3685           auto& src1  = inst.operands[1];
3686           auto& src2  = inst.operands[2];
3687           auto& src3  = inst.operands[3];
3688           auto  lsb   = src2.getImmediate().getValue();
3689           auto  width = src3.getImmediate().getValue();
3690 
3691           if (lsb + width > dst.getBitSize())
3692             throw triton::exceptions::Semantics("AArch64Semantics::ubfiz_s(): Invalid lsb and width.");
3693 
3694           /* Create symbolic operands */
3695           auto op = this->symbolicEngine->getOperandAst(inst, src1);
3696 
3697           /* Create the semantics */
3698           std::vector<triton::ast::SharedAbstractNode> bits;
3699           bits.reserve(3);
3700 
3701           if (lsb + width < dst.getBitSize()) {
3702             bits.push_back(this->astCtxt->bv(0, dst.getBitSize() - (lsb + width)));
3703           }
3704 
3705           bits.push_back(this->astCtxt->extract(width, 0, op));
3706 
3707           if (lsb) {
3708             bits.push_back(this->astCtxt->bv(0, lsb));
3709           }
3710 
3711           auto node = this->astCtxt->concat(bits);
3712 
3713           /* Create symbolic expression */
3714           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UBFIZ operation");
3715 
3716           /* Spread taint */
3717           expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
3718 
3719           /* Update the symbolic control flow */
3720           this->controlFlow_s(inst);
3721         }
3722 
3723 
ubfx_s(triton::arch::Instruction & inst)3724         void AArch64Semantics::ubfx_s(triton::arch::Instruction& inst) {
3725           auto& dst   = inst.operands[0];
3726           auto& src1  = inst.operands[1];
3727           auto& src2  = inst.operands[2];
3728           auto& src3  = inst.operands[3];
3729           auto  lsb   = src2.getImmediate().getValue();
3730           auto  width = src3.getImmediate().getValue();
3731 
3732           if (lsb + width > dst.getBitSize())
3733             throw triton::exceptions::Semantics("AArch64Semantics::ubfx_s(): Invalid lsb and width.");
3734 
3735           /* Create symbolic operands */
3736           auto op = this->symbolicEngine->getOperandAst(inst, src1);
3737 
3738           /* Create the semantics */
3739           auto node = this->astCtxt->zx(dst.getBitSize() - width, this->astCtxt->extract(lsb+width-1, lsb, op));
3740 
3741           /* Create symbolic expression */
3742           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UBFX operation");
3743 
3744           /* Spread taint */
3745           expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
3746 
3747           /* Update the symbolic control flow */
3748           this->controlFlow_s(inst);
3749         }
3750 
3751 
udiv_s(triton::arch::Instruction & inst)3752         void AArch64Semantics::udiv_s(triton::arch::Instruction& inst) {
3753           auto& dst  = inst.operands[0];
3754           auto& src1 = inst.operands[1];
3755           auto& src2 = inst.operands[2];
3756 
3757           /* Create symbolic operands */
3758           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3759           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3760 
3761           /* Create the semantics */
3762           auto node = this->astCtxt->ite(
3763                         this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
3764                         this->astCtxt->bv(0, dst.getBitSize()),
3765                         this->astCtxt->bvudiv(op1, op2)
3766                       );
3767 
3768           /* Create symbolic expression */
3769           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UDIV operation");
3770 
3771           /* Spread taint */
3772           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3773 
3774           /* Update the symbolic control flow */
3775           this->controlFlow_s(inst);
3776         }
3777 
3778 
umaddl_s(triton::arch::Instruction & inst)3779         void AArch64Semantics::umaddl_s(triton::arch::Instruction& inst) {
3780           auto& dst  = inst.operands[0];
3781           auto& src1 = inst.operands[1];
3782           auto& src2 = inst.operands[2];
3783           auto& src3 = inst.operands[3];
3784 
3785           /* Create symbolic operands */
3786           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3787           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3788           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
3789 
3790           /* Create the semantics */
3791           auto node = this->astCtxt->bvadd(
3792                         op3,
3793                         this->astCtxt->bvmul(
3794                           this->astCtxt->zx(triton::bitsize::dword, op1),
3795                           this->astCtxt->zx(triton::bitsize::dword, op2)
3796                         )
3797                       );
3798 
3799           /* Create symbolic expression */
3800           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMADDL operation");
3801 
3802           /* Spread taint */
3803           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
3804 
3805           /* Update the symbolic control flow */
3806           this->controlFlow_s(inst);
3807         }
3808 
3809 
umnegl_s(triton::arch::Instruction & inst)3810         void AArch64Semantics::umnegl_s(triton::arch::Instruction& inst) {
3811           auto& dst  = inst.operands[0];
3812           auto& src1 = inst.operands[1];
3813           auto& src2 = inst.operands[2];
3814 
3815           /* Create symbolic operands */
3816           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3817           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3818 
3819           /* Create the semantics */
3820           auto node = this->astCtxt->bvneg(
3821                         this->astCtxt->bvmul(
3822                           this->astCtxt->zx(triton::bitsize::dword, op1),
3823                           this->astCtxt->zx(triton::bitsize::dword, op2)
3824                         )
3825                       );
3826 
3827           /* Create symbolic expression */
3828           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMNEGL operation");
3829 
3830           /* Spread taint */
3831           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3832 
3833           /* Update the symbolic control flow */
3834           this->controlFlow_s(inst);
3835         }
3836 
3837 
umsubl_s(triton::arch::Instruction & inst)3838         void AArch64Semantics::umsubl_s(triton::arch::Instruction& inst) {
3839           auto& dst  = inst.operands[0];
3840           auto& src1 = inst.operands[1];
3841           auto& src2 = inst.operands[2];
3842           auto& src3 = inst.operands[3];
3843 
3844           /* Create symbolic operands */
3845           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3846           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3847           auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
3848 
3849           /* Create the semantics */
3850           auto node = this->astCtxt->bvsub(
3851                         op3,
3852                         this->astCtxt->bvmul(
3853                           this->astCtxt->zx(triton::bitsize::dword, op1),
3854                           this->astCtxt->zx(triton::bitsize::dword, op2)
3855                         )
3856                       );
3857 
3858           /* Create symbolic expression */
3859           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMSUBL operation");
3860 
3861           /* Spread taint */
3862           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
3863 
3864           /* Update the symbolic control flow */
3865           this->controlFlow_s(inst);
3866         }
3867 
3868 
umulh_s(triton::arch::Instruction & inst)3869         void AArch64Semantics::umulh_s(triton::arch::Instruction& inst) {
3870           auto& dst  = inst.operands[0];
3871           auto& src1 = inst.operands[1];
3872           auto& src2 = inst.operands[2];
3873 
3874           /* Create symbolic operands */
3875           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3876           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3877 
3878           /* Create the semantics */
3879           auto node = this->astCtxt->extract(
3880                         triton::bitsize::dqword-1,
3881                         triton::bitsize::qword,
3882                         this->astCtxt->bvmul(
3883                           this->astCtxt->zx(triton::bitsize::qword, op1),
3884                           this->astCtxt->zx(triton::bitsize::qword, op2)
3885                         )
3886                       );
3887 
3888           /* Create symbolic expression */
3889           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMULH operation");
3890 
3891           /* Spread taint */
3892           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3893 
3894           /* Update the symbolic control flow */
3895           this->controlFlow_s(inst);
3896         }
3897 
3898 
umull_s(triton::arch::Instruction & inst)3899         void AArch64Semantics::umull_s(triton::arch::Instruction& inst) {
3900           auto& dst  = inst.operands[0];
3901           auto& src1 = inst.operands[1];
3902           auto& src2 = inst.operands[2];
3903 
3904           /* Create symbolic operands */
3905           auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3906           auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3907 
3908           /* Create the semantics */
3909           auto node = this->astCtxt->bvmul(
3910                         this->astCtxt->zx(triton::bitsize::dword, op1),
3911                         this->astCtxt->zx(triton::bitsize::dword, op2)
3912                       );
3913 
3914           /* Create symbolic expression */
3915           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMULL operation");
3916 
3917           /* Spread taint */
3918           expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
3919 
3920           /* Update the symbolic control flow */
3921           this->controlFlow_s(inst);
3922         }
3923 
3924 
uxtb_s(triton::arch::Instruction & inst)3925         void AArch64Semantics::uxtb_s(triton::arch::Instruction& inst) {
3926           auto& dst = inst.operands[0];
3927           auto& src = inst.operands[1];
3928 
3929           /* Create symbolic operands */
3930           auto op = this->symbolicEngine->getOperandAst(inst, src);
3931 
3932           /* Create the semantics */
3933           auto node = this->astCtxt->zx(dst.getBitSize() - 8, this->astCtxt->extract(7, 0, op));
3934 
3935           /* Create symbolic expression */
3936           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UXTB operation");
3937 
3938           /* Spread taint */
3939           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3940 
3941           /* Update the symbolic control flow */
3942           this->controlFlow_s(inst);
3943         }
3944 
3945 
uxth_s(triton::arch::Instruction & inst)3946         void AArch64Semantics::uxth_s(triton::arch::Instruction& inst) {
3947           auto& dst = inst.operands[0];
3948           auto& src = inst.operands[1];
3949 
3950           /* Create symbolic operands */
3951           auto op = this->symbolicEngine->getOperandAst(inst, src);
3952 
3953           /* Create the semantics */
3954           auto node = this->astCtxt->zx(dst.getBitSize() - 16, this->astCtxt->extract(15, 0, op));
3955 
3956           /* Create symbolic expression */
3957           auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UXTH operation");
3958 
3959           /* Spread taint */
3960           expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3961 
3962           /* Update the symbolic control flow */
3963           this->controlFlow_s(inst);
3964         }
3965 
3966       }; /* aarch64 namespace */
3967     }; /* arm namespace */
3968   }; /* arch namespace */
3969 }; /* triton namespace */
3970