Provide a standalone static IR #473
Assignees
Labels
Comments
|
An even better option would be a version of processing() that stores the before/after values of each written register and memory but without updating the global state used by set/getConcreteMemory/RegisterValue. Then I could call this function, check the values, and depending on the situation, commit the changes to the global state. |
|
That's exactly what I want in long term.
|
JonathanSalwan
changed the title
Closed
|
Ok, for a first try it looks not too bad. Below, a patch for the aarch64 semantics. The idea is to make all expressions volatile, and then, assign these expressions to their destination in diff --git a/src/libtriton/arch/arm/aarch64/aarch64Semantics.cpp b/src/libtriton/arch/arm/aarch64/aarch64Semantics.cpp
index 4eba9e95..a39ddd1a 100644
--- a/src/libtriton/arch/arm/aarch64/aarch64Semantics.cpp
+++ b/src/libtriton/arch/arm/aarch64/aarch64Semantics.cpp
@@ -311,7 +311,7 @@ namespace triton {
auto node = this->astCtxt->bv(inst.getNextAddress(), pc.getBitSize());
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicRegisterExpression(inst, node, this->architecture->getParentRegister(ID_REG_AARCH64_PC), "Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, pc, "Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(this->architecture->getParentRegister(ID_REG_AARCH64_PC), triton::engines::taint::UNTAINTED);
@@ -573,7 +573,7 @@ namespace triton {
auto node = this->astCtxt->bv(0, 1);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, flag, comment);
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
@@ -585,7 +585,7 @@ namespace triton {
auto node = this->astCtxt->bv(1, 1);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, flag, comment);
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, flag, comment);
/* Spread taint */
expr->isTainted = this->taintEngine->setTaintRegister(flag, triton::engines::taint::UNTAINTED);
@@ -606,7 +606,7 @@ namespace triton {
auto node = this->astCtxt->extract(high, high, this->astCtxt->reference(parent));
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, nf, "Negative flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, nf, "Negative flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(nf, parent->isTainted);
@@ -630,7 +630,7 @@ namespace triton {
auto node3 = this->getCodeConditionAst(inst, node1, node2);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, nf, "Negative flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, nf, "Negative flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(nf, parent->isTainted);
@@ -660,7 +660,7 @@ namespace triton {
);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, zf, "Zero flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, zf, "Zero flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(zf, parent->isTainted);
@@ -693,7 +693,7 @@ namespace triton {
auto node3 = this->getCodeConditionAst(inst, node1, node2);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, zf, "Zero flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, zf, "Zero flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(zf, parent->isTainted);
@@ -728,7 +728,7 @@ namespace triton {
);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf, "Carry flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, cf, "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
@@ -764,7 +764,7 @@ namespace triton {
);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, cf, "Carry flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, cf, "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
@@ -806,7 +806,7 @@ namespace triton {
auto node3 = this->getCodeConditionAst(inst, node1, node2);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, cf, "Carry flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, cf, "Carry flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(cf, parent->isTainted);
@@ -836,7 +836,7 @@ namespace triton {
);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, vf, "Overflow flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, vf, "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
@@ -866,7 +866,7 @@ namespace triton {
);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, vf, "Overflow flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, vf, "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
@@ -902,7 +902,7 @@ namespace triton {
auto node3 = this->getCodeConditionAst(inst, node1, node2);
/* Create the symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node3, vf, "Overflow flag");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, vf, "Overflow flag");
/* Spread the taint from the parent to the child */
expr->isTainted = this->taintEngine->setTaintRegister(vf, parent->isTainted);
@@ -924,7 +924,7 @@ namespace triton {
auto node = this->astCtxt->bvadd(this->astCtxt->bvadd(op1, op2), this->astCtxt->zx(dst.getBitSize()-1, op3));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADC operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ADC operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(cf));
@@ -947,7 +947,7 @@ namespace triton {
auto node = this->astCtxt->bvadd(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADD(S) operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ADD(S) operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -978,7 +978,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ADR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src) | this->taintEngine->isTainted(pc));
@@ -1001,7 +1001,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ADRP operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ADRP operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src) | this->taintEngine->isTainted(pc));
@@ -1024,7 +1024,7 @@ namespace triton {
auto node = this->astCtxt->bvand(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "AND(S) operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "AND(S) operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1055,7 +1055,7 @@ namespace triton {
auto node = this->astCtxt->bvashr(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ASR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ASR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1077,7 +1077,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "B operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "B operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
@@ -1123,7 +1123,7 @@ namespace triton {
auto node = this->astCtxt->concat(chunks);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BFI operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "BFI operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src1);
@@ -1146,7 +1146,7 @@ namespace triton {
auto node = this->astCtxt->bvand(op1, this->astCtxt->bvnot(op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BIC operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "BIC operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1166,8 +1166,8 @@ namespace triton {
auto node2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "BL operation - Link Register");
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BL operation - Program Counter");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst1, "BL operation - Link Register");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, dst2, "BL operation - Program Counter");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
@@ -1191,8 +1191,8 @@ namespace triton {
auto node2 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "BLR operation - Link Register");
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "BLR operation - Program Counter");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst1, "BLR operation - Link Register");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, dst2, "BLR operation - Program Counter");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
@@ -1214,7 +1214,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "BR operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "BR operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1244,7 +1244,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBNZ operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CBNZ operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1275,7 +1275,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CBZ operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CBZ operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1331,7 +1331,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op2, op1);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CINC operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CINC operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
@@ -1463,7 +1463,7 @@ namespace triton {
}
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CLZ operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CLZ operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1542,7 +1542,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSEL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CSEL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1563,7 +1563,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSET operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CSET operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->getCodeConditionTainteSate(inst));
@@ -1589,7 +1589,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSINC operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CSINC operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1612,7 +1612,7 @@ namespace triton {
auto node = this->getCodeConditionAst(inst, op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "CSNEG operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "CSNEG operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1635,7 +1635,7 @@ namespace triton {
auto node = this->astCtxt->bvxnor(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EON operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "EON operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1658,7 +1658,7 @@ namespace triton {
auto node = this->astCtxt->bvxor(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EOR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "EOR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -1683,7 +1683,7 @@ namespace triton {
auto node = this->astCtxt->extract(lsb + dst.getBitSize() - 1, lsb, this->astCtxt->concat(op1, op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "EXTR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "EXTR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -1701,7 +1701,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAR operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDAR operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1722,7 +1722,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDARB operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDARB operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1743,7 +1743,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDARH operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDARH operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1761,7 +1761,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXR operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDAXR operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1782,7 +1782,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXRB operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDAXRB operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1803,7 +1803,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDAXRH operation - LOAD access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDAXRH operation - LOAD access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1829,8 +1829,8 @@ namespace triton {
auto node2 = this->astCtxt->extract((dst1.getBitSize() + dst2.getBitSize()) - 1, dst1.getBitSize(), op);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst1, "LDP operation - LOAD access");
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, dst2, "LDP operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst1, "LDP operation - LOAD access");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, dst2, "LDP operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst1, src);
@@ -1850,7 +1850,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDP operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDP operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -1864,7 +1864,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDP operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDP operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -1883,7 +1883,7 @@ namespace triton {
auto node1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDR operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDR operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1902,7 +1902,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDR operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDR operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -1916,7 +1916,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDR operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDR operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -1938,7 +1938,7 @@ namespace triton {
auto node1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRB operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDRB operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -1957,7 +1957,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRB operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDRB operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -1971,7 +1971,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRB operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDRB operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -1993,7 +1993,7 @@ namespace triton {
auto node1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRH operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDRH operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2012,7 +2012,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRH operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDRH operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -2026,7 +2026,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRH operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDRH operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -2051,7 +2051,7 @@ namespace triton {
auto node1 = this->astCtxt->sx(dst.getBitSize() - 8, op);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSB operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDRSB operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2070,7 +2070,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSB operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDRSB operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -2084,7 +2084,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSB operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDRSB operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -2109,7 +2109,7 @@ namespace triton {
auto node1 = this->astCtxt->sx(dst.getBitSize() - 16, op);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSH operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDRSH operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2128,7 +2128,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSH operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDRSH operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -2142,7 +2142,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSH operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDRSH operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -2167,7 +2167,7 @@ namespace triton {
auto node1 = this->astCtxt->sx(dst.getBitSize() - 32, op);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "LDRSW operation - LOAD access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "LDRSW operation - LOAD access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2186,7 +2186,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "LDRSW operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "LDRSW operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -2200,7 +2200,7 @@ namespace triton {
auto node3 = src.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "LDRSW operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "LDRSW operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -2219,7 +2219,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDUR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDUR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2243,7 +2243,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 8, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDURB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2267,7 +2267,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 16, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDURH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2291,7 +2291,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 8, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDURSB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2315,7 +2315,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 16, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDURSH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2339,7 +2339,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 32, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDURSW operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDURSW operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2357,7 +2357,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDXR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2381,7 +2381,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 8, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXRB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDXRB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2405,7 +2405,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 16, op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LDXRH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LDXRH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2432,7 +2432,7 @@ namespace triton {
auto node = this->astCtxt->bvshl(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LSL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LSL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2459,7 +2459,7 @@ namespace triton {
auto node = this->astCtxt->bvlshr(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "LSR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "LSR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2484,7 +2484,7 @@ namespace triton {
auto node = this->astCtxt->bvadd(op3, this->astCtxt->bvmul(op1, op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MADD operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MADD operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -2507,7 +2507,7 @@ namespace triton {
auto node = this->astCtxt->bvneg(this->astCtxt->bvmul(op1, op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MNEG operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MNEG operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2525,7 +2525,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOV operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MOV operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2589,7 +2589,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVK operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MOVK operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintUnion(dst, src);
@@ -2610,7 +2610,7 @@ namespace triton {
auto node = this->astCtxt->bvnot(op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVN operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MOVN operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2628,7 +2628,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MOVZ operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MOVZ operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2653,7 +2653,7 @@ namespace triton {
auto node = this->astCtxt->bvsub(op3, this->astCtxt->bvmul(op1, op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MSUB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MSUB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -2676,7 +2676,7 @@ namespace triton {
auto node = this->astCtxt->bvmul(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MUL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MUL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2697,7 +2697,7 @@ namespace triton {
auto node = this->astCtxt->bvnot(op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MVN operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MVN operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2718,7 +2718,7 @@ namespace triton {
auto node = this->astCtxt->bvneg(op);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "MEG operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "MEG operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2747,7 +2747,7 @@ namespace triton {
auto node = this->astCtxt->bvor(op1, this->astCtxt->bvnot(op2));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ORN operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ORN operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2770,7 +2770,7 @@ namespace triton {
auto node = this->astCtxt->bvor(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ORR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ORR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2798,7 +2798,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "RBIT operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "RBIT operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2816,7 +2816,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "RET operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "RET operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2853,7 +2853,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "REV operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2894,7 +2894,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV16 operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "REV16 operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2927,7 +2927,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "REV32 operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "REV32 operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -2950,7 +2950,7 @@ namespace triton {
auto node = this->astCtxt->bvror(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "ROR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "ROR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -2978,7 +2978,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - width, this->astCtxt->extract(lsb+width-1, lsb, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SBFX operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SBFX operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
@@ -3005,7 +3005,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SDIV operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SDIV operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3036,7 +3036,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMADDL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SMADDL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -3067,7 +3067,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMSUBL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SMSUBL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -3097,7 +3097,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMULH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SMULH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3123,7 +3123,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SMULL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SMULL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3141,7 +3141,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLR operation - STORE access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STLR operation - STORE access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3162,7 +3162,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(7, 0));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLRB operation - STORE access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STLRB operation - STORE access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3183,7 +3183,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(15, 0));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STLRH operation - STORE access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STLRH operation - STORE access");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3209,7 +3209,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(node->getBitvectorSize()-1, 0));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STP operation - STORE access");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STP operation - STORE access");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3228,7 +3228,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STP operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "STP operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -3242,7 +3242,7 @@ namespace triton {
auto node3 = dst.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STP operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "STP operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -3261,7 +3261,7 @@ namespace triton {
auto node1 = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STR operation - STORE access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "STR operation - STORE access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3280,7 +3280,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STR operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "STR operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -3294,7 +3294,7 @@ namespace triton {
auto node3 = dst.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STR operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "STR operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -3319,7 +3319,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(7, 0));
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STRB operation - STORE access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "STRB operation - STORE access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3338,7 +3338,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STRB operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "STRB operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -3352,7 +3352,7 @@ namespace triton {
auto node3 = dst.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STRB operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "STRB operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -3377,7 +3377,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(15, 0));
/* Create symbolic expression */
- auto expr1 = this->symbolicEngine->createSymbolicExpression(inst, node1, dst, "STRH operation - STORE access");
+ auto expr1 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node1, dst, "STRH operation - STORE access");
/* Spread taint */
expr1->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3396,7 +3396,7 @@ namespace triton {
auto node2 = this->astCtxt->bvadd(baseNode, this->astCtxt->sx(base.getBitSize() - imm.getBitSize(), immNode));
/* Create symbolic expression */
- auto expr2 = this->symbolicEngine->createSymbolicExpression(inst, node2, base, "STRH operation - Base register computation");
+ auto expr2 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node2, base, "STRH operation - Base register computation");
/* Spread taint */
expr2->isTainted = this->taintEngine->isTainted(base);
@@ -3410,7 +3410,7 @@ namespace triton {
auto node3 = dst.getMemory().getLeaAst();
/* Create symbolic expression */
- auto expr3 = this->symbolicEngine->createSymbolicExpression(inst, node3, base, "STRH operation - Base register computation");
+ auto expr3 = this->symbolicEngine->createSymbolicVolatileExpression(inst, node3, base, "STRH operation - Base register computation");
/* Spread taint */
expr3->isTainted = this->taintEngine->isTainted(base);
@@ -3429,7 +3429,7 @@ namespace triton {
auto node = this->symbolicEngine->getOperandAst(inst, src);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STUR operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STUR operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3453,7 +3453,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(7, 0));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STURB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STURB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3477,7 +3477,7 @@ namespace triton {
dst.getMemory().setPair(std::make_pair(15, 0));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "STURH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "STURH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3500,7 +3500,7 @@ namespace triton {
auto node = this->astCtxt->bvsub(op1, op2);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SUB(S) operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SUB(S) operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3540,7 +3540,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 8, this->astCtxt->extract(7, 0, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SXTB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3561,7 +3561,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 16, this->astCtxt->extract(15, 0, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SXTH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3582,7 +3582,7 @@ namespace triton {
auto node = this->astCtxt->sx(dst.getBitSize() - 32, this->astCtxt->extract(31, 0, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "SXTW operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "SXTW operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3614,7 +3614,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "TBNZ operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "TBNZ operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3643,7 +3643,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "TBZ operation - Program Counter");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "TBZ operation - Program Counter");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3711,7 +3711,7 @@ namespace triton {
auto node = this->astCtxt->concat(bits);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UBFIZ operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UBFIZ operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
@@ -3739,7 +3739,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - width, this->astCtxt->extract(lsb+width-1, lsb, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UBFX operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UBFX operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src1);
@@ -3766,7 +3766,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UDIV operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UDIV operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3797,7 +3797,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMADDL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UMADDL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -3825,7 +3825,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMNEGL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UMNEGL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3856,7 +3856,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMSUBL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UMSUBL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2) | this->taintEngine->isTainted(src3));
@@ -3886,7 +3886,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMULH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UMULH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3912,7 +3912,7 @@ namespace triton {
);
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UMULL operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UMULL operation");
/* Spread taint */
expr->isTainted = this->taintEngine->setTaint(dst, this->taintEngine->isTainted(src1) | this->taintEngine->isTainted(src2));
@@ -3933,7 +3933,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 8, this->astCtxt->extract(7, 0, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UXTB operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UXTB operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
@@ -3954,7 +3954,7 @@ namespace triton {
auto node = this->astCtxt->zx(dst.getBitSize() - 16, this->astCtxt->extract(15, 0, op));
/* Create symbolic expression */
- auto expr = this->symbolicEngine->createSymbolicExpression(inst, node, dst, "UXTH operation");
+ auto expr = this->symbolicEngine->createSymbolicVolatileExpression(inst, node, dst, "UXTH operation");
/* Spread taint */
expr->isTainted = this->taintEngine->taintAssignment(dst, src);
diff --git a/src/libtriton/arch/irBuilder.cpp b/src/libtriton/arch/irBuilder.cpp
index 21b99c2e..57f7eaca 100644
--- a/src/libtriton/arch/irBuilder.cpp
+++ b/src/libtriton/arch/irBuilder.cpp
@@ -97,6 +97,20 @@ namespace triton {
/* Post IR processing */
this->postIrInit(inst);
+ /* commit expressions */
+ for (const auto& se : inst.symbolicExpressions) {
+ switch (se->getType()) {
+ case triton::engines::symbolic::REGISTER_EXPRESSION:
+ this->symbolicEngine->assignSymbolicExpressionToRegister(se, se->getOriginRegister());
+ break;
+ case triton::engines::symbolic::MEMORY_EXPRESSION:
+ this->symbolicEngine->assignSymbolicExpressionToMemory(se, se->getOriginMemory());
+ break;
+ default:
+ break;
+ }
+ }
+
return ret;
}
diff --git a/src/libtriton/engines/symbolic/symbolicEngine.cpp b/src/libtriton/engines/symbolic/symbolicEngine.cpp
index e7e63138..65eccbe2 100644
--- a/src/libtriton/engines/symbolic/symbolicEngine.cpp
+++ b/src/libtriton/engines/symbolic/symbolicEngine.cpp
@@ -1014,6 +1014,25 @@ namespace triton {
}
+ /* Returns the new symbolic volatile expression */
+ const SharedSymbolicExpression& SymbolicEngine::createSymbolicVolatileExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::OperandWrapper& dst, const std::string& comment) {
+ switch (dst.getType()) {
+ case triton::arch::OP_MEM: {
+ const SharedSymbolicExpression& se = this->newSymbolicExpression(this->astCtxt->extract(dst.getBitSize()-2, 0, node), MEMORY_EXPRESSION, comment);
+ se->setOriginMemory(dst.getConstMemory());
+ return inst.addSymbolicExpression(se);
+ }
+ case triton::arch::OP_REG: {
+ const SharedSymbolicExpression& se = this->newSymbolicExpression(this->insertSubRegisterInParent(dst.getConstRegister(), node), REGISTER_EXPRESSION, comment);
+ se->setOriginRegister(this->architecture->getParentRegister(dst.getConstRegister()));
+ return inst.addSymbolicExpression(se);
+ }
+ default:
+ throw triton::exceptions::SymbolicEngine("SymbolicEngine::createSymbolicVolatileExpression(): Invalid destination.");
+ }
+ }
+
+
/* Adds and assign a new memory reference */
inline void SymbolicEngine::addMemoryReference(triton::uint64 mem, const SharedSymbolicExpression& expr) {
this->memoryReference[mem] = expr;
diff --git a/src/libtriton/includes/triton/symbolicEngine.hpp b/src/libtriton/includes/triton/symbolicEngine.hpp
index c69971cb..7d1940f5 100644
--- a/src/libtriton/includes/triton/symbolicEngine.hpp
+++ b/src/libtriton/includes/triton/symbolicEngine.hpp
@@ -247,6 +247,7 @@ namespace triton {
//! Returns the new shared symbolic volatile expression expression and links this expression to the instruction.
TRITON_EXPORT const SharedSymbolicExpression& createSymbolicVolatileExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const std::string& comment="");
+ TRITON_EXPORT const SharedSymbolicExpression& createSymbolicVolatileExpression(triton::arch::Instruction& inst, const triton::ast::SharedAbstractNode& node, const triton::arch::OperandWrapper& dst, const std::string& comment="");
//! Assigns a symbolic expression to a register.
TRITON_EXPORT void assignSymbolicExpressionToRegister(const SharedSymbolicExpression& se, const triton::arch::Register& reg); |
|
Some brainstorming with @RobinDavid
Dunno yet if the game is worth the candle |
JonathanSalwan
changed the title
This was referenced Jul 16, 2020
Closed
|
If you are familiar with BAP you might be interested in their approach of uplifting directly to something like SMT - Core theory/Knowledge Base:
This is how ARM lifter looks like with this representation: Since Triton effectively uses Z3, reducing unnecessary middleman of the "classic IR" might be desirable. |
|
Note to myself: To implement a static IR we must not used |
46 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Is there a simple way to find out what the value of the written registers/memory was before an instruction? Calling processing on an instruction changes the register values, but I can't find a function that fills in only the written register/memory variables without also carrying out the write so I can't query the old value afterwards.
The text was updated successfully, but these errors were encountered: