1
//! \file
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

11
#include <triton/exceptions.hpp>
12
#include <triton/coreUtils.hpp>
13
#include <triton/symbolicEngine.hpp>
14
#include <triton/astContext.hpp>
15

16

17

18
namespace triton {
19
  namespace engines {
20
    namespace symbolic {
21

22 1
      SymbolicEngine::SymbolicEngine(triton::arch::Architecture* architecture,
23
                                     const triton::modes::SharedModes& modes,
24
                                     const triton::ast::SharedAstContext& astCtxt,
25
                                     triton::callbacks::Callbacks* callbacks)
26
        : triton::engines::symbolic::SymbolicSimplification(callbacks),
27
          triton::engines::symbolic::PathManager(modes, astCtxt),
28
          astCtxt(astCtxt),
29 1
          modes(modes) {
30

31 1
        if (architecture == nullptr) {
32 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::SymbolicEngine(): The architecture pointer must be valid.");
33
        }
34

35 1
        this->architecture      = architecture;
36 1
        this->callbacks         = callbacks;
37 1
        this->enableFlag        = true;
38 1
        this->numberOfRegisters = this->architecture->numberOfRegisters();
39 1
        this->uniqueSymExprId   = 0;
40 1
        this->uniqueSymVarId    = 0;
41

42 1
        this->symbolicReg.resize(this->numberOfRegisters);
43
      }
44

45

46 0
      SymbolicEngine::SymbolicEngine(const SymbolicEngine& other)
47
        : triton::engines::symbolic::SymbolicSimplification(other),
48
          triton::engines::symbolic::PathManager(other),
49
          astCtxt(other.astCtxt),
50 0
          modes(other.modes) {
51

52 0
        this->alignedMemoryReference      = other.alignedMemoryReference;
53 0
        this->architecture                = other.architecture;
54 0
        this->callbacks                   = other.callbacks;
55 0
        this->enableFlag                  = other.enableFlag;
56 0
        this->memoryReference             = other.memoryReference;
57 0
        this->numberOfRegisters           = other.numberOfRegisters;
58 0
        this->symbolicExpressions         = other.symbolicExpressions;
59 0
        this->symbolicReg                 = other.symbolicReg;
60 0
        this->symbolicVariables           = other.symbolicVariables;
61 0
        this->uniqueSymExprId             = other.uniqueSymExprId;
62 0
        this->uniqueSymVarId              = other.uniqueSymVarId;
63
      }
64

65

66 1
      SymbolicEngine::~SymbolicEngine() {
67
        /* See #828: Release ownership before calling container destructor */
68 1
        this->memoryReference.clear();
69 1
        this->symbolicReg.clear();
70
      }
71

72

73 1
      SymbolicEngine& SymbolicEngine::operator=(const SymbolicEngine& other) {
74 1
        triton::engines::symbolic::SymbolicSimplification::operator=(other);
75 1
        triton::engines::symbolic::PathManager::operator=(other);
76

77 1
        this->alignedMemoryReference      = other.alignedMemoryReference;
78 1
        this->architecture                = other.architecture;
79 1
        this->astCtxt                     = other.astCtxt;
80 1
        this->callbacks                   = other.callbacks;
81 1
        this->enableFlag                  = other.enableFlag;
82 1
        this->memoryReference             = other.memoryReference;
83 1
        this->modes                       = other.modes;
84 1
        this->numberOfRegisters           = other.numberOfRegisters;
85 1
        this->symbolicExpressions         = other.symbolicExpressions;
86 1
        this->symbolicReg                 = other.symbolicReg;
87 1
        this->symbolicVariables           = other.symbolicVariables;
88 1
        this->uniqueSymExprId             = other.uniqueSymExprId;
89 1
        this->uniqueSymVarId              = other.uniqueSymVarId;
90

91 1
        return *this;
92
      }
93

94

95
      /*
96
       * Concretize a register. If the register is setup as nullptr, the next assignment
97
       * will be over the concretization. This method must be called before symbolic
98
       * processing.
99
       */
100 1
      void SymbolicEngine::concretizeRegister(const triton::arch::Register& reg) {
101 1
        triton::arch::register_e parentId = reg.getParent();
102

103 1
        if (this->architecture->isRegisterValid(parentId)) {
104 1
          this->symbolicReg[parentId] = nullptr;
105
        }
106
      }
107

108

109
      /* Same as concretizeRegister but with all registers */
110 1
      void SymbolicEngine::concretizeAllRegister(void) {
111 1
        for (triton::uint32 i = 0; i < this->numberOfRegisters; i++) {
112 1
          this->symbolicReg[i] = nullptr;
113
        }
114
      }
115

116

117
      /*
118
       * Concretize a memory. If the memory is not found into the map, the next
119
       * assignment will be over the concretization. This method must be called
120
       * before symbolic processing.
121
       */
122 1
      void SymbolicEngine::concretizeMemory(const triton::arch::MemoryAccess& mem) {
123 1
        triton::uint64 addr = mem.getAddress();
124 1
        triton::uint32 size = mem.getSize();
125

126 1
        for (triton::uint32 index = 0; index < size; index++) {
127 1
          this->concretizeMemory(addr+index);
128
        }
129
      }
130

131

132
      /*
133
       * Concretize a memory. If the memory is not found into the map, the next
134
       * assignment will be over the concretization. This method must be called
135
       * before symbolic processing.
136
       */
137 1
      void SymbolicEngine::concretizeMemory(triton::uint64 addr) {
138 1
        this->memoryReference.erase(addr);
139 1
        this->removeAlignedMemory(addr, triton::size::byte);
140
      }
141

142

143
      /* Same as concretizeMemory but with all address memory */
144 1
      void SymbolicEngine::concretizeAllMemory(void) {
145 1
        this->memoryReference.clear();
146 1
        this->alignedMemoryReference.clear();
147
      }
148

149

150
      /* Gets an aligned entry. */
151 1
      const SharedSymbolicExpression& SymbolicEngine::getAlignedMemory(triton::uint64 address, triton::uint32 size) {
152 1
        return this->alignedMemoryReference[std::make_pair(address, size)];
153
      }
154

155

156
      /* Checks if the aligned memory is recored. */
157 1
      bool SymbolicEngine::isAlignedMemory(triton::uint64 address, triton::uint32 size) {
158 1
        if (this->alignedMemoryReference.find(std::make_pair(address, size)) != this->alignedMemoryReference.end()) {
159
          return true;
160
        }
161 1
        return false;
162
      }
163

164

165
      /* Adds an aligned memory */
166 1
      void SymbolicEngine::addAlignedMemory(triton::uint64 address, triton::uint32 size, const SharedSymbolicExpression& expr) {
167 1
        this->removeAlignedMemory(address, size);
168 1
        if (!(this->modes->isModeEnabled(triton::modes::ONLY_ON_SYMBOLIZED) && expr->getAst()->isSymbolized() == false)) {
169 1
          this->alignedMemoryReference[std::make_pair(address, size)] = expr;
170
        }
171
      }
172

173

174
      /* Removes an aligned memory */
175 1
      void SymbolicEngine::removeAlignedMemory(triton::uint64 address, triton::uint32 size) {
176
        /* Remove overloaded positive ranges */
177 1
        for (triton::uint32 index = 0; index < size; index++) {
178 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::byte));
179 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::word));
180 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dword));
181 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qword));
182 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqword));
183 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qqword));
184 1
          this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqqword));
185
        }
186

187
        /* Remove overloaded negative ranges */
188 1
        for (triton::uint32 index = 1; index < triton::size::dqqword; index++) {
189 1
          if (index < triton::size::word)    this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::word));
190 1
          if (index < triton::size::dword)   this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dword));
191 1
          if (index < triton::size::qword)   this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qword));
192 1
          if (index < triton::size::dqword)  this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dqword));
193 1
          if (index < triton::size::qqword)  this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qqword));
194 1
          if (index < triton::size::dqqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dqqword));
195
        }
196
      }
197

198

199
      /* Returns the reference memory if it's referenced otherwise returns nullptr */
200 1
      SharedSymbolicExpression SymbolicEngine::getSymbolicMemory(triton::uint64 addr) const {
201 1
        auto it = this->memoryReference.find(addr);
202 1
        if (it != this->memoryReference.end()) {
203 1
          return it->second;
204
        }
205 1
        return nullptr;
206
      }
207

208

209
      /* Returns the symbolic variable otherwise raises an exception */
210 1
      SharedSymbolicVariable SymbolicEngine::getSymbolicVariable(triton::usize symVarId) const {
211 1
        auto it = this->symbolicVariables.find(symVarId);
212 1
        if (it == this->symbolicVariables.end()) {
213 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred symbolic variable.");
214
        }
215

216 1
        if (auto node = it->second.lock()) {
217 1
          return node;
218
        }
219

220 0
        throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): This symbolic variable is dead.");
221
      }
222

223

224
      /* Returns the symbolic variable otherwise returns nullptr */
225 1
      SharedSymbolicVariable SymbolicEngine::getSymbolicVariable(const std::string& symVarName) const {
226
        /*
227
         * FIXME: When there is a ton of symvar, this loop takes a while to go through.
228
         *        What about adding two maps {id:symvar} and {string:symvar}? See #648.
229
         */
230 1
        for (auto& sv: this->symbolicVariables) {
231 1
          if (auto symVar = sv.second.lock()) {
232 1
            if (symVar->getName() == symVarName) {
233 1
              return symVar;
234
            }
235
          }
236
        }
237 0
        throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred or dead symbolic variable.");
238
      }
239

240

241
      /* Returns all symbolic variables */
242 1
      std::unordered_map<triton::usize, SharedSymbolicVariable> SymbolicEngine::getSymbolicVariables(void) const {
243
        // Copy and clean up dead weak ref
244 1
        std::unordered_map<triton::usize, SharedSymbolicVariable> ret;
245 1
        std::vector<triton::usize> toRemove;
246

247 1
        for (auto& kv : this->symbolicVariables) {
248 1
          if (auto sp = kv.second.lock()) {
249 1
            ret[kv.first] = sp;
250
          } else {
251 0
            toRemove.push_back(kv.first);
252
          }
253
        }
254

255 1
        for (triton::usize id : toRemove) {
256 0
          this->symbolicVariables.erase(id);
257
        }
258

259 1
        return ret;
260
      }
261

262

263 1
      void SymbolicEngine::setImplicitReadRegisterFromEffectiveAddress(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) {
264
        /* Set implicit read of the base register (LEA) */
265 1
        if (this->architecture->isRegisterValid(mem.getConstBaseRegister())) {
266 1
          (void)this->getRegisterAst(inst, mem.getConstBaseRegister());
267
        }
268

269
        /* Set implicit read of the index register (LEA) */
270 1
        if (this->architecture->isRegisterValid(mem.getConstIndexRegister())) {
271 1
          (void)this->getRegisterAst(inst, mem.getConstIndexRegister());
272
        }
273
      }
274

275

276
      /* Returns the shared symbolic expression corresponding to the register */
277 1
      const SharedSymbolicExpression& SymbolicEngine::getSymbolicRegister(const triton::arch::Register& reg) const {
278 1
        triton::arch::register_e parentId = reg.getParent();
279

280 1
        if (this->architecture->isRegisterValid(parentId)) {
281 1
          return this->symbolicReg.at(parentId);
282
        }
283

284 0
        throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicRegister(): Invalid Register");
285
      }
286

287

288
      /* Returns the symbolic address value */
289 0
      triton::uint8 SymbolicEngine::getSymbolicMemoryValue(triton::uint64 address) {
290 0
        triton::arch::MemoryAccess mem(address, triton::size::byte);
291 0
        return this->getSymbolicMemoryValue(mem).convert_to<triton::uint8>();
292
      }
293

294

295
      /* Returns the symbolic memory value */
296 1
      triton::uint512 SymbolicEngine::getSymbolicMemoryValue(const triton::arch::MemoryAccess& mem) {
297 1
        const triton::ast::SharedAbstractNode& node = this->getMemoryAst(mem);
298 1
        return node->evaluate();
299
      }
300

301

302
      /* Returns the symbolic values of a memory area */
303 0
      std::vector<triton::uint8> SymbolicEngine::getSymbolicMemoryAreaValue(triton::uint64 baseAddr, triton::usize size) {
304 0
        std::vector<triton::uint8> area;
305

306 0
        area.reserve(size);
307 0
        for (triton::usize index = 0; index < size; index++) {
308 0
          area.push_back(this->getSymbolicMemoryValue(baseAddr + index));
309
        }
310

311 0
        return area;
312
      }
313

314

315
      /* Returns the symbolic register value */
316 1
      triton::uint512 SymbolicEngine::getSymbolicRegisterValue(const triton::arch::Register& reg) {
317 1
        return this->getRegisterAst(reg)->evaluate();
318
      }
319

320

321
      /* Creates a new symbolic expression */
322
      /* Get an unique id.
323
       * Mainly used when a new symbolic expression is created */
324 1
      triton::usize SymbolicEngine::getUniqueSymExprId(void) {
325 1
        return this->uniqueSymExprId++;
326
      }
327

328

329
      /* Creates a new symbolic variable */
330
      /* Get an unique id.
331
       * Mainly used when a new symbolic variable is created */
332 1
      triton::usize SymbolicEngine::getUniqueSymVarId(void) {
333 1
        return this->uniqueSymVarId++;
334
      }
335

336

337
      /* Creates a new symbolic expression with comment */
338 1
      SharedSymbolicExpression SymbolicEngine::newSymbolicExpression(const triton::ast::SharedAbstractNode& node, triton::engines::symbolic::expression_e type, const std::string& comment) {
339 1
        if (this->modes->isModeEnabled(triton::modes::AST_OPTIMIZATIONS)) {
340
          /*
341
           * Create volatile expression for extended part to avoid long
342
           * formulas while printing. Long formulas are introduced by
343
           * optimizations of AstContext::concat and AstContext::extract
344
           */
345 1
          if (node->getType() == triton::ast::ZX_NODE || node->getType() == triton::ast::SX_NODE) {
346 1
            auto n = node->getChildren()[1];
347 1
            if (n->getType() != triton::ast::REFERENCE_NODE && n->getType() != triton::ast::VARIABLE_NODE) {
348 1
              auto e = this->newSymbolicExpression(n, VOLATILE_EXPRESSION, "Extended part - " + comment);
349 1
              node->setChild(1, this->astCtxt->reference(e));
350
            }
351
          }
352
        }
353

354
        /* Each symbolic expression must have an unique id */
355 1
        triton::usize id = this->getUniqueSymExprId();
356

357
        /* Performes transformation if there are rules recorded */
358 1
        const triton::ast::SharedAbstractNode& snode = this->processSimplification(node);
359

360
        /* Allocates the new shared symbolic expression */
361 1
        SharedSymbolicExpression expr = std::make_shared<SymbolicExpression>(snode, id, type, comment);
362 1
        if (expr == nullptr) {
363 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicExpression(): not enough memory");
364
        }
365

366
        /* Save and returns the new shared symbolic expression */
367 1
        this->symbolicExpressions[id] = expr;
368 1
        return expr;
369
      }
