Symbolized pointers mode

src/libtriton/api/api.cpp

@@ -673,6 +673,12 @@ namespace triton {
   }
 
 
+  triton::ast::SharedAbstractNode API::getMemoryAst(const triton::ast::SharedAbstractNode& reg, triton::uint64 offset, triton::uint32 size) {
+    this->checkSymbolic();
+    return this->symbolic->getMemoryAst(reg, offset, size);
+  }
+
+
   triton::ast::SharedAbstractNode API::getRegisterAst(const triton::arch::Register& reg) {
     this->checkSymbolic();
     return this->symbolic->getRegisterAst(reg);

src/libtriton/ast/ast.cpp

@@ -2277,6 +2277,109 @@ namespace triton {
       return triton::ast::rotl(h, deep);
     }
 
+
+    /* ====== array */
+
+
+    ArrayNode::ArrayNode(triton::uint32 addrSize, AstContext& ctxt): AbstractNode(ARRAY_NODE, ctxt) {
+      this->addChild(ctxt.decimal(addrSize));
+    }
+
+
+    void ArrayNode::init(void) {
+      /* Init attributes */
+      this->eval        = 0;
+      this->size        = 8;
+      this->symbolized  = true;
+
+      /* Init children and spread information */
+      for (triton::uint32 index = 0; index < this->children.size(); index++) {
+        this->children[index]->setParent(this);
+        this->symbolized |= this->children[index]->isSymbolized();
+      }
+
+      /* Init parents */
+      this->initParents();
+    }
+
+
+    triton::uint512 ArrayNode::hash(triton::uint32 deep) const {
+      triton::uint512 h = this->kind, s = this->children.size();
+      if (s) h = h * s;
+      for (triton::uint32 index = 0; index < this->children.size(); index++)
+        h = h * triton::ast::hash2n(this->children[index]->hash(deep+1), index+1);
+      return triton::ast::rotl(h, deep);
+    }
+
+
+    /* ====== select */
+
+
+    SelectNode::SelectNode(const SharedAbstractNode& a, const SharedAbstractNode& i): AbstractNode(SELECT_NODE, a->getContext()) {
+      this->addChild(a);
+      this->addChild(i);
+    }
+
+
+    void SelectNode::init(void) {
+      /* Init attributes */
+      this->eval        = 0; // TODO
+      this->size        = this->children[0]->getBitvectorSize();
+
+      /* Init children and spread information */
+      for (triton::uint32 index = 0; index < this->children.size(); index++) {
+        this->children[index]->setParent(this);
+        this->symbolized |= this->children[index]->isSymbolized();
+      }
+
+      /* Init parents */
+      this->initParents();
+    }
+
+
+    triton::uint512 SelectNode::hash(triton::uint32 deep) const {
+      triton::uint512 h = this->kind, s = this->children.size();
+      if (s) h = h * s;
+      for (triton::uint32 index = 0; index < this->children.size(); index++)
+        h = h * triton::ast::hash2n(this->children[index]->hash(deep+1), index+1);
+      return triton::ast::rotl(h, deep);
+    }
+
+
+    /* ====== store */
+
+
+    StoreNode::StoreNode(const SharedAbstractNode& a, const SharedAbstractNode& i, const SharedAbstractNode& v): AbstractNode(STORE_NODE, a->getContext()) {
+      this->addChild(a);
+      this->addChild(i);
+      this->addChild(v);
+    }
+
+
+    void StoreNode::init(void) {
+      /* Init attributes */
+      this->eval        = 0; // TODO
+      this->size        = this->children[0]->getBitvectorSize();
+
+      /* Init children and spread information */
+      for (triton::uint32 index = 0; index < this->children.size(); index++) {
+        this->children[index]->setParent(this);
+        this->symbolized |= this->children[index]->isSymbolized();
+      }
+
+      /* Init parents */
+      this->initParents();
+    }
+
+
+    triton::uint512 StoreNode::hash(triton::uint32 deep) const {
+      triton::uint512 h = this->kind, s = this->children.size();
+      if (s) h = h * s;
+      for (triton::uint32 index = 0; index < this->children.size(); index++)
+        h = h * triton::ast::hash2n(this->children[index]->hash(deep+1), index+1);
+      return triton::ast::rotl(h, deep);
+    }
+
   }; /* ast namespace */
 }; /* triton namespace */
 
