libTriton version 1.0 build 1588
Loading...
Searching...
No Matches
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(architecture, 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 this->memoryArray = nullptr;
42
43 this->symbolicReg.resize(this->numberOfRegisters);
44 }
45
46
48 : triton::engines::symbolic::SymbolicSimplification(other),
49 triton::engines::symbolic::PathManager(other),
50 astCtxt(other.astCtxt),
51 modes(other.modes) {
52
54 this->architecture = other.architecture;
55 this->callbacks = other.callbacks;
56 this->memoryArray = other.memoryArray;
57 this->memoryBitvector = other.memoryBitvector;
60 this->symbolicReg = other.symbolicReg;
62 this->uniqueSymExprId = other.uniqueSymExprId;
63 this->uniqueSymVarId = other.uniqueSymVarId;
64 }
65
66
68 /* See #828: Release ownership before calling container destructor */
69 this->memoryBitvector.clear();
70 this->symbolicReg.clear();
71 this->memoryArray = nullptr;
72 }
73
74
78
80 this->architecture = other.architecture;
81 this->astCtxt = other.astCtxt;
82 this->callbacks = other.callbacks;
83 this->memoryBitvector = other.memoryBitvector;
84 this->modes = other.modes;
87 this->symbolicReg = other.symbolicReg;
89 this->uniqueSymExprId = other.uniqueSymExprId;
90 this->uniqueSymVarId = other.uniqueSymVarId;
91
92 return *this;
93 }
94
95
96 /*
97 * Concretize a register. If the register is setup as nullptr, the next assignment
98 * will be over the concretization. This method must be called before symbolic
99 * processing.
100 */
102 triton::arch::register_e parentId = reg.getParent();
103
104 if (this->architecture->isRegisterValid(parentId)) {
105 this->symbolicReg[parentId] = nullptr;
106 }
107 }
108
109
110 /* Same as concretizeRegister but with all registers */
112 for (triton::uint32 i = 0; i < this->numberOfRegisters; i++) {
113 this->symbolicReg[i] = nullptr;
114 }
115 }
116
117
118 /*
119 * Concretize a memory. If the memory is not found into the map, the next
120 * assignment will be over the concretization. This method must be called
121 * before symbolic processing.
122 */
124 triton::uint64 addr = mem.getAddress();
125 triton::uint32 size = mem.getSize();
126
127 for (triton::uint32 index = 0; index < size; index++) {
128 this->concretizeMemory(addr+index, array);
129 }
130 }
131
132
133 /*
134 * Concretize a memory. If the memory is not found into the map, the next
135 * assignment will be over the concretization. This method must be called
136 * before symbolic processing.
137 */
139 /* Symbolic array */
140 if (this->isArrayMode() && array) {
141 auto cv = this->architecture->getConcreteMemoryValue(addr);
142 auto cell = this->astCtxt->store(this->astCtxt->reference(this->getMemoryArray()), addr, this->astCtxt->bv(cv, triton::bitsize::byte));
143 this->memoryArray = this->newSymbolicExpression(cell, MEMORY_EXPRESSION, "Concretization");
144 this->memoryArray->setOriginMemory(triton::arch::MemoryAccess(addr, triton::size::byte));
145 }
146
147 /* Symbolic bitvector */
148 this->memoryBitvector.erase(addr);
149 this->removeAlignedMemory(addr, triton::size::byte);
150 }
151
152
153 /* Same as concretizeMemory but with all address memory */
155 this->memoryArray = nullptr; /* abv logic */
156 this->memoryBitvector.clear(); /* bv logic */
157 this->alignedBitvectorMemory.clear(); /* bv optim */
158 }
159
160
161 /* Gets an aligned entry. */
162 const SharedSymbolicExpression& SymbolicEngine::getAlignedMemory(triton::uint64 address, triton::uint32 size) {
163 return this->alignedBitvectorMemory[std::make_pair(address, size)];
164 }
165
166
167 /* Checks if the aligned memory is recored. */
168 bool SymbolicEngine::isAlignedMemory(triton::uint64 address, triton::uint32 size) {
169 if (this->alignedBitvectorMemory.find(std::make_pair(address, size)) != this->alignedBitvectorMemory.end()) {
170 return true;
171 }
172 return false;
173 }
174
175
176 /* Adds an aligned memory */
177 void SymbolicEngine::addAlignedMemory(triton::uint64 address, triton::uint32 size, const SharedSymbolicExpression& expr) {
178 this->removeAlignedMemory(address, size);
179 if (!(this->modes->isModeEnabled(triton::modes::ONLY_ON_SYMBOLIZED) && expr->getAst()->isSymbolized() == false)) {
180 this->alignedBitvectorMemory[std::make_pair(address, size)] = expr;
181 }
182 }
183
184
185 /* Removes an aligned memory */
186 void SymbolicEngine::removeAlignedMemory(triton::uint64 address, triton::uint32 size) {
187 /*
188 * Avoid accessing the alignedBitvectorMemory array when empty. This usually happens when
189 * you initialize the symbolic engine and concretize whole sections of an executable using
190 * setConcreteMemoryValue. No symbolic memory has been created yet but this function will
191 * still try to rougly erase (size * 7) elements.
192 */
193 if (this->alignedBitvectorMemory.empty())
194 return;
195
196 /* Do nothing if we are in array mode */
197 if (this->isArrayMode())
198 return;
199
200 /* Remove overloaded positive ranges */
201 for (triton::uint32 index = 0; index < size; index++) {
202 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::byte));
203 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::word));
204 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::dword));
205 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::qword));
206 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::fword));
207 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::dqword));
208 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::qqword));
209 this->alignedBitvectorMemory.erase(std::make_pair(address+index, triton::size::dqqword));
210 }
211
212 /* Remove overloaded negative ranges */
213 for (triton::uint32 index = 1; index < triton::size::dqqword; index++) {
214 if (index < triton::size::word) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::word));
215 if (index < triton::size::dword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::dword));
216 if (index < triton::size::qword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::qword));
217 if (index < triton::size::fword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::fword));
218 if (index < triton::size::dqword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::dqword));
219 if (index < triton::size::qqword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::qqword));
220 if (index < triton::size::dqqword) this->alignedBitvectorMemory.erase(std::make_pair(address-index, triton::size::dqqword));
221 }
222 }
223
224
225 /* Returns the reference memory if it's referenced otherwise returns nullptr */
227 auto it = this->memoryBitvector.find(addr);
228 if (it != this->memoryBitvector.end()) {
229 return it->second;
230 }
231 return nullptr;
232 }
233
234
235 /* Returns the symbolic variable otherwise raises an exception */
237 auto it = this->symbolicVariables.find(symVarId);
238 if (it == this->symbolicVariables.end()) {
239 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred symbolic variable.");
240 }
241
242 if (auto node = it->second.lock()) {
243 return node;
244 }
245
246 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): This symbolic variable is dead.");
247 }
248
249
250 /* Returns the symbolic variable otherwise returns nullptr */
252 /*
253 * FIXME: 1) When there is a ton of symvar, this loop takes a while to go through.
254 * What about adding two maps {id:symvar} and {string:symvar}? See #648.
255 *
256 * 2) If we are looking for alias, we return the first occurrence. It's not
257 * ideal if we have multiple same aliases.
258 */
259 for (auto& sv: this->symbolicVariables) {
260 if (auto symVar = sv.second.lock()) {
261 if (symVar->getName() == name || symVar->getAlias() == name) {
262 return symVar;
263 }
264 }
265 }
266 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred or dead symbolic variable.");
267 }
268
269
270 /* Returns all symbolic variables */
271 std::map<triton::usize, SharedSymbolicVariable> SymbolicEngine::getSymbolicVariables(void) const {
272 // Copy and clean up dead weak ref
273 std::map<triton::usize, SharedSymbolicVariable> ret;
274 std::vector<triton::usize> toRemove;
275
276 for (auto& kv : this->symbolicVariables) {
277 if (auto sp = kv.second.lock()) {
278 ret[kv.first] = sp;
279 } else {
280 toRemove.push_back(kv.first);
281 }
282 }
283
284 for (triton::usize id : toRemove) {
285 this->symbolicVariables.erase(id);
286 }
287
288 return ret;
289 }
290
291
292 void SymbolicEngine::setImplicitReadRegisterFromEffectiveAddress(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) {
293 /* Set implicit read of the segment register (LEA) */
294 if (this->architecture->isRegisterValid(mem.getConstSegmentRegister())) {
295 (void)this->getRegisterAst(inst, mem.getConstSegmentRegister());
296 }
297
298 /* Set implicit read of the base register (LEA) */
299 if (this->architecture->isRegisterValid(mem.getConstBaseRegister())) {
300 (void)this->getRegisterAst(inst, mem.getConstBaseRegister());
301 }
302
303 /* Set implicit read of the index register (LEA) */
304 if (this->architecture->isRegisterValid(mem.getConstIndexRegister())) {
305 (void)this->getRegisterAst(inst, mem.getConstIndexRegister());
306 }
307 }
308
309
310 const SharedSymbolicExpression& SymbolicEngine::addSymbolicExpressions(triton::arch::Instruction& inst, triton::usize id) const {
311 /* See #1002: There may be multiple new symbolic expressions when AST_OPTIMIZATIONS are on */
312 for (triton::usize i = id; i != this->uniqueSymExprId; ++i) {
313 if (this->isSymbolicExpressionExists(i)) {
315 }
316 }
317 return inst.symbolicExpressions.back();
318 }
319
320
321 /* Returns the shared symbolic expression corresponding to the register */
323 triton::arch::register_e parentId = reg.getParent();
324
325 if (this->architecture->isRegisterValid(parentId)) {
326 return this->symbolicReg.at(parentId);
327 }
328
329 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicRegister(): Invalid Register");
330 }
331
332
333 /* Returns the symbolic address value */
336 return static_cast<triton::uint8>(this->getSymbolicMemoryValue(mem));
337 }
338
339
340 /* Returns the symbolic memory value */
342 const triton::ast::SharedAbstractNode& node = this->getMemoryAst(mem);
343 return node->evaluate();
344 }
345
346
347 /* Returns the symbolic values of a memory area */
349 std::vector<triton::uint8> area;
350
351 area.reserve(size);
352 for (triton::usize index = 0; index < size; index++) {
353 area.push_back(this->getSymbolicMemoryValue(baseAddr + index));
354 }
355
356 return area;
357 }
358
359
360 /* Returns the symbolic register value */
362 return this->getRegisterAst(reg)->evaluate();
363 }
364
365
366 /* Creates a new symbolic expression */
367 /* Get an unique id.
368 * Mainly used when a new symbolic expression is created */
369 triton::usize SymbolicEngine::getUniqueSymExprId(void) {
370 return this->uniqueSymExprId++;
371 }
372
373
374 /* Creates a new symbolic variable */
375 /* Get an unique id.
376 * Mainly used when a new symbolic variable is created */
377 triton::usize SymbolicEngine::getUniqueSymVarId(void) {
378 return this->uniqueSymVarId++;
379 }
380
381
382 /* Returns or init the symbolic memory array */
383 SharedSymbolicExpression SymbolicEngine::getMemoryArray(void) {
384 if (this->isArrayMode() && this->memoryArray == nullptr) {
385 triton::uint32 gpr_size = this->architecture->gprBitSize();
386 this->memoryArray = this->newSymbolicExpression(this->astCtxt->array(gpr_size), VOLATILE_EXPRESSION);
387 }
388 return this->memoryArray;
389 }
390
391
392 /* Creates a new symbolic expression with comment */
394 if (this->modes->isModeEnabled(triton::modes::AST_OPTIMIZATIONS)) {
395 /*
396 * Create volatile expression for extended part to avoid long
397 * formulas while printing. Long formulas are introduced by
398 * optimizations of AstContext::concat and AstContext::extract
399 */
400 if (node->getType() == triton::ast::ZX_NODE || node->getType() == triton::ast::SX_NODE) {
401 auto n = node->getChildren()[1];
402 if (n->getType() != triton::ast::REFERENCE_NODE && n->getType() != triton::ast::VARIABLE_NODE) {
403 /* FIXME: We lost the origin if we create a new symbolic expression without returning it */
404 auto e = this->newSymbolicExpression(n, VOLATILE_EXPRESSION, "Extended part - " + comment);
405 node->setChild(1, this->astCtxt->reference(e));
406 }
407 }
408 }
409
410 /* Each symbolic expression must have an unique id */
411 triton::usize id = this->getUniqueSymExprId();
412
413 /* Performes transformation if there are rules recorded */
414 const triton::ast::SharedAbstractNode& snode = this->simplify(node);
415
416 /* Allocates the new shared symbolic expression */
417 SharedSymbolicExpression expr = std::make_shared<SymbolicExpression>(snode, id, type, comment);
418 if (expr == nullptr) {
419 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicExpression(): not enough memory");
420 }
421
422 /* Save and returns the new shared symbolic expression */
423 this->symbolicExpressions[id] = expr;
424 return expr;
425 }
426
427
428 /* Removes the symbolic expression corresponding to the id */
430 if (this->symbolicExpressions.find(expr->getId()) != this->symbolicExpressions.end()) {
431 /* Concretize memory */
432 if (expr->getType() == MEMORY_EXPRESSION) {
433 const auto& mem = expr->getOriginMemory();
434 this->concretizeMemory(mem, false);
435 }
436
437 /* Concretize register */
438 else if (expr->getType() == REGISTER_EXPRESSION) {
439 const auto& reg = expr->getOriginRegister();
440 this->concretizeRegister(reg);
441 }
442
443 /* Delete and remove the pointer */
444 this->symbolicExpressions.erase(expr->getId());
445 }
446 }
447
448
449 /* Gets the shared symbolic expression from a symbolic id */
451 auto it = this->symbolicExpressions.find(symExprId);
452 if (it == this->symbolicExpressions.end()) {
453 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression id not found");
454 }
455
456 if (auto sp = it->second.lock()) {
457 return sp;
458 }
459
460 this->symbolicExpressions.erase(symExprId);
461 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression is not available anymore");
462 }
463
464
465 /* Returns all symbolic expressions */
466 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::getSymbolicExpressions(void) const {
467 // Copy and clean up dead weak ref
468 std::unordered_map<triton::usize, SharedSymbolicExpression> ret;
469 std::vector<triton::usize> toRemove;
470
471 for (auto& kv : this->symbolicExpressions) {
472 if (auto sp = kv.second.lock()) {
473 ret[kv.first] = sp;
474 } else {
475 toRemove.push_back(kv.first);
476 }
477 }
478
479 for (auto id : toRemove)
480 this->symbolicExpressions.erase(id);
481
482 return ret;
483 }
484
485
486 /* Slices all expressions from a given one */
487 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::sliceExpressions(const SharedSymbolicExpression& expr) {
488 std::unordered_map<triton::usize, SharedSymbolicExpression> exprs;
489
490 if (expr == nullptr) {
491 throw triton::exceptions::SymbolicEngine("SymbolicEngine::sliceExpressions(): expr cannot be null.");
492 }
493
494 exprs[expr->getId()] = expr;
495
496 auto worklist = triton::ast::childrenExtraction(expr->getAst(), true /* unroll */, false /* revert */);
497 for (auto&& n : worklist) {
498 if (n->getType() == triton::ast::REFERENCE_NODE) {
499 auto expr = reinterpret_cast<triton::ast::ReferenceNode*>(n.get())->getSymbolicExpression();
500 auto eid = expr->getId();
501 exprs[eid] = expr;
502 }
503 }
504
505 return exprs;
506 }
507
508
509 /* Returns a list which contains all tainted expressions */
510 std::vector<SharedSymbolicExpression> SymbolicEngine::getTaintedSymbolicExpressions(void) const {
511 std::vector<SharedSymbolicExpression> taintedExprs;
512 std::vector<triton::usize> invalidSymExpr;
513
514 for (auto it = this->symbolicExpressions.begin(); it != this->symbolicExpressions.end(); it++) {
515 if (auto sp = it->second.lock()) {
516 if (sp->isTainted) {
517 taintedExprs.push_back(sp);
518 }
519 } else {
520 invalidSymExpr.push_back(it->first);
521 }
522 }
523
524 for (auto id : invalidSymExpr) {
525 this->symbolicExpressions.erase(id);
526 }
527
528 return taintedExprs;
529 }
530
531
532 /* Returns the map of symbolic registers defined */
533 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> SymbolicEngine::getSymbolicRegisters(void) const {
534 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> ret;
535
536 for (triton::uint32 it = 0; it < this->numberOfRegisters; it++) {
537 if (this->symbolicReg[it] != nullptr) {
538 ret[triton::arch::register_e(it)] = this->symbolicReg[it];
539 }
540 }
541
542 return ret;
543 }
544
545
546 /* Returns the map of symbolic memory defined */
547 const std::unordered_map<triton::uint64, SharedSymbolicExpression>& SymbolicEngine::getSymbolicMemory(void) const {
548 return this->memoryBitvector;
549 }
550
551
552 /*
553 * Converts an expression id to a symbolic variable.
554 * e.g:
555 * #43 = (_ bv10 8)
556 * symbolizeExpression(43, 8)
557 * #43 = SymVar_4
558 */
560 const SharedSymbolicExpression& expression = this->getSymbolicExpression(exprId);
561 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(UNDEFINED_VARIABLE, 0, symVarSize, symVarAlias);
562 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->variable(symVar);
563
564 if (expression->getAst()) {
565 this->setConcreteVariableValue(symVar, expression->getAst()->evaluate());
566 }
567
568 expression->setAst(tmp);
569
570 return symVar;
571 }
572
573
574 /* Symbolize a memory area to 8-bits symbolic variables */
576 for (triton::usize i = 0; i != size; i++) {
578 }
579 }
580
581
582 /* The memory size is used to define the symbolic variable's size. */
584 triton::uint64 memAddr = mem.getAddress();
585 triton::uint32 symVarSize = mem.getSize();
586 triton::uint512 cv = this->architecture->getConcreteMemoryValue(mem);
587
588 /* First we create a symbolic variable */
589 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(MEMORY_VARIABLE, memAddr, symVarSize * bitsize::byte, symVarAlias);
590
591 /* Create the AST node */
592 const triton::ast::SharedAbstractNode& symVarNode = this->astCtxt->variable(symVar);
593
594 /* Setup the concrete value to the symbolic variable */
595 this->setConcreteVariableValue(symVar, cv);
596
597 /* Record the aligned symbolic variable for a symbolic optimization */
598 if (this->isAlignedMode() && this->isArrayMode() == false) {
599 const SharedSymbolicExpression& aligned = this->newSymbolicExpression(symVarNode, MEMORY_EXPRESSION, "Aligned optimization");
600 aligned->setOriginMemory(mem);
601 this->addAlignedMemory(memAddr, symVarSize, aligned);
602 }
603
604 /* Split expression in bytes */
605 for (triton::sint32 index = symVarSize-1; index >= 0; index--) {
606 triton::uint32 high = ((bitsize::byte * (index + 1)) - 1);
607 triton::uint32 low = ((bitsize::byte * (index + 1)) - bitsize::byte);
608
609 /* Isolate the good part of the symbolic variable */
610 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, symVarNode);
611
612 /* Create a new symbolic expression containing the symbolic variable */
613 /* Symbolic array */
614 if (this->isArrayMode()) {
615 const auto& cell = this->astCtxt->store(this->astCtxt->reference(this->getMemoryArray()), memAddr + index, tmp);
616 this->memoryArray = this->newSymbolicExpression(cell, MEMORY_EXPRESSION, "Byte reference");
617 this->memoryArray->setOriginMemory(triton::arch::MemoryAccess(memAddr + index, triton::size::byte));
618 this->addBitvectorMemory(memAddr + index, this->memoryArray);
619 }
620 /* Symbolic bitvector */
621 else {
622 const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
623 se->setOriginMemory(triton::arch::MemoryAccess(memAddr + index, triton::size::byte));
624 this->addBitvectorMemory(memAddr + index, se);
625 }
626 }
627
628 return symVar;
629 }
630
631
633 const triton::arch::Register& parent = this->architecture->getRegister(reg.getParent());
634 triton::uint32 symVarSize = reg.getBitSize();
635 triton::uint512 cv = this->architecture->getConcreteRegisterValue(reg);
636
637 if (!this->architecture->isRegisterValid(parent.getId()))
638 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): Invalid register id");
639
640 if (reg.isMutable() == false)
641 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): This register is immutable");
642
643 /* Create the symbolic variable */
644 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(REGISTER_VARIABLE, reg.getId(), symVarSize, symVarAlias);
645
646 /* Create the AST node */
647 const triton::ast::SharedAbstractNode& tmp = this->insertSubRegisterInParent(reg, this->astCtxt->variable(symVar), false);
648
649 /* Setup the concrete value to the symbolic variable */
650 this->setConcreteVariableValue(symVar, cv);
651
652 /* Create a new symbolic expression containing the symbolic variable */
654
655 /* Assign the symbolic expression to the register */
656 this->assignSymbolicExpressionToRegister(se, parent);
657
658 return symVar;
659 }
660
661
662 /* Adds a new symbolic variable */
664 triton::usize uniqueId = this->getUniqueSymVarId();
665
666 SharedSymbolicVariable symVar = std::make_shared<SymbolicVariable>(type, origin, uniqueId, size, alias);
667 if (symVar == nullptr) {
668 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicVariable(): Cannot allocate a new symbolic variable");
669 }
670
671 this->symbolicVariables[uniqueId] = symVar;
672 return symVar;
673 }
674
675
676 /* Returns the AST corresponding to the operand. */
678 switch (op.getType()) {
680 case triton::arch::OP_MEM: return this->getMemoryAst(op.getConstMemory());
682 default:
683 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
684 }
685 }
686
687
688 /* Returns the AST corresponding to the operand. */
690 switch (op.getType()) {
691 case triton::arch::OP_IMM: return this->getImmediateAst(inst, op.getConstImmediate());
692 case triton::arch::OP_MEM: return this->getMemoryAst(inst, op.getConstMemory());
693 case triton::arch::OP_REG: return this->getRegisterAst(inst, op.getConstRegister());
694 default:
695 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
696 }
697 }
698
699
701 auto imm = shift.getShiftImmediate();
702 auto reg = shift.getShiftRegister();
703
704 switch (shift.getShiftType()) {
706 return this->astCtxt->bvashr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
707
709 return this->astCtxt->bvshl(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
710
712 return this->astCtxt->bvlshr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
713
715 return this->astCtxt->bvror(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
716
717 case triton::arch::arm::ID_SHIFT_RRX: /* Arm32 only. */
718 return this->astCtxt->extract(
719 node->getBitvectorSize(),
720 1,
721 this->astCtxt->bvror(
722 this->astCtxt->concat(
723 node,
724 this->getRegisterAst(this->architecture->getRegister(triton::arch::ID_REG_ARM32_C))
725 ),
726 1
727 )
728 );
729
730 case triton::arch::arm::ID_SHIFT_ASR_REG: /* Arm32 only. */
731 return this->astCtxt->bvashr(
732 node,
733 this->astCtxt->zx(
734 this->architecture->getRegister(reg).getBitSize() - 8,
735 this->astCtxt->extract(
736 7,
737 0,
738 this->getRegisterAst(this->architecture->getRegister(reg))
739 )
740 )
741 );
742
743 case triton::arch::arm::ID_SHIFT_LSL_REG: /* Arm32 only. */
744 return this->astCtxt->bvshl(
745 node,
746 this->astCtxt->zx(
747 this->architecture->getRegister(reg).getBitSize() - 8,
748 this->astCtxt->extract(
749 7,
750 0,
751 this->getRegisterAst(this->architecture->getRegister(reg))
752 )
753 )
754 );
755
756 case triton::arch::arm::ID_SHIFT_LSR_REG: /* Arm32 only. */
757 return this->astCtxt->bvlshr(
758 node,
759 this->astCtxt->zx(
760 this->architecture->getRegister(reg).getBitSize() - 8,
761 this->astCtxt->extract(
762 7,
763 0,
764 this->getRegisterAst(this->architecture->getRegister(reg))
765 )
766 )
767 );
768
769 case triton::arch::arm::ID_SHIFT_ROR_REG: /* Arm32 only. */
770 return this->astCtxt->bvror(
771 node,
772 this->astCtxt->zx(
773 this->architecture->getRegister(reg).getBitSize() - 8,
774 this->astCtxt->extract(
775 7,
776 0,
777 this->getRegisterAst(this->architecture->getRegister(reg))
778 )
779 )
780 );
781
783 /* NOTE: Capstone considers this as a viable shift operand but
784 * according to the ARM manual this is not possible.
785 */
786 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): ID_SHIFT_RRX_REG is an invalid shift operand.");
787
788 default:
789 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): Invalid shift operand.");
790 }
791 }
792
793
795 triton::uint32 size = extend.getExtendSize();
796
797 switch (extend.getExtendType()) {
799 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
800
802 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
803
805 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
806
808 return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
809
811 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
812
814 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
815
817 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
818
820 return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
821
822 default:
823 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getExtendAst(): Invalid extend operand.");
824 }
825 }
826
827
828 /* Returns the AST corresponding to the immediate */
830 triton::ast::SharedAbstractNode node = this->astCtxt->bv(imm.getValue(), imm.getBitSize());
831
832 /* Shift AST if it's a shift operand */
834 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(imm), node);
835 }
836
837 return node;
838 }
839
840
841 /* Returns the AST corresponding to the immediate and defines the immediate as input of the instruction */
844 inst.setReadImmediate(imm, node);
845 return node;
846 }
847
848
849 /* Returns the AST corresponding to the memory */
851 std::vector<triton::ast::SharedAbstractNode> cells;
852
854 triton::uint64 address = mem.getAddress();
855 triton::uint32 size = mem.getSize();
856 triton::uint8 raw[64] = {0};
857 triton::uint512 value = this->architecture->getConcreteMemoryValue(mem);
858
859 /* Convert the integer value to a raw buffer */
861
862 /*
863 * Symbolic optimization
864 * If the memory access is aligned, don't split the memory.
865 */
866 if (this->isArrayMode() == false && this->isAlignedMode() && this->isAlignedMemory(address, size)) {
867 return this->getAlignedMemory(address, size)->getAst();
868 }
869
870 cells.reserve(size);
871 while (size) {
872 /* Symbolic Array */
873 if (this->isArrayMode()) {
874 auto gpr_size = this->architecture->gprBitSize();
875 auto memor_ea = mem.getLeaAst() != nullptr ? mem.getLeaAst() : this->astCtxt->bv(address, gpr_size);
876 auto final_ea = this->astCtxt->bvadd(memor_ea, this->astCtxt->bv(size - 1, gpr_size));
877
878 /* Symbolic mode: Should we concretize memory indexing? */
879 if (this->modes->isModeEnabled(triton::modes::SYMBOLIZE_LOAD) == false) {
880 final_ea = this->astCtxt->bv(final_ea->evaluate(), gpr_size);
881 }
882
883 cells.push_back(this->astCtxt->select(this->astCtxt->reference(this->getMemoryArray()), final_ea));
884 }
885 /* Symbolic Bitvector */
886 else {
887 const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address + size - 1);
888 if (symMem) cells.push_back(this->astCtxt->reference(symMem));
889 else cells.push_back(this->astCtxt->bv(raw[size - 1], bitsize::byte));
890 }
891 size--;
892 }
893
894 /* If size is 1, return the memory cell */
895 if (cells.size() == 1) {
896 return cells.back();
897 }
898
899 /* Otherwise concat them all */
900 return this->astCtxt->concat(cells);
901 }
902
903
904 /* Returns the AST corresponding to the memory and defines the memory as input of the instruction */
907
908 /* Set load access */
909 inst.setLoadAccess(mem, node);
910
911 /* Set implicit read of the base and index registers from an effective address */
912 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
913
914 return node;
915 }
916
917
918 /* Returns the AST corresponding to the register */
920 triton::ast::SharedAbstractNode node = nullptr;
921 triton::uint32 bvSize = reg.getBitSize();
922 triton::uint32 high = reg.getHigh();
923 triton::uint32 low = reg.getLow();
924 triton::uint512 value = this->architecture->getConcreteRegisterValue(reg);
925
926 /* Check if the register is already symbolic */
927 const SharedSymbolicExpression& symReg = this->getSymbolicRegister(reg);
928 if (symReg) node = this->astCtxt->extract(high, low, this->astCtxt->reference(symReg));
929 else node = this->astCtxt->bv(value, bvSize);
930
931 /* extend AST if it's a extend operand (mainly used for AArch64) */
933 return this->getExtendAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
934 }
935
936 /* Shift AST if it's a shift operand (mainly used for Arm) */
938 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
939 }
940
941 return node;
942 }
943
944
945 /* Returns the AST corresponding to the register and defines the register as input of the instruction */
948 inst.setReadRegister(reg, node);
949 return node;
950 }
951
952
953 /* Returns the new symbolic abstract expression and links this expression to the instruction. */
955 switch (dst.getType()) {
956 case triton::arch::OP_MEM: return this->createSymbolicMemoryExpression(inst, node, dst.getConstMemory(), comment);
957 case triton::arch::OP_REG: return this->createSymbolicRegisterExpression(inst, node, dst.getConstRegister(), comment);
958 default:
959 throw triton::exceptions::SymbolicEngine("SymbolicEngine::createSymbolicExpression(): Invalid operand.");
960 }
961 }
962
963
964 /* Returns the new symbolic memory expression */
967 SharedSymbolicExpression se = nullptr;
968 triton::uint64 address = mem.getAddress();
969 triton::uint32 writeSize = mem.getSize();
971
972 /* Record the aligned memory for a symbolic optimization */
973 if (this->isAlignedMode() && this->isArrayMode() == false) {
974 const SharedSymbolicExpression& aligned = this->newSymbolicExpression(node, MEMORY_EXPRESSION, "Aligned optimization - " + comment);
975 aligned->setOriginMemory(mem);
976 this->addAlignedMemory(address, writeSize, aligned);
977 /* Refresh the current id to not link the aligned expression to the instruction */
978 id = this->uniqueSymExprId;
979 }
980
981 /*
982 * As the x86's memory can be accessed without alignment, each byte of the
983 * memory must be assigned to an unique reference.
984 */
985 while (writeSize) {
986 triton::uint32 high = ((writeSize * bitsize::byte) - 1);
987 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte);
988
989 /* Extract each byte of the memory */
990 tmp = this->astCtxt->extract(high, low, node);
991
992 /* Symbolic array */
993 if (this->isArrayMode()) {
994 auto gpr_size = this->architecture->gprBitSize();
995 auto memor_ea = mem.getLeaAst() != nullptr ? mem.getLeaAst() : this->astCtxt->bv(address, gpr_size);
996 auto final_ea = this->astCtxt->bvadd(memor_ea, this->astCtxt->bv(writeSize - 1, gpr_size));
997
998 /* Symbolic mode: Should we concretize memory indexing? */
999 if (this->modes->isModeEnabled(triton::modes::SYMBOLIZE_STORE) == false) {
1000 final_ea = this->astCtxt->bv(final_ea->evaluate(), gpr_size);
1001 }
1002
1003 auto cell = this->astCtxt->store(this->astCtxt->reference(this->getMemoryArray()), final_ea, tmp);
1004 this->memoryArray = this->newSymbolicExpression(cell, MEMORY_EXPRESSION, "Byte reference - " + comment);
1005 this->memoryArray->setOriginMemory(triton::arch::MemoryAccess((address + writeSize) - 1, triton::size::byte));
1006 this->addBitvectorMemory((address + writeSize) - 1, this->memoryArray);
1007 }
1008 /* Symbolic bitvector */
1009 else {
1010 se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference - " + comment);
1011 se->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
1012 this->addBitvectorMemory((address + writeSize) - 1, se);
1013 }
1014
1015 /* continue */
1016 writeSize--;
1017 }
1018
1019 /* Set implicit read of the base and index registers from an effective address */
1020 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
1021
1022 /* Set explicit write of the memory access */
1023 inst.setStoreAccess(mem, node);
1024
1025 /* Synchronize the concrete state */
1026 this->architecture->setConcreteMemoryValue(mem, node->evaluate());
1027
1028 /* Keep a symbolic expression that represents the original store assignment */
1029 se = this->newSymbolicExpression(node, MEMORY_EXPRESSION, "Original memory access - " + comment);
1030 se->setOriginMemory(mem);
1031
1032 return this->addSymbolicExpressions(inst, id);
1033 }
1034
1035
1036 /* Returns the parent AST after inserting the subregister (node) in its AST. */
1037 triton::ast::SharedAbstractNode SymbolicEngine::insertSubRegisterInParent(const triton::arch::Register& reg, const triton::ast::SharedAbstractNode& node, bool zxForAssign) {
1038 const triton::arch::Register& parentReg = this->architecture->getParentRegister(reg);
1039
1040 /* If it's a flag register, there is nothing to do with sub register */
1041 if (this->architecture->isFlag(reg)) {
1042 return node;
1043 }
1044
1045 switch (reg.getSize()) {
1046 /* ----------------------------------------------------------------*/
1047 case triton::size::byte: {
1048 const auto& origReg = this->getRegisterAst(parentReg);
1049 /*
1050 * Mainly used for x86
1051 * r[........xxxxxxxx]
1052 */
1053 if (reg.getLow() == 0) {
1054 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::byte, origReg);
1055 return this->astCtxt->concat(keep, node);
1056 }
1057 /*
1058 * Mainly used for x86
1059 * r[xxxxxxxx........]
1060 */
1061 else {
1062 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg);
1063 return this->astCtxt->concat(keep, this->astCtxt->concat(node, this->astCtxt->extract((bitsize::byte - 1), 0, origReg)));
1064 }
1065 }
1066
1067 /* ----------------------------------------------------------------*/
1068 case triton::size::word: {
1069 const auto& origReg = this->getRegisterAst(parentReg);
1070 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg), node);
1071 }
1072
1073 /* ----------------------------------------------------------------*/
1079 case triton::size::dqqword: {
1080 if (zxForAssign == false) {
1081 if (parentReg.getBitSize() > reg.getBitSize()) {
1082 const auto& origReg = this->getRegisterAst(parentReg);
1083 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), reg.getHigh() + 1, origReg), node);
1084 }
1085 else {
1086 return node;
1087 }
1088 }
1089 /* zxForAssign == true */
1090 else {
1091 return this->astCtxt->zx(parentReg.getBitSize() - node->getBitvectorSize(), node);
1092 }
1093 }
1094 /* ----------------------------------------------------------------*/
1095 }
1096
1097 throw triton::exceptions::SymbolicEngine("SymbolicEngine::insertSubRegisterInParent(): Invalid register size.");
1098 }
1099
1100
1101 /* Returns the new symbolic register expression */
1103 triton::usize id = this->uniqueSymExprId;
1104 SharedSymbolicExpression se = nullptr;
1105
1106 se = this->newSymbolicExpression(this->insertSubRegisterInParent(reg, node), REGISTER_EXPRESSION, comment);
1107 this->assignSymbolicExpressionToRegister(se, this->architecture->getParentRegister(reg));
1108
1109 inst.setWrittenRegister(reg, node);
1110 return this->addSymbolicExpressions(inst, id);
1111 }
1112
1113
1114 /* Returns the new symbolic volatile expression */
1116 triton::usize id = this->uniqueSymExprId;
1117 const SharedSymbolicExpression& se = this->newSymbolicExpression(node, VOLATILE_EXPRESSION, comment);
1118 return this->addSymbolicExpressions(inst, id);
1119 }
1120
1121
1122 /* Adds a symbolic expression to the bitvector memory model */
1123 inline void SymbolicEngine::addBitvectorMemory(triton::uint64 mem, const SharedSymbolicExpression& expr) {
1124 this->memoryBitvector[mem] = expr;
1125 }
1126
1127
1128 /* Assigns a symbolic expression to a register */
1130 const triton::ast::SharedAbstractNode& node = se->getAst();
1131 triton::uint32 id = reg.getParent();
1132
1133 /* We can assign an expression only on parent registers */
1134 if (reg.getId() != id) {
1135 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): We can assign an expression only on parent registers.");
1136 }
1137
1138 /* Check if the size of the symbolic expression is equal to the target register */
1139 if (node->getBitvectorSize() != reg.getBitSize()) {
1140 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): The size of the symbolic expression is not equal to the target register.");
1141 }
1142
1143 se->setType(REGISTER_EXPRESSION);
1144 se->setOriginRegister(reg);
1145
1146 if (reg.isMutable()) {
1147 /* Assign if this register is mutable */
1148 this->symbolicReg[id] = se;
1149 /* Synchronize the concrete state */
1150 this->architecture->setConcreteRegisterValue(reg, node->evaluate());
1151 }
1152 }
1153
1154
1155 /* Assigns a symbolic expression to a memory */
1157 const triton::ast::SharedAbstractNode& node = se->getAst();
1158 triton::uint64 address = mem.getAddress();
1159 triton::uint32 writeSize = mem.getSize();
1160
1161 /* Check if the size of the symbolic expression is equal to the memory access */
1162 if (node->getBitvectorSize() != mem.getBitSize()) {
1163 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToMemory(): The size of the symbolic expression is not equal to the memory access.");
1164 }
1165
1166 /* Record the aligned memory for a symbolic optimization */
1167 if (this->isAlignedMode() && this->isArrayMode() == false) {
1168 this->addAlignedMemory(address, writeSize, se);
1169 }
1170
1171 /*
1172 * As the x86's memory can be accessed without alignment, each byte of the
1173 * memory must be assigned to an unique reference.
1174 */
1175 while (writeSize) {
1176 triton::uint32 high = ((writeSize * bitsize::byte) - 1);
1177 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte);
1178
1179 /* Extract each byte of the memory */
1180 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, node);
1181
1182 /* Symbolic array */
1183 if (this->isArrayMode()) {
1184 const auto& cell = this->astCtxt->store(this->astCtxt->reference(this->getMemoryArray()), ((address + writeSize) - 1), tmp);
1185 this->memoryArray = this->newSymbolicExpression(cell, MEMORY_EXPRESSION, "Byte reference");
1186 this->memoryArray->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
1187 this->addBitvectorMemory((address + writeSize) - 1, this->memoryArray);
1188 }
1189 /* Symbolic bitvector */
1190 else {
1191 const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
1192 se->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
1193 this->addBitvectorMemory((address + writeSize) - 1, se);
1194 }
1195
1196 writeSize--;
1197 }
1198
1199 /* Synchronize the concrete state */
1200 this->architecture->setConcreteMemoryValue(mem, node->evaluate());
1201 }
1202
1203
1204 /* Returns true if the symbolic expression ID exists */
1206 auto it = this->symbolicExpressions.find(symExprId);
1207
1208 if (it != this->symbolicExpressions.end()) {
1209 return (it->second.use_count() > 0);
1210 }
1211
1212 return false;
1213 }
1214
1215
1216 /* Returns true if memory cell expressions contain symbolic variables. */
1218 triton::uint64 addr = mem.getAddress();
1219 triton::uint32 size = mem.getSize();
1220
1221 return this->isMemorySymbolized(addr, size);
1222 }
1223
1224
1225 /* Returns true if memory cell expressions contain symbolic variables. */
1227 for (triton::uint32 i = 0; i < size; i++) {
1228 const SharedSymbolicExpression& expr = this->getSymbolicMemory(addr + i);
1229 if (expr && expr->isSymbolized()) {
1230 return true;
1231 }
1232 }
1233 return false;
1234 }
1235
1236
1237 /* Returns true if the register expression contains a symbolic variable. */
1239 const SharedSymbolicExpression& expr = this->getSymbolicRegister(reg);
1240 if (expr) {
1241 return expr->isSymbolized();
1242 }
1243 return false;
1244 }
1245
1246
1247 /* Initializes the memory access AST (LOAD and STORE) */
1249 if (mem.getBitSize() >= bitsize::byte) {
1250 const triton::arch::Register& base = mem.getConstBaseRegister();
1251 const triton::arch::Register& index = mem.getConstIndexRegister();
1253 triton::uint64 scaleValue = mem.getConstScale().getValue();
1254 triton::uint64 dispValue = mem.getConstDisplacement().getValue();
1255 triton::uint32 bitSize = (this->architecture->isRegisterValid(base) ? base.getBitSize() :
1256 (this->architecture->isRegisterValid(index) ? index.getBitSize() :
1258 this->architecture->gprBitSize()
1259 )
1260 )
1261 );
1262
1263 /* Initialize the AST of the memory access (LEA) -> ((pc + base) + (index * scale) + disp) */
1264 auto pcPlusBaseAst = mem.getPcRelative() ? this->astCtxt->bv(mem.getPcRelative(), bitSize) :
1265 (this->architecture->isRegisterValid(base) ? this->getRegisterAst(base) :
1266 this->astCtxt->bv(0, bitSize));
1267
1268 auto indexMulScaleAst = this->astCtxt->bvmul(
1269 (this->architecture->isRegisterValid(index) ? this->getRegisterAst(index) : this->astCtxt->bv(0, bitSize)),
1270 this->astCtxt->bv(scaleValue, bitSize)
1271 );
1272
1273 auto dispAst = this->astCtxt->bv(dispValue, bitSize);
1274 auto leaAst = this->astCtxt->bvadd(
1275 index.isSubtracted() ? this->astCtxt->bvsub(pcPlusBaseAst, indexMulScaleAst) : this->astCtxt->bvadd(pcPlusBaseAst, indexMulScaleAst),
1276 dispAst
1277 );
1278
1279 /* Use segments as base address instead of selector into the GDT. */
1280 if (this->architecture->isRegisterValid(seg)) {
1281 leaAst = this->astCtxt->bvadd(
1282 this->getRegisterAst(seg),
1283 this->astCtxt->sx((seg.getBitSize() - bitSize), leaAst)
1284 );
1285 }
1286
1287 /* Set AST */
1288 mem.setLeaAst(leaAst);
1289
1290 /* Initialize the address only if it is not already defined */
1291 if (!mem.getAddress() || force)
1292 mem.setAddress(static_cast<triton::uint64>(leaAst->evaluate()));
1293 }
1294 }
1295
1296
1298 return this->astCtxt->getVariableValue(symVar->getName());
1299 }
1300
1301
1303 triton::uint512 max = -1;
1304
1305 /* Check if the value is too big */
1306 max = max >> (512 - symVar->getSize());
1307 if (value > max) {
1308 throw triton::exceptions::SymbolicEngine("SymbolicEngine::setConcreteVariableValue(): Can not set this value (too big) to this symbolic variable.");
1309 }
1310
1311 /* Update the symbolic variable value */
1312 this->astCtxt->updateVariable(symVar->getName(), value);
1313
1314 /* Synchronize concrete state */
1315 if (symVar->getType() == REGISTER_VARIABLE) {
1316 const triton::arch::Register& reg = this->architecture->getRegister(static_cast<triton::arch::register_e>(symVar->getOrigin()));
1317 this->architecture->setConcreteRegisterValue(reg, value);
1318 }
1319
1320 else if (symVar->getType() == MEMORY_VARIABLE && symVar->getSize() && !(symVar->getSize() % bitsize::byte)) {
1321 triton::uint64 addr = symVar->getOrigin();
1322 triton::uint32 size = symVar->getSize() / bitsize::byte;
1324
1325 this->architecture->setConcreteMemoryValue(mem, value);
1326 }
1327 }
1328
1329
1330 inline bool SymbolicEngine::isAlignedMode(void) const {
1331 return this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY);
1332 }
1333
1334
1335 inline bool SymbolicEngine::isArrayMode(void) const {
1336 return this->modes->isModeEnabled(triton::modes::MEMORY_ARRAY);
1337 }
1338
1339 }; /* symbolic namespace */
1340 }; /* engines namespace */
1341}; /*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 triton::ast::SharedAbstractNode getLeaAst(void) const
Returns the AST of the memory access (LEA).
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:95
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 <id : SymbolicExpression>
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 symbolic memory expression expression and links this expression to the instruction.
triton::usize uniqueSymExprId
Symbolic expressions id.
TRITON_EXPORT void concretizeMemory(const triton::arch::MemoryAccess &mem, bool array=true)
Concretizes specific symbolic memory cells.
SharedSymbolicExpression memoryArray
An array memory model.
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.
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 symbolic volatile expression expression and links this expression to the instruction.
TRITON_EXPORT void assignSymbolicExpressionToMemory(const SharedSymbolicExpression &se, const triton::arch::MemoryAccess &mem)
Assigns a symbolic expression to a memory.
std::unordered_map< triton::uint64, SharedSymbolicExpression > memoryBitvector
A bitvector memory model represented by a map of <address:SymbolicExpression>
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 assigned.
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 effective address of a memory access.
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.
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 symbolic 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 symbolic expression.
TRITON_EXPORT const SharedSymbolicExpression & getSymbolicRegister(const triton::arch::Register &reg) const
Returns the symbolic expression assigned to the 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 the symbolic memory.
std::unordered_map< triton::usize, WeakSymbolicVariable > symbolicVariables
The map of symbolic variables <id : SymbolicVariable>
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
The list of all symbolic registers.
TRITON_EXPORT void concretizeAllRegister(void)
Concretizes all symbolic registers.
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.
TRITON_EXPORT triton::ast::SharedAbstractNode getOperandAst(const triton::arch::OperandWrapper &op)
Returns the AST corresponding to the operand.
std::map< std::pair< triton::uint64, triton::uint32 >, SharedSymbolicExpression > alignedBitvectorMemory
The map of aligned symbolic expressions (used for symbolic optimizations) <<addr : size> : SharedSymb...
TRITON_EXPORT bool isRegisterSymbolized(const triton::arch::Register &reg) const
Returns true if the register expression contains a symbolic variable.
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:128
@ ID_SHIFT_LSR_REG
Logical Shift Right (register)
Definition: archEnums.hpp:133
@ ID_SHIFT_ASR
Arithmetic Shift Right (immediate)
Definition: archEnums.hpp:126
@ ID_SHIFT_ROR_REG
Rotate Right (register)
Definition: archEnums.hpp:134
@ ID_SHIFT_ROR
Rotate Right (immediate)
Definition: archEnums.hpp:129
@ ID_SHIFT_ASR_REG
Arithmetic Shift Right (register)
Definition: archEnums.hpp:131
@ ID_SHIFT_RRX
Rotate Right with Extend (immediate)
Definition: archEnums.hpp:130
@ ID_SHIFT_RRX_REG
Rotate Right with Extend (register)
Definition: archEnums.hpp:135
@ ID_SHIFT_LSL_REG
Logical Shift Left (register)
Definition: archEnums.hpp:132
@ ID_SHIFT_INVALID
invalid
Definition: archEnums.hpp:125
@ ID_SHIFT_LSL
Logical Shift Left (immediate)
Definition: archEnums.hpp:127
@ 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:148
@ ID_EXTEND_UXTX
Use the whole 64-bit register.
Definition: archEnums.hpp:145
@ ID_EXTEND_SXTX
Use the whole 64-bit register.
Definition: archEnums.hpp:149
@ 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:147
@ 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:142
@ ID_EXTEND_INVALID
invalid
Definition: archEnums.hpp:141
@ 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:144
@ 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:146
@ 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:143
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:3689
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
@ SYMBOLIZE_STORE
[symbolic] Symbolize memory store if memory array is enabled
Definition: modesEnums.hpp:40
@ ONLY_ON_SYMBOLIZED
[symbolic] Perform symbolic execution only on symbolized expressions.
Definition: modesEnums.hpp:35
@ SYMBOLIZE_LOAD
[symbolic] Symbolize memory load if memory array is enabled
Definition: modesEnums.hpp:39
@ AST_OPTIMIZATIONS
[AST] Classical arithmetic optimisations to reduce the depth of the trees.
Definition: modesEnums.hpp:31
@ MEMORY_ARRAY
[symbolic] Enable memory symbolic array
Definition: modesEnums.hpp:34
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.