370

371

372
      /* Removes the symbolic expression corresponding to the id */
373 1
      void SymbolicEngine::removeSymbolicExpression(const SharedSymbolicExpression& expr) {
374 1
        if (this->symbolicExpressions.find(expr->getId()) != this->symbolicExpressions.end()) {
375
          /* Concretize memory */
376 1
          if (expr->getType() == MEMORY_EXPRESSION) {
377 1
            const auto& mem = expr->getOriginMemory();
378 1
            this->concretizeMemory(mem);
379
          }
380

381
          /* Concretize register */
382 1
          else if (expr->getType() == REGISTER_EXPRESSION) {
383 1
            const auto& reg = expr->getOriginRegister();
384 1
            this->concretizeRegister(reg);
385
          }
386

387
          /* Delete and remove the pointer */
388 1
          this->symbolicExpressions.erase(expr->getId());
389
        }
390
      }
391

392

393
      /* Gets the shared symbolic expression from a symbolic id */
394 1
      SharedSymbolicExpression SymbolicEngine::getSymbolicExpression(triton::usize symExprId) const {
395 1
        auto it = this->symbolicExpressions.find(symExprId);
396 1
        if (it == this->symbolicExpressions.end()) {
397 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression id not found");
398
        }
399

400 1
        if (auto sp = it->second.lock()) {
401 1
          return sp;
402
        }
403

404 0
        this->symbolicExpressions.erase(symExprId);
405 0
        throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression is not available anymore");
406
      }
407

408

409
      /* Returns all symbolic expressions */
410 1
      std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::getSymbolicExpressions(void) const {
411
        // Copy and clean up dead weak ref
412 1
        std::unordered_map<triton::usize, SharedSymbolicExpression> ret;
413 1
        std::vector<triton::usize> toRemove;
414

415 1
        for (auto& kv : this->symbolicExpressions) {
416 1
          if (auto sp = kv.second.lock()) {
417 1
            ret[kv.first] = sp;
418
          } else {
419 0
            toRemove.push_back(kv.first);
420
          }
421
        }
422

423 1
        for (auto id : toRemove)
424 0
          this->symbolicExpressions.erase(id);
425

426 1
        return ret;
427
      }
428

429

430
      /* Slices all expressions from a given one */
431 1
      std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::sliceExpressions(const SharedSymbolicExpression& expr) {
432 1
        std::unordered_map<triton::usize, SharedSymbolicExpression> exprs;
433

434 1
        if (expr == nullptr) {
435 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::sliceExpressions(): expr cannot be null.");
436
        }
437

438 1
        exprs[expr->getId()] = expr;
439

440 1
        auto worklist = triton::ast::childrenExtraction(expr->getAst(), true /* unroll */, false /* revert */);
441 1
        for (auto&& n : worklist) {
442 1
          if (n->getType() == triton::ast::REFERENCE_NODE) {
443 1
            auto expr  = reinterpret_cast<triton::ast::ReferenceNode*>(n.get())->getSymbolicExpression();
444 1
            auto eid   = expr->getId();
445 1
            exprs[eid] = expr;
446
          }
447
        }
448

449 1
        return exprs;
450
      }
451

452

453
      /* Prints symbolic expression with used references and symbolic variables */
454 0
      std::ostream& SymbolicEngine::printSlicedExpressions(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_) {
455 0
        auto symVars = this->getSymbolicVariables();
456 0
        auto ssa = this->sliceExpressions(expr);
457

458 0
        std::vector<usize> ids;
459 0
        ids.reserve(std::max(symVars.size(), ssa.size()));
460 0
        for (const auto& symVar : symVars) {
461 0
          ids.push_back(symVar.first);
462
        }
463

464 0
        std::sort(ids.begin(), ids.end());
465 0
        for (const auto& id : ids) {
466 0
          auto n = this->astCtxt->declare(this->astCtxt->variable(symVars[id]));
467 0
          this->astCtxt->print(stream, n.get());
468 0
          stream << std::endl;
469
        }
470

471 0
        ids.clear();
472 0
        for (const auto& se : ssa) {
473 0
          ids.push_back(se.first);
474
        }
475

476 0
        std::sort(ids.begin(), ids.end());
477 0
        if (assert_) {
478 0
          ids.pop_back();
479
        }
480

481 0
        for (const auto& id : ids) {
482 0
          stream << ssa[id]->getFormattedExpression() << std::endl;
483
        }
484

485 0
        if (assert_) {
486
          /* Print conjuncts in separate asserts */
487 0
          std::vector<triton::ast::SharedAbstractNode> exprs;
488 0
          std::vector<triton::ast::SharedAbstractNode> wl{expr->getAst()};
489

490 0
          while (!wl.empty()) {
491 0
            auto n = wl.back();
492 0
            wl.pop_back();
493

494 0
            if (n->getType() != triton::ast::LAND_NODE) {
495 0
              exprs.push_back(n);
496 0
              continue;
497
            }
498

499 0
            for (const auto& child : n->getChildren()) {
500 0
              wl.push_back(child);
501
            }
502
          }
503

504 0
          for (auto it = exprs.crbegin(); it != exprs.crend(); ++it) {
505 0
            this->astCtxt->print(stream, this->astCtxt->assert_(*it).get());
506
            stream << std::endl;
507
          }
508

509 0
          if (this->astCtxt->getRepresentationMode() == ast::representations::SMT_REPRESENTATION) {
510 0
            stream << "(check-sat)" << std::endl;
511 0
            stream << "(get-model)" << std::endl;
512
          }
513
        }
514

515 0
        return stream;
516
      }
517

518

519
      /* Returns a list which contains all tainted expressions */
520 0
      std::vector<SharedSymbolicExpression> SymbolicEngine::getTaintedSymbolicExpressions(void) const {
521 0
        std::vector<SharedSymbolicExpression> taintedExprs;
522 0
        std::vector<triton::usize> invalidSymExpr;
523

524 0
        for (auto it = this->symbolicExpressions.begin(); it != this->symbolicExpressions.end(); it++) {
525 0
          if (auto sp = it->second.lock()) {
526 0
            if (sp->isTainted) {
527 0
              taintedExprs.push_back(sp);
528
            }
529
          } else {
530 0
            invalidSymExpr.push_back(it->first);
531
          }
532
        }
533

534 0
        for (auto id : invalidSymExpr) {
535 0
          this->symbolicExpressions.erase(id);
536
        }
537

538 0
        return taintedExprs;
539
      }
540

541

542
      /* Returns the map of symbolic registers defined */