@@ -2415,6 +2518,9 @@ namespace triton {
         case SX_NODE:                   newNode = std::make_shared<SxNode>(*reinterpret_cast<SxNode*>(node)); break;
         case VARIABLE_NODE:             newNode = std::make_shared<VariableNode>(*reinterpret_cast<VariableNode*>(node)); break;
         case ZX_NODE:                   newNode = std::make_shared<ZxNode>(*reinterpret_cast<ZxNode*>(node)); break;
+        case ARRAY_NODE:                newNode = std::make_shared<ArrayNode>(*reinterpret_cast<ArrayNode*>(node)); break;
+        case SELECT_NODE:               newNode = std::make_shared<SelectNode>(*reinterpret_cast<SelectNode*>(node)); break;
+        case STORE_NODE:                newNode = std::make_shared<StoreNode>(*reinterpret_cast<StoreNode*>(node)); break;
         default:
           throw triton::exceptions::Ast("triton::ast::newInstance(): Invalid kind node.");
       }

src/libtriton/ast/astContext.cpp

@@ -547,6 +547,39 @@ namespace triton {
     }
 
 
+    SharedAbstractNode AstContext::array(triton::uint32 addrSize) {
+      SharedAbstractNode node = std::make_shared<ArrayNode>(addrSize, *this);
+
+      if (node == nullptr)
+        throw triton::exceptions::Ast("Node builders - Not enough memory");
+
+      node->init();
+      return node;
+    }
+
+
+    SharedAbstractNode AstContext::select(const SharedAbstractNode& a, const SharedAbstractNode& i) {
+      SharedAbstractNode node = std::make_shared<SelectNode>(a, i);
+
+      if (node == nullptr)
+        throw triton::exceptions::Ast("Node builders - Not enough memory");
+
+      node->init();
+      return node;
+    }
+
+
+    SharedAbstractNode AstContext::store(const SharedAbstractNode& a, const SharedAbstractNode& i, const SharedAbstractNode& v) {
+      SharedAbstractNode node = std::make_shared<StoreNode>(a, i, v);
+
+      if (node == nullptr)
+        throw triton::exceptions::Ast("Node builders - Not enough memory");
+
+      node->init();
+      return node;
+    }
+
+
     void AstContext::initVariable(const std::string& name, const triton::uint512& value, const SharedAbstractNode& node) {
       auto it = this->valueMapping.find(name);
       if (it == this->valueMapping.end())

src/libtriton/ast/representations/astPythonRepresentation.cpp

@@ -71,6 +71,9 @@ namespace triton {
           case SX_NODE:                   return this->print(stream, reinterpret_cast<triton::ast::SxNode*>(node)); break;
           case VARIABLE_NODE:             return this->print(stream, reinterpret_cast<triton::ast::VariableNode*>(node)); break;
           case ZX_NODE:                   return this->print(stream, reinterpret_cast<triton::ast::ZxNode*>(node)); break;
+          case ARRAY_NODE:                return this->print(stream, reinterpret_cast<triton::ast::ArrayNode*>(node)); break;
+          case SELECT_NODE:               return this->print(stream, reinterpret_cast<triton::ast::SelectNode*>(node)); break;
+          case STORE_NODE:                return this->print(stream, reinterpret_cast<triton::ast::StoreNode*>(node)); break;
           default:
             throw triton::exceptions::AstRepresentation("AstPythonRepresentation::print(AbstractNode): Invalid kind node.");
         }
@@ -452,6 +455,27 @@ namespace triton {
         return stream;
       }
 
+
+      /* array representation */
+      std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::ArrayNode* node) {
+        stream << 'M';
+        return stream;
+      }
+
+
+      /* select representation */
+      std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::SelectNode* node) {
+        stream << node->getChildren()[0] << '[' << node->getChildren()[1] << ']';
+        return stream;
+      }
+
+
+      /* store representation */
+      std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::StoreNode* node) {
+        stream << '(' << node->getChildren()[0] << '[' << node->getChildren()[1] << "] = " << node->getChildren()[2] << ")";
+        return stream;
+      }
+
     };
   };
 };

