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