libTriton  version 0.7 build 1398
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 bvSize = op3->getBitvectorSize();
1413  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1414 
1415  /*
1416  * Create the semantic.
1417  * cf = MSB(rol(op3, concat(op2,op1))) if op3 != 0
1418  */
1419  auto node = this->astCtxt.ite(
1420  this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
1421  this->symbolicEngine->getOperandAst(cf),
1422  this->astCtxt.extract(
1423  dst.getBitSize(), dst.getBitSize(),
1424  this->astCtxt.bvrol(
1425  this->astCtxt.decimal(op3->evaluate()),
1426  this->astCtxt.concat(op2, op1)
1427  )
1428  )
1429  );
1430 
1431  /* Create the symbolic expression */
1432  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1433 
1434  if (op3->evaluate()) {
1435  /* Spread the taint from the parent to the child */
1436  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1437  }
1438  else {
1439  inst.removeWrittenRegister(cf.getConstRegister());
1440  }
1441  }
1442 
1443 
1444  void x86Semantics::cfShr_s(triton::arch::Instruction& inst,
1449  bool vol) {
1450 
1451  auto bvSize = dst.getBitSize();
1452  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1453 
1454  /*
1455  * Create the semantic.
1456  * cf = ((op1 >> (op2 - 1)) & 1) if op2 != 0
1457  */
1458  auto node = this->astCtxt.ite(
1459  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
1460  this->symbolicEngine->getOperandAst(cf),
1461  this->astCtxt.extract(0, 0,
1462  this->astCtxt.bvlshr(
1463  op1,
1464  this->astCtxt.bvsub(
1465  op2,
1466  this->astCtxt.bv(1, bvSize))
1467  )
1468  )
1469  );
1470 
1471  /* Create the symbolic expression */
1472  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1473 
1474  if (op2->evaluate()) {
1475  /* Spread the taint from the parent to the child */
1476  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1477  }
1478  else {
1479  inst.removeWrittenRegister(cf.getConstRegister());
1480  }
1481  }
1482 
1483 
1484  void x86Semantics::cfShrd_s(triton::arch::Instruction& inst,
1490  bool vol) {
1491 
1492  auto bvSize = op3->getBitvectorSize();
1493  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1494 
1495  /*
1496  * Create the semantic.
1497  * cf = MSB(ror(op3, concat(op2,op1))) if op3 != 0
1498  */
1499  auto node = this->astCtxt.ite(
1500  this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
1501  this->symbolicEngine->getOperandAst(cf),
1502  this->astCtxt.extract(
1503  (dst.getBitSize() * 2)-1, (dst.getBitSize()*2)-1,
1504  this->astCtxt.bvror(
1505  this->astCtxt.decimal(op3->evaluate()),
1506  this->astCtxt.concat(op2, op1)
1507  )
1508  )
1509  );
1510 
1511  /* Create the symbolic expression */
1512  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf.getConstRegister(), "Carry flag");
1513 
1514  if (op3->evaluate()) {
1515  /* Spread the taint from the parent to the child */
1516  expr->isTainted = this->taintEngine->setTaintRegister(cf.getConstRegister(), parent->isTainted);
1517  }
1518  else {
1519  inst.removeWrittenRegister(cf.getConstRegister());
1520  }
1521  }
1522 
1523 
1524  void x86Semantics::cfSub_s(triton::arch::Instruction& inst,
1529  bool vol) {
1530 
1531  auto bvSize = dst.getBitSize();
1532  auto low = vol ? 0 : dst.getLow();
1533  auto high = vol ? bvSize-1 : dst.getHigh();
1534 
1535  /*
1536  * Create the semantic.
1537  * cf = extract(bvSize, bvSize (((op1 ^ op2 ^ res) ^ ((op1 ^ res) & (op1 ^ op2)))))
1538  */
1539  auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
1540  this->astCtxt.bvxor(
1541  this->astCtxt.bvxor(op1, this->astCtxt.bvxor(op2, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))),
1542  this->astCtxt.bvand(
1543  this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent))),
1544  this->astCtxt.bvxor(op1, op2)
1545  )
1546  )
1547  );
1548 
1549  /* Create the symbolic expression */
1550  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "Carry flag");
1551 
1552  /* Spread the taint from the parent to the child */
1553  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_CF), parent->isTainted);
1554  }
1555 
1556 
1557  void x86Semantics::ofAdd_s(triton::arch::Instruction& inst,
1562  bool vol) {
1563 
1564  auto bvSize = dst.getBitSize();
1565  auto low = vol ? 0 : dst.getLow();
1566  auto high = vol ? bvSize-1 : dst.getHigh();
1567 
1568  /*
1569  * Create the semantic.
1570  * of = MSB((op1 ^ ~op2) & (op1 ^ regDst))
1571  */
1572  auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
1573  this->astCtxt.bvand(
1574  this->astCtxt.bvxor(op1, this->astCtxt.bvnot(op2)),
1575  this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))
1576  )
1577  );
1578 
1579  /* Create the symbolic expression */
1580  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1581 
1582  /* Spread the taint from the parent to the child */
1583  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1584  }
1585 
1586 
1587  void x86Semantics::ofImul_s(triton::arch::Instruction& inst,
1592  bool vol) {
1593  /*
1594  * Create the semantic.
1595  * of = 0 if sx(dst) == node else 1
1596  */
1597  auto node = this->astCtxt.ite(
1598  this->astCtxt.equal(
1599  this->astCtxt.sx(dst.getBitSize(), op1),
1600  res
1601  ),
1602  this->astCtxt.bv(0, 1),
1603  this->astCtxt.bv(1, 1)
1604  );
1605 
1606  /* Create the symbolic expression */
1607  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1608 
1609  /* Spread the taint from the parent to the child */
1610  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1611  }
1612 
1613 
1614  void x86Semantics::ofMul_s(triton::arch::Instruction& inst,
1618  bool vol) {
1619 
1620  /*
1621  * Create the semantic.
1622  * of = 0 if up == 0 else 1
1623  */
1624  auto node = this->astCtxt.ite(
1625  this->astCtxt.equal(
1626  op1,
1627  this->astCtxt.bv(0, dst.getBitSize())
1628  ),
1629  this->astCtxt.bv(0, 1),
1630  this->astCtxt.bv(1, 1)
1631  );
1632 
1633  /* Create the symbolic expression */
1634  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1635 
1636  /* Spread the taint from the parent to the child */
1637  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1638  }
1639 
1640 
1641  void x86Semantics::ofNeg_s(triton::arch::Instruction& inst,
1645  bool vol) {
1646 
1647  auto bvSize = dst.getBitSize();
1648  auto low = vol ? 0 : dst.getLow();
1649  auto high = vol ? bvSize-1 : dst.getHigh();
1650 
1651  /*
1652  * Create the semantic.
1653  * of = (res & op1) >> (bvSize - 1) & 1
1654  */
1655  auto node = this->astCtxt.extract(0, 0,
1656  this->astCtxt.bvlshr(
1657  this->astCtxt.bvand(this->astCtxt.extract(high, low, this->astCtxt.reference(parent)), op1),
1658  this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize))
1659  )
1660  );
1661 
1662  /* Create the symbolic expression */
1663  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
1664 
1665  /* Spread the taint from the parent to the child */
1666  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
1667  }
1668 
1669 
1670  void x86Semantics::ofRol_s(triton::arch::Instruction& inst,
1674  bool vol) {
1675 
1676  auto bvSize = dst.getBitSize();
1677  auto high = vol ? bvSize-1 : dst.getHigh();
1678  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1679  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1680 
1681  auto node = this->astCtxt.ite(
1682  this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(1, bvSize)),
1683  this->astCtxt.bvxor(
1684  this->astCtxt.extract(high, high, this->astCtxt.reference(parent)),
1685  this->symbolicEngine->getOperandAst(inst, cf)
1686  ),
1687  this->symbolicEngine->getOperandAst(of)
1688  );
1689 
1690  /* Create the symbolic expression */
1691  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1692 
1693  if (op2->evaluate()) {
1694  /* Spread the taint from the parent to the child */
1695  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1696  }
1697  else {
1698  inst.removeReadRegister(cf.getConstRegister());
1700  }
1701  }
1702 
1703 
1704  void x86Semantics::ofRor_s(triton::arch::Instruction& inst,
1708  bool vol) {
1709 
1710  auto bvSize = op2->getBitvectorSize();
1711  auto high = vol ? bvSize-1 : dst.getHigh();
1712  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1713 
1714  auto node = this->astCtxt.ite(
1715  this->astCtxt.equal(op2, this->astCtxt.bv(1, bvSize)),
1716  this->astCtxt.bvxor(
1717  this->astCtxt.extract(high, high, this->astCtxt.reference(parent)),
1718  this->astCtxt.extract(high-1, high-1, this->astCtxt.reference(parent))
1719  ),
1720  this->symbolicEngine->getOperandAst(of)
1721  );
1722 
1723  /* Create the symbolic expression */
1724  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1725 
1726  if (op2->evaluate()) {
1727  /* Spread the taint from the parent to the child */
1728  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1729  }
1730  else {
1732  }
1733  }
1734 
1735 
1736  void x86Semantics::ofRcr_s(triton::arch::Instruction& inst,
1741  bool vol) {
1742 
1743  auto bvSize = op2->getBitvectorSize();
1744  auto high = dst.getBitSize()-1;
1745  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
1746  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1747 
1748  auto node = this->astCtxt.ite(
1749  this->astCtxt.equal(op2, this->astCtxt.bv(1, bvSize)),
1750  this->astCtxt.bvxor(
1751  this->astCtxt.extract(high, high, op1),
1752  this->symbolicEngine->getOperandAst(inst, cf)
1753  ),
1754  this->symbolicEngine->getOperandAst(of)
1755  );
1756 
1757  /* Create the symbolic expression */
1758  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1759 
1760  if (op2->evaluate()) {
1761  /* Spread the taint from the parent to the child */
1762  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1763  }
1764  else {
1765  inst.removeReadRegister(cf.getConstRegister());
1767  }
1768  }
1769 
1770 
1771  void x86Semantics::ofSar_s(triton::arch::Instruction& inst,
1775  bool vol) {
1776 
1777  auto bvSize = dst.getBitSize();
1778  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1779 
1780  /*
1781  * Create the semantic.
1782  * of = 0 if op2 == 1
1783  */
1784  auto node = this->astCtxt.ite(
1785  this->astCtxt.land(
1786  this->astCtxt.equal(
1787  /* #672 */
1788  this->astCtxt.reference(parent),
1789  this->astCtxt.reference(parent)
1790  /* ---- */
1791  ),
1792  this->astCtxt.equal(
1793  op2,
1794  this->astCtxt.bv(1, bvSize)
1795  )
1796  ),
1797  this->astCtxt.bv(0, 1),
1798  this->symbolicEngine->getOperandAst(of)
1799  );
1800 
1801  /* Create the symbolic expression */
1802  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1803 
1804  if (op2->evaluate()) {
1805  /* Spread the taint from the parent to the child */
1806  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1807  }
1808  else {
1810  }
1811  }
1812 
1813 
1814  void x86Semantics::ofShl_s(triton::arch::Instruction& inst,
1819  bool vol) {
1820 
1821  auto bvSize = dst.getBitSize();
1822  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1823 
1824  /*
1825  * Create the semantic.
1826  * of = ((op1 >> (bvSize - 1)) ^ (op1 >> (bvSize - 2))) & 1; if op2 == 1
1827  */
1828  auto node = this->astCtxt.ite(
1829  this->astCtxt.equal(
1830  op2,
1831  this->astCtxt.bv(1, bvSize)),
1832  this->astCtxt.extract(0, 0,
1833  this->astCtxt.bvxor(
1834  this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize))),
1835  this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(2, bvSize)))
1836  )
1837  ),
1838  this->symbolicEngine->getOperandAst(of)
1839  );
1840 
1841  /* Create the symbolic expression */
1842  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1843 
1844  if (op2->evaluate()) {
1845  /* Spread the taint from the parent to the child */
1846  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1847  }
1848  else {
1850  }
1851  }
1852 
1853 
1854  void x86Semantics::ofShld_s(triton::arch::Instruction& inst,
1860  bool vol) {
1861 
1862  auto bvSize = dst.getBitSize();
1863  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1864 
1865  /*
1866  * Create the semantic.
1867  * of = MSB(rol(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
1868  */
1869  auto node = this->astCtxt.ite(
1870  this->astCtxt.equal(
1871  this->astCtxt.zx(bvSize - op3->getBitvectorSize(), op3),
1872  this->astCtxt.bv(1, bvSize)),
1873  this->astCtxt.bvxor(
1874  this->astCtxt.extract(
1875  dst.getBitSize()-1, dst.getBitSize()-1,
1876  this->astCtxt.bvrol(
1877  this->astCtxt.decimal(op3->evaluate()),
1878  this->astCtxt.concat(op2, op1)
1879  )
1880  ),
1881  this->astCtxt.extract(dst.getBitSize()-1, dst.getBitSize()-1, op1)
1882  ),
1883  this->symbolicEngine->getOperandAst(of)
1884  );
1885 
1886  /* Create the symbolic expression */
1887  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1888 
1889  if (op3->evaluate()) {
1890  /* Spread the taint from the parent to the child */
1891  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1892  }
1893  else {
1895  }
1896  }
1897 
1898 
1899  void x86Semantics::ofShr_s(triton::arch::Instruction& inst,
1904  bool vol) {
1905 
1906  auto bvSize = dst.getBitSize();
1907  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1908 
1909  /*
1910  * Create the semantic.
1911  * of = ((op1 >> (bvSize - 1)) & 1) if op2 == 1
1912  */
1913  auto node = this->astCtxt.ite(
1914  this->astCtxt.equal(
1915  op2,
1916  this->astCtxt.bv(1, bvSize)),
1917  this->astCtxt.extract(0, 0, this->astCtxt.bvlshr(op1, this->astCtxt.bvsub(this->astCtxt.bv(bvSize, bvSize), this->astCtxt.bv(1, bvSize)))),
1918  this->symbolicEngine->getOperandAst(of)
1919  );
1920 
1921  /* Create the symbolic expression */
1922  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1923 
1924  if (op2->evaluate()) {
1925  /* Spread the taint from the parent to the child */
1926  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1927  }
1928  else {
1930  }
1931  }
1932 
1933 
1934  void x86Semantics::ofShrd_s(triton::arch::Instruction& inst,
1940  bool vol) {
1941 
1942  auto bvSize = dst.getBitSize();
1943  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
1944 
1945  /*
1946  * Create the semantic.
1947  * of = MSB(ror(op3, concat(op2,op1))) ^ MSB(op1); if op3 == 1
1948  */
1949  auto node = this->astCtxt.ite(
1950  this->astCtxt.equal(
1951  this->astCtxt.zx(bvSize - op3->getBitvectorSize(), op3),
1952  this->astCtxt.bv(1, bvSize)),
1953  this->astCtxt.bvxor(
1954  this->astCtxt.extract(
1955  dst.getBitSize()-1, dst.getBitSize()-1,
1956  this->astCtxt.bvror(
1957  this->astCtxt.decimal(op3->evaluate()),
1958  this->astCtxt.concat(op2, op1)
1959  )
1960  ),
1961  this->astCtxt.extract(dst.getBitSize()-1, dst.getBitSize()-1, op1)
1962  ),
1963  this->symbolicEngine->getOperandAst(of)
1964  );
1965 
1966  /* Create the symbolic expression */
1967  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, of.getConstRegister(), "Overflow flag");
1968 
1969  if (op3->evaluate()) {
1970  /* Spread the taint from the parent to the child */
1971  expr->isTainted = this->taintEngine->setTaintRegister(of.getConstRegister(), parent->isTainted);
1972  }
1973  else {
1975  }
1976  }
1977 
1978 
1979  void x86Semantics::ofSub_s(triton::arch::Instruction& inst,
1984  bool vol) {
1985 
1986  auto bvSize = dst.getBitSize();
1987  auto low = vol ? 0 : dst.getLow();
1988  auto high = vol ? bvSize-1 : dst.getHigh();
1989 
1990  /*
1991  * Create the semantic.
1992  * of = high:bool((op1 ^ op2) & (op1 ^ regDst))
1993  */
1994  auto node = this->astCtxt.extract(bvSize-1, bvSize-1,
1995  this->astCtxt.bvand(
1996  this->astCtxt.bvxor(op1, op2),
1997  this->astCtxt.bvxor(op1, this->astCtxt.extract(high, low, this->astCtxt.reference(parent)))
1998  )
1999  );
2000 
2001  /* Create the symbolic expression */
2002  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_OF), "Overflow flag");
2003 
2004  /* Spread the taint from the parent to the child */
2005  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_OF), parent->isTainted);
2006  }
2007 
2008 
2009  void x86Semantics::pf_s(triton::arch::Instruction& inst,
2012  bool vol) {
2013 
2014  auto low = vol ? 0 : dst.getLow();
2015  auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
2016 
2017  /*
2018  * Create the semantics.
2019  *
2020  * pf is set to one if there is an even number of bit set to 1 in the least
2021  * significant byte of the result.
2022  */
2023  auto node = this->astCtxt.bv(1, 1);
2024  for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
2025  node = this->astCtxt.bvxor(
2026  node,
2027  this->astCtxt.extract(0, 0,
2028  this->astCtxt.bvlshr(
2029  this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
2030  this->astCtxt.bv(counter, BYTE_SIZE_BIT)
2031  )
2032  )
2033  );
2034  }
2035 
2036  /* Create the symbolic expression */
2037  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_PF), "Parity flag");
2038 
2039  /* Spread the taint from the parent to the child */
2040  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_PF), parent->isTainted);
2041  }
2042 
2043 
2044  void x86Semantics::pfShl_s(triton::arch::Instruction& inst,
2048  bool vol) {
2049 
2050  auto bvSize = dst.getBitSize();
2051  auto low = vol ? 0 : dst.getLow();
2052  auto high = vol ? BYTE_SIZE_BIT-1 : !low ? BYTE_SIZE_BIT-1 : WORD_SIZE_BIT-1;
2053  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
2054 
2055  /*
2056  * Create the semantics.
2057  * pf if op2 != 0
2058  */
2059  auto node1 = this->astCtxt.bv(1, 1);
2060  for (triton::uint32 counter = 0; counter <= BYTE_SIZE_BIT-1; counter++) {
2061  node1 = this->astCtxt.bvxor(
2062  node1,
2063  this->astCtxt.extract(0, 0,
2064  this->astCtxt.bvlshr(
2065  this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
2066  this->astCtxt.bv(counter, BYTE_SIZE_BIT)
2067  )
2068  )
2069  );
2070  }
2071 
2072  auto node2 = this->astCtxt.ite(
2073  this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(0, bvSize)),
2074  this->symbolicEngine->getOperandAst(pf),
2075  node1
2076  );
2077 
2078  /* Create the symbolic expression */
2079  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node2, pf.getConstRegister(), "Parity flag");
2080 
2081  if (op2->evaluate()) {
2082  /* Spread the taint from the parent to the child */
2083  expr->isTainted = this->taintEngine->setTaintRegister(pf.getConstRegister(), parent->isTainted);
2084  }
2085  else {
2086  inst.removeWrittenRegister(pf.getConstRegister());
2087  }
2088  }
2089 
2090 
2091  void x86Semantics::sf_s(triton::arch::Instruction& inst,
2094  bool vol) {
2095 
2096  auto bvSize = dst.getBitSize();
2097  auto high = vol ? bvSize-1 : dst.getHigh();
2098 
2099  /*
2100  * Create the semantic.
2101  * sf = high:bool(regDst)
2102  */
2103  auto node = this->astCtxt.extract(high, high, this->astCtxt.reference(parent));
2104 
2105  /* Create the symbolic expression */
2106  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_SF), "Sign flag");
2107 
2108  /* Spread the taint from the parent to the child */
2109  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_SF), parent->isTainted);
2110  }
2111 
2112 
2113  void x86Semantics::sfShl_s(triton::arch::Instruction& inst,
2117  bool vol) {
2118 
2119  auto bvSize = dst.getBitSize();
2120  auto high = vol ? bvSize-1 : dst.getHigh();
2121  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2122 
2123  /*
2124  * Create the semantic.
2125  * sf if op2 != 0
2126  */
2127  auto node = this->astCtxt.ite(
2128  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize)),
2129  this->symbolicEngine->getOperandAst(sf),
2130  this->astCtxt.extract(high, high, this->astCtxt.reference(parent))
2131  );
2132 
2133  /* Create the symbolic expression */
2134  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2135 
2136  if (op2->evaluate()) {
2137  /* Spread the taint from the parent to the child */
2138  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2139  }
2140  else {
2141  inst.removeWrittenRegister(sf.getConstRegister());
2142  }
2143  }
2144 
2145 
2146  void x86Semantics::sfShld_s(triton::arch::Instruction& inst,
2152  bool vol) {
2153 
2154  auto bvSize = op3->getBitvectorSize();
2155  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2156 
2157  /*
2158  * Create the semantic.
2159  * MSB(rol(op3, concat(op2,op1))) if op3 != 0
2160  */
2161  auto node = this->astCtxt.ite(
2162  this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
2163  this->symbolicEngine->getOperandAst(sf),
2164  this->astCtxt.extract(
2165  dst.getBitSize()-1, dst.getBitSize()-1,
2166  this->astCtxt.bvrol(
2167  this->astCtxt.decimal(op3->evaluate()),
2168  this->astCtxt.concat(op2, op1)
2169  )
2170  )
2171  );
2172 
2173  /* Create the symbolic expression */
2174  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2175 
2176  if (op3->evaluate()) {
2177  /* Spread the taint from the parent to the child */
2178  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2179  }
2180  else {
2181  inst.removeWrittenRegister(sf.getConstRegister());
2182  }
2183  }
2184 
2185 
2186  void x86Semantics::sfShrd_s(triton::arch::Instruction& inst,
2192  bool vol) {
2193 
2194  auto bvSize = op3->getBitvectorSize();
2195  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
2196 
2197  /*
2198  * Create the semantic.
2199  * MSB(ror(op3, concat(op2,op1))) if op3 != 0
2200  */
2201  auto node = this->astCtxt.ite(
2202  this->astCtxt.equal(op3, this->astCtxt.bv(0, bvSize)),
2203  this->symbolicEngine->getOperandAst(sf),
2204  this->astCtxt.extract(
2205  dst.getBitSize()-1, dst.getBitSize()-1,
2206  this->astCtxt.bvror(
2207  this->astCtxt.decimal(op3->evaluate()),
2208  this->astCtxt.concat(op2, op1)
2209  )
2210  )
2211  );
2212 
2213  /* Create the symbolic expression */
2214  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sf.getConstRegister(), "Sign flag");
2215 
2216  if (op3->evaluate()) {
2217  /* Spread the taint from the parent to the child */
2218  expr->isTainted = this->taintEngine->setTaintRegister(sf.getConstRegister(), parent->isTainted);
2219  }
2220  else {
2221  inst.removeWrittenRegister(sf.getConstRegister());
2222  }
2223  }
2224 
2225 
2226  void x86Semantics::zf_s(triton::arch::Instruction& inst,
2229  bool vol) {
2230 
2231  auto bvSize = dst.getBitSize();
2232  auto low = vol ? 0 : dst.getLow();
2233  auto high = vol ? bvSize-1 : dst.getHigh();
2234 
2235  /*
2236  * Create the semantic.
2237  * zf = 0 == regDst
2238  */
2239  auto node = this->astCtxt.ite(
2240  this->astCtxt.equal(
2241  this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
2242  this->astCtxt.bv(0, bvSize)
2243  ),
2244  this->astCtxt.bv(1, 1),
2245  this->astCtxt.bv(0, 1)
2246  );
2247 
2248  /* Create the symbolic expression */
2249  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_ZF), "Zero flag");
2250 
2251  /* Spread the taint from the parent to the child */
2252  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_ZF), parent->isTainted);
2253  }
2254 
2255 
2256  void x86Semantics::zfBsf_s(triton::arch::Instruction& inst,
2260  bool vol) {
2261 
2262  /*
2263  * Create the semantic.
2264  * zf = 1 if op2 == 0 else 0
2265  */
2266  auto node = this->astCtxt.ite(
2267  this->astCtxt.equal(op2, this->astCtxt.bv(0, src.getBitSize())),
2268  this->astCtxt.bvtrue(),
2269  this->astCtxt.bvfalse()
2270  );
2271 
2272  /* Create the symbolic expression */
2273  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_ZF), "Zero flag");
2274 
2275  /* Spread the taint from the parent to the child */
2276  expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getRegister(ID_REG_X86_ZF), parent->isTainted);
2277  }
2278 
2279 
2280  void x86Semantics::zfShl_s(triton::arch::Instruction& inst,
2284  bool vol) {
2285 
2286  auto bvSize = dst.getBitSize();
2287  auto low = vol ? 0 : dst.getLow();
2288  auto high = vol ? bvSize-1 : dst.getHigh();
2289  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
2290 
2291  /*
2292  * Create the semantic.
2293  * zf if op2 != 0
2294  */
2295  auto node = this->astCtxt.ite(
2296  this->astCtxt.equal(this->astCtxt.zx(bvSize - op2->getBitvectorSize(), op2), this->astCtxt.bv(0, bvSize)),
2297  this->symbolicEngine->getOperandAst(zf),
2298  this->astCtxt.ite(
2299  this->astCtxt.equal(
2300  this->astCtxt.extract(high, low, this->astCtxt.reference(parent)),
2301  this->astCtxt.bv(0, bvSize)
2302  ),
2303  this->astCtxt.bv(1, 1),
2304  this->astCtxt.bv(0, 1)
2305  )
2306  );
2307 
2308  /* Create the symbolic expression */
2309  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, zf.getConstRegister(), "Zero flag");
2310 
2311  if (op2->evaluate()) {
2312  /* Spread the taint from the parent to the child */
2313  expr->isTainted = this->taintEngine->setTaintRegister(zf.getConstRegister(), parent->isTainted);
2314  }
2315  else {
2317  }
2318  }
2319 
2320 
2321  void x86Semantics::aaa_s(triton::arch::Instruction& inst) {
2322  auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2323  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2324  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AF));
2325  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2326  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2327 
2328  /* Create symbolic operands */
2329  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2330  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2331  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2332 
2333  /* Create the semantics */
2334  auto node = this->astCtxt.ite(
2335  // if
2336  this->astCtxt.lor(
2337  this->astCtxt.bvugt(
2338  this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize())),
2339  this->astCtxt.bv(9, src1.getBitSize())
2340  ),
2341  this->astCtxt.equal(op3, this->astCtxt.bvtrue())
2342  ),
2343  // then
2344  this->astCtxt.concat(
2345  this->astCtxt.bvadd(op2, this->astCtxt.bv(1, src2.getBitSize())),
2346  this->astCtxt.bvand(
2347  this->astCtxt.bvadd(op1, this->astCtxt.bv(6, src1.getBitSize())),
2348  this->astCtxt.bv(0xf, src1.getBitSize())
2349  )
2350  ),
2351  // else
2352  this->astCtxt.concat(
2353  op2,
2354  this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize()))
2355  )
2356  );
2357 
2358  /* Create symbolic expression */
2359  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAA operation");
2360 
2361  /* Spread taint */
2362  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2363 
2364  /* Update symbolic flags */
2365  this->afAaa_s(inst, expr, dsttmp, op1, op3);
2366  this->cfAaa_s(inst, expr, dsttmp, op1, op3);
2367 
2368  /* Tag undefined flags */
2369  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2370  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
2371  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
2372  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
2373 
2374  /* Update the symbolic control flow */
2375  this->controlFlow_s(inst);
2376  }
2377 
2378 
2379  void x86Semantics::aad_s(triton::arch::Instruction& inst) {
2380  auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D5 0A */
2381  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2382  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2383  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2384  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2385 
2386  /* D5 ib */
2387  if (inst.operands.size() == 1)
2388  src1 = inst.operands[0];
2389 
2390  /* Create symbolic operands */
2391  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2392  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2393  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2394 
2395  /* Create the semantics */
2396  auto node = this->astCtxt.zx(
2397  BYTE_SIZE_BIT,
2398  this->astCtxt.bvadd(
2399  op2,
2400  this->astCtxt.bvmul(op3, op1)
2401  )
2402  );
2403 
2404  /* Create symbolic expression */
2405  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAD operation");
2406 
2407  /* Spread taint */
2408  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2409 
2410  /* Update symbolic flags */
2411  this->pf_s(inst, expr, dsttmp);
2412  this->sf_s(inst, expr, dsttmp);
2413  this->zf_s(inst, expr, dsttmp);
2414 
2415  /* Tag undefined flags */
2416  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2417  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
2418  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2419 
2420  /* Update the symbolic control flow */
2421  this->controlFlow_s(inst);
2422  }
2423 
2424 
2425  void x86Semantics::aam_s(triton::arch::Instruction& inst) {
2426  auto src1 = triton::arch::OperandWrapper(triton::arch::Immediate(0x0a, BYTE_SIZE)); /* D4 0A */
2427  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2428  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2429  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2430 
2431  /* D4 ib */
2432  if (inst.operands.size() == 1)
2433  src1 = inst.operands[0];
2434 
2435  /* Create symbolic operands */
2436  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2437  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2438 
2439  /* Create the semantics */
2440  auto node = this->astCtxt.concat(
2441  this->astCtxt.bvudiv(op2, op1),
2442  this->astCtxt.bvurem(op2, op1)
2443  );
2444 
2445  /* Create symbolic expression */
2446  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAM operation");
2447 
2448  /* Spread taint */
2449  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2450 
2451  /* Update symbolic flags */
2452  this->pf_s(inst, expr, dsttmp);
2453  this->sf_s(inst, expr, dsttmp);
2454  this->zf_s(inst, expr, dsttmp);
2455 
2456  /* Tag undefined flags */
2457  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2458  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
2459  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2460 
2461  /* Update the symbolic control flow */
2462  this->controlFlow_s(inst);
2463  }
2464 
2465 
2466  void x86Semantics::aas_s(triton::arch::Instruction& inst) {
2467  auto src1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2468  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AH));
2469  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AF));
2470  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
2471  auto dsttmp = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AL));
2472 
2473  /* Create symbolic operands */
2474  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2475  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2476  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
2477 
2478  /* Create the semantics */
2479  auto node = this->astCtxt.ite(
2480  // if
2481  this->astCtxt.lor(
2482  this->astCtxt.bvugt(
2483  this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize())),
2484  this->astCtxt.bv(9, src1.getBitSize())
2485  ),
2486  this->astCtxt.equal(op3, this->astCtxt.bvtrue())
2487  ),
2488  // then
2489  this->astCtxt.concat(
2490  this->astCtxt.bvsub(op2, this->astCtxt.bv(1, src2.getBitSize())),
2491  this->astCtxt.bvand(
2492  this->astCtxt.bvsub(op1, this->astCtxt.bv(6, src1.getBitSize())),
2493  this->astCtxt.bv(0xf, src1.getBitSize())
2494  )
2495  ),
2496  // else
2497  this->astCtxt.concat(
2498  op2,
2499  this->astCtxt.bvand(op1, this->astCtxt.bv(0xf, src1.getBitSize()))
2500  )
2501  );
2502 
2503  /* Create symbolic expression */
2504  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AAS operation");
2505 
2506  /* Spread taint */
2507  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
2508 
2509  /* Update symbolic flags */
2510  this->afAaa_s(inst, expr, dsttmp, op1, op3);
2511  this->cfAaa_s(inst, expr, dsttmp, op1, op3);
2512 
2513  /* Tag undefined flags */
2514  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
2515  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
2516  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
2517  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_ZF));
2518 
2519  /* Update the symbolic control flow */
2520  this->controlFlow_s(inst);
2521  }
2522 
2523 
2524  void x86Semantics::adc_s(triton::arch::Instruction& inst) {
2525  auto& dst = inst.operands[0];
2526  auto& src = inst.operands[1];
2527  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
2528 
2529  /* Create symbolic operands */
2530  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2531  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2532  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
2533 
2534  /* Create the semantics */
2535  auto node = this->astCtxt.bvadd(this->astCtxt.bvadd(op1, op2), this->astCtxt.zx(dst.getBitSize()-1, op3));
2536 
2537  /* Create symbolic expression */
2538  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADC operation");
2539 
2540  /* Spread taint */
2541  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2542  expr->isTainted = this->taintEngine->taintUnion(dst, cf);
2543 
2544  /* Update symbolic flags */
2545  this->af_s(inst, expr, dst, op1, op2);
2546  this->cfAdd_s(inst, expr, dst, op1, op2);
2547  this->ofAdd_s(inst, expr, dst, op1, op2);
2548  this->pf_s(inst, expr, dst);
2549  this->sf_s(inst, expr, dst);
2550  this->zf_s(inst, expr, dst);
2551 
2552  /* Update the symbolic control flow */
2553  this->controlFlow_s(inst);
2554  }
2555 
2556 
2557  void x86Semantics::adcx_s(triton::arch::Instruction& inst) {
2558  auto& dst = inst.operands[0];
2559  auto& src = inst.operands[1];
2560  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
2561 
2562  /* Create symbolic operands */
2563  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2564  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2565  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
2566 
2567  /* Create the semantics */
2568  auto node = this->astCtxt.bvadd(this->astCtxt.bvadd(op1, op2), this->astCtxt.zx(dst.getBitSize()-1, op3));
2569 
2570  /* Create symbolic expression */
2571  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADCX operation");
2572 
2573  /* Spread taint */
2574  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2575  expr->isTainted = this->taintEngine->taintUnion(dst, cf);
2576 
2577  /* Update symbolic flags */
2578  this->cfAdd_s(inst, expr, dst, op1, op2);
2579 
2580  /* Update the symbolic control flow */
2581  this->controlFlow_s(inst);
2582  }
2583 
2584 
2585  void x86Semantics::add_s(triton::arch::Instruction& inst) {
2586  auto& dst = inst.operands[0];
2587  auto& src = inst.operands[1];
2588 
2589  /* Create symbolic operands */
2590  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2591  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2592 
2593  /* Create the semantics */
2594  auto node = this->astCtxt.bvadd(op1, op2);
2595 
2596  /* Create symbolic expression */
2597  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD operation");
2598 
2599  /* Spread taint */
2600  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2601 
2602  /* Update symbolic flags */
2603  this->af_s(inst, expr, dst, op1, op2);
2604  this->cfAdd_s(inst, expr, dst, op1, op2);
2605  this->ofAdd_s(inst, expr, dst, op1, op2);
2606  this->pf_s(inst, expr, dst);
2607  this->sf_s(inst, expr, dst);
2608  this->zf_s(inst, expr, dst);
2609 
2610  /* Update the symbolic control flow */
2611  this->controlFlow_s(inst);
2612  }
2613 
2614 
2615  void x86Semantics::and_s(triton::arch::Instruction& inst) {
2616  auto& dst = inst.operands[0];
2617  auto& src = inst.operands[1];
2618 
2619  /* Create symbolic operands */
2620  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2621  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2622 
2623  /* Create the semantics */
2624  auto node = this->astCtxt.bvand(op1, op2);
2625 
2626  /* Create symbolic expression */
2627  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND operation");
2628 
2629  /* Spread taint */
2630  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2631 
2632  /* Update symbolic flags */
2633  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2634  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2635  this->pf_s(inst, expr, dst);
2636  this->sf_s(inst, expr, dst);
2637  this->zf_s(inst, expr, dst);
2638 
2639  /* Tag undefined flags */
2640  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
2641 
2642  /* Update the symbolic control flow */
2643  this->controlFlow_s(inst);
2644  }
2645 
2646 
2647  void x86Semantics::andn_s(triton::arch::Instruction& inst) {
2648  auto& dst = inst.operands[0];
2649  auto& src1 = inst.operands[1];
2650  auto& src2 = inst.operands[2];
2651 
2652  /* Create symbolic operands */
2653  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
2654  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
2655 
2656  /* Create the semantics */
2657  auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op2), op3);
2658 
2659  /* Create symbolic expression */
2660  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDN operation");
2661 
2662  /* Spread taint */
2663  expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
2664 
2665  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2666  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2667  this->sf_s(inst, expr, dst);
2668  this->zf_s(inst, expr, dst);
2669 
2670  /* Update the symbolic control flow */
2671  this->controlFlow_s(inst);
2672  }
2673 
2674 
2675  void x86Semantics::andnpd_s(triton::arch::Instruction& inst) {
2676  auto& dst = inst.operands[0];
2677  auto& src = inst.operands[1];
2678 
2679  /* Create symbolic operands */
2680  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2681  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2682 
2683  /* Create the semantics */
2684  auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op1), op2);
2685 
2686  /* Create symbolic expression */
2687  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPD operation");
2688 
2689  /* Spread taint */
2690  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2691 
2692  /* Update the symbolic control flow */
2693  this->controlFlow_s(inst);
2694  }
2695 
2696 
2697  void x86Semantics::andnps_s(triton::arch::Instruction& inst) {
2698  auto& dst = inst.operands[0];
2699  auto& src = inst.operands[1];
2700 
2701  /* Create symbolic operands */
2702  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2703  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2704 
2705  /* Create the semantics */
2706  auto node = this->astCtxt.bvand(this->astCtxt.bvnot(op1), op2);
2707 
2708  /* Create symbolic expression */
2709  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDNPS operation");
2710 
2711  /* Spread taint */
2712  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2713 
2714  /* Update the symbolic control flow */
2715  this->controlFlow_s(inst);
2716  }
2717 
2718 
2719  void x86Semantics::andpd_s(triton::arch::Instruction& inst) {
2720  auto& dst = inst.operands[0];
2721  auto& src = inst.operands[1];
2722 
2723  /* Create symbolic operands */
2724  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2725  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2726 
2727  /* Create the semantics */
2728  auto node = this->astCtxt.bvand(op1, op2);
2729 
2730  /* Create symbolic expression */
2731  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPD operation");
2732 
2733  /* Spread taint */
2734  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2735 
2736  /* Update the symbolic control flow */
2737  this->controlFlow_s(inst);
2738  }
2739 
2740 
2741  void x86Semantics::andps_s(triton::arch::Instruction& inst) {
2742  auto& dst = inst.operands[0];
2743  auto& src = inst.operands[1];
2744 
2745  /* Create symbolic operands */
2746  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2747  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2748 
2749  /* Create the semantics */
2750  auto node = this->astCtxt.bvand(op1, op2);
2751 
2752  /* Create symbolic expression */
2753  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ANDPS operation");
2754 
2755  /* Spread taint */
2756  expr->isTainted = this->taintEngine->taintUnion(dst, src);
2757 
2758  /* Update the symbolic control flow */
2759  this->controlFlow_s(inst);
2760  }
2761 
2762 
2763  void x86Semantics::bextr_s(triton::arch::Instruction& inst) {
2764  auto& dst = inst.operands[0];
2765  auto& src1 = inst.operands[1];
2766  auto& src2 = inst.operands[2];
2767 
2768  /* Create symbolic operands */
2769  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2770  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2771 
2772  /* Create the semantics */
2773  auto node = this->astCtxt.bvand(
2774  this->astCtxt.bvlshr(
2775  op1,
2776  this->astCtxt.zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt.extract(7, 0, op2))
2777  ),
2778  this->astCtxt.bvsub(
2779  this->astCtxt.bvshl(
2780  this->astCtxt.bv(1, src1.getBitSize()),
2781  this->astCtxt.zx(src1.getBitSize() - BYTE_SIZE_BIT, this->astCtxt.extract(15, 8, op2))
2782  ),
2783  this->astCtxt.bv(1, src1.getBitSize())
2784  )
2785  );
2786 
2787  /* Create symbolic expression */
2788  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BEXTR operation");
2789 
2790  /* Spread taint */
2791  expr->isTainted = this->taintEngine->taintAssignment(dst, src1) | this->taintEngine->taintUnion(dst, src2);
2792 
2793  /* Update symbolic flags */
2794  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
2795  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2796  this->zf_s(inst, expr, dst);
2797 
2798  /* Update the symbolic control flow */
2799  this->controlFlow_s(inst);
2800  }
2801 
2802 
2803  void x86Semantics::blsi_s(triton::arch::Instruction& inst) {
2804  auto& dst = inst.operands[0];
2805  auto& src = inst.operands[1];
2806 
2807  /* Create symbolic operands */
2808  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2809 
2810  /* Create the semantics */
2811  auto node = this->astCtxt.bvand(this->astCtxt.bvneg(op1), op1);
2812 
2813  /* Create symbolic expression */
2814  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSI operation");
2815 
2816  /* Spread taint */
2817  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2818 
2819  /* Update symbolic flags */
2820  this->cfBlsi_s(inst, expr, src, op1);
2821  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2822  this->sf_s(inst, expr, dst);
2823  this->zf_s(inst, expr, dst);
2824 
2825  /* Update the symbolic control flow */
2826  this->controlFlow_s(inst);
2827  }
2828 
2829 
2830  void x86Semantics::blsmsk_s(triton::arch::Instruction& inst) {
2831  auto& dst = inst.operands[0];
2832  auto& src = inst.operands[1];
2833 
2834  /* Create symbolic operands */
2835  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2836 
2837  /* Create the semantics */
2838  auto node = this->astCtxt.bvxor(
2839  this->astCtxt.bvsub(op1, this->astCtxt.bv(1, src.getBitSize())),
2840  op1
2841  );
2842 
2843  /* Create symbolic expression */
2844  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSMSK operation");
2845 
2846  /* Spread taint */
2847  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2848 
2849  /* Update symbolic flags */
2850  this->cfBlsmsk_s(inst, expr, src, op1);
2851  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2852  this->sf_s(inst, expr, dst);
2853  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_ZF), "Clears zero flag");
2854 
2855  /* Update the symbolic control flow */
2856  this->controlFlow_s(inst);
2857  }
2858 
2859 
2860  void x86Semantics::blsr_s(triton::arch::Instruction& inst) {
2861  auto& dst = inst.operands[0];
2862  auto& src = inst.operands[1];
2863 
2864  /* Create symbolic operands */
2865  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2866 
2867  /* Create the semantics */
2868  auto node = this->astCtxt.bvand(
2869  this->astCtxt.bvsub(op1, this->astCtxt.bv(1, src.getBitSize())),
2870  op1
2871  );
2872 
2873  /* Create symbolic expression */
2874  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BLSR operation");
2875 
2876  /* Spread taint */
2877  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2878 
2879  /* Update symbolic flags */
2880  this->cfBlsr_s(inst, expr, src, op1);
2881  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_OF), "Clears overflow flag");
2882  this->sf_s(inst, expr, dst);
2883  this->zf_s(inst, expr, dst);
2884 
2885  /* Update the symbolic control flow */
2886  this->controlFlow_s(inst);
2887  }
2888 
2889 
2890  void x86Semantics::bsf_s(triton::arch::Instruction& inst) {
2891  auto& dst = inst.operands[0];
2892  auto& src = inst.operands[1];
2893  auto bvSize1 = dst.getBitSize();
2894  auto bvSize2 = src.getBitSize();
2895 
2896  /* Create symbolic operands */
2897  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
2898  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
2899 
2900  /* Create the semantics */
2901  triton::ast::SharedAbstractNode node = nullptr;
2902  switch (src.getSize()) {
2903  case BYTE_SIZE:
2904  node = this->astCtxt.ite(
2905  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2906  op1,
2907  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
2908  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
2909  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
2910  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
2911  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
2912  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
2913  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
2914  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
2915  this->astCtxt.bv(0, bvSize1)
2916  ))))))))
2917  );
2918  break;
2919  case WORD_SIZE:
2920  node = this->astCtxt.ite(
2921  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2922  op1,
2923  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
2924  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
2925  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
2926  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
2927  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
2928  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
2929  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
2930  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
2931  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
2932  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
2933  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
2934  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
2935  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
2936  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
2937  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
2938  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
2939  this->astCtxt.bv(0, bvSize1)
2940  ))))))))))))))))
2941  );
2942  break;
2943  case DWORD_SIZE:
2944  node = this->astCtxt.ite(
2945  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2946  op1,
2947  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
2948  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
2949  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
2950  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
2951  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
2952  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
2953  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
2954  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
2955  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
2956  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
2957  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
2958  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
2959  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
2960  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
2961  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
2962  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
2963  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
2964  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
2965  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
2966  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
2967  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
2968  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
2969  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
2970  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
2971  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
2972  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
2973  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
2974  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
2975  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
2976  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
2977  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
2978  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
2979  this->astCtxt.bv(0, bvSize1)
2980  ))))))))))))))))))))))))))))))))
2981  );
2982  break;
2983  case QWORD_SIZE:
2984  node = this->astCtxt.ite(
2985  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSF only if op2 != 0 */
2986  op1,
2987  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
2988  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
2989  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
2990  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
2991  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
2992  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
2993  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
2994  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
2995  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
2996  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
2997  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
2998  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
2999  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
3000  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
3001  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
3002  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
3003  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
3004  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
3005  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
3006  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
3007  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
3008  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
3009  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
3010  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
3011  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
3012  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
3013  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
3014  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
3015  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
3016  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
3017  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
3018  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
3019  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(32, 32, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(32, bvSize1),
3020  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(33, 33, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(33, bvSize1),
3021  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(34, 34, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(34, bvSize1),
3022  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(35, 35, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(35, bvSize1),
3023  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(36, 36, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(36, bvSize1),
3024  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(37, 37, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(37, bvSize1),
3025  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(38, 38, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(38, bvSize1),
3026  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(39, 39, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(39, bvSize1),
3027  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(40, 40, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(40, bvSize1),
3028  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(41, 41, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(41, bvSize1),
3029  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(42, 42, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(42, bvSize1),
3030  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(43, 43, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(43, bvSize1),
3031  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(44, 44, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(44, bvSize1),
3032  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(45, 45, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(45, bvSize1),
3033  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(46, 46, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(46, bvSize1),
3034  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(47, 47, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(47, bvSize1),
3035  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(48, 48, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(48, bvSize1),
3036  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(49, 49, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(49, bvSize1),
3037  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(50, 50, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(50, bvSize1),
3038  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(51, 51, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(51, bvSize1),
3039  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(52, 52, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(52, bvSize1),
3040  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(53, 53, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(53, bvSize1),
3041  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(54, 54, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(54, bvSize1),
3042  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(55, 55, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(55, bvSize1),
3043  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(56, 56, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(56, bvSize1),
3044  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(57, 57, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(57, bvSize1),
3045  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(58, 58, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(58, bvSize1),
3046  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(59, 59, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(59, bvSize1),
3047  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(60, 60, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(60, bvSize1),
3048  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(61, 61, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(61, bvSize1),
3049  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(62, 62, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(62, bvSize1),
3050  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(63, 63, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(63, bvSize1),
3051  this->astCtxt.bv(0, bvSize1)
3052  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
3053  );
3054  break;
3055  default:
3056  throw triton::exceptions::Semantics("x86Semantics::bsf_s(): Invalid operand size.");
3057  }
3058 
3059  /* Create symbolic expression */
3060  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BSF operation");
3061 
3062  /* Spread taint */
3063  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3064 
3065  /* Update symbolic flags */
3066  this->zfBsf_s(inst, expr, src, op2);
3067 
3068  /* Tag undefined flags */
3069  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3070  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
3071  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3072  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3073  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3074 
3075  /* Update the symbolic control flow */
3076  this->controlFlow_s(inst);
3077  }
3078 
3079 
3080  void x86Semantics::bsr_s(triton::arch::Instruction& inst) {
3081  auto& dst = inst.operands[0];
3082  auto& src = inst.operands[1];
3083  auto bvSize1 = dst.getBitSize();
3084  auto bvSize2 = src.getBitSize();
3085 
3086  /* Create symbolic operands */
3087  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3088  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3089 
3090  /* Create the semantics */
3091  triton::ast::SharedAbstractNode node = nullptr;
3092  switch (src.getSize()) {
3093  case BYTE_SIZE:
3094  node = this->astCtxt.ite(
3095  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3096  op1,
3097  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
3098  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
3099  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
3100  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
3101  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
3102  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
3103  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
3104  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
3105  this->astCtxt.bv(0, bvSize1)
3106  ))))))))
3107  );
3108  break;
3109  case WORD_SIZE:
3110  node = this->astCtxt.ite(
3111  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3112  op1,
3113  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
3114  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
3115  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
3116  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
3117  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
3118  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
3119  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
3120  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
3121  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
3122  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
3123  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
3124  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
3125  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
3126  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
3127  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
3128  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
3129  this->astCtxt.bv(0, bvSize1)
3130  ))))))))))))))))
3131  );
3132  break;
3133  case DWORD_SIZE:
3134  node = this->astCtxt.ite(
3135  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3136  op1,
3137  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
3138  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
3139  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
3140  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
3141  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
3142  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
3143  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
3144  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
3145  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
3146  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
3147  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
3148  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
3149  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
3150  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
3151  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
3152  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
3153  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
3154  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
3155  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
3156  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
3157  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
3158  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
3159  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
3160  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
3161  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
3162  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
3163  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
3164  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
3165  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
3166  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
3167  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
3168  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
3169  this->astCtxt.bv(0, bvSize1)
3170  ))))))))))))))))))))))))))))))))
3171  );
3172  break;
3173  case QWORD_SIZE:
3174  node = this->astCtxt.ite(
3175  this->astCtxt.equal(op2, this->astCtxt.bv(0, bvSize2)), /* Apply BSR only if op2 != 0 */
3176  op1,
3177  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(63, 63, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(63, bvSize1),
3178  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(62, 62, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(62, bvSize1),
3179  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(61, 61, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(61, bvSize1),
3180  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(60, 60, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(60, bvSize1),
3181  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(59, 59, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(59, bvSize1),
3182  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(58, 58, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(58, bvSize1),
3183  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(57, 57, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(57, bvSize1),
3184  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(56, 56, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(56, bvSize1),
3185  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(55, 55, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(55, bvSize1),
3186  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(54, 54, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(54, bvSize1),
3187  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(53, 53, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(53, bvSize1),
3188  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(52, 52, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(52, bvSize1),
3189  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(51, 51, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(51, bvSize1),
3190  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(50, 50, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(50, bvSize1),
3191  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(49, 49, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(49, bvSize1),
3192  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(48, 48, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(48, bvSize1),
3193  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(47, 47, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(47, bvSize1),
3194  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(46, 46, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(46, bvSize1),
3195  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(45, 45, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(45, bvSize1),
3196  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(44, 44, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(44, bvSize1),
3197  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(43, 43, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(43, bvSize1),
3198  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(42, 42, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(42, bvSize1),
3199  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(41, 41, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(41, bvSize1),
3200  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(40, 40, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(40, bvSize1),
3201  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(39, 39, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(39, bvSize1),
3202  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(38, 38, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(38, bvSize1),
3203  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(37, 37, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(37, bvSize1),
3204  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(36, 36, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(36, bvSize1),
3205  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(35, 35, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(35, bvSize1),
3206  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(34, 34, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(34, bvSize1),
3207  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(33, 33, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(33, bvSize1),
3208  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(32, 32, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(32, bvSize1),
3209  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(31, 31, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(31, bvSize1),
3210  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(30, 30, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(30, bvSize1),
3211  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(29, 29, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(29, bvSize1),
3212  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(28, 28, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(28, bvSize1),
3213  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(27, 27, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(27, bvSize1),
3214  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(26, 26, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(26, bvSize1),
3215  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(25, 25, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(25, bvSize1),
3216  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(24, 24, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(24, bvSize1),
3217  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(23, 23, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(23, bvSize1),
3218  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(22, 22, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(22, bvSize1),
3219  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(21, 21, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(21, bvSize1),
3220  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(20, 20, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(20, bvSize1),
3221  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(19, 19, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(19, bvSize1),
3222  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(18, 18, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(18, bvSize1),
3223  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(17, 17, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(17, bvSize1),
3224  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(16, 16, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(16, bvSize1),
3225  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(15, 15, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(15, bvSize1),
3226  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(14, 14, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(14, bvSize1),
3227  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(13, 13, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(13, bvSize1),
3228  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(12, 12, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(12, bvSize1),
3229  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(11, 11, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(11, bvSize1),
3230  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(10, 10, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(10, bvSize1),
3231  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(9, 9, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(9, bvSize1),
3232  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(8, 8, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(8, bvSize1),
3233  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(7, 7, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(7, bvSize1),
3234  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(6, 6, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(6, bvSize1),
3235  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(5, 5, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(5, bvSize1),
3236  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(4, 4, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(4, bvSize1),
3237  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(3, 3, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(3, bvSize1),
3238  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(2, 2, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(2, bvSize1),
3239  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(1, 1, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(1, bvSize1),
3240  this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.extract(0, 0, op2), this->astCtxt.bvtrue()), this->astCtxt.bv(0, bvSize1),
3241  this->astCtxt.bv(0, bvSize1)
3242  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
3243  );
3244  break;
3245  default:
3246  throw triton::exceptions::Semantics("x86Semantics::bsr_s(): Invalid operand size.");
3247  }
3248 
3249  /* Create symbolic expression */
3250  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BSR operation");
3251 
3252  /* Spread taint */
3253  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3254 
3255  /* Update symbolic flags */
3256  this->zfBsf_s(inst, expr, src, op2); /* same as bsf */
3257 
3258  /* Tag undefined flags */
3259  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3260  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_CF));
3261  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3262  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3263  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3264 
3265  /* Update the symbolic control flow */
3266  this->controlFlow_s(inst);
3267  }
3268 
3269 
3270  void x86Semantics::bswap_s(triton::arch::Instruction& inst) {
3271  auto& src = inst.operands[0];
3272 
3273  /* Create symbolic operands */
3274  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3275 
3276  /* Create the semantics */
3277  std::list<triton::ast::SharedAbstractNode> bytes;
3278  switch (src.getSize()) {
3279  case QWORD_SIZE:
3280  bytes.push_front(this->astCtxt.extract(63, 56, op1));
3281  bytes.push_front(this->astCtxt.extract(55, 48, op1));
3282  bytes.push_front(this->astCtxt.extract(47, 40, op1));
3283  bytes.push_front(this->astCtxt.extract(39, 32, op1));
3284  case DWORD_SIZE:
3285  bytes.push_front(this->astCtxt.extract(31, 24, op1));
3286  bytes.push_front(this->astCtxt.extract(23, 16, op1));
3287  case WORD_SIZE:
3288  bytes.push_front(this->astCtxt.extract(15, 8, op1));
3289  bytes.push_front(this->astCtxt.extract(7, 0, op1));
3290  break;
3291  default:
3292  throw triton::exceptions::Semantics("x86Semantics::bswap_s(): Invalid operand size.");
3293  }
3294 
3295  auto node = this->astCtxt.concat(bytes);
3296 
3297  /* Create symbolic expression */
3298  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, src, "BSWAP operation");
3299 
3300  /* Spread taint */
3301  expr->isTainted = this->taintEngine->taintAssignment(src, src);
3302 
3303  /* Update the symbolic control flow */
3304  this->controlFlow_s(inst);
3305  }
3306 
3307 
3308  void x86Semantics::bt_s(triton::arch::Instruction& inst) {
3309  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3310  auto& src1 = inst.operands[0];
3311  auto& src2 = inst.operands[1];
3312 
3313  /* Create symbolic operands */
3314  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
3315  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
3316 
3317  /* Create the semantics */
3318  auto node = this->astCtxt.extract(0, 0,
3319  this->astCtxt.bvlshr(
3320  op1,
3321  this->astCtxt.bvsmod(
3322  op2,
3323  this->astCtxt.bv(src1.getBitSize(), src1.getBitSize())
3324  )
3325  )
3326  );
3327 
3328  /* Create symbolic expression */
3329  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, this->architecture->getRegister(ID_REG_X86_CF), "BT operation");
3330 
3331  /* Spread taint */
3332  expr->isTainted = this->taintEngine->taintUnion(dst, src1);
3333  expr->isTainted = this->taintEngine->taintUnion(dst, src2);
3334 
3335  /* Tag undefined flags */
3336  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3337  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3338  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3339  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3340 
3341  /* Update the symbolic control flow */
3342  this->controlFlow_s(inst);
3343  }
3344 
3345 
3346  void x86Semantics::btc_s(triton::arch::Instruction& inst) {
3347  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3348  auto& dst2 = inst.operands[0];
3349  auto& src1 = inst.operands[1];
3350 
3351  /* Create symbolic operands */
3352  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3353  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
3354 
3355  /* Create the semantics */
3356  auto node1 = this->astCtxt.extract(0, 0,
3357  this->astCtxt.bvlshr(
3358  op1,
3359  this->astCtxt.bvsmod(
3360  op2,
3361  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3362  )
3363  )
3364  );
3365  auto node2 = this->astCtxt.ite(
3366  this->astCtxt.equal(node1, this->astCtxt.bvfalse()),
3367  /* BTS */
3368  this->astCtxt.bvor(
3369  op1,
3370  this->astCtxt.bvshl(
3371  this->astCtxt.bv(1, dst2.getBitSize()),
3372  this->astCtxt.bvsmod(
3373  op2,
3374  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3375  )
3376  )
3377  ),
3378  /* BTR */
3379  this->astCtxt.bvand(
3380  op1,
3381  this->astCtxt.bvsub(
3382  op1,
3383  this->astCtxt.bvshl(
3384  this->astCtxt.bv(1, dst2.getBitSize()),
3385  this->astCtxt.bvsmod(
3386  op2,
3387  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3388  )
3389  )
3390  )
3391  )
3392  );
3393 
3394  /* Create symbolic expression */
3395  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTC carry operation");
3396  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTC complement operation");
3397 
3398  /* Spread taint */
3399  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3400  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3401  expr2->isTainted = this->taintEngine->taintUnion(dst2, dst1);
3402 
3403  /* Tag undefined flags */
3404  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3405  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3406  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3407  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3408 
3409  /* Update the symbolic control flow */
3410  this->controlFlow_s(inst);
3411  }
3412 
3413 
3414  void x86Semantics::btr_s(triton::arch::Instruction& inst) {
3415  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3416  auto& dst2 = inst.operands[0];
3417  auto& src1 = inst.operands[1];
3418 
3419  /* Create symbolic operands */
3420  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3421  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
3422 
3423  /* Create the semantics */
3424  auto node1 = this->astCtxt.extract(0, 0,
3425  this->astCtxt.bvlshr(
3426  op1,
3427  this->astCtxt.bvsmod(
3428  op2,
3429  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3430  )
3431  )
3432  );
3433  auto node2 = this->astCtxt.ite(
3434  this->astCtxt.equal(node1, this->astCtxt.bvfalse()),
3435  op1,
3436  this->astCtxt.bvand(
3437  op1,
3438  this->astCtxt.bvsub(
3439  op1,
3440  this->astCtxt.bvshl(
3441  this->astCtxt.bv(1, dst2.getBitSize()),
3442  this->astCtxt.bvsmod(
3443  op2,
3444  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3445  )
3446  )
3447  )
3448  )
3449  );
3450 
3451  /* Create symbolic expression */
3452  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTR carry operation");
3453  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTR reset operation");
3454 
3455  /* Spread taint */
3456  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3457  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3458  expr2->isTainted = this->taintEngine->taintUnion(dst2, dst1);
3459 
3460  /* Tag undefined flags */
3461  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3462  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3463  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3464  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3465 
3466  /* Update the symbolic control flow */
3467  this->controlFlow_s(inst);
3468  }
3469 
3470 
3471  void x86Semantics::bts_s(triton::arch::Instruction& inst) {
3472  auto dst1 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3473  auto& dst2 = inst.operands[0];
3474  auto& src1 = inst.operands[1];
3475 
3476  /* Create symbolic operands */
3477  auto op1 = this->symbolicEngine->getOperandAst(inst, dst2);
3478  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
3479 
3480  /* Create the semantics */
3481  auto node1 = this->astCtxt.extract(0, 0,
3482  this->astCtxt.bvlshr(
3483  op1,
3484  this->astCtxt.bvsmod(
3485  op2,
3486  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3487  )
3488  )
3489  );
3490  auto node2 = this->astCtxt.bvor(
3491  op1,
3492  this->astCtxt.bvshl(
3493  this->astCtxt.bv(1, dst2.getBitSize()),
3494  this->astCtxt.bvsmod(
3495  op2,
3496  this->astCtxt.bv(dst2.getBitSize(), dst2.getBitSize())
3497  )
3498  )
3499  );
3500 
3501  /* Create symbolic expression */
3502  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, this->architecture->getRegister(ID_REG_X86_CF), "BTS carry operation");
3503  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BTS set operation");
3504 
3505  /* Spread taint */
3506  expr1->isTainted = this->taintEngine->taintUnion(dst1, dst2);
3507  expr1->isTainted = this->taintEngine->taintUnion(dst1, src1);
3508  expr2->isTainted = this->taintEngine->taintUnion(dst2, dst1);
3509 
3510  /* Tag undefined flags */
3511  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_AF));
3512  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_OF));
3513  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_PF));
3514  this->undefined_s(inst, this->architecture->getRegister(ID_REG_X86_SF));
3515 
3516  /* Update the symbolic control flow */
3517  this->controlFlow_s(inst);
3518  }
3519 
3520 
3521  void x86Semantics::call_s(triton::arch::Instruction& inst) {
3522  auto stack = this->architecture->getStackPointer();
3523 
3524  /* Create the semantics - side effect */
3525  auto stackValue = alignSubStack_s(inst, stack.getSize());
3526  auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
3527  auto sp = triton::arch::OperandWrapper(triton::arch::MemoryAccess(stackValue, stack.getSize()));
3528  auto& src = inst.operands[0];
3529 
3530  /* Create symbolic operands */
3531  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3532 
3533  /* Create the semantics - side effect */
3534  auto node1 = this->astCtxt.bv(inst.getNextAddress(), pc.getBitSize());
3535 
3536  /* Create the semantics */
3537  auto node2 = op1;
3538 
3539  /* Create the symbolic expression */
3540  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, sp, "Saved Program Counter");
3541 
3542  /* Create symbolic expression */
3543  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, pc, "Program Counter");
3544 
3545  /* Spread taint */
3546  expr1->isTainted = this->taintEngine->taintAssignmentMemoryImmediate(sp.getMemory());
3547  expr2->isTainted = this->taintEngine->taintAssignment(pc, src);
3548 
3549  /* Create the path constraint */
3550  this->symbolicEngine->addPathConstraint(inst, expr2);
3551  }
3552 
3553 
3554  void x86Semantics::cbw_s(triton::arch::Instruction& inst) {
3555  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_AX));
3556 
3557  /* Create symbolic operands */
3558  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3559 
3560  /* Create the semantics */
3561  auto node = this->astCtxt.sx(BYTE_SIZE_BIT, this->astCtxt.extract(BYTE_SIZE_BIT-1, 0, op1));
3562 
3563  /* Create symbolic expression */
3564  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBW operation");
3565 
3566  /* Spread taint */
3567  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3568 
3569  /* Update the symbolic control flow */
3570  this->controlFlow_s(inst);
3571  }
3572 
3573 
3574  void x86Semantics::cdq_s(triton::arch::Instruction& inst) {
3575  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
3576  auto src = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
3577 
3578  /* Create symbolic operands */
3579  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
3580 
3581  /* Create the semantics - TMP = 64 bitvec (EDX:EAX) */
3582  auto node1 = this->astCtxt.sx(DWORD_SIZE_BIT, op1);
3583 
3584  /* Create symbolic expression */
3585  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "Temporary variable");
3586 
3587  /* Spread taint */
3588  expr1->isTainted = this->taintEngine->isRegisterTainted(this->architecture->getRegister(ID_REG_X86_EAX));
3589 
3590  /* Create the semantics - EDX = TMP[63...32] */
3591  auto node2 = this->astCtxt.extract(QWORD_SIZE_BIT-1, DWORD_SIZE_BIT, this->astCtxt.reference(expr1));
3592 
3593  /* Create symbolic expression */
3594  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst, "CDQ operation");
3595 
3596  /* Spread taint */
3597  expr2->isTainted = this->taintEngine->taintAssignment(dst, src);
3598 
3599  /* Update the symbolic control flow */
3600  this->controlFlow_s(inst);
3601  }
3602 
3603 
3604  void x86Semantics::cdqe_s(triton::arch::Instruction& inst) {
3605  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
3606 
3607  /* Create symbolic operands */
3608  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3609 
3610  /* Create the semantics */
3611  auto node = this->astCtxt.sx(DWORD_SIZE_BIT, this->astCtxt.extract(DWORD_SIZE_BIT-1, 0, op1));
3612 
3613  /* Create symbolic expression */
3614  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CDQE operation");
3615 
3616  /* Spread taint */
3617  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3618 
3619  /* Update the symbolic control flow */
3620  this->controlFlow_s(inst);
3621  }
3622 
3623 
3624  void x86Semantics::clc_s(triton::arch::Instruction& inst) {
3625  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_CF), "Clears carry flag");
3626  /* Update the symbolic control flow */
3627  this->controlFlow_s(inst);
3628  }
3629 
3630 
3631  void x86Semantics::cld_s(triton::arch::Instruction& inst) {
3632  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_DF), "Clears direction flag");
3633  /* Update the symbolic control flow */
3634  this->controlFlow_s(inst);
3635  }
3636 
3637 
3638  void x86Semantics::clflush_s(triton::arch::Instruction& inst) {
3639  /* Update the symbolic control flow */
3640  this->controlFlow_s(inst);
3641  }
3642 
3643 
3644  void x86Semantics::clts_s(triton::arch::Instruction& inst) {
3645  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CR0));
3646 
3647  /* Create symbolic operands */
3648  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3649 
3650  /* Create the semantics */
3651  triton::ast::SharedAbstractNode node = nullptr;
3652 
3653  switch (dst.getBitSize()) {
3654  case QWORD_SIZE_BIT:
3655  node = this->astCtxt.bvand(op1, this->astCtxt.bv(0xfffffffffffffff7, QWORD_SIZE_BIT));
3656  break;
3657  case DWORD_SIZE_BIT:
3658  node = this->astCtxt.bvand(op1, this->astCtxt.bv(0xfffffff7, DWORD_SIZE_BIT));
3659  break;
3660  default:
3661  throw triton::exceptions::Semantics("x86Semantics::clts_s(): Invalid operand size.");
3662  }
3663 
3664  /* Create symbolic expression */
3665  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CLTS operation");
3666 
3667  /* Spread taint */
3668  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3669 
3670  /* Update the symbolic control flow */
3671  this->controlFlow_s(inst);
3672  }
3673 
3674 
3675  void x86Semantics::cli_s(triton::arch::Instruction& inst) {
3676  this->clearFlag_s(inst, this->architecture->getRegister(ID_REG_X86_IF), "Clears interrupt flag");
3677  /* Update the symbolic control flow */
3678  this->controlFlow_s(inst);
3679  }
3680 
3681 
3682  void x86Semantics::cmc_s(triton::arch::Instruction& inst) {
3683  auto dst = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3684 
3685  /* Create symbolic operands */
3686  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3687 
3688  /* Create the semantics */
3689  auto node = this->astCtxt.bvnot(op1);
3690 
3691  /* Create symbolic expression */
3692  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst.getRegister(), "CMC operation");
3693 
3694  /* Spread taint */
3695  expr->isTainted = this->taintEngine->taintAssignment(dst, dst);
3696 
3697  /* Update the symbolic control flow */
3698  this->controlFlow_s(inst);
3699  }
3700 
3701 
3702  void x86Semantics::cmova_s(triton::arch::Instruction& inst) {
3703  auto& dst = inst.operands[0];
3704  auto& src = inst.operands[1];
3705  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3706  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3707 
3708  /* Create symbolic operands */
3709  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3710  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3711  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3712  auto op4 = this->symbolicEngine->getOperandAst(inst, zf);
3713 
3714  /* Create the semantics */
3715  auto node = this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.bvand(this->astCtxt.bvnot(op3), this->astCtxt.bvnot(op4)), this->astCtxt.bvtrue()), op2, op1);
3716 
3717  /* Create symbolic expression */
3718  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVA operation");
3719 
3720  /* Spread taint and condition flag */
3721  if (op3->evaluate().is_zero() && op4->evaluate().is_zero()) {
3722  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3723  inst.setConditionTaken(true);
3724  }
3725  else
3726  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3727 
3728  /* Update the symbolic control flow */
3729  this->controlFlow_s(inst);
3730  }
3731 
3732 
3733  void x86Semantics::cmovae_s(triton::arch::Instruction& inst) {
3734  auto& dst = inst.operands[0];
3735  auto& src = inst.operands[1];
3736  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3737 
3738  /* Create symbolic operands */
3739  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3740  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3741  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3742 
3743  /* Create the semantics */
3744  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvfalse()), op2, op1);
3745 
3746  /* Create symbolic expression */
3747  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVAE operation");
3748 
3749  /* Spread taint and condition flag */
3750  if (op3->evaluate().is_zero()) {
3751  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3752  inst.setConditionTaken(true);
3753  }
3754  else
3755  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3756 
3757  /* Update the symbolic control flow */
3758  this->controlFlow_s(inst);
3759  }
3760 
3761 
3762  void x86Semantics::cmovb_s(triton::arch::Instruction& inst) {
3763  auto& dst = inst.operands[0];
3764  auto& src = inst.operands[1];
3765  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3766 
3767  /* Create symbolic operands */
3768  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3769  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3770  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3771 
3772  /* Create the semantics */
3773  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvtrue()), op2, op1);
3774 
3775  /* Create symbolic expression */
3776  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVB operation");
3777 
3778  /* Spread taint and condition flag */
3779  if (!op3->evaluate().is_zero()) {
3780  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3781  inst.setConditionTaken(true);
3782  }
3783  else
3784  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3785 
3786  /* Update the symbolic control flow */
3787  this->controlFlow_s(inst);
3788  }
3789 
3790 
3791  void x86Semantics::cmovbe_s(triton::arch::Instruction& inst) {
3792  auto& dst = inst.operands[0];
3793  auto& src = inst.operands[1];
3794  auto cf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_CF));
3795  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3796 
3797  /* Create symbolic operands */
3798  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3799  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3800  auto op3 = this->symbolicEngine->getOperandAst(inst, cf);
3801  auto op4 = this->symbolicEngine->getOperandAst(inst, zf);
3802 
3803  /* Create the semantics */
3804  auto node = this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.bvor(op3, op4), this->astCtxt.bvtrue()), op2, op1);
3805 
3806  /* Create symbolic expression */
3807  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVBE operation");
3808 
3809  /* Spread taint and condition flag */
3810  if (!op3->evaluate().is_zero() || !op4->evaluate().is_zero()) {
3811  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3812  inst.setConditionTaken(true);
3813  }
3814  else
3815  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3816 
3817  /* Update the symbolic control flow */
3818  this->controlFlow_s(inst);
3819  }
3820 
3821 
3822  void x86Semantics::cmove_s(triton::arch::Instruction& inst) {
3823  auto& dst = inst.operands[0];
3824  auto& src = inst.operands[1];
3825  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3826 
3827  /* Create symbolic operands */
3828  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3829  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3830  auto op3 = this->symbolicEngine->getOperandAst(inst, zf);
3831 
3832  /* Create the semantics */
3833  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvtrue()), op2, op1);
3834 
3835  /* Create symbolic expression */
3836  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVE operation");
3837 
3838  /* Spread taint and condition flag */
3839  if (!op3->evaluate().is_zero()) {
3840  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3841  inst.setConditionTaken(true);
3842  }
3843  else
3844  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3845 
3846  /* Update the symbolic control flow */
3847  this->controlFlow_s(inst);
3848  }
3849 
3850 
3851  void x86Semantics::cmovg_s(triton::arch::Instruction& inst) {
3852  auto& dst = inst.operands[0];
3853  auto& src = inst.operands[1];
3854  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3855  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3856  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3857 
3858  /* Create symbolic operands */
3859  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3860  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3861  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3862  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3863  auto op5 = this->symbolicEngine->getOperandAst(inst, zf);
3864 
3865  /* Create the semantics */
3866  auto node = this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.bvor(this->astCtxt.bvxor(op3, op4), op5), this->astCtxt.bvfalse()), op2, op1);
3867 
3868  /* Create symbolic expression */
3869  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVG operation");
3870 
3871  /* Spread taint and condition flag */
3872  if ((op3->evaluate().is_zero() == op4->evaluate().is_zero()) && op5->evaluate().is_zero()) {
3873  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3874  inst.setConditionTaken(true);
3875  }
3876  else
3877  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3878 
3879  /* Update the symbolic control flow */
3880  this->controlFlow_s(inst);
3881  }
3882 
3883 
3884  void x86Semantics::cmovge_s(triton::arch::Instruction& inst) {
3885  auto& dst = inst.operands[0];
3886  auto& src = inst.operands[1];
3887  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3888  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3889 
3890  /* Create symbolic operands */
3891  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3892  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3893  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3894  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3895 
3896  /* Create the semantics */
3897  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, op4), op2, op1);
3898 
3899  /* Create symbolic expression */
3900  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVGE operation");
3901 
3902  /* Spread taint and condition flag */
3903  if (op3->evaluate().is_zero() == op4->evaluate().is_zero()) {
3904  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3905  inst.setConditionTaken(true);
3906  }
3907  else
3908  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3909 
3910  /* Update the symbolic control flow */
3911  this->controlFlow_s(inst);
3912  }
3913 
3914 
3915  void x86Semantics::cmovl_s(triton::arch::Instruction& inst) {
3916  auto& dst = inst.operands[0];
3917  auto& src = inst.operands[1];
3918  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3919  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3920 
3921  /* Create symbolic operands */
3922  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3923  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3924  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3925  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3926 
3927  /* Create the semantics */
3928  auto node = this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.bvxor(op3, op4), this->astCtxt.bvtrue()), op2, op1);
3929 
3930  /* Create symbolic expression */
3931  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVL operation");
3932 
3933  /* Spread taint and condition flag */
3934  if (op3->evaluate().is_zero() != op4->evaluate().is_zero()) {
3935  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3936  inst.setConditionTaken(true);
3937  }
3938  else
3939  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3940 
3941  /* Update the symbolic control flow */
3942  this->controlFlow_s(inst);
3943  }
3944 
3945 
3946  void x86Semantics::cmovle_s(triton::arch::Instruction& inst) {
3947  auto& dst = inst.operands[0];
3948  auto& src = inst.operands[1];
3949  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
3950  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
3951  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3952 
3953  /* Create symbolic operands */
3954  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3955  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3956  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
3957  auto op4 = this->symbolicEngine->getOperandAst(inst, of);
3958  auto op5 = this->symbolicEngine->getOperandAst(inst, zf);
3959 
3960  /* Create the semantics */
3961  auto node = this->astCtxt.ite(this->astCtxt.equal(this->astCtxt.bvor(this->astCtxt.bvxor(op3, op4), op5), this->astCtxt.bvtrue()), op2, op1);
3962 
3963  /* Create symbolic expression */
3964  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVBE operation");
3965 
3966  /* Spread taint and condition flag */
3967  if ((op3->evaluate().is_zero() != op4->evaluate().is_zero()) || !op5->evaluate().is_zero()) {
3968  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3969  inst.setConditionTaken(true);
3970  }
3971  else
3972  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
3973 
3974  /* Update the symbolic control flow */
3975  this->controlFlow_s(inst);
3976  }
3977 
3978 
3979  void x86Semantics::cmovne_s(triton::arch::Instruction& inst) {
3980  auto& dst = inst.operands[0];
3981  auto& src = inst.operands[1];
3982  auto zf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ZF));
3983 
3984  /* Create symbolic operands */
3985  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
3986  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
3987  auto op3 = this->symbolicEngine->getOperandAst(inst, zf);
3988 
3989  /* Create the semantics */
3990  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvfalse()), op2, op1);
3991 
3992  /* Create symbolic expression */
3993  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNE operation");
3994 
3995  /* Spread taint and condition flag */
3996  if (op3->evaluate().is_zero()) {
3997  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
3998  inst.setConditionTaken(true);
3999  }
4000  else
4001  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4002 
4003  /* Update the symbolic control flow */
4004  this->controlFlow_s(inst);
4005  }
4006 
4007 
4008  void x86Semantics::cmovno_s(triton::arch::Instruction& inst) {
4009  auto& dst = inst.operands[0];
4010  auto& src = inst.operands[1];
4011  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
4012 
4013  /* Create symbolic operands */
4014  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4015  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4016  auto op3 = this->symbolicEngine->getOperandAst(inst, of);
4017 
4018  /* Create the semantics */
4019  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvfalse()), op2, op1);
4020 
4021  /* Create symbolic expression */
4022  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNO operation");
4023 
4024  /* Spread taint and condition flag */
4025  if (op3->evaluate().is_zero()) {
4026  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4027  inst.setConditionTaken(true);
4028  }
4029  else
4030  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4031 
4032  /* Update the symbolic control flow */
4033  this->controlFlow_s(inst);
4034  }
4035 
4036 
4037  void x86Semantics::cmovnp_s(triton::arch::Instruction& inst) {
4038  auto& dst = inst.operands[0];
4039  auto& src = inst.operands[1];
4040  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
4041 
4042  /* Create symbolic operands */
4043  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4044  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4045  auto op3 = this->symbolicEngine->getOperandAst(inst, pf);
4046 
4047  /* Create the semantics */
4048  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvfalse()), op2, op1);
4049 
4050  /* Create symbolic expression */
4051  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNP operation");
4052 
4053  /* Spread taint and condition flag */
4054  if (op3->evaluate().is_zero()) {
4055  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4056  inst.setConditionTaken(true);
4057  }
4058  else
4059  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4060 
4061  /* Update the symbolic control flow */
4062  this->controlFlow_s(inst);
4063  }
4064 
4065 
4066  void x86Semantics::cmovns_s(triton::arch::Instruction& inst) {
4067  auto& dst = inst.operands[0];
4068  auto& src = inst.operands[1];
4069  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
4070 
4071  /* Create symbolic operands */
4072  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4073  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4074  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
4075 
4076  /* Create the semantics */
4077  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvfalse()), op2, op1);
4078 
4079  /* Create symbolic expression */
4080  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVNS operation");
4081 
4082  /* Spread taint and condition flag */
4083  if (op3->evaluate().is_zero()) {
4084  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4085  inst.setConditionTaken(true);
4086  }
4087  else
4088  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4089 
4090  /* Update the symbolic control flow */
4091  this->controlFlow_s(inst);
4092  }
4093 
4094 
4095  void x86Semantics::cmovo_s(triton::arch::Instruction& inst) {
4096  auto& dst = inst.operands[0];
4097  auto& src = inst.operands[1];
4098  auto of = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_OF));
4099 
4100  /* Create symbolic operands */
4101  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4102  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4103  auto op3 = this->symbolicEngine->getOperandAst(inst, of);
4104 
4105  /* Create the semantics */
4106  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvtrue()), op2, op1);
4107 
4108  /* Create symbolic expression */
4109  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVO operation");
4110 
4111  /* Spread taint and condition flag */
4112  if (!op3->evaluate().is_zero()) {
4113  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4114  inst.setConditionTaken(true);
4115  }
4116  else
4117  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4118 
4119  /* Update the symbolic control flow */
4120  this->controlFlow_s(inst);
4121  }
4122 
4123 
4124  void x86Semantics::cmovp_s(triton::arch::Instruction& inst) {
4125  auto& dst = inst.operands[0];
4126  auto& src = inst.operands[1];
4127  auto pf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_PF));
4128 
4129  /* Create symbolic operands */
4130  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4131  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4132  auto op3 = this->symbolicEngine->getOperandAst(inst, pf);
4133 
4134  /* Create the semantics */
4135  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvtrue()), op2, op1);
4136 
4137  /* Create symbolic expression */
4138  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVP operation");
4139 
4140  /* Spread taint and condition flag */
4141  if (!op3->evaluate().is_zero()) {
4142  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4143  inst.setConditionTaken(true);
4144  }
4145  else
4146  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4147 
4148  /* Update the symbolic control flow */
4149  this->controlFlow_s(inst);
4150  }
4151 
4152 
4153  void x86Semantics::cmovs_s(triton::arch::Instruction& inst) {
4154  auto& dst = inst.operands[0];
4155  auto& src = inst.operands[1];
4156  auto sf = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_SF));
4157 
4158  /* Create symbolic operands */
4159  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4160  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4161  auto op3 = this->symbolicEngine->getOperandAst(inst, sf);
4162 
4163  /* Create the semantics */
4164  auto node = this->astCtxt.ite(this->astCtxt.equal(op3, this->astCtxt.bvtrue()), op2, op1);
4165 
4166  /* Create symbolic expression */
4167  auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CMOVS operation");
4168 
4169  /* Spread taint and condition flag */
4170  if (!op3->evaluate().is_zero()) {
4171  expr->isTainted = this->taintEngine->taintAssignment(dst, src);
4172  inst.setConditionTaken(true);
4173  }
4174  else
4175  expr->isTainted = this->taintEngine->taintUnion(dst, dst);
4176 
4177  /* Update the symbolic control flow */
4178  this->controlFlow_s(inst);
4179  }
4180 
4181 
4182  void x86Semantics::cmp_s(triton::arch::Instruction& inst) {
4183  auto& dst = inst.operands[0];
4184  auto& src = inst.operands[1];
4185 
4186  /* Create symbolic operands */
4187  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4188  auto op2 = this->astCtxt.sx(dst.getBitSize() - src.getBitSize(), this->symbolicEngine->getOperandAst(inst, src));
4189 
4190  /* Create the semantics */
4191  auto node = this->astCtxt.bvsub(op1, op2);
4192 
4193  /* Create symbolic expression */
4194  auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, "CMP operation");
4195 
4196  /* Spread taint */
4197  expr->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4198 
4199  /* Update symbolic flags */
4200  this->af_s(inst, expr, dst, op1, op2, true);
4201  this->cfSub_s(inst, expr, dst, op1, op2, true);
4202  this->ofSub_s(inst, expr, dst, op1, op2, true);
4203  this->pf_s(inst, expr, dst, true);
4204  this->sf_s(inst, expr, dst, true);
4205  this->zf_s(inst, expr, dst, true);
4206 
4207  /* Update the symbolic control flow */
4208  this->controlFlow_s(inst);
4209  }
4210 
4211 
4212  void x86Semantics::cmpsb_s(triton::arch::Instruction& inst) {
4213  auto& dst = inst.operands[0];
4214  auto& src = inst.operands[1];
4215  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4216  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4217  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4218  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4219 
4220  /* If the REP prefix is defined, convert REP into REPE */
4223 
4224  /* Check if there is a REP prefix and a counter to zero */
4225  auto cnt = this->symbolicEngine->getOperandAst(cx);
4226  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4227  this->controlFlow_s(inst);
4228  return;
4229  }
4230 
4231  /* Create symbolic operands */
4232  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4233  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4234  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4235  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4236  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4237 
4238  /* Create the semantics */
4239  auto node1 = this->astCtxt.bvsub(op1, op2);
4240  auto node2 = this->astCtxt.ite(
4241  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4242  this->astCtxt.bvadd(op3, this->astCtxt.bv(BYTE_SIZE, index1.getBitSize())),
4243  this->astCtxt.bvsub(op3, this->astCtxt.bv(BYTE_SIZE, index1.getBitSize()))
4244  );
4245  auto node3 = this->astCtxt.ite(
4246  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4247  this->astCtxt.bvadd(op4, this->astCtxt.bv(BYTE_SIZE, index2.getBitSize())),
4248  this->astCtxt.bvsub(op4, this->astCtxt.bv(BYTE_SIZE, index2.getBitSize()))
4249  );
4250 
4251  /* Create symbolic expression */
4252  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSB operation");
4253  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4254  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4255 
4256  /* Spread taint */
4257  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4258  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4259  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4260 
4261  /* Update symbolic flags */
4262  this->af_s(inst, expr1, dst, op1, op2, true);
4263  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4264  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4265  this->pf_s(inst, expr1, dst, true);
4266  this->sf_s(inst, expr1, dst, true);
4267  this->zf_s(inst, expr1, dst, true);
4268 
4269  /* Update the symbolic control flow */
4270  this->controlFlow_s(inst);
4271  }
4272 
4273 
4274  void x86Semantics::cmpsd_s(triton::arch::Instruction& inst) {
4275  auto& dst = inst.operands[0];
4276  auto& src = inst.operands[1];
4277  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4278  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4279  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4280  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4281 
4282  /* If the REP prefix is defined, convert REP into REPE */
4285 
4286  /* Check if there is a REP prefix and a counter to zero */
4287  auto cnt = this->symbolicEngine->getOperandAst(cx);
4288  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4289  this->controlFlow_s(inst);
4290  return;
4291  }
4292 
4293  /* Create symbolic operands */
4294  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4295  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4296  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4297  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4298  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4299 
4300  /* Create the semantics */
4301  auto node1 = this->astCtxt.bvsub(op1, op2);
4302  auto node2 = this->astCtxt.ite(
4303  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4304  this->astCtxt.bvadd(op3, this->astCtxt.bv(DWORD_SIZE, index1.getBitSize())),
4305  this->astCtxt.bvsub(op3, this->astCtxt.bv(DWORD_SIZE, index1.getBitSize()))
4306  );
4307  auto node3 = this->astCtxt.ite(
4308  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4309  this->astCtxt.bvadd(op4, this->astCtxt.bv(DWORD_SIZE, index2.getBitSize())),
4310  this->astCtxt.bvsub(op4, this->astCtxt.bv(DWORD_SIZE, index2.getBitSize()))
4311  );
4312 
4313  /* Create symbolic expression */
4314  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSD operation");
4315  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4316  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4317 
4318  /* Spread taint */
4319  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4320  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4321  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4322 
4323  /* Update symbolic flags */
4324  this->af_s(inst, expr1, dst, op1, op2, true);
4325  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4326  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4327  this->pf_s(inst, expr1, dst, true);
4328  this->sf_s(inst, expr1, dst, true);
4329  this->zf_s(inst, expr1, dst, true);
4330 
4331  /* Update the symbolic control flow */
4332  this->controlFlow_s(inst);
4333  }
4334 
4335 
4336  void x86Semantics::cmpsq_s(triton::arch::Instruction& inst) {
4337  auto& dst = inst.operands[0];
4338  auto& src = inst.operands[1];
4339  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4340  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4341  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4342  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4343 
4344  /* If the REP prefix is defined, convert REP into REPE */
4347 
4348  /* Check if there is a REP prefix and a counter to zero */
4349  auto cnt = this->symbolicEngine->getOperandAst(cx);
4350  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4351  this->controlFlow_s(inst);
4352  return;
4353  }
4354 
4355  /* Create symbolic operands */
4356  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4357  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4358  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4359  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4360  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4361 
4362  /* Create the semantics */
4363  auto node1 = this->astCtxt.bvsub(op1, op2);
4364  auto node2 = this->astCtxt.ite(
4365  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4366  this->astCtxt.bvadd(op3, this->astCtxt.bv(QWORD_SIZE, index1.getBitSize())),
4367  this->astCtxt.bvsub(op3, this->astCtxt.bv(QWORD_SIZE, index1.getBitSize()))
4368  );
4369  auto node3 = this->astCtxt.ite(
4370  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4371  this->astCtxt.bvadd(op4, this->astCtxt.bv(QWORD_SIZE, index2.getBitSize())),
4372  this->astCtxt.bvsub(op4, this->astCtxt.bv(QWORD_SIZE, index2.getBitSize()))
4373  );
4374 
4375  /* Create symbolic expression */
4376  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSQ operation");
4377  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4378  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4379 
4380  /* Spread taint */
4381  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4382  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4383  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4384 
4385  /* Update symbolic flags */
4386  this->af_s(inst, expr1, dst, op1, op2, true);
4387  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4388  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4389  this->pf_s(inst, expr1, dst, true);
4390  this->sf_s(inst, expr1, dst, true);
4391  this->zf_s(inst, expr1, dst, true);
4392 
4393  /* Update the symbolic control flow */
4394  this->controlFlow_s(inst);
4395  }
4396 
4397 
4398  void x86Semantics::cmpsw_s(triton::arch::Instruction& inst) {
4399  auto& dst = inst.operands[0];
4400  auto& src = inst.operands[1];
4401  auto index1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_SI));
4402  auto index2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DI));
4403  auto cx = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4404  auto df = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_DF));
4405 
4406  /* If the REP prefix is defined, convert REP into REPE */
4409 
4410  /* Check if there is a REP prefix and a counter to zero */
4411  auto cnt = this->symbolicEngine->getOperandAst(cx);
4412  if (inst.getPrefix() != triton::arch::x86::ID_PREFIX_INVALID && cnt->evaluate().is_zero()) {
4413  this->controlFlow_s(inst);
4414  return;
4415  }
4416 
4417  /* Create symbolic operands */
4418  auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
4419  auto op2 = this->symbolicEngine->getOperandAst(inst, src);
4420  auto op3 = this->symbolicEngine->getOperandAst(inst, index1);
4421  auto op4 = this->symbolicEngine->getOperandAst(inst, index2);
4422  auto op5 = this->symbolicEngine->getOperandAst(inst, df);
4423 
4424  /* Create the semantics */
4425  auto node1 = this->astCtxt.bvsub(op1, op2);
4426  auto node2 = this->astCtxt.ite(
4427  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4428  this->astCtxt.bvadd(op3, this->astCtxt.bv(WORD_SIZE, index1.getBitSize())),
4429  this->astCtxt.bvsub(op3, this->astCtxt.bv(WORD_SIZE, index1.getBitSize()))
4430  );
4431  auto node3 = this->astCtxt.ite(
4432  this->astCtxt.equal(op5, this->astCtxt.bvfalse()),
4433  this->astCtxt.bvadd(op4, this->astCtxt.bv(WORD_SIZE, index2.getBitSize())),
4434  this->astCtxt.bvsub(op4, this->astCtxt.bv(WORD_SIZE, index2.getBitSize()))
4435  );
4436 
4437  /* Create symbolic expression */
4438  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMPSW operation");
4439  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, index1, "Index (SI) operation");
4440  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, index2, "Index (DI) operation");
4441 
4442  /* Spread taint */
4443  expr1->isTainted = this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src);
4444  expr2->isTainted = this->taintEngine->taintUnion(index1, index1);
4445  expr3->isTainted = this->taintEngine->taintUnion(index2, index2);
4446 
4447  /* Update symbolic flags */
4448  this->af_s(inst, expr1, dst, op1, op2, true);
4449  this->cfSub_s(inst, expr1, dst, op1, op2, true);
4450  this->ofSub_s(inst, expr1, dst, op1, op2, true);
4451  this->pf_s(inst, expr1, dst, true);
4452  this->sf_s(inst, expr1, dst, true);
4453  this->zf_s(inst, expr1, dst, true);
4454 
4455  /* Update the symbolic control flow */
4456  this->controlFlow_s(inst);
4457  }
4458 
4459 
4460  void x86Semantics::cmpxchg_s(triton::arch::Instruction& inst) {
4461  auto& src1 = inst.operands[0];
4462  auto& src2 = inst.operands[1];
4463 
4464  /* Create the tempory accumulator */
4465  triton::arch::OperandWrapper accumulator(this->architecture->getRegister(ID_REG_X86_AL));
4466  triton::arch::OperandWrapper accumulatorp(this->architecture->getParentRegister(ID_REG_X86_AL));
4467 
4468  switch (src1.getSize()) {
4469  case WORD_SIZE:
4470  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_AX)));
4471  break;
4472  case DWORD_SIZE:
4473  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_EAX)));
4474  break;
4475  case QWORD_SIZE:
4476  accumulator.setRegister(arch::Register(this->architecture->getRegister(ID_REG_X86_RAX)));
4477  break;
4478  }
4479 
4480  /* Create symbolic operands */
4481  auto op1 = this->symbolicEngine->getOperandAst(inst, accumulator);
4482  auto op2 = this->symbolicEngine->getOperandAst(inst, src1);
4483  auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
4484  auto op1p = this->symbolicEngine->getOperandAst(accumulatorp);
4485  auto op2p = this->symbolicEngine->getRegisterAst((src1.getType() == triton::arch::OP_REG ? Register(this->architecture->getParentRegister(src1.getRegister())) : accumulatorp.getRegister()));
4486  auto op3p = this->symbolicEngine->getRegisterAst((src1.getType() == triton::arch::OP_REG ? Register(this->architecture->getParentRegister(src2.getRegister())) : accumulatorp.getRegister()));
4487 
4488  /* Create the semantics */
4489  auto nodeq = this->astCtxt.equal(op1, op2);
4490  auto node1 = this->astCtxt.bvsub(op1, op2);
4491  auto node2 = this->astCtxt.ite(nodeq, op3, op2);
4492  auto node3 = this->astCtxt.ite(nodeq, op1, op2);
4493  auto node2p = this->astCtxt.ite(nodeq, op3p, op2p);
4494  auto node3p = this->astCtxt.ite(nodeq, op1p, op2p);
4495 
4496  /* Create symbolic expression */
4497  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4498  auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, "Temporary operation");
4499  auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2p, "Temporary operation");
4500  auto expr4 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, "Temporary operation");
4501  auto expr5 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3p, "Temporary operation");
4502 
4505 
4506  /* Destination */
4507  if (nodeq->evaluate() == false && src1.getType() == triton::arch::OP_REG) {
4508  const auto& src1p = this->architecture->getParentRegister(src1.getRegister());
4509  expr6 = this->symbolicEngine->createSymbolicRegisterExpression(inst, node2p, src1p, "XCHG operation");
4510  } else
4511  expr6 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG operation");
4512 
4513  /* Accumulator */
4514  if (nodeq->evaluate() == true)
4515  expr7 = this->symbolicEngine->createSymbolicExpression(inst, node3p, accumulatorp, "XCHG operation");
4516  else
4517  expr7 = this->symbolicEngine->createSymbolicExpression(inst, node3, accumulator, "XCHG operation");
4518 
4519  /* Spread taint */
4520  expr1->isTainted = this->taintEngine->isTainted(accumulator) | this->taintEngine->isTainted(src1);
4521  expr2->isTainted = expr1->isTainted;
4522  expr3->isTainted = expr1->isTainted;
4523  expr4->isTainted = expr1->isTainted;
4524  expr5->isTainted = expr1->isTainted;
4525  expr6->isTainted = this->taintEngine->taintAssignment(src1, src2);
4526  expr7->isTainted = this->taintEngine->taintAssignment(accumulator, src1);
4527 
4528  /* Update symbolic flags */
4529  this->af_s(inst, expr1, accumulator, op1, op2, true);
4530  this->cfSub_s(inst, expr1, accumulator, op1, op2, true);
4531  this->ofSub_s(inst, expr1, accumulator, op1, op2, true);
4532  this->pf_s(inst, expr1, accumulator, true);
4533  this->sf_s(inst, expr1, accumulator, true);
4534  this->zf_s(inst, expr1, accumulator, true);
4535 
4536  /* Update the symbolic control flow */
4537  this->controlFlow_s(inst);
4538  }
4539 
4540 
4541  void x86Semantics::cmpxchg16b_s(triton::arch::Instruction& inst) {
4542  auto& src1 = inst.operands[0];
4543  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RDX));
4544  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RAX));
4545  auto src4 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RCX));
4546  auto src5 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_RBX));
4547 
4548  /* Create symbolic operands */
4549  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
4550  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
4551  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
4552  auto op4 = this->symbolicEngine->getOperandAst(inst, src4);
4553  auto op5 = this->symbolicEngine->getOperandAst(inst, src5);
4554 
4555  /* Create the semantics */
4556  /* CMP8B */
4557  auto node1 = this->astCtxt.bvsub(this->astCtxt.concat(op2, op3), op1);
4558  /* Destination */
4559  auto node2 = this->astCtxt.ite(this->astCtxt.equal(node1, this->astCtxt.bv(0, DQWORD_SIZE_BIT)), this->astCtxt.concat(op4, op5), op1);
4560  /* EDX:EAX */
4561  auto node3 = this->astCtxt.ite(this->astCtxt.equal(node1, this->astCtxt.bv(0, DQWORD_SIZE_BIT)), this->astCtxt.concat(op2, op3), op1);
4562 
4563  /* Create symbolic expression */
4564  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4565  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG16B memory operation");
4566  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract(127, 64, node3), src2, "XCHG16B RDX operation");
4567  auto expr4 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract(63, 0, node3), src3, "XCHG16B RAX operation");
4568 
4569  /* Spread taint */
4570  expr1->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4571  expr2->isTainted = this->taintEngine->setTaint(src1, this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
4572  expr3->isTainted = this->taintEngine->taintAssignment(src2, src1);
4573  expr4->isTainted = this->taintEngine->taintAssignment(src3, src1);
4574 
4575  /* Update symbolic flags */
4576  this->zf_s(inst, expr1, src1, true);
4577 
4578  /* Update the symbolic control flow */
4579  this->controlFlow_s(inst);
4580  }
4581 
4582 
4583  void x86Semantics::cmpxchg8b_s(triton::arch::Instruction& inst) {
4584  auto& src1 = inst.operands[0];
4585  auto src2 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EDX));
4586  auto src3 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EAX));
4587  auto src4 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_ECX));
4588  auto src5 = triton::arch::OperandWrapper(this->architecture->getRegister(ID_REG_X86_EBX));
4589  auto src2p = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_EDX));
4590  auto src3p = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_EAX));
4591 
4592  /* Create symbolic operands */
4593  auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
4594  auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
4595  auto op3 = this->symbolicEngine->getOperandAst(inst, src3);
4596  auto op4 = this->symbolicEngine->getOperandAst(inst, src4);
4597  auto op5 = this->symbolicEngine->getOperandAst(inst, src5);
4598  auto op2p = this->symbolicEngine->getOperandAst(inst, src2p);
4599  auto op3p = this->symbolicEngine->getOperandAst(inst, src3p);
4600 
4601  /* Create the semantics */
4602  /* CMP8B */
4603  auto node1 = this->astCtxt.bvsub(this->astCtxt.concat(op2, op3), op1);
4604  /* Destination */
4605  auto node2 = this->astCtxt.ite(this->astCtxt.equal(node1, this->astCtxt.bv(0, QWORD_SIZE_BIT)), this->astCtxt.concat(op4, op5), op1);
4606  /* EDX:EAX */
4607  auto node3 = this->astCtxt.ite(this->astCtxt.equal(node1, this->astCtxt.bv(0, QWORD_SIZE_BIT)), this->astCtxt.concat(op2, op3), op1);
4608  auto node3p = this->astCtxt.ite(
4609  this->astCtxt.equal(
4610  node1,
4611  this->astCtxt.bv(0, QWORD_SIZE_BIT)),
4612  this->astCtxt.concat(op2p, op3p),
4613  this->astCtxt.zx(src2p.getBitSize() + src3p.getBitSize() - src1.getBitSize(), op1)
4614  );
4615 
4616  /* Create symbolic expression */
4617  auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, "CMP operation");
4618  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, src1, "XCHG8B memory operation");
4619  auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, "Temporary operation");
4620  auto expr4 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3p, "Temporary operation");
4621 
4624 
4625  /* EDX */
4626  if (node1->evaluate() == 0)
4627  expr5 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract((src2p.getBitSize() * 2 - 1), src2p.getBitSize(), node3p), src2p, "XCHG8B EDX operation");
4628  else
4629  expr5 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract(63, 32, node3), src2, "XCHG8B EDX operation");
4630 
4631  /* EAX */
4632  if (node1->evaluate() == 0)
4633  expr6 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract(src2p.getBitSize() - 1, 0, node3p), src3p, "XCHG8B EAX operation");
4634  else
4635  expr6 = this->symbolicEngine->createSymbolicExpression(inst, this->astCtxt.extract(31, 0, node3), src3, "XCHG8B EAX operation");
4636 
4637  /* Spread taint */
4638  expr1->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4639  expr2->isTainted = this->taintEngine->setTaint(src1, this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
4640  expr3->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4641  expr4->isTainted = this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3);
4642  expr5->isTainted = this->taintEngine->taintAssignment(src2, src1);
4643  expr6->isTainted = this->taintEngine->taintAssignment(src3, src1);
4644 
4645  /* Update symbolic flags */
4646  this->zf_s(inst, expr1, src1, true);
4647 
4648  /* Update the symbolic control flow */
4649  this->controlFlow_s(inst);
4650  }
4651 
4652 
4653  void x86Semantics::cpuid_s(triton::arch::Instruction& inst) {
4654  auto src = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_AX));
4655  auto dst1 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_AX));
4656  auto dst2 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_BX));
4657  auto dst3 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_CX));
4658  auto dst4 = triton::arch::OperandWrapper(this->architecture->getParentRegister(ID_REG_X86_DX));
4659 
4660  /* Create symbolic operands */
4661  auto op1 = this->symbolicEngine->getOperandAst(inst, src);
4662 
4663  /* Create the semantics */
4664  triton::ast::SharedAbstractNode node1 = nullptr;
4665  triton::ast::SharedAbstractNode node2 = nullptr;
4666  triton::ast::SharedAbstractNode node3 = nullptr;
4667  triton::ast::SharedAbstractNode node4 = nullptr;
4668 
4669  /* In this case, we concretize the AX option */
4670  switch (op1->evaluate().convert_to<triton::uint32>()) {
4671  case 0:
4672  node1 = this->astCtxt.bv(0x0000000d, dst1.getBitSize());
4673  node2 = this->astCtxt.bv(0x756e6547, dst2.getBitSize());
4674  node3 = this->astCtxt.bv(0x6c65746e, dst3.getBitSize());
4675  node4 = this->astCtxt.bv(0x49656e69, dst4.getBitSize());
4676  break;
4677  case 1:
4678  node1 = this->astCtxt.bv(0x000306a9, dst1.getBitSize());
4679  node2 = this->astCtxt.bv(0x02100800, dst2.getBitSize());
4680  node3 = this->astCtxt.bv(0x7fbae3ff, dst3.getBitSize());
4681  node4 = this->astCtxt.bv(0xbfebfbff, dst4.getBitSize());
4682  break;
4683  case 2:
4684  node1 = this->astCtxt.bv(0x76035a01, dst1.getBitSize());
4685  node2 = this->astCtxt.bv(0x00f0b2ff, dst2.getBitSize());
4686  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4687  node4 = this->astCtxt.bv(0x00ca0000, dst4.getBitSize());
4688  break;
4689  case 3:
4690  node1 = this->astCtxt.bv(0x00000000, dst1.getBitSize());
4691  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4692  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4693  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4694  break;
4695  case 4:
4696  node1 = this->astCtxt.bv(0x1c004121, dst1.getBitSize());
4697  node2 = this->astCtxt.bv(0x01c0003f, dst2.getBitSize());
4698  node3 = this->astCtxt.bv(0x0000003f, dst3.getBitSize());
4699  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4700  break;
4701  case 5:
4702  node1 = this->astCtxt.bv(0x00000040, dst1.getBitSize());
4703  node2 = this->astCtxt.bv(0x00000040, dst2.getBitSize());
4704  node3 = this->astCtxt.bv(0x00000003, dst3.getBitSize());
4705  node4 = this->astCtxt.bv(0x00021120, dst4.getBitSize());
4706  break;
4707  case 0x80000000:
4708  node1 = this->astCtxt.bv(0x80000008, dst1.getBitSize());
4709  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4710  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4711  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4712  break;
4713  case 0x80000001:
4714  node1 = this->astCtxt.bv(0x00000000, dst1.getBitSize());
4715  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4716  node3 = this->astCtxt.bv(0x00000001, dst3.getBitSize());
4717  node4 = this->astCtxt.bv(0x28100800, dst4.getBitSize());
4718  break;
4719  case 0x80000002:
4720  node1 = this->astCtxt.bv(0x20202020, dst1.getBitSize());
4721  node2 = this->astCtxt.bv(0x49202020, dst2.getBitSize());
4722  node3 = this->astCtxt.bv(0x6c65746e, dst3.getBitSize());
4723  node4 = this->astCtxt.bv(0x20295228, dst4.getBitSize());
4724  break;
4725  case 0x80000003:
4726  node1 = this->astCtxt.bv(0x65726f43, dst1.getBitSize());
4727  node2 = this->astCtxt.bv(0x294d5428, dst2.getBitSize());
4728  node3 = this->astCtxt.bv(0x2d376920, dst3.getBitSize());
4729  node4 = this->astCtxt.bv(0x30323533, dst4.getBitSize());
4730  break;
4731  case 0x80000004:
4732  node1 = this->astCtxt.bv(0x5043204d, dst1.getBitSize());
4733  node2 = this->astCtxt.bv(0x20402055, dst2.getBitSize());
4734  node3 = this->astCtxt.bv(0x30392e32, dst3.getBitSize());
4735  node4 = this->astCtxt.bv(0x007a4847, dst4.getBitSize());
4736  break;
4737  case 0x80000005:
4738  node1 = this->astCtxt.bv(0x00000000, dst1.getBitSize());
4739  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4740  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4741  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4742  break;
4743  case 0x80000006:
4744  node1 = this->astCtxt.bv(0x00000000, dst1.getBitSize());
4745  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4746  node3 = this->astCtxt.bv(0x01006040, dst3.getBitSize());
4747  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4748  break;
4749  case 0x80000007:
4750  node1 = this->astCtxt.bv(0x00000000, dst1.getBitSize());
4751  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4752  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4753  node4 = this->astCtxt.bv(0x00000100, dst4.getBitSize());
4754  break;
4755  case 0x80000008:
4756  node1 = this->astCtxt.bv(0x00003024, dst1.getBitSize());
4757  node2 = this->astCtxt.bv(0x00000000, dst2.getBitSize());
4758  node3 = this->astCtxt.bv(0x00000000, dst3.getBitSize());
4759  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4760  break;
4761  default:
4762  node1 = this->astCtxt.bv(0x00000007, dst1.getBitSize());
4763  node2 = this->astCtxt.bv(0x00000340, dst2.getBitSize());
4764  node3 = this->astCtxt.bv(0x00000340, dst3.getBitSize());
4765  node4 = this->astCtxt.bv(0x00000000, dst4.getBitSize());
4766  break;
4767  }
4768 
4769  /* Create symbolic expression */
4770  auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "CPUID AX operation");
4771  auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "CPUID BX operation");
4772  auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, dst3, "CPUID CX operation");
4773  auto expr4 = this->symbolicEngine->createSymbolicExpression(inst, node4, dst4, "CPUID DX operation");
4774 
4775  /* Spread taint */
4776  expr1->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_AX), false);
4777  expr2->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_BX), false);
4778  expr3->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_X86_CX), false);
4779  expr4->isTainted = this->taintEngine->setTaintRegister(this->architecture->