src/libtriton/ast/representations/astSmtRepresentation.cpp

@@ -71,6 +71,9 @@ namespace triton {
           case SX_NODE:                   return this->print(stream, reinterpret_cast<triton::ast::SxNode*>(node)); break;
           case VARIABLE_NODE:             return this->print(stream, reinterpret_cast<triton::ast::VariableNode*>(node)); break;
           case ZX_NODE:                   return this->print(stream, reinterpret_cast<triton::ast::ZxNode*>(node)); break;
+          case ARRAY_NODE:                return this->print(stream, reinterpret_cast<triton::ast::ArrayNode*>(node)); break;
+          case SELECT_NODE:               return this->print(stream, reinterpret_cast<triton::ast::SelectNode*>(node)); break;
+          case STORE_NODE:                return this->print(stream, reinterpret_cast<triton::ast::StoreNode*>(node)); break;
           default:
             throw triton::exceptions::AstRepresentation("AstSmtRepresentation::print(AbstractNode): Invalid kind node.");
         }
@@ -442,6 +445,27 @@ namespace triton {
         return stream;
       }
 
+
+      /* array representation */
+      std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ArrayNode* node) {
+        stream << "(Array (_ BitVec " << node->getChildren()[0] << ") (_ BitVec 8))";
+        return stream;
+      }
+
+
+      /* select representation */
+      std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::SelectNode* node) {
+        stream << "(select " << node->getChildren()[0] << ' ' << node->getChildren()[1] << ")";
+        return stream;
+      }
+
+
+      /* store representation */
+      std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::StoreNode* node) {
+        stream << "(store " << node->getChildren()[0] << ' ' << node->getChildren()[1] << ' ' << node->getChildren()[2] << ")";
+        return stream;
+      }
+
     };
   };
 };

src/libtriton/ast/z3/tritonToZ3Ast.cpp

@@ -293,6 +293,31 @@ namespace triton {
           return to_expr(this->context, Z3_mk_zero_ext(this->context, extv, value));
         }
 
+        case ARRAY_NODE: {
+          z3::expr size        = this->convert(node->getChildren()[0]);
+          triton::uint32 sizev = static_cast<triton::uint32>(this->getUintValue(size));
+          auto isort           = this->context.bv_sort(sizev);
+          auto vsort           = this->context.bv_sort(8);
+          auto asort           = this->context.array_sort(isort, vsort);
+
+          return this->context.constant(("M" + std::to_string(sizev)).c_str(), asort);
+        }
+
+        case SELECT_NODE: {
+          z3::expr a = this->convert(node->getChildren()[0]);
+          z3::expr i = this->convert(node->getChildren()[1]);
+
+          return to_expr(this->context, Z3_mk_select(this->context, a, i));
+        }
+
+        case STORE_NODE: {
+          z3::expr a = this->convert(node->getChildren()[0]);
+          z3::expr i = this->convert(node->getChildren()[1]);
+          z3::expr v = this->convert(node->getChildren()[2]);
+
+          return to_expr(this->context, Z3_mk_store(this->context, a, i, v));
+        }
+
         default:
           throw triton::exceptions::AstTranslations("TritonToZ3Ast::convert(): Invalid kind of node.");
       }

src/libtriton/bindings/python/namespaces/initModeNamespace.cpp