543 1
      std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> SymbolicEngine::getSymbolicRegisters(void) const {
544 1
        std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> ret;
545

546 1
        for (triton::uint32 it = 0; it < this->numberOfRegisters; it++) {
547 1
          if (this->symbolicReg[it] != nullptr) {
548 1
            ret[triton::arch::register_e(it)] = this->symbolicReg[it];
549
          }
550
        }
551

552 1
        return ret;
553
      }
554

555

556
      /* Returns the map of symbolic memory defined */
557 1
      const std::unordered_map<triton::uint64, SharedSymbolicExpression>& SymbolicEngine::getSymbolicMemory(void) const {
558 1
        return this->memoryReference;
559
      }
560

561

562
      /*
563
       * Converts an expression id to a symbolic variable.
564
       * e.g:
565
       * #43 = (_ bv10 8)
566
       * symbolizeExpression(43, 8)
567
       * #43 = SymVar_4
568
       */
569 0
      SharedSymbolicVariable SymbolicEngine::symbolizeExpression(triton::usize exprId, triton::uint32 symVarSize, const std::string& symVarAlias) {
570 0
        const SharedSymbolicExpression& expression = this->getSymbolicExpression(exprId);
571 0
        const SharedSymbolicVariable& symVar       = this->newSymbolicVariable(UNDEFINED_VARIABLE, 0, symVarSize, symVarAlias);
572 0
        const triton::ast::SharedAbstractNode& tmp = this->astCtxt->variable(symVar);
573

574 0
        if (expression->getAst()) {
575 0
           this->setConcreteVariableValue(symVar, expression->getAst()->evaluate());
576
        }
577

578 0
        expression->setAst(tmp);
579

580 0
        return symVar;
581
      }
582

583

584
      /* The memory size is used to define the symbolic variable's size. */
585 1
      SharedSymbolicVariable SymbolicEngine::symbolizeMemory(const triton::arch::MemoryAccess& mem, const std::string& symVarAlias) {
586 1
        triton::uint64 memAddr    = mem.getAddress();
587 1
        triton::uint32 symVarSize = mem.getSize();
588 1
        triton::uint512 cv        = this->architecture->getConcreteMemoryValue(mem);
589

590
        /* First we create a symbolic variable */
591 1
        const SharedSymbolicVariable& symVar = this->newSymbolicVariable(MEMORY_VARIABLE, memAddr, symVarSize * bitsize::byte, symVarAlias);
592

593
        /* Create the AST node */
594 1
        const triton::ast::SharedAbstractNode& symVarNode = this->astCtxt->variable(symVar);
595

596
        /* Setup the concrete value to the symbolic variable */
597 1
        this->setConcreteVariableValue(symVar, cv);
598

599
        /* Record the aligned symbolic variable for a symbolic optimization */
600 1
        if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
601 1
          const SharedSymbolicExpression& se = this->newSymbolicExpression(symVarNode, MEMORY_EXPRESSION, "aligned Byte reference");
602 1
          se->setOriginMemory(mem);
603 1
          this->addAlignedMemory(memAddr, symVarSize, se);
604
        }
605

606
        /*  Split expression in bytes */
607 1
        for (triton::sint32 index = symVarSize-1; index >= 0; index--) {
608 1
          triton::uint32 high = ((bitsize::byte * (index + 1)) - 1);
609 1
          triton::uint32 low  = ((bitsize::byte * (index + 1)) - bitsize::byte);
610

611
          /* Isolate the good part of the symbolic variable */
612 1
          const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, symVarNode);
613

614
          /* Create a new symbolic expression containing the symbolic variable */
615 1
          const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
616 1
          se->setOriginMemory(triton::arch::MemoryAccess(memAddr+index, triton::size::byte));
617

618
          /* Assign the symbolic expression to the memory cell */
619 1
          this->addMemoryReference(memAddr+index, se);
620
        }
621

622 1
        return symVar;
623
      }
624

625

626 1
      SharedSymbolicVariable SymbolicEngine::symbolizeRegister(const triton::arch::Register& reg, const std::string& symVarAlias) {
627 1
        const triton::arch::Register& parent  = this->architecture->getRegister(reg.getParent());
628 1
        triton::uint32 symVarSize             = reg.getBitSize();
629 1
        triton::uint512 cv                    = this->architecture->getConcreteRegisterValue(reg);
630

631 1
        if (!this->architecture->isRegisterValid(parent.getId()))
632 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): Invalid register id");
633

634 1
        if (reg.isMutable() == false)
635 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): This register is immutable");
636

637
        /* Create the symbolic variable */
638 1
        const SharedSymbolicVariable& symVar = this->newSymbolicVariable(REGISTER_VARIABLE, reg.getId(), symVarSize, symVarAlias);
639

640
        /* Create the AST node */
641 1
        const triton::ast::SharedAbstractNode& tmp = this->insertSubRegisterInParent(reg, this->astCtxt->variable(symVar), false);
642

643
        /* Setup the concrete value to the symbolic variable */
644 1
        this->setConcreteVariableValue(symVar, cv);
645

646
        /* Create a new symbolic expression containing the symbolic variable */
647 1
        const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, REGISTER_EXPRESSION);
648

649
        /* Assign the symbolic expression to the register */
650 1
        this->assignSymbolicExpressionToRegister(se, parent);
651

652 1
        return symVar;
653
      }
654

655

656
      /* Adds a new symbolic variable */
657 1
      SharedSymbolicVariable SymbolicEngine::newSymbolicVariable(triton::engines::symbolic::variable_e type, triton::uint64 origin, triton::uint32 size, const std::string& alias) {
658 1
        triton::usize uniqueId = this->getUniqueSymVarId();
659

660 1
        SharedSymbolicVariable symVar = std::make_shared<SymbolicVariable>(type, origin, uniqueId, size, alias);
661 1
        if (symVar == nullptr) {
662 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicVariable(): Cannot allocate a new symbolic variable");
663
        }
664

665 1
        this->symbolicVariables[uniqueId] = symVar;
666 1
        return symVar;
667
      }
668

669

670
      /* Returns the AST corresponding to the operand. */
671 1
      triton::ast::SharedAbstractNode SymbolicEngine::getOperandAst(const triton::arch::OperandWrapper& op) {
672 1
        switch (op.getType()) {
673 1
          case triton::arch::OP_IMM: return this->getImmediateAst(op.getConstImmediate());
674 0
          case triton::arch::OP_MEM: return this->getMemoryAst(op.getConstMemory());
675 1
          case triton::arch::OP_REG: return this->getRegisterAst(op.getConstRegister());
676
          default:
677 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
678
        }
679
      }
680

681

682
      /* Returns the AST corresponding to the operand. */
683 1
      triton::ast::SharedAbstractNode SymbolicEngine::getOperandAst(triton::arch::Instruction& inst, const triton::arch::OperandWrapper& op) {
684 1
        switch (op.getType()) {
685 1
          case triton::arch::OP_IMM: return this->getImmediateAst(inst, op.getConstImmediate());
686 1
          case triton::arch::OP_MEM: return this->getMemoryAst(inst, op.getConstMemory());
687 1
          case triton::arch::OP_REG: return this->getRegisterAst(inst, op.getConstRegister());
688
          default:
689 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand.");
690
        }
691
      }
