libTriton  version 1.0 build 1549
symbolicEngine.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 <cstring>
9#include <new>
10#include <set>
11
12#include <triton/exceptions.hpp>
13#include <triton/coreUtils.hpp>
15#include <triton/astContext.hpp>
16
17
18
19namespace triton {
20 namespace engines {
21 namespace symbolic {
22
24 const triton::modes::SharedModes& modes,
25 const triton::ast::SharedAstContext& astCtxt,
27 : triton::engines::symbolic::SymbolicSimplification(callbacks),
28 triton::engines::symbolic::PathManager(modes, astCtxt),
29 astCtxt(astCtxt),
30 modes(modes) {
31
32 if (architecture == nullptr) {
33 throw triton::exceptions::SymbolicEngine("SymbolicEngine::SymbolicEngine(): The architecture pointer must be valid.");
34 }
35
36 this->architecture = architecture;
37 this->callbacks = callbacks;
38 this->numberOfRegisters = this->architecture->numberOfRegisters();
39 this->uniqueSymExprId = 0;
40 this->uniqueSymVarId = 0;
41
42 this->symbolicReg.resize(this->numberOfRegisters);
43 }
44
45
47 : triton::engines::symbolic::SymbolicSimplification(other),
48 triton::engines::symbolic::PathManager(other),
49 astCtxt(other.astCtxt),
50 modes(other.modes) {
51
53 this->architecture = other.architecture;
54 this->callbacks = other.callbacks;
55 this->memoryReference = other.memoryReference;
58 this->symbolicReg = other.symbolicReg;
60 this->uniqueSymExprId = other.uniqueSymExprId;
61 this->uniqueSymVarId = other.uniqueSymVarId;
62 }
63
64
66 /* See #828: Release ownership before calling container destructor */
67 this->memoryReference.clear();
68 this->symbolicReg.clear();
69 }
70
71
75
77 this->architecture = other.architecture;
78 this->astCtxt = other.astCtxt;
79 this->callbacks = other.callbacks;
80 this->memoryReference = other.memoryReference;
81 this->modes = other.modes;
84 this->symbolicReg = other.symbolicReg;
86 this->uniqueSymExprId = other.uniqueSymExprId;
87 this->uniqueSymVarId = other.uniqueSymVarId;
88
89 return *this;
90 }
91
92
93 /*
94 * Concretize a register. If the register is setup as nullptr, the next assignment
95 * will be over the concretization. This method must be called before symbolic
96 * processing.
97 */
99 triton::arch::register_e parentId = reg.getParent();
100
101 if (this->architecture->isRegisterValid(parentId)) {
102 this->symbolicReg[parentId] = nullptr;
103 }
104 }
105
106
107 /* Same as concretizeRegister but with all registers */
109 for (triton::uint32 i = 0; i < this->numberOfRegisters; i++) {
110 this->symbolicReg[i] = nullptr;
111 }
112 }
113
114
115 /*
116 * Concretize a memory. If the memory is not found into the map, the next
117 * assignment will be over the concretization. This method must be called
118 * before symbolic processing.
119 */
121 triton::uint64 addr = mem.getAddress();
122 triton::uint32 size = mem.getSize();
123
124 for (triton::uint32 index = 0; index < size; index++) {
125 this->concretizeMemory(addr+index);
126 }
127 }
128
129
130 /*
131 * Concretize a memory. If the memory is not found into the map, the next
132 * assignment will be over the concretization. This method must be called
133 * before symbolic processing.
134 */
136 this->memoryReference.erase(addr);
137 this->removeAlignedMemory(addr, triton::size::byte);
138 }
139
140
141 /* Same as concretizeMemory but with all address memory */
143 this->memoryReference.clear();
144 this->alignedMemoryReference.clear();
145 }
146
147
148 /* Gets an aligned entry. */
149 const SharedSymbolicExpression& SymbolicEngine::getAlignedMemory(triton::uint64 address, triton::uint32 size) {
150 return this->alignedMemoryReference[std::make_pair(address, size)];
151 }
152
153
154 /* Checks if the aligned memory is recored. */
155 bool SymbolicEngine::isAlignedMemory(triton::uint64 address, triton::uint32 size) {
156 if (this->alignedMemoryReference.find(std::make_pair(address, size)) != this->alignedMemoryReference.end()) {
157 return true;
158 }
159 return false;
160 }
161
162
163 /* Adds an aligned memory */
164 void SymbolicEngine::addAlignedMemory(triton::uint64 address, triton::uint32 size, const SharedSymbolicExpression& expr) {
165 this->removeAlignedMemory(address, size);
166 if (!(this->modes->isModeEnabled(triton::modes::ONLY_ON_SYMBOLIZED) && expr->getAst()->isSymbolized() == false)) {
167 this->alignedMemoryReference[std::make_pair(address, size)] = expr;
168 }
169 }
170
171
172 /* Removes an aligned memory */
173 void SymbolicEngine::removeAlignedMemory(triton::uint64 address, triton::uint32 size) {
174 /*
175 * Avoid accessing the alignedMemoryReference array when empty. This usually happens when
176 * you initialize the symbolic engine and concretize whole sections of an executable using
177 * setConcreteMemoryValue. No symbolic memory has been created yet but this function will
178 * still try to rougly erase (size * 7) elements.
179 */
180 if (this->alignedMemoryReference.empty())
181 return;
182
183 /* Remove overloaded positive ranges */
184 for (triton::uint32 index = 0; index < size; index++) {
185 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::byte));
186 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::word));
187 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dword));
188 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qword));
189 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::fword));
190 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqword));
191 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qqword));
192 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqqword));
193 }
194
195 /* Remove overloaded negative ranges */
196 for (triton::uint32 index = 1; index < triton::size::dqqword; index++) {
197 if (index < triton::size::word) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::word));
198 if (index < triton::size::dword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dword));
199 if (index < triton::size::qword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qword));
200 if (index < triton::size::fword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::fword));
201 if (index < triton::size::dqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dqword));
202 if (index < triton::size::qqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qqword));
203 if (index < triton::size::dqqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dqqword));
204 }
205 }
206
207
208 /* Returns the reference memory if it's referenced otherwise returns nullptr */
210 auto it = this->memoryReference.find(addr);
211 if (it != this->memoryReference.end()) {
212 return it->second;
213 }
214 return nullptr;
215 }
216
217
218 /* Returns the symbolic variable otherwise raises an exception */
220 auto it = this->symbolicVariables.find(symVarId);
221 if (it == this->symbolicVariables.end()) {
222 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred symbolic variable.");
223 }
224
225 if (auto node = it->second.lock()) {
226 return node;
227 }
228
229 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): This symbolic variable is dead.");
230 }
231
232
233 /* Returns the symbolic variable otherwise returns nullptr */
235 /*
236 * FIXME: 1) When there is a ton of symvar, this loop takes a while to go through.
237 * What about adding two maps {id:symvar} and {string:symvar}? See #648.
238 *
239 * 2) If we are looking for alias, we return the first occurrence. It's not
240 * ideal if we have multiple same aliases.
241 */
242 for (auto& sv: this->symbolicVariables) {
243 if (auto symVar = sv.second.lock()) {
244 if (symVar->getName() == name || symVar->getAlias() == name) {
245 return symVar;
246 }
247 }
248 }
249 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred or dead symbolic variable.");
250 }
251
252
253 /* Returns all symbolic variables */
254 std::map<triton::usize, SharedSymbolicVariable> SymbolicEngine::getSymbolicVariables(void) const {
255 // Copy and clean up dead weak ref
256 std::map<triton::usize, SharedSymbolicVariable> ret;
257 std::vector<triton::usize> toRemove;
258
259 for (auto& kv : this->symbolicVariables) {
260 if (auto sp = kv.second.lock()) {
261 ret[kv.first] = sp;
262 } else {
263 toRemove.push_back(kv.first);
264 }
265 }
266
267 for (triton::usize id : toRemove) {
268 this->symbolicVariables.erase(id);
269 }
270
271 return ret;
272 }
273
274
275 void SymbolicEngine::setImplicitReadRegisterFromEffectiveAddress(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) {
276 /* Set implicit read of the segment register (LEA) */
277 if (this->architecture->isRegisterValid(mem.getConstSegmentRegister())) {
278 (void)this->getRegisterAst(inst, mem.getConstSegmentRegister());
279 }
280
281 /* Set implicit read of the base register (LEA) */
282 if (this->architecture->isRegisterValid(mem.getConstBaseRegister())) {
283 (void)this->getRegisterAst(inst, mem.getConstBaseRegister());
284 }
285
286 /* Set implicit read of the index register (LEA) */
287 if (this->architecture->isRegisterValid(mem.getConstIndexRegister())) {
288 (void)this->getRegisterAst(inst, mem.getConstIndexRegister());
289 }
290 }
291
292
293 const SharedSymbolicExpression& SymbolicEngine::addSymbolicExpressions(triton::arch::Instruction& inst, triton::usize id) const {
294 /* See #1002: There may be multiple new symbolic expressions when AST_OPTIMIZATIONS are on */
295 for (triton::usize i = id; i != this->uniqueSymExprId; ++i) {
296 if (this->isSymbolicExpressionExists(i)) {
298 }
299 }
300 return inst.symbolicExpressions.back();
301 }
302
303
304 /* Returns the shared symbolic expression corresponding to the register */
306 triton::arch::register_e parentId = reg.getParent();
307
308 if (this->architecture->isRegisterValid(parentId)) {
309 return this->symbolicReg.at(parentId);
310 }
311
312 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicRegister(): Invalid Register");
313 }
314
315
316 /* Returns the symbolic address value */
319 return static_cast<triton::uint8>(this->getSymbolicMemoryValue(mem));
320 }
321
322
323 /* Returns the symbolic memory value */
325 const triton::ast::SharedAbstractNode& node = this->getMemoryAst(mem);
326 return node->evaluate();
327 }
328
329
330 /* Returns the symbolic values of a memory area */
332 std::vector<triton::uint8> area;
333
334 area.reserve(size);
335 for (triton::usize index = 0; index < size; index++) {
336 area.push_back(this->getSymbolicMemoryValue(baseAddr + index));
337 }
338
339 return area;
340 }
341
342
343 /* Returns the symbolic register value */
345 return this->getRegisterAst(reg)->evaluate();
346 }
347
348
349 /* Creates a new symbolic expression */
350 /* Get an unique id.
351 * Mainly used when a new symbolic expression is created */
352 triton::usize SymbolicEngine::getUniqueSymExprId(void) {
353 return this->uniqueSymExprId++;
354 }
355
356
357 /* Creates a new symbolic variable */
358 /* Get an unique id.
359 * Mainly used when a new symbolic variable is created */
360 triton::usize SymbolicEngine::getUniqueSymVarId(void) {
361 return this->uniqueSymVarId++;
362 }
363
364
365 /* Creates a new symbolic expression with comment */
367 if (this->modes->isModeEnabled(triton::modes::AST_OPTIMIZATIONS)) {
368 /*
369 * Create volatile expression for extended part to avoid long
370 * formulas while printing. Long formulas are introduced by
371 * optimizations of AstContext::concat and AstContext::extract
372 */
373 if (node->getType() == triton::ast::ZX_NODE || node->getType() == triton::ast::SX_NODE) {
374 auto n = node->getChildren()[1];
375 if (n->getType() != triton::ast::REFERENCE_NODE && n->getType() != triton::ast::VARIABLE_NODE) {
376 /* FIXME: We lost the origin if we create a new symbolic expression without returning it */
377 auto e = this->newSymbolicExpression(n, VOLATILE_EXPRESSION, "Extended part - " + comment);
378 node->setChild(1, this->astCtxt->reference(e));
379 }
380 }
381 }
382
383 /* Each symbolic expression must have an unique id */
384 triton::usize id = this->getUniqueSymExprId();
385
386 /* Performes transformation if there are rules recorded */
387 const triton::ast::SharedAbstractNode& snode = this->simplify(node);
388
389 /* Allocates the new shared symbolic expression */
390 SharedSymbolicExpression expr = std::make_shared<SymbolicExpression>(snode, id, type, comment);
391 if (expr == nullptr) {
392 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicExpression(): not enough memory");
393 }
394
395 /* Save and returns the new shared symbolic expression */
396 this->symbolicExpressions[id] = expr;
397 return expr;
398 }
399
400
401 /* Removes the symbolic expression corresponding to the id */
403 if (this->symbolicExpressions.find(expr->getId()) != this->symbolicExpressions.end()) {
404 /* Concretize memory */
405 if (expr->getType() == MEMORY_EXPRESSION) {
406 const auto& mem = expr->getOriginMemory();
407 this->concretizeMemory(mem);
408 }
409
410 /* Concretize register */
411 else if (expr->getType() == REGISTER_EXPRESSION) {
412 const auto& reg = expr->getOriginRegister();
413 this->concretizeRegister(reg);
414 }
415
416 /* Delete and remove the pointer */
417 this->symbolicExpressions.erase(expr->getId());
418 }
419 }
420
421
422 /* Gets the shared symbolic expression from a symbolic id */
424 auto it = this->symbolicExpressions.find(symExprId);
425 if (it == this->symbolicExpressions.end()) {
426 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression id not found");
427 }
428
429 if (auto sp = it->second.lock()) {
430 return sp;
431 }
432
433 this->symbolicExpressions.erase(symExprId);
434 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression is not available anymore");
435 }
436
437
438 /* Returns all symbolic expressions */
439 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::getSymbolicExpressions(void) const {
440 // Copy and clean up dead weak ref
441 std::unordered_map<triton::usize, SharedSymbolicExpression> ret;
442 std::vector<triton::usize> toRemove;
443
444 for (auto& kv : this->symbolicExpressions) {
445 if (auto sp = kv.second.lock()) {
446 ret[kv.first] = sp;
447 } else {
448 toRemove.push_back(kv.first);
449 }
450 }
451
452 for (auto id : toRemove)
453 this->symbolicExpressions.erase(id);
454
455 return ret;
456 }
457
458
459 /* Slices all expressions from a given one */
460 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::sliceExpressions(const SharedSymbolicExpression& expr) {
461 std::unordered_map<triton::usize, SharedSymbolicExpression> exprs;
462
463 if (expr == nullptr) {
464 throw triton::exceptions::SymbolicEngine("SymbolicEngine::sliceExpressions(): expr cannot be null.");
465 }
466
467 exprs[expr->getId()] = expr;
468
469 auto worklist = triton::ast::childrenExtraction(expr->getAst(), true /* unroll */, false /* revert */);
470 for (auto&& n : worklist) {
471 if (n->getType() == triton::ast::REFERENCE_NODE) {
472 auto expr = reinterpret_cast<triton::ast::ReferenceNode*>(n.get())->getSymbolicExpression();
473 auto eid = expr->getId();
474 exprs[eid] = expr;
475 }
476 }
477
478 return exprs;
479 }
480
481
482 /* Returns a list which contains all tainted expressions */
483 std::vector<SharedSymbolicExpression> SymbolicEngine::getTaintedSymbolicExpressions(void) const {
484 std::vector<SharedSymbolicExpression> taintedExprs;
485 std::vector<triton::usize> invalidSymExpr;
486
487 for (auto it = this->symbolicExpressions.begin(); it != this->symbolicExpressions.end(); it++) {
488 if (auto sp = it->second.lock()) {
489 if (sp->isTainted) {
490 taintedExprs.push_back(sp);
491 }
492 } else {
493 invalidSymExpr.push_back(it->first);
494 }
495 }
496
497 for (auto id : invalidSymExpr) {
498 this->symbolicExpressions.erase(id);
499 }
500
501 return taintedExprs;
502 }
503
504
505 /* Returns the map of symbolic registers defined */
506 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> SymbolicEngine::getSymbolicRegisters(void) const {
507 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> ret;
508
509 for (triton::uint32 it = 0; it < this->numberOfRegisters; it++) {
510 if (this->symbolicReg[it] != nullptr) {
511 ret[triton::arch::register_e(it)] = this->symbolicReg[it];
512 }
513 }
514
515 return ret;
516 }
517
518
519 /* Returns the map of symbolic memory defined */
520 const std::unordered_map<triton::uint64, SharedSymbolicExpression>& SymbolicEngine::getSymbolicMemory(void) const {
521 return this->memoryReference;
522 }
523
524
525 /*
526 * Converts an expression id to a symbolic variable.
527 * e.g:
528 * #43 = (_ bv10 8)
529 * symbolizeExpression(43, 8)
530 * #43 = SymVar_4
531 */
533 const SharedSymbolicExpression& expression = this->getSymbolicExpression(exprId);
534 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(UNDEFINED_VARIABLE, 0, symVarSize, symVarAlias);
535 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->variable(symVar);
536
537 if (expression->getAst()) {
538 this->setConcreteVariableValue(symVar, expression->getAst()->evaluate());
539 }
540
541 expression->setAst(tmp);
542
543 return symVar;
544 }
545
546
547 /* Symbolize a memory area to 8-bits symbolic variables */
549 for (triton::usize i = 0; i != size; i++) {
551 }
552 }
553
554
555 /* The memory size is used to define the symbolic variable's size. */
557 triton::uint64 memAddr = mem.getAddress();
558 triton::uint32 symVarSize = mem.getSize();
559 triton::uint512 cv = this->architecture->getConcreteMemoryValue(mem);
560
561 /* First we create a symbolic variable */
562 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(MEMORY_VARIABLE, memAddr, symVarSize * bitsize::byte, symVarAlias);
563
564 /* Create the AST node */
565 const triton::ast::SharedAbstractNode& symVarNode = this->astCtxt->variable(symVar);
566
567 /* Setup the concrete value to the symbolic variable */
568 this->setConcreteVariableValue(symVar, cv);
569
570 /* Record the aligned symbolic variable for a symbolic optimization */
571 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
572 const SharedSymbolicExpression& se = this->newSymbolicExpression(symVarNode, MEMORY_EXPRESSION, "aligned Byte reference");
573 se->setOriginMemory(mem);
574 this->addAlignedMemory(memAddr, symVarSize, se);
575 }
576
577 /* Split expression in bytes */
578 for (triton::sint32 index = symVarSize-1; index >= 0; index--) {
579 triton::uint32 high = ((bitsize::byte * (index + 1)) - 1);
580 triton::uint32 low = ((bitsize::byte * (index + 1)) - bitsize::byte);
581
582 /* Isolate the good part of the symbolic variable */
583 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, symVarNode);
584
585 /* Create a new symbolic expression containing the symbolic variable */
586 const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
587 se->setOriginMemory(triton::arch::MemoryAccess(memAddr+index, triton::size::byte));
588
589 /* Assign the symbolic expression to the memory cell */
590 this->addMemoryReference(memAddr+index, se);
591 }
592
593 return symVar;
594 }
595
596
598 const triton::arch::Register& parent = this->architecture->getRegister(reg.getParent());
599 triton::uint32 symVarSize = reg.getBitSize();
600 triton::uint512 cv = this->architecture->getConcreteRegisterValue(reg);
601
602 if (!this->architecture->isRegisterValid(parent.getId()))
603 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): Invalid register id");
604
605 if (reg.isMutable() == false)
606 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): This register is immutable");
607
608 /* Create the symbolic variable */
609 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(REGISTER_VARIABLE, reg.getId(), symVarSize, symVarAlias);
610
611 /* Create the AST node */
612 const triton::ast::SharedAbstractNode& tmp = this->insertSubRegisterInParent(reg, this->astCtxt->variable(symVar), false);
613
614 /* Setup the concrete value to the symbolic variable */
615 this->setConcreteVariableValue(symVar, cv);
616
617 /* Create a new symbolic expression containing the symbolic variable */
619
620 /* Assign the symbolic expression to the register */
621 this->assignSymbolicExpressionToRegister(se, parent);
622
623 return symVar;
624 }
625
626
627 /* Adds a new symbolic variable */
629 triton::usize uniqueId = this->getUniqueSymVarId();
630
631 SharedSymbolicVariable symVar = std::make_shared<SymbolicVariable>(type, origin, uniqueId, size, alias);
632 if (symVar == nullptr) {
633 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicVariable(): Cannot allocate a new symbolic variable");
634 }
635
636 this->symbolicVariables[uniqueId] = symVar;
637 return symVar;
638 }
639
640
641 /* Returns the AST corresponding to the operand. */
643 switch (op.getType()) {
645 case triton::arch::OP_MEM: return this->getMemoryAst(op.getConstMemory());
647 default:
648 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
649 }
650 }
651
652
653 /* Returns the AST corresponding to the operand. */
655 switch (op.getType()) {
656 case triton::arch::OP_IMM: return this->getImmediateAst(inst, op.getConstImmediate());
657 case triton::arch::OP_MEM: return this->getMemoryAst(inst, op.getConstMemory());
658 case triton::arch::OP_REG: return this->getRegisterAst(inst, op.getConstRegister());
659 default:
660 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
661 }
662 }
663
664
666 auto imm = shift.getShiftImmediate();
667 auto reg = shift.getShiftRegister();
668
669 switch (shift.getShiftType()) {
671 return this->astCtxt->bvashr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
672
674 return this->astCtxt->bvshl(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
675
677 return this->astCtxt->bvlshr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
678
680 return this->astCtxt->bvror(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
681
682 case triton::arch::arm::ID_SHIFT_RRX: /* Arm32 only. */
683 return this->astCtxt->extract(
684 node->getBitvectorSize(),
685 1,
686 this->astCtxt->bvror(
687 this->astCtxt->concat(
688 node,
689 this->getRegisterAst(this->architecture->getRegister(triton::arch::ID_REG_ARM32_C))
690 ),
691 1
692 )
693 );
694
695 case triton::arch::arm::ID_SHIFT_ASR_REG: /* Arm32 only. */
696 return this->astCtxt->bvashr(
697 node,
698 this->astCtxt->zx(
699 this->architecture->getRegister(reg).getBitSize() - 8,
700 this->astCtxt->extract(
701 7,
702 0,
703 this->getRegisterAst(this->architecture->getRegister(reg))
704 )
705 )
706 );
707
708 case triton::arch::arm::ID_SHIFT_LSL_REG: /* Arm32 only. */
709 return this->astCtxt->bvshl(
710 node,
711 this->astCtxt->zx(
712 this->architecture->getRegister(reg).getBitSize() - 8,
713 this->astCtxt->extract(
714 7,
715 0,
716 this->getRegisterAst(this->architecture->getRegister(reg))
717 )
718 )
719 );
720
721 case triton::arch::arm::ID_SHIFT_LSR_REG: /* Arm32 only. */
722 return this->astCtxt->bvlshr(
723 node,
724 this->astCtxt->zx(
725 this->architecture->getRegister(reg).getBitSize() - 8,
726 this->astCtxt->extract(
727 7,
728 0,
729 this->getRegisterAst(this->architecture->getRegister(reg))
730 )
731 )
732 );
733
734 case triton::arch::arm::ID_SHIFT_ROR_REG: /* Arm32 only. */
735 return this->astCtxt->bvror(
736 node,
737 this->astCtxt->zx(
738 this->architecture->getRegister(reg).getBitSize() - 8,
739 this->astCtxt->extract(
740 7,
741 0,
742 this->getRegisterAst(this->architecture->getRegister(reg))
743 )
744 )
745 );
746
748 /* NOTE: Capstone considers this as a viable shift operand but
749 * according to the ARM manual this is not possible.
750 */
751 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): ID_SHIFT_RRX_REG is an invalid shift operand.");
752
753 default:
754 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): Invalid shift operand.");
755 }
756 }
757
758
760 triton::uint32 size = extend.getExtendSize();
761
762 switch (extend.getExtendType()) {
764 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
765
767 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
768
770 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
771
773 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
774
776 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
777
779 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
780
782 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
783
785 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
786
787 default:
788 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getExtendAst(): Invalid extend operand.");
789 }
790 }
791
792
793 /* Returns the AST corresponding to the immediate */
795 triton::ast::SharedAbstractNode node = this->astCtxt->bv(imm.getValue(), imm.getBitSize());
796
797 /* Shift AST if it's a shift operand */
799 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(imm), node);
800 }
801
802 return node;
803 }
804
805
806 /* Returns the AST corresponding to the immediate and defines the immediate as input of the instruction */
809 inst.setReadImmediate(imm, node);
810 return node;
811 }
812
813
814 /* Returns the AST corresponding to the memory */
816 std::vector<triton::ast::SharedAbstractNode> opVec;
817
819 triton::uint64 address = mem.getAddress();
820 triton::uint32 size = mem.getSize();
821 triton::uint8 concreteValue[triton::size::dqqword] = {0};
822 triton::uint512 value = this->architecture->getConcreteMemoryValue(mem);
823
824 triton::utils::fromUintToBuffer(value, concreteValue);
825
826 /*
827 * Symbolic optimization
828 * If the memory access is aligned, don't split the memory.
829 */
830 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY) && this->isAlignedMemory(address, size)) {
831 return this->getAlignedMemory(address, size)->getAst();
832 }
833
834 /* If the memory access is 1 byte long, just return the appropriate 8-bit vector */
835 if (size == 1) {
836 const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address);
837 if (symMem) return this->astCtxt->reference(symMem);
838 else return this->astCtxt->bv(concreteValue[size - 1], bitsize::byte);
839 }
840
841 /* If the memory access is more than 1 byte long, concatenate each memory cell */
842 opVec.reserve(size);
843 while (size) {
844 const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address + size - 1);
845 if (symMem) opVec.push_back(this->astCtxt->reference(symMem));
846 else opVec.push_back(this->astCtxt->bv(concreteValue[size - 1], bitsize::byte));
847 size--;
848 }
849 return this->astCtxt->concat(opVec);
850 }
851
852
853 /* Returns the AST corresponding to the memory and defines the memory as input of the instruction */
856
857 /* Set load access */
858 inst.setLoadAccess(mem, node);
859
860 /* Set implicit read of the base and index registers from an effective address */
861 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
862
863 return node;
864 }
865
866
867 /* Returns the AST corresponding to the register */
869 triton::ast::SharedAbstractNode node = nullptr;
870 triton::uint32 bvSize = reg.getBitSize();
871 triton::uint32 high = reg.getHigh();
872 triton::uint32 low = reg.getLow();
873 triton::uint512 value = this->architecture->getConcreteRegisterValue(reg);
874
875 /* Check if the register is already symbolic */
876 const SharedSymbolicExpression& symReg = this->getSymbolicRegister(reg);
877 if (symReg) node = this->astCtxt->extract(high, low, this->astCtxt->reference(symReg));
878 else node = this->astCtxt->bv(value, bvSize);
879
880 /* extend AST if it's a extend operand (mainly used for AArch64) */
882 return this->getExtendAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
883 }
884
885 /* Shift AST if it's a shift operand (mainly used for Arm) */
887 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
888 }
889
890 return node;
891 }
892
893
894 /* Returns the AST corresponding to the register and defines the register as input of the instruction */
897 inst.setReadRegister(reg, node);
898 return node;
899 }
900
901
902 /* Returns the new symbolic abstract expression and links this expression to the instruction. */
904 switch (dst.getType()) {
905 case triton::arch::OP_MEM: return this->createSymbolicMemoryExpression(inst, node, dst.getConstMemory(), comment);
906 case triton::arch::OP_REG: return this->createSymbolicRegisterExpression(inst, node, dst.getConstRegister(), comment);
907 default:
908 throw triton::exceptions::SymbolicEngine("SymbolicEngine::createSymbolicExpression(): Invalid operand.");
909 }
910 }
911
912
913 /* Returns the new symbolic memory expression */
915 std::vector<triton::ast::SharedAbstractNode> ret;
917 SharedSymbolicExpression se = nullptr;
918 triton::uint64 address = mem.getAddress();
919 triton::uint32 writeSize = mem.getSize();
921
922 /* Record the aligned memory for a symbolic optimization */
923 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
924 const SharedSymbolicExpression& aligned = this->newSymbolicExpression(node, MEMORY_EXPRESSION, "Aligned Byte reference - " + comment);
925 this->addAlignedMemory(address, writeSize, aligned);
926 }
927
928 /*
929 * As the x86's memory can be accessed without alignment, each byte of the
930 * memory must be assigned to an unique reference.
931 */
932 ret.reserve(mem.getSize());
933 while (writeSize) {
934 triton::uint32 high = ((writeSize * bitsize::byte) - 1);
935 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte);
936 /* Extract each byte of the memory */
937 tmp = this->astCtxt->extract(high, low, node);
938 /* Assign each byte to a new symbolic expression */
939 se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference - " + comment);
940 /* Set the origin of the symbolic expression */
941 se->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
942 /* ret is the for the final expression */
943 ret.push_back(tmp);
944 /* Assign memory with little endian */
945 this->addMemoryReference((address + writeSize) - 1, se);
946 /* continue */
947 writeSize--;
948 }
949
950 /* Set implicit read of the base and index registers from an effective address */
951 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
952
953 /* Set explicit write of the memory access */
954 inst.setStoreAccess(mem, node);
955
956 /* If there is only one reference, we return the symbolic expression */
957 if (ret.size() == 1) {
958 /* Synchronize the concrete state */
959 this->architecture->setConcreteMemoryValue(mem, tmp->evaluate());
960 return this->addSymbolicExpressions(inst, id);
961 }
962
963 /* Otherwise, we return the concatenation of all symbolic expressions */
964 tmp = this->astCtxt->concat(ret);
965
966 /* Synchronize the concrete state */
967 this->architecture->setConcreteMemoryValue(mem, tmp->evaluate());
968
969 se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Temporary concatenation reference - " + comment);
970 se->setOriginMemory(triton::arch::MemoryAccess(address, mem.getSize()));
971
972 return this->addSymbolicExpressions(inst, id);
973 }
974
975
976 /* Returns the parent AST after inserting the subregister (node) in its AST. */
977 triton::ast::SharedAbstractNode SymbolicEngine::insertSubRegisterInParent(const triton::arch::Register& reg, const triton::ast::SharedAbstractNode& node, bool zxForAssign) {
978 const triton::arch::Register& parentReg = this->architecture->getParentRegister(reg);
979
980 /* If it's a flag register, there is nothing to do with sub register */
981 if (this->architecture->isFlag(reg)) {
982 return node;
983 }
984
985 switch (reg.getSize()) {
986 /* ----------------------------------------------------------------*/
987 case triton::size::byte: {
988 const auto& origReg = this->getRegisterAst(parentReg);
989 /*
990 * Mainly used for x86
991 * r[........xxxxxxxx]
992 */
993 if (reg.getLow() == 0) {
994 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::byte, origReg);
995 return this->astCtxt->concat(keep, node);
996 }
997 /*
998 * Mainly used for x86
999 * r[xxxxxxxx........]
1000 */
1001 else {
1002 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg);
1003 return this->astCtxt->concat(keep, this->astCtxt->concat(node, this->astCtxt->extract((bitsize::byte - 1), 0, origReg)));
1004 }
1005 }
1006
1007 /* ----------------------------------------------------------------*/
1008 case triton::size::word: {
1009 const auto& origReg = this->getRegisterAst(parentReg);
1010 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg), node);
1011 }
1012
1013 /* ----------------------------------------------------------------*/
1019 case triton::size::dqqword: {
1020 if (zxForAssign == false) {
1021 if (parentReg.getBitSize() > reg.getBitSize()) {
1022 const auto& origReg = this->getRegisterAst(parentReg);
1023 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), reg.getHigh() + 1, origReg), node);
1024 }
1025 else {
1026 return node;
1027 }
1028 }
1029 /* zxForAssign == true */
1030 else {
1031 return this->astCtxt->zx(parentReg.getBitSize() - node->getBitvectorSize(), node);
1032 }
1033 }
1034 /* ----------------------------------------------------------------*/
1035 }
1036
1037 throw triton::exceptions::SymbolicEngine("SymbolicEngine::insertSubRegisterInParent(): Invalid register size.");
1038 }
1039
1040
1041 /* Returns the new symbolic register expression */
1043 triton::usize id = this->uniqueSymExprId;
1044 SharedSymbolicExpression se = nullptr;
1045
1046 se = this->newSymbolicExpression(this->insertSubRegisterInParent(reg, node), REGISTER_EXPRESSION, comment);
1047 this->assignSymbolicExpressionToRegister(se, this->architecture->getParentRegister(reg));
1048
1049 inst.setWrittenRegister(reg, node);
1050 return this->addSymbolicExpressions(inst, id);
1051 }
1052
1053
1054 /* Returns the new symbolic volatile expression */
1056 triton::usize id = this->uniqueSymExprId;
1057 const SharedSymbolicExpression& se = this->newSymbolicExpression(node, VOLATILE_EXPRESSION, comment);
1058 return this->addSymbolicExpressions(inst, id);
1059 }
1060
1061
1062 /* Adds and assign a new memory reference */
1063 inline void SymbolicEngine::addMemoryReference(triton::uint64 mem, const SharedSymbolicExpression& expr) {
1064 this->memoryReference[mem] = expr;
1065 }
1066
1067
1068 /* Assigns a symbolic expression to a register */
1070 const triton::ast::SharedAbstractNode& node = se->getAst();
1071 triton::uint32 id = reg.getParent();
1072
1073 /* We can assign an expression only on parent registers */
1074 if (reg.getId() != id) {
1075 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): We can assign an expression only on parent registers.");
1076 }
1077
1078 /* Check if the size of the symbolic expression is equal to the target register */
1079 if (node->getBitvectorSize() != reg.getBitSize()) {
1080 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): The size of the symbolic expression is not equal to the target register.");
1081 }
1082
1083 se->setType(REGISTER_EXPRESSION);
1084 se->setOriginRegister(reg);
1085
1086 if (reg.isMutable()) {
1087 /* Assign if this register is mutable */
1088 this->symbolicReg[id] = se;
1089 /* Synchronize the concrete state */
1090 this->architecture->setConcreteRegisterValue(reg, node->evaluate());
1091 }
1092 }
1093
1094
1095 /* Assigns a symbolic expression to a memory */
1097 const triton::ast::SharedAbstractNode& node = se->getAst();
1098 triton::uint64 address = mem.getAddress();
1099 triton::uint32 writeSize = mem.getSize();
1100
1101 /* Check if the size of the symbolic expression is equal to the memory access */
1102 if (node->getBitvectorSize() != mem.getBitSize()) {
1103 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToMemory(): The size of the symbolic expression is not equal to the memory access.");
1104 }
1105
1106 /* Record the aligned memory for a symbolic optimization */
1107 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
1108 this->addAlignedMemory(address, writeSize, se);
1109 }
1110
1111 /*
1112 * As the x86's memory can be accessed without alignment, each byte of the
1113 * memory must be assigned to an unique reference.
1114 */
1115 while (writeSize) {
1116 triton::uint32 high = ((writeSize * bitsize::byte) - 1);
1117 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte);
1118 /* Extract each byte of the memory */
1119 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, node);
1120 /* For each byte create a new symbolic expression */
1121 const SharedSymbolicExpression& byteRef = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
1122 /* Set the origin of the symbolic expression */
1123 byteRef->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
1124 /* Assign memory with little endian */
1125 this->addMemoryReference((address + writeSize) - 1, byteRef);
1126 /* continue */
1127 writeSize--;
1128 }
1129
1130 /* Synchronize the concrete state */
1131 this->architecture->setConcreteMemoryValue(mem, node->evaluate());
1132 }
1133
1134
1135 /* Returns true if the symbolic expression ID exists */
1137 auto it = this->symbolicExpressions.find(symExprId);
1138
1139 if (it != this->symbolicExpressions.end()) {
1140 return (it->second.use_count() > 0);
1141 }
1142
1143 return false;
1144 }
1145
1146
1147 /* Returns true if memory cell expressions contain symbolic variables. */
1149 triton::uint64 addr = mem.getAddress();
1150 triton::uint32 size = mem.getSize();
1151
1152 return this->isMemorySymbolized(addr, size);
1153 }
1154
1155
1156 /* Returns true if memory cell expressions contain symbolic variables. */
1158 for (triton::uint32 i = 0; i < size; i++) {
1159 const SharedSymbolicExpression& expr = this->getSymbolicMemory(addr + i);
1160 if (expr && expr->isSymbolized()) {
1161 return true;
1162 }
1163 }
1164 return false;
1165 }
1166
1167
1168 /* Returns true if the register expression contains a symbolic variable. */
1170 const SharedSymbolicExpression& expr = this->getSymbolicRegister(reg);
1171 if (expr) {
1172 return expr->isSymbolized();
1173 }
1174 return false;
1175 }
1176
1177
1178 /* Initializes the memory access AST (LOAD and STORE) */
1180 if (mem.getBitSize() >= bitsize::byte) {
1181 const triton::arch::Register& base = mem.getConstBaseRegister();
1182 const triton::arch::Register& index = mem.getConstIndexRegister();
1184 triton::uint64 scaleValue = mem.getConstScale().getValue();
1185 triton::uint64 dispValue = mem.getConstDisplacement().getValue();
1186 triton::uint32 bitSize = (this->architecture->isRegisterValid(base) ? base.getBitSize() :
1187 (this->architecture->isRegisterValid(index) ? index.getBitSize() :
1189 this->architecture->gprBitSize()
1190 )
1191 )
1192 );
1193
1194 /* Initialize the AST of the memory access (LEA) -> ((pc + base) + (index * scale) + disp) */
1195 auto pcPlusBaseAst = mem.getPcRelative() ? this->astCtxt->bv(mem.getPcRelative(), bitSize) :
1196 (this->architecture->isRegisterValid(base) ? this->getRegisterAst(base) :
1197 this->astCtxt->bv(0, bitSize));
1198
1199 auto indexMulScaleAst = this->astCtxt->bvmul(
1200 (this->architecture->isRegisterValid(index) ? this->getRegisterAst(index) : this->astCtxt->bv(0, bitSize)),
1201 this->astCtxt->bv(scaleValue, bitSize)
1202 );
1203
1204 auto dispAst = this->astCtxt->bv(dispValue, bitSize);
1205 auto leaAst = this->astCtxt->bvadd(
1206 index.isSubtracted() ? this->astCtxt->bvsub(pcPlusBaseAst, indexMulScaleAst) : this->astCtxt->bvadd(pcPlusBaseAst, indexMulScaleAst),
1207 dispAst
1208 );
1209
1210 /* Use segments as base address instead of selector into the GDT. */
1211 if (this->architecture->isRegisterValid(seg)) {
1212 leaAst = this->astCtxt->bvadd(
1213 this->getRegisterAst(seg),
1214 this->astCtxt->sx((seg.getBitSize() - bitSize), leaAst)
1215 );
1216 }
1217
1218 /* Set AST */
1219 mem.setLeaAst(leaAst);
1220
1221 /* Initialize the address only if it is not already defined */
1222 if (!mem.getAddress() || force)
1223 mem.setAddress(static_cast<triton::uint64>(leaAst->evaluate()));
1224 }
1225 }
1226
1227
1229 return this->astCtxt->getVariableValue(symVar->getName());
1230 }
1231
1232
1234 triton::uint512 max = -1;
1235
1236 /* Check if the value is too big */
1237 max = max >> (512 - symVar->getSize());
1238 if (value > max) {
1239 throw triton::exceptions::SymbolicEngine("SymbolicEngine::setConcreteVariableValue(): Can not set this value (too big) to this symbolic variable.");
1240 }
1241
1242 /* Update the symbolic variable value */
1243 this->astCtxt->updateVariable(symVar->getName(), value);
1244
1245 /* Synchronize concrete state */
1246 if (symVar->getType() == REGISTER_VARIABLE) {
1247 const triton::arch::Register& reg = this->architecture->getRegister(static_cast<triton::arch::register_e>(symVar->getOrigin()));
1248 this->architecture->setConcreteRegisterValue(reg, value);
1249 }
1250
1251 else if (symVar->getType() == MEMORY_VARIABLE && symVar->getSize() && !(symVar->getSize() % bitsize::byte)) {
1252 triton::uint64 addr = symVar->getOrigin();
1253 triton::uint32 size = symVar->getSize() / bitsize::byte;
1255
1256 this->architecture->setConcreteMemoryValue(mem, value);
1257 }
1258 }
1259
1260 }; /* symbolic namespace */
1261 }; /* engines namespace */
1262}; /*triton namespace */
The abstract architecture class.
TRITON_EXPORT const triton::arch::Register & getRegister(triton::arch::register_e id) const
Returns register from id.
TRITON_EXPORT triton::uint32 numberOfRegisters(void) const
Returns the number of registers according to the CPU architecture.
TRITON_EXPORT triton::uint32 gprBitSize(void) const
Returns the bit in bit of the General Purpose Registers.
TRITON_EXPORT void setConcreteRegisterValue(const triton::arch::Register &reg, const triton::uint512 &value, bool execCallbacks=true)
[architecture api] - Sets the concrete value of a register.
TRITON_EXPORT void setConcreteMemoryValue(triton::uint64 addr, triton::uint8 value, bool execCallbacks=true)
[architecture api] - Sets the concrete value of a memory cell.
TRITON_EXPORT bool isFlag(triton::arch::register_e regId) const
Returns true if the register ID is a flag.
TRITON_EXPORT triton::uint8 getConcreteMemoryValue(triton::uint64 addr, bool execCallbacks=true) const
Returns the concrete value of a memory cell.
TRITON_EXPORT triton::uint512 getConcreteRegisterValue(const triton::arch::Register &reg, bool execCallbacks=true) const
Returns the concrete value of a register.
TRITON_EXPORT bool isRegisterValid(triton::arch::register_e regId) const
Returns true if the register ID is a register or a flag.
TRITON_EXPORT const triton::arch::Register & getParentRegister(triton::arch::register_e id) const
Returns parent register from id.
TRITON_EXPORT triton::uint32 getHigh(void) const
Returns the highest bit.
Definition: bitsVector.cpp:34
TRITON_EXPORT triton::uint32 getLow(void) const
Returns the lower bit.
Definition: bitsVector.cpp:39
This class is used to represent an immediate.
Definition: immediate.hpp:37
TRITON_EXPORT triton::uint32 getBitSize(void) const
Returns the size (in bits) of the immediate vector.
Definition: immediate.cpp:85
TRITON_EXPORT triton::uint64 getValue(void) const
Returns the value of the operand.
Definition: immediate.cpp:34
This class is used to represent an instruction.
Definition: instruction.hpp:48
TRITON_EXPORT void setLoadAccess(const triton::arch::MemoryAccess &mem, const triton::ast::SharedAbstractNode &node)
Sets a load access.
TRITON_EXPORT void setWrittenRegister(const triton::arch::Register &reg, const triton::ast::SharedAbstractNode &node)
Sets a written register.
TRITON_EXPORT void setStoreAccess(const triton::arch::MemoryAccess &mem, const triton::ast::SharedAbstractNode &node)
Sets a store access.
TRITON_EXPORT void addSymbolicExpression(const triton::engines::symbolic::SharedSymbolicExpression &expr)
Adds a symbolic expression.
TRITON_EXPORT void setReadImmediate(const triton::arch::Immediate &imm, const triton::ast::SharedAbstractNode &node)
Sets a read immediate.
std::vector< triton::engines::symbolic::SharedSymbolicExpression > symbolicExpressions
The semantics set of the instruction.
TRITON_EXPORT void setReadRegister(const triton::arch::Register &reg, const triton::ast::SharedAbstractNode &node)
Sets a read register.
This class is used to represent a memory access.
TRITON_EXPORT triton::uint64 getPcRelative(void) const
LEA - Gets pc relative.
TRITON_EXPORT const triton::arch::Register & getConstBaseRegister(void) const
LEA - Returns the base register operand.
TRITON_EXPORT void setLeaAst(const triton::ast::SharedAbstractNode &ast)
Sets the AST of the memory access (LEA).
TRITON_EXPORT const triton::arch::Register & getConstSegmentRegister(void) const
LEA - Returns the segment register operand.
TRITON_EXPORT triton::uint32 getBitSize(void) const
Returns the size (in bits) of the memory vector.
TRITON_EXPORT const triton::arch::Immediate & getConstDisplacement(void) const
LEA - Returns the displacement operand.
TRITON_EXPORT triton::uint64 getAddress(void) const
Returns the address of the memory.
TRITON_EXPORT triton::uint32 getSize(void) const
Returns the size (in bytes) of the memory vector.
TRITON_EXPORT void setAddress(triton::uint64 addr)
Sets the address of the memory access.
TRITON_EXPORT const triton::arch::Register & getConstIndexRegister(void) const
LEA - Returns the index register operand.
TRITON_EXPORT const triton::arch::Immediate & getConstScale(void) const
LEA - Returns the scale operand.
This class is used as operand wrapper.
TRITON_EXPORT triton::arch::operand_e getType(void) const
Returns the abstract type of the operand.
TRITON_EXPORT const triton::arch::MemoryAccess & getConstMemory(void) const
Returns the memory operand as const.
TRITON_EXPORT const triton::arch::Register & getConstRegister(void) const
Returns the register operand.
TRITON_EXPORT const triton::arch::Immediate & getConstImmediate(void) const
Returns the immediate operand.
This class is used when an instruction has a register operand.
Definition: register.hpp:44
TRITON_EXPORT triton::uint32 getBitSize(void) const
Returns the size (in bits) of the register.
Definition: register.cpp:63
TRITON_EXPORT triton::arch::register_e getParent(void) const
Returns the parent id of the register.
Definition: register.cpp:58
TRITON_EXPORT triton::arch::register_e getId(void) const
Returns the id of the register.
Definition: register.cpp:53
TRITON_EXPORT bool isMutable(void) const
Returns true if this register is mutable. Mainly used in AArch64 to define that some registers like X...
Definition: register.cpp:92
TRITON_EXPORT triton::uint32 getSize(void) const
Returns the size (in bytes) of the register.
Definition: register.cpp:68
This class is used to represent specific properties of an Arm operand.
TRITON_EXPORT triton::arch::arm::shift_e getShiftType(void) const
Returns the type of the shift.
TRITON_EXPORT triton::arch::register_e getShiftRegister(void) const
Returns the value of the shift register.
TRITON_EXPORT triton::arch::arm::extend_e getExtendType(void) const
Returns the type of the extend.
TRITON_EXPORT triton::uint32 getExtendSize(void) const
Returns the size (in bits) of the extend.
TRITON_EXPORT triton::uint32 getShiftImmediate(void) const
Returns the value of the shift immediate.
TRITON_EXPORT bool isSubtracted(void) const
Returns true if the operand has to be subtracted when computing a memory access.
Reference node.
Definition: ast.hpp:789
The callbacks class.
Definition: callbacks.hpp:79
TRITON_EXPORT PathManager & operator=(const PathManager &other)
Copies a PathManager.
Definition: pathManager.cpp:30
std::unordered_map< triton::usize, WeakSymbolicExpression > symbolicExpressions
The map of symbolic expressions.
TRITON_EXPORT const SharedSymbolicExpression & createSymbolicMemoryExpression(triton::arch::Instruction &inst, const triton::ast::SharedAbstractNode &node, const triton::arch::MemoryAccess &mem, const std::string &comment="")
Returns the new shared symbolic memory expression expression and links this expression to the instruc...
triton::usize uniqueSymExprId
Symbolic expressions id.
std::unordered_map< triton::uint64, SharedSymbolicExpression > memoryReference
map of address -> symbolic expression
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 shared symbolic register expression expression and links this expression to the instr...
TRITON_EXPORT SharedSymbolicVariable symbolizeExpression(triton::usize exprId, triton::uint32 symVarSize, const std::string &symVarAlias="")
Converts a symbolic expression to a symbolic variable. symVarSize must be in bits.
triton::usize uniqueSymVarId
Symbolic variables id.
TRITON_EXPORT bool isMemorySymbolized(const triton::arch::MemoryAccess &mem) const
Returns true if memory cell expressions contain symbolic variables.
TRITON_EXPORT std::unordered_map< triton::usize, SharedSymbolicExpression > getSymbolicExpressions(void) const
Returns all symbolic expressions.
TRITON_EXPORT bool isSymbolicExpressionExists(triton::usize symExprId) const
Returns true if the symbolic expression ID exists.
TRITON_EXPORT SymbolicEngine & operator=(const SymbolicEngine &other)
Copies a SymbolicEngine.
TRITON_EXPORT SharedSymbolicVariable symbolizeRegister(const triton::arch::Register &reg, const std::string &symVarAlias="")
Converts a symbolic register expression to a symbolic variable.
triton::ast::SharedAbstractNode getShiftAst(const triton::arch::arm::ArmOperandProperties &shift, const triton::ast::SharedAbstractNode &node)
Returns the AST corresponding to the shift operation. Mainly used for Arm32 operands.
TRITON_EXPORT SharedSymbolicExpression getSymbolicExpression(triton::usize symExprId) const
Returns the symbolic expression corresponding to an id.
TRITON_EXPORT SharedSymbolicVariable getSymbolicVariable(triton::usize symVarId) const
Returns the symbolic variable corresponding to the symbolic variable id.
TRITON_EXPORT const SharedSymbolicExpression & createSymbolicVolatileExpression(triton::arch::Instruction &inst, const triton::ast::SharedAbstractNode &node, const std::string &comment="")
Returns the new shared symbolic volatile expression expression and links this expression to the instr...
TRITON_EXPORT void assignSymbolicExpressionToMemory(const SharedSymbolicExpression &se, const triton::arch::MemoryAccess &mem)
Assigns a symbolic expression to a memory.
TRITON_EXPORT void setConcreteVariableValue(const SharedSymbolicVariable &symVar, const triton::uint512 &value)
Sets the concrete value of a symbolic variable.
TRITON_EXPORT const std::unordered_map< triton::uint64, SharedSymbolicExpression > & getSymbolicMemory(void) const
Returns the map (addr:expr) of all symbolic memory defined.
TRITON_EXPORT void assignSymbolicExpressionToRegister(const SharedSymbolicExpression &se, const triton::arch::Register &reg)
Assigns a symbolic expression to a register.
TRITON_EXPORT void initLeaAst(triton::arch::MemoryAccess &mem, bool force=true)
Initializes the memory access AST (LOAD and STORE).
TRITON_EXPORT std::vector< triton::uint8 > getSymbolicMemoryAreaValue(triton::uint64 baseAddr, triton::usize size)
Returns the symbolic values of a memory area.
TRITON_EXPORT std::unordered_map< triton::arch::register_e, SharedSymbolicExpression > getSymbolicRegisters(void) const
Returns the map of symbolic registers defined.
std::map< std::pair< triton::uint64, triton::uint32 >, SharedSymbolicExpression > alignedMemoryReference
map of <address:size> -> symbolic expression.
TRITON_EXPORT SymbolicEngine(triton::arch::Architecture *architecture, const triton::modes::SharedModes &modes, const triton::ast::SharedAstContext &astCtxt, triton::callbacks::Callbacks *callbacks=nullptr)
Constructor.
TRITON_EXPORT triton::ast::SharedAbstractNode getMemoryAst(const triton::arch::MemoryAccess &mem)
Returns the AST corresponding to the memory.
TRITON_EXPORT SharedSymbolicVariable symbolizeMemory(const triton::arch::MemoryAccess &mem, const std::string &symVarAlias="")
Converts a symbolic memory expression to a symbolic variable.
TRITON_EXPORT triton::uint512 getSymbolicRegisterValue(const triton::arch::Register &reg)
Returns the symbolic register value.
TRITON_EXPORT std::vector< SharedSymbolicExpression > getTaintedSymbolicExpressions(void) const
Returns the vector of the tainted symbolic expressions.
TRITON_EXPORT triton::ast::SharedAbstractNode getRegisterAst(const triton::arch::Register &reg)
Returns the AST corresponding to the register.
TRITON_EXPORT triton::uint512 getConcreteVariableValue(const SharedSymbolicVariable &symVar) const
Gets the concrete value of a symbolic variable.
TRITON_EXPORT SharedSymbolicVariable newSymbolicVariable(triton::engines::symbolic::variable_e type, triton::uint64 source, triton::uint32 size, const std::string &alias="")
Adds a symbolic variable.
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 shared symbolic abstract expression and links this expression to the instruction.
TRITON_EXPORT SharedSymbolicExpression newSymbolicExpression(const triton::ast::SharedAbstractNode &node, triton::engines::symbolic::expression_e type, const std::string &comment="")
Creates a new shared symbolic expression.
TRITON_EXPORT const SharedSymbolicExpression & getSymbolicRegister(const triton::arch::Register &reg) const
Returns the shared symbolic expression corresponding to the parent register.
TRITON_EXPORT void removeSymbolicExpression(const SharedSymbolicExpression &expr)
Removes the symbolic expression corresponding to the id.
TRITON_EXPORT std::unordered_map< triton::usize, SharedSymbolicExpression > sliceExpressions(const SharedSymbolicExpression &expr)
Slices all expressions from a given one.
triton::uint32 numberOfRegisters
Number of registers.
TRITON_EXPORT triton::uint8 getSymbolicMemoryValue(triton::uint64 address)
Returns the symbolic memory value.
TRITON_EXPORT void concretizeAllMemory(void)
Concretizes all symbolic memory references.
std::unordered_map< triton::usize, WeakSymbolicVariable > symbolicVariables
The map of symbolic variables.
TRITON_EXPORT ~SymbolicEngine()
Destructor.
TRITON_EXPORT triton::ast::SharedAbstractNode getImmediateAst(const triton::arch::Immediate &imm)
Returns the AST corresponding to the immediate.
std::vector< SharedSymbolicExpression > symbolicReg
Symbolic register state.
TRITON_EXPORT void concretizeAllRegister(void)
Concretizes all symbolic register references.
TRITON_EXPORT std::map< triton::usize, SharedSymbolicVariable > getSymbolicVariables(void) const
Returns all symbolic variables.
TRITON_EXPORT void concretizeRegister(const triton::arch::Register &reg)
Concretizes a specific symbolic register reference.
TRITON_EXPORT triton::ast::SharedAbstractNode getOperandAst(const triton::arch::OperandWrapper &op)
Returns the AST corresponding to the operand.
TRITON_EXPORT bool isRegisterSymbolized(const triton::arch::Register &reg) const
Returns true if the register expression contains a symbolic variable.
TRITON_EXPORT void concretizeMemory(const triton::arch::MemoryAccess &mem)
Concretizes a specific symbolic memory reference.
TRITON_EXPORT triton::ast::SharedAbstractNode simplify(const triton::ast::SharedAbstractNode &node) const
Processes all recorded simplifications. Returns the simplified node.
TRITON_EXPORT SymbolicSimplification & operator=(const SymbolicSimplification &other)
Copies a SymbolicSimplification.
The exception class used by the symbolic engine.
Definition: exceptions.hpp:77
register_e
Types of register.
Definition: archEnums.hpp:64
@ ID_SHIFT_LSR
Logical Shift Right (immediate)
Definition: archEnums.hpp:127
@ ID_SHIFT_LSR_REG
Logical Shift Right (register)
Definition: archEnums.hpp:132
@ ID_SHIFT_ASR
Arithmetic Shift Right (immediate)
Definition: archEnums.hpp:125
@ ID_SHIFT_ROR_REG
Rotate Right (register)
Definition: archEnums.hpp:133
@ ID_SHIFT_ROR
Rotate Right (immediate)
Definition: archEnums.hpp:128
@ ID_SHIFT_ASR_REG
Arithmetic Shift Right (register)
Definition: archEnums.hpp:130
@ ID_SHIFT_RRX
Rotate Right with Extend (immediate)
Definition: archEnums.hpp:129
@ ID_SHIFT_RRX_REG
Rotate Right with Extend (register)
Definition: archEnums.hpp:134
@ ID_SHIFT_LSL_REG
Logical Shift Left (register)
Definition: archEnums.hpp:131
@ ID_SHIFT_INVALID
invalid
Definition: archEnums.hpp:124
@ ID_SHIFT_LSL
Logical Shift Left (immediate)
Definition: archEnums.hpp:126
@ ID_EXTEND_SXTW
Extracts a word (32-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:147
@ ID_EXTEND_UXTX
Use the whole 64-bit register.
Definition: archEnums.hpp:144
@ ID_EXTEND_SXTX
Use the whole 64-bit register.
Definition: archEnums.hpp:148
@ ID_EXTEND_SXTH
Extracts a halfword (16-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:146
@ ID_EXTEND_UXTB
Extracts a byte (8-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:141
@ ID_EXTEND_INVALID
invalid
Definition: archEnums.hpp:140
@ ID_EXTEND_UXTW
Extracts a word (32-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:143
@ ID_EXTEND_SXTB
Extracts a byte (8-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:145
@ ID_EXTEND_UXTH
Extracts a halfword (16-bit) value from a register and zero extends it to the size of the register.
Definition: archEnums.hpp:142
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition: ast.hpp:59
std::vector< SharedAbstractNode > childrenExtraction(const SharedAbstractNode &node, bool unroll, bool revert)
Returns node and all its children of an AST sorted topologically. If unroll is true,...
Definition: ast.cpp:3687
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition: ast.hpp:65
@ REFERENCE_NODE
Definition: astEnums.hpp:79
constexpr triton::uint32 byte
byte size in bit
Definition: cpuSize.hpp:60
constexpr triton::uint32 word
word size in bit
Definition: cpuSize.hpp:62
std::shared_ptr< triton::modes::Modes > SharedModes
Shared Modes.
Definition: modes.hpp:66
@ ALIGNED_MEMORY
[symbolic] Keep a map of aligned memory.
Definition: modesEnums.hpp:30
@ ONLY_ON_SYMBOLIZED
[symbolic] Perform symbolic execution only on symbolized expressions.
Definition: modesEnums.hpp:34
@ AST_OPTIMIZATIONS
[AST] Classical arithmetic optimisations to reduce the depth of the trees.
Definition: modesEnums.hpp:31
constexpr triton::uint32 fword
fword size in byte
Definition: cpuSize.hpp:38
constexpr triton::uint32 dword
dword size in byte
Definition: cpuSize.hpp:34
constexpr triton::uint32 dqqword
dqqword size in byte
Definition: cpuSize.hpp:44
constexpr triton::uint32 word
word size in byte
Definition: cpuSize.hpp:32
constexpr triton::uint32 dqword
dqword size in byte
Definition: cpuSize.hpp:40
constexpr triton::uint32 byte
byte size in byte
Definition: cpuSize.hpp:30
constexpr triton::uint32 qword
qword size in byte
Definition: cpuSize.hpp:36
constexpr triton::uint32 qqword
qqword size in byte
Definition: cpuSize.hpp:42
std::shared_ptr< triton::engines::symbolic::SymbolicVariable > SharedSymbolicVariable
Shared Symbolic variable.
Definition: ast.hpp:43
expression_e
Type of symbolic expressions.
std::shared_ptr< triton::engines::symbolic::SymbolicExpression > SharedSymbolicExpression
Shared Symbolic Expression.
Definition: ast.hpp:40
variable_e
Type of symbolic variable.
@ REGISTER_EXPRESSION
Assigned to a register expression.
@ MEMORY_EXPRESSION
Assigned to a memory expression.
@ VOLATILE_EXPRESSION
Assigned to a volatile expression.
@ REGISTER_VARIABLE
Variable assigned to a register.
@ MEMORY_VARIABLE
Variable assigned to a memory.
@ UNDEFINED_VARIABLE
Undefined assignment.
std::int32_t sint32
signed 32-bits
Definition: tritonTypes.hpp:79
std::size_t usize
unsigned MAX_INT 32 or 64 bits according to the CPU.
std::uint64_t uint64
unisgned 64-bits
Definition: tritonTypes.hpp:42
std::uint32_t uint32
unisgned 32-bits
Definition: tritonTypes.hpp:39
std::uint8_t uint8
unisgned 8-bits
Definition: tritonTypes.hpp:33
TRITON_EXPORT void fromUintToBuffer(triton::uint80 value, triton::uint8 *buffer)
Inject the value into the buffer. Make sure that the buffer contains at least 10 allocated bytes.
Definition: coreUtils.cpp:16
The Triton namespace.