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