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.
87 1
      void SolverModel_dealloc(PyObject* self) {
88 1
        std::cout << std::flush;
89 1
        delete PySolverModel_AsSolverModel(self);
90 1
        Py_TYPE(self)->tp_free((PyObject*)self);
91
      }
92

93

94 1
      static PyObject* SolverModel_getId(PyObject* self, PyObject* noarg) {
95
        try {
96 1
          return PyLong_FromUsize(PySolverModel_AsSolverModel(self)->getId());
97
        }
98 0
        catch (const triton::exceptions::Exception& e) {
99 0
          return PyErr_Format(PyExc_TypeError, "%s", e.what());
100
        }
101
      }
102

103

104 1
      static PyObject* SolverModel_getValue(PyObject* self, PyObject* noarg) {
105
        try {
106 1
          return PyLong_FromUint512(PySolverModel_AsSolverModel(self)->getValue());
107
        }
108 0
        catch (const triton::exceptions::Exception& e) {
109 0
          return PyErr_Format(PyExc_TypeError, "%s", e.what());
110
        }
111
      }
112

113

114 1
      static PyObject* SolverModel_getVariable(PyObject* self, PyObject* noarg) {
115
        try {
116 1
          return PySymbolicVariable(PySolverModel_AsSolverModel(self)->getVariable());
117
        }
118 0
        catch (const triton::exceptions::Exception& e) {
119 0
          return PyErr_Format(PyExc_TypeError, "%s", e.what());
120
        }
121
      }
122

123

124
      #if !defined(IS_PY3_8) || !IS_PY3_8
125 0
      static int SolverModel_print(PyObject* self, void* io, int s) {
126 0
        std::cout << PySolverModel_AsSolverModel(self);
127 0
        return 0;
128
      }
129
      #endif
130

131

132 1
      static PyObject* SolverModel_str(PyObject* self) {
133
        try {
134 1
          std::stringstream str;
135 1
          str << PySolverModel_AsSolverModel(self);
136 1
          return PyStr_FromFormat("%s", str.str().c_str());
137
        }
138 0
        catch (const triton::exceptions::Exception& e) {
139 0
          return PyErr_Format(PyExc_TypeError, "%s", e.what());
140
        }
141
      }
142

143

144
      //! SolverModel methods.
145
      PyMethodDef SolverModel_callbacks[] = {
146
        {"getId",       SolverModel_getId,        METH_NOARGS,    ""},
147
        {"getValue",    SolverModel_getValue,     METH_NOARGS,    ""},
148
        {"getVariable", SolverModel_getVariable,  METH_NOARGS,    ""},
149
        {nullptr,       nullptr,                  0,              nullptr}
150
      };
151

152

153
      PyTypeObject SolverModel_Type = {
154
        PyVarObject_HEAD_INIT(&PyType_Type, 0)
155
        "SolverModel",                              /* tp_name */
156
        sizeof(SolverModel_Object),                 /* tp_basicsize */
157
        0,                                          /* tp_itemsize */
158
        (destructor)SolverModel_dealloc,            /* tp_dealloc */
159
        #if IS_PY3_8
160
        0,                                          /* tp_vectorcall_offset */
161
        #else
162
        (printfunc)SolverModel_print,               /* tp_print */
163
        #endif
164
        0,                                          /* tp_getattr */
165
        0,                                          /* tp_setattr */
166
        0,                                          /* tp_compare */
167
        (reprfunc)SolverModel_str,                  /* tp_repr */
168
        0,                                          /* tp_as_number */
169
        0,                                          /* tp_as_sequence */
170
        0,                                          /* tp_as_mapping */
171
        0,                                          /* tp_hash */
172
        0,                                          /* tp_call */
173
        (reprfunc)SolverModel_str,                  /* tp_str */
174
        0,                                          /* tp_getattro */
175
        0,                                          /* tp_setattro */
176
        0,                                          /* tp_as_buffer */
177
        Py_TPFLAGS_DEFAULT,                         /* tp_flags */
178
        "SolverModel objects",                      /* tp_doc */
179
        0,                                          /* tp_traverse */
180
        0,                                          /* tp_clear */
181
        0,                                          /* tp_richcompare */
182
        0,                                          /* tp_weaklistoffset */
183
        0,                                          /* tp_iter */
184
        0,                                          /* tp_iternext */
185
        SolverModel_callbacks,                      /* tp_methods */
186
        0,                                          /* tp_members */
187
        0,                                          /* tp_getset */
188
        0,                                          /* tp_base */
189
        0,                                          /* tp_dict */
190
        0,                                          /* tp_descr_get */
191
        0,                                          /* tp_descr_set */
192
        0,                                          /* tp_dictoffset */
193
        0,                                          /* tp_init */
194
        0,                                          /* tp_alloc */
195
        0,                                          /* tp_new */
196
        0,                                          /* tp_free */
197
        0,                                          /* tp_is_gc */
198
        0,                                          /* tp_bases */
199
        0,                                          /* tp_mro */
200
        0,                                          /* tp_cache */
201
        0,                                          /* tp_subclasses */
202
        0,                                          /* tp_weaklist */
203
        0,                                          /* tp_del */
204
        #if IS_PY3
205
          0,                                        /* tp_version_tag */
206
          0,                                        /* tp_finalize */
207
          #if IS_PY3_8
208
            0,                                      /* tp_vectorcall */
209
            #if !IS_PY3_9
210
              0,                                    /* bpo-37250: kept for backwards compatibility in CPython 3.8 only */
211
            #endif
212
          #endif
213
        #else
214
          0                                         /* tp_version_tag */
215
        #endif
216
      };
217

218

219 1
      PyObject* PySolverModel(const triton::engines::solver::SolverModel& model) {
220
        SolverModel_Object* object;
221

222 1
        PyType_Ready(&SolverModel_Type);
223 1
        object = PyObject_NEW(SolverModel_Object, &SolverModel_Type);
224 1
        if (object != NULL)
225 1
          object->model = new triton::engines::solver::SolverModel(model);
226

227 1
        return (PyObject*)object;
228
      }
229

230
    }; /* python namespace */
231
  }; /* bindings namespace */
232 1
}; /* triton namespace */

Read our documentation on viewing source code .

Loading