692

693

694 1
      triton::ast::SharedAbstractNode SymbolicEngine::getShiftAst(const triton::arch::arm::ArmOperandProperties& shift, const triton::ast::SharedAbstractNode& node) {
695 1
        auto imm = shift.getShiftImmediate();
696 1
        auto reg = shift.getShiftRegister();
697

698 1
        switch (shift.getShiftType()) {
699
          case triton::arch::arm::ID_SHIFT_ASR:
700 1
            return this->astCtxt->bvashr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
701

702
          case triton::arch::arm::ID_SHIFT_LSL:
703 1
            return this->astCtxt->bvshl(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
704

705
          case triton::arch::arm::ID_SHIFT_LSR:
706 1
            return this->astCtxt->bvlshr(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
707

708
          case triton::arch::arm::ID_SHIFT_ROR:
709 1
            return this->astCtxt->bvror(node, this->astCtxt->bv(imm, node->getBitvectorSize()));
710

711
          case triton::arch::arm::ID_SHIFT_RRX: /* Arm32 only. */
712
            return this->astCtxt->extract(
713
                      node->getBitvectorSize(),
714
                      1,
715 1
                      this->astCtxt->bvror(
716 1
                        this->astCtxt->concat(
717
                          node,
718 1
                          this->getRegisterAst(this->architecture->getRegister(triton::arch::ID_REG_ARM32_C))
719
                        ),
720
                        1
721
                      )
722 1
                    );
723

724
          case triton::arch::arm::ID_SHIFT_ASR_REG: /* Arm32 only. */
725
            return this->astCtxt->bvashr(
726
                      node,
727 1
                      this->astCtxt->zx(
728 1
                        this->architecture->getRegister(reg).getBitSize() - 8,
729 1
                        this->astCtxt->extract(
730
                          7,
731
                          0,
732 1
                          this->getRegisterAst(this->architecture->getRegister(reg))
733
                        )
734
                      )
735 1
                    );
736

737
          case triton::arch::arm::ID_SHIFT_LSL_REG: /* Arm32 only. */
738
            return this->astCtxt->bvshl(
739
                      node,
740 1
                      this->astCtxt->zx(
741 1
                        this->architecture->getRegister(reg).getBitSize() - 8,
742 1
                        this->astCtxt->extract(
743
                          7,
744
                          0,
745 1
                          this->getRegisterAst(this->architecture->getRegister(reg))
746
                        )
747
                      )
748 1
                    );
749

750
          case triton::arch::arm::ID_SHIFT_LSR_REG: /* Arm32 only. */
751
            return this->astCtxt->bvlshr(
752
                      node,
753 1
                      this->astCtxt->zx(
754 1
                        this->architecture->getRegister(reg).getBitSize() - 8,
755 1
                        this->astCtxt->extract(
756
                          7,
757
                          0,
758 1
                          this->getRegisterAst(this->architecture->getRegister(reg))
759
                        )
760
                      )
761 1
                    );
762

763
          case triton::arch::arm::ID_SHIFT_ROR_REG: /* Arm32 only. */
764
            return this->astCtxt->bvror(
765
                      node,
766 1
                      this->astCtxt->zx(
767 1
                        this->architecture->getRegister(reg).getBitSize() - 8,
768 1
                        this->astCtxt->extract(
769
                          7,
770
                          0,
771 1
                          this->getRegisterAst(this->architecture->getRegister(reg))
772
                        )
773
                      )
774 1
                    );
775

776
          case triton::arch::arm::ID_SHIFT_RRX_REG:
777
            /* NOTE: Capstone considers this as a viable shift operand but
778
             * according to the ARM manual this is not possible.
779
             */
780 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): ID_SHIFT_RRX_REG is an invalid shift operand.");
781

782
          default:
783 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): Invalid shift operand.");
784
        }
785
      }
786

787

788 1
      triton::ast::SharedAbstractNode SymbolicEngine::getExtendAst(const triton::arch::arm::ArmOperandProperties& extend, const triton::ast::SharedAbstractNode& node) {
789 1
        triton::uint32 size = extend.getExtendSize();
790

791 1
        switch (extend.getExtendType()) {
792
          case triton::arch::arm::ID_EXTEND_UXTB:
793 0
            return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
794

795
          case triton::arch::arm::ID_EXTEND_UXTH:
796 0
            return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
797

798
          case triton::arch::arm::ID_EXTEND_UXTW:
799 1
            return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
800

801
          case triton::arch::arm::ID_EXTEND_UXTX:
802 0
            return this->astCtxt->zx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
803

804
          case triton::arch::arm::ID_EXTEND_SXTB:
805 1
            return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(7, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 8)));
806

807
          case triton::arch::arm::ID_EXTEND_SXTH:
808 1
            return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(15, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 16)));
809

810
          case triton::arch::arm::ID_EXTEND_SXTW:
811 1
            return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(31, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 32)));
812

813
          case triton::arch::arm::ID_EXTEND_SXTX:
814 1
            return this->astCtxt->sx(size, this->astCtxt->bvshl(this->astCtxt->extract(63, 0, node), this->astCtxt->bv(extend.getShiftImmediate(), 64)));
815

816
          default:
817 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::getExtendAst(): Invalid extend operand.");
818
        }
819
      }
820

821

822
      /* Returns the AST corresponding to the immediate */
823 1
      triton::ast::SharedAbstractNode SymbolicEngine::getImmediateAst(const triton::arch::Immediate& imm) {
824 1
        triton::ast::SharedAbstractNode node = this->astCtxt->bv(imm.getValue(), imm.getBitSize());
825

826
        /* Shift AST if it's a shift operand */
827 1
        if (imm.getShiftType() != triton::arch::arm::ID_SHIFT_INVALID) {
828 1
          return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(imm), node);
829
        }
830

831
        return node;
832
      }
833

834

835
      /* Returns the AST corresponding to the immediate and defines the immediate as input of the instruction */
836 1
      triton::ast::SharedAbstractNode SymbolicEngine::getImmediateAst(triton::arch::Instruction& inst, const triton::arch::Immediate& imm) {
837 1
        triton::ast::SharedAbstractNode node = this->getImmediateAst(imm);
838 1
        inst.setReadImmediate(imm, node);
839 1
        return node;
840
      }
841

842

843
      /* Returns the AST corresponding to the memory */
844 1
      triton::ast::SharedAbstractNode SymbolicEngine::getMemoryAst(const triton::arch::MemoryAccess& mem) {
845 1
        std::vector<triton::ast::SharedAbstractNode> opVec;
846

847 1
        triton::ast::SharedAbstractNode tmp       = nullptr;
848 1
        triton::uint64 address                    = mem.getAddress();
849 1
        triton::uint32 size                       = mem.getSize();
850 1
        triton::uint8 concreteValue[triton::size::dqqword] = {0};
851 1
        triton::uint512 value                     = this->architecture->getConcreteMemoryValue(mem);
852

853 1
        triton::utils::fromUintToBuffer(value, concreteValue);
854

855
        /*
856
         * Symbolic optimization
857
         * If the memory access is aligned, don't split the memory.
858
         */
859 1
        if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY) && this->isAlignedMemory(address, size)) {
860 1
          return this->getAlignedMemory(address, size)->getAst();
861
        }
862

