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 SymbolicEngine(triton::arch::Architecture * architecture,const triton::modes::SharedModes & modes,const triton::ast::SharedAstContext & astCtxt,triton::callbacks::Callbacks * callbacks)22 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 modes(modes) { 30 31 if (architecture == nullptr) { 32 throw triton::exceptions::SymbolicEngine("SymbolicEngine::SymbolicEngine(): The architecture pointer must be valid."); 33 } 34 35 this->architecture = architecture; 36 this->callbacks = callbacks; 37 this->enableFlag = true; 38 this->numberOfRegisters = this->architecture->numberOfRegisters(); 39 this->uniqueSymExprId = 0; 40 this->uniqueSymVarId = 0; 41 42 this->symbolicReg.resize(this->numberOfRegisters); 43 } 44 45 SymbolicEngine(const SymbolicEngine & other)46 SymbolicEngine::SymbolicEngine(const SymbolicEngine& other) 47 : triton::engines::symbolic::SymbolicSimplification(other), 48 triton::engines::symbolic::PathManager(other), 49 astCtxt(other.astCtxt), 50 modes(other.modes) { 51 52 this->alignedMemoryReference = other.alignedMemoryReference; 53 this->architecture = other.architecture; 54 this->callbacks = other.callbacks; 55 this->enableFlag = other.enableFlag; 56 this->memoryReference = other.memoryReference; 57 this->numberOfRegisters = other.numberOfRegisters; 58 this->symbolicExpressions = other.symbolicExpressions; 59 this->symbolicReg = other.symbolicReg; 60 this->symbolicVariables = other.symbolicVariables; 61 this->uniqueSymExprId = other.uniqueSymExprId; 62 this->uniqueSymVarId = other.uniqueSymVarId; 63 } 64 65 ~SymbolicEngine()66 SymbolicEngine::~SymbolicEngine() { 67 /* See #828: Release ownership before calling container destructor */ 68 this->memoryReference.clear(); 69 this->symbolicReg.clear(); 70 } 71 72 operator =(const SymbolicEngine & other)73 SymbolicEngine& SymbolicEngine::operator=(const SymbolicEngine& other) { 74 triton::engines::symbolic::SymbolicSimplification::operator=(other); 75 triton::engines::symbolic::PathManager::operator=(other); 76 77 this->alignedMemoryReference = other.alignedMemoryReference; 78 this->architecture = other.architecture; 79 this->astCtxt = other.astCtxt; 80 this->callbacks = other.callbacks; 81 this->enableFlag = other.enableFlag; 82 this->memoryReference = other.memoryReference; 83 this->modes = other.modes; 84 this->numberOfRegisters = other.numberOfRegisters; 85 this->symbolicExpressions = other.symbolicExpressions; 86 this->symbolicReg = other.symbolicReg; 87 this->symbolicVariables = other.symbolicVariables; 88 this->uniqueSymExprId = other.uniqueSymExprId; 89 this->uniqueSymVarId = other.uniqueSymVarId; 90 91 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 */ concretizeRegister(const triton::arch::Register & reg)100 void SymbolicEngine::concretizeRegister(const triton::arch::Register& reg) { 101 triton::arch::register_e parentId = reg.getParent(); 102 103 if (this->architecture->isRegisterValid(parentId)) { 104 this->symbolicReg[parentId] = nullptr; 105 } 106 } 107 108 109 /* Same as concretizeRegister but with all registers */ concretizeAllRegister(void)110 void SymbolicEngine::concretizeAllRegister(void) { 111 for (triton::uint32 i = 0; i < this->numberOfRegisters; i++) { 112 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 */ concretizeMemory(const triton::arch::MemoryAccess & mem)122 void SymbolicEngine::concretizeMemory(const triton::arch::MemoryAccess& mem) { 123 triton::uint64 addr = mem.getAddress(); 124 triton::uint32 size = mem.getSize(); 125 126 for (triton::uint32 index = 0; index < size; index++) { 127 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 */ concretizeMemory(triton::uint64 addr)137 void SymbolicEngine::concretizeMemory(triton::uint64 addr) { 138 this->memoryReference.erase(addr); 139 this->removeAlignedMemory(addr, triton::size::byte); 140 } 141 142 143 /* Same as concretizeMemory but with all address memory */ concretizeAllMemory(void)144 void SymbolicEngine::concretizeAllMemory(void) { 145 this->memoryReference.clear(); 146 this->alignedMemoryReference.clear(); 147 } 148 149 150 /* Gets an aligned entry. */ getAlignedMemory(triton::uint64 address,triton::uint32 size)151 const SharedSymbolicExpression& SymbolicEngine::getAlignedMemory(triton::uint64 address, triton::uint32 size) { 152 return this->alignedMemoryReference[std::make_pair(address, size)]; 153 } 154 155 156 /* Checks if the aligned memory is recored. */ isAlignedMemory(triton::uint64 address,triton::uint32 size)157 bool SymbolicEngine::isAlignedMemory(triton::uint64 address, triton::uint32 size) { 158 if (this->alignedMemoryReference.find(std::make_pair(address, size)) != this->alignedMemoryReference.end()) { 159 return true; 160 } 161 return false; 162 } 163 164 165 /* Adds an aligned memory */ addAlignedMemory(triton::uint64 address,triton::uint32 size,const SharedSymbolicExpression & expr)166 void SymbolicEngine::addAlignedMemory(triton::uint64 address, triton::uint32 size, const SharedSymbolicExpression& expr) { 167 this->removeAlignedMemory(address, size); 168 if (!(this->modes->isModeEnabled(triton::modes::ONLY_ON_SYMBOLIZED) && expr->getAst()->isSymbolized() == false)) { 169 this->alignedMemoryReference[std::make_pair(address, size)] = expr; 170 } 171 } 172 173 174 /* Removes an aligned memory */ removeAlignedMemory(triton::uint64 address,triton::uint32 size)175 void SymbolicEngine::removeAlignedMemory(triton::uint64 address, triton::uint32 size) { 176 /* Remove overloaded positive ranges */ 177 for (triton::uint32 index = 0; index < size; index++) { 178 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::byte)); 179 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::word)); 180 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dword)); 181 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qword)); 182 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqword)); 183 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::qqword)); 184 this->alignedMemoryReference.erase(std::make_pair(address+index, triton::size::dqqword)); 185 } 186 187 /* Remove overloaded negative ranges */ 188 for (triton::uint32 index = 1; index < triton::size::dqqword; index++) { 189 if (index < triton::size::word) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::word)); 190 if (index < triton::size::dword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dword)); 191 if (index < triton::size::qword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qword)); 192 if (index < triton::size::dqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::dqword)); 193 if (index < triton::size::qqword) this->alignedMemoryReference.erase(std::make_pair(address-index, triton::size::qqword)); 194 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 */ getSymbolicMemory(triton::uint64 addr) const200 SharedSymbolicExpression SymbolicEngine::getSymbolicMemory(triton::uint64 addr) const { 201 auto it = this->memoryReference.find(addr); 202 if (it != this->memoryReference.end()) { 203 return it->second; 204 } 205 return nullptr; 206 } 207 208 209 /* Returns the symbolic variable otherwise raises an exception */ getSymbolicVariable(triton::usize symVarId) const210 SharedSymbolicVariable SymbolicEngine::getSymbolicVariable(triton::usize symVarId) const { 211 auto it = this->symbolicVariables.find(symVarId); 212 if (it == this->symbolicVariables.end()) { 213 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred symbolic variable."); 214 } 215 216 if (auto node = it->second.lock()) { 217 return node; 218 } 219 220 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): This symbolic variable is dead."); 221 } 222 223 224 /* Returns the symbolic variable otherwise returns nullptr */ getSymbolicVariable(const std::string & symVarName) const225 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 for (auto& sv: this->symbolicVariables) { 231 if (auto symVar = sv.second.lock()) { 232 if (symVar->getName() == symVarName) { 233 return symVar; 234 } 235 } 236 } 237 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicVariable(): Unregistred or dead symbolic variable."); 238 } 239 240 241 /* Returns all symbolic variables */ getSymbolicVariables(void) const242 std::unordered_map<triton::usize, SharedSymbolicVariable> SymbolicEngine::getSymbolicVariables(void) const { 243 // Copy and clean up dead weak ref 244 std::unordered_map<triton::usize, SharedSymbolicVariable> ret; 245 std::vector<triton::usize> toRemove; 246 247 for (auto& kv : this->symbolicVariables) { 248 if (auto sp = kv.second.lock()) { 249 ret[kv.first] = sp; 250 } else { 251 toRemove.push_back(kv.first); 252 } 253 } 254 255 for (triton::usize id : toRemove) { 256 this->symbolicVariables.erase(id); 257 } 258 259 return ret; 260 } 261 262 setImplicitReadRegisterFromEffectiveAddress(triton::arch::Instruction & inst,const triton::arch::MemoryAccess & mem)263 void SymbolicEngine::setImplicitReadRegisterFromEffectiveAddress(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) { 264 /* Set implicit read of the base register (LEA) */ 265 if (this->architecture->isRegisterValid(mem.getConstBaseRegister())) { 266 (void)this->getRegisterAst(inst, mem.getConstBaseRegister()); 267 } 268 269 /* Set implicit read of the index register (LEA) */ 270 if (this->architecture->isRegisterValid(mem.getConstIndexRegister())) { 271 (void)this->getRegisterAst(inst, mem.getConstIndexRegister()); 272 } 273 } 274 275 276 /* Returns the shared symbolic expression corresponding to the register */ getSymbolicRegister(const triton::arch::Register & reg) const277 const SharedSymbolicExpression& SymbolicEngine::getSymbolicRegister(const triton::arch::Register& reg) const { 278 triton::arch::register_e parentId = reg.getParent(); 279 280 if (this->architecture->isRegisterValid(parentId)) { 281 return this->symbolicReg.at(parentId); 282 } 283 284 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicRegister(): Invalid Register"); 285 } 286 287 288 /* Returns the symbolic address value */ getSymbolicMemoryValue(triton::uint64 address)289 triton::uint8 SymbolicEngine::getSymbolicMemoryValue(triton::uint64 address) { 290 triton::arch::MemoryAccess mem(address, triton::size::byte); 291 return this->getSymbolicMemoryValue(mem).convert_to<triton::uint8>(); 292 } 293 294 295 /* Returns the symbolic memory value */ getSymbolicMemoryValue(const triton::arch::MemoryAccess & mem)296 triton::uint512 SymbolicEngine::getSymbolicMemoryValue(const triton::arch::MemoryAccess& mem) { 297 const triton::ast::SharedAbstractNode& node = this->getMemoryAst(mem); 298 return node->evaluate(); 299 } 300 301 302 /* Returns the symbolic values of a memory area */ getSymbolicMemoryAreaValue(triton::uint64 baseAddr,triton::usize size)303 std::vector<triton::uint8> SymbolicEngine::getSymbolicMemoryAreaValue(triton::uint64 baseAddr, triton::usize size) { 304 std::vector<triton::uint8> area; 305 306 area.reserve(size); 307 for (triton::usize index = 0; index < size; index++) { 308 area.push_back(this->getSymbolicMemoryValue(baseAddr + index)); 309 } 310 311 return area; 312 } 313 314 315 /* Returns the symbolic register value */ getSymbolicRegisterValue(const triton::arch::Register & reg)316 triton::uint512 SymbolicEngine::getSymbolicRegisterValue(const triton::arch::Register& reg) { 317 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 */ getUniqueSymExprId(void)324 triton::usize SymbolicEngine::getUniqueSymExprId(void) { 325 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 */ getUniqueSymVarId(void)332 triton::usize SymbolicEngine::getUniqueSymVarId(void) { 333 return this->uniqueSymVarId++; 334 } 335 336 337 /* Creates a new symbolic expression with comment */ newSymbolicExpression(const triton::ast::SharedAbstractNode & node,triton::engines::symbolic::expression_e type,const std::string & comment)338 SharedSymbolicExpression SymbolicEngine::newSymbolicExpression(const triton::ast::SharedAbstractNode& node, triton::engines::symbolic::expression_e type, const std::string& comment) { 339 /* Each symbolic expression must have an unique id */ 340 triton::usize id = this->getUniqueSymExprId(); 341 342 /* Performes transformation if there are rules recorded */ 343 const triton::ast::SharedAbstractNode& snode = this->processSimplification(node); 344 345 /* Allocates the new shared symbolic expression */ 346 SharedSymbolicExpression expr = std::make_shared<SymbolicExpression>(snode, id, type, comment); 347 if (expr == nullptr) { 348 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicExpression(): not enough memory"); 349 } 350 351 /* Save and returns the new shared symbolic expression */ 352 this->symbolicExpressions[id] = expr; 353 return expr; 354 } 355 356 357 /* Removes the symbolic expression corresponding to the id */ removeSymbolicExpression(const SharedSymbolicExpression & expr)358 void SymbolicEngine::removeSymbolicExpression(const SharedSymbolicExpression& expr) { 359 if (this->symbolicExpressions.find(expr->getId()) != this->symbolicExpressions.end()) { 360 /* Concretize memory */ 361 if (expr->getType() == MEMORY_EXPRESSION) { 362 const auto& mem = expr->getOriginMemory(); 363 this->concretizeMemory(mem); 364 } 365 366 /* Concretize register */ 367 else if (expr->getType() == REGISTER_EXPRESSION) { 368 const auto& reg = expr->getOriginRegister(); 369 this->concretizeRegister(reg); 370 } 371 372 /* Delete and remove the pointer */ 373 this->symbolicExpressions.erase(expr->getId()); 374 } 375 } 376 377 378 /* Gets the shared symbolic expression from a symbolic id */ getSymbolicExpression(triton::usize symExprId) const379 SharedSymbolicExpression SymbolicEngine::getSymbolicExpression(triton::usize symExprId) const { 380 auto it = this->symbolicExpressions.find(symExprId); 381 if (it == this->symbolicExpressions.end()) { 382 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression id not found"); 383 } 384 385 if (auto sp = it->second.lock()) { 386 return sp; 387 } 388 389 this->symbolicExpressions.erase(symExprId); 390 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getSymbolicExpression(): symbolic expression is not available anymore"); 391 } 392 393 394 /* Returns all symbolic expressions */ getSymbolicExpressions(void) const395 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::getSymbolicExpressions(void) const { 396 // Copy and clean up dead weak ref 397 std::unordered_map<triton::usize, SharedSymbolicExpression> ret; 398 std::vector<triton::usize> toRemove; 399 400 for (auto& kv : this->symbolicExpressions) { 401 if (auto sp = kv.second.lock()) { 402 ret[kv.first] = sp; 403 } else { 404 toRemove.push_back(kv.first); 405 } 406 } 407 408 for (auto id : toRemove) 409 this->symbolicExpressions.erase(id); 410 411 return ret; 412 } 413 414 415 /* Slices all expressions from a given one */ sliceExpressions(const SharedSymbolicExpression & expr)416 std::unordered_map<triton::usize, SharedSymbolicExpression> SymbolicEngine::sliceExpressions(const SharedSymbolicExpression& expr) { 417 std::unordered_map<triton::usize, SharedSymbolicExpression> exprs; 418 419 if (expr == nullptr) { 420 throw triton::exceptions::SymbolicEngine("SymbolicEngine::sliceExpressions(): expr cannot be null."); 421 } 422 423 exprs[expr->getId()] = expr; 424 425 auto worklist = triton::ast::childrenExtraction(expr->getAst(), true /* unroll */, false /* revert */); 426 for (auto&& n : worklist) { 427 if (n->getType() == triton::ast::REFERENCE_NODE) { 428 auto expr = reinterpret_cast<triton::ast::ReferenceNode*>(n.get())->getSymbolicExpression(); 429 auto eid = expr->getId(); 430 exprs[eid] = expr; 431 } 432 } 433 434 return exprs; 435 } 436 437 438 /* Returns a list which contains all tainted expressions */ getTaintedSymbolicExpressions(void) const439 std::vector<SharedSymbolicExpression> SymbolicEngine::getTaintedSymbolicExpressions(void) const { 440 std::vector<SharedSymbolicExpression> taintedExprs; 441 std::vector<triton::usize> invalidSymExpr; 442 443 for (auto it = this->symbolicExpressions.begin(); it != this->symbolicExpressions.end(); it++) { 444 if (auto sp = it->second.lock()) { 445 if (sp->isTainted) { 446 taintedExprs.push_back(sp); 447 } 448 } else { 449 invalidSymExpr.push_back(it->first); 450 } 451 } 452 453 for (auto id : invalidSymExpr) { 454 this->symbolicExpressions.erase(id); 455 } 456 457 return taintedExprs; 458 } 459 460 461 /* Returns the map of symbolic registers defined */ getSymbolicRegisters(void) const462 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> SymbolicEngine::getSymbolicRegisters(void) const { 463 std::unordered_map<triton::arch::register_e, SharedSymbolicExpression> ret; 464 465 for (triton::uint32 it = 0; it < this->numberOfRegisters; it++) { 466 if (this->symbolicReg[it] != nullptr) { 467 ret[triton::arch::register_e(it)] = this->symbolicReg[it]; 468 } 469 } 470 471 return ret; 472 } 473 474 475 /* Returns the map of symbolic memory defined */ getSymbolicMemory(void) const476 const std::unordered_map<triton::uint64, SharedSymbolicExpression>& SymbolicEngine::getSymbolicMemory(void) const { 477 return this->memoryReference; 478 } 479 480 481 /* 482 * Converts an expression id to a symbolic variable. 483 * e.g: 484 * #43 = (_ bv10 8) 485 * symbolizeExpression(43, 8) 486 * #43 = SymVar_4 487 */ symbolizeExpression(triton::usize exprId,triton::uint32 symVarSize,const std::string & symVarAlias)488 SharedSymbolicVariable SymbolicEngine::symbolizeExpression(triton::usize exprId, triton::uint32 symVarSize, const std::string& symVarAlias) { 489 const SharedSymbolicExpression& expression = this->getSymbolicExpression(exprId); 490 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(UNDEFINED_VARIABLE, 0, symVarSize, symVarAlias); 491 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->variable(symVar); 492 493 if (expression->getAst()) { 494 this->setConcreteVariableValue(symVar, expression->getAst()->evaluate()); 495 } 496 497 expression->setAst(tmp); 498 499 return symVar; 500 } 501 502 503 /* The memory size is used to define the symbolic variable's size. */ symbolizeMemory(const triton::arch::MemoryAccess & mem,const std::string & symVarAlias)504 SharedSymbolicVariable SymbolicEngine::symbolizeMemory(const triton::arch::MemoryAccess& mem, const std::string& symVarAlias) { 505 triton::uint64 memAddr = mem.getAddress(); 506 triton::uint32 symVarSize = mem.getSize(); 507 triton::uint512 cv = this->architecture->getConcreteMemoryValue(mem); 508 509 /* First we create a symbolic variable */ 510 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(MEMORY_VARIABLE, memAddr, symVarSize * bitsize::byte, symVarAlias); 511 512 /* Create the AST node */ 513 const triton::ast::SharedAbstractNode& symVarNode = this->astCtxt->variable(symVar); 514 515 /* Setup the concrete value to the symbolic variable */ 516 this->setConcreteVariableValue(symVar, cv); 517 518 /* Record the aligned symbolic variable for a symbolic optimization */ 519 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) { 520 const SharedSymbolicExpression& se = this->newSymbolicExpression(symVarNode, MEMORY_EXPRESSION, "aligned Byte reference"); 521 se->setOriginMemory(mem); 522 this->addAlignedMemory(memAddr, symVarSize, se); 523 } 524 525 /* Split expression in bytes */ 526 for (triton::sint32 index = symVarSize-1; index >= 0; index--) { 527 triton::uint32 high = ((bitsize::byte * (index + 1)) - 1); 528 triton::uint32 low = ((bitsize::byte * (index + 1)) - bitsize::byte); 529 530 /* Isolate the good part of the symbolic variable */ 531 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, symVarNode); 532 533 /* Create a new symbolic expression containing the symbolic variable */ 534 const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference"); 535 se->setOriginMemory(triton::arch::MemoryAccess(memAddr+index, triton::size::byte)); 536 537 /* Assign the symbolic expression to the memory cell */ 538 this->addMemoryReference(memAddr+index, se); 539 } 540 541 return symVar; 542 } 543 544 symbolizeRegister(const triton::arch::Register & reg,const std::string & symVarAlias)545 SharedSymbolicVariable SymbolicEngine::symbolizeRegister(const triton::arch::Register& reg, const std::string& symVarAlias) { 546 const triton::arch::Register& parent = this->architecture->getRegister(reg.getParent()); 547 triton::uint32 symVarSize = reg.getBitSize(); 548 triton::uint512 cv = this->architecture->getConcreteRegisterValue(reg); 549 550 if (!this->architecture->isRegisterValid(parent.getId())) 551 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): Invalid register id"); 552 553 if (reg.isMutable() == false) 554 throw triton::exceptions::SymbolicEngine("SymbolicEngine::symbolizeRegister(): This register is immutable"); 555 556 /* Create the symbolic variable */ 557 const SharedSymbolicVariable& symVar = this->newSymbolicVariable(REGISTER_VARIABLE, reg.getId(), symVarSize, symVarAlias); 558 559 /* Create the AST node */ 560 const triton::ast::SharedAbstractNode& tmp = this->insertSubRegisterInParent(reg, this->astCtxt->variable(symVar), false); 561 562 /* Setup the concrete value to the symbolic variable */ 563 this->setConcreteVariableValue(symVar, cv); 564 565 /* Create a new symbolic expression containing the symbolic variable */ 566 const SharedSymbolicExpression& se = this->newSymbolicExpression(tmp, REGISTER_EXPRESSION); 567 568 /* Assign the symbolic expression to the register */ 569 this->assignSymbolicExpressionToRegister(se, parent); 570 571 return symVar; 572 } 573 574 575 /* Adds a new symbolic variable */ newSymbolicVariable(triton::engines::symbolic::variable_e type,triton::uint64 origin,triton::uint32 size,const std::string & alias)576 SharedSymbolicVariable SymbolicEngine::newSymbolicVariable(triton::engines::symbolic::variable_e type, triton::uint64 origin, triton::uint32 size, const std::string& alias) { 577 triton::usize uniqueId = this->getUniqueSymVarId(); 578 579 SharedSymbolicVariable symVar = std::make_shared<SymbolicVariable>(type, origin, uniqueId, size, alias); 580 if (symVar == nullptr) { 581 throw triton::exceptions::SymbolicEngine("SymbolicEngine::newSymbolicVariable(): Cannot allocate a new symbolic variable"); 582 } 583 584 this->symbolicVariables[uniqueId] = symVar; 585 return symVar; 586 } 587 588 589 /* Returns the AST corresponding to the operand. */ getOperandAst(const triton::arch::OperandWrapper & op)590 triton::ast::SharedAbstractNode SymbolicEngine::getOperandAst(const triton::arch::OperandWrapper& op) { 591 switch (op.getType()) { 592 case triton::arch::OP_IMM: return this->getImmediateAst(op.getConstImmediate()); 593 case triton::arch::OP_MEM: return this->getMemoryAst(op.getConstMemory()); 594 case triton::arch::OP_REG: return this->getRegisterAst(op.getConstRegister()); 595 default: 596 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand."); 597 } 598 } 599 600 601 /* Returns the AST corresponding to the operand. */ getOperandAst(triton::arch::Instruction & inst,const triton::arch::OperandWrapper & op)602 triton::ast::SharedAbstractNode SymbolicEngine::getOperandAst(triton::arch::Instruction& inst, const triton::arch::OperandWrapper& op) { 603 switch (op.getType()) { 604 case triton::arch::OP_IMM: return this->getImmediateAst(inst, op.getConstImmediate()); 605 case triton::arch::OP_MEM: return this->getMemoryAst(inst, op.getConstMemory()); 606 case triton::arch::OP_REG: return this->getRegisterAst(inst, op.getConstRegister()); 607 default: 608 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getOperandAst(): Invalid operand."); 609 } 610 } 611 612 getShiftAst(const triton::arch::arm::ArmOperandProperties & shift,const triton::ast::SharedAbstractNode & node)613 triton::ast::SharedAbstractNode SymbolicEngine::getShiftAst(const triton::arch::arm::ArmOperandProperties& shift, const triton::ast::SharedAbstractNode& node) { 614 auto imm = shift.getShiftImmediate(); 615 auto reg = shift.getShiftRegister(); 616 617 switch (shift.getShiftType()) { 618 case triton::arch::arm::ID_SHIFT_ASR: 619 return this->astCtxt->bvashr(node, this->astCtxt->bv(imm, node->getBitvectorSize())); 620 621 case triton::arch::arm::ID_SHIFT_LSL: 622 return this->astCtxt->bvshl(node, this->astCtxt->bv(imm, node->getBitvectorSize())); 623 624 case triton::arch::arm::ID_SHIFT_LSR: 625 return this->astCtxt->bvlshr(node, this->astCtxt->bv(imm, node->getBitvectorSize())); 626 627 case triton::arch::arm::ID_SHIFT_ROR: 628 return this->astCtxt->bvror(node, this->astCtxt->bv(imm, node->getBitvectorSize())); 629 630 case triton::arch::arm::ID_SHIFT_RRX: /* Arm32 only. */ 631 return this->astCtxt->extract( 632 node->getBitvectorSize(), 633 1, 634 this->astCtxt->bvror( 635 this->astCtxt->concat( 636 node, 637 this->getRegisterAst(this->architecture->getRegister(triton::arch::ID_REG_ARM32_C)) 638 ), 639 1 640 ) 641 ); 642 643 case triton::arch::arm::ID_SHIFT_ASR_REG: /* Arm32 only. */ 644 return this->astCtxt->bvashr( 645 node, 646 this->astCtxt->zx( 647 this->architecture->getRegister(reg).getBitSize() - 8, 648 this->astCtxt->extract( 649 7, 650 0, 651 this->getRegisterAst(this->architecture->getRegister(reg)) 652 ) 653 ) 654 ); 655 656 case triton::arch::arm::ID_SHIFT_LSL_REG: /* Arm32 only. */ 657 return this->astCtxt->bvshl( 658 node, 659 this->astCtxt->zx( 660 this->architecture->getRegister(reg).getBitSize() - 8, 661 this->astCtxt->extract( 662 7, 663 0, 664 this->getRegisterAst(this->architecture->getRegister(reg)) 665 ) 666 ) 667 ); 668 669 case triton::arch::arm::ID_SHIFT_LSR_REG: /* Arm32 only. */ 670 return this->astCtxt->bvlshr( 671 node, 672 this->astCtxt->zx( 673 this->architecture->getRegister(reg).getBitSize() - 8, 674 this->astCtxt->extract( 675 7, 676 0, 677 this->getRegisterAst(this->architecture->getRegister(reg)) 678 ) 679 ) 680 ); 681 682 case triton::arch::arm::ID_SHIFT_ROR_REG: /* Arm32 only. */ 683 return this->astCtxt->bvror( 684 node, 685 this->astCtxt->zx( 686 this->architecture->getRegister(reg).getBitSize() - 8, 687 this->astCtxt->extract( 688 7, 689 0, 690 this->getRegisterAst(this->architecture->getRegister(reg)) 691 ) 692 ) 693 ); 694 695 case triton::arch::arm::ID_SHIFT_RRX_REG: 696 /* NOTE: Capstone considers this as a viable shift operand but 697 * according to the ARM manual this is not possible. 698 */ 699 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): ID_SHIFT_RRX_REG is an invalid shift operand."); 700 701 default: 702 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getShiftAst(): Invalid shift operand."); 703 } 704 } 705 706 getExtendAst(const triton::arch::arm::ArmOperandProperties & extend,const triton::ast::SharedAbstractNode & node)707 triton::ast::SharedAbstractNode SymbolicEngine::getExtendAst(const triton::arch::arm::ArmOperandProperties& extend, const triton::ast::SharedAbstractNode& node) { 708 triton::uint32 size = extend.getExtendSize(); 709 710 switch (extend.getExtendType()) { 711 case triton::arch::arm::ID_EXTEND_UXTB: 712 return this->astCtxt->zx(size, this->astCtxt->extract(7, 0, node)); 713 714 case triton::arch::arm::ID_EXTEND_UXTH: 715 return this->astCtxt->zx(size, this->astCtxt->extract(15, 0, node)); 716 717 case triton::arch::arm::ID_EXTEND_UXTW: 718 return this->astCtxt->zx(size, this->astCtxt->extract(31, 0, node)); 719 720 case triton::arch::arm::ID_EXTEND_UXTX: 721 return this->astCtxt->zx(size, this->astCtxt->extract(63, 0, node)); 722 723 case triton::arch::arm::ID_EXTEND_SXTB: 724 return this->astCtxt->sx(size, this->astCtxt->extract(7, 0, node)); 725 726 case triton::arch::arm::ID_EXTEND_SXTH: 727 return this->astCtxt->sx(size, this->astCtxt->extract(15, 0, node)); 728 729 case triton::arch::arm::ID_EXTEND_SXTW: 730 return this->astCtxt->sx(size, this->astCtxt->extract(31, 0, node)); 731 732 case triton::arch::arm::ID_EXTEND_SXTX: 733 return this->astCtxt->sx(size, this->astCtxt->extract(63, 0, node)); 734 735 default: 736 throw triton::exceptions::SymbolicEngine("SymbolicEngine::getExtendAst(): Invalid extend operand."); 737 } 738 } 739 740 741 /* Returns the AST corresponding to the immediate */ getImmediateAst(const triton::arch::Immediate & imm)742 triton::ast::SharedAbstractNode SymbolicEngine::getImmediateAst(const triton::arch::Immediate& imm) { 743 triton::ast::SharedAbstractNode node = this->astCtxt->bv(imm.getValue(), imm.getBitSize()); 744 745 /* Shift AST if it's a shift operand */ 746 if (imm.getShiftType() != triton::arch::arm::ID_SHIFT_INVALID) { 747 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(imm), node); 748 } 749 750 return node; 751 } 752 753 754 /* Returns the AST corresponding to the immediate and defines the immediate as input of the instruction */ getImmediateAst(triton::arch::Instruction & inst,const triton::arch::Immediate & imm)755 triton::ast::SharedAbstractNode SymbolicEngine::getImmediateAst(triton::arch::Instruction& inst, const triton::arch::Immediate& imm) { 756 triton::ast::SharedAbstractNode node = this->getImmediateAst(imm); 757 inst.setReadImmediate(imm, node); 758 return node; 759 } 760 761 762 /* Returns the AST corresponding to the memory */ getMemoryAst(const triton::arch::MemoryAccess & mem)763 triton::ast::SharedAbstractNode SymbolicEngine::getMemoryAst(const triton::arch::MemoryAccess& mem) { 764 std::vector<triton::ast::SharedAbstractNode> opVec; 765 766 triton::ast::SharedAbstractNode tmp = nullptr; 767 triton::uint64 address = mem.getAddress(); 768 triton::uint32 size = mem.getSize(); 769 triton::uint8 concreteValue[triton::size::dqqword] = {0}; 770 triton::uint512 value = this->architecture->getConcreteMemoryValue(mem); 771 772 triton::utils::fromUintToBuffer(value, concreteValue); 773 774 /* 775 * Symbolic optimization 776 * If the memory access is aligned, don't split the memory. 777 */ 778 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY) && this->isAlignedMemory(address, size)) { 779 return this->getAlignedMemory(address, size)->getAst(); 780 } 781 782 /* If the memory access is 1 byte long, just return the appropriate 8-bit vector */ 783 if (size == 1) { 784 const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address); 785 if (symMem) return this->astCtxt->reference(symMem); 786 else return this->astCtxt->bv(concreteValue[size - 1], bitsize::byte); 787 } 788 789 /* If the memory access is more than 1 byte long, concatenate each memory cell */ 790 opVec.reserve(size); 791 while (size) { 792 const SharedSymbolicExpression& symMem = this->getSymbolicMemory(address + size - 1); 793 if (symMem) opVec.push_back(this->astCtxt->reference(symMem)); 794 else opVec.push_back(this->astCtxt->bv(concreteValue[size - 1], bitsize::byte)); 795 size--; 796 } 797 return this->astCtxt->concat(opVec); 798 } 799 800 801 /* Returns the AST corresponding to the memory and defines the memory as input of the instruction */ getMemoryAst(triton::arch::Instruction & inst,const triton::arch::MemoryAccess & mem)802 triton::ast::SharedAbstractNode SymbolicEngine::getMemoryAst(triton::arch::Instruction& inst, const triton::arch::MemoryAccess& mem) { 803 triton::ast::SharedAbstractNode node = this->getMemoryAst(mem); 804 805 /* Set load access */ 806 inst.setLoadAccess(mem, node); 807 808 /* Set implicit read of the base and index registers from an effective address */ 809 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem); 810 811 return node; 812 } 813 814 815 /* Returns the AST corresponding to the register */ getRegisterAst(const triton::arch::Register & reg)816 triton::ast::SharedAbstractNode SymbolicEngine::getRegisterAst(const triton::arch::Register& reg) { 817 triton::ast::SharedAbstractNode node = nullptr; 818 triton::uint32 bvSize = reg.getBitSize(); 819 triton::uint32 high = reg.getHigh(); 820 triton::uint32 low = reg.getLow(); 821 triton::uint512 value = this->architecture->getConcreteRegisterValue(reg); 822 823 /* Check if the register is already symbolic */ 824 const SharedSymbolicExpression& symReg = this->getSymbolicRegister(reg); 825 if (symReg) node = this->astCtxt->extract(high, low, this->astCtxt->reference(symReg)); 826 else node = this->astCtxt->bv(value, bvSize); 827 828 /* extend AST if it's a extend operand (mainly used for AArch64) */ 829 if (reg.getExtendType() != triton::arch::arm::ID_EXTEND_INVALID) { 830 return this->getExtendAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node); 831 } 832 833 /* Shift AST if it's a shift operand (mainly used for Arm) */ 834 if (reg.getShiftType() != triton::arch::arm::ID_SHIFT_INVALID) { 835 return this->getShiftAst(static_cast<const triton::arch::arm::ArmOperandProperties>(reg), node); 836 } 837 838 return node; 839 } 840 841 842 /* Returns the AST corresponding to the register and defines the register as input of the instruction */ getRegisterAst(triton::arch::Instruction & inst,const triton::arch::Register & reg)843 triton::ast::SharedAbstractNode SymbolicEngine::getRegisterAst(triton::arch::Instruction& inst, const triton::arch::Register& reg) { 844 triton::ast::SharedAbstractNode node = this->getRegisterAst(reg); 845 inst.setReadRegister(reg, node); 846 return node; 847 } 848 849 850 /* Returns the new symbolic abstract expression and links this expression to the instruction. */ createSymbolicExpression(triton::arch::Instruction & inst,const triton::ast::SharedAbstractNode & node,const triton::arch::OperandWrapper & dst,const std::string & comment)851 const SharedSymbolicExpression& SymbolicEngine::createSymbolicExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::OperandWrapper& dst, const std::string& comment) { 852 switch (dst.getType()) { 853 case triton::arch::OP_MEM: return this->createSymbolicMemoryExpression(inst, node, dst.getConstMemory(), comment); 854 case triton::arch::OP_REG: return this->createSymbolicRegisterExpression(inst, node, dst.getConstRegister(), comment); 855 default: 856 throw triton::exceptions::SymbolicEngine("SymbolicEngine::createSymbolicExpression(): Invalid operand."); 857 } 858 } 859 860 861 /* Returns the new symbolic memory expression */ createSymbolicMemoryExpression(triton::arch::Instruction & inst,const triton::ast::SharedAbstractNode & node,const triton::arch::MemoryAccess & mem,const std::string & comment)862 const SharedSymbolicExpression& SymbolicEngine::createSymbolicMemoryExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::MemoryAccess& mem, const std::string& comment) { 863 std::vector<triton::ast::SharedAbstractNode> ret; 864 triton::ast::SharedAbstractNode tmp = nullptr; 865 SharedSymbolicExpression se = nullptr; 866 triton::uint64 address = mem.getAddress(); 867 triton::uint32 writeSize = mem.getSize(); 868 869 /* Record the aligned memory for a symbolic optimization */ 870 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) { 871 const SharedSymbolicExpression& aligned = this->newSymbolicExpression(node, MEMORY_EXPRESSION, "Aligned Byte reference - " + comment); 872 this->addAlignedMemory(address, writeSize, aligned); 873 } 874 875 /* 876 * As the x86's memory can be accessed without alignment, each byte of the 877 * memory must be assigned to an unique reference. 878 */ 879 ret.reserve(mem.getSize()); 880 while (writeSize) { 881 triton::uint32 high = ((writeSize * bitsize::byte) - 1); 882 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte); 883 /* Extract each byte of the memory */ 884 tmp = this->astCtxt->extract(high, low, node); 885 /* Assign each byte to a new symbolic expression */ 886 se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference - " + comment); 887 /* Set the origin of the symbolic expression */ 888 se->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte)); 889 /* ret is the for the final expression */ 890 ret.push_back(tmp); 891 /* add the symbolic expression to the instruction */ 892 inst.addSymbolicExpression(se); 893 /* Assign memory with little endian */ 894 this->addMemoryReference((address + writeSize) - 1, se); 895 /* continue */ 896 writeSize--; 897 } 898 899 /* Set implicit read of the base and index registers from an effective address */ 900 this->setImplicitReadRegisterFromEffectiveAddress(inst, mem); 901 902 /* Set explicit write of the memory access */ 903 inst.setStoreAccess(mem, node); 904 905 /* If there is only one reference, we return the symbolic expression */ 906 if (ret.size() == 1) { 907 /* Synchronize the concrete state */ 908 this->architecture->setConcreteMemoryValue(mem, tmp->evaluate()); 909 /* It will return se */ 910 return inst.symbolicExpressions.back(); 911 } 912 913 /* Otherwise, we return the concatenation of all symbolic expressions */ 914 tmp = this->astCtxt->concat(ret); 915 916 /* Synchronize the concrete state */ 917 this->architecture->setConcreteMemoryValue(mem, tmp->evaluate()); 918 919 se = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Temporary concatenation reference - " + comment); 920 se->setOriginMemory(triton::arch::MemoryAccess(address, mem.getSize())); 921 922 return inst.addSymbolicExpression(se); 923 } 924 925 926 /* Returns the parent AST after inserting the subregister (node) in its AST. */ insertSubRegisterInParent(const triton::arch::Register & reg,const triton::ast::SharedAbstractNode & node,bool zxForAssign)927 triton::ast::SharedAbstractNode SymbolicEngine::insertSubRegisterInParent(const triton::arch::Register& reg, const triton::ast::SharedAbstractNode& node, bool zxForAssign) { 928 const triton::arch::Register& parentReg = this->architecture->getParentRegister(reg); 929 930 /* If it's a flag register, there is nothing to do with sub register */ 931 if (this->architecture->isFlag(reg)) { 932 return node; 933 } 934 935 switch (reg.getSize()) { 936 /* ----------------------------------------------------------------*/ 937 case triton::size::byte: { 938 const auto& origReg = this->getRegisterAst(parentReg); 939 /* 940 * Mainly used for x86 941 * r[........xxxxxxxx] 942 */ 943 if (reg.getLow() == 0) { 944 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::byte, origReg); 945 return this->astCtxt->concat(keep, node); 946 } 947 /* 948 * Mainly used for x86 949 * r[xxxxxxxx........] 950 */ 951 else { 952 const auto& keep = this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg); 953 return this->astCtxt->concat(keep, this->astCtxt->concat(node, this->astCtxt->extract((bitsize::byte - 1), 0, origReg))); 954 } 955 } 956 957 /* ----------------------------------------------------------------*/ 958 case triton::size::word: { 959 const auto& origReg = this->getRegisterAst(parentReg); 960 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), bitsize::word, origReg), node); 961 } 962 963 /* ----------------------------------------------------------------*/ 964 case triton::size::dword: 965 case triton::size::qword: 966 case triton::size::dqword: 967 case triton::size::qqword: 968 case triton::size::dqqword: { 969 if (zxForAssign == false) { 970 if (parentReg.getBitSize() > reg.getBitSize()) { 971 const auto& origReg = this->getRegisterAst(parentReg); 972 return this->astCtxt->concat(this->astCtxt->extract((parentReg.getBitSize() - 1), reg.getHigh() + 1, origReg), node); 973 } 974 else { 975 return node; 976 } 977 } 978 /* zxForAssign == true */ 979 else { 980 return this->astCtxt->zx(parentReg.getBitSize() - node->getBitvectorSize(), node); 981 } 982 } 983 /* ----------------------------------------------------------------*/ 984 } 985 986 throw triton::exceptions::SymbolicEngine("SymbolicEngine::insertSubRegisterInParent(): Invalid register size."); 987 } 988 989 990 /* Returns the new symbolic register expression */ createSymbolicRegisterExpression(triton::arch::Instruction & inst,const triton::ast::SharedAbstractNode & node,const triton::arch::Register & reg,const std::string & comment)991 const SharedSymbolicExpression& SymbolicEngine::createSymbolicRegisterExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::Register& reg, const std::string& comment) { 992 SharedSymbolicExpression se = nullptr; 993 994 se = this->newSymbolicExpression(this->insertSubRegisterInParent(reg, node), REGISTER_EXPRESSION, comment); 995 this->assignSymbolicExpressionToRegister(se, this->architecture->getParentRegister(reg)); 996 997 inst.setWrittenRegister(reg, node); 998 return inst.addSymbolicExpression(se); 999 } 1000 1001 1002 /* Returns the new symbolic volatile expression */ createSymbolicVolatileExpression(triton::arch::Instruction & inst,const triton::ast::SharedAbstractNode & node,const std::string & comment)1003 const SharedSymbolicExpression& SymbolicEngine::createSymbolicVolatileExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const std::string& comment) { 1004 const SharedSymbolicExpression& se = this->newSymbolicExpression(node, VOLATILE_EXPRESSION, comment); 1005 return inst.addSymbolicExpression(se); 1006 } 1007 1008 1009 /* Adds and assign a new memory reference */ addMemoryReference(triton::uint64 mem,const SharedSymbolicExpression & expr)1010 inline void SymbolicEngine::addMemoryReference(triton::uint64 mem, const SharedSymbolicExpression& expr) { 1011 this->memoryReference[mem] = expr; 1012 } 1013 1014 1015 /* Assigns a symbolic expression to a register */ assignSymbolicExpressionToRegister(const SharedSymbolicExpression & se,const triton::arch::Register & reg)1016 void SymbolicEngine::assignSymbolicExpressionToRegister(const SharedSymbolicExpression& se, const triton::arch::Register& reg) { 1017 const triton::ast::SharedAbstractNode& node = se->getAst(); 1018 triton::uint32 id = reg.getParent(); 1019 1020 /* We can assign an expression only on parent registers */ 1021 if (reg.getId() != id) { 1022 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): We can assign an expression only on parent registers."); 1023 } 1024 1025 /* Check if the size of the symbolic expression is equal to the target register */ 1026 if (node->getBitvectorSize() != reg.getBitSize()) { 1027 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToRegister(): The size of the symbolic expression is not equal to the target register."); 1028 } 1029 1030 se->setType(REGISTER_EXPRESSION); 1031 se->setOriginRegister(reg); 1032 1033 if (reg.isMutable()) { 1034 /* Assign if this register is mutable */ 1035 this->symbolicReg[id] = se; 1036 /* Synchronize the concrete state */ 1037 this->architecture->setConcreteRegisterValue(reg, node->evaluate()); 1038 } 1039 } 1040 1041 1042 /* Assigns a symbolic expression to a memory */ assignSymbolicExpressionToMemory(const SharedSymbolicExpression & se,const triton::arch::MemoryAccess & mem)1043 void SymbolicEngine::assignSymbolicExpressionToMemory(const SharedSymbolicExpression& se, const triton::arch::MemoryAccess& mem) { 1044 const triton::ast::SharedAbstractNode& node = se->getAst(); 1045 triton::uint64 address = mem.getAddress(); 1046 triton::uint32 writeSize = mem.getSize(); 1047 1048 /* Check if the size of the symbolic expression is equal to the memory access */ 1049 if (node->getBitvectorSize() != mem.getBitSize()) { 1050 throw triton::exceptions::SymbolicEngine("SymbolicEngine::assignSymbolicExpressionToMemory(): The size of the symbolic expression is not equal to the memory access."); 1051 } 1052 1053 /* Record the aligned memory for a symbolic optimization */ 1054 if (this->modes->isModeEnabled(triton::modes::ALIGNED_MEMORY)) { 1055 this->addAlignedMemory(address, writeSize, se); 1056 } 1057 1058 /* 1059 * As the x86's memory can be accessed without alignment, each byte of the 1060 * memory must be assigned to an unique reference. 1061 */ 1062 while (writeSize) { 1063 triton::uint32 high = ((writeSize * bitsize::byte) - 1); 1064 triton::uint32 low = ((writeSize * bitsize::byte) - bitsize::byte); 1065 /* Extract each byte of the memory */ 1066 const triton::ast::SharedAbstractNode& tmp = this->astCtxt->extract(high, low, node); 1067 /* For each byte create a new symbolic expression */ 1068 const SharedSymbolicExpression& byteRef = this->newSymbolicExpression(tmp, MEMORY_EXPRESSION, "Byte reference"); 1069 /* Set the origin of the symbolic expression */ 1070 byteRef->setOriginMemory(triton::arch::MemoryAccess(((address + writeSize) - 1), triton::size::byte)); 1071 /* Assign memory with little endian */ 1072 this->addMemoryReference((address + writeSize) - 1, byteRef); 1073 /* continue */ 1074 writeSize--; 1075 } 1076 1077 /* Synchronize the concrete state */ 1078 this->architecture->setConcreteMemoryValue(mem, node->evaluate()); 1079 } 1080 1081 1082 /* Returns true if the symbolic engine is enable */ isEnabled(void) const1083 bool SymbolicEngine::isEnabled(void) const { 1084 return this->enableFlag; 1085 } 1086 1087 1088 /* Returns true if the symbolic expression ID exists */ isSymbolicExpressionExists(triton::usize symExprId) const1089 bool SymbolicEngine::isSymbolicExpressionExists(triton::usize symExprId) const { 1090 auto it = this->symbolicExpressions.find(symExprId); 1091 1092 if (it != this->symbolicExpressions.end()) { 1093 return (it->second.use_count() > 0); 1094 } 1095 1096 return false; 1097 } 1098 1099 1100 /* Returns true if memory cell expressions contain symbolic variables. */ isMemorySymbolized(const triton::arch::MemoryAccess & mem) const1101 bool SymbolicEngine::isMemorySymbolized(const triton::arch::MemoryAccess& mem) const { 1102 triton::uint64 addr = mem.getAddress(); 1103 triton::uint32 size = mem.getSize(); 1104 1105 return this->isMemorySymbolized(addr, size); 1106 } 1107 1108 1109 /* Returns true if memory cell expressions contain symbolic variables. */ isMemorySymbolized(triton::uint64 addr,triton::uint32 size) const1110 bool SymbolicEngine::isMemorySymbolized(triton::uint64 addr, triton::uint32 size) const { 1111 for (triton::uint32 i = 0; i < size; i++) { 1112 const SharedSymbolicExpression& expr = this->getSymbolicMemory(addr + i); 1113 if (expr && expr->isSymbolized()) { 1114 return true; 1115 } 1116 } 1117 return false; 1118 } 1119 1120 1121 /* Returns true if the register expression contains a symbolic variable. */ isRegisterSymbolized(const triton::arch::Register & reg) const1122 bool SymbolicEngine::isRegisterSymbolized(const triton::arch::Register& reg) const { 1123 const SharedSymbolicExpression& expr = this->getSymbolicRegister(reg); 1124 if (expr) { 1125 return expr->isSymbolized(); 1126 } 1127 return false; 1128 } 1129 1130 1131 /* Enables or disables the symbolic engine */ enable(bool flag)1132 void SymbolicEngine::enable(bool flag) { 1133 this->enableFlag = flag; 1134 } 1135 1136 1137 /* Initializes the memory access AST (LOAD and STORE) */ initLeaAst(triton::arch::MemoryAccess & mem,bool force)1138 void SymbolicEngine::initLeaAst(triton::arch::MemoryAccess& mem, bool force) { 1139 if (mem.getBitSize() >= bitsize::byte) { 1140 const triton::arch::Register& base = mem.getConstBaseRegister(); 1141 const triton::arch::Register& index = mem.getConstIndexRegister(); 1142 const triton::arch::Register& seg = mem.getConstSegmentRegister(); 1143 triton::uint64 segmentValue = (this->architecture->isRegisterValid(seg) ? this->architecture->getConcreteRegisterValue(seg).convert_to<triton::uint64>() : 0); 1144 triton::uint64 scaleValue = mem.getConstScale().getValue(); 1145 triton::uint64 dispValue = mem.getConstDisplacement().getValue(); 1146 triton::uint32 bitSize = (this->architecture->isRegisterValid(base) ? base.getBitSize() : 1147 (this->architecture->isRegisterValid(index) ? index.getBitSize() : 1148 (mem.getConstDisplacement().getBitSize() ? mem.getConstDisplacement().getBitSize() : 1149 this->architecture->gprBitSize() 1150 ) 1151 ) 1152 ); 1153 1154 1155 /* Initialize the AST of the memory access (LEA) -> ((pc + base) + (index * scale) + disp) */ 1156 auto pcPlusBaseAst = mem.getPcRelative() ? this->astCtxt->bv(mem.getPcRelative(), bitSize) : 1157 (this->architecture->isRegisterValid(base) ? this->getRegisterAst(base) : 1158 this->astCtxt->bv(0, bitSize)); 1159 1160 auto indexMulScaleAst = this->astCtxt->bvmul( 1161 (this->architecture->isRegisterValid(index) ? this->getRegisterAst(index) : this->astCtxt->bv(0, bitSize)), 1162 this->astCtxt->bv(scaleValue, bitSize) 1163 ); 1164 1165 auto dispAst = this->astCtxt->bv(dispValue, bitSize); 1166 auto leaAst = this->astCtxt->bvadd( 1167 index.isSubtracted() ? this->astCtxt->bvsub(pcPlusBaseAst, indexMulScaleAst) : this->astCtxt->bvadd(pcPlusBaseAst, indexMulScaleAst), 1168 dispAst 1169 ); 1170 1171 /* Use segments as base address instead of selector into the GDT. */ 1172 if (segmentValue) { 1173 leaAst = this->astCtxt->bvadd( 1174 this->astCtxt->bv(segmentValue, seg.getBitSize()), 1175 this->astCtxt->sx((seg.getBitSize() - bitSize), leaAst) 1176 ); 1177 } 1178 1179 /* Set AST */ 1180 mem.setLeaAst(leaAst); 1181 1182 /* Initialize the address only if it is not already defined */ 1183 if (!mem.getAddress() || force) 1184 mem.setAddress(leaAst->evaluate().convert_to<triton::uint64>()); 1185 } 1186 } 1187 1188 getConcreteVariableValue(const SharedSymbolicVariable & symVar) const1189 triton::uint512 SymbolicEngine::getConcreteVariableValue(const SharedSymbolicVariable& symVar) const { 1190 return this->astCtxt->getVariableValue(symVar->getName()); 1191 } 1192 1193 setConcreteVariableValue(const SharedSymbolicVariable & symVar,const triton::uint512 & value)1194 void SymbolicEngine::setConcreteVariableValue(const SharedSymbolicVariable& symVar, const triton::uint512& value) { 1195 triton::uint512 max = -1; 1196 1197 /* Check if the value is too big */ 1198 max = max >> (512 - symVar->getSize()); 1199 if (value > max) { 1200 throw triton::exceptions::SymbolicEngine("SymbolicEngine::setConcreteVariableValue(): Can not set this value (too big) to this symbolic variable."); 1201 } 1202 1203 /* Update the symbolic variable value */ 1204 this->astCtxt->updateVariable(symVar->getName(), value); 1205 1206 /* Synchronize concrete state */ 1207 if (symVar->getType() == REGISTER_VARIABLE) { 1208 const triton::arch::Register& reg = this->architecture->getRegister(static_cast<triton::arch::register_e>(symVar->getOrigin())); 1209 this->architecture->setConcreteRegisterValue(reg, value); 1210 } 1211 1212 else if (symVar->getType() == MEMORY_VARIABLE && symVar->getSize() && !(symVar->getSize() % bitsize::byte)) { 1213 triton::uint64 addr = symVar->getOrigin(); 1214 triton::uint32 size = symVar->getSize() / bitsize::byte; 1215 triton::arch::MemoryAccess mem = triton::arch::MemoryAccess(addr, size); 1216 1217 this->architecture->setConcreteMemoryValue(mem, value); 1218 } 1219 } 1220 1221 }; /* symbolic namespace */ 1222 }; /* engines namespace */ 1223 }; /*triton namespace */ 1224