@@ -59,6 +59,7 @@ namespace triton {
         xPyDict_SetItemString(modeDict, "ONLY_ON_TAINTED",        PyLong_FromUint32(triton::modes::ONLY_ON_TAINTED));
         xPyDict_SetItemString(modeDict, "PC_TRACKING_SYMBOLIC",   PyLong_FromUint32(triton::modes::PC_TRACKING_SYMBOLIC));
         xPyDict_SetItemString(modeDict, "TAINT_THROUGH_POINTERS", PyLong_FromUint32(triton::modes::TAINT_THROUGH_POINTERS));
+        xPyDict_SetItemString(modeDict, "SYMBOLIZED_POINTERS",    PyLong_FromUint32(triton::modes::SYMBOLIZED_POINTERS));
       }
 
     }; /* python namespace */

src/libtriton/bindings/python/objects/pyAstContext.cpp

@@ -1466,6 +1466,67 @@ namespace triton {
       }
 
 
+      static PyObject* AstContext_array(PyObject* self, PyObject* addrSize) {
+        if (!PyLong_Check(addrSize) && !PyInt_Check(addrSize))
+          return PyErr_Format(PyExc_TypeError, "array(): expected an integer as first argument");
+
+        try {
+          return PyAstNode(PyAstContext_AsAstContext(self)->array(PyLong_AsUint32(addrSize)));
+        }
+        catch (const triton::exceptions::Exception& e) {
+          return PyErr_Format(PyExc_TypeError, "%s", e.what());
+        }
+      }
+
+
+      static PyObject* AstContext_select(PyObject* self, PyObject* args) {
+        PyObject* op1 = nullptr;
+        PyObject* op2 = nullptr;
+
+        /* Extract arguments */
+        PyArg_ParseTuple(args, "|OO", &op1, &op2);
+
+        if (op1 == nullptr || !PyAstNode_Check(op1))
+          return PyErr_Format(PyExc_TypeError, "select(): expected a AstNode as first argument");
+
+        if (op2 == nullptr || !PyAstNode_Check(op2))
+          return PyErr_Format(PyExc_TypeError, "select(): expected a AstNode as second argument");
+
+        try {
+          return PyAstNode(PyAstContext_AsAstContext(self)->select(PyAstNode_AsAstNode(op1), PyAstNode_AsAstNode(op2)));
+        }
+        catch (const triton::exceptions::Exception& e) {
+          return PyErr_Format(PyExc_TypeError, "%s", e.what());
+        }
+      }
+
+
+      static PyObject* AstContext_store(PyObject* self, PyObject* args) {
+        PyObject* op1 = nullptr;
+        PyObject* op2 = nullptr;
+        PyObject* op3 = nullptr;
+
+        /* Extract arguments */
+        PyArg_ParseTuple(args, "|OOO", &op1, &op2, &op3);
+
+        if (op1 == nullptr || !PyAstNode_Check(op1))
+          return PyErr_Format(PyExc_TypeError, "store(): expected a AstNode as first argument");
+
+        if (op2 == nullptr || !PyAstNode_Check(op2))
+          return PyErr_Format(PyExc_TypeError, "store(): expected a AstNode as second argument");
+
+        if (op3 == nullptr || !PyAstNode_Check(op3))
+          return PyErr_Format(PyExc_TypeError, "store(): expected a AstNode as third argument");
+
+        try {
+          return PyAstNode(PyAstContext_AsAstContext(self)->store(PyAstNode_AsAstNode(op1), PyAstNode_AsAstNode(op2), PyAstNode_AsAstNode(op3)));
+        }
+        catch (const triton::exceptions::Exception& e) {
+          return PyErr_Format(PyExc_TypeError, "%s", e.what());
+        }
+      }
+
+
       //! AstContext methods.
       PyMethodDef AstContext_callbacks[] = {
         {"assert_",       AstContext_assert,          METH_O,           ""},
@@ -1518,6 +1579,9 @@ namespace triton {
         {"sx",            AstContext_sx,              METH_VARARGS,     ""},
         {"variable",      AstContext_variable,        METH_O,           ""},
         {"zx",            AstContext_zx,              METH_VARARGS,     ""},
+        {"array",         AstContext_array,           METH_O,           ""},
+        {"select",        AstContext_select,          METH_VARARGS,     ""},
+        {"store",         AstContext_store,           METH_VARARGS,     ""},
         {nullptr,         nullptr,                    0,                nullptr}
       };