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