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