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 <triton/pythonObjects.hpp> 9 #include <triton/pythonUtils.hpp> 10 #include <triton/pythonXFunctions.hpp> 11 #include <triton/exceptions.hpp> 12 #include <triton/solverModel.hpp> 13 14 15 16 /*! \page py_SolverModel_page SolverModel 17 \brief [**python api**] All information about the SolverModel Python object. 18 19 \tableofcontents 20 21 \section py_SolverModel_description Description 22 <hr> 23 24 This object is used to represent a model for an SMT solver. 25 26 ~~~~~~~~~~~~~{.py} 27 >>> from __future__ import print_function 28 >>> from triton import TritonContext, ARCH, Instruction, REG 29 30 >>> ctxt = TritonContext() 31 >>> ctxt.setArchitecture(ARCH.X86_64) 32 >>> inst = Instruction() 33 >>> inst.setOpcode(b"\x48\x35\x44\x33\x22\x11") # xor rax, 0x11223344 34 35 >>> symvar = ctxt.symbolizeRegister(ctxt.registers.rax) 36 >>> print(symvar) 37 SymVar_0:64 38 39 >>> ctxt.processing(inst) 40 True 41 >>> print(inst) 42 0x0: xor rax, 0x11223344 43 44 >>> ast = ctxt.getAstContext() 45 >>> raxAst = ast.unroll(ctxt.getSymbolicRegister(ctxt.registers.rax).getAst()) 46 >>> print(raxAst) 47 (bvxor SymVar_0 (_ bv287454020 64)) 48 49 >>> astCtxt = ctxt.getAstContext() 50 >>> constraint = astCtxt.equal(raxAst, astCtxt.bv(0, raxAst.getBitvectorSize())) 51 >>> print(constraint) 52 (= (bvxor SymVar_0 (_ bv287454020 64)) (_ bv0 64)) 53 54 >>> model = ctxt.getModel(constraint) 55 >>> print(model) #doctest: +ELLIPSIS 56 {0: SymVar_0:64 = 0x11223344} 57 58 >>> symvarModel = model[symvar.getId()] # Model from the symvar's id 59 >>> print(symvarModel) 60 SymVar_0:64 = 0x11223344 61 >>> hex(symvarModel.getValue()) 62 '0x11223344' 63 64 ~~~~~~~~~~~~~ 65 66 \section SolverModel_py_api Python API - Methods of the SolverModel class 67 <hr> 68 69 - <b>integer getId(void)</b><br> 70 Returns the id of the model. This id is the same as the variable id. 71 72 - <b>integer getValue(void)</b><br> 73 Returns the value of the model. 74 75 - <b>\ref py_SymbolicVariable_page getVariable(void)</b><br> 76 Returns the symbolic variable. 77 78 */ 79 80 81 82 namespace triton { 83 namespace bindings { 84 namespace python { 85 86 //! SolverModel destructor. SolverModel_dealloc(PyObject * self)87 void SolverModel_dealloc(PyObject* self) { 88 std::cout << std::flush; 89 delete PySolverModel_AsSolverModel(self); 90 Py_TYPE(self)->tp_free((PyObject*)self); 91 } 92 93 SolverModel_getId(PyObject * self,PyObject * noarg)94 static PyObject* SolverModel_getId(PyObject* self, PyObject* noarg) { 95 try { 96 return PyLong_FromUsize(PySolverModel_AsSolverModel(self)->getId()); 97 } 98 catch (const triton::exceptions::Exception& e) { 99 return PyErr_Format(PyExc_TypeError, "%s", e.what()); 100 } 101 } 102 103 SolverModel_getValue(PyObject * self,PyObject * noarg)104 static PyObject* SolverModel_getValue(PyObject* self, PyObject* noarg) { 105 try { 106 return PyLong_FromUint512(PySolverModel_AsSolverModel(self)->getValue()); 107 } 108 catch (const triton::exceptions::Exception& e) { 109 return PyErr_Format(PyExc_TypeError, "%s", e.what()); 110 } 111 } 112 113 SolverModel_getVariable(PyObject * self,PyObject * noarg)114 static PyObject* SolverModel_getVariable(PyObject* self, PyObject* noarg) { 115 try { 116 return PySymbolicVariable(PySolverModel_AsSolverModel(self)->getVariable()); 117 } 118 catch (const triton::exceptions::Exception& e) { 119 return PyErr_Format(PyExc_TypeError, "%s", e.what()); 120 } 121 } 122 123 SolverModel_print(PyObject * self,void * io,int s)124 static int SolverModel_print(PyObject* self, void* io, int s) { 125 std::cout << PySolverModel_AsSolverModel(self); 126 return 0; 127 } 128 129 SolverModel_str(PyObject * self)130 static PyObject* SolverModel_str(PyObject* self) { 131 try { 132 std::stringstream str; 133 str << PySolverModel_AsSolverModel(self); 134 return PyStr_FromFormat("%s", str.str().c_str()); 135 } 136 catch (const triton::exceptions::Exception& e) { 137 return PyErr_Format(PyExc_TypeError, "%s", e.what()); 138 } 139 } 140 141 142 //! SolverModel methods. 143 PyMethodDef SolverModel_callbacks[] = { 144 {"getId", SolverModel_getId, METH_NOARGS, ""}, 145 {"getValue", SolverModel_getValue, METH_NOARGS, ""}, 146 {"getVariable", SolverModel_getVariable, METH_NOARGS, ""}, 147 {nullptr, nullptr, 0, nullptr} 148 }; 149 150 151 PyTypeObject SolverModel_Type = { 152 PyVarObject_HEAD_INIT(&PyType_Type, 0) 153 "SolverModel", /* tp_name */ 154 sizeof(SolverModel_Object), /* tp_basicsize */ 155 0, /* tp_itemsize */ 156 (destructor)SolverModel_dealloc, /* tp_dealloc */ 157 (printfunc)SolverModel_print, /* tp_print */ 158 0, /* tp_getattr */ 159 0, /* tp_setattr */ 160 0, /* tp_compare */ 161 (reprfunc)SolverModel_str, /* tp_repr */ 162 0, /* tp_as_number */ 163 0, /* tp_as_sequence */ 164 0, /* tp_as_mapping */ 165 0, /* tp_hash */ 166 0, /* tp_call */ 167 (reprfunc)SolverModel_str, /* tp_str */ 168 0, /* tp_getattro */ 169 0, /* tp_setattro */ 170 0, /* tp_as_buffer */ 171 Py_TPFLAGS_DEFAULT, /* tp_flags */ 172 "SolverModel objects", /* tp_doc */ 173 0, /* tp_traverse */ 174 0, /* tp_clear */ 175 0, /* tp_richcompare */ 176 0, /* tp_weaklistoffset */ 177 0, /* tp_iter */ 178 0, /* tp_iternext */ 179 SolverModel_callbacks, /* tp_methods */ 180 0, /* tp_members */ 181 0, /* tp_getset */ 182 0, /* tp_base */ 183 0, /* tp_dict */ 184 0, /* tp_descr_get */ 185 0, /* tp_descr_set */ 186 0, /* tp_dictoffset */ 187 0, /* tp_init */ 188 0, /* tp_alloc */ 189 0, /* tp_new */ 190 0, /* tp_free */ 191 0, /* tp_is_gc */ 192 0, /* tp_bases */ 193 0, /* tp_mro */ 194 0, /* tp_cache */ 195 0, /* tp_subclasses */ 196 0, /* tp_weaklist */ 197 0, /* tp_del */ 198 #if IS_PY3 199 0, /* tp_version_tag */ 200 0, /* tp_finalize */ 201 #else 202 0 /* tp_version_tag */ 203 #endif 204 }; 205 206 PySolverModel(const triton::engines::solver::SolverModel & model)207 PyObject* PySolverModel(const triton::engines::solver::SolverModel& model) { 208 SolverModel_Object* object; 209 210 PyType_Ready(&SolverModel_Type); 211 object = PyObject_NEW(SolverModel_Object, &SolverModel_Type); 212 if (object != NULL) 213 object->model = new triton::engines::solver::SolverModel(model); 214 215 return (PyObject*)object; 216 } 217 218 }; /* python namespace */ 219 }; /* bindings namespace */ 220 }; /* triton namespace */ 221