libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
riscvSemantics.cpp
Go to the documentation of this file.
1
2/*
3** Copyright (C) - Triton
4**
5** This program is under the terms of the Apache License 2.0.
6*/
7
8#include <triton/cpuSize.hpp>
9#include <triton/exceptions.hpp>
10#include <triton/riscvSemantics.hpp>
11#include <triton/riscvSpecifications.hpp>
12#include <triton/astContext.hpp>
13
14
15
126namespace triton {
127 namespace arch {
128 namespace riscv {
129
130 riscvSemantics::riscvSemantics(triton::arch::Architecture* architecture,
131 triton::engines::symbolic::SymbolicEngine* symbolicEngine,
132 triton::engines::taint::TaintEngine* taintEngine,
133 const triton::modes::SharedModes& modes,
134 const triton::ast::SharedAstContext& astCtxt) : modes(modes), astCtxt(astCtxt) {
135
136 this->architecture = architecture;
137 this->exception = triton::arch::NO_FAULT;
138 this->symbolicEngine = symbolicEngine;
139 this->taintEngine = taintEngine;
140
141 if (architecture == nullptr)
142 throw triton::exceptions::Semantics("riscvSemantics::riscvSemantics(): The architecture API must be defined.");
143
144 if (this->symbolicEngine == nullptr)
145 throw triton::exceptions::Semantics("riscvSemantics::riscvSemantics(): The symbolic engine API must be defined.");
146
147 if (this->taintEngine == nullptr)
148 throw triton::exceptions::Semantics("riscvSemantics::riscvSemantics(): The taint engines API must be defined.");
149 }
150
151
152 triton::arch::exception_e riscvSemantics::buildSemantics(triton::arch::Instruction& inst) {
153 this->exception = triton::arch::NO_FAULT;
154 switch (inst.getType()) {
155 case ID_INS_ADD: this->add_s(inst); break;
156 case ID_INS_ADDI: this->addi_s(inst); break;
157 case ID_INS_ADDIW: this->addiw_s(inst); break;
158 case ID_INS_ADDW: this->addw_s(inst); break;
159 case ID_INS_AND: this->and_s(inst); break;
160 case ID_INS_ANDI: this->and_s(inst); break;
161 case ID_INS_AUIPC: this->auipc_s(inst); break;
162 case ID_INS_BEQ: this->beq_s(inst); break;
163 case ID_INS_BGE: this->bge_s(inst); break;
164 case ID_INS_BGEU: this->bgeu_s(inst); break;
165 case ID_INS_BLT: this->blt_s(inst); break;
166 case ID_INS_BLTU: this->bltu_s(inst); break;
167 case ID_INS_BNE: this->bne_s(inst); break;
168 /* Compressed instructions */
169 case ID_INS_C_ADD: this->c_add_s(inst); break;
170 case ID_INS_C_ADDI: this->c_add_s(inst); break;
171 case ID_INS_C_ADDI16SP: this->c_addi16sp_s(inst); break;
172 case ID_INS_C_ADDI4SPN: this->c_addi4spn_s(inst); break;
173 case ID_INS_C_ADDIW: this->c_addw_s(inst); break;
174 case ID_INS_C_ADDW: this->c_addw_s(inst); break;
175 case ID_INS_C_AND: this->c_and_s(inst); break;
176 case ID_INS_C_ANDI: this->c_and_s(inst); break;
177 case ID_INS_C_BEQZ: this->c_beqz_s(inst); break;
178 case ID_INS_C_BNEZ: this->c_bnez_s(inst); break;
179 case ID_INS_C_J: this->jal_j_s(inst); break;
180 case ID_INS_C_JAL: this->c_jal_s(inst); break;
181 case ID_INS_C_JALR: this->c_jalr_s(inst); break;
182 case ID_INS_C_JR: this->jalr_no_link_s(inst); break;
183 case ID_INS_C_LD: this->c_ld_s(inst); break;
184 case ID_INS_C_LDSP: this->c_ldsp_s(inst); break;
185 case ID_INS_C_LI: this->c_li_s(inst); break;
186 case ID_INS_C_LW: this->c_lw_s(inst); break;
187 case ID_INS_C_LWSP: this->c_lwsp_s(inst); break;
188 case ID_INS_C_LUI: this->lui_s(inst); break;
189 case ID_INS_C_MV: this->c_mv_s(inst); break;
190 case ID_INS_C_NOP: this->c_nop_s(inst); break;
191 case ID_INS_C_OR: this->c_or_s(inst); break;
192 case ID_INS_C_SD: this->c_sd_s(inst); break;
193 case ID_INS_C_SDSP: this->c_sdsp_s(inst); break;
194 case ID_INS_C_SLLI: this->c_slli_s(inst); break;
195 case ID_INS_C_SRAI: this->c_srai_s(inst); break;
196 case ID_INS_C_SRLI: this->c_srli_s(inst); break;
197 case ID_INS_C_SUB: this->c_sub_s(inst); break;
198 case ID_INS_C_SUBW: this->c_subw_s(inst); break;
199 case ID_INS_C_SW: this->c_sw_s(inst); break;
200 case ID_INS_C_SWSP: this->c_swsp_s(inst); break;
201 case ID_INS_C_XOR: this->c_xor_s(inst); break;
202 /* End of compressed instructions */
203 case ID_INS_DIV: this->div_s(inst); break;
204 case ID_INS_DIVU: this->divu_s(inst); break;
205 case ID_INS_DIVUW: this->divuw_s(inst); break;
206 case ID_INS_DIVW: this->divw_s(inst); break;
207 case ID_INS_JAL: this->jal_s(inst); break;
208 case ID_INS_JALR: this->jalr_s(inst); break;
209 case ID_INS_LB: this->lb_s(inst); break;
210 case ID_INS_LBU: this->lbu_s(inst); break;
211 case ID_INS_LD: this->ld_s(inst); break;
212 case ID_INS_LH: this->lh_s(inst); break;
213 case ID_INS_LHU: this->lhu_s(inst); break;
214 case ID_INS_LUI: this->lui_s(inst); break;
215 case ID_INS_LW: this->lw_s(inst); break;
216 case ID_INS_LWU: this->lwu_s(inst); break;
217 case ID_INS_MUL: this->mul_s(inst); break;
218 case ID_INS_MULH: this->mulh_s(inst); break;
219 case ID_INS_MULHSU: this->mulhsu_s(inst); break;
220 case ID_INS_MULHU: this->mulhu_s(inst); break;
221 case ID_INS_MULW: this->mulw_s(inst); break;
222 case ID_INS_OR: this->or_s(inst); break;
223 case ID_INS_ORI: this->or_s(inst); break;
224 case ID_INS_REM: this->rem_s(inst); break;
225 case ID_INS_REMU: this->remu_s(inst); break;
226 case ID_INS_REMUW: this->remuw_s(inst); break;
227 case ID_INS_REMW: this->remw_s(inst); break;
228 case ID_INS_SB: this->sb_s(inst); break;
229 case ID_INS_SD: this->sd_s(inst); break;
230 case ID_INS_SH: this->sh_s(inst); break;
231 case ID_INS_SLL: this->sll_s(inst); break;
232 case ID_INS_SLLI: this->sll_s(inst); break;
233 case ID_INS_SLLIW: this->sllw_s(inst); break;
234 case ID_INS_SLLW: this->sllw_s(inst); break;
235 case ID_INS_SLT: this->slt_s(inst); break;
236 case ID_INS_SLTI: this->slt_s(inst); break;
237 case ID_INS_SLTIU: this->sltu_s(inst); break;
238 case ID_INS_SLTU: this->sltu_s(inst); break;
239 case ID_INS_SRA: this->sra_s(inst); break;
240 case ID_INS_SRAI: this->sra_s(inst); break;
241 case ID_INS_SRAIW: this->sraw_s(inst); break;
242 case ID_INS_SRAW: this->sraw_s(inst); break;
243 case ID_INS_SRL: this->srl_s(inst); break;
244 case ID_INS_SRLI: this->srl_s(inst); break;
245 case ID_INS_SRLIW: this->srlw_s(inst); break;
246 case ID_INS_SRLW: this->srlw_s(inst); break;
247 case ID_INS_SUB: this->sub_s(inst); break;
248 case ID_INS_SUBW: this->subw_s(inst); break;
249 case ID_INS_SW: this->sw_s(inst); break;
250 case ID_INS_XOR: this->xor_s(inst); break;
251 case ID_INS_XORI: this->xori_s(inst); break;
252
253 default:
254 this->exception = triton::arch::FAULT_UD;
255 break;
256 }
257 return this->exception;
258 }
259
260
261 void riscvSemantics::controlFlow_s(triton::arch::Instruction& inst) {
262 auto pc = this->architecture->getProgramCounter();
263 auto pc_op = triton::arch::OperandWrapper(pc);
264
265 /* Create the semantics */
266 auto node = this->astCtxt->bv(inst.getNextAddress(), pc_op.getBitSize());
267
268 /* Create symbolic expression */
269 auto expr = this->symbolicEngine->createSymbolicRegisterExpression(inst, node, pc, "Program Counter");
270
271 /* Spread taint */
272 expr->isTainted = this->taintEngine->setTaintRegister(pc, triton::engines::taint::UNTAINTED);
273 }
274
275
276 void riscvSemantics::add_s(triton::arch::Instruction& inst) {
277 auto& dst = inst.operands[0];
278 auto& src1 = inst.operands[1];
279 auto& src2 = inst.operands[2];
280
281 /* Create symbolic operands */
282 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
283 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
284
285 /* Create the semantics */
286 auto node = this->astCtxt->bvadd(op1, op2);
287
288 /* Create symbolic expression */
289 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD(I) operation");
290
291 /* Spread taint */
292 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
293
294 /* Update the symbolic control flow */
295 this->controlFlow_s(inst);
296 }
297
298
299 void riscvSemantics::addi_s(triton::arch::Instruction& inst) {
300 /* Check for possible pseudo instructions
301 mv rd, rs -- [addi rd, rs, 0] -- Copy register
302 nop -- [addi x0, x0, 0] -- No operation
303 */
304 switch (inst.operands.size()) {
305 case 0: this->controlFlow_s(inst); return; // nop
306 case 2: addi_mv_s(inst); return; // mv
307 default: add_s(inst); return; // addi
308 }
309 }
310
311
312 void riscvSemantics::addi_mv_s(triton::arch::Instruction& inst) {
313 auto& dst = inst.operands[0];
314 auto& src = inst.operands[1];
315
316 /* Create the semantics */
317 auto node = this->symbolicEngine->getOperandAst(inst, src);
318
319 /* Create symbolic expression */
320 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MV operation");
321
322 /* Spread taint */
323 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
324
325 /* Update the symbolic control flow */
326 this->controlFlow_s(inst);
327 }
328
329
330 void riscvSemantics::addiw_s(triton::arch::Instruction& inst) { /* 64-bit only */
331 auto& dst = inst.operands[0];
332 auto& src1 = inst.operands[1];
333 auto size = dst.getBitSize();
334
335 /* Create symbolic operands */
336 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
337 auto node = this->astCtxt->sx(32, this->astCtxt->extract(31, 0, op1)); // sext.w pseudo instruction semantics
338 if (inst.operands.size() > 2) {
339 auto& src2 = inst.operands[2];
340 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
341 node = this->astCtxt->sx(32, this->astCtxt->extract(31, 0, this->astCtxt->bvadd(op1, op2)));
342 }
343
344 /* Create symbolic expression */
345 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADDIW operation");
346
347 /* Spread taint */
348 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1));
349
350 /* Update the symbolic control flow */
351 this->controlFlow_s(inst);
352 }
353
354
355 void riscvSemantics::addw_s(triton::arch::Instruction& inst) { /* 64-bit only */
356 auto& dst = inst.operands[0];
357 auto& src1 = inst.operands[1];
358 auto& src2 = inst.operands[2];
359
360 /* Create symbolic operands */
361 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
362 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
363
364 /* Create the semantics */
365 auto node = this->astCtxt->sx(32, this->astCtxt->bvadd(
366 this->astCtxt->extract(31, 0, op1),
367 this->astCtxt->extract(31, 0, op2)
368 ));
369
370 /* Create symbolic expression */
371 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADDW operation");
372
373 /* Spread taint */
374 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
375
376 /* Update the symbolic control flow */
377 this->controlFlow_s(inst);
378 }
379
380
381 void riscvSemantics::and_s(triton::arch::Instruction& inst) {
382 auto& dst = inst.operands[0];
383 auto& src1 = inst.operands[1];
384 auto& src2 = inst.operands[2];
385
386 /* Create symbolic operands */
387 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
388 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
389
390 /* Create the semantics */
391 auto node = this->astCtxt->bvand(op1, op2);
392
393 /* Create symbolic expression */
394 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND(I) operation");
395
396 /* Spread taint */
397 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
398
399 /* Update the symbolic control flow */
400 this->controlFlow_s(inst);
401 }
402
403
404 void riscvSemantics::auipc_s(triton::arch::Instruction& inst) {
405 // dst := pc + sx_64(src_imm(_20) << 12)
406 auto& dst = inst.operands[0];
407 auto& src = inst.operands[1];
408 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
409
410 /* Create symbolic operands */
411 auto imm = this->symbolicEngine->getOperandAst(inst, src);
412 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
413
414 /* Create the semantics */
415 auto node = this->astCtxt->concat(this->astCtxt->extract(19, 0, imm), this->astCtxt->bv(0, 12));
416 if (dst.getBitSize() == 64) {
417 node = this->astCtxt->sx(32, node);
418 }
419 node = this->astCtxt->bvadd(node, pc_ast);
420
421 /* Create symbolic expression */
422 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AUIPC operation");
423
424 /* Spread taint */
425 expr->isTainted = this->taintEngine->isTainted(pc);
426
427 /* Update the symbolic control flow */
428 this->controlFlow_s(inst);
429 }
430
431
432 void riscvSemantics::beq_s(triton::arch::Instruction& inst) {
433 /* Check for possible pseudo instructions
434 beqz rs, offset -- [beq rs, x0, offset] -- Branch if == zero
435 */
436 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
437 auto& src1 = inst.operands[0];
438 auto& src2 = inst.operands[1];
439 auto size = src1.getBitSize();
440
441 /* Create symbolic operands */
442 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
443 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
444 auto op2 = this->astCtxt->bv(0, size);
445 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
446
447 if (inst.operands.size() == 3) {
448 auto& imm = inst.operands[2];
449 op2 = op3;
450 op3 = this->symbolicEngine->getOperandAst(inst, imm);
451 }
452
453 /* Create the semantics */
454 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, op2),
455 this->astCtxt->bvadd(pc_ast, op3),
456 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
457 );
458
459 /* Create symbolic expression */
460 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
461
462 /* Set condition flag */
463 if (op1->evaluate() == op2->evaluate())
464 inst.setConditionTaken(true);
465
466 /* Spread taint */
467 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
468 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
469
470 /* Create the path constraint */
471 this->symbolicEngine->pushPathConstraint(inst, expr);
472 }
473
474
475 void riscvSemantics::bge_s(triton::arch::Instruction& inst) {
476 /* Check for possible pseudo instructions (no ble in capstone)
477 blez rs, offset -- [bge x0, rs, offset] -- Branch if <= zero
478 bgez rs, offset -- [bge rs, x0, offset] -- Branch if >= zero
479 */
480 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
481 auto& src1 = inst.operands[0];
482 auto& src2 = inst.operands[1];
483 auto size = src1.getBitSize();
484
485 /* Create symbolic operands */
486 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
487 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
488 auto op2 = this->astCtxt->bv(0, size);
489 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
490
491 /* Create branch condition AST */
492 bool taken = false;
493 auto node = this->astCtxt->bvsge(op1, op2); // bgez
494 if (inst.operands.size() < 3) {
495 auto mnem = inst.getDisassembly();
496 if (mnem[1] == 'l') { // blez
497 node = this->astCtxt->bvsle(op1, op2);
498 taken = (long long)(op1->evaluate()) <= 0;
499 }
500 else {
501 taken = (long long)(op1->evaluate()) >= 0;
502 }
503 }
504 else { // bge
505 auto& imm = inst.operands[2];
506 op2 = op3;
507 op3 = this->symbolicEngine->getOperandAst(inst, imm);
508 node = this->astCtxt->bvsge(op1, op2);
509 taken = (long long)(op1->evaluate() - op2->evaluate()) >= 0;
510 }
511
512 /* Create the semantics */
513 node = this->astCtxt->ite(node,
514 this->astCtxt->bvadd(pc_ast, op3),
515 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
516 );
517
518 /* Create symbolic expression */
519 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
520
521 /* Set condition flag */
522 inst.setConditionTaken(taken);
523
524 /* Spread taint */
525 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
526 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
527
528 /* Create the path constraint */
529 this->symbolicEngine->pushPathConstraint(inst, expr);
530 }
531
532
533 void riscvSemantics::bgeu_s(triton::arch::Instruction& inst) {
534 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
535 auto& src1 = inst.operands[0];
536 auto& src2 = inst.operands[1];
537 auto& imm = inst.operands[2];
538
539 /* Create symbolic operands */
540 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
541 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
542 auto op3 = this->symbolicEngine->getOperandAst(inst, imm);
543 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
544
545 /* Create the semantics */
546 auto node = this->astCtxt->ite(this->astCtxt->bvuge(op1, op2),
547 this->astCtxt->bvadd(pc_ast, op3),
548 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
549 );
550
551 /* Create symbolic expression */
552 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
553
554 /* Set condition flag */
555 if (op1->evaluate() >= op2->evaluate())
556 inst.setConditionTaken(true);
557
558 /* Spread taint */
559 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
560 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
561
562 /* Create the path constraint */
563 this->symbolicEngine->pushPathConstraint(inst, expr);
564 }
565
566
567 void riscvSemantics::blt_s(triton::arch::Instruction& inst) {
568 /* Check for possible pseudo instructions (no bgt in capstone)
569 bltz rs, offset -- [blt rs, x0, offset] -- Branch if < zero
570 bgtz rs, offset -- [blt x0, rs, offset] -- Branch if > zero
571 */
572 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
573 auto& src1 = inst.operands[0];
574 auto& src2 = inst.operands[1];
575 auto size = src1.getBitSize();
576
577 /* Create symbolic operands */
578 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
579 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
580 auto op2 = this->astCtxt->bv(0, size);
581 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
582
583 /* Create branch condition AST */
584 bool taken = false;
585 auto node = this->astCtxt->bvslt(op1, op2); // bltz
586 if (inst.operands.size() < 3) {
587 auto mnem = inst.getDisassembly();
588 if (mnem[1] == 'g') { // bgtz
589 node = this->astCtxt->bvsgt(op1, op2);
590 taken = (long long)(op1->evaluate()) > 0;
591 }
592 else {
593 taken = (long long)(op1->evaluate()) < 0;
594 }
595 }
596 else { // blt
597 auto& imm = inst.operands[2];
598 op2 = op3;
599 op3 = this->symbolicEngine->getOperandAst(inst, imm);
600 node = this->astCtxt->bvslt(op1, op2);
601 taken = (long long)(op1->evaluate() - op2->evaluate()) < 0;
602 }
603
604 /* Create the semantics */
605 node = this->astCtxt->ite(node,
606 this->astCtxt->bvadd(pc_ast, op3),
607 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
608 );
609
610 /* Create symbolic expression */
611 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
612
613 /* Set condition flag */
614 inst.setConditionTaken(taken);
615
616 /* Spread taint */
617
618 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
619 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
620
621 /* Create the path constraint */
622 this->symbolicEngine->pushPathConstraint(inst, expr);
623 }
624
625
626 void riscvSemantics::bltu_s(triton::arch::Instruction& inst) {
627 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
628 auto& src1 = inst.operands[0];
629 auto& src2 = inst.operands[1];
630 auto& imm = inst.operands[2];
631
632 /* Create symbolic operands */
633 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
634 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
635 auto op3 = this->symbolicEngine->getOperandAst(inst, imm);
636 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
637
638 /* Create the semantics */
639 auto node = this->astCtxt->ite(this->astCtxt->bvult(op1, op2),
640 this->astCtxt->bvadd(pc_ast, op3),
641 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
642 );
643
644 /* Create symbolic expression */
645 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
646
647 /* Set condition flag */
648 if (op2->evaluate() > op1->evaluate())
649 inst.setConditionTaken(true);
650
651 /* Spread taint */
652 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
653 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
654
655 /* Create the path constraint */
656 this->symbolicEngine->pushPathConstraint(inst, expr);
657 }
658
659
660 void riscvSemantics::bne_s(triton::arch::Instruction& inst) {
661 /* Check for possible pseudo instructions
662 bnez rs, offset -- [blt rs, x0, offset] -- Branch if != zero
663 */
664 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
665 auto& src1 = inst.operands[0];
666 auto& src2 = inst.operands[1];
667 auto size = src1.getBitSize();
668
669 /* Create symbolic operands */
670 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
671 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
672 auto op2 = this->astCtxt->bv(0, size);
673 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
674
675 if (inst.operands.size() == 3) {
676 auto& imm = inst.operands[2];
677 op2 = op3;
678 op3 = this->symbolicEngine->getOperandAst(inst, imm);
679 }
680
681 /* Create the semantics */
682 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, op2),
683 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize()),
684 this->astCtxt->bvadd(pc_ast, op3)
685 );
686
687 /* Create symbolic expression */
688 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
689
690 /* Set condition flag */
691 if (op1->evaluate() - op2->evaluate())
692 inst.setConditionTaken(true);
693
694 /* Spread taint */
695 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
696 expr->isTainted = this->taintEngine->taintUnion(pc, src2);
697
698 /* Create the path constraint */
699 this->symbolicEngine->pushPathConstraint(inst, expr);
700 }
701
702
703 // Compressed instructions:
704 void riscvSemantics::c_add_s(triton::arch::Instruction& inst) {
705 auto& dst = inst.operands[0];
706 auto& src = inst.operands[1];
707
708 /* Create symbolic operands */
709 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
710 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
711
712 /* Create the semantics */
713 auto node = this->astCtxt->bvadd(op1, op2);
714
715 /* Create symbolic expression */
716 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.ADD(I) operation");
717
718 /* Spread taint */
719 expr->isTainted = this->taintEngine->taintUnion(dst, src);
720
721 /* Update the symbolic control flow */
722 this->controlFlow_s(inst);
723 }
724
725
726 void riscvSemantics::c_addi16sp_s(triton::arch::Instruction& inst) {
727 auto& sp = inst.operands[0];
728 auto& imm = inst.operands[1];
729
730 /* Create symbolic operands */
731 auto op1 = this->symbolicEngine->getOperandAst(inst, sp);
732 auto op2 = this->symbolicEngine->getOperandAst(inst, imm);
733
734 /* Create the semantics */
735 auto node = this->astCtxt->bvadd(op1, op2);
736
737 /* Create symbolic expression */
738 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, sp, "C.ADDI16SP operation");
739
740 /* Spread taint */
741 expr->isTainted = this->taintEngine->isTainted(sp);
742
743 /* Update the symbolic control flow */
744 this->controlFlow_s(inst);
745 }
746
747
748 void riscvSemantics::c_addi4spn_s(triton::arch::Instruction& inst) {
749 auto& dst = inst.operands[0];
750 auto& src = inst.operands[1];
751 auto& imm = inst.operands[2];
752
753 /* Create symbolic operands */
754 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
755 auto op2 = this->symbolicEngine->getOperandAst(inst, imm);
756
757 /* Create the semantics */
758 auto node = this->astCtxt->bvadd(op1, op2);
759
760 /* Create symbolic expression */
761 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.ADDI4SPN operation");
762
763 /* Spread taint */
764 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src));
765
766 /* Update the symbolic control flow */
767 this->controlFlow_s(inst);
768 }
769
770
771 void riscvSemantics::c_addw_s(triton::arch::Instruction& inst) { /* 64-bit only */
772 auto& dst = inst.operands[0];
773 auto& src = inst.operands[1];
774
775 /* Create symbolic operands */
776 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
777 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
778
779 /* Create the semantics */
780 auto node = this->astCtxt->sx(32, this->astCtxt->bvadd(
781 this->astCtxt->extract(31, 0, op1),
782 this->astCtxt->extract(31, 0, op2)
783 ));
784
785 /* Create symbolic expression */
786 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.ADD(I)W operation");
787
788 /* Spread taint */
789 expr->isTainted = this->taintEngine->taintUnion(dst, src);
790
791 /* Update the symbolic control flow */
792 this->controlFlow_s(inst);
793 }
794
795
796 void riscvSemantics::c_and_s(triton::arch::Instruction& inst) {
797 auto& dst = inst.operands[0];
798 auto& src = inst.operands[1];
799
800 /* Create symbolic operands */
801 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
802 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
803
804 /* Create the semantics */
805 auto node = this->astCtxt->bvand(op1, op2);
806
807 /* Create symbolic expression */
808 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.AND(I) operation");
809
810 /* Spread taint */
811 expr->isTainted = this->taintEngine->taintUnion(dst, src);
812
813 /* Update the symbolic control flow */
814 this->controlFlow_s(inst);
815 }
816
817
818 void riscvSemantics::c_beqz_s(triton::arch::Instruction& inst) {
819 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
820 auto& src1 = inst.operands[0];
821 auto& src2 = inst.operands[1];
822 auto size = src1.getBitSize();
823
824 /* Create symbolic operands */
825 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
826 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
827 auto op2 = this->astCtxt->bv(0, size);
828 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
829
830 /* Create the semantics */
831 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, op2),
832 this->astCtxt->bvadd(pc_ast, op3),
833 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize())
834 );
835
836 /* Create symbolic expression */
837 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
838
839 /* Set condition flag */
840 if (op1->evaluate() == 0)
841 inst.setConditionTaken(true);
842
843 /* Spread taint */
844 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
845
846 /* Create the path constraint */
847 this->symbolicEngine->pushPathConstraint(inst, expr);
848 }
849
850
851 void riscvSemantics::c_bnez_s(triton::arch::Instruction& inst) {
852 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
853 auto& src1 = inst.operands[0];
854 auto& src2 = inst.operands[1];
855 auto size = src1.getBitSize();
856
857 /* Create symbolic operands */
858 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
859 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
860 auto op2 = this->astCtxt->bv(0, size);
861 auto op3 = this->symbolicEngine->getOperandAst(inst, src2);
862
863 /* Create the semantics */
864 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, op2),
865 this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize()),
866 this->astCtxt->bvadd(pc_ast, op3)
867 );
868
869 /* Create symbolic expression */
870 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
871
872 /* Set condition flag */
873 if (op1->evaluate() != 0)
874 inst.setConditionTaken(true);
875
876 /* Spread taint */
877 expr->isTainted = this->taintEngine->taintUnion(pc, src1);
878
879 /* Create the path constraint */
880 this->symbolicEngine->pushPathConstraint(inst, expr);
881 }
882
883
884 void riscvSemantics::c_jal_s(triton::arch::Instruction& inst) { /* 32-bit only */
885 /* x1 := pc + 2; pc := pc + offset
886 Compressed instruction expands to:
887 jal offset -- [jal x1, offset] -- Jump and link
888 */
889 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
890 auto size = pc.getBitSize();
891 auto& src = inst.operands[0];
892 auto ra = this->architecture->getRegister(triton::arch::ID_REG_RV32_X1);
893 auto reg = triton::arch::OperandWrapper(ra);
894
895 /* Create symbolic operands */
896 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
897 auto imm = this->symbolicEngine->getOperandAst(inst, src);
898
899 /* Create the semantics */
900 auto node = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
901 auto node_pc = this->astCtxt->bvadd(pc_ast, imm);
902
903 /* Create symbolic expression */
904 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, reg, "C.JAL operation ra (x1)");
905 auto expr_pc = this->symbolicEngine->createSymbolicExpression(inst, node_pc, pc, "Program Counter");
906
907 /* Spread taint */
908 expr->isTainted = this->taintEngine->isTainted(pc);
909 expr_pc->isTainted = this->taintEngine->isTainted(pc);
910
911 /* Create the path constraint */
912 this->symbolicEngine->pushPathConstraint(inst, expr_pc);
913 }
914
915
916 void riscvSemantics::c_jalr_s(triton::arch::Instruction& inst) {
917 /* x1 := pc + 2; pc := (x[rs] + imm) & ~1
918 Compressed instruction expands to:
919 jalr rs -- [jalr x1, rs, 0] -- Jump and link register
920 */
921 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
922 auto size = pc.getBitSize();
923 auto& src = inst.operands[0];
924 auto ra = this->architecture->getRegister(
925 size == 64 ?
926 triton::arch::ID_REG_RV64_X1 :
927 triton::arch::ID_REG_RV32_X1
928 );
929 auto dst = triton::arch::OperandWrapper(ra);
930
931 /* Create symbolic operands */
932 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
933 auto op_src = this->symbolicEngine->getOperandAst(inst, src);
934
935 /* Create the semantics */
936 auto node_dst = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
937 auto node_pc = this->astCtxt->bvand( /* ignore last bit */
938 op_src,
939 this->astCtxt->bvshl(this->astCtxt->bv(-1, size), this->astCtxt->bv(1, size))
940 );
941
942 /* Create symbolic expression */
943 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node_dst, dst, "C.JALR operation ra (x1)");
944 auto expr_pc = this->symbolicEngine->createSymbolicExpression(inst, node_pc, pc, "Program Counter");
945
946 /* Spread taint */
947 expr->isTainted = this->taintEngine->isTainted(pc);
948 expr_pc->isTainted = this->taintEngine->setTaint(pc, this->taintEngine->isTainted(src));
949
950 /* Create the path constraint */
951 this->symbolicEngine->pushPathConstraint(inst, expr_pc);
952 }
953
954
955 void riscvSemantics::c_ld_s(triton::arch::Instruction& inst) { /* 64-bit only */
956 // x[rd] := M[sp + offset][63:0]
957 auto& dst = inst.operands[0]; // rd
958 auto& src1 = inst.operands[1]; // offset - disp
959 auto& src2 = inst.operands[2]; // rs1 - base
960
961 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
962 /* Construct double word memory access manually with base and displacement */
963 triton::arch::MemoryAccess mem;
964 mem.setBits(triton::bitsize::qword - 1, 0);
965 triton::arch::Immediate& disp = src1.getImmediate();
966 triton::arch::Register& base = src2.getRegister();
967 mem.setBaseRegister(base);
968 mem.setDisplacement(disp);
969 auto mem_op = triton::arch::OperandWrapper(mem);
970 this->symbolicEngine->initLeaAst(mem_op.getMemory());
971
972 /* Create the semantics */
973 auto node = this->symbolicEngine->getOperandAst(inst, mem_op);
974
975 /* Create symbolic expression */
976 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.LD operation - LOAD access");
977
978 /* Spread taint */
979 expr->isTainted = this->taintEngine->taintAssignment(dst, mem_op);
980
981 /* Update the symbolic control flow */
982 this->controlFlow_s(inst);
983 }
984
985
986 void riscvSemantics::c_ldsp_s(triton::arch::Instruction& inst) { /* 64-bit only */
987 // x[rd] := M[sp + offset][63:0]
988 auto& dst = inst.operands[0]; // rd
989 auto& src1 = inst.operands[1]; // offset - disp; (sp - base)
990
991 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
992 /* Construct double word memory access manually with base and displacement */
993 triton::arch::MemoryAccess mem;
994 mem.setBits(triton::bitsize::qword - 1, 0);
995 triton::arch::Immediate& disp = src1.getImmediate();
996 auto sp = this->architecture->getStackPointer();
997 mem.setBaseRegister(sp);
998 mem.setDisplacement(disp);
999 auto mem_op = triton::arch::OperandWrapper(mem);
1000 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1001
1002 /* Create the semantics */
1003 auto node = this->symbolicEngine->getOperandAst(inst, mem_op);
1004
1005 /* Create symbolic expression */
1006 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.LDSP operation - LOAD access");
1007
1008 /* Spread taint */
1009 expr->isTainted = this->taintEngine->taintAssignment(dst, mem_op);
1010
1011 /* Update the symbolic control flow */
1012 this->controlFlow_s(inst);
1013 }
1014
1015
1016 void riscvSemantics::c_li_s(triton::arch::Instruction& inst) {
1017 auto& dst = inst.operands[0];
1018 auto& src = inst.operands[1];
1019
1020 /* Create the semantics */
1021 auto node = this->symbolicEngine->getOperandAst(inst, src);
1022
1023 /* Create symbolic expression */
1024 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.LI operation");
1025
1026 /* Spread taint */
1027 expr->isTainted = this->taintEngine->setTaint(dst, false);
1028
1029 /* Update the symbolic control flow */
1030 this->controlFlow_s(inst);
1031 }
1032
1033
1034 void riscvSemantics::c_lw_s(triton::arch::Instruction& inst) {
1035 // x[rd] := M[x[rs] + offset][31:0]
1036 auto& dst = inst.operands[0]; // rd
1037 auto& src1 = inst.operands[1]; // offset - disp
1038 auto& src2 = inst.operands[2]; // rs1 - base
1039
1040 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1041 /* Construct word memory access manually with base and displacement */
1042 triton::arch::MemoryAccess mem;
1043 mem.setBits(triton::bitsize::dword - 1, 0);
1044 triton::arch::Immediate& disp = src1.getImmediate();
1045 triton::arch::Register& base = src2.getRegister();
1046 mem.setBaseRegister(base);
1047 mem.setDisplacement(disp);
1048 auto mem_op = triton::arch::OperandWrapper(mem);
1049 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1050
1051 /* Create the semantics */
1052 auto node = this->symbolicEngine->getOperandAst(inst, mem_op);
1053 if (dst.getBitSize() == 64) { /* extend to register size */
1054 node = this->astCtxt->sx(32, node);
1055 }
1056
1057 /* Create symbolic expression */
1058 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.LW operation - LOAD access");
1059
1060 /* Spread taint */
1061 expr->isTainted = this->taintEngine->taintAssignment(dst, mem_op);
1062
1063 /* Update the symbolic control flow */
1064 this->controlFlow_s(inst);
1065 }
1066
1067
1068 void riscvSemantics::c_lwsp_s(triton::arch::Instruction& inst) {
1069 // x[rd] := M[sp + offset][31:0]
1070 auto& dst = inst.operands[0]; // rd
1071 auto& src = inst.operands[1]; // offset - disp; (sp - base)
1072
1073 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1074 /* Construct word memory access manually with base and displacement */
1075 triton::arch::MemoryAccess mem;
1076 mem.setBits(triton::bitsize::dword - 1, 0);
1077 triton::arch::Immediate& disp = src.getImmediate();
1078 auto sp = this->architecture->getStackPointer();
1079 mem.setBaseRegister(sp);
1080 mem.setDisplacement(disp);
1081 auto mem_op = triton::arch::OperandWrapper(mem);
1082 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1083
1084 /* Create the semantics */
1085 auto node = this->symbolicEngine->getOperandAst(inst, mem_op);
1086 if (dst.getBitSize() == 64) { /* extend to register size */
1087 node = this->astCtxt->sx(32, node);
1088 }
1089
1090 /* Create symbolic expression */
1091 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.LWSP operation - LOAD access");
1092
1093 /* Spread taint */
1094 expr->isTainted = this->taintEngine->taintAssignment(dst, mem_op);
1095
1096 /* Update the symbolic control flow */
1097 this->controlFlow_s(inst);
1098 }
1099
1100
1101 void riscvSemantics::c_mv_s(triton::arch::Instruction& inst) {
1102 auto& dst = inst.operands[0];
1103 auto& src = inst.operands[1];
1104
1105 /* Create the semantics */
1106 auto node = this->symbolicEngine->getOperandAst(inst, src);
1107
1108 /* Create symbolic expression */
1109 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.MV operation");
1110
1111 /* Spread taint */
1112 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1113
1114 /* Update the symbolic control flow */
1115 this->controlFlow_s(inst);
1116 }
1117
1118
1119 void riscvSemantics::c_nop_s(triton::arch::Instruction& inst) {
1120 /* Update the symbolic control flow */
1121 this->controlFlow_s(inst);
1122 }
1123
1124
1125 void riscvSemantics::c_or_s(triton::arch::Instruction& inst) {
1126 auto& dst = inst.operands[0];
1127 auto& src = inst.operands[1];
1128
1129 /* Create symbolic operands */
1130 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1131 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
1132
1133 /* Create the semantics */
1134 auto node = this->astCtxt->bvor(op1, op2);
1135
1136 /* Create symbolic expression */
1137 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.OR operation");
1138
1139 /* Spread taint */
1140 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src));
1141
1142 /* Update the symbolic control flow */
1143 this->controlFlow_s(inst);
1144 }
1145
1146
1147 void riscvSemantics::c_sd_s(triton::arch::Instruction& inst) { /* 64-bit only */
1148 // M[x[rs1] + offset] := x[rs2]
1149 auto& src = inst.operands[0]; // rs2
1150 auto& imm = inst.operands[1]; // offset - disp
1151 auto& dst = inst.operands[2]; // rs1 - base
1152
1153 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1154 /* Construct double word memory access manually with base and displacement */
1155 triton::arch::MemoryAccess mem;
1156 mem.setBits(triton::bitsize::qword - 1, 0);
1157 triton::arch::Immediate& disp = imm.getImmediate();
1158 triton::arch::Register& base = dst.getRegister();
1159 mem.setBaseRegister(base);
1160 mem.setDisplacement(disp);
1161 auto mem_op = triton::arch::OperandWrapper(mem);
1162 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1163
1164 /* Create the semantics */
1165 auto node = this->symbolicEngine->getOperandAst(inst, src);
1166
1167 /* Create symbolic expression */
1168 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, mem_op, "C.SD operation - STORE access");
1169
1170 /* Spread taint */
1171 expr->isTainted = this->taintEngine->taintAssignment(mem_op, src);
1172
1173 /* Update the symbolic control flow */
1174 this->controlFlow_s(inst);
1175 }
1176
1177
1178 void riscvSemantics::c_sdsp_s(triton::arch::Instruction& inst) { /* 64-bit only */
1179 // M[sp + offset] := x[rs]
1180 auto& src = inst.operands[0]; // rs
1181 auto& imm = inst.operands[1]; // offset - disp; (sp - base)
1182
1183 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1184 /* Construct double word memory access manually with base and displacement */
1185 triton::arch::MemoryAccess mem;
1186 mem.setBits(triton::bitsize::qword - 1, 0);
1187 triton::arch::Immediate& disp = imm.getImmediate();
1188 auto sp = this->architecture->getStackPointer();
1189 mem.setBaseRegister(sp);
1190 mem.setDisplacement(disp);
1191 auto mem_op = triton::arch::OperandWrapper(mem);
1192 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1193
1194 /* Create the semantics */
1195 auto node = this->symbolicEngine->getOperandAst(inst, src);
1196
1197 /* Create symbolic expression */
1198 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, mem_op, "C.SDSP operation - STORE access");
1199
1200 /* Spread taint */
1201 expr->isTainted = this->taintEngine->taintAssignment(mem_op, src);
1202
1203 /* Update the symbolic control flow */
1204 this->controlFlow_s(inst);
1205 }
1206
1207
1208 void riscvSemantics::c_slli_s(triton::arch::Instruction& inst) {
1209 auto& dst = inst.operands[0];
1210 auto& src = inst.operands[1];
1211 auto size = src.getBitSize();
1212
1213 /* Create symbolic operands */
1214 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1215 auto op2 = this->astCtxt->bvand(
1216 this->symbolicEngine->getOperandAst(inst, src),
1217 dst.getBitSize() == 64 ? this->astCtxt->bv(0x3f, size) : this->astCtxt->bv(0x1f, size)
1218 );
1219
1220 /* Create the semantics */
1221 auto node = this->astCtxt->bvshl(op1, op2);
1222
1223 /* Create symbolic expression */
1224 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.SLLI operation");
1225
1226 /* Spread taint */
1227 expr->isTainted = this->taintEngine->taintUnion(dst, src);
1228
1229 /* Update the symbolic control flow */
1230 this->controlFlow_s(inst);
1231 }
1232
1233
1234 void riscvSemantics::c_srai_s(triton::arch::Instruction& inst) {
1235 auto& dst = inst.operands[0];
1236 auto& src = inst.operands[1];
1237 auto size = src.getBitSize();
1238
1239 /* Create symbolic operands */
1240 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1241 auto op2 = this->astCtxt->bvand(
1242 this->symbolicEngine->getOperandAst(inst, src),
1243 dst.getBitSize() == 64 ? this->astCtxt->bv(0x3f, size) : this->astCtxt->bv(0x1f, size)
1244 );
1245
1246 /* Create the semantics */
1247 auto node = this->astCtxt->bvashr(op1, op2);
1248
1249 /* Create symbolic expression */
1250 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.SRAI operation");
1251
1252 /* Spread taint */
1253 expr->isTainted = this->taintEngine->taintUnion(dst, src);
1254
1255 /* Update the symbolic control flow */
1256 this->controlFlow_s(inst);
1257 }
1258
1259
1260 void riscvSemantics::c_srli_s(triton::arch::Instruction& inst) {
1261 auto& dst = inst.operands[0];
1262 auto& src = inst.operands[1];
1263 auto size = src.getBitSize();
1264
1265 /* Create symbolic operands */
1266 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1267 auto op2 = this->astCtxt->bvand(
1268 this->symbolicEngine->getOperandAst(inst, src),
1269 dst.getBitSize() == 64 ? this->astCtxt->bv(0x3f, size) : this->astCtxt->bv(0x1f, size)
1270 );
1271
1272 /* Create the semantics */
1273 auto node = this->astCtxt->bvlshr(op1, op2);
1274
1275 /* Create symbolic expression */
1276 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.SRLI operation");
1277
1278 /* Spread taint */
1279 expr->isTainted = this->taintEngine->taintUnion(dst, src);
1280
1281 /* Update the symbolic control flow */
1282 this->controlFlow_s(inst);
1283 }
1284
1285
1286 void riscvSemantics::c_sub_s(triton::arch::Instruction& inst) {
1287 auto& dst = inst.operands[0];
1288 auto& src = inst.operands[1];
1289
1290 /* Create symbolic operands */
1291 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1292 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
1293
1294 /* Create the semantics */
1295 auto node = this->astCtxt->bvsub(op1, op2);
1296
1297 /* Create symbolic expression */
1298 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.SUB operation");
1299
1300 /* Spread taint */
1301 expr->isTainted = this->taintEngine->taintUnion(dst, src);
1302
1303 /* Update the symbolic control flow */
1304 this->controlFlow_s(inst);
1305 }
1306
1307
1308 void riscvSemantics::c_subw_s(triton::arch::Instruction& inst) { /* 64-bit only */
1309 auto& dst = inst.operands[0];
1310 auto& src = inst.operands[1];
1311
1312 /* Create symbolic operands */
1313 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, dst));
1314 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src));
1315
1316 /* Create the semantics */
1317 auto node = this->astCtxt->sx(32, this->astCtxt->bvsub(op1, op2));
1318
1319 /* Create symbolic expression */
1320 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.SUBW operation");
1321
1322 /* Spread taint */
1323 expr->isTainted = this->taintEngine->taintUnion(dst, src);
1324
1325 /* Update the symbolic control flow */
1326 this->controlFlow_s(inst);
1327 }
1328
1329
1330 void riscvSemantics::c_sw_s(triton::arch::Instruction& inst) {
1331 // M[x[rs1] + offset] := (x[rs2] & 0xffffffff)
1332 auto& src = inst.operands[0]; // rs2
1333 auto& imm = inst.operands[1]; // offset - disp
1334 auto& dst = inst.operands[2]; // rs1 - base
1335
1336 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1337 /* Construct double word memory access manually with base and displacement */
1338 triton::arch::MemoryAccess mem;
1339 mem.setBits(triton::bitsize::dword - 1, 0);
1340 triton::arch::Immediate& disp = imm.getImmediate();
1341 triton::arch::Register& base = dst.getRegister();
1342 mem.setBaseRegister(base);
1343 mem.setDisplacement(disp);
1344 auto mem_op = triton::arch::OperandWrapper(mem);
1345 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1346
1347 /* Create the semantics */
1348 auto node = this->symbolicEngine->getOperandAst(inst, src);
1349 if (src.getBitSize() == 64) {
1350 node = this->astCtxt->extract(31, 0, node);
1351 }
1352
1353 /* Create symbolic expression */
1354 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, mem_op, "C.SW operation - STORE access");
1355
1356 /* Spread taint */
1357 expr->isTainted = this->taintEngine->taintAssignment(mem_op, src);
1358
1359 /* Update the symbolic control flow */
1360 this->controlFlow_s(inst);
1361 }
1362
1363
1364 void riscvSemantics::c_swsp_s(triton::arch::Instruction& inst) {
1365 // M[sp + offset] := (x[rs] & 0xffffffff)
1366 auto& src = inst.operands[0]; // rs
1367 auto& imm = inst.operands[1]; // offset - disp; (sp - base)
1368
1369 // FIXME when fixed https://github.com/capstone-engine/capstone/issues/2351
1370 /* Construct double word memory access manually with base and displacement */
1371 triton::arch::MemoryAccess mem;
1372 mem.setBits(triton::bitsize::dword - 1, 0);
1373 triton::arch::Immediate& disp = imm.getImmediate();
1374 auto sp = this->architecture->getStackPointer();
1375 mem.setBaseRegister(sp);
1376 mem.setDisplacement(disp);
1377 auto mem_op = triton::arch::OperandWrapper(mem);
1378 this->symbolicEngine->initLeaAst(mem_op.getMemory());
1379
1380 /* Create the semantics */
1381 auto node = this->symbolicEngine->getOperandAst(inst, src);
1382 if (src.getBitSize() == 64) {
1383 node = this->astCtxt->extract(31, 0, node);
1384 }
1385
1386 /* Create symbolic expression */
1387 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, mem_op, "C.SWSP operation - STORE access");
1388
1389 /* Spread taint */
1390 expr->isTainted = this->taintEngine->taintAssignment(mem_op, src);
1391
1392 /* Update the symbolic control flow */
1393 this->controlFlow_s(inst);
1394 }
1395
1396
1397 void riscvSemantics::c_xor_s(triton::arch::Instruction& inst) {
1398 auto& dst = inst.operands[0];
1399 auto& src = inst.operands[1];
1400
1401 /* Create symbolic operands */
1402 auto op1 = this->symbolicEngine->getOperandAst(inst, dst);
1403 auto op2 = this->symbolicEngine->getOperandAst(inst, src);
1404
1405 /* Create the semantics */
1406 auto node = this->astCtxt->bvxor(op1, op2);
1407
1408 /* Create symbolic expression */
1409 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "C.XOR operation");
1410
1411 /* Spread taint */
1412 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(dst) | this->taintEngine->isTainted(src));
1413
1414 /* Update the symbolic control flow */
1415 this->controlFlow_s(inst);
1416 }
1417
1418
1419 void riscvSemantics::div_s(triton::arch::Instruction& inst) {
1420 auto& dst = inst.operands[0];
1421 auto& src1 = inst.operands[1];
1422 auto& src2 = inst.operands[2];
1423
1424 /* Create symbolic operands */
1425 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1426 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1427
1428 /* Create the semantics */
1429 auto node = this->astCtxt->ite(
1430 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
1431 this->astCtxt->bv(-1, dst.getBitSize()),
1432 this->astCtxt->bvsdiv(op1, op2)
1433 );
1434
1435 /* Create symbolic expression */
1436 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "DIV operation");
1437
1438 /* Spread taint */
1439 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1440
1441 /* Update the symbolic control flow */
1442 this->controlFlow_s(inst);
1443 }
1444
1445
1446 void riscvSemantics::divu_s(triton::arch::Instruction& inst) {
1447 auto& dst = inst.operands[0];
1448 auto& src1 = inst.operands[1];
1449 auto& src2 = inst.operands[2];
1450
1451 /* Create symbolic operands */
1452 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1453 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1454
1455 /* Create the semantics */
1456 auto node = this->astCtxt->ite(
1457 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
1458 this->astCtxt->bv(-1, dst.getBitSize()),
1459 this->astCtxt->bvudiv(op1, op2)
1460 );
1461
1462 /* Create symbolic expression */
1463 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "DIVU operation");
1464
1465 /* Spread taint */
1466 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1467
1468 /* Update the symbolic control flow */
1469 this->controlFlow_s(inst);
1470 }
1471
1472
1473 void riscvSemantics::divuw_s(triton::arch::Instruction& inst) { /* 64-bit only */
1474 auto& dst = inst.operands[0];
1475 auto& src1 = inst.operands[1];
1476 auto& src2 = inst.operands[2];
1477
1478 /* Create symbolic operands */
1479 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
1480 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
1481
1482 /* Create the semantics */
1483 auto node = this->astCtxt->ite(
1484 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
1485 this->astCtxt->bv(-1, dst.getBitSize()),
1486 this->astCtxt->sx(32, this->astCtxt->bvudiv(op1, op2))
1487 );
1488
1489 /* Create symbolic expression */
1490 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "DIVUW operation");
1491
1492 /* Spread taint */
1493 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1494
1495 /* Update the symbolic control flow */
1496 this->controlFlow_s(inst);
1497 }
1498
1499
1500 void riscvSemantics::divw_s(triton::arch::Instruction& inst) { /* 64-bit only */
1501 auto& dst = inst.operands[0];
1502 auto& src1 = inst.operands[1];
1503 auto& src2 = inst.operands[2];
1504
1505 /* Create symbolic operands */
1506 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
1507 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
1508
1509 /* Create the semantics */
1510 auto node = this->astCtxt->ite(
1511 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
1512 this->astCtxt->bv(-1, dst.getBitSize()),
1513 this->astCtxt->sx(32, this->astCtxt->bvsdiv(op1, op2))
1514 );
1515
1516 /* Create symbolic expression */
1517 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "DIVW operation");
1518
1519 /* Spread taint */
1520 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1521
1522 /* Update the symbolic control flow */
1523 this->controlFlow_s(inst);
1524 }
1525
1526 void riscvSemantics::jal_s(triton::arch::Instruction& inst) {
1527 /* Check for possible pseudo instructions
1528 j offset -- [jal x0, offset] -- Jump
1529 jal offset -- [jal x1, offset] -- Jump and link
1530 */
1531 auto mnem = inst.getDisassembly();
1532 if (mnem[1] == ' ') {
1533 jal_j_s(inst);
1534 return;
1535 }
1536
1537 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
1538 auto size = pc.getBitSize();
1539
1540 auto ra = this->architecture->getRegister(
1541 size == 64 ?
1542 triton::arch::ID_REG_RV64_X1 :
1543 triton::arch::ID_REG_RV32_X1
1544 );
1545 auto reg = triton::arch::OperandWrapper(ra);
1546 auto& src1 = inst.operands[0];
1547
1548 /* Create symbolic operands */
1549 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
1550 auto imm = this->symbolicEngine->getOperandAst(inst, src1);
1551 if (src1.getType() == triton::arch::OP_REG) {
1552 auto& src2 = inst.operands[1];
1553 reg = src1;
1554 imm = this->symbolicEngine->getOperandAst(inst, src2);
1555 }
1556
1557 /* Create the semantics */
1558 auto node = this->astCtxt->bv(inst.getNextAddress(), size);
1559 auto node_pc = this->astCtxt->bvadd(pc_ast, imm);
1560
1561 /* Create symbolic expression */
1562 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, reg, "JAL operation ret addr");
1563 auto expr_pc = this->symbolicEngine->createSymbolicExpression(inst, node_pc, pc, "Program Counter");
1564
1565 /* Spread taint */
1566 expr->isTainted = this->taintEngine->setTaint(reg, this->taintEngine->isTainted(pc));
1567 expr_pc->isTainted = this->taintEngine->setTaint(pc, this->taintEngine->isTainted(pc));
1568
1569 /* Create the path constraint */
1570 this->symbolicEngine->pushPathConstraint(inst, expr_pc);
1571 }
1572
1573
1574 void riscvSemantics::jal_j_s(triton::arch::Instruction& inst) {
1575 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
1576 auto& src1 = inst.operands[0];
1577 auto size = pc.getBitSize();
1578
1579 /* Create symbolic operands */
1580 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
1581 auto imm = this->symbolicEngine->getOperandAst(inst, src1);
1582
1583 /* Create the semantics */
1584 auto node_pc = this->astCtxt->bvadd(pc_ast, imm);
1585
1586 /* Create symbolic expression */
1587 auto expr_pc = this->symbolicEngine->createSymbolicExpression(inst, node_pc, pc, "Program Counter");
1588
1589 /* Spread taint */
1590 expr_pc->isTainted = this->taintEngine->isTainted(pc);
1591
1592 /* Create the path constraint */
1593 this->symbolicEngine->pushPathConstraint(inst, expr_pc);
1594 }
1595
1596
1597 void riscvSemantics::jalr_s(triton::arch::Instruction& inst) {
1598 /*
1599 * x[rd] := pc + 4; pc := (x[rs] + imm) & ~1
1600 * Check for possible pseudo instructions
1601 * ret -- [jalr x0, x1, 0] -- Return from subroutine
1602 * jr rs -- [jalr x0, rs, 0] -- Jump register
1603 * jalr rs -- [jalr x1, rs, 0] -- Jump and link register
1604 */
1605 auto mnem = inst.getDisassembly();
1606 if (mnem[2] != 'l') { jalr_no_link_s(inst); return; } // ret & jr semantics
1607
1608 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
1609 auto size = pc.getBitSize();
1610 auto ra = this->architecture->getRegister(
1611 size == 64 ?
1612 triton::arch::ID_REG_RV64_X1 :
1613 triton::arch::ID_REG_RV32_X1
1614 );
1615 auto dst = triton::arch::OperandWrapper(ra);
1616 auto& src = inst.operands[0];
1617
1618 /* Create semantics (jalr with 1 operand) */
1619 auto pc_ast = this->symbolicEngine->getOperandAst(pc);
1620 auto node_dst = this->astCtxt->bv(inst.getNextAddress(), size);
1621 auto node_pc = this->symbolicEngine->getOperandAst(inst, src);
1622 if (inst.operands.size() == 3) { // jalr with 3 operands semantics
1623 dst = src;
1624 src = inst.operands[1];
1625 auto& imm = inst.operands[2];
1626
1627 /* Create symbolic operands */
1628 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
1629 auto op2 = this->symbolicEngine->getOperandAst(inst, imm);
1630
1631 node_pc = this->astCtxt->bvadd(op1, op2);
1632 }
1633 node_pc = this->astCtxt->bvand( /* ignore last bit */
1634 node_pc,
1635 this->astCtxt->bvshl(this->astCtxt->bv(-1, size), this->astCtxt->bv(1, size))
1636 );
1637
1638 /* Create symbolic expression */
1639 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node_dst, dst, "JALR operation ret addr");
1640 auto expr_pc = this->symbolicEngine->createSymbolicExpression(inst, node_pc, pc, "Program Counter");
1641
1642 /* Spread taint */
1643 expr->isTainted = this->taintEngine->isTainted(pc);
1644 expr_pc->isTainted = this->taintEngine->setTaint(pc, this->taintEngine->isTainted(src));
1645
1646 /* Create the path constraint */
1647 this->symbolicEngine->pushPathConstraint(inst, expr_pc);
1648 }
1649
1650
1651 void riscvSemantics::jalr_no_link_s(triton::arch::Instruction& inst) { // rd == x0
1652 auto pc = triton::arch::OperandWrapper(this->architecture->getProgramCounter());
1653 auto size = pc.getBitSize();
1654 auto ra = this->architecture->getRegister(
1655 size == 64 ?
1656 triton::arch::ID_REG_RV64_X1 :
1657 triton::arch::ID_REG_RV32_X1
1658 );
1659 auto src = triton::arch::OperandWrapper(ra);
1660 if (inst.operands.size()) {
1661 src = inst.operands[0];
1662 }
1663
1664 /* Create the semantics */
1665 auto node = this->symbolicEngine->getOperandAst(inst, src);
1666 node = this->astCtxt->bvand( /* ignore last bit */
1667 node,
1668 this->astCtxt->bvshl(this->astCtxt->bv(-1, size), this->astCtxt->bv(1, size))
1669 );
1670
1671 /* Create symbolic expression */
1672 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, pc, "Program Counter");
1673
1674 /* Spread taint */
1675 expr->isTainted = this->taintEngine->setTaint(pc, this->taintEngine->isTainted(src));
1676
1677 /* Create the path constraint */
1678 this->symbolicEngine->pushPathConstraint(inst, expr);
1679 }
1680
1681
1682 void riscvSemantics::lb_s(triton::arch::Instruction& inst) {
1683 // x[rd] := M[x[rs] + offset][7:0]
1684 auto& dst = inst.operands[0]; // rd
1685 auto& src = inst.operands[1]; // rs - base, offset - disp
1686 auto size = dst.getBitSize();
1687
1688 /* Create the semantics */
1689 auto node = this->symbolicEngine->getOperandAst(inst, src);
1690 node = this->astCtxt->sx(size - 8, node);
1691
1692 /* Create symbolic expression */
1693 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LB operation - LOAD access");
1694
1695 /* Spread taint */
1696 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1697
1698 /* Update the symbolic control flow */
1699 this->controlFlow_s(inst);
1700 }
1701
1702
1703 void riscvSemantics::lbu_s(triton::arch::Instruction& inst) {
1704 // x[rd] := M[x[rs] + offset][7:0]
1705 auto& dst = inst.operands[0]; // rd
1706 auto& src = inst.operands[1]; // rs - base, offset - disp
1707 auto size = dst.getBitSize();
1708
1709 /* Create the semantics */
1710 auto node = this->symbolicEngine->getOperandAst(inst, src);
1711 node = this->astCtxt->zx(size - 8, node);
1712
1713 /* Create symbolic expression */
1714 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LBU operation - LOAD access");
1715
1716 /* Spread taint */
1717 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1718
1719 /* Update the symbolic control flow */
1720 this->controlFlow_s(inst);
1721 }
1722
1723
1724 void riscvSemantics::ld_s(triton::arch::Instruction& inst) { /* 64-bit only */
1725 // x[rd] := M[x[rs] + offset][63:0]
1726 auto& dst = inst.operands[0]; // rd
1727 auto& src = inst.operands[1]; // rs - base, offset - disp
1728
1729 /* Create the semantics */
1730 auto node = this->symbolicEngine->getOperandAst(inst, src);
1731
1732 /* Create symbolic expression */
1733 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LD operation - LOAD access");
1734
1735 /* Spread taint */
1736 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1737
1738 /* Update the symbolic control flow */
1739 this->controlFlow_s(inst);
1740 }
1741
1742
1743 void riscvSemantics::lh_s(triton::arch::Instruction& inst) {
1744 // x[rd] := M[x[rs] + offset][15:0]
1745 auto& dst = inst.operands[0]; // rd
1746 auto& src = inst.operands[1]; // rs - base, offset - disp
1747 auto size = dst.getBitSize();
1748
1749 /* Create the semantics */
1750 auto node = this->symbolicEngine->getOperandAst(inst, src);
1751 node = this->astCtxt->sx(size - 16, node);
1752
1753 /* Create symbolic expression */
1754 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LH operation - LOAD access");
1755
1756 /* Spread taint */
1757 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1758
1759 /* Update the symbolic control flow */
1760 this->controlFlow_s(inst);
1761 }
1762
1763
1764 void riscvSemantics::lhu_s(triton::arch::Instruction& inst) {
1765 // x[rd] := M[x[rs] + offset][15:0]
1766 auto& dst = inst.operands[0]; // rd
1767 auto& src = inst.operands[1]; // rs - base, offset - disp
1768 auto size = dst.getBitSize();
1769
1770 /* Create the semantics */
1771 auto node = this->symbolicEngine->getOperandAst(inst, src);
1772 node = this->astCtxt->zx(size - 16, node);
1773
1774 /* Create symbolic expression */
1775 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LHU operation - LOAD access");
1776
1777 /* Spread taint */
1778 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1779
1780 /* Update the symbolic control flow */
1781 this->controlFlow_s(inst);
1782 }
1783
1784
1785 void riscvSemantics::lui_s(triton::arch::Instruction& inst) {
1786 // dst := (src_imm(_20) << 12)
1787 auto& dst = inst.operands[0];
1788 auto& src = inst.operands[1];
1789 auto size = dst.getBitSize();
1790
1791 /* Create symbolic operands */
1792 auto imm = this->symbolicEngine->getOperandAst(inst, src);
1793
1794 /* Create the semantics */
1795 auto node = this->astCtxt->bvshl(
1796 this->astCtxt->sx(size - 20, this->astCtxt->extract(19, 0, imm)),
1797 this->astCtxt->bv(12, size)
1798 );
1799
1800 /* Create symbolic expression */
1801 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LUI operation");
1802
1803 /* Spread taint */
1804 expr->isTainted = this->taintEngine->setTaint(dst, false);
1805
1806 /* Update the symbolic control flow */
1807 this->controlFlow_s(inst);
1808 }
1809
1810
1811 void riscvSemantics::lw_s(triton::arch::Instruction& inst) {
1812 // x[rd] := M[x[rs] + offset][31:0]
1813 auto& dst = inst.operands[0]; // rd
1814 auto& src = inst.operands[1]; // rs1 - base, offset - disp
1815
1816 /* Create the semantics */
1817 auto node = this->symbolicEngine->getOperandAst(inst, src);
1818 if (dst.getBitSize() == 64) { /* extend to register size */
1819 node = this->astCtxt->sx(32, node);
1820 }
1821
1822 /* Create symbolic expression */
1823 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LW operation - LOAD access");
1824
1825 /* Spread taint */
1826 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1827
1828 /* Update the symbolic control flow */
1829 this->controlFlow_s(inst);
1830 }
1831
1832
1833 void riscvSemantics::lwu_s(triton::arch::Instruction& inst) { /* 64-bit only */
1834 // x[rd] := M[x[rs] + offset][31:0]
1835 auto& dst = inst.operands[0]; // rd
1836 auto& src = inst.operands[1]; // rs1 - base, offset - disp
1837 auto size = dst.getBitSize();
1838
1839 /* Create the semantics */
1840 auto node = this->symbolicEngine->getOperandAst(inst, src);
1841 node = this->astCtxt->zx(32, node);
1842
1843 /* Create symbolic expression */
1844 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LWU operation - LOAD access");
1845
1846 /* Spread taint */
1847 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
1848
1849 /* Update the symbolic control flow */
1850 this->controlFlow_s(inst);
1851 }
1852
1853
1854 void riscvSemantics::mul_s(triton::arch::Instruction& inst) {
1855 auto& dst = inst.operands[0];
1856 auto& src1 = inst.operands[1];
1857 auto& src2 = inst.operands[2];
1858
1859 /* Create symbolic operands */
1860 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1861 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1862
1863 /* Create the semantics */
1864 auto node = this->astCtxt->bvmul(op1, op2);
1865
1866 /* Create symbolic expression */
1867 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MUL operation");
1868
1869 /* Spread taint */
1870 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1871
1872 /* Update the symbolic control flow */
1873 this->controlFlow_s(inst);
1874 }
1875
1876
1877 void riscvSemantics::mulh_s(triton::arch::Instruction& inst) {
1878 auto& dst = inst.operands[0];
1879 auto& src1 = inst.operands[1];
1880 auto& src2 = inst.operands[2];
1881 auto size = src2.getBitSize();
1882
1883 /* Create symbolic operands */
1884 auto op1 = this->astCtxt->sx(size, this->symbolicEngine->getOperandAst(inst, src1));
1885 auto op2 = this->astCtxt->sx(size, this->symbolicEngine->getOperandAst(inst, src2));
1886
1887 /* Create the semantics */
1888 auto node = this->astCtxt->extract(size * 2 - 1, size, this->astCtxt->bvmul(op1, op2));
1889
1890 /* Create symbolic expression */
1891 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MULH operation");
1892
1893 /* Spread taint */
1894 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1895
1896 /* Update the symbolic control flow */
1897 this->controlFlow_s(inst);
1898 }
1899
1900
1901 void riscvSemantics::mulhsu_s(triton::arch::Instruction& inst) {
1902 auto& dst = inst.operands[0];
1903 auto& src1 = inst.operands[1];
1904 auto& src2 = inst.operands[2];
1905 auto size = src2.getBitSize();
1906
1907 /* Create symbolic operands */
1908 auto op1 = this->astCtxt->sx(size, this->symbolicEngine->getOperandAst(inst, src1));
1909 auto op2 = this->astCtxt->zx(size, this->symbolicEngine->getOperandAst(inst, src2));
1910
1911 /* Create the semantics */
1912 auto node = this->astCtxt->extract(size * 2 - 1, size, this->astCtxt->bvmul(op1, op2));
1913
1914 /* Create symbolic expression */
1915 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MULHSU operation");
1916
1917 /* Spread taint */
1918 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1919
1920 /* Update the symbolic control flow */
1921 this->controlFlow_s(inst);
1922 }
1923
1924
1925 void riscvSemantics::mulhu_s(triton::arch::Instruction& inst) {
1926 auto& dst = inst.operands[0];
1927 auto& src1 = inst.operands[1];
1928 auto& src2 = inst.operands[2];
1929 auto size = src2.getBitSize();
1930
1931 /* Create symbolic operands */
1932 auto op1 = this->astCtxt->zx(size, this->symbolicEngine->getOperandAst(inst, src1));
1933 auto op2 = this->astCtxt->zx(size, this->symbolicEngine->getOperandAst(inst, src2));
1934
1935 /* Create the semantics */
1936 auto node = this->astCtxt->extract(size * 2 - 1, size, this->astCtxt->bvmul(op1, op2));
1937
1938 /* Create symbolic expression */
1939 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MULHU operation");
1940
1941 /* Spread taint */
1942 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1943
1944 /* Update the symbolic control flow */
1945 this->controlFlow_s(inst);
1946 }
1947
1948
1949 void riscvSemantics::mulw_s(triton::arch::Instruction& inst) { /* 64-bit only */
1950 auto& dst = inst.operands[0];
1951 auto& src1 = inst.operands[1];
1952 auto& src2 = inst.operands[2];
1953
1954 /* Create symbolic operands */
1955 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
1956 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
1957
1958 /* Create the semantics */
1959 auto node = this->astCtxt->sx(32, this->astCtxt->bvmul(op1, op2));
1960
1961 /* Create symbolic expression */
1962 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MULW operation");
1963
1964 /* Spread taint */
1965 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1966
1967 /* Update the symbolic control flow */
1968 this->controlFlow_s(inst);
1969 }
1970
1971
1972 void riscvSemantics::or_s(triton::arch::Instruction& inst) {
1973 auto& dst = inst.operands[0];
1974 auto& src1 = inst.operands[1];
1975 auto& src2 = inst.operands[2];
1976
1977 /* Create symbolic operands */
1978 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
1979 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
1980
1981 /* Create the semantics */
1982 auto node = this->astCtxt->bvor(op1, op2);
1983
1984 /* Create symbolic expression */
1985 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "OR(I) operation");
1986
1987 /* Spread taint */
1988 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
1989
1990 /* Update the symbolic control flow */
1991 this->controlFlow_s(inst);
1992 }
1993
1994
1995 void riscvSemantics::rem_s(triton::arch::Instruction& inst) {
1996 auto& dst = inst.operands[0];
1997 auto& src1 = inst.operands[1];
1998 auto& src2 = inst.operands[2];
1999 auto size = dst.getBitSize();
2000
2001 /* Create symbolic operands */
2002 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2003 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2004
2005 /* Create the semantics */
2006 auto node = this->astCtxt->ite(
2007 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
2008 op1,
2009 this->astCtxt->ite( // overflow check
2010 this->astCtxt->land(
2011 this->astCtxt->equal(op1, this->astCtxt->bv(-1, size)),
2012 this->astCtxt->equal(op2, this->astCtxt->bv((1 << (size - 1)), size))
2013 ),
2014 this->astCtxt->bv(0, size),
2015 this->astCtxt->bvsrem(op1, op2)
2016 )
2017 );
2018
2019 /* Create symbolic expression */
2020 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REM operation");
2021
2022 /* Spread taint */
2023 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2024
2025 /* Update the symbolic control flow */
2026 this->controlFlow_s(inst);
2027 }
2028
2029
2030 void riscvSemantics::remu_s(triton::arch::Instruction& inst) {
2031 auto& dst = inst.operands[0];
2032 auto& src1 = inst.operands[1];
2033 auto& src2 = inst.operands[2];
2034
2035 /* Create symbolic operands */
2036 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2037 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2038
2039 /* Create the semantics */
2040 auto node = this->astCtxt->ite(
2041 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
2042 op1,
2043 this->astCtxt->bvurem(op1, op2)
2044 );
2045
2046 /* Create symbolic expression */
2047 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REMU operation");
2048
2049 /* Spread taint */
2050 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2051
2052 /* Update the symbolic control flow */
2053 this->controlFlow_s(inst);
2054 }
2055
2056
2057 void riscvSemantics::remuw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2058 auto& dst = inst.operands[0];
2059 auto& src1 = inst.operands[1];
2060 auto& src2 = inst.operands[2];
2061
2062 /* Create symbolic operands */
2063 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
2064 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
2065
2066 /* Create the semantics */
2067 auto node = this->astCtxt->ite(
2068 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
2069 this->astCtxt->sx(32, op1),
2070 this->astCtxt->sx(32, this->astCtxt->bvurem(op1, op2))
2071 );
2072
2073 /* Create symbolic expression */
2074 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REMUW operation");
2075
2076 /* Spread taint */
2077 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2078
2079 /* Update the symbolic control flow */
2080 this->controlFlow_s(inst);
2081 }
2082
2083
2084 void riscvSemantics::remw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2085 auto& dst = inst.operands[0];
2086 auto& src1 = inst.operands[1];
2087 auto& src2 = inst.operands[2];
2088
2089 /* Create symbolic operands */
2090 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
2091 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
2092
2093 /* Create the semantics */
2094 uint32_t ov_value = 0x80000000;
2095 auto node = this->astCtxt->ite( // div-by-zero check
2096 this->astCtxt->equal(op2, this->astCtxt->bv(0, op2->getBitvectorSize())),
2097 this->astCtxt->sx(32, op1),
2098 this->astCtxt->ite( // signed overflow check
2099 this->astCtxt->land(
2100 this->astCtxt->equal(op1, this->astCtxt->bv(ov_value, 32)),
2101 this->astCtxt->equal(op2, this->astCtxt->bv(-1, 32))
2102 ),
2103 this->astCtxt->bv(0, dst.getBitSize()),
2104 this->astCtxt->sx(32, this->astCtxt->bvsrem(op1, op2))
2105 )
2106 );
2107
2108 /* Create symbolic expression */
2109 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REMW operation");
2110
2111 /* Spread taint */
2112 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2113
2114 /* Update the symbolic control flow */
2115 this->controlFlow_s(inst);
2116 }
2117
2118
2119 void riscvSemantics::sb_s(triton::arch::Instruction& inst) {
2120 // M[x[rs1] + offset] := (x[rs2] & 0xff)
2121 auto& src = inst.operands[0]; // rs2
2122 auto& dst = inst.operands[1]; // rs1 - base, offset - disp
2123
2124 /* Create symbolic operands */
2125 auto node = this->symbolicEngine->getOperandAst(inst, src);
2126 node = this->astCtxt->extract(7, 0, node);
2127
2128 /* Create symbolic expression */
2129 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SB operation - STORE access");
2130
2131 /* Spread taint */
2132 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2133
2134 /* Update the symbolic control flow */
2135 this->controlFlow_s(inst);
2136 }
2137
2138
2139 void riscvSemantics::sd_s(triton::arch::Instruction& inst) { /* 64-bit only */
2140 // M[x[rs1] + offset] := x[rs2]
2141 auto& src = inst.operands[0]; // rs2
2142 auto& dst = inst.operands[1]; // rs1 - base, offset - disp
2143
2144 /* Create symbolic operands */
2145 auto node = this->symbolicEngine->getOperandAst(inst, src);
2146
2147 /* Create symbolic expression */
2148 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SD operation - STORE access");
2149
2150 /* Spread taint */
2151 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2152
2153 /* Update the symbolic control flow */
2154 this->controlFlow_s(inst);
2155 }
2156
2157
2158 void riscvSemantics::sh_s(triton::arch::Instruction& inst) {
2159 // M[x[rs1] + offset] := (x[rs2] & 0xffff)
2160 auto& src = inst.operands[0]; // rs2
2161 auto& dst = inst.operands[1]; // rs1 - base, offset - disp
2162
2163 /* Create symbolic operands */
2164 auto node = this->symbolicEngine->getOperandAst(inst, src);
2165 node = this->astCtxt->extract(15, 0, node);
2166
2167 /* Create symbolic expression */
2168 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SH operation - STORE access");
2169
2170 /* Spread taint */
2171 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2172
2173 /* Update the symbolic control flow */
2174 this->controlFlow_s(inst);
2175 }
2176
2177
2178 void riscvSemantics::sll_s(triton::arch::Instruction& inst) {
2179 auto& dst = inst.operands[0];
2180 auto& src1 = inst.operands[1];
2181 auto& src2 = inst.operands[2];
2182 auto size = src2.getBitSize();
2183
2184 /* Create symbolic operands */
2185 auto bits = size == 64 ? 0x3f : 0x1f;
2186 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2187 auto op2 = this->astCtxt->bvand(
2188 this->symbolicEngine->getOperandAst(inst, src2),
2189 this->astCtxt->bv(bits, size)
2190 );
2191
2192 /* Create the semantics */
2193 auto node = this->astCtxt->bvshl(op1, op2);
2194
2195 /* Create symbolic expression */
2196 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SLL(I) operation");
2197
2198 /* Spread taint */
2199 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2200
2201 /* Update the symbolic control flow */
2202 this->controlFlow_s(inst);
2203 }
2204
2205
2206 void riscvSemantics::sllw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2207 auto& dst = inst.operands[0];
2208 auto& src1 = inst.operands[1];
2209 auto& src2 = inst.operands[2];
2210 auto size = src2.getBitSize();
2211
2212 /* Create symbolic operands */
2213 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2214 auto op2 = this->astCtxt->bvand(
2215 this->symbolicEngine->getOperandAst(inst, src2),
2216 this->astCtxt->bv(0x1f, size)
2217 );
2218
2219 /* Create the semantics */
2220 auto node = this->astCtxt->sx(32,
2221 this->astCtxt->bvshl(this->astCtxt->extract(31, 0, op1),
2222 this->astCtxt->extract(31, 0, op2)));
2223
2224 /* Create symbolic expression */
2225 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SLL(I)W operation");
2226
2227 /* Spread taint */
2228 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2229
2230 /* Update the symbolic control flow */
2231 this->controlFlow_s(inst);
2232 }
2233
2234
2235 void riscvSemantics::slt_s(triton::arch::Instruction& inst) {
2236 /* Check for possible pseudo instructions
2237 sltz rd, rs -- [slt rd, rs, x0] -- Set if < zero
2238 sgtz rd, rs -- [slt rd, x0, rs] -- Set if > zero
2239 */
2240 auto mnem = inst.getDisassembly();
2241 if (mnem[3] == 'z') {
2242 if (mnem[1] == 'l') { slt_sltz_s(inst); } else { slt_sgtz_s(inst); }
2243 } else {
2244 slti_s(inst);
2245 }
2246 }
2247
2248
2249 void riscvSemantics::slt_sgtz_s(triton::arch::Instruction& inst) {
2250 auto& dst = inst.operands[0];
2251 auto& src = inst.operands[1];
2252 auto size = dst.getBitSize();
2253
2254 /* Create symbolic operands */
2255 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2256 auto zero = this->astCtxt->bv(0, size);
2257
2258 /* Create the semantics */
2259 auto node = this->astCtxt->ite(this->astCtxt->bvsgt(op1, zero),
2260 this->astCtxt->bv(1, size),
2261 zero
2262 );
2263
2264 /* Create symbolic expression */
2265 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SGTZ operation");
2266
2267 /* Set condition flag */
2268 if ((long long)op1->evaluate() > 0)
2269 inst.setConditionTaken(true);
2270
2271 /* Spread taint */
2272 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src));
2273
2274 /* Update the symbolic control flow */
2275 this->controlFlow_s(inst);
2276 }
2277
2278
2279 void riscvSemantics::slt_sltz_s(triton::arch::Instruction& inst) {
2280 auto& dst = inst.operands[0];
2281 auto& src = inst.operands[1];
2282 auto size = dst.getBitSize();
2283
2284 /* Create symbolic operands */
2285 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2286 auto zero = this->astCtxt->bv(0, size);
2287
2288 /* Create the semantics */
2289 auto node = this->astCtxt->ite(this->astCtxt->bvslt(op1, zero),
2290 this->astCtxt->bv(1, size),
2291 zero
2292 );
2293
2294 /* Create symbolic expression */
2295 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SLTZ operation");
2296
2297 /* Set condition flag */
2298 if ((long long)op1->evaluate() < 0)
2299 inst.setConditionTaken(true);
2300
2301 /* Spread taint */
2302 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src));
2303
2304 /* Update the symbolic control flow */
2305 this->controlFlow_s(inst);
2306 }
2307
2308
2309 void riscvSemantics::slti_s(triton::arch::Instruction& inst) {
2310 auto& dst = inst.operands[0];
2311 auto& src1 = inst.operands[1];
2312 auto& src2 = inst.operands[2];
2313 auto size = dst.getBitSize();
2314
2315 /* Create symbolic operands */
2316 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2317 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2318
2319 /* Create the semantics */
2320 auto node = this->astCtxt->ite(this->astCtxt->bvslt(op1, op2),
2321 this->astCtxt->bv(1, size),
2322 this->astCtxt->bv(0, size)
2323 );
2324
2325 /* Create symbolic expression */
2326 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SLT(I) operation");
2327
2328 /* Set condition flag */
2329 if ((long long)(op2->evaluate() - op1->evaluate()) > 0)
2330 inst.setConditionTaken(true);
2331
2332 /* Spread taint */
2333 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2334
2335 /* Update the symbolic control flow */
2336 this->controlFlow_s(inst);
2337 }
2338
2339
2340 void riscvSemantics::sltiu_seqz_s(triton::arch::Instruction& inst) {
2341 auto& dst = inst.operands[0];
2342 auto& src = inst.operands[1];
2343 auto size = dst.getBitSize();
2344
2345 /* Create symbolic operands */
2346 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2347 auto zero = this->astCtxt->bv(0, size);
2348
2349 /* Create the semantics */
2350 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, zero),
2351 this->astCtxt->bv(1, size),
2352 zero
2353 );
2354
2355 /* Create symbolic expression */
2356 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SEQZ operation");
2357
2358 /* Set condition flag */
2359 if (op1->evaluate() == 0)
2360 inst.setConditionTaken(true);
2361
2362 /* Spread taint */
2363 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src));
2364
2365 /* Update the symbolic control flow */
2366 this->controlFlow_s(inst);
2367 }
2368
2369
2370 void riscvSemantics::sltu_s(triton::arch::Instruction& inst) {
2371 /* Check for possible pseudo instructions
2372 seqz rd, rs -- [sltiu rd, rs, 1] -- Set if == zero
2373 snez rd, rs -- [sltu rd, x0, rs] -- Set if != zero
2374 */
2375 auto mnem = inst.getDisassembly();
2376 if (mnem[1] == 'e') {
2377 sltiu_seqz_s(inst);
2378 return;
2379 }
2380 if (mnem[1] == 'n') {
2381 sltu_snez_s(inst);
2382 return;
2383 }
2384
2385 auto& dst = inst.operands[0];
2386 auto& src1 = inst.operands[1];
2387 auto& src2 = inst.operands[2];
2388 auto size = dst.getBitSize();
2389
2390 /* Create symbolic operands */
2391 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2392 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2393
2394 /* Create the semantics */
2395 auto node = this->astCtxt->ite(this->astCtxt->bvult(op1, op2),
2396 this->astCtxt->bv(1, size),
2397 this->astCtxt->bv(0, size)
2398 );
2399
2400 /* Create symbolic expression */
2401 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SLT(I)U operation");
2402
2403 /* Set condition flag */
2404 if (op2->evaluate() > op1->evaluate())
2405 inst.setConditionTaken(true);
2406
2407 /* Spread taint */
2408 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2409
2410 /* Update the symbolic control flow */
2411 this->controlFlow_s(inst);
2412 }
2413
2414
2415 void riscvSemantics::sltu_snez_s(triton::arch::Instruction& inst) {
2416 auto& dst = inst.operands[0];
2417 auto& src = inst.operands[1];
2418 auto size = dst.getBitSize();
2419
2420 /* Create symbolic operands */
2421 auto op1 = this->symbolicEngine->getOperandAst(inst, src);
2422 auto zero = this->astCtxt->bv(0, size);
2423
2424 /* Create the semantics */
2425 auto node = this->astCtxt->ite(this->astCtxt->equal(op1, zero),
2426 zero,
2427 this->astCtxt->bv(1, size)
2428 );
2429
2430 /* Create symbolic expression */
2431 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SNEZ operation");
2432
2433 /* Set condition flag */
2434 if (op1->evaluate() != 0)
2435 inst.setConditionTaken(true);
2436
2437 /* Spread taint */
2438 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src));
2439
2440 /* Update the symbolic control flow */
2441 this->controlFlow_s(inst);
2442 }
2443
2444
2445 void riscvSemantics::sra_s(triton::arch::Instruction& inst) {
2446 auto& dst = inst.operands[0];
2447 auto& src1 = inst.operands[1];
2448 auto& src2 = inst.operands[2];
2449 auto size = src2.getBitSize();
2450
2451 /* Create symbolic operands */
2452 auto bits = size == 64 ? 0x3f : 0x1f;
2453 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2454 auto op2 = this->astCtxt->bvand(
2455 this->symbolicEngine->getOperandAst(inst, src2),
2456 this->astCtxt->bv(bits, size)
2457 );
2458
2459 /* Create the semantics */
2460 auto node = this->astCtxt->bvashr(op1, op2);
2461
2462 /* Create symbolic expression */
2463 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SRA operation");
2464
2465 /* Spread taint */
2466 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2467
2468 /* Update the symbolic control flow */
2469 this->controlFlow_s(inst);
2470 }
2471
2472
2473 void riscvSemantics::sraw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2474 auto& dst = inst.operands[0];
2475 auto& src1 = inst.operands[1];
2476 auto& src2 = inst.operands[2];
2477 auto size = src2.getBitSize();
2478
2479 /* Create symbolic operands */
2480 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2481 auto op2 = this->astCtxt->bvand(
2482 this->symbolicEngine->getOperandAst(inst, src2),
2483 this->astCtxt->bv(0x1f, size)
2484 );
2485
2486 /* Create the semantics */
2487 auto node = this->astCtxt->sx(32,
2488 this->astCtxt->bvashr(this->astCtxt->extract(31, 0, op1),
2489 this->astCtxt->extract(31, 0, op2)));
2490
2491 /* Create symbolic expression */
2492 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SRA(I)W operation");
2493
2494 /* Spread taint */
2495 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2496
2497 /* Update the symbolic control flow */
2498 this->controlFlow_s(inst);
2499 }
2500
2501
2502 void riscvSemantics::srl_s(triton::arch::Instruction& inst) {
2503 auto& dst = inst.operands[0];
2504 auto& src1 = inst.operands[1];
2505 auto& src2 = inst.operands[2];
2506 auto size = src2.getBitSize();
2507
2508 /* Create symbolic operands */
2509 auto bits = size == 64 ? 0x3f : 0x1f;
2510 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2511 auto op2 = this->astCtxt->bvand(
2512 this->symbolicEngine->getOperandAst(inst, src2),
2513 this->astCtxt->bv(bits, size)
2514 );
2515
2516 /* Create the semantics */
2517 auto node = this->astCtxt->bvlshr(op1, op2);
2518
2519 /* Create symbolic expression */
2520 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SRL(I) operation");
2521
2522 /* Spread taint */
2523 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2524
2525 /* Update the symbolic control flow */
2526 this->controlFlow_s(inst);
2527 }
2528
2529
2530 void riscvSemantics::srlw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2531 auto& dst = inst.operands[0];
2532 auto& src1 = inst.operands[1];
2533 auto& src2 = inst.operands[2];
2534 auto size = src2.getBitSize();
2535
2536 /* Create symbolic operands */
2537 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2538 auto op2 = this->astCtxt->bvand(
2539 this->symbolicEngine->getOperandAst(inst, src2),
2540 this->astCtxt->bv(0x1f, size)
2541 );
2542
2543 /* Create the semantics */
2544 auto node = this->astCtxt->sx(32,
2545 this->astCtxt->bvlshr(this->astCtxt->extract(31, 0, op1),
2546 this->astCtxt->extract(31, 0, op2)));
2547
2548 /* Create symbolic expression */
2549 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SRL(I)W operation");
2550
2551 /* Spread taint */
2552 expr->isTainted = this->taintEngine->taintUnion(src1, src2);
2553
2554 /* Update the symbolic control flow */
2555 this->controlFlow_s(inst);
2556 }
2557
2558
2559 void riscvSemantics::sub_s(triton::arch::Instruction& inst) {
2560 auto& dst = inst.operands[0];
2561 auto& src1 = inst.operands[1];
2562 auto size = dst.getBitSize();
2563 bool fix_taint = false;
2564
2565 /* Create symbolic operands and semantics */
2566 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2567 auto node = this->astCtxt->bvneg(op1); // neg pseudo instruction semantics
2568 if (inst.operands.size() > 2) {
2569 auto& src2 = inst.operands[2];
2570 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2571 node = this->astCtxt->bvsub(op1, op2); // sub semantics
2572 fix_taint = this->taintEngine->isTainted(src2);
2573 }
2574
2575 /* Create symbolic expression */
2576 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SUB operation");
2577
2578 /* Spread taint */
2579 expr->isTainted = this->taintEngine->isTainted(src1) || fix_taint;
2580
2581 /* Update the symbolic control flow */
2582 this->controlFlow_s(inst);
2583 }
2584
2585
2586 void riscvSemantics::subw_s(triton::arch::Instruction& inst) { /* 64-bit only */
2587 auto& dst = inst.operands[0];
2588 auto& src1 = inst.operands[1];
2589 auto size = dst.getBitSize();
2590 bool fix_taint = false;
2591
2592 /* Create symbolic operands and semantics */
2593 auto op1 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src1));
2594 auto node = this->astCtxt->sx(32, this->astCtxt->bvneg(op1)); // negw pseudo instruction semantics
2595 if (inst.operands.size() > 2) {
2596 auto& src2 = inst.operands[2];
2597 auto op2 = this->astCtxt->extract(31, 0, this->symbolicEngine->getOperandAst(inst, src2));
2598 node = this->astCtxt->sx(32, this->astCtxt->bvsub(op1, op2)); // subw semantics
2599 fix_taint = this->taintEngine->isTainted(src2);
2600 }
2601
2602 /* Create symbolic expression */
2603 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SUBW operation");
2604
2605 /* Spread taint */
2606 expr->isTainted = this->taintEngine->isTainted(src1) || fix_taint;
2607
2608 /* Update the symbolic control flow */
2609 this->controlFlow_s(inst);
2610 }
2611
2612
2613 void riscvSemantics::sw_s(triton::arch::Instruction& inst) {
2614 // M[x[rs1] + offset] := (x[rs2] & 0xffffffff)
2615 auto& src = inst.operands[0]; // rs2
2616 auto& dst = inst.operands[1]; // rs1 - base, offset - disp
2617
2618 /* Create symbolic operands and semantics */
2619 auto node = this->symbolicEngine->getOperandAst(inst, src);
2620 if (src.getBitSize() == 64) {
2621 node = this->astCtxt->extract(31, 0, node);
2622 }
2623
2624 /* Create symbolic expression */
2625 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SW operation - STORE access");
2626
2627 /* Spread taint */
2628 expr->isTainted = this->taintEngine->taintAssignment(dst, src);
2629
2630 /* Update the symbolic control flow */
2631 this->controlFlow_s(inst);
2632 }
2633
2634
2635 void riscvSemantics::xor_s(triton::arch::Instruction& inst) {
2636 auto& dst = inst.operands[0];
2637 auto& src1 = inst.operands[1];
2638 auto& src2 = inst.operands[2];
2639
2640 /* Create symbolic operands */
2641 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2642 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2643
2644 /* Create the semantics */
2645 auto node = this->astCtxt->bvxor(op1, op2);
2646
2647 /* Create symbolic expression */
2648 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "XOR operation");
2649
2650 /* Spread taint */
2651 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
2652
2653 /* Update the symbolic control flow */
2654 this->controlFlow_s(inst);
2655 }
2656
2657
2658 void riscvSemantics::xori_s(triton::arch::Instruction& inst) {
2659 auto& dst = inst.operands[0];
2660 auto& src1 = inst.operands[1];
2661
2662 /* Create symbolic operands */
2663 auto op1 = this->symbolicEngine->getOperandAst(inst, src1);
2664 auto node = this->astCtxt->bvnot(op1); // not pseudo instruction semantics
2665
2666 if (inst.operands.size() > 2) {
2667 auto& src2 = inst.operands[2];
2668 auto op2 = this->symbolicEngine->getOperandAst(inst, src2);
2669 node = this->astCtxt->bvxor(op1, op2); // xori semantics
2670 }
2671
2672 /* Create symbolic expression */
2673 auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "XORI operation");
2674
2675 /* Spread taint */
2676 expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1));
2677
2678 /* Update the symbolic control flow */
2679 this->controlFlow_s(inst);
2680 }
2681
2682 }; /* riscv namespace */
2683 }; /* arch namespace */
2684}; /* triton namespace */
triton::arch::Architecture
The abstract architecture class.
Definition architecture.hpp:45
triton::arch::Architecture::getRegister
TRITON_EXPORT const triton::arch::Register & getRegister(triton::arch::register_e id) const
Returns register from id.
Definition architecture.cpp:212
triton::arch::Architecture::getStackPointer
TRITON_EXPORT const triton::arch::Register & getStackPointer(void) const
Returns the stack pointer register.
Definition architecture.cpp:205
triton::arch::Architecture::getProgramCounter
TRITON_EXPORT const triton::arch::Register & getProgramCounter(void) const
Returns the program counter register.
Definition architecture.cpp:198
triton::arch::BitsVector::setBits
TRITON_EXPORT void setBits(triton::uint32 high, triton::uint32 low)
Sets the bits (high, low) position.
Definition bitsVector.cpp:72
triton::arch::Immediate
This class is used to represent an immediate.
Definition immediate.hpp:37
triton::arch::Instruction
This class is used to represent an instruction.
Definition instruction.hpp:48
triton::arch::Instruction::setConditionTaken
TRITON_EXPORT void setConditionTaken(bool flag)
Sets flag to define if the condition is taken or not.
Definition instruction.cpp:514
triton::arch::Instruction::getType
TRITON_EXPORT triton::uint32 getType(void) const
Returns the type of the instruction.
Definition instruction.cpp:152
triton::arch::Instruction::operands
std::vector< triton::arch::OperandWrapper > operands
A list of operands.
Definition instruction.hpp:122
triton::arch::Instruction::getDisassembly
TRITON_EXPORT std::string getDisassembly(void) const
Returns the disassembly of the instruction.
Definition instruction.cpp:129
triton::arch::Instruction::getNextAddress
TRITON_EXPORT triton::uint64 getNextAddress(void) const
Returns the next address of the instruction.
Definition instruction.cpp:119
triton::arch::MemoryAccess
This class is used to represent a memory access.
Definition memoryAccess.hpp:40
triton::arch::MemoryAccess::setDisplacement
TRITON_EXPORT void setDisplacement(const triton::arch::Immediate &displacement)
LEA - Sets the displacement operand.
Definition memoryAccess.cpp:163
triton::arch::MemoryAccess::setBaseRegister
TRITON_EXPORT void setBaseRegister(const triton::arch::Register &base)
LEA - Sets the base register operand.
Definition memoryAccess.cpp:153
triton::arch::OperandWrapper
This class is used as operand wrapper.
Definition operandWrapper.hpp:38
triton::arch::Register
This class is used when an instruction has a register operand.
Definition register.hpp:44
triton::arch::riscv::riscvSemantics::riscvSemantics
TRITON_EXPORT riscvSemantics(triton::arch::Architecture *architecture, triton::engines::symbolic::SymbolicEngine *symbolicEngine, triton::engines::taint::TaintEngine *taintEngine, const triton::modes::SharedModes &modes, const triton::ast::SharedAstContext &astCtxt)
Constructor.
Definition riscvSemantics.cpp:130
triton::arch::riscv::riscvSemantics::buildSemantics
TRITON_EXPORT triton::arch::exception_e buildSemantics(triton::arch::Instruction &inst)
Builds the semantics of the instruction. Returns triton::arch::NO_FAULT if succeed.
Definition riscvSemantics.cpp:152
triton::engines::symbolic::PathManager::pushPathConstraint
TRITON_EXPORT void pushPathConstraint(const triton::arch::Instruction &inst, const triton::engines::symbolic::SharedSymbolicExpression &expr)
Pushs constraints of a branch instruction to the path predicate.
Definition pathManager.cpp:155
triton::engines::symbolic::SymbolicEngine::createSymbolicRegisterExpression
TRITON_EXPORT const SharedSymbolicExpression & createSymbolicRegisterExpression(triton::arch::Instruction &inst, const triton::ast::SharedAbstractNode &node, const triton::arch::Register &reg, const std::string &comment="")
Returns the new symbolic register expression expression and links this expression to the instruction.
Definition symbolicEngine.cpp:1116
triton::engines::symbolic::SymbolicEngine::initLeaAst
TRITON_EXPORT void initLeaAst(triton::arch::MemoryAccess &mem, bool force=true)
Initializes the effective address of a memory access.
Definition symbolicEngine.cpp:1262
triton::engines::symbolic::SymbolicEngine::createSymbolicExpression
TRITON_EXPORT const SharedSymbolicExpression & createSymbolicExpression(triton::arch::Instruction &inst, const triton::ast::SharedAbstractNode &node, const triton::arch::OperandWrapper &dst, const std::string &comment="")
Returns the new symbolic expression and links this expression to the instruction.
Definition symbolicEngine.cpp:968
triton::engines::symbolic::SymbolicEngine::getOperandAst
TRITON_EXPORT triton::ast::SharedAbstractNode getOperandAst(const triton::arch::OperandWrapper &op)
Returns the AST corresponding to the operand.
Definition symbolicEngine.cpp:677
triton::engines::taint::TaintEngine::setTaint
TRITON_EXPORT bool setTaint(const triton::arch::OperandWrapper &op, bool flag)
Sets the flag (taint or untaint) to an abstract operand (Register or Memory).
Definition taintEngine.cpp:133
triton::engines::taint::TaintEngine::isTainted
TRITON_EXPORT bool isTainted(const triton::arch::OperandWrapper &op) const
Abstract taint verification. Returns true if the operand is tainted.
Definition taintEngine.cpp:107
triton::engines::taint::TaintEngine::taintUnion
TRITON_EXPORT bool taintUnion(const triton::arch::OperandWrapper &op1, const triton::arch::OperandWrapper &op2)
Abstract union tainting.
Definition taintEngine.cpp:207
triton::engines::taint::TaintEngine::setTaintRegister
TRITON_EXPORT bool setTaintRegister(const triton::arch::Register &reg, bool flag)
Sets the flag (taint or untaint) to a register.
Definition taintEngine.cpp:157
triton::engines::taint::TaintEngine::taintAssignment
TRITON_EXPORT bool taintAssignment(const triton::arch::OperandWrapper &op1, const triton::arch::OperandWrapper &op2)
Abstract assignment tainting.
Definition taintEngine.cpp:234
triton::exceptions::Semantics
The exception class used by all semantics.
Definition exceptions.hpp:377
triton::arch::exception_e
exception_e
Definition archEnums.hpp:59
triton::arch::OP_REG
@ OP_REG
Definition archEnums.hpp:55
triton::arch::NO_FAULT
@ NO_FAULT
Definition archEnums.hpp:60
triton::arch::FAULT_UD
@ FAULT_UD
Definition archEnums.hpp:63
triton::ast::SharedAstContext
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition ast.hpp:65
triton::bitsize::dword
constexpr triton::uint32 dword
dword size in bit
Definition cpuSize.hpp:64
triton::bitsize::qword
constexpr triton::uint32 qword
qword size in bit
Definition cpuSize.hpp:66
triton::modes::SharedModes
std::shared_ptr< triton::modes::Modes > SharedModes
Shared Modes.
Definition modes.hpp:66
triton::engines::taint::UNTAINTED
const bool UNTAINTED
Defines an untainted item.
Definition taintEngine.hpp:49
triton
The Triton namespace.
Definition architecture.cpp:27
Generated by doxygen 1.10.0