863
        /* If the memory access is 1 byte long, just return the appropriate 8-bit vector */
864 1
        if (size == 1) {
865 1
          const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address);
866 1
          if (symMem) return this->astCtxt->reference(symMem);
867 1
          else        return this->astCtxt->bv(concreteValue[size - 1], bitsize::byte);
868
        }
869

870
        /* If the memory access is more than 1 byte long, concatenate each memory cell */
871 1
        opVec.reserve(size);
872 1
        while (size) {
873 1
          const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address + size - 1);
874 1
          if (symMem) opVec.push_back(this->astCtxt->reference(symMem));
875 1
          else        opVec.push_back(this->astCtxt->bv(concreteValue[size - 1], bitsize::byte));
876 1
          size--;
877
        }
878 1
        return this->astCtxt->concat(opVec);
879
      }
880

881

882
      /* Returns the AST corresponding to the memory and defines the memory as input of the instruction */
883 1
      triton::ast::SharedAbstractNode SymbolicEngine::getMemoryAst(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) {
884 1
        triton::ast::SharedAbstractNode node = this->getMemoryAst(mem);
885

886
        /* Set load access */
887 1
        inst.setLoadAccess(mem, node);
888

889
        /* Set implicit read of the base and index registers from an effective address */
890 1
        this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
891

892 1
        return node;
893
      }
894

895

896
      /* Returns the AST corresponding to the register */
897 1
      triton::ast::SharedAbstractNode SymbolicEngine::getRegisterAst(const triton::arch::Register& reg) {
898 1
        triton::ast::SharedAbstractNode node = nullptr;
899 1
        triton::uint32 bvSize                = reg.getBitSize();
900 1
        triton::uint32 high                  = reg.getHigh();
901 1
        triton::uint32 low                   = reg.getLow();
902 1
        triton::uint512 value                = this->architecture->getConcreteRegisterValue(reg);
903

904
        /* Check if the register is already symbolic */
905 1
        const SharedSymbolicExpression& symReg = this->getSymbolicRegister(reg);
906 1
        if (symReg) node = this->astCtxt->extract(high, low, this->astCtxt->reference(symReg));
907 1
        else        node = this->astCtxt->bv(value, bvSize);
908

909
        /* extend AST if it's a extend operand (mainly used for AArch64) */
910 1
        if (reg.getExtendType() != triton::arch::arm::ID_EXTEND_INVALID) {
911 1
          return this->getExtendAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
912
        }
913

914
        /* Shift AST if it's a shift operand (mainly used for Arm) */
915 1
        if (reg.getShiftType() != triton::arch::arm::ID_SHIFT_INVALID) {
916 1
          return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node);
917
        }
918

919
        return node;
920
      }
921

922

923
      /* Returns the AST corresponding to the register and defines the register as input of the instruction */
924 1
      triton::ast::SharedAbstractNode SymbolicEngine::getRegisterAst(triton::arch::Instruction& inst, const triton::arch::Register& reg) {
925 1
        triton::ast::SharedAbstractNode node = this->getRegisterAst(reg);
926 1
        inst.setReadRegister(reg, node);
927 1
        return node;
928
      }
929

930

931
      /* Returns the new symbolic abstract expression and links this expression to the instruction. */
932 1
      const SharedSymbolicExpression& SymbolicEngine::createSymbolicExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::OperandWrapper& dst, const std::string& comment) {
933 1
        switch (dst.getType()) {
934 1
          case triton::arch::OP_MEM: return this->createSymbolicMemoryExpression(inst, node, dst.getConstMemory(), comment);
935 1
          case triton::arch::OP_REG: return this->createSymbolicRegisterExpression(inst, node, dst.getConstRegister(), comment);
936
          default:
937 0
            throw triton::exceptions::SymbolicEngine("SymbolicEngine::createSymbolicExpression(): Invalid operand.");
938
        }
939
      }
940

941

942
      /* Returns the new symbolic memory expression */
943 1
      const SharedSymbolicExpression& SymbolicEngine::createSymbolicMemoryExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::MemoryAccess& mem, const std::string& comment) {
944 1
        std::vector<triton::ast::SharedAbstractNode> ret;
945 1
        triton::ast::SharedAbstractNode tmp = nullptr;
946 1
        SharedSymbolicExpression se         = nullptr;
947 1
        triton::uint64 address              = mem.getAddress();
948 1
        triton::uint32 writeSize            = mem.getSize();
949

950 1
        std::stringstream s;
951 1
        s << comment << (comment.empty() ? "" : " - ") << inst;
952

953
        /* Record the aligned memory for a symbolic optimization */
954 1
        if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
955 1
          const SharedSymbolicExpression& aligned = this->newSymbolicExpression(node, MEMORY_EXPRESSION, "Aligned Byte reference - " + s.str());
956 1
          this->addAlignedMemory(address, writeSize, aligned);
957
        }
958

959
        /*
960
         * As the x86's memory can be accessed without alignment, each byte of the
961
         * memory must be assigned to an unique reference.
962
         */
963 1
        ret.reserve(mem.getSize());
964 1
        while (writeSize) {
965 1
          triton::uint32 high = ((writeSize * bitsize::byte) - 1);
966 1
          triton::uint32 low  = ((writeSize * bitsize::byte) - bitsize::byte);
967
          /* Extract each byte of the memory */
968 1
          tmp = this->astCtxt->extract(high, low, node);
969
          /* Assign each byte to a new symbolic expression */
970 1
          se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference - " + s.str());
971
          /* Set the origin of the symbolic expression */
972 1
          se->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
973
          /* ret is the for the final expression */
974 1
          ret.push_back(tmp);
975
          /* add the symbolic expression to the instruction */
976 1
          inst.addSymbolicExpression(se);
977
          /* Assign memory with little endian */
978 1
          this->addMemoryReference((address + writeSize) - 1, se);
979
          /* continue */
980 1
          writeSize--;
981
        }
982

983
        /* Set implicit read of the base and index registers from an effective address */
984 1
        this->setImplicitReadRegisterFromEffectiveAddress(inst, mem);
985

986
        /* Set explicit write of the memory access */
987 1
        inst.setStoreAccess(mem, node);
988

989
        /* If there is only one reference, we return the symbolic expression */
990 1
        if (ret.size() == 1) {
991
          /* Synchronize the concrete state */
992 1
          this->architecture->setConcreteMemoryValue(mem, tmp->evaluate());
993
          /* It will return se */
994 1
          return inst.symbolicExpressions.back();
995
        }
996

997
        /* Otherwise, we return the concatenation of all symbolic expressions */
998 1
        tmp = this->astCtxt->concat(ret);
999

1000
        /* Synchronize the concrete state */
1001 1
        this->architecture->setConcreteMemoryValue(mem, tmp->evaluate());
1002

1003 1
        se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Temporary concatenation reference - " + s.str());
1004 1
        se->setOriginMemory(triton::arch::MemoryAccess(address, mem.getSize()));
1005

1006 1
        return inst.addSymbolicExpression(se);
1007
      }
1008

1009

1010
      /* Returns the parent AST after inserting the subregister (node) in its AST. */
