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