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