1011 1
      triton::ast::SharedAbstractNode SymbolicEngine::insertSubRegisterInParent(const triton::arch::Register& reg, const triton::ast::SharedAbstractNode& node, bool zxForAssign) {
1012 1
        const triton::arch::Register& parentReg = this->architecture->getParentRegister(reg);
1013

1014
        /* If it's a flag register, there is nothing to do with sub register */
1015 1
        if (this->architecture->isFlag(reg)) {
1016
          return node;
1017
        }
1018

1019 1
        switch (reg.getSize()) {
1020
          /* ----------------------------------------------------------------*/
1021
          case triton::size::byte: {
1022 1
            const auto& origReg = this->getRegisterAst(parentReg);
1023
            /*
1024
             * Mainly used for x86
1025
             * r[........xxxxxxxx]
1026
             */
1027 1
            if (reg.getLow() == 0) {
1028 1
              const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::byte, origReg);
1029 1
              return this->astCtxt->concat(keep, node);
1030
            }
1031
            /*
1032
             * Mainly used for x86
1033
             * r[xxxxxxxx........]
1034
             */
1035
            else {
1036 1
              const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg);
1037 1
              return this->astCtxt->concat(keep, this->astCtxt->concat(node, this->astCtxt->extract((bitsize::byte - 1), 0, origReg)));
1038
            }
1039
          }
1040

1041
          /* ----------------------------------------------------------------*/
1042
          case triton::size::word: {
1043 1
            const auto& origReg = this->getRegisterAst(parentReg);
1044 1
            return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg), node);
1045
          }
1046

1047
          /* ----------------------------------------------------------------*/
1048
          case triton::size::dword:
1049
          case triton::size::qword:
1050
          case triton::size::dqword:
1051
          case triton::size::qqword:
1052
          case triton::size::dqqword: {
1053 1
            if (zxForAssign == false) {
1054 1
              if (parentReg.getBitSize() > reg.getBitSize()) {
1055 1
                const auto& origReg = this->getRegisterAst(parentReg);
1056 1
                return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), reg.getHigh() + 1, origReg), node);
1057
              }
1058
              else {
1059
                return node;
1060
              }
1061
            }
1062
            /* zxForAssign == true */
1063
            else {
1064 1
              return this->astCtxt->zx(parentReg.getBitSize() - node->getBitvectorSize(), node);
1065
            }
1066
          }
1067
          /* ----------------------------------------------------------------*/
1068
        }
1069

1070 0
        throw triton::exceptions::SymbolicEngine("SymbolicEngine::insertSubRegisterInParent(): Invalid register size.");
1071
      }
1072

1073

1074
      /* Returns the new symbolic register expression */
1075 1
      const SharedSymbolicExpression& SymbolicEngine::createSymbolicRegisterExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::Register& reg, const std::string& comment) {
1076 1
        SharedSymbolicExpression se = nullptr;
1077

1078 1
        std::stringstream s;
1079 1
        s << comment << (comment.empty() ? "" : " - ") << inst;
1080 1
        se = this->newSymbolicExpression(this->insertSubRegisterInParent(reg, node), REGISTER_EXPRESSION, s.str());
1081 1
        this->assignSymbolicExpressionToRegister(se, this->architecture->getParentRegister(reg));
1082

1083 1
        inst.setWrittenRegister(reg, node);
1084 1
        return inst.addSymbolicExpression(se);
1085
      }
1086

1087

1088
      /* Returns the new symbolic volatile expression */
1089 1
      const SharedSymbolicExpression& SymbolicEngine::createSymbolicVolatileExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const std::string& comment) {
1090 1
        std::stringstream s;
1091 1
        s << comment << (comment.empty() ? "" : " - ") << inst;
1092 1
        const SharedSymbolicExpression& se = this->newSymbolicExpression(node, VOLATILE_EXPRESSION, s.str());
1093 1
        return inst.addSymbolicExpression(se);
1094
      }
1095

1096

1097
      /* Adds and assign a new memory reference */
1098 1
      inline void SymbolicEngine::addMemoryReference(triton::uint64 mem, const SharedSymbolicExpression& expr) {
1099 1
        this->memoryReference[mem] = expr;
1100
      }
1101

1102

1103
      /* Assigns a symbolic expression to a register */
1104 1
      void SymbolicEngine::assignSymbolicExpressionToRegister(const SharedSymbolicExpression& se, const triton::arch::Register& reg) {
1105 1
        const triton::ast::SharedAbstractNode& node = se->getAst();
1106 1
        triton::uint32 id                           = reg.getParent();
1107

1108
        /* We can assign an expression only on parent registers */
1109 1
        if (reg.getId() != id) {
1110 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): We can assign an expression only on parent registers.");
1111
        }
1112

1113
        /* Check if the size of the symbolic expression is equal to the target register */
1114 1
        if (node->getBitvectorSize() != reg.getBitSize()) {
1115 1
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): The size of the symbolic expression is not equal to the target register.");
1116
        }
1117

1118 1
        se->setType(REGISTER_EXPRESSION);
1119 1
        se->setOriginRegister(reg);
1120

1121 1
        if (reg.isMutable()) {
1122
          /* Assign if this register is mutable */
1123 1
          this->symbolicReg[id] = se;
1124
          /* Synchronize the concrete state */
1125 1
          this->architecture->setConcreteRegisterValue(reg, node->evaluate());
1126
        }
1127
      }
1128

1129

1130
      /* Assigns a symbolic expression to a memory */
1131 1
      void SymbolicEngine::assignSymbolicExpressionToMemory(const SharedSymbolicExpression& se, const triton::arch::MemoryAccess& mem) {
1132 1
        const triton::ast::SharedAbstractNode& node = se->getAst();
1133 1
        triton::uint64 address                      = mem.getAddress();
1134 1
        triton::uint32 writeSize                    = mem.getSize();
1135

1136
        /* Check if the size of the symbolic expression is equal to the memory access */
1137 1
        if (node->getBitvectorSize() != mem.getBitSize()) {
1138 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToMemory(): The size of the symbolic expression is not equal to the memory access.");
1139
        }
1140

1141
        /* Record the aligned memory for a symbolic optimization */
1142 1
        if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) {
1143 1
          this->addAlignedMemory(address, writeSize, se);
1144
        }
1145

1146
        /*
1147
         * As the x86's memory can be accessed without alignment, each byte of the
1148
         * memory must be assigned to an unique reference.
1149
         */
1150 1
        while (writeSize) {
1151 1
          triton::uint32 high = ((writeSize * bitsize::byte) - 1);
1152 1
          triton::uint32 low  = ((writeSize * bitsize::byte) - bitsize::byte);
1153
          /* Extract each byte of the memory */
1154 1
          const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, node);
1155
          /* For each byte create a new symbolic expression */
1156 1
          const SharedSymbolicExpression& byteRef = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference");
1157
          /* Set the origin of the symbolic expression */
1158 1
          byteRef->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte));
1159
          /* Assign memory with little endian */
1160 1
          this->addMemoryReference((address + writeSize) - 1, byteRef);
1161
          /* continue */
1162 1
          writeSize--;
1163
        }
1164

1165
        /* Synchronize the concrete state */
1166 1
        this->architecture->setConcreteMemoryValue(mem, node->evaluate());
1167
      }
1168

1169

1170
      /* Returns true if the symbolic engine is enable */
1171 1
      bool SymbolicEngine::isEnabled(void) const {
1172 1
        return this->enableFlag;
1173
      }
