libTriton  version 0.7 build 1419
x86Semantics.cpp
Go to the documentation of this file.
1 /*
3 ** Copyright (C) - Triton
4 **
5 ** This program is under the terms of the BSD License.
6 */
7 
8 #include <triton/cpuSize.hpp>
9 #include <triton/exceptions.hpp>
10 #include <triton/x86Semantics.hpp>
12 #include <triton/astContext.hpp>
13 
14 
15 
328 namespace triton {
329  namespace arch {
330  namespace x86 {
331 
335  const triton::modes::SharedModes& modes,
336  const triton::ast::SharedAstContext& astCtxt) : modes(modes), astCtxt(astCtxt) {
337 
338  this->architecture = architecture;
339  this->symbolicEngine = symbolicEngine;
340  this->taintEngine = taintEngine;
341 
342  if (architecture == nullptr)
343  throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The architecture API must be defined.");
344 
345  if (this->symbolicEngine == nullptr)
346  throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The symbolic engine API must be defined.");
347 
348  if (this->taintEngine == nullptr)
349  throw triton::exceptions::Semantics("x86Semantics::x86Semantics(): The taint engines API must be defined.");
350  }
351 
352 
354  switch (inst.getType()) {
355  case ID_INS_AAA: this->aaa_s(inst); break;
356  case ID_INS_AAD: this->aad_s(inst); break;
357  case ID_INS_AAM: this->aam_s(inst); break;
358  case ID_INS_AAS: this->aas_s(inst); break;
359  case ID_INS_ADC: this->adc_s(inst); break;
360  case ID_INS_ADCX: this->adcx_s(inst); break;
361  case ID_INS_ADD: this->add_s(inst); break;
362  case ID_INS_AND: this->and_s(inst); break;
363  case ID_INS_ANDN: this->andn_s(inst); break;
364  case ID_INS_ANDNPD: this->andnpd_s(inst); break;
365  case ID_INS_ANDNPS: this->andnps_s(inst); break;
366  case ID_INS_ANDPD: this->andpd_s(inst); break;
367  case ID_INS_ANDPS: this->andps_s(inst); break;
368  case ID_INS_BEXTR: this->bextr_s(inst); break;
369  case ID_INS_BLSI: this->blsi_s(inst); break;
370  case ID_INS_BLSMSK: this->blsmsk_s(inst); break;
371  case ID_INS_BLSR: this->blsr_s(inst); break;
372  case ID_INS_BSF: this->bsf_s(inst); break;
373  case ID_INS_BSR: this->bsr_s(inst); break;
374  case ID_INS_BSWAP: this->bswap_s(inst); break;
375  case ID_INS_BT: this->bt_s(inst); break;
376  case ID_INS_BTC: this->btc_s(inst); break;
377  case ID_INS_BTR: this->btr_s(inst); break;
378  case ID_INS_BTS: this->bts_s(inst); break;
379  case ID_INS_CALL: this->call_s(inst); break;
380  case ID_INS_CBW: this->cbw_s(inst); break;
381  case ID_INS_CDQ: this->cdq_s(inst); break;
382  case ID_INS_CDQE: this->cdqe_s(inst); break;
383  case ID_INS_CLC: this->clc_s(inst); break;
384  case ID_INS_CLD: this->cld_s(inst); break;
385  case ID_INS_CLFLUSH: this->clflush_s(inst); break;
386  case ID_INS_CLTS: this->clts_s(inst); break;
387  case ID_INS_CLI: this->cli_s(inst); break;
388  case ID_INS_CMC: this->cmc_s(inst); break;
389  case ID_INS_CMOVA: this->cmova_s(inst); break;
390  case ID_INS_CMOVAE: this->cmovae_s(inst); break;
391  case ID_INS_CMOVB: this->cmovb_s(inst); break;
392  case ID_INS_CMOVBE: this->cmovbe_s(inst); break;
393  case ID_INS_CMOVE: this->cmove_s(inst); break;
394  case ID_INS_CMOVG: this->cmovg_s(inst); break;
395  case ID_INS_CMOVGE: this->cmovge_s(inst); break;
396  case ID_INS_CMOVL: this->cmovl_s(inst); break;
397  case ID_INS_CMOVLE: this->cmovle_s(inst); break;
398  case ID_INS_CMOVNE: this->cmovne_s(inst); break;
399  case ID_INS_CMOVNO: this->cmovno_s(inst); break;
400  case ID_INS_CMOVNP: this->cmovnp_s(inst); break;
401  case ID_INS_CMOVNS: this->cmovns_s(inst); break;
402  case ID_INS_CMOVO: this->cmovo_s(inst); break;
403  case ID_INS_CMOVP: this->cmovp_s(inst); break;
404  case ID_INS_CMOVS: this->cmovs_s(inst); break;
405  case ID_INS_CMP: this->cmp_s(inst); break;
406  case ID_INS_CMPSB: this->cmpsb_s(inst); break;
407  case ID_INS_CMPSD: this->cmpsd_s(inst); break;
408  case ID_INS_CMPSQ: this->cmpsq_s(inst); break;
409  case ID_INS_CMPSW: this->cmpsw_s(inst); break;
410  case ID_INS_CMPXCHG: this->cmpxchg_s(inst); break;
411  case ID_INS_CMPXCHG16B: this->cmpxchg16b_s(inst); break;
412  case ID_INS_CMPXCHG8B: this->cmpxchg8b_s(inst); break;
413  case ID_INS_CPUID: this->cpuid_s(inst); break;
414  case ID_INS_CQO: this->cqo_s(inst); break;
415  case ID_INS_CWD: this->cwd_s(inst); break;
416  case ID_INS_CWDE: this->cwde_s(inst); break;
417  case ID_INS_DEC: this->dec_s(inst); break;
418  case ID_INS_DIV: this->div_s(inst); break;
419  case ID_INS_EXTRACTPS: this->extractps_s(inst); break;
420  case ID_INS_IDIV: this->idiv_s(inst); break;
421  case ID_INS_IMUL: this->imul_s(inst); break;
422  case ID_INS_INC: this->inc_s(inst); break;
423  case ID_INS_INVD: this->invd_s(inst); break;
424  case ID_INS_INVLPG: this->invlpg_s(inst); break;
425  case ID_INS_JA: this->ja_s(inst); break;
426  case ID_INS_JAE: this->jae_s(inst); break;
427  case ID_INS_JB: this->jb_s(inst); break;
428  case ID_INS_JBE: this->jbe_s(inst); break;
429  case ID_INS_JE: this->je_s(inst); break;
430  case ID_INS_JG: this->jg_s(inst); break;
431  case ID_INS_JGE: this->jge_s(inst); break;
432  case ID_INS_JL: this->jl_s(inst); break;
433  case ID_INS_JLE: this->jle_s(inst); break;
434  case ID_INS_JMP: this->jmp_s(inst); break;
435  case ID_INS_JNE: this->jne_s(inst); break;
436  case ID_INS_JNO: this->jno_s(inst); break;
437  case ID_INS_JNP: this->jnp_s(inst); break;
438  case ID_INS_JNS: this->jns_s(inst); break;
439  case ID_INS_JO: this->jo_s(inst); break;
440  case ID_INS_JP: this->jp_s(inst); break;
441  case ID_INS_JS: this->js_s(inst); break;
442  case ID_INS_LAHF: this->lahf_s(inst); break;
443  case ID_INS_LDDQU: this->lddqu_s(inst); break;
444  case ID_INS_LDMXCSR: this->ldmxcsr_s(inst); break;
445  case ID_INS_LEA: this->lea_s(inst); break;
446  case ID_INS_LEAVE: this->leave_s(inst); break;
447  case ID_INS_LFENCE: this->lfence_s(inst); break;
448  case ID_INS_LODSB: this->lodsb_s(inst); break;
449  case ID_INS_LODSD: this->lodsd_s(inst); break;
450  case ID_INS_LODSQ: this->lodsq_s(inst); break;
451  case ID_INS_LODSW: this->lodsw_s(inst); break;
452  case ID_INS_MFENCE: this->mfence_s(inst); break;
453  case ID_INS_MOV: this->mov_s(inst); break;
454  case ID_INS_MOVABS: this->movabs_s(inst); break;
455  case ID_INS_MOVAPD: this->movapd_s(inst); break;
456  case ID_INS_MOVAPS: this->movaps_s(inst); break;
457  case ID_INS_MOVD: this->movd_s(inst); break;
458  case ID_INS_MOVDDUP: this->movddup_s(inst); break;
459  case ID_INS_MOVDQ2Q: this->movdq2q_s(inst); break;
460  case ID_INS_MOVDQA: this->movdqa_s(inst); break;
461  case ID_INS_MOVDQU: this->movdqu_s(inst); break;
462  case ID_INS_MOVHLPS: this->movhlps_s(inst); break;
463  case ID_INS_MOVHPD: this->movhpd_s(inst); break;
464  case ID_INS_MOVHPS: this->movhps_s(inst); break;
465  case ID_INS_MOVLHPS: this->movlhps_s(inst); break;
466  case ID_INS_MOVLPD: this->movlpd_s(inst); break;
467  case ID_INS_MOVLPS: this->movlps_s(inst); break;
468  case ID_INS_MOVMSKPD: this->movmskpd_s(inst); break;
469  case ID_INS_MOVMSKPS: this->movmskps_s(inst); break;
470  case ID_INS_MOVNTDQ: this->movntdq_s(inst); break;
471  case ID_INS_MOVNTI: this->movnti_s(inst); break;
472  case ID_INS_MOVNTPD: this->movntpd_s(inst); break;
473  case ID_INS_MOVNTPS: this->movntps_s(inst); break;
474  case ID_INS_MOVNTQ: this->movntq_s(inst); break;
475  case ID_INS_MOVQ2DQ: this->movq2dq_s(inst); break;
476  case ID_INS_MOVQ: this->movq_s(inst); break;
477  case ID_INS_MOVSB: this->movsb_s(inst); break;
478  case ID_INS_MOVSD: this->movsd_s(inst); break;
479  case ID_INS_MOVSHDUP: this->movshdup_s(inst); break;
480  case ID_INS_MOVSLDUP: this->movsldup_s(inst); break;
481  case ID_INS_MOVSQ: this->movsq_s(inst); break;
482  case ID_INS_MOVSW: this->movsw_s(inst); break;
483  case ID_INS_MOVSX: this->movsx_s(inst); break;
484  case ID_INS_MOVSXD: this->movsxd_s(inst); break;
485  case ID_INS_MOVUPD: this->movupd_s(inst); break;
486  case ID_INS_MOVUPS: this->movups_s(inst); break;
487  case ID_INS_MOVZX: this->movzx_s(inst); break;
488  case ID_INS_MUL: this->mul_s(inst); break;
489  case ID_INS_MULX: this->mulx_s(inst); break;
490  case ID_INS_NEG: this->neg_s(inst); break;
491  case ID_INS_NOP: this->nop_s(inst); break;
492  case ID_INS_NOT: this->not_s(inst); break;
493  case ID_INS_OR: this->or_s(inst); break;
494  case ID_INS_ORPD: this->orpd_s(inst); break;
495  case ID_INS_ORPS: this->orps_s(inst); break;
496  case ID_INS_PADDB: this->paddb_s(inst); break;
497  case ID_INS_PADDD: this->paddd_s(inst); break;
498  case ID_INS_PADDQ: this->paddq_s(inst); break;
499  case ID_INS_PADDW: this->paddw_s(inst); break;
500  case ID_INS_PAND: this->pand_s(inst); break;
501  case ID_INS_PANDN: this->pandn_s(inst); break;
502  case ID_INS_PAUSE: this->pause_s(inst); break;
503  case ID_INS_PAVGB: this->pavgb_s(inst); break;
504  case ID_INS_PAVGW: this->pavgw_s(inst); break;
505  case ID_INS_PCMPEQB: this->pcmpeqb_s(inst); break;
506  case ID_INS_PCMPEQD: this->pcmpeqd_s(inst); break;
507  case ID_INS_PCMPEQW: this->pcmpeqw_s(inst); break;
508  case ID_INS_PCMPGTB: this->pcmpgtb_s(inst); break;
509  case ID_INS_PCMPGTD: this->pcmpgtd_s(inst); break;
510  case ID_INS_PCMPGTW: this->pcmpgtw_s(inst); break;
511  case ID_INS_PMAXSB: this->pmaxsb_s(inst); break;
512  case ID_INS_PMAXSD: this->pmaxsd_s(inst); break;
513  case ID_INS_PMAXSW: this->pmaxsw_s(inst); break;
514  case ID_INS_PMAXUB: this->pmaxub_s(inst); break;
515  case ID_INS_PMAXUD: this->pmaxud_s(inst); break;
516  case ID_INS_PMAXUW: this->pmaxuw_s(inst); break;
517  case ID_INS_PMINSB: this->pminsb_s(inst); break;
518  case ID_INS_PMINSD: this->pminsd_s(inst); break;
519  case ID_INS_PMINSW: this->pminsw_s(inst); break;
520  case ID_INS_PMINUB: this->pminub_s(inst); break;
521  case ID_INS_PMINUD: this->pminud_s(inst); break;
522  case ID_INS_PMINUW: this->pminuw_s(inst); break;
523  case ID_INS_PMOVMSKB: this->pmovmskb_s(inst); break;
524  case ID_INS_PMOVSXBD: this->pmovsxbd_s(inst); break;
525  case ID_INS_PMOVSXBQ: this->pmovsxbq_s(inst); break;
526  case ID_INS_PMOVSXBW: this->pmovsxbw_s(inst); break;
527  case ID_INS_PMOVSXDQ: this->pmovsxdq_s(inst); break;
528  case ID_INS_PMOVSXWD: this->pmovsxwd_s(inst); break;
529  case ID_INS_PMOVSXWQ: this->pmovsxwq_s(inst); break;
530  case ID_INS_PMOVZXBD: this->pmovzxbd_s(inst); break;
531  case ID_INS_PMOVZXBQ: this->pmovzxbq_s(inst); break;
532  case ID_INS_PMOVZXBW: this->pmovzxbw_s(inst); break;
533  case ID_INS_PMOVZXDQ: this->pmovzxdq_s(inst); break;
534  case ID_INS_PMOVZXWD: this->pmovzxwd_s(inst); break;
535  case ID_INS_PMOVZXWQ: this->pmovzxwq_s(inst); break;
536  case ID_INS_POP: this->pop_s(inst); break;
537  case ID_INS_POPAL: this->popal_s(inst); break;
538  case ID_INS_POPF: this->popf_s(inst); break;
539  case ID_INS_POPFD: this->popfd_s(inst); break;
540  case ID_INS_POPFQ: this->popfq_s(inst); break;
541  case ID_INS_POR: this->por_s(inst); break;
542  case ID_INS_PREFETCH: this->prefetchx_s(inst); break;
543  case ID_INS_PREFETCHNTA: this->prefetchx_s(inst); break;
544  case ID_INS_PREFETCHT0: this->prefetchx_s(inst); break;
545  case ID_INS_PREFETCHT1: this->prefetchx_s(inst); break;
546  case ID_INS_PREFETCHT2: this->prefetchx_s(inst); break;
547  case ID_INS_PREFETCHW: this->prefetchx_s(inst); break;
548  case ID_INS_PSHUFD: this->pshufd_s(inst); break;
549  case ID_INS_PSHUFHW: this->pshufhw_s(inst); break;
550  case ID_INS_PSHUFLW: this->pshuflw_s(inst); break;
551  case ID_INS_PSHUFW: this->pshufw_s(inst); break;
552  case ID_INS_PSLLD: this->pslld_s(inst); break;
553  case ID_INS_PSLLDQ: this->pslldq_s(inst); break;
554  case ID_INS_PSLLQ: this->psllq_s(inst); break;
555  case ID_INS_PSLLW: this->psllw_s(inst); break;
556  case ID_INS_PSRLDQ: this->psrldq_s(inst); break;
557  case ID_INS_PSUBB: this->psubb_s(inst); break;
558  case ID_INS_PSUBD: this->psubd_s(inst); break;
559  case ID_INS_PSUBQ: this->psubq_s(inst); break;
560  case ID_INS_PSUBW: this->psubw_s(inst); break;
561  case ID_INS_PTEST: this->ptest_s(inst); break;
562  case ID_INS_PUNPCKHBW: this->punpckhbw_s(inst); break;
563  case ID_INS_PUNPCKHDQ: this->punpckhdq_s(inst); break;
564  case ID_INS_PUNPCKHQDQ: this->punpckhqdq_s(inst); break;
565  case ID_INS_PUNPCKHWD: this->punpckhwd_s(inst); break;
566  case ID_INS_PUNPCKLBW: this->punpcklbw_s(inst); break;
567  case ID_INS_PUNPCKLDQ: this->punpckldq_s(inst); break;
568  case ID_INS_PUNPCKLQDQ: this->punpcklqdq_s(inst); break;
569  case ID_INS_PUNPCKLWD: this->punpcklwd_s(inst); break;
570  case ID_INS_PUSH: this->push_s(inst); break;
571  case ID_INS_PUSHAL: this->pushal_s(inst); break;
572  case ID_INS_PUSHFD: this->pushfd_s(inst); break;
573  case ID_INS_PUSHFQ: this->pushfq_s(inst); break;
574  case ID_INS_PXOR: this->pxor_s(inst); break;
575  case ID_INS_RCL: this->rcl_s(inst); break;
576  case ID_INS_RCR: this->rcr_s(inst); break;
577  case ID_INS_RDTSC: this->rdtsc_s(inst); break;
578  case ID_INS_RET: this->ret_s(inst); break;
579  case ID_INS_ROL: this->rol_s(inst); break;
580  case ID_INS_ROR: this->ror_s(inst); break;
581  case ID_INS_RORX: this->rorx_s(inst); break;
582  case ID_INS_SAHF: this->sahf_s(inst); break;
583  case ID_INS_SAL: this->shl_s(inst); break;
584  case ID_INS_SAR: this->sar_s(inst); break;
585  case ID_INS_SARX: this->sarx_s(inst); break;
586  case ID_INS_SBB: this->sbb_s(inst); break;
587  case ID_INS_SCASB: this->scasb_s(inst); break;
588  case ID_INS_SCASD: this->scasd_s(inst); break;
589  case ID_INS_SCASQ: this->scasq_s(inst); break;
590  case ID_INS_SCASW: this->scasw_s(inst); break;
591  case ID_INS_SETA: this->seta_s(inst); break;
592  case ID_INS_SETAE: this->setae_s(inst); break;
593  case ID_INS_SETB: this->setb_s(inst); break;
594  case ID_INS_SETBE: this->setbe_s(inst); break;
595  case ID_INS_SETE: this->sete_s(inst); break;
596  case ID_INS_SETG: this->setg_s(inst); break;
597  case ID_INS_SETGE: this->setge_s(inst); break;
598  case ID_INS_SETL: this->setl_s(inst); break;
599  case ID_INS_SETLE: this->setle_s(inst); break;
600  case ID_INS_SETNE: this->setne_s(inst); break;
601  case ID_INS_SETNO: this->setno_s(inst); break;
602  case ID_INS_SETNP: this->setnp_s(inst); break;
603  case ID_INS_SETNS: this->setns_s(inst); break;
604  case ID_INS_SETO: this->seto_s(inst); break;
605  case ID_INS_SETP: this->setp_s(inst); break;
606  case ID_INS_SETS: this->sets_s(inst); break;
607  case ID_INS_SFENCE: this->sfence_s(inst); break;
608  case ID_INS_SHL: this->shl_s(inst); break;
609  case ID_INS_SHLD: this->shld_s(inst); break;
610  case ID_INS_SHLX: this->shlx_s(inst); break;
611  case ID_INS_SHR: this->shr_s(inst); break;
612  case ID_INS_SHRD: this->shrd_s(inst); break;
613  case ID_INS_SHRX: this->shrx_s(inst); break;
614  case ID_INS_STC: this->stc_s(inst); break;
615  case ID_INS_STD: this->std_s(inst); break;
616  case ID_INS_STI: this->sti_s(inst); break;
617  case ID_INS_STMXCSR: this->stmxcsr_s(inst); break;
618  case ID_INS_STOSB: this->stosb_s(inst); break;
619  case ID_INS_STOSD: this->stosd_s(inst); break;
620  case ID_INS_STOSQ: this->stosq_s(inst); break;
621  case ID_INS_STOSW: this->stosw_s(inst); break;
622  case ID_INS_SUB: this->sub_s(inst); break;
623  case ID_INS_SYSCALL: this->syscall_s(inst); break;
624  case ID_INS_SYSENTER: this->sysenter_s(inst); break;
625  case ID_INS_TEST: this->test_s(inst); break;
626  case ID_INS_TZCNT: this->tzcnt_s(inst); break;
627  case ID_INS_UNPCKHPD: this->unpckhpd_s(inst); break;
628  case ID_INS_UNPCKHPS: this->unpckhps_s(inst); break;
629  case ID_INS_UNPCKLPD: this->unpcklpd_s(inst); break;
630  case ID_INS_UNPCKLPS: this->unpcklps_s(inst); break;
631  case ID_INS_VMOVDQA: this->vmovdqa_s(inst); break;
632  case ID_INS_VMOVDQU: this->vmovdqu_s(inst); break;
633  case ID_INS_VPAND: this->vpand_s(inst); break;
634  case ID_INS_VPANDN: this->vpandn_s(inst); break;
635  case ID_INS_VPMOVMSKB: this->vpmovmskb_s(inst); break;
636  case ID_INS_VPOR: this->vpor_s(inst); break;
637  case ID_INS_VPTEST: this->vptest_s(inst); break;
638  case ID_INS_VPSHUFD: this->vpshufd_s(inst); break;
639  case ID_INS_VPXOR: this->vpxor_s(inst); break;
640  case ID_INS_WAIT: this->wait_s(inst); break;
641  case ID_INS_WBINVD: this->wbinvd_s(inst); break;
642  case ID_INS_XADD: this->xadd_s(inst); break;
643  case ID_INS_XCHG: this->xchg_s(inst); break;
644  case ID_INS_XOR: this->xor_s(inst); break;
645  case ID_INS_XORPD: this->xorpd_s(inst); break;
646  case ID_INS_XORPS: this->xorps_s(inst); break;
647  default:
648  return false;
649  }
650  return true;
651  }
652 
653 
654  triton::uint64 x86Semantics::alignAddStack_s(triton::arch::Instruction& inst, triton::uint32 delta) {
655  auto dst = triton::arch::OperandWrapper(this->architecture->getStackPointer());
656 
657  /* Create symbolic operands */
658  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
659  auto op2 = this->astCtxt->bv(delta, dst.getBitSize());
660 
661  /* Create the semantics */
662  auto node = this->astCtxt->bvadd(op1, op2);
663 
664  /* Create symbolic expression */
665  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "Stack alignment");
666 
667  /* Spread taint */
668  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
669 
670  /* Return the new stack value */
671  return node->evaluate().convert_to<triton::uint64>();
672  }
673 
674 
675  triton::uint64 x86Semantics::alignSubStack_s(triton::arch::Instruction& inst, triton::uint32 delta) {
676  auto dst = triton::arch::OperandWrapper(this->architecture->getStackPointer());
677 
678  /* Create symbolic operands */
679  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
680  auto op2 = this->astCtxt->bv(delta, dst.getBitSize());
681 
682  /* Create the semantics */
683  auto node = this->astCtxt->bvsub(op1, op2);
684 
685  /* Create symbolic expression */
686  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "Stack alignment");
687 
688  /* Spread taint */
689  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
690 
691  /* Return the new stack value */
692  return node->evaluate().convert_to<triton::uint64>();
693  }
694 
695 
696  void x86Semantics::clearFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
697  /* Create the semantics */
698  auto node = this->astCtxt->bv(0, 1);
699 
700  /* Create symbolic expression */
701  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
702 
703  /* Spread taint */
704  expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
705  }
706 
707 
708  void x86Semantics::setFlag_s(triton::arch::Instruction& inst, const triton::arch::Register& flag, std::string comment) {
709  /* Create the semantics */
710  auto node = this->astCtxt->bv(1, 1);
711 
712  /* Create symbolic expression */
713  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
714 
715  /* Spread taint */
716  expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
717  }
718 
719 
720  void x86Semantics::undefined_s(triton::arch::Instruction& inst, const triton::arch::Register& reg) {
721  if (this->modes->isModeEnabled(triton::modes::CONCRETIZE_UNDEFINED_REGISTERS)) {
722  this->symbolicEngine->concretizeRegister(reg);
723  }
724  /* Tell that the instruction defines a register as undefined and untaint */
725  inst.setUndefinedRegister(reg);
726  this->taintEngine->setTaintRegister(reg, triton::engines::taint::UNTAINTED);
727  }
728 
729 
730  void x86Semantics::controlFlow_s(triton::arch::Instruction& inst) {
731  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
732  auto counter = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
733  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
734 
735  switch (inst.getPrefix()) {
736 
738  /* Create symbolic operands */
739  auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
740 
741  /* Create the semantics for Counter */
742  auto node1 = this->astCtxt->ite(
743  this->astCtxt->equal(op1, this->astCtxt->bv(0, counter.getBitSize())),
744  op1,
745  this->astCtxt->bvsub(op1, this->astCtxt->bv(1, counter.getBitSize()))
746  );
747 
748  /* Create the semantics for PC */
749  auto node2 = this->astCtxt->ite(
750  this->astCtxt->equal(node1, this->astCtxt->bv(0, counter.getBitSize())),
751  this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize()),
752  this->astCtxt->bv(inst.getAddress(), pc.getBitSize())
753  );
754 
755  /* Create symbolic expression */
756  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
757  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
758 
759  /* Spread taint for PC */
760  expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
761  expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
762  break;
763  }
764 
766  /* Create symbolic operands */
767  auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
768  auto op2 = this->symbolicEngine->getOperandAst(inst, zf);
769 
770  /* Create the semantics for Counter */
771  auto node1 = this->astCtxt->ite(
772  this->astCtxt->equal(op1, this->astCtxt->bv(0, counter.getBitSize())),
773  op1,
774  this->astCtxt->bvsub(op1, this->astCtxt->bv(1, counter.getBitSize()))
775  );
776 
777  /* Create the semantics for PC */
778  auto node2 = this->astCtxt->ite(
779  this->astCtxt->lor(
780  this->astCtxt->equal(node1, this->astCtxt->bv(0, counter.getBitSize())),
781  this->astCtxt->equal(op2, this->astCtxt->bvfalse())
782  ),
783  this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize()),
784  this->astCtxt->bv(inst.getAddress(), pc.getBitSize())
785  );
786 
787  /* Create symbolic expression */
788  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
789  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
790 
791  /* Spread taint */
792  expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
793  expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
794  break;
795  }
796 
798  /* Create symbolic operands */
799  auto op1 = this->symbolicEngine->getOperandAst(inst, counter);
800  auto op2 = this->symbolicEngine->getOperandAst(inst, zf);
801 
802  /* Create the semantics for Counter */
803  auto node1 = this->astCtxt->ite(
804  this->astCtxt->equal(op1, this->astCtxt->bv(0, counter.getBitSize())),
805  op1,
806  this->astCtxt->bvsub(op1, this->astCtxt->bv(1, counter.getBitSize()))
807  );
808 
809  /* Create the semantics for PC */
810  auto node2 = this->astCtxt->ite(
811  this->astCtxt->lor(
812  this->astCtxt->equal(node1, this->astCtxt->bv(0, counter.getBitSize())),
813  this->astCtxt->equal(op2, this->astCtxt->bvtrue())
814  ),
815  this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize()),
816  this->astCtxt->bv(inst.getAddress(), pc.getBitSize())
817  );
818 
819  /* Create symbolic expression */
820  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, counter, "Counter operation");
821  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
822 
823  /* Spread taint */
824  expr1->isTainted = this->taintEngine->taintUnion(counter, counter);
825  expr2->isTainted = this->taintEngine->taintAssignment(pc, counter);
826  break;
827  }
828 
829  default: {
830  /* Create the semantics */
831  auto node = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
832 
833  /* Create symbolic expression */
834  auto expr = this->symbolicEngine->createSymbolicRegisterExpression(inst, node, this->architecture->getProgramCounter(), "Program Counter");
835 
836  /* Spread taint */
837  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getProgramCounter(), triton::engines::taint::UNTAINTED);
838  break;
839  }
840  }
841  }
842 
843 
844  void x86Semantics::af_s(triton::arch::Instruction& inst,
849  bool vol) {
850 
851  auto bvSize = dst.getBitSize();
852  auto low = vol ? 0 : dst.getLow();
853  auto high = vol ? bvSize-1 : dst.getHigh();
854 
855  /*
856  * Create the semantic.
857  * af = 0x10 == (0x10 & (regDst ^ op1 ^ op2))
858  */
859  auto node = this->astCtxt->ite(
860  this->astCtxt->equal(
861  this->astCtxt->bv(0x10, bvSize),
862  this->astCtxt->bvand(
863  this->astCtxt->bv(0x10, bvSize),
864  this->astCtxt->bvxor(
865  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
866  this->astCtxt->bvxor(op1, op2)
867  )
868  )
869  ),
870  this->astCtxt->bv(1, 1),
871  this->astCtxt->bv(0, 1)
872  );
873 
874  /* Create the symbolic expression */
875  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_AF), "Adjust flag");
876 
877  /* Spread the taint from the parent to the child */
878  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_AF), parent->isTainted);
879  }
880 
881 
882  void x86Semantics::afAaa_s(triton::arch::Instruction& inst,
887  bool vol) {
888 
889  auto bvSize = dst.getBitSize();
890 
891  /*
892  * Create the semantic.
893  * af = 1 if ((AL AND 0FH) > 9) or (AF = 1) then 0
894  */
895  auto node = this->astCtxt->ite(
896  this->astCtxt->lor(
897  this->astCtxt->bvugt(
898  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, bvSize)),
899  this->astCtxt->bv(9, bvSize)
900  ),
901  this->astCtxt->equal(op3, this->astCtxt->bvtrue())
902  ),
903  this->astCtxt->bv(1, 1),
904  this->astCtxt->bv(0, 1)
905  );
906 
907  /* Create the symbolic expression */
908  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_AF), "Adjust flag");
909 
910  /* Spread the taint from the parent to the child */
911  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_AF), parent->isTainted);
912  }
913 
914 
915  void x86Semantics::afNeg_s(triton::arch::Instruction& inst,
919  bool vol) {
920 
921  auto bvSize = dst.getBitSize();
922  auto low = vol ? 0 : dst.getLow();
923  auto high = vol ? bvSize-1 : dst.getHigh();
924 
925  /*
926  * Create the semantic.
927  * af = 0x10 == (0x10 & (op1 ^ regDst))
928  */
929  auto node = this->astCtxt->ite(
930  this->astCtxt->equal(
931  this->astCtxt->bv(0x10, bvSize),
932  this->astCtxt->bvand(
933  this->astCtxt->bv(0x10, bvSize),
934  this->astCtxt->bvxor(
935  op1,
936  this->astCtxt->extract(high, low, this->astCtxt->reference(parent))
937  )
938  )
939  ),
940  this->astCtxt->bv(1, 1),
941  this->astCtxt->bv(0, 1)
942  );
943 
944  /* Create the symbolic expression */
945  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_AF), "Adjust flag");
946 
947  /* Spread the taint from the parent to the child */
948  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_AF), parent->isTainted);
949  }
950 
951 
952  void x86Semantics::cfAaa_s(triton::arch::Instruction& inst,
957  bool vol) {
958 
959  auto bvSize = dst.getBitSize();
960 
961  /*
962  * Create the semantic.
963  * cf = 1 if ((AL AND 0FH) > 9) or (AF = 1) then 0
964  */
965  auto node = this->astCtxt->ite(
966  this->astCtxt->lor(
967  this->astCtxt->bvugt(
968  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, bvSize)),
969  this->astCtxt->bv(9, bvSize)
970  ),
971  this->astCtxt->equal(op3, this->astCtxt->bvtrue())
972  ),
973  this->astCtxt->bv(1, 1),
974  this->astCtxt->bv(0, 1)
975  );
976 
977  /* Create the symbolic expression */
978  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
979 
980  /* Spread the taint from the parent to the child */
981  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
982  }
983 
984 
985  void x86Semantics::cfAdd_s(triton::arch::Instruction& inst,
990  bool vol) {
991 
992  auto bvSize = dst.getBitSize();
993  auto low = vol ? 0 : dst.getLow();
994  auto high = vol ? bvSize-1 : dst.getHigh();
995 
996  /*
997  * Create the semantic.
998  * cf = MSB((op1 & op2) ^ ((op1 ^ op2 ^ parent) & (op1 ^ op2)));
999  */
1000  auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
1001  this->astCtxt->bvxor(
1002  this->astCtxt->bvand(op1, op2),
1003  this->astCtxt->bvand(
1004  this->astCtxt->bvxor(
1005  this->astCtxt->bvxor(op1, op2),
1006  this->astCtxt->extract(high, low, this->astCtxt->reference(parent))
1007  ),
1008  this->astCtxt->bvxor(op1, op2))
1009  )
1010  );
1011 
1012  /* Create the symbolic expression */
1013  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1014 
1015  /* Spread the taint from the parent to the child */
1016  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1017  }
1018 
1019 
1020  void x86Semantics::cfBlsi_s(triton::arch::Instruction& inst,
1024  bool vol) {
1025 
1026  /*
1027  * Create the semantic.
1028  * cf = 0 if op1 == 0 else 1
1029  */
1030  auto node = this->astCtxt->ite(
1031  this->astCtxt->equal(
1032  op1,
1033  this->astCtxt->bv(0, dst.getBitSize())
1034  ),
1035  this->astCtxt->bv(0, 1),
1036  this->astCtxt->bv(1, 1)
1037  );
1038 
1039  /* Create the symbolic expression */
1040  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1041 
1042  /* Spread the taint from the parent to the child */
1043  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1044  }
1045 
1046 
1047  void x86Semantics::cfBlsmsk_s(triton::arch::Instruction& inst,
1051  bool vol) {
1052 
1053  /*
1054  * Create the semantic.
1055  * cf = 1 if op1 == 0 else 0
1056  */
1057  auto node = this->astCtxt->ite(
1058  this->astCtxt->equal(
1059  op1,
1060  this->astCtxt->bv(0, dst.getBitSize())
1061  ),
1062  this->astCtxt->bv(1, 1),
1063  this->astCtxt->bv(0, 1)
1064  );
1065 
1066  /* Create the symbolic expression */
1067  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1068 
1069  /* Spread the taint from the parent to the child */
1070  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1071  }
1072 
1073 
1074  void x86Semantics::cfBlsr_s(triton::arch::Instruction& inst,
1078  bool vol) {
1079 
1080  /*
1081  * Create the semantic.
1082  * cf = 1 if op1 == 0 else 0
1083  */
1084  auto node = this->astCtxt->ite(
1085  this->astCtxt->equal(
1086  op1,
1087  this->astCtxt->bv(0, dst.getBitSize())
1088  ),
1089  this->astCtxt->bv(1, 1),
1090  this->astCtxt->bv(0, 1)
1091  );
1092 
1093  /* Create the symbolic expression */
1094  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1095 
1096  /* Spread the taint from the parent to the child */
1097  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1098  }
1099 
1100 
1101  void x86Semantics::cfImul_s(triton::arch::Instruction& inst,
1106  bool vol) {
1107 
1108  /*
1109  * Create the semantic.
1110  * cf = 0 if sx(dst) == node else 1
1111  */
1112  auto node = this->astCtxt->ite(
1113  this->astCtxt->equal(
1114  this->astCtxt->sx(dst.getBitSize(), op1),
1115  res
1116  ),
1117  this->astCtxt->bv(0, 1),
1118  this->astCtxt->bv(1, 1)
1119  );
1120 
1121  /* Create the symbolic expression */
1122  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1123 
1124  /* Spread the taint from the parent to the child */
1125  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1126  }
1127 
1128 
1129  void x86Semantics::cfMul_s(triton::arch::Instruction& inst,
1133  bool vol) {
1134 
1135  /*
1136  * Create the semantic.
1137  * cf = 0 if op1 == 0 else 1
1138  */
1139  auto node = this->astCtxt->ite(
1140  this->astCtxt->equal(
1141  op1,
1142  this->astCtxt->bv(0, dst.getBitSize())
1143  ),
1144  this->astCtxt->bv(0, 1),
1145  this->astCtxt->bv(1, 1)
1146  );
1147 
1148  /* Create the symbolic expression */
1149  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1150 
1151  /* Spread the taint from the parent to the child */
1152  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1153  }
1154 
1155 
1156  void x86Semantics::cfNeg_s(triton::arch::Instruction& inst,
1160  bool vol) {
1161 
1162  /*
1163  * Create the semantic.
1164  * cf = 0 if op1 == 0 else 1
1165  */
1166  auto node = this->astCtxt->ite(
1167  this->astCtxt->equal(
1168  op1,
1169  this->astCtxt->bv(0, dst.getBitSize())
1170  ),
1171  this->astCtxt->bv(0, 1),
1172  this->astCtxt->bv(1, 1)
1173  );
1174 
1175  /* Create the symbolic expression */
1176  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1177 
1178  /* Spread the taint from the parent to the child */
1179  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1180  }
1181 
1182 
1183  void x86Semantics::cfPtest_s(triton::arch::Instruction& inst,
1186  bool vol) {
1187 
1188  auto bvSize = dst.getBitSize();
1189  auto low = vol ? 0 : dst.getLow();
1190  auto high = vol ? bvSize-1 : dst.getHigh();
1191 
1192  /*
1193  * Create the semantic.
1194  * cf = 0 == regDst
1195  */
1196  auto node = this->astCtxt->ite(
1197  this->astCtxt->equal(
1198  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
1199  this->astCtxt->bv(0, bvSize)
1200  ),
1201  this->astCtxt->bv(1, 1),
1202  this->astCtxt->bv(0, 1)
1203  );
1204 
1205  /* Create the symbolic expression */
1206  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1207 
1208  /* Spread the taint from the parent to the child */
1209  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1210  }
1211 
1212 
1213  void x86Semantics::cfRcl_s(triton::arch::Instruction& inst,
1215  const triton::ast::SharedAbstractNode& result,
1217  bool vol) {
1218 
1219  auto bvSize = op2->getBitvectorSize();
1220  auto high = result->getBitvectorSize() - 1;
1221  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1222 
1223  auto node = this->astCtxt->ite(
1224  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1225  this->symbolicEngine->getOperandAst(cf),
1226  this->astCtxt->extract(high, high, result)
1227  );
1228 
1229  /* Create the symbolic expression */
1230  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1231 
1232  if (op2->evaluate()) {
1233  /* Spread the taint from the parent to the child */
1234  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1235  }
1236  else {
1237  inst.removeWrittenRegister(cf.getConstRegister());
1238  }
1239  }
1240 
1241 
1242  void x86Semantics::cfRcr_s(triton::arch::Instruction& inst,
1245  const triton::ast::SharedAbstractNode& result,
1247  bool vol) {
1248 
1249  auto bvSize = op2->getBitvectorSize();
1250  auto high = result->getBitvectorSize() - 1;
1251  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1252 
1253  auto node = this->astCtxt->ite(
1254  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1255  this->symbolicEngine->getOperandAst(cf),
1256  this->astCtxt->extract(high, high, result) /* yes it's should be LSB, but here it's a trick :-) */
1257  );
1258 
1259  /* Create the symbolic expression */
1260  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1261 
1262  if (op2->evaluate()) {
1263  /* Spread the taint from the parent to the child */
1264  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1265  }
1266  else {
1267  inst.removeWrittenRegister(cf.getConstRegister());
1268  }
1269  }
1270 
1271 
1272  void x86Semantics::cfRol_s(triton::arch::Instruction& inst,
1276  bool vol) {
1277 
1278  auto bvSize = op2->getBitvectorSize();
1279  auto low = vol ? 0 : dst.getLow();
1280  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1281 
1282  auto node = this->astCtxt->ite(
1283  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1284  this->symbolicEngine->getOperandAst(cf),
1285  this->astCtxt->extract(low, low, this->astCtxt->reference(parent))
1286  );
1287 
1288  /* Create the symbolic expression */
1289  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1290 
1291  if (op2->evaluate()) {
1292  /* Spread the taint from the parent to the child */
1293  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1294  }
1295  else {
1296  inst.removeWrittenRegister(cf.getConstRegister());
1297  }
1298  }
1299 
1300 
1301  void x86Semantics::cfRor_s(triton::arch::Instruction& inst,
1305  bool vol) {
1306 
1307  auto bvSize = op2->getBitvectorSize();
1308  auto high = vol ? bvSize-1 : dst.getHigh();
1309  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1310 
1311  auto node = this->astCtxt->ite(
1312  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1313  this->symbolicEngine->getOperandAst(cf),
1314  this->astCtxt->extract(high, high, this->astCtxt->reference(parent))
1315  );
1316 
1317  /* Create the symbolic expression */
1318  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1319 
1320  if (op2->evaluate()) {
1321  /* Spread the taint from the parent to the child */
1322  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1323  }
1324  else {
1325  inst.removeWrittenRegister(cf.getConstRegister());
1326  }
1327  }
1328 
1329 
1330  void x86Semantics::cfSar_s(triton::arch::Instruction& inst,
1335  bool vol) {
1336 
1337  auto bvSize = dst.getBitSize();
1338  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1339 
1340  /*
1341  * Create the semantic.
1342  * if op2 != 0:
1343  * if op2 > bvSize:
1344  * cf.id = ((op1 >> (bvSize - 1)) & 1)
1345  * else:
1346  * cf.id = ((op1 >> (op2 - 1)) & 1)
1347  */
1348  auto node = this->astCtxt->ite(
1349  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1350  this->symbolicEngine->getOperandAst(cf),
1351  this->astCtxt->ite(
1352  this->astCtxt->bvugt(op2, this->astCtxt->bv(bvSize, bvSize)),
1353  this->astCtxt->extract(0, 0, this->astCtxt->bvlshr(op1, this->astCtxt->bvsub(this->astCtxt->bv(bvSize, bvSize), this->astCtxt->bv(1, bvSize)))),
1354  this->astCtxt->extract(0, 0, this->astCtxt->bvlshr(op1, this->astCtxt->bvsub(op2, this->astCtxt->bv(1, bvSize))))
1355  )
1356  );
1357 
1358  /* Create the symbolic expression */
1359  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1360 
1361  if (op2->evaluate()) {
1362  /* Spread the taint from the parent to the child */
1363  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1364  }
1365  else {
1366  inst.removeWrittenRegister(cf.getConstRegister());
1367  }
1368  }
1369 
1370 
1371  void x86Semantics::cfShl_s(triton::arch::Instruction& inst,
1376  bool vol) {
1377 
1378  auto bvSize = dst.getBitSize();
1379  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1380 
1381  /*
1382  * Create the semantic.
1383  * cf = (op1 >> ((bvSize - op2) & 1) if op2 != 0
1384  */
1385  auto node = this->astCtxt->ite(
1386  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1387  this->symbolicEngine->getOperandAst(cf),
1388  this->astCtxt->extract(0, 0,
1389  this->astCtxt->bvlshr(
1390  op1,
1391  this->astCtxt->bvsub(
1392  this->astCtxt->bv(bvSize, bvSize),
1393  op2
1394  )
1395  )
1396  )
1397  );
1398 
1399  /* Create the symbolic expression */
1400  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1401 
1402  if (op2->evaluate()) {
1403  /* Spread the taint from the parent to the child */
1404  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1405  }
1406  else {
1407  inst.removeWrittenRegister(cf.getConstRegister());
1408  }
1409  }
1410 
1411 
1412  void x86Semantics::cfShld_s(triton::arch::Instruction& inst,
1418  bool vol) {
1419 
1420  auto bv1Size = op1->getBitvectorSize();
1421  auto bv2Size = op2->getBitvectorSize();
1422  auto bv3Size = op3->getBitvectorSize();
1423  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1424 
1425  /*
1426  * Create the semantic.
1427  * cf = MSB(rol(op3, concat(op2,op1))) if op3 != 0
1428  */
1429  auto node = this->astCtxt->ite(
1430  this->astCtxt->equal(op3, this->astCtxt->bv(0, bv3Size)),
1431  this->symbolicEngine->getOperandAst(cf),
1432  this->astCtxt->extract(
1433  dst.getBitSize(), dst.getBitSize(),
1434  this->astCtxt->bvrol(
1435  this->astCtxt->concat(op2, op1),
1436  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
1437  )
1438  )
1439  );
1440 
1441  /* Create the symbolic expression */
1442  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1443 
1444  if (op3->evaluate()) {
1445  /* Spread the taint from the parent to the child */
1446  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1447  }
1448  else {
1449  inst.removeWrittenRegister(cf.getConstRegister());
1450  }
1451  }
1452 
1453 
1454  void x86Semantics::cfShr_s(triton::arch::Instruction& inst,
1459  bool vol) {
1460 
1461  auto bvSize = dst.getBitSize();
1462  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1463 
1464  /*
1465  * Create the semantic.
1466  * cf = ((op1 >> (op2 - 1)) & 1) if op2 != 0
1467  */
1468  auto node = this->astCtxt->ite(
1469  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
1470  this->symbolicEngine->getOperandAst(cf),
1471  this->astCtxt->extract(0, 0,
1472  this->astCtxt->bvlshr(
1473  op1,
1474  this->astCtxt->bvsub(
1475  op2,
1476  this->astCtxt->bv(1, bvSize))
1477  )
1478  )
1479  );
1480 
1481  /* Create the symbolic expression */
1482  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1483 
1484  if (op2->evaluate()) {
1485  /* Spread the taint from the parent to the child */
1486  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1487  }
1488  else {
1489  inst.removeWrittenRegister(cf.getConstRegister());
1490  }
1491  }
1492 
1493 
1494  void x86Semantics::cfShrd_s(triton::arch::Instruction& inst,
1500  bool vol) {
1501 
1502  auto bvSize = dst.getBitSize();
1503  auto bv1Size = op1->getBitvectorSize();
1504  auto bv2Size = op2->getBitvectorSize();
1505  auto bv3Size = op3->getBitvectorSize();
1506  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1507 
1508  /*
1509  * Create the semantic.
1510  * cf = MSB(ror(op3, concat(op2,op1))) if op3 != 0
1511  */
1512  auto node = this->astCtxt->ite(
1513  this->astCtxt->equal(op3, this->astCtxt->bv(0, bv3Size)),
1514  this->symbolicEngine->getOperandAst(cf),
1515  this->astCtxt->extract(
1516  (bvSize * 2) - 1, (bvSize * 2) - 1,
1517  this->astCtxt->bvror(
1518  this->astCtxt->concat(op2, op1),
1519  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
1520  )
1521  )
1522  );
1523 
1524  /* Create the symbolic expression */
1525  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1526 
1527  if (op3->evaluate()) {
1528  /* Spread the taint from the parent to the child */
1529  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1530  }
1531  else {
1532  inst.removeWrittenRegister(cf.getConstRegister());
1533  }
1534  }
1535 
1536 
1537  void x86Semantics::cfSub_s(triton::arch::Instruction& inst,
1542  bool vol) {
1543 
1544  auto bvSize = dst.getBitSize();
1545  auto low = vol ? 0 : dst.getLow();
1546  auto high = vol ? bvSize-1 : dst.getHigh();
1547 
1548  /*
1549  * Create the semantic.
1550  * cf = extract(bvSize, bvSize (((op1 ^ op2 ^ res) ^ ((op1 ^ res) & (op1 ^ op2)))))
1551  */
1552  auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
1553  this->astCtxt->bvxor(
1554  this->astCtxt->bvxor(op1, this->astCtxt->bvxor(op2, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))),
1555  this->astCtxt->bvand(
1556  this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent))),
1557  this->astCtxt->bvxor(op1, op2)
1558  )
1559  )
1560  );
1561 
1562  /* Create the symbolic expression */
1563  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1564 
1565  /* Spread the taint from the parent to the child */
1566  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1567  }
1568 
1569 
1570  void x86Semantics::ofAdd_s(triton::arch::Instruction& inst,
1575  bool vol) {
1576 
1577  auto bvSize = dst.getBitSize();
1578  auto low = vol ? 0 : dst.getLow();
1579  auto high = vol ? bvSize-1 : dst.getHigh();
1580 
1581  /*
1582  * Create the semantic.
1583  * of = MSB((op1 ^ ~op2) & (op1 ^ regDst))
1584  */
1585  auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
1586  this->astCtxt->bvand(
1587  this->astCtxt->bvxor(op1, this->astCtxt->bvnot(op2)),
1588  this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))
1589  )
1590  );
1591 
1592  /* Create the symbolic expression */
1593  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1594 
1595  /* Spread the taint from the parent to the child */
1596  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1597  }
1598 
1599 
1600  void x86Semantics::ofImul_s(triton::arch::Instruction& inst,
1605  bool vol) {
1606  /*
1607  * Create the semantic.
1608  * of = 0 if sx(dst) == node else 1
1609  */
1610  auto node = this->astCtxt->ite(
1611  this->astCtxt->equal(
1612  this->astCtxt->sx(dst.getBitSize(), op1),
1613  res
1614  ),
1615  this->astCtxt->bv(0, 1),
1616  this->astCtxt->bv(1, 1)
1617  );
1618 
1619  /* Create the symbolic expression */
1620  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1621 
1622  /* Spread the taint from the parent to the child */
1623  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1624  }
1625 
1626 
1627  void x86Semantics::ofMul_s(triton::arch::Instruction& inst,
1631  bool vol) {
1632 
1633  /*
1634  * Create the semantic.
1635  * of = 0 if up == 0 else 1
1636  */
1637  auto node = this->astCtxt->ite(
1638  this->astCtxt->equal(
1639  op1,
1640  this->astCtxt->bv(0, dst.getBitSize())
1641  ),
1642  this->astCtxt->bv(0, 1),
1643  this->astCtxt->bv(1, 1)
1644  );
1645 
1646  /* Create the symbolic expression */
1647  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1648 
1649  /* Spread the taint from the parent to the child */
1650  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1651  }
1652 
1653 
1654  void x86Semantics::ofNeg_s(triton::arch::Instruction& inst,
1658  bool vol) {
1659 
1660  auto bvSize = dst.getBitSize();
1661  auto low = vol ? 0 : dst.getLow();
1662  auto high = vol ? bvSize-1 : dst.getHigh();
1663 
1664  /*
1665  * Create the semantic.
1666  * of = (res & op1) >> (bvSize - 1) & 1
1667  */
1668  auto node = this->astCtxt->extract(0, 0,
1669  this->astCtxt->bvlshr(
1670  this->astCtxt->bvand(this->astCtxt->extract(high, low, this->astCtxt->reference(parent)), op1),
1671  this->astCtxt->bvsub(this->astCtxt->bv(bvSize, bvSize), this->astCtxt->bv(1, bvSize))
1672  )
1673  );
1674 
1675  /* Create the symbolic expression */
1676  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1677 
1678  /* Spread the taint from the parent to the child */
1679  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1680  }
1681 
1682 
1683  void x86Semantics::ofRol_s(triton::arch::Instruction& inst,
1687  bool vol) {
1688 
1689  auto bvSize = dst.getBitSize();
1690  auto high = vol ? bvSize-1 : dst.getHigh();
1691  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1692  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1693 
1694  auto node = this->astCtxt->ite(
1695  this->astCtxt->equal(this->astCtxt->zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt->bv(1, bvSize)),
1696  this->astCtxt->bvxor(
1697  this->astCtxt->extract(high, high, this->astCtxt->reference(parent)),
1698  this->symbolicEngine->getOperandAst(inst, cf)
1699  ),
1700  this->symbolicEngine->getOperandAst(of)
1701  );
1702 
1703  /* Create the symbolic expression */
1704  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1705 
1706  if (op2->evaluate()) {
1707  /* Spread the taint from the parent to the child */
1708  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1709  }
1710  else {
1711  inst.removeReadRegister(cf.getConstRegister());
1713  }
1714  }
1715 
1716 
1717  void x86Semantics::ofRor_s(triton::arch::Instruction& inst,
1721  bool vol) {
1722 
1723  auto bvSize = op2->getBitvectorSize();
1724  auto high = vol ? bvSize-1 : dst.getHigh();
1725  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1726 
1727  auto node = this->astCtxt->ite(
1728  this->astCtxt->equal(op2, this->astCtxt->bv(1, bvSize)),
1729  this->astCtxt->bvxor(
1730  this->astCtxt->extract(high, high, this->astCtxt->reference(parent)),
1731  this->astCtxt->extract(high-1, high-1, this->astCtxt->reference(parent))
1732  ),
1733  this->symbolicEngine->getOperandAst(of)
1734  );
1735 
1736  /* Create the symbolic expression */
1737  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1738 
1739  if (op2->evaluate()) {
1740  /* Spread the taint from the parent to the child */
1741  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1742  }
1743  else {
1745  }
1746  }
1747 
1748 
1749  void x86Semantics::ofRcr_s(triton::arch::Instruction& inst,
1754  bool vol) {
1755 
1756  auto bvSize = op2->getBitvectorSize();
1757  auto high = dst.getBitSize()-1;
1758  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1759  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1760 
1761  auto node = this->astCtxt->ite(
1762  this->astCtxt->equal(op2, this->astCtxt->bv(1, bvSize)),
1763  this->astCtxt->bvxor(
1764  this->astCtxt->extract(high, high, op1),
1765  this->symbolicEngine->getOperandAst(inst, cf)
1766  ),
1767  this->symbolicEngine->getOperandAst(of)
1768  );
1769 
1770  /* Create the symbolic expression */
1771  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1772 
1773  if (op2->evaluate()) {
1774  /* Spread the taint from the parent to the child */
1775  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1776  }
1777  else {
1778  inst.removeReadRegister(cf.getConstRegister());
1780  }
1781  }
1782 
1783 
1784  void x86Semantics::ofSar_s(triton::arch::Instruction& inst,
1788  bool vol) {
1789 
1790  auto bvSize = dst.getBitSize();
1791  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1792 
1793  /*
1794  * Create the semantic.
1795  * of = 0 if op2 == 1
1796  */
1797  auto node = this->astCtxt->ite(
1798  this->astCtxt->land(
1799  this->astCtxt->equal(
1800  /* #672 */
1801  this->astCtxt->reference(parent),
1802  this->astCtxt->reference(parent)
1803  /* ---- */
1804  ),
1805  this->astCtxt->equal(
1806  op2,
1807  this->astCtxt->bv(1, bvSize)
1808  )
1809  ),
1810  this->astCtxt->bv(0, 1),
1811  this->symbolicEngine->getOperandAst(of)
1812  );
1813 
1814  /* Create the symbolic expression */
1815  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1816 
1817  if (op2->evaluate()) {
1818  /* Spread the taint from the parent to the child */
1819  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1820  }
1821  else {
1823  }
1824  }
1825 
1826 
1827  void x86Semantics::ofShl_s(triton::arch::Instruction& inst,
1832  bool vol) {
1833 
1834  auto bvSize = dst.getBitSize();
1835  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1836 
1837  /*
1838  * Create the semantic.
1839  * of = ((op1 >> (bvSize - 1)) ^ (op1 >> (bvSize - 2))) & 1; if op2 == 1
1840  */
1841  auto node = this->astCtxt->ite(
1842  this->astCtxt->equal(
1843  op2,
1844  this->astCtxt->bv(1, bvSize)),
1845  this->astCtxt->extract(0, 0,
1846  this->astCtxt->bvxor(
1847  this->astCtxt->bvlshr(op1, this->astCtxt->bvsub(this->astCtxt->bv(bvSize, bvSize), this->astCtxt->bv(1, bvSize))),
1848  this->astCtxt->bvlshr(op1, this->astCtxt->bvsub(this->astCtxt->bv(bvSize, bvSize), this->astCtxt->bv(2, bvSize)))
1849  )
1850  ),
1851  this->symbolicEngine->getOperandAst(of)
1852  );
1853 
1854  /* Create the symbolic expression */
1855  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1856 
1857  if (op2->evaluate()) {
1858  /* Spread the taint from the parent to the child */
1859  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1860  }
1861  else {
1863  }
1864  }
1865 
1866 
1867  void x86Semantics::ofShld_s(triton::arch::Instruction& inst,
1873  bool vol) {
1874 
1875  auto bvSize = dst.getBitSize();
1876  auto bv1Size = op1->getBitvectorSize();
1877  auto bv2Size = op2->getBitvectorSize();
1878  auto bv3Size = op3->getBitvectorSize();
1879  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1880 
1881  /*
1882  * Create the semantic.
1883  * of = MSB(rol(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
1884  */
1885  auto node = this->astCtxt->ite(
1886  this->astCtxt->equal(
1887  this->astCtxt->zx(bvSize - bv3Size, op3),
1888  this->astCtxt->bv(1, bvSize)),
1889  this->astCtxt->bvxor(
1890  this->astCtxt->extract(
1891  bvSize-1, bvSize-1,
1892  this->astCtxt->bvrol(
1893  this->astCtxt->concat(op2, op1),
1894  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
1895  )
1896  ),
1897  this->astCtxt->extract(bvSize-1, bvSize-1, op1)
1898  ),
1899  this->symbolicEngine->getOperandAst(of)
1900  );
1901 
1902  /* Create the symbolic expression */
1903  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1904 
1905  if (op3->evaluate()) {
1906  /* Spread the taint from the parent to the child */
1907  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1908  }
1909  else {
1911  }
1912  }
1913 
1914 
1915  void x86Semantics::ofShr_s(triton::arch::Instruction& inst,
1920  bool vol) {
1921 
1922  auto bvSize = dst.getBitSize();
1923  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1924 
1925  /*
1926  * Create the semantic.
1927  * of = ((op1 >> (bvSize - 1)) & 1) if op2 == 1
1928  */
1929  auto node = this->astCtxt->ite(
1930  this->astCtxt->equal(
1931  op2,
1932  this->astCtxt->bv(1, bvSize)),
1933  this->astCtxt->extract(0, 0, this->astCtxt->bvlshr(op1, this->astCtxt->bvsub(this->astCtxt->bv(bvSize, bvSize), this->astCtxt->bv(1, bvSize)))),
1934  this->symbolicEngine->getOperandAst(of)
1935  );
1936 
1937  /* Create the symbolic expression */
1938  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1939 
1940  if (op2->evaluate()) {
1941  /* Spread the taint from the parent to the child */
1942  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1943  }
1944  else {
1946  }
1947  }
1948 
1949 
1950  void x86Semantics::ofShrd_s(triton::arch::Instruction& inst,
1956  bool vol) {
1957 
1958  auto bvSize = dst.getBitSize();
1959  auto bv1Size = op1->getBitvectorSize();
1960  auto bv2Size = op2->getBitvectorSize();
1961  auto bv3Size = op3->getBitvectorSize();
1962  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1963 
1964  /*
1965  * Create the semantic.
1966  * of = MSB(ror(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
1967  */
1968  auto node = this->astCtxt->ite(
1969  this->astCtxt->equal(
1970  this->astCtxt->zx(bvSize - op3->getBitvectorSize(), op3),
1971  this->astCtxt->bv(1, bvSize)),
1972  this->astCtxt->bvxor(
1973  this->astCtxt->extract(
1974  bvSize - 1, bvSize - 1,
1975  this->astCtxt->bvror(
1976  this->astCtxt->concat(op2, op1),
1977  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
1978  )
1979  ),
1980  this->astCtxt->extract(dst.getBitSize()-1, dst.getBitSize()-1, op1)
1981  ),
1982  this->symbolicEngine->getOperandAst(of)
1983  );
1984 
1985  /* Create the symbolic expression */
1986  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1987 
1988  if (op3->evaluate()) {
1989  /* Spread the taint from the parent to the child */
1990  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1991  }
1992  else {
1994  }
1995  }
1996 
1997 
1998  void x86Semantics::ofSub_s(triton::arch::Instruction& inst,
2003  bool vol) {
2004 
2005  auto bvSize = dst.getBitSize();
2006  auto low = vol ? 0 : dst.getLow();
2007  auto high = vol ? bvSize-1 : dst.getHigh();
2008 
2009  /*
2010  * Create the semantic.
2011  * of = high:bool((op1 ^ op2) & (op1 ^ regDst))
2012  */
2013  auto node = this->astCtxt->extract(bvSize-1, bvSize-1,
2014  this->astCtxt->bvand(
2015  this->astCtxt->bvxor(op1, op2),
2016  this->astCtxt->bvxor(op1, this->astCtxt->extract(high, low, this->astCtxt->reference(parent)))
2017  )
2018  );
2019 
2020  /* Create the symbolic expression */
2021  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
2022 
2023  /* Spread the taint from the parent to the child */
2024  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
2025  }
2026 
2027 
2028  void x86Semantics::pf_s(triton::arch::Instruction& inst,
2031  bool vol) {
2032 
2033  auto low = vol ? 0 : dst.getLow();
2034  auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
2035 
2036  /*
2037  * Create the semantics.
2038  *
2039  * pf is set to one if there is an even number of bit set to 1 in the least
2040  * significant byte of the result.
2041  */
2042  auto node = this->astCtxt->bv(1, 1);
2043  for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
2044  node = this->astCtxt->bvxor(
2045  node,
2046  this->astCtxt->extract(0, 0,
2047  this->astCtxt->bvlshr(
2048  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
2049  this->astCtxt->bv(counter, BYTE_SIZE_BIT)
2050  )
2051  )
2052  );
2053  }
2054 
2055  /* Create the symbolic expression */
2056  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_PF), "Parity flag");
2057 
2058  /* Spread the taint from the parent to the child */
2059  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_PF), parent->isTainted);
2060  }
2061 
2062 
2063  void x86Semantics::pfShl_s(triton::arch::Instruction& inst,
2067  bool vol) {
2068 
2069  auto bvSize = dst.getBitSize();
2070  auto low = vol ? 0 : dst.getLow();
2071  auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
2072  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
2073 
2074  /*
2075  * Create the semantics.
2076  * pf if op2 != 0
2077  */
2078  auto node1 = this->astCtxt->bv(1, 1);
2079  for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
2080  node1 = this->astCtxt->bvxor(
2081  node1,
2082  this->astCtxt->extract(0, 0,
2083  this->astCtxt->bvlshr(
2084  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
2085  this->astCtxt->bv(counter, BYTE_SIZE_BIT)
2086  )
2087  )
2088  );
2089  }
2090 
2091  auto node2 = this->astCtxt->ite(
2092  this->astCtxt->equal(this->astCtxt->zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt->bv(0, bvSize)),
2093  this->symbolicEngine->getOperandAst(pf),
2094  node1
2095  );
2096 
2097  /* Create the symbolic expression */
2098  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node2, pf.getConstRegister(), "Parity flag");
2099 
2100  if (op2->evaluate()) {
2101  /* Spread the taint from the parent to the child */
2102  expr->isTainted = this->taintEngine->setTaintRegister(pf.getConstRegister(), parent->isTainted);
2103  }
2104  else {
2105  inst.removeWrittenRegister(pf.getConstRegister());
2106  }
2107  }
2108 
2109 
2110  void x86Semantics::sf_s(triton::arch::Instruction& inst,
2113  bool vol) {
2114 
2115  auto bvSize = dst.getBitSize();
2116  auto high = vol ? bvSize-1 : dst.getHigh();
2117 
2118  /*
2119  * Create the semantic.
2120  * sf = high:bool(regDst)
2121  */
2122  auto node = this->astCtxt->extract(high, high, this->astCtxt->reference(parent));
2123 
2124  /* Create the symbolic expression */
2125  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_SF), "Sign flag");
2126 
2127  /* Spread the taint from the parent to the child */
2128  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_SF), parent->isTainted);
2129  }
2130 
2131 
2132  void x86Semantics::sfShl_s(triton::arch::Instruction& inst,
2136  bool vol) {
2137 
2138  auto bvSize = dst.getBitSize();
2139  auto high = vol ? bvSize-1 : dst.getHigh();
2140  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2141 
2142  /*
2143  * Create the semantic.
2144  * sf if op2 != 0
2145  */
2146  auto node = this->astCtxt->ite(
2147  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize)),
2148  this->symbolicEngine->getOperandAst(sf),
2149  this->astCtxt->extract(high, high, this->astCtxt->reference(parent))
2150  );
2151 
2152  /* Create the symbolic expression */
2153  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2154 
2155  if (op2->evaluate()) {
2156  /* Spread the taint from the parent to the child */
2157  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2158  }
2159  else {
2160  inst.removeWrittenRegister(sf.getConstRegister());
2161  }
2162  }
2163 
2164 
2165  void x86Semantics::sfShld_s(triton::arch::Instruction& inst,
2171  bool vol) {
2172 
2173  auto bvSize = dst.getBitSize();
2174  auto bv1Size = op1->getBitvectorSize();
2175  auto bv2Size = op2->getBitvectorSize();
2176  auto bv3Size = op3->getBitvectorSize();
2177  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2178 
2179  /*
2180  * Create the semantic.
2181  * MSB(rol(op3, concat(op2,op1))) if op3 != 0
2182  */
2183  auto node = this->astCtxt->ite(
2184  this->astCtxt->equal(op3, this->astCtxt->bv(0, bv3Size)),
2185  this->symbolicEngine->getOperandAst(sf),
2186  this->astCtxt->extract(
2187  bvSize-1, bvSize-1,
2188  this->astCtxt->bvrol(
2189  this->astCtxt->concat(op2, op1),
2190  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
2191  )
2192  )
2193  );
2194 
2195  /* Create the symbolic expression */
2196  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2197 
2198  if (op3->evaluate()) {
2199  /* Spread the taint from the parent to the child */
2200  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2201  }
2202  else {
2203  inst.removeWrittenRegister(sf.getConstRegister());
2204  }
2205  }
2206 
2207 
2208  void x86Semantics::sfShrd_s(triton::arch::Instruction& inst,
2214  bool vol) {
2215 
2216  auto bvSize = dst.getBitSize();
2217  auto bv1Size = op1->getBitvectorSize();
2218  auto bv2Size = op2->getBitvectorSize();
2219  auto bv3Size = op3->getBitvectorSize();
2220  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2221 
2222  /*
2223  * Create the semantic.
2224  * MSB(ror(op3, concat(op2,op1))) if op3 != 0
2225  */
2226  auto node = this->astCtxt->ite(
2227  this->astCtxt->equal(op3, this->astCtxt->bv(0, bv3Size)),
2228  this->symbolicEngine->getOperandAst(sf),
2229  this->astCtxt->extract(
2230  bvSize - 1, bvSize - 1,
2231  this->astCtxt->bvror(
2232  this->astCtxt->concat(op2, op1),
2233  this->astCtxt->zx(((bv1Size + bv2Size) - bv3Size), op3)
2234  )
2235  )
2236  );
2237 
2238  /* Create the symbolic expression */
2239  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2240 
2241  if (op3->evaluate()) {
2242  /* Spread the taint from the parent to the child */
2243  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2244  }
2245  else {
2246  inst.removeWrittenRegister(sf.getConstRegister());
2247  }
2248  }
2249 
2250 
2251  void x86Semantics::zf_s(triton::arch::Instruction& inst,
2254  bool vol) {
2255 
2256  auto bvSize = dst.getBitSize();
2257  auto low = vol ? 0 : dst.getLow();
2258  auto high = vol ? bvSize-1 : dst.getHigh();
2259 
2260  /*
2261  * Create the semantic.
2262  * zf = 0 == regDst
2263  */
2264  auto node = this->astCtxt->ite(
2265  this->astCtxt->equal(
2266  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
2267  this->astCtxt->bv(0, bvSize)
2268  ),
2269  this->astCtxt->bv(1, 1),
2270  this->astCtxt->bv(0, 1)
2271  );
2272 
2273  /* Create the symbolic expression */
2274  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_ZF), "Zero flag");
2275 
2276  /* Spread the taint from the parent to the child */
2277  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_ZF), parent->isTainted);
2278  }
2279 
2280 
2281  void x86Semantics::zfBsf_s(triton::arch::Instruction& inst,
2285  bool vol) {
2286 
2287  /*
2288  * Create the semantic.
2289  * zf = 1 if op2 == 0 else 0
2290  */
2291  auto node = this->astCtxt->ite(
2292  this->astCtxt->equal(op2, this->astCtxt->bv(0, src.getBitSize())),
2293  this->astCtxt->bvtrue(),
2294  this->astCtxt->bvfalse()
2295  );
2296 
2297  /* Create the symbolic expression */
2298  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_ZF), "Zero flag");
2299 
2300  /* Spread the taint from the parent to the child */
2301  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_ZF), parent->isTainted);
2302  }
2303 
2304 
2305  void x86Semantics::zfShl_s(triton::arch::Instruction& inst,
2309  bool vol) {
2310 
2311  auto bvSize = dst.getBitSize();
2312  auto low = vol ? 0 : dst.getLow();
2313  auto high = vol ? bvSize-1 : dst.getHigh();
2314  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
2315 
2316  /*
2317  * Create the semantic.
2318  * zf if op2 != 0
2319  */
2320  auto node = this->astCtxt->ite(
2321  this->astCtxt->equal(this->astCtxt->zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt->bv(0, bvSize)),
2322  this->symbolicEngine->getOperandAst(zf),
2323  this->astCtxt->ite(
2324  this->astCtxt->equal(
2325  this->astCtxt->extract(high, low, this->astCtxt->reference(parent)),
2326  this->astCtxt->bv(0, bvSize)
2327  ),
2328  this->astCtxt->bv(1, 1),
2329  this->astCtxt->bv(0, 1)
2330  )
2331  );
2332 
2333  /* Create the symbolic expression */
2334  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, zf.getConstRegister(), "Zero flag");
2335 
2336  if (op2->evaluate()) {
2337  /* Spread the taint from the parent to the child */
2338  expr->isTainted = this->taintEngine->setTaintRegister(zf.getConstRegister(), parent->isTainted);
2339  }
2340  else {
2342  }
2343  }
2344 
2345 
2346  void x86Semantics::aaa_s(triton::arch::Instruction& inst) {
2347  auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2348  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2349  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AF));
2350  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2351  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2352 
2353  /* Create symbolic operands */
2354  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2355  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2356  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2357 
2358  /* Create the semantics */
2359  auto node = this->astCtxt->ite(
2360  // if
2361  this->astCtxt->lor(
2362  this->astCtxt->bvugt(
2363  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, src1.getBitSize())),
2364  this->astCtxt->bv(9, src1.getBitSize())
2365  ),
2366  this->astCtxt->equal(op3, this->astCtxt->bvtrue())
2367  ),
2368  // then
2369  this->astCtxt->concat(
2370  this->astCtxt->bvadd(op2, this->astCtxt->bv(1, src2.getBitSize())),
2371  this->astCtxt->bvand(
2372  this->astCtxt->bvadd(op1, this->astCtxt->bv(6, src1.getBitSize())),
2373  this->astCtxt->bv(0xf, src1.getBitSize())
2374  )
2375  ),
2376  // else
2377  this->astCtxt->concat(
2378  op2,
2379  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, src1.getBitSize()))
2380  )
2381  );
2382 
2383  /* Create symbolic expression */
2384  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAA operation");
2385 
2386  /* Spread taint */
2387  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2388 
2389  /* Update symbolic flags */
2390  this->afAaa_s(inst, expr, dsttmp, op1, op3);
2391  this->cfAaa_s(inst, expr, dsttmp, op1, op3);
2392 
2393  /* Tag undefined flags */
2394  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2395  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
2396  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
2397  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
2398 
2399  /* Update the symbolic control flow */
2400  this->controlFlow_s(inst);
2401  }
2402 
2403 
2404  void x86Semantics::aad_s(triton::arch::Instruction& inst) {
2405  auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D5 0A */
2406  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2407  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2408  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2409  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2410 
2411  /* D5 ib */
2412  if (inst.operands.size() == 1)
2413  src1 = inst.operands[0];
2414 
2415  /* Create symbolic operands */
2416  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2417  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2418  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2419 
2420  /* Create the semantics */
2421  auto node = this->astCtxt->zx(
2422  BYTE_SIZE_BIT,
2423  this->astCtxt->bvadd(
2424  op2,
2425  this->astCtxt->bvmul(op3, op1)
2426  )
2427  );
2428 
2429  /* Create symbolic expression */
2430  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAD operation");
2431 
2432  /* Spread taint */
2433  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2434 
2435  /* Update symbolic flags */
2436  this->pf_s(inst, expr, dsttmp);
2437  this->sf_s(inst, expr, dsttmp);
2438  this->zf_s(inst, expr, dsttmp);
2439 
2440  /* Tag undefined flags */
2441  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2442  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
2443  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2444 
2445  /* Update the symbolic control flow */
2446  this->controlFlow_s(inst);
2447  }
2448 
2449 
2450  void x86Semantics::aam_s(triton::arch::Instruction& inst) {
2451  auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D4 0A */
2452  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2453  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2454  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2455 
2456  /* D4 ib */
2457  if (inst.operands.size() == 1)
2458  src1 = inst.operands[0];
2459 
2460  /* Create symbolic operands */
2461  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2462  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2463 
2464  /* Create the semantics */
2465  auto node = this->astCtxt->concat(
2466  this->astCtxt->bvudiv(op2, op1),
2467  this->astCtxt->bvurem(op2, op1)
2468  );
2469 
2470  /* Create symbolic expression */
2471  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAM operation");
2472 
2473  /* Spread taint */
2474  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2475 
2476  /* Update symbolic flags */
2477  this->pf_s(inst, expr, dsttmp);
2478  this->sf_s(inst, expr, dsttmp);
2479  this->zf_s(inst, expr, dsttmp);
2480 
2481  /* Tag undefined flags */
2482  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2483  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
2484  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2485 
2486  /* Update the symbolic control flow */
2487  this->controlFlow_s(inst);
2488  }
2489 
2490 
2491  void x86Semantics::aas_s(triton::arch::Instruction& inst) {
2492  auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2493  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2494  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AF));
2495  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2496  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2497 
2498  /* Create symbolic operands */
2499  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2500  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2501  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2502 
2503  /* Create the semantics */
2504  auto node = this->astCtxt->ite(
2505  // if
2506  this->astCtxt->lor(
2507  this->astCtxt->bvugt(
2508  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, src1.getBitSize())),
2509  this->astCtxt->bv(9, src1.getBitSize())
2510  ),
2511  this->astCtxt->equal(op3, this->astCtxt->bvtrue())
2512  ),
2513  // then
2514  this->astCtxt->concat(
2515  this->astCtxt->bvsub(op2, this->astCtxt->bv(1, src2.getBitSize())),
2516  this->astCtxt->bvand(
2517  this->astCtxt->bvsub(op1, this->astCtxt->bv(6, src1.getBitSize())),
2518  this->astCtxt->bv(0xf, src1.getBitSize())
2519  )
2520  ),
2521  // else
2522  this->astCtxt->concat(
2523  op2,
2524  this->astCtxt->bvand(op1, this->astCtxt->bv(0xf, src1.getBitSize()))
2525  )
2526  );
2527 
2528  /* Create symbolic expression */
2529  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAS operation");
2530 
2531  /* Spread taint */
2532  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2533 
2534  /* Update symbolic flags */
2535  this->afAaa_s(inst, expr, dsttmp, op1, op3);
2536  this->cfAaa_s(inst, expr, dsttmp, op1, op3);
2537 
2538  /* Tag undefined flags */
2539  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2540  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
2541  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
2542  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
2543 
2544  /* Update the symbolic control flow */
2545  this->controlFlow_s(inst);
2546  }
2547 
2548 
2549  void x86Semantics::adc_s(triton::arch::Instruction& inst) {
2550  auto& dst = inst.operands[0];
2551  auto& src = inst.operands[1];
2552  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
2553 
2554  /* Create symbolic operands */
2555  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2556  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2557  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
2558 
2559  /* Create the semantics */
2560  auto node = this->astCtxt->bvadd(this->astCtxt->bvadd(op1, op2), this->astCtxt->zx(dst.getBitSize()-1, op3));
2561 
2562  /* Create symbolic expression */
2563  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADC operation");
2564 
2565  /* Spread taint */
2566  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2567  expr->isTainted = this->taintEngine->taintUnion(dst, cf);
2568 
2569  /* Update symbolic flags */
2570  this->af_s(inst, expr, dst, op1, op2);
2571  this->cfAdd_s(inst, expr, dst, op1, op2);
2572  this->ofAdd_s(inst, expr, dst, op1, op2);
2573  this->pf_s(inst, expr, dst);
2574  this->sf_s(inst, expr, dst);
2575  this->zf_s(inst, expr, dst);
2576 
2577  /* Update the symbolic control flow */
2578  this->controlFlow_s(inst);
2579  }
2580 
2581 
2582  void x86Semantics::adcx_s(triton::arch::Instruction& inst) {
2583  auto& dst = inst.operands[0];
2584  auto& src = inst.operands[1];
2585  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
2586 
2587  /* Create symbolic operands */
2588  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2589  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2590  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
2591 
2592  /* Create the semantics */
2593  auto node = this->astCtxt->bvadd(this->astCtxt->bvadd(op1, op2), this->astCtxt->zx(dst.getBitSize()-1, op3));
2594 
2595  /* Create symbolic expression */
2596  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADCX operation");
2597 
2598  /* Spread taint */
2599  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2600  expr->isTainted = this->taintEngine->taintUnion(dst, cf);
2601 
2602  /* Update symbolic flags */
2603  this->cfAdd_s(inst, expr, dst, op1, op2);
2604 
2605  /* Update the symbolic control flow */
2606  this->controlFlow_s(inst);
2607  }
2608 
2609 
2610  void x86Semantics::add_s(triton::arch::Instruction& inst) {
2611  auto& dst = inst.operands[0];
2612  auto& src = inst.operands[1];
2613 
2614  /* Create symbolic operands */
2615  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2616  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2617 
2618  /* Create the semantics */
2619  auto node = this->astCtxt->bvadd(op1, op2);
2620 
2621  /* Create symbolic expression */
2622  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD operation");
2623 
2624  /* Spread taint */
2625  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2626 
2627  /* Update symbolic flags */
2628  this->af_s(inst, expr, dst, op1, op2);
2629  this->cfAdd_s(inst, expr, dst, op1, op2);
2630  this->ofAdd_s(inst, expr, dst, op1, op2);
2631  this->pf_s(inst, expr, dst);
2632  this->sf_s(inst, expr, dst);
2633  this->zf_s(inst, expr, dst);
2634 
2635  /* Update the symbolic control flow */
2636  this->controlFlow_s(inst);
2637  }
2638 
2639 
2640  void x86Semantics::and_s(triton::arch::Instruction& inst) {
2641  auto& dst = inst.operands[0];
2642  auto& src = inst.operands[1];
2643 
2644  /* Create symbolic operands */
2645  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2646  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2647 
2648  /* Create the semantics */
2649  auto node = this->astCtxt->bvand(op1, op2);
2650 
2651  /* Create symbolic expression */
2652  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND operation");
2653 
2654  /* Spread taint */
2655  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2656 
2657  /* Update symbolic flags */
2658  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2659  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2660  this->pf_s(inst, expr, dst);
2661  this->sf_s(inst, expr, dst);
2662  this->zf_s(inst, expr, dst);
2663 
2664  /* Tag undefined flags */
2665  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2666 
2667  /* Update the symbolic control flow */
2668  this->controlFlow_s(inst);
2669  }
2670 
2671 
2672  void x86Semantics::andn_s(triton::arch::Instruction& inst) {
2673  auto& dst = inst.operands[0];
2674  auto& src1 = inst.operands[1];
2675  auto& src2 = inst.operands[2];
2676 
2677  /* Create symbolic operands */
2678  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
2679  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
2680 
2681  /* Create the semantics */
2682  auto node = this->astCtxt->bvand(this->astCtxt->bvnot(op2), op3);
2683 
2684  /* Create symbolic expression */
2685  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDN operation");
2686 
2687  /* Spread taint */
2688  expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
2689 
2690  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2691  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2692  this->sf_s(inst, expr, dst);
2693  this->zf_s(inst, expr, dst);
2694 
2695  /* Update the symbolic control flow */
2696  this->controlFlow_s(inst);
2697  }
2698 
2699 
2700  void x86Semantics::andnpd_s(triton::arch::Instruction& inst) {
2701  auto& dst = inst.operands[0];
2702  auto& src = inst.operands[1];
2703 
2704  /* Create symbolic operands */
2705  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2706  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2707 
2708  /* Create the semantics */
2709  auto node = this->astCtxt->bvand(this->astCtxt->bvnot(op1), op2);
2710 
2711  /* Create symbolic expression */
2712  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPD operation");
2713 
2714  /* Spread taint */
2715  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2716 
2717  /* Update the symbolic control flow */
2718  this->controlFlow_s(inst);
2719  }
2720 
2721 
2722  void x86Semantics::andnps_s(triton::arch::Instruction& inst) {
2723  auto& dst = inst.operands[0];
2724  auto& src = inst.operands[1];
2725 
2726  /* Create symbolic operands */
2727  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2728  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2729 
2730  /* Create the semantics */
2731  auto node = this->astCtxt->bvand(this->astCtxt->bvnot(op1), op2);
2732 
2733  /* Create symbolic expression */
2734  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPS operation");
2735 
2736  /* Spread taint */
2737  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2738 
2739  /* Update the symbolic control flow */
2740  this->controlFlow_s(inst);
2741  }
2742 
2743 
2744  void x86Semantics::andpd_s(triton::arch::Instruction& inst) {
2745  auto& dst = inst.operands[0];
2746  auto& src = inst.operands[1];
2747 
2748  /* Create symbolic operands */
2749  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2750  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2751 
2752  /* Create the semantics */
2753  auto node = this->astCtxt->bvand(op1, op2);
2754 
2755  /* Create symbolic expression */
2756  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPD operation");
2757 
2758  /* Spread taint */
2759  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2760 
2761  /* Update the symbolic control flow */
2762  this->controlFlow_s(inst);
2763  }
2764 
2765 
2766  void x86Semantics::andps_s(triton::arch::Instruction& inst) {
2767  auto& dst = inst.operands[0];
2768  auto& src = inst.operands[1];
2769 
2770  /* Create symbolic operands */
2771  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2772  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2773 
2774  /* Create the semantics */
2775  auto node = this->astCtxt->bvand(op1, op2);
2776 
2777  /* Create symbolic expression */
2778  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPS operation");
2779 
2780  /* Spread taint */
2781  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2782 
2783  /* Update the symbolic control flow */
2784  this->controlFlow_s(inst);
2785  }
2786 
2787 
2788  void x86Semantics::bextr_s(triton::arch::Instruction& inst) {
2789  auto& dst = inst.operands[0];
2790  auto& src1 = inst.operands[1];
2791  auto& src2 = inst.operands[2];
2792 
2793  /* Create symbolic operands */
2794  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2795  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2796 
2797  /* Create the semantics */
2798  auto node = this->astCtxt->bvand(
2799  this->astCtxt->bvlshr(
2800  op1,
2801  this->astCtxt->zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt->extract(7, 0, op2))
2802  ),
2803  this->astCtxt->bvsub(
2804  this->astCtxt->bvshl(
2805  this->astCtxt->bv(1, src1.getBitSize()),
2806  this->astCtxt->zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt->extract(15, 8, op2))
2807  ),
2808  this->astCtxt->bv(1, src1.getBitSize())
2809  )
2810  );
2811 
2812  /* Create symbolic expression */
2813  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BEXTR operation");
2814 
2815  /* Spread taint */
2816  expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
2817 
2818  /* Update symbolic flags */
2819  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2820  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2821  this->zf_s(inst, expr, dst);
2822 
2823  /* Update the symbolic control flow */
2824  this->controlFlow_s(inst);
2825  }
2826 
2827 
2828  void x86Semantics::blsi_s(triton::arch::Instruction& inst) {
2829  auto& dst = inst.operands[0];
2830  auto& src = inst.operands[1];
2831 
2832  /* Create symbolic operands */
2833  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2834 
2835  /* Create the semantics */
2836  auto node = this->astCtxt->bvand(this->astCtxt->bvneg(op1), op1);
2837 
2838  /* Create symbolic expression */
2839  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSI operation");
2840 
2841  /* Spread taint */
2842  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2843 
2844  /* Update symbolic flags */
2845  this->cfBlsi_s(inst, expr, src, op1);
2846  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2847  this->sf_s(inst, expr, dst);
2848  this->zf_s(inst, expr, dst);
2849 
2850  /* Update the symbolic control flow */
2851  this->controlFlow_s(inst);
2852  }
2853 
2854 
2855  void x86Semantics::blsmsk_s(triton::arch::Instruction& inst) {
2856  auto& dst = inst.operands[0];
2857  auto& src = inst.operands[1];
2858 
2859  /* Create symbolic operands */
2860  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2861 
2862  /* Create the semantics */
2863  auto node = this->astCtxt->bvxor(
2864  this->astCtxt->bvsub(op1, this->astCtxt->bv(1, src.getBitSize())),
2865  op1
2866  );
2867 
2868  /* Create symbolic expression */
2869  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSMSK operation");
2870 
2871  /* Spread taint */
2872  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2873 
2874  /* Update symbolic flags */
2875  this->cfBlsmsk_s(inst, expr, src, op1);
2876  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2877  this->sf_s(inst, expr, dst);
2878  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_ZF), "Clears zero flag");
2879 
2880  /* Update the symbolic control flow */
2881  this->controlFlow_s(inst);
2882  }
2883 
2884 
2885  void x86Semantics::blsr_s(triton::arch::Instruction& inst) {
2886  auto& dst = inst.operands[0];
2887  auto& src = inst.operands[1];
2888 
2889  /* Create symbolic operands */
2890  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2891 
2892  /* Create the semantics */
2893  auto node = this->astCtxt->bvand(
2894  this->astCtxt->bvsub(op1, this->astCtxt->bv(1, src.getBitSize())),
2895  op1
2896  );
2897 
2898  /* Create symbolic expression */
2899  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSR operation");
2900 
2901  /* Spread taint */
2902  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2903 
2904  /* Update symbolic flags */
2905  this->cfBlsr_s(inst, expr, src, op1);
2906  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2907  this->sf_s(inst, expr, dst);
2908  this->zf_s(inst, expr, dst);
2909 
2910  /* Update the symbolic control flow */
2911  this->controlFlow_s(inst);
2912  }
2913 
2914 
2915  void x86Semantics::bsf_s(triton::arch::Instruction& inst) {
2916  auto& dst = inst.operands[0];
2917  auto& src = inst.operands[1];
2918  auto bvSize1 = dst.getBitSize();
2919  auto bvSize2 = src.getBitSize();
2920 
2921  /* Create symbolic operands */
2922  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2923  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2924 
2925  /* Create the semantics */
2926  triton::ast::SharedAbstractNode node = nullptr;
2927  switch (src.getSize()) {
2928  case BYTE_SIZE:
2929  node = this->astCtxt->ite(
2930  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2931  op1,
2932  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
2933  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
2934  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
2935  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
2936  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
2937  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
2938  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
2939  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
2940  this->astCtxt->bv(0, bvSize1)
2941  ))))))))
2942  );
2943  break;
2944  case WORD_SIZE:
2945  node = this->astCtxt->ite(
2946  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2947  op1,
2948  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
2949  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
2950  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
2951  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
2952  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
2953  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
2954  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
2955  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
2956  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
2957  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
2958  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
2959  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
2960  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
2961  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
2962  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
2963  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
2964  this->astCtxt->bv(0, bvSize1)
2965  ))))))))))))))))
2966  );
2967  break;
2968  case DWORD_SIZE:
2969  node = this->astCtxt->ite(
2970  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2971  op1,
2972  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
2973  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
2974  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
2975  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
2976  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
2977  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
2978  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
2979  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
2980  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
2981  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
2982  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
2983  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
2984  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
2985  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
2986  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
2987  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
2988  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize1),
2989  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize1),
2990  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize1),
2991  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize1),
2992  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize1),
2993  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize1),
2994  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(22, bvSize1),
2995  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(23, bvSize1),
2996  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(24, bvSize1),
2997  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(25, bvSize1),
2998  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(26, bvSize1),
2999  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(27, bvSize1),
3000  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(28, bvSize1),
3001  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(29, bvSize1),
3002  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(30, bvSize1),
3003  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(31, bvSize1),
3004  this->astCtxt->bv(0, bvSize1)
3005  ))))))))))))))))))))))))))))))))
3006  );
3007  break;
3008  case QWORD_SIZE:
3009  node = this->astCtxt->ite(
3010  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
3011  op1,
3012  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
3013  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
3014  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
3015  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
3016  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
3017  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
3018  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
3019  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
3020  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
3021  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
3022  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
3023  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
3024  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
3025  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
3026  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
3027  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
3028  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize1),
3029  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize1),
3030  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize1),
3031  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize1),
3032  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize1),
3033  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize1),
3034  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(22, bvSize1),
3035  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(23, bvSize1),
3036  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(24, bvSize1),
3037  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(25, bvSize1),
3038  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(26, bvSize1),
3039  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(27, bvSize1),
3040  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(28, bvSize1),
3041  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(29, bvSize1),
3042  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(30, bvSize1),
3043  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(31, bvSize1),
3044  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(32, 32, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(32, bvSize1),
3045  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(33, 33, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(33, bvSize1),
3046  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(34, 34, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(34, bvSize1),
3047  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(35, 35, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(35, bvSize1),
3048  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(36, 36, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(36, bvSize1),
3049  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(37, 37, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(37, bvSize1),
3050  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(38, 38, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(38, bvSize1),
3051  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(39, 39, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(39, bvSize1),
3052  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(40, 40, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(40, bvSize1),
3053  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(41, 41, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(41, bvSize1),
3054  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(42, 42, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(42, bvSize1),
3055  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(43, 43, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(43, bvSize1),
3056  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(44, 44, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(44, bvSize1),
3057  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(45, 45, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(45, bvSize1),
3058  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(46, 46, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(46, bvSize1),
3059  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(47, 47, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(47, bvSize1),
3060  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(48, 48, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(48, bvSize1),
3061  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(49, 49, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(49, bvSize1),
3062  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(50, 50, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(50, bvSize1),
3063  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(51, 51, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(51, bvSize1),
3064  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(52, 52, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(52, bvSize1),
3065  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(53, 53, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(53, bvSize1),
3066  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(54, 54, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(54, bvSize1),
3067  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(55, 55, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(55, bvSize1),
3068  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(56, 56, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(56, bvSize1),
3069  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(57, 57, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(57, bvSize1),
3070  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(58, 58, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(58, bvSize1),
3071  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(59, 59, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(59, bvSize1),
3072  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(60, 60, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(60, bvSize1),
3073  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(61, 61, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(61, bvSize1),
3074  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(62, 62, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(62, bvSize1),
3075  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(63, 63, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(63, bvSize1),
3076  this->astCtxt->bv(0, bvSize1)
3077  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
3078  );
3079  break;
3080  default:
3081  throw triton::exceptions::Semantics("x86Semantics::bsf_s(): Invalid operand size.");
3082  }
3083 
3084  /* Create symbolic expression */
3085  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BSF operation");
3086 
3087  /* Spread taint */
3088  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3089 
3090  /* Update symbolic flags */
3091  this->zfBsf_s(inst, expr, src, op2);
3092 
3093  /* Tag undefined flags */
3094  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3095  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
3096  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3097  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3098  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3099 
3100  /* Update the symbolic control flow */
3101  this->controlFlow_s(inst);
3102  }
3103 
3104 
3105  void x86Semantics::bsr_s(triton::arch::Instruction& inst) {
3106  auto& dst = inst.operands[0];
3107  auto& src = inst.operands[1];
3108  auto bvSize1 = dst.getBitSize();
3109  auto bvSize2 = src.getBitSize();
3110 
3111  /* Create symbolic operands */
3112  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3113  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3114 
3115  /* Create the semantics */
3116  triton::ast::SharedAbstractNode node = nullptr;
3117  switch (src.getSize()) {
3118  case BYTE_SIZE:
3119  node = this->astCtxt->ite(
3120  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3121  op1,
3122  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
3123  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
3124  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
3125  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
3126  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
3127  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
3128  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
3129  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
3130  this->astCtxt->bv(0, bvSize1)
3131  ))))))))
3132  );
3133  break;
3134  case WORD_SIZE:
3135  node = this->astCtxt->ite(
3136  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3137  op1,
3138  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
3139  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
3140  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
3141  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
3142  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
3143  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
3144  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
3145  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
3146  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
3147  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
3148  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
3149  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
3150  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
3151  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
3152  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
3153  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
3154  this->astCtxt->bv(0, bvSize1)
3155  ))))))))))))))))
3156  );
3157  break;
3158  case DWORD_SIZE:
3159  node = this->astCtxt->ite(
3160  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3161  op1,
3162  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(31, bvSize1),
3163  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(30, bvSize1),
3164  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(29, bvSize1),
3165  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(28, bvSize1),
3166  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(27, bvSize1),
3167  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(26, bvSize1),
3168  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(25, bvSize1),
3169  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(24, bvSize1),
3170  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(23, bvSize1),
3171  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(22, bvSize1),
3172  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize1),
3173  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize1),
3174  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize1),
3175  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize1),
3176  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize1),
3177  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize1),
3178  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
3179  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
3180  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
3181  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
3182  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
3183  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
3184  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
3185  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
3186  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
3187  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
3188  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
3189  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
3190  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
3191  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
3192  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
3193  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
3194  this->astCtxt->bv(0, bvSize1)
3195  ))))))))))))))))))))))))))))))))
3196  );
3197  break;
3198  case QWORD_SIZE:
3199  node = this->astCtxt->ite(
3200  this->astCtxt->equal(op2, this->astCtxt->bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3201  op1,
3202  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(63, 63, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(63, bvSize1),
3203  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(62, 62, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(62, bvSize1),
3204  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(61, 61, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(61, bvSize1),
3205  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(60, 60, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(60, bvSize1),
3206  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(59, 59, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(59, bvSize1),
3207  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(58, 58, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(58, bvSize1),
3208  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(57, 57, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(57, bvSize1),
3209  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(56, 56, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(56, bvSize1),
3210  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(55, 55, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(55, bvSize1),
3211  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(54, 54, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(54, bvSize1),
3212  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(53, 53, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(53, bvSize1),
3213  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(52, 52, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(52, bvSize1),
3214  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(51, 51, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(51, bvSize1),
3215  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(50, 50, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(50, bvSize1),
3216  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(49, 49, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(49, bvSize1),
3217  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(48, 48, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(48, bvSize1),
3218  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(47, 47, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(47, bvSize1),
3219  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(46, 46, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(46, bvSize1),
3220  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(45, 45, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(45, bvSize1),
3221  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(44, 44, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(44, bvSize1),
3222  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(43, 43, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(43, bvSize1),
3223  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(42, 42, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(42, bvSize1),
3224  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(41, 41, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(41, bvSize1),
3225  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(40, 40, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(40, bvSize1),
3226  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(39, 39, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(39, bvSize1),
3227  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(38, 38, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(38, bvSize1),
3228  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(37, 37, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(37, bvSize1),
3229  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(36, 36, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(36, bvSize1),
3230  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(35, 35, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(35, bvSize1),
3231  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(34, 34, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(34, bvSize1),
3232  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(33, 33, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(33, bvSize1),
3233  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(32, 32, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(32, bvSize1),
3234  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(31, 31, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(31, bvSize1),
3235  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(30, 30, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(30, bvSize1),
3236  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(29, 29, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(29, bvSize1),
3237  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(28, 28, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(28, bvSize1),
3238  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(27, 27, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(27, bvSize1),
3239  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(26, 26, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(26, bvSize1),
3240  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(25, 25, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(25, bvSize1),
3241  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(24, 24, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(24, bvSize1),
3242  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(23, 23, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(23, bvSize1),
3243  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(22, 22, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(22, bvSize1),
3244  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(21, 21, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(21, bvSize1),
3245  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(20, 20, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(20, bvSize1),
3246  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(19, 19, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(19, bvSize1),
3247  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(18, 18, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(18, bvSize1),
3248  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(17, 17, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(17, bvSize1),
3249  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(16, 16, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(16, bvSize1),
3250  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(15, 15, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(15, bvSize1),
3251  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(14, 14, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(14, bvSize1),
3252  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(13, 13, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(13, bvSize1),
3253  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(12, 12, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(12, bvSize1),
3254  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(11, 11, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(11, bvSize1),
3255  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(10, 10, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(10, bvSize1),
3256  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(9, 9, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(9, bvSize1),
3257  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(8, 8, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(8, bvSize1),
3258  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(7, 7, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(7, bvSize1),
3259  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(6, 6, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(6, bvSize1),
3260  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(5, 5, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(5, bvSize1),
3261  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(4, 4, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(4, bvSize1),
3262  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(3, 3, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(3, bvSize1),
3263  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(2, 2, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(2, bvSize1),
3264  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(1, 1, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(1, bvSize1),
3265  this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->extract(0, 0, op2), this->astCtxt->bvtrue()), this->astCtxt->bv(0, bvSize1),
3266  this->astCtxt->bv(0, bvSize1)
3267  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
3268  );
3269  break;
3270  default:
3271  throw triton::exceptions::Semantics("x86Semantics::bsr_s(): Invalid operand size.");
3272  }
3273 
3274  /* Create symbolic expression */
3275  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BSR operation");
3276 
3277  /* Spread taint */
3278  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3279 
3280  /* Update symbolic flags */
3281  this->zfBsf_s(inst, expr, src, op2); /* same as bsf */
3282 
3283  /* Tag undefined flags */
3284  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3285  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
3286  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3287  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3288  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3289 
3290  /* Update the symbolic control flow */
3291  this->controlFlow_s(inst);
3292  }
3293 
3294 
3295  void x86Semantics::bswap_s(triton::arch::Instruction& inst) {
3296  auto& src = inst.operands[0];
3297 
3298  /* Create symbolic operands */
3299  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3300 
3301  /* Create the semantics */
3302  std::list<triton::ast::SharedAbstractNode> bytes;
3303  switch (src.getSize()) {
3304  case QWORD_SIZE:
3305  bytes.push_front(this->astCtxt->extract(63, 56, op1));
3306  bytes.push_front(this->astCtxt->extract(55, 48, op1));
3307  bytes.push_front(this->astCtxt->extract(47, 40, op1));
3308  bytes.push_front(this->astCtxt->extract(39, 32, op1));
3309  case DWORD_SIZE:
3310  bytes.push_front(this->astCtxt->extract(31, 24, op1));
3311  bytes.push_front(this->astCtxt->extract(23, 16, op1));
3312  case WORD_SIZE:
3313  bytes.push_front(this->astCtxt->extract(15, 8, op1));
3314  bytes.push_front(this->astCtxt->extract(7, 0, op1));
3315  break;
3316  default:
3317  throw triton::exceptions::Semantics("x86Semantics::bswap_s(): Invalid operand size.");
3318  }
3319 
3320  auto node = this->astCtxt->concat(bytes);
3321 
3322  /* Create symbolic expression */
3323  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, src, "BSWAP operation");
3324 
3325  /* Spread taint */
3326  expr->isTainted = this->taintEngine->taintAssignment(src, src);
3327 
3328  /* Update the symbolic control flow */
3329  this->controlFlow_s(inst);
3330  }
3331 
3332 
3333  void x86Semantics::bt_s(triton::arch::Instruction& inst) {
3334  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3335  auto& src1 = inst.operands[0];
3336  auto& src2 = inst.operands[1];
3337 
3338  /* Create symbolic operands */
3339  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3340  auto op2 = this->astCtxt->zx(src1.getBitSize() - src2.getBitSize(), this->symbolicEngine->getOperandAst(inst, src2));
3341 
3342  /* Create the semantics */
3343  auto node = this->astCtxt->extract(0, 0,
3344  this->astCtxt->bvlshr(
3345  op1,
3346  this->astCtxt->bvsmod(
3347  op2,
3348  this->astCtxt->bv(src1.getBitSize(), src1.getBitSize())
3349  )
3350  )
3351  );
3352 
3353  /* Create symbolic expression */
3354  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "BT operation");
3355 
3356  /* Spread taint */
3357  expr->isTainted = this->taintEngine->taintUnion(dst, src1);
3358  expr->isTainted = this->taintEngine->taintUnion(dst, src2);
3359 
3360  /* Tag undefined flags */
3361  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3362  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3363  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3364  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3365 
3366  /* Update the symbolic control flow */
3367  this->controlFlow_s(inst);
3368  }
3369 
3370 
3371  void x86Semantics::btc_s(triton::arch::Instruction& inst) {
3372  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3373  auto& dst2 = inst.operands[0];
3374  auto& src1 = inst.operands[1];
3375 
3376  /* Create symbolic operands */
3377  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3378  auto op2 = this->astCtxt->zx(dst2.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
3379 
3380  /* Create the semantics */
3381  auto node1 = this->astCtxt->extract(0, 0,
3382  this->astCtxt->bvlshr(
3383  op1,
3384  this->astCtxt->bvsmod(
3385  op2,
3386  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3387  )
3388  )
3389  );
3390  auto node2 = this->astCtxt->ite(
3391  this->astCtxt->equal(node1, this->astCtxt->bvfalse()),
3392  /* BTS */
3393  this->astCtxt->bvor(
3394  op1,
3395  this->astCtxt->bvshl(
3396  this->astCtxt->bv(1, dst2.getBitSize()),
3397  this->astCtxt->bvsmod(
3398  op2,
3399  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3400  )
3401  )
3402  ),
3403  /* BTR */
3404  this->astCtxt->bvand(
3405  op1,
3406  this->astCtxt->bvsub(
3407  op1,
3408  this->astCtxt->bvshl(
3409  this->astCtxt->bv(1, dst2.getBitSize()),
3410  this->astCtxt->bvsmod(
3411  op2,
3412  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3413  )
3414  )
3415  )
3416  )
3417  );
3418 
3419  /* Create symbolic expression */
3420  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTC carry operation");
3421  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTC complement operation");
3422 
3423  /* Spread taint */
3424  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3425  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3426  expr2->isTainted = this->taintEngine->taintUnion(dst2, src1);
3427 
3428  /* Tag undefined flags */
3429  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3430  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3431  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3432  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3433 
3434  /* Update the symbolic control flow */
3435  this->controlFlow_s(inst);
3436  }
3437 
3438 
3439  void x86Semantics::btr_s(triton::arch::Instruction& inst) {
3440  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3441  auto& dst2 = inst.operands[0];
3442  auto& src1 = inst.operands[1];
3443 
3444  /* Create symbolic operands */
3445  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3446  auto op2 = this->astCtxt->zx(dst2.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
3447 
3448  /* Create the semantics */
3449  auto node1 = this->astCtxt->extract(0, 0,
3450  this->astCtxt->bvlshr(
3451  op1,
3452  this->astCtxt->bvsmod(
3453  op2,
3454  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3455  )
3456  )
3457  );
3458  auto node2 = this->astCtxt->ite(
3459  this->astCtxt->equal(node1, this->astCtxt->bvfalse()),
3460  op1,
3461  this->astCtxt->bvand(
3462  op1,
3463  this->astCtxt->bvsub(
3464  op1,
3465  this->astCtxt->bvshl(
3466  this->astCtxt->bv(1, dst2.getBitSize()),
3467  this->astCtxt->bvsmod(
3468  op2,
3469  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3470  )
3471  )
3472  )
3473  )
3474  );
3475 
3476  /* Create symbolic expression */
3477  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTR carry operation");
3478  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTR reset operation");
3479 
3480  /* Spread taint */
3481  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3482  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3483  expr2->isTainted = this->taintEngine->taintUnion(dst2, src1);
3484 
3485  /* Tag undefined flags */
3486  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3487  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3488  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3489  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3490 
3491  /* Update the symbolic control flow */
3492  this->controlFlow_s(inst);
3493  }
3494 
3495 
3496  void x86Semantics::bts_s(triton::arch::Instruction& inst) {
3497  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3498  auto& dst2 = inst.operands[0];
3499  auto& src1 = inst.operands[1];
3500 
3501  /* Create symbolic operands */
3502  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3503  auto op2 = this->astCtxt->zx(dst2.getBitSize() - src1.getBitSize(), this->symbolicEngine->getOperandAst(inst, src1));
3504 
3505  /* Create the semantics */
3506  auto node1 = this->astCtxt->extract(0, 0,
3507  this->astCtxt->bvlshr(
3508  op1,
3509  this->astCtxt->bvsmod(
3510  op2,
3511  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3512  )
3513  )
3514  );
3515  auto node2 = this->astCtxt->bvor(
3516  op1,
3517  this->astCtxt->bvshl(
3518  this->astCtxt->bv(1, dst2.getBitSize()),
3519  this->astCtxt->bvsmod(
3520  op2,
3521  this->astCtxt->bv(dst2.getBitSize(), dst2.getBitSize())
3522  )
3523  )
3524  );
3525 
3526  /* Create symbolic expression */
3527  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTS carry operation");
3528  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTS set operation");
3529 
3530  /* Spread taint */
3531  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3532  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3533  expr2->isTainted = this->taintEngine->taintUnion(dst2, src1);
3534 
3535  /* Tag undefined flags */
3536  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3537  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3538  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3539  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3540 
3541  /* Update the symbolic control flow */
3542  this->controlFlow_s(inst);
3543  }
3544 
3545 
3546  void x86Semantics::call_s(triton::arch::Instruction& inst) {
3547  auto stack = this->architecture->getStackPointer();
3548 
3549  /* Create the semantics - side effect */
3550  auto stackValue = alignSubStack_s(inst, stack.getSize());
3551  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
3552  auto sp = triton::arch::OperandWrapper(triton::arch::MemoryAccess(stackValue, stack.getSize()));
3553  auto& src = inst.operands[0];
3554 
3555  /* Create symbolic operands */
3556  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3557 
3558  /* Create the semantics - side effect */
3559  auto node1 = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
3560 
3561  /* Create the semantics */
3562  auto node2 = op1;
3563 
3564  /* Create the symbolic expression */
3565  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, sp, "Saved Program Counter");
3566 
3567  /* Create symbolic expression */
3568  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
3569 
3570  /* Spread taint */
3571  expr1->isTainted = this->taintEngine->taintAssignmentMemoryImmediate(sp.getMemory());
3572  expr2->isTainted = this->taintEngine->taintAssignment(pc, src);
3573 
3574  /* Create the path constraint */
3575  this->symbolicEngine->addPathConstraint(inst, expr2);
3576  }
3577 
3578 
3579  void x86Semantics::cbw_s(triton::arch::Instruction& inst) {
3580  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
3581 
3582  /* Create symbolic operands */
3583  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3584 
3585  /* Create the semantics */
3586  auto node = this->astCtxt->sx(BYTE_SIZE_BIT, this->astCtxt->extract(BYTE_SIZE_BIT-1, 0, op1));
3587 
3588  /* Create symbolic expression */
3589  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBW operation");
3590 
3591  /* Spread taint */
3592  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3593 
3594  /* Update the symbolic control flow */
3595  this->controlFlow_s(inst);
3596  }
3597 
3598 
3599  void x86Semantics::cdq_s(triton::arch::Instruction& inst) {
3600  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
3601  auto src = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
3602 
3603  /* Create symbolic operands */
3604  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3605 
3606  /* Create the semantics - TMP = 64 bitvec (EDX:EAX) */
3607  auto node1 = this->astCtxt->sx(DWORD_SIZE_BIT, op1);
3608 
3609  /* Create symbolic expression */
3610  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "Temporary variable");
3611 
3612  /* Spread taint */
3613  expr1->isTainted = this->taintEngine->isRegisterTainted(this->architecture->getRegister(ID_REG_X86_EAX));
3614 
3615  /* Create the semantics - EDX = TMP[63...32] */
3616  auto node2 = this->astCtxt->extract(QWORD_SIZE_BIT-1, DWORD_SIZE_BIT, this->astCtxt->reference(expr1));
3617 
3618  /* Create symbolic expression */
3619  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst, "CDQ operation");
3620 
3621  /* Spread taint */
3622  expr2->isTainted = this->taintEngine->taintAssignment(dst, src);
3623 
3624  /* Update the symbolic control flow */
3625  this->controlFlow_s(inst);
3626  }
3627 
3628 
3629  void x86Semantics::cdqe_s(triton::arch::Instruction& inst) {
3630  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
3631 
3632  /* Create symbolic operands */
3633  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3634 
3635  /* Create the semantics */
3636  auto node = this->astCtxt->sx(DWORD_SIZE_BIT, this->astCtxt->extract(DWORD_SIZE_BIT-1, 0, op1));
3637 
3638  /* Create symbolic expression */
3639  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CDQE operation");
3640 
3641  /* Spread taint */
3642  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3643 
3644  /* Update the symbolic control flow */
3645  this->controlFlow_s(inst);
3646  }
3647 
3648 
3649  void x86Semantics::clc_s(triton::arch::Instruction& inst) {
3650  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
3651  /* Update the symbolic control flow */
3652  this->controlFlow_s(inst);
3653  }
3654 
3655 
3656  void x86Semantics::cld_s(triton::arch::Instruction& inst) {
3657  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_DF), "Clears direction flag");
3658  /* Update the symbolic control flow */
3659  this->controlFlow_s(inst);
3660  }
3661 
3662 
3663  void x86Semantics::clflush_s(triton::arch::Instruction& inst) {
3664  /* Update the symbolic control flow */
3665  this->controlFlow_s(inst);
3666  }
3667 
3668 
3669  void x86Semantics::clts_s(triton::arch::Instruction& inst) {
3670  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CR0));
3671 
3672  /* Create symbolic operands */
3673  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3674 
3675  /* Create the semantics */
3676  triton::ast::SharedAbstractNode node = nullptr;
3677 
3678  switch (dst.getBitSize()) {
3679  case QWORD_SIZE_BIT:
3680  node = this->astCtxt->bvand(op1, this->astCtxt->bv(0xfffffffffffffff7, QWORD_SIZE_BIT));
3681  break;
3682  case DWORD_SIZE_BIT:
3683  node = this->astCtxt->bvand(op1, this->astCtxt->bv(0xfffffff7, DWORD_SIZE_BIT));
3684  break;
3685  default:
3686  throw triton::exceptions::Semantics("x86Semantics::clts_s(): Invalid operand size.");
3687  }
3688 
3689  /* Create symbolic expression */
3690  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CLTS operation");
3691 
3692  /* Spread taint */
3693  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3694 
3695  /* Update the symbolic control flow */
3696  this->controlFlow_s(inst);
3697  }
3698 
3699 
3700  void x86Semantics::cli_s(triton::arch::Instruction& inst) {
3701  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_IF), "Clears interrupt flag");
3702  /* Update the symbolic control flow */
3703  this->controlFlow_s(inst);
3704  }
3705 
3706 
3707  void x86Semantics::cmc_s(triton::arch::Instruction& inst) {
3708  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3709 
3710  /* Create symbolic operands */
3711  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3712 
3713  /* Create the semantics */
3714  auto node = this->astCtxt->bvnot(op1);
3715 
3716  /* Create symbolic expression */
3717  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst.getRegister(), "CMC operation");
3718 
3719  /* Spread taint */
3720  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3721 
3722  /* Update the symbolic control flow */
3723  this->controlFlow_s(inst);
3724  }
3725 
3726 
3727  void x86Semantics::cmova_s(triton::arch::Instruction& inst) {
3728  auto& dst = inst.operands[0];
3729  auto& src = inst.operands[1];
3730  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3731  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3732 
3733  /* Create symbolic operands */
3734  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3735  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3736  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3737  auto op4 = this->symbolicEngine->getOperandAst(inst, zf);
3738 
3739  /* Create the semantics */
3740  auto node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->bvand(this->astCtxt->bvnot(op3), this->astCtxt->bvnot(op4)), this->astCtxt->bvtrue()), op2, op1);
3741 
3742  /* Create symbolic expression */
3743  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVA operation");
3744 
3745  /* Spread taint and condition flag */
3746  if (op3->evaluate().is_zero() && op4->evaluate().is_zero()) {
3747  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3748  inst.setConditionTaken(true);
3749  }
3750  else {
3751  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3752  }
3753 
3754  expr->isTainted |= this->taintEngine->isTainted(cf) || this->taintEngine->isTainted(zf);
3755 
3756  /* Update the symbolic control flow */
3757  this->controlFlow_s(inst);
3758  }
3759 
3760 
3761  void x86Semantics::cmovae_s(triton::arch::Instruction& inst) {
3762  auto& dst = inst.operands[0];
3763  auto& src = inst.operands[1];
3764  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3765 
3766  /* Create symbolic operands */
3767  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3768  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3769  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3770 
3771  /* Create the semantics */
3772  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvfalse()), op2, op1);
3773 
3774  /* Create symbolic expression */
3775  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVAE operation");
3776 
3777  /* Spread taint and condition flag */
3778  if (op3->evaluate().is_zero()) {
3779  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3780  inst.setConditionTaken(true);
3781  }
3782  else {
3783  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3784  }
3785 
3786  expr->isTainted |= this->taintEngine->isTainted(cf);
3787 
3788  /* Update the symbolic control flow */
3789  this->controlFlow_s(inst);
3790  }
3791 
3792 
3793  void x86Semantics::cmovb_s(triton::arch::Instruction& inst) {
3794  auto& dst = inst.operands[0];
3795  auto& src = inst.operands[1];
3796  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3797 
3798  /* Create symbolic operands */
3799  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3800  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3801  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3802 
3803  /* Create the semantics */
3804  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvtrue()), op2, op1);
3805 
3806  /* Create symbolic expression */
3807  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVB operation");
3808 
3809  /* Spread taint and condition flag */
3810  if (!op3->evaluate().is_zero()) {
3811  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3812  inst.setConditionTaken(true);
3813  }
3814  else {
3815  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3816  }
3817 
3818  expr->isTainted |= this->taintEngine->isTainted(cf);
3819 
3820  /* Update the symbolic control flow */
3821  this->controlFlow_s(inst);
3822  }
3823 
3824 
3825  void x86Semantics::cmovbe_s(triton::arch::Instruction& inst) {
3826  auto& dst = inst.operands[0];
3827  auto& src = inst.operands[1];
3828  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3829  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3830 
3831  /* Create symbolic operands */
3832  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3833  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3834  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3835  auto op4 = this->symbolicEngine->getOperandAst(inst, zf);
3836 
3837  /* Create the semantics */
3838  auto node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->bvor(op3, op4), this->astCtxt->bvtrue()), op2, op1);
3839 
3840  /* Create symbolic expression */
3841  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVBE operation");
3842 
3843  /* Spread taint and condition flag */
3844  if (!op3->evaluate().is_zero() || !op4->evaluate().is_zero()) {
3845  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3846  inst.setConditionTaken(true);
3847  }
3848  else {
3849  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3850  }
3851 
3852  expr->isTainted |= this->taintEngine->isTainted(cf) || this->taintEngine->isTainted(zf);
3853 
3854  /* Update the symbolic control flow */
3855  this->controlFlow_s(inst);
3856  }
3857 
3858 
3859  void x86Semantics::cmove_s(triton::arch::Instruction& inst) {
3860  auto& dst = inst.operands[0];
3861  auto& src = inst.operands[1];
3862  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3863 
3864  /* Create symbolic operands */
3865  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3866  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3867  auto op3 = this->symbolicEngine->getOperandAst(inst, zf);
3868 
3869  /* Create the semantics */
3870  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvtrue()), op2, op1);
3871 
3872  /* Create symbolic expression */
3873  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVE operation");
3874 
3875  /* Spread taint and condition flag */
3876  if (!op3->evaluate().is_zero()) {
3877  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3878  inst.setConditionTaken(true);
3879  }
3880  else {
3881  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3882  }
3883 
3884  expr->isTainted |= this->taintEngine->isTainted(zf);
3885 
3886  /* Update the symbolic control flow */
3887  this->controlFlow_s(inst);
3888  }
3889 
3890 
3891  void x86Semantics::cmovg_s(triton::arch::Instruction& inst) {
3892  auto& dst = inst.operands[0];
3893  auto& src = inst.operands[1];
3894  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3895  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3896  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3897 
3898  /* Create symbolic operands */
3899  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3900  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3901  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3902  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3903  auto op5 = this->symbolicEngine->getOperandAst(inst, zf);
3904 
3905  /* Create the semantics */
3906  auto node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->bvor(this->astCtxt->bvxor(op3, op4), op5), this->astCtxt->bvfalse()), op2, op1);
3907 
3908  /* Create symbolic expression */
3909  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVG operation");
3910 
3911  /* Spread taint and condition flag */
3912  if ((op3->evaluate().is_zero() == op4->evaluate().is_zero()) && op5->evaluate().is_zero()) {
3913  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3914  inst.setConditionTaken(true);
3915  }
3916  else {
3917  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3918  }
3919 
3920  expr->isTainted |= this->taintEngine->isTainted(sf) || this->taintEngine->isTainted(of) || this->taintEngine->isTainted(zf);
3921 
3922  /* Update the symbolic control flow */
3923  this->controlFlow_s(inst);
3924  }
3925 
3926 
3927  void x86Semantics::cmovge_s(triton::arch::Instruction& inst) {
3928  auto& dst = inst.operands[0];
3929  auto& src = inst.operands[1];
3930  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3931  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3932 
3933  /* Create symbolic operands */
3934  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3935  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3936  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3937  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3938 
3939  /* Create the semantics */
3940  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, op4), op2, op1);
3941 
3942  /* Create symbolic expression */
3943  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVGE operation");
3944 
3945  /* Spread taint and condition flag */
3946  if (op3->evaluate().is_zero() == op4->evaluate().is_zero()) {
3947  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3948  inst.setConditionTaken(true);
3949  }
3950  else {
3951  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3952  }
3953 
3954  expr->isTainted |= this->taintEngine->isTainted(sf) || this->taintEngine->isTainted(of);
3955 
3956  /* Update the symbolic control flow */
3957  this->controlFlow_s(inst);
3958  }
3959 
3960 
3961  void x86Semantics::cmovl_s(triton::arch::Instruction& inst) {
3962  auto& dst = inst.operands[0];
3963  auto& src = inst.operands[1];
3964  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3965  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3966 
3967  /* Create symbolic operands */
3968  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3969  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3970  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3971  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3972 
3973  /* Create the semantics */
3974  auto node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->bvxor(op3, op4), this->astCtxt->bvtrue()), op2, op1);
3975 
3976  /* Create symbolic expression */
3977  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVL operation");
3978 
3979  /* Spread taint and condition flag */
3980  if (op3->evaluate().is_zero() != op4->evaluate().is_zero()) {
3981  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3982  inst.setConditionTaken(true);
3983  }
3984  else {
3985  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3986  }
3987 
3988  expr->isTainted |= this->taintEngine->isTainted(sf) || this->taintEngine->isTainted(of);
3989 
3990 
3991  /* Update the symbolic control flow */
3992  this->controlFlow_s(inst);
3993  }
3994 
3995 
3996  void x86Semantics::cmovle_s(triton::arch::Instruction& inst) {
3997  auto& dst = inst.operands[0];
3998  auto& src = inst.operands[1];
3999  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
4000  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
4001  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
4002 
4003  /* Create symbolic operands */
4004  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4005  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4006  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
4007  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
4008  auto op5 = this->symbolicEngine->getOperandAst(inst, zf);
4009 
4010  /* Create the semantics */
4011  auto node = this->astCtxt->ite(this->astCtxt->equal(this->astCtxt->bvor(this->astCtxt->bvxor(op3, op4), op5), this->astCtxt->bvtrue()), op2, op1);
4012 
4013  /* Create symbolic expression */
4014  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVBE operation");
4015 
4016  /* Spread taint and condition flag */
4017  if ((op3->evaluate().is_zero() != op4->evaluate().is_zero()) || !op5->evaluate().is_zero()) {
4018  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4019  inst.setConditionTaken(true);
4020  }
4021  else {
4022  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4023  }
4024 
4025  expr->isTainted |= this->taintEngine->isTainted(sf) || this->taintEngine->isTainted(of) || this->taintEngine->isTainted(zf);
4026 
4027  /* Update the symbolic control flow */
4028  this->controlFlow_s(inst);
4029  }
4030 
4031 
4032  void x86Semantics::cmovne_s(triton::arch::Instruction& inst) {
4033  auto& dst = inst.operands[0];
4034  auto& src = inst.operands[1];
4035  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
4036 
4037  /* Create symbolic operands */
4038  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4039  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4040  auto op3 = this->symbolicEngine->getOperandAst(inst, zf);
4041 
4042  /* Create the semantics */
4043  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvfalse()), op2, op1);
4044 
4045  /* Create symbolic expression */
4046  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNE operation");
4047 
4048  /* Spread taint and condition flag */
4049  if (op3->evaluate().is_zero()) {
4050  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4051  inst.setConditionTaken(true);
4052  }
4053  else {
4054  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4055  }
4056 
4057  expr->isTainted |= this->taintEngine->isTainted(zf);
4058 
4059  /* Update the symbolic control flow */
4060  this->controlFlow_s(inst);
4061  }
4062 
4063 
4064  void x86Semantics::cmovno_s(triton::arch::Instruction& inst) {
4065  auto& dst = inst.operands[0];
4066  auto& src = inst.operands[1];
4067  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
4068 
4069  /* Create symbolic operands */
4070  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4071  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4072  auto op3 = this->symbolicEngine->getOperandAst(inst, of);
4073 
4074  /* Create the semantics */
4075  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvfalse()), op2, op1);
4076 
4077  /* Create symbolic expression */
4078  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNO operation");
4079 
4080  /* Spread taint and condition flag */
4081  if (op3->evaluate().is_zero()) {
4082  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4083  inst.setConditionTaken(true);
4084  }
4085  else {
4086  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4087  }
4088 
4089  expr->isTainted |= this->taintEngine->isTainted(of);
4090 
4091  /* Update the symbolic control flow */
4092  this->controlFlow_s(inst);
4093  }
4094 
4095 
4096  void x86Semantics::cmovnp_s(triton::arch::Instruction& inst) {
4097  auto& dst = inst.operands[0];
4098  auto& src = inst.operands[1];
4099  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
4100 
4101  /* Create symbolic operands */
4102  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4103  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4104  auto op3 = this->symbolicEngine->getOperandAst(inst, pf);
4105 
4106  /* Create the semantics */
4107  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvfalse()), op2, op1);
4108 
4109  /* Create symbolic expression */
4110  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNP operation");
4111 
4112  /* Spread taint and condition flag */
4113  if (op3->evaluate().is_zero()) {
4114  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4115  inst.setConditionTaken(true);
4116  }
4117  else {
4118  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4119  }
4120 
4121  expr->isTainted |= this->taintEngine->isTainted(pf);
4122 
4123  /* Update the symbolic control flow */
4124  this->controlFlow_s(inst);
4125  }
4126 
4127 
4128  void x86Semantics::cmovns_s(triton::arch::Instruction& inst) {
4129  auto& dst = inst.operands[0];
4130  auto& src = inst.operands[1];
4131  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
4132 
4133  /* Create symbolic operands */
4134  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4135  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4136  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
4137 
4138  /* Create the semantics */
4139  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvfalse()), op2, op1);
4140 
4141  /* Create symbolic expression */
4142  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNS operation");
4143 
4144  /* Spread taint and condition flag */
4145  if (op3->evaluate().is_zero()) {
4146  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4147  inst.setConditionTaken(true);
4148  }
4149  else {
4150  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4151  }
4152 
4153  expr->isTainted |= this->taintEngine->isTainted(sf);
4154 
4155  /* Update the symbolic control flow */
4156  this->controlFlow_s(inst);
4157  }
4158 
4159 
4160  void x86Semantics::cmovo_s(triton::arch::Instruction& inst) {
4161  auto& dst = inst.operands[0];
4162  auto& src = inst.operands[1];
4163  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
4164 
4165  /* Create symbolic operands */
4166  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4167  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4168  auto op3 = this->symbolicEngine->getOperandAst(inst, of);
4169 
4170  /* Create the semantics */
4171  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvtrue()), op2, op1);
4172 
4173  /* Create symbolic expression */
4174  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVO operation");
4175 
4176  /* Spread taint and condition flag */
4177  if (!op3->evaluate().is_zero()) {
4178  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4179  inst.setConditionTaken(true);
4180  }
4181  else {
4182  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4183  }
4184 
4185  expr->isTainted |= this->taintEngine->isTainted(of);
4186 
4187  /* Update the symbolic control flow */
4188  this->controlFlow_s(inst);
4189  }
4190 
4191 
4192  void x86Semantics::cmovp_s(triton::arch::Instruction& inst) {
4193  auto& dst = inst.operands[0];
4194  auto& src = inst.operands[1];
4195  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
4196 
4197  /* Create symbolic operands */
4198  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4199  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4200  auto op3 = this->symbolicEngine->getOperandAst(inst, pf);
4201 
4202  /* Create the semantics */
4203  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvtrue()), op2, op1);
4204 
4205  /* Create symbolic expression */
4206  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVP operation");
4207 
4208  /* Spread taint and condition flag */
4209  if (!op3->evaluate().is_zero()) {
4210  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4211  inst.setConditionTaken(true);
4212  }
4213  else {
4214  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4215  }
4216 
4217  expr->isTainted |= this->taintEngine->isTainted(pf);
4218 
4219  /* Update the symbolic control flow */
4220  this->controlFlow_s(inst);
4221  }
4222 
4223 
4224  void x86Semantics::cmovs_s(triton::arch::Instruction& inst) {
4225  auto& dst = inst.operands[0];
4226  auto& src = inst.operands[1];
4227  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
4228 
4229  /* Create symbolic operands */
4230  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4231  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4232  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
4233 
4234  /* Create the semantics */
4235  auto node = this->astCtxt->ite(this->astCtxt->equal(op3, this->astCtxt->bvtrue()), op2, op1);
4236 
4237  /* Create symbolic expression */
4238  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVS operation");
4239 
4240  /* Spread taint and condition flag */
4241  if (!op3->evaluate().is_zero()) {
4242  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4243  inst.setConditionTaken(true);
4244  }
4245  else {
4246  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4247  }
4248 
4249  expr->isTainted |= this->taintEngine->isTainted(sf);
4250 
4251  /* Update the symbolic control flow */
4252  this->controlFlow_s(inst);
4253  }
4254 
4255 
4256  void x86Semantics::cmp_s(triton::arch::Instruction& inst) {
4257  auto& dst = inst.operands[0];
4258  auto& src = inst.operands[1];
4259 
4260  /* Create symbolic operands */
4261  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4262  auto op2 = this->astCtxt->sx(dst.getBitSize() - src.getBitSize(), this->symbolicEngine->getOperandAst(inst, src));
4263 
4264  /* Create the semantics */
4265  auto node = this->astCtxt->bvsub(op1, op2);
4266 
4267  /* Create symbolic expression */
4268  auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "CMP operation");
4269 
4270  /* Spread taint */
4271  expr->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4272 
4273  /* Update symbolic flags */
4274  this->af_s(inst, expr, dst, op1, op2, true);
4275  this->cfSub_s(inst, expr, dst, op1, op2, true);
4276  this->ofSub_s(inst, expr, dst, op1, op2, true);
4277  this->pf_s(inst, expr, dst, true);
4278  this->sf_s(inst, expr, dst, true);
4279  this->zf_s(inst, expr, dst, true);
4280 
4281  /* Update the symbolic control flow */
4282  this->controlFlow_s(inst);
4283  }
4284 
4285 
4286  void x86Semantics::cmpsb_s(triton::arch::Instruction& inst) {
4287  auto& dst = inst.operands[0];
4288  auto& src = inst.operands[1];
4289  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4290  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4291  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4292  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4293 
4294  /* If the REP prefix is defined, convert REP into REPE */
4297 
4298  /* Check if there is a REP prefix and a counter to zero */
4299  auto cnt = this->symbolicEngine->getOperandAst(cx);
4300  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4301  this->controlFlow_s(inst);
4302  return;
4303  }
4304 
4305  /* Create symbolic operands */
4306  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4307  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4308  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4309  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4310  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4311 
4312  /* Create the semantics */
4313  auto node1 = this->astCtxt->bvsub(op1, op2);
4314  auto node2 = this->astCtxt->ite(
4315  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4316  this->astCtxt->bvadd(op3, this->astCtxt->bv(BYTE_SIZE, index1.getBitSize())),
4317  this->astCtxt->bvsub(op3, this->astCtxt->bv(BYTE_SIZE, index1.getBitSize()))
4318  );
4319  auto node3 = this->astCtxt->ite(
4320  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4321  this->astCtxt->bvadd(op4, this->astCtxt->bv(BYTE_SIZE, index2.getBitSize())),
4322  this->astCtxt->bvsub(op4, this->astCtxt->bv(BYTE_SIZE, index2.getBitSize()))
4323  );
4324 
4325  /* Create symbolic expression */
4326  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSB operation");
4327  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4328  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4329 
4330  /* Spread taint */
4331  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4332  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4333  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4334 
4335  /* Update symbolic flags */
4336  this->af_s(inst, expr1, dst, op1, op2, true);
4337  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4338  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4339  this->pf_s(inst, expr1, dst, true);
4340  this->sf_s(inst, expr1, dst, true);
4341  this->zf_s(inst, expr1, dst, true);
4342 
4343  /* Update the symbolic control flow */
4344  this->controlFlow_s(inst);
4345  }
4346 
4347 
4348  void x86Semantics::cmpsd_s(triton::arch::Instruction& inst) {
4349  auto& dst = inst.operands[0];
4350  auto& src = inst.operands[1];
4351  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4352  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4353  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4354  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4355 
4356  /* If the REP prefix is defined, convert REP into REPE */
4359 
4360  /* Check if there is a REP prefix and a counter to zero */
4361  auto cnt = this->symbolicEngine->getOperandAst(cx);
4362  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4363  this->controlFlow_s(inst);
4364  return;
4365  }
4366 
4367  /* Create symbolic operands */
4368  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4369  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4370  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4371  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4372  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4373 
4374  /* Create the semantics */
4375  auto node1 = this->astCtxt->bvsub(op1, op2);
4376  auto node2 = this->astCtxt->ite(
4377  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4378  this->astCtxt->bvadd(op3, this->astCtxt->bv(DWORD_SIZE, index1.getBitSize())),
4379  this->astCtxt->bvsub(op3, this->astCtxt->bv(DWORD_SIZE, index1.getBitSize()))
4380  );
4381  auto node3 = this->astCtxt->ite(
4382  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4383  this->astCtxt->bvadd(op4, this->astCtxt->bv(DWORD_SIZE, index2.getBitSize())),
4384  this->astCtxt->bvsub(op4, this->astCtxt->bv(DWORD_SIZE, index2.getBitSize()))
4385  );
4386 
4387  /* Create symbolic expression */
4388  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSD operation");
4389  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4390  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4391 
4392  /* Spread taint */
4393  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4394  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4395  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4396 
4397  /* Update symbolic flags */
4398  this->af_s(inst, expr1, dst, op1, op2, true);
4399  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4400  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4401  this->pf_s(inst, expr1, dst, true);
4402  this->sf_s(inst, expr1, dst, true);
4403  this->zf_s(inst, expr1, dst, true);
4404 
4405  /* Update the symbolic control flow */
4406  this->controlFlow_s(inst);
4407  }
4408 
4409 
4410  void x86Semantics::cmpsq_s(triton::arch::Instruction& inst) {
4411  auto& dst = inst.operands[0];
4412  auto& src = inst.operands[1];
4413  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4414  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4415  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4416  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4417 
4418  /* If the REP prefix is defined, convert REP into REPE */
4421 
4422  /* Check if there is a REP prefix and a counter to zero */
4423  auto cnt = this->symbolicEngine->getOperandAst(cx);
4424  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4425  this->controlFlow_s(inst);
4426  return;
4427  }
4428 
4429  /* Create symbolic operands */
4430  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4431  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4432  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4433  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4434  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4435 
4436  /* Create the semantics */
4437  auto node1 = this->astCtxt->bvsub(op1, op2);
4438  auto node2 = this->astCtxt->ite(
4439  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4440  this->astCtxt->bvadd(op3, this->astCtxt->bv(QWORD_SIZE, index1.getBitSize())),
4441  this->astCtxt->bvsub(op3, this->astCtxt->bv(QWORD_SIZE, index1.getBitSize()))
4442  );
4443  auto node3 = this->astCtxt->ite(
4444  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4445  this->astCtxt->bvadd(op4, this->astCtxt->bv(QWORD_SIZE, index2.getBitSize())),
4446  this->astCtxt->bvsub(op4, this->astCtxt->bv(QWORD_SIZE, index2.getBitSize()))
4447  );
4448 
4449  /* Create symbolic expression */
4450  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSQ operation");
4451  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4452  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4453 
4454  /* Spread taint */
4455  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4456  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4457  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4458 
4459  /* Update symbolic flags */
4460  this->af_s(inst, expr1, dst, op1, op2, true);
4461  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4462  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4463  this->pf_s(inst, expr1, dst, true);
4464  this->sf_s(inst, expr1, dst, true);
4465  this->zf_s(inst, expr1, dst, true);
4466 
4467  /* Update the symbolic control flow */
4468  this->controlFlow_s(inst);
4469  }
4470 
4471 
4472  void x86Semantics::cmpsw_s(triton::arch::Instruction& inst) {
4473  auto& dst = inst.operands[0];
4474  auto& src = inst.operands[1];
4475  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4476  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4477  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4478  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4479 
4480  /* If the REP prefix is defined, convert REP into REPE */
4483 
4484  /* Check if there is a REP prefix and a counter to zero */
4485  auto cnt = this->symbolicEngine->getOperandAst(cx);
4486  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4487  this->controlFlow_s(inst);
4488  return;
4489  }
4490 
4491  /* Create symbolic operands */
4492  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4493  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4494  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4495  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4496  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4497 
4498  /* Create the semantics */
4499  auto node1 = this->astCtxt->bvsub(op1, op2);
4500  auto node2 = this->astCtxt->ite(
4501  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4502  this->astCtxt->bvadd(op3, this->astCtxt->bv(WORD_SIZE, index1.getBitSize())),
4503  this->astCtxt->bvsub(op3, this->astCtxt->bv(WORD_SIZE, index1.getBitSize()))
4504  );
4505  auto node3 = this->astCtxt->ite(
4506  this->astCtxt->equal(op5, this->astCtxt->bvfalse()),
4507  this->astCtxt->bvadd(op4, this->astCtxt->bv(WORD_SIZE, index2.getBitSize())),
4508  this->astCtxt->bvsub(op4, this->astCtxt->bv(WORD_SIZE, index2.getBitSize()))
4509  );
4510 
4511  /* Create symbolic expression */
4512  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSW operation");
4513  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4514  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4515 
4516  /* Spread taint */
4517  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4518  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4519  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4520 
4521  /* Update symbolic flags */
4522  this->af_s(inst, expr1, dst, op1, op2, true);
4523  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4524  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4525  this->pf_s(inst, expr1, dst, true);
4526  this->sf_s(inst, expr1, dst, true);
4527  this->zf_s(inst, expr1, dst, true);
4528 
4529  /* Update the symbolic control flow */
4530  this->controlFlow_s(inst);
4531  }
4532 
4533 
4534  void x86Semantics::cmpxchg_s(triton::arch::Instruction& inst) {
4535  auto& src1 = inst.operands[0];
4536  auto& src2 = inst.operands[1];
4537 
4538  /* Create the tempory accumulator */
4539  triton::arch::OperandWrapper accumulator(this->architecture->getRegister(ID_REG_X86_AL));
4540  triton::arch::OperandWrapper accumulatorp(this->architecture->getParentRegister(ID_REG_X86_AL));
4541 
4542  switch (src1.getSize()) {
4543  case WORD_SIZE:
4544  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_AX)));
4545  break;
4546  case DWORD_SIZE:
4547  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_EAX)));
4548  break;
4549  case QWORD_SIZE:
4550  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_RAX)));
4551  break;
4552  }
4553 
4554  /* Create symbolic operands */
4555  auto op1 = this->symbolicEngine->getOperandAst(inst, accumulator);
4556  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
4557  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
4558  auto op1p = this->symbolicEngine->getOperandAst(accumulatorp);
4559  auto op2p = this->symbolicEngine->getRegisterAst((src1.getType() == triton::arch::OP_REG ? Register(this->architecture->getParentRegister(src1.getRegister())) : accumulatorp.getRegister()));
4560  auto op3p = this->symbolicEngine->getRegisterAst((src1.getType() == triton::arch::OP_REG ? Register(this->architecture->getParentRegister(src2.getRegister())) : accumulatorp.getRegister()));
4561 
4562  /* Create the semantics */
4563  auto nodeq = this->astCtxt->equal(op1, op2);
4564  auto node1 = this->astCtxt->bvsub(op1, op2);
4565  auto node2 = this->astCtxt->ite(nodeq, op3, op2);
4566  auto node3 = this->astCtxt->ite(nodeq, op1, op2);
4567  auto node2p = this->astCtxt->ite(nodeq, op3p, op2p);
4568  auto node3p = this->astCtxt->ite(nodeq, op1p, op2p);
4569 
4570  /* Create symbolic expression */
4571  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4572  auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, "Temporary operation");
4573  auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2p, "Temporary operation");
4574  auto expr4 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, "Temporary operation");
4575  auto expr5 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3p, "Temporary operation");
4576 
4579 
4580  /* Destination */
4581  if (nodeq->evaluate() == false && src1.getType() == triton::arch::OP_REG) {
4582  const auto& src1p = this->architecture->getParentRegister(src1.getRegister());
4583  expr6 = this->symbolicEngine->createSymbolicRegisterExpression(inst, node2p, src1p, "XCHG operation");
4584  } else
4585  expr6 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG operation");
4586 
4587  /* Accumulator */
4588  if (nodeq->evaluate() == true)
4589  expr7 = this->symbolicEngine->createSymbolicExpression(inst, node3p, accumulatorp, "XCHG operation");
4590  else
4591  expr7 = this->symbolicEngine->createSymbolicExpression(inst, node3, accumulator, "XCHG operation");
4592 
4593  /* Spread taint */
4594  expr1->isTainted = this->taintEngine->isTainted(accumulator) | this->taintEngine->isTainted(src1);
4595  expr2->isTainted = expr1->isTainted;
4596  expr3->isTainted = expr1->isTainted;
4597  expr4->isTainted = expr1->isTainted;
4598  expr5->isTainted = expr1->isTainted;
4599  expr6->isTainted = this->taintEngine->taintAssignment(src1, src2);
4600  expr7->isTainted = this->taintEngine->taintAssignment(accumulator, src1);
4601 
4602  /* Update symbolic flags */
4603  this->af_s(inst, expr1, accumulator, op1, op2, true);
4604  this->cfSub_s(inst, expr1, accumulator, op1, op2, true);
4605  this->ofSub_s(inst, expr1, accumulator, op1, op2, true);
4606  this->pf_s(inst, expr1, accumulator, true);
4607  this->sf_s(inst, expr1, accumulator, true);
4608  this->zf_s(inst, expr1, accumulator, true);
4609 
4610  /* Update the symbolic control flow */
4611  this->controlFlow_s(inst);
4612  }
4613 
4614 
4615  void x86Semantics::cmpxchg16b_s(triton::arch::Instruction& inst) {
4616  auto& src1 = inst.operands[0];
4617  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
4618  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
4619  auto src4 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RCX));
4620  auto src5 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RBX));
4621 
4622  /* Create symbolic operands */
4623  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
4624  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
4625  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
4626  auto op4 = this->symbolicEngine->getOperandAst(inst, src4);
4627  auto op5 = this->symbolicEngine->getOperandAst(inst, src5);
4628 
4629  /* Create the semantics */
4630  /* CMP8B */
4631  auto node1 = this->astCtxt->bvsub(this->astCtxt->concat(op2, op3), op1);
4632  /* Destination */
4633  auto node2 = this->astCtxt->ite(this->astCtxt->equal(node1, this->astCtxt->bv(0, DQWORD_SIZE_BIT)), this->astCtxt->concat(op4, op5), op1);
4634  /* EDX:EAX */
4635  auto node3 = this->astCtxt->ite(this->astCtxt->equal(node1, this->astCtxt->bv(0, DQWORD_SIZE_BIT)), this->astCtxt->concat(op2, op3), op1);
4636 
4637  /* Create symbolic expression */
4638  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4639  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG16B memory operation");
4640  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(127, 64, node3), src2, "XCHG16B RDX operation");
4641  auto expr4 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(63, 0, node3), src3, "XCHG16B RAX operation");
4642 
4643  /* Spread taint */
4644  expr1->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4645  expr2->isTainted = this->taintEngine->setTaint(src1, this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
4646  expr3->isTainted = this->taintEngine->taintAssignment(src2, src1);
4647  expr4->isTainted = this->taintEngine->taintAssignment(src3, src1);
4648 
4649  /* Update symbolic flags */
4650  this->zf_s(inst, expr1, src1, true);
4651 
4652  /* Update the symbolic control flow */
4653  this->controlFlow_s(inst);
4654  }
4655 
4656 
4657  void x86Semantics::cmpxchg8b_s(triton::arch::Instruction& inst) {
4658  auto& src1 = inst.operands[0];
4659  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
4660  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
4661  auto src4 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ECX));
4662  auto src5 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EBX));
4663  auto src2p = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_EDX));
4664  auto src3p = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_EAX));
4665 
4666  /* Create symbolic operands */
4667  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
4668  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
4669  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
4670  auto op4 = this->symbolicEngine->getOperandAst(inst, src4);
4671  auto op5 = this->symbolicEngine->getOperandAst(inst, src5);
4672  auto op2p = this->symbolicEngine->getOperandAst(inst, src2p);
4673  auto op3p = this->symbolicEngine->getOperandAst(inst, src3p);
4674 
4675  /* Create the semantics */
4676  /* CMP8B */
4677  auto node1 = this->astCtxt->bvsub(this->astCtxt->concat(op2, op3), op1);
4678  /* Destination */
4679  auto node2 = this->astCtxt->ite(this->astCtxt->equal(node1, this->astCtxt->bv(0, QWORD_SIZE_BIT)), this->astCtxt->concat(op4, op5), op1);
4680  /* EDX:EAX */
4681  auto node3 = this->astCtxt->ite(this->astCtxt->equal(node1, this->astCtxt->bv(0, QWORD_SIZE_BIT)), this->astCtxt->concat(op2, op3), op1);
4682  auto node3p = this->astCtxt->ite(
4683  this->astCtxt->equal(
4684  node1,
4685  this->astCtxt->bv(0, QWORD_SIZE_BIT)),
4686  this->astCtxt->concat(op2p, op3p),
4687  this->astCtxt->zx(src2p.getBitSize() + src3p.getBitSize() - src1.getBitSize(), op1)
4688  );
4689 
4690  /* Create symbolic expression */
4691  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4692  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG8B memory operation");
4693  auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, "Temporary operation");
4694  auto expr4 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3p, "Temporary operation");
4695 
4698 
4699  /* EDX */
4700  if (node1->evaluate() == 0)
4701  expr5 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract((src2p.getBitSize() * 2 - 1), src2p.getBitSize(), node3p), src2p, "XCHG8B EDX operation");
4702  else
4703  expr5 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(63, 32, node3), src2, "XCHG8B EDX operation");
4704 
4705  /* EAX */
4706  if (node1->evaluate() == 0)
4707  expr6 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(src2p.getBitSize() - 1, 0, node3p), src3p, "XCHG8B EAX operation");
4708  else
4709  expr6 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(31, 0, node3), src3, "XCHG8B EAX operation");
4710 
4711  /* Spread taint */
4712  expr1->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4713  expr2->isTainted = this->taintEngine->setTaint(src1, this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
4714  expr3->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4715  expr4->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4716  expr5->isTainted = this->taintEngine->taintAssignment(src2, src1);
4717  expr6->isTainted = this->taintEngine->taintAssignment(src3, src1);
4718 
4719  /* Update symbolic flags */
4720  this->zf_s(inst, expr1, src1, true);
4721 
4722  /* Update the symbolic control flow */
4723  this->controlFlow_s(inst);
4724  }
4725 
4726 
4727  void x86Semantics::cpuid_s(triton::arch::Instruction& inst) {
4728  auto src = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_AX));
4729  auto dst1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_AX));
4730  auto dst2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_BX));
4731  auto dst3 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4732  auto dst4 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DX));
4733 
4734  /* Create symbolic operands */
4735  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
4736 
4737  /* Create the semantics */
4738  triton::ast::SharedAbstractNode node1 = nullptr;
4739  triton::ast::SharedAbstractNode node2 = nullptr;
4740  triton::ast::SharedAbstractNode node3 = nullptr;
4741  triton::ast::SharedAbstractNode node4 = nullptr;
4742 
4743  /* In this case, we concretize the AX option */
4744  switch (op1->evaluate().convert_to<triton::uint32>()) {
4745  case 0:
4746  node1 = this->astCtxt->bv(0x0000000d, dst1.getBitSize());
4747  node2 = this->astCtxt->bv(0x756e6547, dst2.getBitSize());
4748  node3 = this->astCtxt->bv(0x6c65746e, dst3.getBitSize());
4749  node4 = this->astCtxt->bv(0x49656e69, dst4.getBitSize());
4750  break;
4751  case 1:
4752  node1 = this->astCtxt->bv(0x000306a9, dst1.getBitSize());
4753  node2 = this->astCtxt->bv(0x02100800, dst2.getBitSize());
4754  node3 = this->astCtxt->bv(0x7fbae3ff, dst3.getBitSize());
4755  node4 = this->astCtxt->bv(0xbfebfbff, dst4.getBitSize());
4756  break;
4757  case 2:
4758  node1 = this->astCtxt->bv(0x76035a01, dst1.getBitSize());
4759  node2 = this->astCtxt->bv(0x00f0b2ff, dst2.getBitSize());
4760  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4761  node4 = this->astCtxt->bv(0x00ca0000, dst4.getBitSize());
4762  break;
4763  case 3:
4764  node1 = this->astCtxt->bv(0x00000000, dst1.getBitSize());
4765  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4766  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4767  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4768  break;
4769  case 4:
4770  node1 = this->astCtxt->bv(0x1c004121, dst1.getBitSize());
4771  node2 = this->astCtxt->bv(0x01c0003f, dst2.getBitSize());
4772  node3 = this->astCtxt->bv(0x0000003f, dst3.getBitSize());
4773  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4774  break;
4775  case 5:
4776  node1 = this->astCtxt->bv(0x00000040, dst1.getBitSize());
4777  node2 = this->astCtxt->bv(0x00000040, dst2.getBitSize());
4778  node3 = this->astCtxt->bv(0x00000003, dst3.getBitSize());
4779  node4 = this->astCtxt->bv(0x00021120, dst4.getBitSize());
4780  break;
4781  case 0x80000000:
4782  node1 = this->astCtxt->bv(0x80000008, dst1.getBitSize());
4783  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4784  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4785  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4786  break;
4787  case 0x80000001:
4788  node1 = this->astCtxt->bv(0x00000000, dst1.getBitSize());
4789  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4790  node3 = this->astCtxt->bv(0x00000001, dst3.getBitSize());
4791  node4 = this->astCtxt->bv(0x28100800, dst4.getBitSize());
4792  break;
4793  case 0x80000002:
4794  node1 = this->astCtxt->bv(0x20202020, dst1.getBitSize());
4795  node2 = this->astCtxt->bv(0x49202020, dst2.getBitSize());
4796  node3 = this->astCtxt->bv(0x6c65746e, dst3.getBitSize());
4797  node4 = this->astCtxt->bv(0x20295228, dst4.getBitSize());
4798  break;
4799  case 0x80000003:
4800  node1 = this->astCtxt->bv(0x65726f43, dst1.getBitSize());
4801  node2 = this->astCtxt->bv(0x294d5428, dst2.getBitSize());
4802  node3 = this->astCtxt->bv(0x2d376920, dst3.getBitSize());
4803  node4 = this->astCtxt->bv(0x30323533, dst4.getBitSize());
4804  break;
4805  case 0x80000004:
4806  node1 = this->astCtxt->bv(0x5043204d, dst1.getBitSize());
4807  node2 = this->astCtxt->bv(0x20402055, dst2.getBitSize());
4808  node3 = this->astCtxt->bv(0x30392e32, dst3.getBitSize());
4809  node4 = this->astCtxt->bv(0x007a4847, dst4.getBitSize());
4810  break;
4811  case 0x80000005:
4812  node1 = this->astCtxt->bv(0x00000000, dst1.getBitSize());
4813  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4814  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4815  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4816  break;
4817  case 0x80000006:
4818  node1 = this->astCtxt->bv(0x00000000, dst1.getBitSize());
4819  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4820  node3 = this->astCtxt->bv(0x01006040, dst3.getBitSize());
4821  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4822  break;
4823  case 0x80000007:
4824  node1 = this->astCtxt->bv(0x00000000, dst1.getBitSize());
4825  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4826  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4827  node4 = this->astCtxt->bv(0x00000100, dst4.getBitSize());
4828  break;
4829  case 0x80000008:
4830  node1 = this->astCtxt->bv(0x00003024, dst1.getBitSize());
4831  node2 = this->astCtxt->bv(0x00000000, dst2.getBitSize());
4832  node3 = this->astCtxt->bv(0x00000000, dst3.getBitSize());
4833  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4834  break;
4835  default:
4836  node1 = this->astCtxt->bv(0x00000007, dst1.getBitSize());
4837  node2 = this->astCtxt->bv(0x00000340, dst2.getBitSize());
4838  node3 = this->astCtxt->bv(0x00000340, dst3.getBitSize());
4839  node4 = this->astCtxt->bv(0x00000000, dst4.getBitSize());
4840  break;
4841  }
4842 
4843  /* Create symbolic expression */
4844  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "CPUID AX operation");
4845  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "CPUID BX operation");
4846  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, dst3, "CPUID CX operation");
4847  auto expr4 = this->symbolicEngine->createSymbolicExpression(inst, node4, dst4, "CPUID DX operation");
4848 
4849  /* Spread taint */
4850  expr1->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_AX), false);
4851  expr2->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_BX), false);
4852  expr3->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_CX), false);
4853  expr4->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_DX), false);
4854 
4855  /* Update the symbolic control flow */
4856  this->controlFlow_s(inst);
4857  }
4858 
4859 
4860  void x86Semantics::cqo_s(triton::arch::Instruction& inst) {
4861  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
4862  auto src = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
4863 
4864  /* Create symbolic operands */
4865  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
4866 
4867  /* Create the semantics - TMP = 128 bitvec (RDX:RAX) */
4868  auto node1 = this->astCtxt->sx(QWORD_SIZE_BIT, op1);
4869 
4870  /* Create symbolic expression */
4871  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "Temporary variable");
4872 
4873  /* Spread taint */
4874  expr1->isTainted = this->taintEngine->isRegisterTainted(this->architecture->getRegister(ID_REG_X86_RAX));
4875 
4876  /* Create the semantics - RDX = TMP[127...64] */
4877  auto node2 = this->astCtxt->extract(DQWORD_SIZE_BIT-1, QWORD_SIZE_BIT, this->astCtxt->reference(expr1));
4878 
4879  /* Create symbolic expression */
4880  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst, "CQO operation");
4881 
4882  /* Spread taint */
4883  expr2->isTainted = this->taintEngine->taintAssignment(dst, src);
4884 
4885  /* Update the symbolic control flow */
4886  this->controlFlow_s(inst);
4887  }
4888 
4889 
4890  void x86Semantics::cwd_s(triton::arch::Instruction& inst) {
4891  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DX));
4892  auto src = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
4893 
4894  /* Create symbolic operands */
4895  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
4896 
4897  /* Create the semantics - TMP = 32 bitvec (DX:AX) */
4898  auto node1 = this->astCtxt->sx(WORD_SIZE_BIT, op1);
4899 
4900  /* Create symbolic expression */
4901  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "Temporary variable");
4902 
4903  /* Spread taint */
4904  expr1->isTainted = this->taintEngine->isRegisterTainted(this->architecture->getRegister(ID_REG_X86_AX));
4905 
4906  /* Create the semantics - DX = TMP[31...16] */
4907  auto node2 = this->astCtxt->extract(DWORD_SIZE_BIT-1, WORD_SIZE_BIT, this->astCtxt->reference(expr1));
4908 
4909  /* Create symbolic expression */
4910  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst, "CWD operation");
4911 
4912  /* Spread taint */
4913  expr2->isTainted = this->taintEngine->taintAssignment(dst, src);
4914 
4915  /* Update the symbolic control flow */
4916  this->controlFlow_s(inst);
4917  }
4918 
4919 
4920  void x86Semantics::cwde_s(triton::arch::Instruction& inst) {
4921  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
4922 
4923  /* Create symbolic operands */
4924  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4925 
4926  /* Create the semantics */
4927  auto node = this->astCtxt->sx(WORD_SIZE_BIT, this->astCtxt->extract(WORD_SIZE_BIT-1, 0, op1));
4928 
4929  /* Create symbolic expression */
4930  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CWDE operation");
4931 
4932  /* Spread taint */
4933  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
4934 
4935  /* Update the symbolic control flow */
4936  this->controlFlow_s(inst);
4937  }
4938 
4939 
4940  void x86Semantics::dec_s(triton::arch::Instruction& inst) {
4941  auto& dst = inst.operands[0];
4942 
4943  /* Create symbolic operands */
4944  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4945  auto op2 = this->astCtxt->bv(1, dst.getBitSize());
4946 
4947  /* Create the semantics */
4948  auto node = this->astCtxt->bvsub(op1, op2);
4949 
4950  /* Create symbolic expression */
4951  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "DEC operation");
4952 
4953  /* Spread taint */
4954  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4955 
4956  /* Update symbolic flags */
4957  this->af_s(inst, expr, dst, op1, op2);
4958  this->ofSub_s(inst, expr, dst, op1, op2);
4959  this->pf_s(inst, expr, dst);
4960  this->sf_s(inst, expr, dst);
4961  this->zf_s(inst, expr, dst);
4962 
4963  /* Update the symbolic control flow */
4964  this->controlFlow_s(inst);
4965  }
4966 
4967 
4968  void x86Semantics::div_s(triton::arch::Instruction& inst) {
4969  auto& src = inst.operands[0];
4970 
4971  /* Create symbolic operands */
4972  auto divisor = this->symbolicEngine->getOperandAst(inst, src);
4973 
4974  /* Create symbolic expression */
4975  switch (src.getSize()) {
4976 
4977  case BYTE_SIZE: {
4978  /* AX */
4979  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
4980  auto dividend = this->symbolicEngine->getOperandAst(inst, ax);
4981  /* res = AX / Source */
4982  auto result = this->astCtxt->bvudiv(dividend, this->astCtxt->zx(BYTE_SIZE_BIT, divisor));
4983  /* mod = AX % Source */
4984  auto mod = this->astCtxt->bvurem(dividend, this->astCtxt->zx(BYTE_SIZE_BIT, divisor));
4985  /* AH = mod */
4986  /* AL = res */
4987  auto node = this->astCtxt->concat(
4988  this->astCtxt->extract((BYTE_SIZE_BIT - 1), 0, mod), /* AH = mod */
4989  this->astCtxt->extract((BYTE_SIZE_BIT - 1), 0, result) /* AL = res */
4990  );
4991  /* Create symbolic expression */
4992  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, ax, "DIV operation");
4993  /* Apply the taint */
4994  expr->isTainted = this->taintEngine->taintUnion(ax, src);
4995  break;
4996  }
4997 
4998  case WORD_SIZE: {
4999  /* DX:AX */
5000  auto dx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DX));
5001  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
5002  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, dx), this->symbolicEngine->getOperandAst(inst, ax));
5003  /* res = DX:AX / Source */
5004  auto result = this->astCtxt->extract((WORD_SIZE_BIT - 1), 0, this->astCtxt->bvudiv(dividend, this->astCtxt->zx(WORD_SIZE_BIT, divisor)));
5005  /* mod = DX:AX % Source */
5006  auto mod = this->astCtxt->extract((WORD_SIZE_BIT - 1), 0, this->astCtxt->bvurem(dividend, this->astCtxt->zx(WORD_SIZE_BIT, divisor)));
5007  /* Create the symbolic expression for AX */
5008  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, ax, "DIV operation");
5009  /* Apply the taint for AX */
5010  expr1->isTainted = this->taintEngine->taintUnion(ax, src);
5011  /* Create the symbolic expression for DX */
5012  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, dx, "DIV operation");
5013  /* Apply the taint for DX */
5014  expr2->isTainted = this->taintEngine->taintUnion(dx, src);
5015  break;
5016  }
5017 
5018  case DWORD_SIZE: {
5019  /* EDX:EAX */
5020  auto edx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
5021  auto eax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
5022  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, edx), this->symbolicEngine->getOperandAst(inst, eax));
5023  /* res = EDX:EAX / Source */
5024  auto result = this->astCtxt->extract((DWORD_SIZE_BIT - 1), 0, this->astCtxt->bvudiv(dividend, this->astCtxt->zx(DWORD_SIZE_BIT, divisor)));
5025  /* mod = EDX:EAX % Source */
5026  auto mod = this->astCtxt->extract((DWORD_SIZE_BIT - 1), 0, this->astCtxt->bvurem(dividend, this->astCtxt->zx(DWORD_SIZE_BIT, divisor)));
5027  /* Create the symbolic expression for EAX */
5028  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, eax, "DIV operation");
5029  /* Apply the taint for EAX */
5030  expr1->isTainted = this->taintEngine->taintUnion(eax, src);
5031  /* Create the symbolic expression for EDX */
5032  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, edx, "DIV operation");
5033  /* Apply the taint for EDX */
5034  expr2->isTainted = this->taintEngine->taintUnion(edx, src);
5035  break;
5036  }
5037 
5038  case QWORD_SIZE: {
5039  /* RDX:RAX */
5040  auto rdx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
5041  auto rax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
5042  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, rdx), this->symbolicEngine->getOperandAst(inst, rax));
5043  /* res = RDX:RAX / Source */
5044  auto result = this->astCtxt->extract((QWORD_SIZE_BIT - 1), 0, this->astCtxt->bvudiv(dividend, this->astCtxt->zx(QWORD_SIZE_BIT, divisor)));
5045  /* mod = RDX:RAX % Source */
5046  auto mod = this->astCtxt->extract((QWORD_SIZE_BIT - 1), 0, this->astCtxt->bvurem(dividend, this->astCtxt->zx(QWORD_SIZE_BIT, divisor)));
5047  /* Create the symbolic expression for RAX */
5048  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, rax, "DIV operation");
5049  /* Apply the taint for EAX */
5050  expr1->isTainted = this->taintEngine->taintUnion(rax, src);
5051  /* Create the symbolic expression for RDX */
5052  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, rdx, "DIV operation");
5053  /* Apply the taint for EDX */
5054  expr2->isTainted = this->taintEngine->taintUnion(rdx, src);
5055  break;
5056  }
5057 
5058  }
5059 
5060  /* Tag undefined flags */
5061  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
5062  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
5063  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
5064  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
5065  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
5066  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
5067 
5068  /* Update the symbolic control flow */
5069  this->controlFlow_s(inst);
5070  }
5071 
5072 
5073  void x86Semantics::extractps_s(triton::arch::Instruction& inst) {
5074  auto& dst = inst.operands[0];
5075  auto& src1 = inst.operands[1];
5076  auto& src2 = inst.operands[2];
5077 
5078  /* Create symbolic operands */
5079  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
5080  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
5081 
5082  /* Create the semantics */
5083  auto node = this->astCtxt->extract(DWORD_SIZE_BIT-1, 0,
5084  this->astCtxt->bvlshr(
5085  op2,
5086  this->astCtxt->bvmul(
5087  this->astCtxt->zx(126, this->astCtxt->extract(1, 0, op3)),
5088  this->astCtxt->bv(DWORD_SIZE_BIT, DQWORD_SIZE_BIT)
5089  )
5090  )
5091  );
5092 
5093  switch (dst.getBitSize()) {
5094  case DWORD_SIZE_BIT:
5095  break;
5096  case QWORD_SIZE_BIT:
5097  node = this->astCtxt->zx(DWORD_SIZE_BIT, node);
5098  break;
5099  default:
5100  throw triton::exceptions::Semantics("x86Semantics::extractps_s(): Invalid destination operand.");
5101  }
5102 
5103  /* Create symbolic expression */
5104  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EXTRACTPS operation");
5105 
5106  /* Spread taint */
5107  expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
5108 
5109  /* Update the symbolic control flow */
5110  this->controlFlow_s(inst);
5111  }
5112 
5113 
5114  void x86Semantics::idiv_s(triton::arch::Instruction& inst) {
5115  auto& src = inst.operands[0];
5116 
5117  /* Create symbolic operands */
5118  auto divisor = this->symbolicEngine->getOperandAst(inst, src);
5119 
5120  /* Create symbolic expression */
5121  switch (src.getSize()) {
5122 
5123  case BYTE_SIZE: {
5124  /* AX */
5125  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
5126  auto dividend = this->symbolicEngine->getOperandAst(inst, ax);
5127  /* res = AX / Source */
5128  auto result = this->astCtxt->bvsdiv(dividend, this->astCtxt->sx(BYTE_SIZE_BIT, divisor));
5129  /* mod = AX % Source */
5130  auto mod = this->astCtxt->bvsrem(dividend, this->astCtxt->sx(BYTE_SIZE_BIT, divisor));
5131  /* AH = mod */
5132  /* AL = res */
5133  auto node = this->astCtxt->concat(
5134  this->astCtxt->extract((BYTE_SIZE_BIT - 1), 0, mod), /* AH = mod */
5135  this->astCtxt->extract((BYTE_SIZE_BIT - 1), 0, result) /* AL = res */
5136  );
5137  /* Create symbolic expression */
5138  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, ax, "IDIV operation");
5139  /* Apply the taint */
5140  expr->isTainted = this->taintEngine->taintUnion(ax, src);
5141  break;
5142  }
5143 
5144  case WORD_SIZE: {
5145  /* DX:AX */
5146  auto dx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DX));
5147  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
5148  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, dx), this->symbolicEngine->getOperandAst(inst, ax));
5149  /* res = DX:AX / Source */
5150  auto result = this->astCtxt->extract((WORD_SIZE_BIT - 1), 0, this->astCtxt->bvsdiv(dividend, this->astCtxt->sx(WORD_SIZE_BIT, divisor)));
5151  /* mod = DX:AX % Source */
5152  auto mod = this->astCtxt->extract((WORD_SIZE_BIT - 1), 0, this->astCtxt->bvsrem(dividend, this->astCtxt->sx(WORD_SIZE_BIT, divisor)));
5153  /* Create the symbolic expression for AX */
5154  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, ax, "IDIV operation");
5155  /* Apply the taint for AX */
5156  expr1->isTainted = this->taintEngine->taintUnion(ax, src);
5157  /* Create the symbolic expression for DX */
5158  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, dx, "IDIV operation");
5159  /* Apply the taint for DX */
5160  expr2->isTainted = this->taintEngine->taintUnion(dx, src);
5161  break;
5162  }
5163 
5164  case DWORD_SIZE: {
5165  /* EDX:EAX */
5166  auto edx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
5167  auto eax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
5168  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, edx), this->symbolicEngine->getOperandAst(inst, eax));
5169  /* res = EDX:EAX / Source */
5170  auto result = this->astCtxt->extract((DWORD_SIZE_BIT - 1), 0, this->astCtxt->bvsdiv(dividend, this->astCtxt->sx(DWORD_SIZE_BIT, divisor)));
5171  /* mod = EDX:EAX % Source */
5172  auto mod = this->astCtxt->extract((DWORD_SIZE_BIT - 1), 0, this->astCtxt->bvsrem(dividend, this->astCtxt->sx(DWORD_SIZE_BIT, divisor)));
5173  /* Create the symbolic expression for EAX */
5174  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, eax, "IDIV operation");
5175  /* Apply the taint for EAX */
5176  expr1->isTainted = this->taintEngine->taintUnion(eax, src);
5177  /* Create the symbolic expression for EDX */
5178  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, edx, "IDIV operation");
5179  /* Apply the taint for EDX */
5180  expr2->isTainted = this->taintEngine->taintUnion(edx, src);
5181  break;
5182  }
5183 
5184  case QWORD_SIZE: {
5185  /* RDX:RAX */
5186  auto rdx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
5187  auto rax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
5188  auto dividend = this->astCtxt->concat(this->symbolicEngine->getOperandAst(inst, rdx), this->symbolicEngine->getOperandAst(inst, rax));
5189  /* res = RDX:RAX / Source */
5190  auto result = this->astCtxt->extract((QWORD_SIZE_BIT - 1), 0, this->astCtxt->bvsdiv(dividend, this->astCtxt->sx(QWORD_SIZE_BIT, divisor)));
5191  /* mod = RDX:RAX % Source */
5192  auto mod = this->astCtxt->extract((QWORD_SIZE_BIT - 1), 0, this->astCtxt->bvsrem(dividend, this->astCtxt->sx(QWORD_SIZE_BIT, divisor)));
5193  /* Create the symbolic expression for RAX */
5194  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, result, rax, "IDIV operation");
5195  /* Apply the taint for EAX */
5196  expr1->isTainted = this->taintEngine->taintUnion(rax, src);
5197  /* Create the symbolic expression for RDX */
5198  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, mod, rdx, "IDIV operation");
5199  /* Apply the taint for EDX */
5200  expr2->isTainted = this->taintEngine->taintUnion(rdx, src);
5201  break;
5202  }
5203 
5204  }
5205 
5206  /* Tag undefined flags */
5207  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
5208  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
5209  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
5210  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
5211  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
5212  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
5213 
5214  /* Update the symbolic control flow */
5215  this->controlFlow_s(inst);
5216  }
5217 
5218 
5219  void x86Semantics::imul_s(triton::arch::Instruction& inst) {
5220  switch (inst.operands.size()) {
5221 
5222  /* one operand */
5223  case 1: {
5224  auto& src = inst.operands[0];
5225 
5226  /* size of the Operand */
5227  switch (src.getSize()) {
5228 
5229  /* dst = AX */
5230  case BYTE_SIZE: {
5231  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
5232  auto al = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
5233  auto op1 = this->symbolicEngine->getOperandAst(inst, al);
5234  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
5235  auto node = this->astCtxt->bvmul(this->astCtxt->sx(BYTE_SIZE_BIT, op1), this->astCtxt->sx(BYTE_SIZE_BIT, op2));
5236  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, ax, "IMUL operation");
5237  expr->isTainted = this->taintEngine->taintUnion(ax, src);
5238  this->cfImul_s(inst, expr, al, this->astCtxt->bvmul(op1, op2), node);
5239  this->ofImul_s(inst, expr, al, this->astCtxt->bvmul(op1, op2), node);
5240  break;
5241  }
5242 
5243  /* dst = DX:AX */
5244  case WORD_SIZE: {
5245  auto ax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
5246  auto dx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DX));
5247  auto op1 = this->symbolicEngine->getOperandAst(inst, ax);
5248  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
5249  auto node = this->astCtxt->bvmul(this->astCtxt->sx(WORD_SIZE_BIT, op1), this->astCtxt->sx(WORD_SIZE_BIT, op2));
5250  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(WORD_SIZE_BIT-1, 0, node), ax, "IMUL operation");
5251  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(DWORD_SIZE_BIT-1, WORD_SIZE_BIT, node), dx, "IMUL operation");
5252  expr1->isTainted = this->taintEngine->taintUnion(ax, src);
5253  expr2->isTainted = this->taintEngine->taintUnion(dx, ax);
5254  this->cfImul_s(inst, expr1, ax, this->astCtxt->bvmul(op1, op2), node);
5255  this->ofImul_s(inst, expr1, ax, this->astCtxt->bvmul(op1, op2), node);
5256  break;
5257  }
5258 
5259  /* dst = EDX:EAX */
5260  case DWORD_SIZE: {
5261  auto eax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
5262  auto edx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
5263  auto op1 = this->symbolicEngine->getOperandAst(inst, eax);
5264  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
5265  auto node = this->astCtxt->bvmul(this->astCtxt->sx(DWORD_SIZE_BIT, op1), this->astCtxt->sx(DWORD_SIZE_BIT, op2));
5266  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(DWORD_SIZE_BIT-1, 0, node), eax, "IMUL operation");
5267  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(QWORD_SIZE_BIT-1, DWORD_SIZE_BIT, node), edx, "IMUL operation");
5268  expr1->isTainted = this->taintEngine->taintUnion(eax, src);
5269  expr2->isTainted = this->taintEngine->taintUnion(edx, eax);
5270  this->cfImul_s(inst, expr1, eax, this->astCtxt->bvmul(op1, op2), node);
5271  this->ofImul_s(inst, expr1, eax, this->astCtxt->bvmul(op1, op2), node);
5272  break;
5273  }
5274 
5275  /* dst = RDX:RAX */
5276  case QWORD_SIZE: {
5277  auto rax = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
5278  auto rdx = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
5279  auto op1 = this->symbolicEngine->getOperandAst(inst, rax);
5280  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
5281  auto node = this->astCtxt->bvmul(this->astCtxt->sx(QWORD_SIZE_BIT, op1), this->astCtxt->sx(QWORD_SIZE_BIT, op2));
5282  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(QWORD_SIZE_BIT-1, 0, node), rax, "IMUL operation");
5283  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(DQWORD_SIZE_BIT-1, QWORD_SIZE_BIT, node), rdx, "IMUL operation");
5284  expr1->isTainted = this->taintEngine->taintUnion(rax, src);
5285  expr2->isTainted = this->taintEngine->taintUnion(rdx, rax);
5286  this->cfImul_s(inst, expr1, rax, this->astCtxt->bvmul(op1, op2), node);
5287  this->ofImul_s(inst, expr1, rax, this->astCtxt->bvmul(op1, op2), node);
5288  break;
5289  }
5290 
5291  }
5292  break;
5293  }
5294 
5295  /* two operands */
5296  case 2: {
5297  auto& dst = inst.operands[0];
5298  auto& src = inst.operands[1];
5299  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
5300  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
5301  auto node = this->astCtxt->bvmul(this->astCtxt->sx(dst.getBitSize(), op1), this->astCtxt->sx(src.getBitSize(), op2));
5302  auto expr = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(dst.getBitSize()-1, 0, node), dst, "IMUL operation");
5303  expr->isTainted = this->taintEngine->taintUnion(dst, src);
5304  this->cfImul_s(inst, expr, dst, this->astCtxt->bvmul(op1, op2), node);
5305  this->ofImul_s(inst, expr, dst, this->astCtxt->bvmul(op1, op2), node);
5306  break;
5307  }
5308 
5309  /* three operands */
5310  case 3: {
5311  auto& dst = inst.operands[0];
5312  auto& src1 = inst.operands[1];
5313  auto& src2 = inst.operands[2];
5314  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
5315  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
5316  auto node = this->astCtxt->bvmul(this->astCtxt->sx(src1.getBitSize(), op2), this->astCtxt->sx(src2.getBitSize(), op3));
5317  auto expr = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt->extract(dst.getBitSize()-1, 0, node), dst, "IMUL operation");
5318  expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
5319  this->cfImul_s(inst, expr, dst, this->astCtxt->bvmul(op2, op3), node);
5320  this->ofImul_s(inst, expr, dst, this->astCtxt->bvmul(op2, op3), node);
5321  break;
5322  }
5323 
5324  }
5325 
5326  /* Tag undefined flags */
5327  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
5328  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
5329  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
5330  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
5331 
5332  /* Update the symbolic control flow */
5333  this->controlFlow_s(inst);
5334  }
5335 
5336 
5337  void x86Semantics::inc_s(triton::arch::Instruction& inst) {
5338  auto& dst = inst.operands[0];
5339 
5340  /* Create symbolic operands */
5341  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
5342  auto op2 = this->astCtxt->bv(1, dst.getBitSize());
5343 
5344  /* Create the semantics */
5345  auto node = this->astCtxt->bvadd(op1, op2);
5346 
5347  /* Create symbolic expression */
5348  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "INC operation");
5349 
5350  /* Spread taint */
5351  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
5352 
5353  /* Update symbolic flags */
5354  this->af_s(inst, expr, dst, op1, op2);
5355  this->ofAdd_s(inst, expr, dst, op1, op2);
5356  this->pf_s(inst, expr, dst);
5357  this->sf_s(inst, expr, dst);
5358  this->zf_s(inst, expr, dst);
5359 
5360  /* Update the symbolic control flow */
5361  this->controlFlow_s(inst);
5362  }
5363 
5364 
5365  void x86Semantics::invd_s(triton::arch::Instruction& inst) {
5366  /* Update the symbolic control flow */
5367  this->controlFlow_s(inst);
5368  }
5369 
5370 
5371  void x86Semantics::invlpg_s(triton::arch::Instruction& inst) {
5372  /* Update the symbolic control flow */
5373  this->controlFlow_s(inst);
5374  }
5375 
5376 
5377  void x86Semantics::ja_s(triton::arch::Instruction& inst) {
5378  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
5379  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
5380  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
5381  auto srcImm1 = triton::arch::OperandWrapper(Immediate(inst.getNextAddress(), pc.getSize()));
5382  auto& srcImm2 = inst.operands[0];
5383 
5384  /* Create symbolic operands */
5385  auto op1 = this->symbolicEngine->getOperandAst(inst, cf);
5386  auto op2 = this->symbolicEngine->getOperandAst(inst, zf);
5387  auto op3 = this->symbolicEngine->getOperandAst(inst, srcImm1);
5388  auto op4 = this->symbolicEngine->getOperandAst(inst, srcImm2);
5389 
5390  /* Create the semantics */
5391  auto node = this->astCtxt->ite(
5392  this->astCtxt->equal(
5393  this->astCtxt->bvand(
5394  this->astCtxt->bvnot(op1),
5395  this->astCtxt->bvnot(op2)
5396  ),
5397  this->astCtxt->bvtrue()
5398  ), op4, op3);
5399 
5400  /* Create symbolic expression */
5401  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
5402 
5403  /* Set condition flag */
5404  if (op1->evaluate().is_zero() && op2->evaluate().is_zero())
5405  inst.setConditionTaken(true);
5406 
5407  /* Spread taint */
5408  expr->isTainted = this->taintEngine->taintAssignment(pc, cf);
5409  expr->isTainted = this->taintEngine->taintUnion(pc, zf);
5410 
5411  /* Create the path constraint */
5412  this->symbolicEngine->addPathConstraint(inst, expr);
5413  }
5414 
5415 
5416  void x86Semantics::jae_s(triton::arch::Instruction& inst) {
5417  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
5418  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
5419  auto srcImm1 = triton::arch::OperandWrapper(Immediate(inst.getNextAddress(), pc.getSize()));
5420  auto& srcImm2 = inst.operands[0];
5421 
5422  /* Create symbolic operands */
5423  auto op1 = this->symbolicEngine->getOperandAst(inst, cf);
5424  auto op2 = this->symbolicEngine->getOperandAst(inst, srcImm1);
5425  auto op3 = this->symbolicEngine->getOperandAst(inst, srcImm2);
5426 
5427  /* Create the semantics */
5428  auto node = this->astCtxt->ite(this->astCtxt->equal(op1, this->astCtxt->bvfalse()), op3, op2);
5429 
5430  /* Create symbolic expression */
5431  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
5432 
5433  /* Set condition flag */
5434  if (op1->evaluate().is_zero())
5435  inst.setConditionTaken(true);
5436 
5437  /* Spread taint */
5438  expr->isTainted = this->taintEngine->taintAssignment(pc, cf);
5439 
5440  /* Create the path constraint */
5441  this->symbolicEngine->addPathConstraint(inst, expr);
5442  }
5443 
5444 
5445  void x86Semantics::jb_s(triton::arch::Instruction& inst) {
5446  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
5447  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
5448  auto srcImm1 = triton::arch::OperandWrapper(Immediate(inst.getNextAddress(), pc.getSize()));
5449  auto& srcImm2 = inst.operands[0];
5450 
5451  /* Create symbolic operands */
5452  auto op1 = this->symbolicEngine->getOperandAst(inst, cf);
5453  auto op2 = this->symbolicEngine->getOperandAst(inst, srcImm1);
5454  auto op3 = this->symbolicEngine->getOperandAst(inst, srcImm2);
5455 
5456  /* Create the semantics */
5457  auto node = this->astCtxt->ite(this->astCtxt->equal(op1, this->astCtxt->bvtrue()), op3, op2);
5458 
5459  /* Create symbolic expression */
5460  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
5461 
5462  /* Set condition flag */
5463  if (!op1->evaluate().is_zero())
5464  inst.setConditionTaken(true);
5465 
5466  /* Spread taint */
5467  expr->isTainted = this->taintEngine->taintAssignment(pc, cf);
5468 
5469