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