1174

1175

1176
      /* Returns true if the symbolic expression ID exists */
1177 0
      bool SymbolicEngine::isSymbolicExpressionExists(triton::usize symExprId) const {
1178 0
        auto it = this->symbolicExpressions.find(symExprId);
1179

1180 0
        if (it != this->symbolicExpressions.end()) {
1181 0
          return (it->second.use_count() > 0);
1182
        }
1183

1184
        return false;
1185
      }
1186

1187

1188
      /* Returns true if memory cell expressions contain symbolic variables. */
1189 0
      bool SymbolicEngine::isMemorySymbolized(const triton::arch::MemoryAccess& mem) const {
1190 0
        triton::uint64 addr = mem.getAddress();
1191 0
        triton::uint32 size = mem.getSize();
1192

1193 0
        return this->isMemorySymbolized(addr, size);
1194
      }
1195

1196

1197
      /* Returns true if memory cell expressions contain symbolic variables. */
1198 0
      bool SymbolicEngine::isMemorySymbolized(triton::uint64 addr, triton::uint32 size) const {
1199 0
        for (triton::uint32 i = 0; i < size; i++) {
1200 0
          const SharedSymbolicExpression& expr = this->getSymbolicMemory(addr + i);
1201 0
          if (expr && expr->isSymbolized()) {
1202 0
            return true;
1203
          }
1204
        }
1205
        return false;
1206
      }
1207

1208

1209
      /* Returns true if the register expression contains a symbolic variable. */
1210 0
      bool SymbolicEngine::isRegisterSymbolized(const triton::arch::Register& reg) const {
1211 0
        const SharedSymbolicExpression& expr = this->getSymbolicRegister(reg);
1212 0
        if (expr) {
1213 0
          return expr->isSymbolized();
1214
        }
1215
        return false;
1216
      }
1217

1218

1219
      /* Enables or disables the symbolic engine */
1220 1
      void SymbolicEngine::enable(bool flag) {
1221 1
        this->enableFlag = flag;
1222
      }
1223

1224

1225
      /* Initializes the memory access AST (LOAD and STORE) */
1226 1
      void SymbolicEngine::initLeaAst(triton::arch::MemoryAccess& mem, bool force) {
1227 1
        if (mem.getBitSize() >= bitsize::byte) {
1228 1
          const triton::arch::Register& base  = mem.getConstBaseRegister();
1229 1
          const triton::arch::Register& index = mem.getConstIndexRegister();
1230 1
          const triton::arch::Register& seg   = mem.getConstSegmentRegister();
1231 1
          triton::uint64 segmentValue         = (this->architecture->isRegisterValid(seg) ? this->architecture->getConcreteRegisterValue(seg).convert_to<triton::uint64>() : 0);
1232 1
          triton::uint64 scaleValue           = mem.getConstScale().getValue();
1233 1
          triton::uint64 dispValue            = mem.getConstDisplacement().getValue();
1234 1
          triton::uint32 bitSize              = (this->architecture->isRegisterValid(base) ? base.getBitSize() :
1235 1
                                                  (this->architecture->isRegisterValid(index) ? index.getBitSize() :
1236 1
                                                    (mem.getConstDisplacement().getBitSize() ? mem.getConstDisplacement().getBitSize() :
1237 0
                                                      this->architecture->gprBitSize()
1238
                                                    )
1239
                                                  )
1240 1
                                                );
1241

1242

1243
          /* Initialize the AST of the memory access (LEA) -> ((pc + base) + (index * scale) + disp) */
1244 1
          auto pcPlusBaseAst    = mem.getPcRelative() ? this->astCtxt->bv(mem.getPcRelative(), bitSize) :
1245 1
                                    (this->architecture->isRegisterValid(base) ? this->getRegisterAst(base) :
1246 1
                                      this->astCtxt->bv(0, bitSize));
1247

1248
          auto indexMulScaleAst = this->astCtxt->bvmul(
1249 1
                                    (this->architecture->isRegisterValid(index) ? this->getRegisterAst(index) : this->astCtxt->bv(0, bitSize)),
1250 1
                                    this->astCtxt->bv(scaleValue, bitSize)
1251 1
                                  );
1252

1253 1
          auto dispAst          = this->astCtxt->bv(dispValue, bitSize);
1254
          auto leaAst           = this->astCtxt->bvadd(
1255 1
                                    index.isSubtracted() ? this->astCtxt->bvsub(pcPlusBaseAst, indexMulScaleAst) : this->astCtxt->bvadd(pcPlusBaseAst, indexMulScaleAst),
1256
                                    dispAst
1257 1
                                  );
1258

1259
          /* Use segments as base address instead of selector into the GDT. */
1260 1
          if (segmentValue) {
1261 1
            leaAst = this->astCtxt->bvadd(
1262 1
                       this->astCtxt->bv(segmentValue, seg.getBitSize()),
1263 1
                       this->astCtxt->sx((seg.getBitSize() - bitSize), leaAst)
1264 1
                     );
1265
          }
1266

1267
          /* Set AST */
1268 1
          mem.setLeaAst(leaAst);
1269

1270
          /* Initialize the address only if it is not already defined */
1271 1
          if (!mem.getAddress() || force)
1272 1
            mem.setAddress(leaAst->evaluate().convert_to<triton::uint64>());
1273
        }
1274
      }
1275

1276

1277 1
      triton::uint512 SymbolicEngine::getConcreteVariableValue(const SharedSymbolicVariable& symVar) const {
1278 1
        return this->astCtxt->getVariableValue(symVar->getName());
1279
      }
1280

1281

1282 1
      void SymbolicEngine::setConcreteVariableValue(const SharedSymbolicVariable& symVar, const triton::uint512& value) {
1283 1
        triton::uint512 max = -1;
1284

1285
        /* Check if the value is too big */
1286 1
        max = max >> (512 - symVar->getSize());
1287 1
        if (value > max) {
1288 0
          throw triton::exceptions::SymbolicEngine("SymbolicEngine::setConcreteVariableValue(): Can not set this value (too big) to this symbolic variable.");
1289
        }
1290

1291
        /* Update the symbolic variable value */
1292 1
        this->astCtxt->updateVariable(symVar->getName(), value);
1293

1294
        /* Synchronize concrete state */
1295 1
        if (symVar->getType() == REGISTER_VARIABLE) {
1296 1
          const triton::arch::Register& reg = this->architecture->getRegister(static_cast<triton::arch::register_e>(symVar->getOrigin()));
1297 1
          this->architecture->setConcreteRegisterValue(reg, value);
1298
        }
1299

1300 1
        else if (symVar->getType() == MEMORY_VARIABLE && symVar->getSize() && !(symVar->getSize() % bitsize::byte)) {
1301 1
          triton::uint64 addr            = symVar->getOrigin();
1302 1
          triton::uint32 size            = symVar->getSize() / bitsize::byte;
1303 1
          triton::arch::MemoryAccess mem = triton::arch::MemoryAccess(addr, size);
1304

1305 1
          this->architecture->setConcreteMemoryValue(mem, value);
1306
        }
1307
      }
1308

1309
    }; /* symbolic namespace */
1310
  }; /* engines namespace */
1311 1
}; /*triton namespace */

Read our documentation on viewing source code .

Loading