libTriton version 1.0 build 1590
Loading...
Searching...
No Matches
tritonToZ3.cpp
Go to the documentation of this file.
1
2/*
3** Copyright (C) - Triton
4**
5** This program is under the terms of the Apache License 2.0.
6*/
7
8#include <vector>
9
10#include <triton/coreUtils.hpp>
11#include <triton/cpuSize.hpp>
12#include <triton/exceptions.hpp>
15#include <triton/tritonToZ3.hpp>
16
17
18
19namespace triton {
20 namespace ast {
21
23 : context() {
24 this->isEval = eval;
25 }
26
27
29 /* See #828: Release ownership before calling container destructor */
30 this->symbols.clear();
31 this->variables.clear();
32 }
33
34
35 std::string TritonToZ3::getStringValue(const z3::expr& expr) {
36 return Z3_get_numeral_string(this->context, expr);
37 }
38
39
41 std::unordered_map<triton::ast::SharedAbstractNode, z3::expr> results;
42
43 auto nodes = triton::ast::childrenExtraction(node, true /* unroll*/, true /* revert */);
44
45 for (auto&& n : nodes) {
46 results.insert(std::make_pair(n, this->do_convert(n, &results)));
47 }
48
49 return results.at(node);
50 }
51
52
53 z3::expr TritonToZ3::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map<triton::ast::SharedAbstractNode, z3::expr>* results) {
54 if (node == nullptr)
55 throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): node cannot be null.");
56
57 /* Prepare z3's children */
58 std::vector<z3::expr> children;
59 for (auto&& n : node->getChildren()) {
60 children.emplace_back(results->at(n));
61 }
62
63 switch (node->getType()) {
64
65 case ARRAY_NODE: {
66 auto size = triton::ast::getInteger<triton::uint32>(node->getChildren()[0]);
67 auto isort = this->context.bv_sort(size);
68 auto value = this->context.bv_val(0, 8);
69 return to_expr(this->context, Z3_mk_const_array(this->context, isort, value));
70 }
71
72 case BSWAP_NODE: {
73 auto bvsize = node->getBitvectorSize();
74 auto retval = to_expr(this->context, Z3_mk_bvand(this->context, children[0], this->context.bv_val(0xff, bvsize)));
75 for (triton::uint32 index = 8 ; index != bvsize ; index += triton::bitsize::byte) {
76 retval = to_expr(this->context, Z3_mk_bvshl(this->context, retval, this->context.bv_val(8, bvsize)));
77 retval = to_expr(this->context, Z3_mk_bvor(this->context, retval,
78 to_expr(this->context, Z3_mk_bvand(this->context,
79 to_expr(this->context, Z3_mk_bvlshr(this->context, children[0], this->context.bv_val(index, bvsize))),
80 this->context.bv_val(0xff, bvsize)
81 ))
82 ));
83 }
84 return to_expr(this->context, retval);
85 }
86
87 case BVADD_NODE:
88 return to_expr(this->context, Z3_mk_bvadd(this->context, children[0], children[1]));
89
90 case BVAND_NODE:
91 return to_expr(this->context, Z3_mk_bvand(this->context, children[0], children[1]));
92
93 case BVASHR_NODE:
94 return to_expr(this->context, Z3_mk_bvashr(this->context, children[0], children[1]));
95
96 case BVLSHR_NODE:
97 return to_expr(this->context, Z3_mk_bvlshr(this->context, children[0], children[1]));
98
99 case BVMUL_NODE:
100 return to_expr(this->context, Z3_mk_bvmul(this->context, children[0], children[1]));
101
102 case BVNAND_NODE:
103 return to_expr(this->context, Z3_mk_bvnand(this->context, children[0], children[1]));
104
105 case BVNEG_NODE:
106 return to_expr(this->context, Z3_mk_bvneg(this->context, children[0]));
107
108 case BVNOR_NODE:
109 return to_expr(this->context, Z3_mk_bvnor(this->context, children[0], children[1]));
110
111 case BVNOT_NODE:
112 return to_expr(this->context, Z3_mk_bvnot(this->context, children[0]));
113
114 case BVOR_NODE:
115 return to_expr(this->context, Z3_mk_bvor(this->context, children[0], children[1]));
116
117 case BVROL_NODE: {
118 triton::uint32 rot = triton::ast::getInteger<triton::uint32>(node->getChildren()[1]);
119 return to_expr(this->context, Z3_mk_rotate_left(this->context, rot, children[0]));
120 }
121
122 case BVROR_NODE: {
123 triton::uint32 rot = triton::ast::getInteger<triton::uint32>(node->getChildren()[1]);
124 return to_expr(this->context, Z3_mk_rotate_right(this->context, rot, children[0]));
125 }
126
127 case BVSDIV_NODE:
128 return to_expr(this->context, Z3_mk_bvsdiv(this->context, children[0], children[1]));
129
130 case BVSGE_NODE:
131 return to_expr(this->context, Z3_mk_bvsge(this->context, children[0], children[1]));
132
133 case BVSGT_NODE:
134 return to_expr(this->context, Z3_mk_bvsgt(this->context, children[0], children[1]));
135
136 case BVSHL_NODE:
137 return to_expr(this->context, Z3_mk_bvshl(this->context, children[0], children[1]));
138
139 case BVSLE_NODE:
140 return to_expr(this->context, Z3_mk_bvsle(this->context, children[0], children[1]));
141
142 case BVSLT_NODE:
143 return to_expr(this->context, Z3_mk_bvslt(this->context, children[0], children[1]));
144
145 case BVSMOD_NODE:
146 return to_expr(this->context, Z3_mk_bvsmod(this->context, children[0], children[1]));
147
148 case BVSREM_NODE:
149 return to_expr(this->context, Z3_mk_bvsrem(this->context, children[0], children[1]));
150
151 case BVSUB_NODE:
152 return to_expr(this->context, Z3_mk_bvsub(this->context, children[0], children[1]));
153
154 case BVUDIV_NODE:
155 return to_expr(this->context, Z3_mk_bvudiv(this->context, children[0], children[1]));
156
157 case BVUGE_NODE:
158 return to_expr(this->context, Z3_mk_bvuge(this->context, children[0], children[1]));
159
160 case BVUGT_NODE:
161 return to_expr(this->context, Z3_mk_bvugt(this->context, children[0], children[1]));
162
163 case BVULE_NODE:
164 return to_expr(this->context, Z3_mk_bvule(this->context, children[0], children[1]));
165
166 case BVULT_NODE:
167 return to_expr(this->context, Z3_mk_bvult(this->context, children[0], children[1]));
168
169 case BVUREM_NODE:
170 return to_expr(this->context, Z3_mk_bvurem(this->context, children[0], children[1]));
171
172 case BVXNOR_NODE:
173 return to_expr(this->context, Z3_mk_bvxnor(this->context, children[0], children[1]));
174
175 case BVXOR_NODE:
176 return to_expr(this->context, Z3_mk_bvxor(this->context, children[0], children[1]));
177
178 case BV_NODE:
179 return this->context.bv_val(this->getStringValue(children[0]).c_str(), children[1].get_numeral_uint());
180
181 case CONCAT_NODE: {
182 z3::expr currentValue = children[0];
183 z3::expr nextValue(this->context);
184
185 // Child[0] is the LSB
186 for (triton::uint32 idx = 1; idx < children.size(); idx++) {
187 nextValue = children[idx];
188 currentValue = to_expr(this->context, Z3_mk_concat(this->context, currentValue, nextValue));
189 }
190
191 return currentValue;
192 }
193
194 case DISTINCT_NODE: {
195 z3::expr op1 = children[0];
196 z3::expr op2 = children[1];
197 Z3_ast ops[] = {op1, op2};
198
199 return to_expr(this->context, Z3_mk_distinct(this->context, 2, ops));
200 }
201
202 case EQUAL_NODE:
203 return to_expr(this->context, Z3_mk_eq(this->context, children[0], children[1]));
204
205 case EXTRACT_NODE:
206 return to_expr(this->context, Z3_mk_extract(this->context, children[0].get_numeral_uint(), children[1].get_numeral_uint(), children[2]));
207
208 case FORALL_NODE: {
209 triton::uint32 size = static_cast<triton::uint32>(node->getChildren().size() - 1);
210 Z3_app* vars = new Z3_app[size];
211
212 for (triton::uint32 i = 0; i != size; i++) {
213 vars[i] = children[i];
214 }
215
216 z3::expr e = to_expr(this->context, Z3_mk_forall_const(this->context, 0, size, vars, 0, 0, children[size]));
217 delete[] vars;
218
219 return e;
220 }
221
222 case IFF_NODE: {
223 z3::expr op1 = children[0];
224 z3::expr op2 = children[1];
225
226 return to_expr(this->context, Z3_mk_iff(this->context, op1, op2));
227 }
228
229 case INTEGER_NODE: {
230 std::string value(triton::ast::getInteger<std::string>(node));
231 return this->context.int_val(value.c_str());
232 }
233
234 case ITE_NODE: {
235 z3::expr op1 = children[0]; // condition
236 z3::expr op2 = children[1]; // if true
237 z3::expr op3 = children[2]; // if false
238
239 return to_expr(this->context, Z3_mk_ite(this->context, op1, op2, op3));
240 }
241
242 case LAND_NODE: {
243 z3::expr currentValue = children[0];
244 z3::expr nextValue(this->context);
245
246 for (triton::uint32 idx = 1; idx < children.size(); idx++) {
247 nextValue = children[idx];
248 Z3_ast ops[] = {currentValue, nextValue};
249 currentValue = to_expr(this->context, Z3_mk_and(this->context, 2, ops));
250 }
251
252 return currentValue;
253 }
254
255 case LET_NODE: {
256 std::string symbol = reinterpret_cast<triton::ast::StringNode*>(node->getChildren()[0].get())->getString();
257 this->symbols[symbol] = node->getChildren()[1];
258
259 return children[2];
260 }
261
262 case LNOT_NODE: {
263 z3::expr value = children[0];
264 return to_expr(this->context, Z3_mk_not(this->context, value));
265 }
266
267 case LOR_NODE: {
268 z3::expr currentValue = children[0];
269 z3::expr nextValue(this->context);
270
271 for (triton::uint32 idx = 1; idx < children.size(); idx++) {
272 nextValue = children[idx];
273 Z3_ast ops[] = {currentValue, nextValue};
274 currentValue = to_expr(this->context, Z3_mk_or(this->context, 2, ops));
275 }
276
277 return currentValue;
278 }
279
280 case LXOR_NODE: {
281 z3::expr currentValue = children[0];
282 z3::expr nextValue(this->context);
283
284 for (triton::uint32 idx = 1; idx < children.size(); idx++) {
285 nextValue = children[idx];
286 currentValue = to_expr(this->context, Z3_mk_xor(this->context, currentValue, nextValue));
287 }
288
289 return currentValue;
290 }
291
292 case REFERENCE_NODE:
293 return results->at(reinterpret_cast<triton::ast::ReferenceNode*>(node.get())->getSymbolicExpression()->getAst());
294
295 case STRING_NODE: {
296 std::string value = reinterpret_cast<triton::ast::StringNode*>(node.get())->getString();
297
298 if (this->symbols.find(value) == this->symbols.end())
299 throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): [STRING_NODE] Symbols not found.");
300
301 return results->at(this->symbols[value]);
302 }
303
304 case SELECT_NODE:
305 return to_expr(this->context, Z3_mk_select(this->context, children[0], children[1]));
306
307 case STORE_NODE:
308 return to_expr(this->context, Z3_mk_store(this->context, children[0], children[1], children[2]));
309
310 case SX_NODE:
311 return to_expr(this->context, Z3_mk_sign_ext(this->context, children[0].get_numeral_uint(), children[1]));
312
313 case VARIABLE_NODE: {
314 const triton::engines::symbolic::SharedSymbolicVariable& symVar = reinterpret_cast<triton::ast::VariableNode*>(node.get())->getSymbolicVariable();
315
316 /* Record variable */
317 this->variables[symVar->getName()] = symVar;
318
319 /* If the conversion is used to evaluate a node, we concretize symbolic variables */
320 if (this->isEval) {
321 triton::uint512 value = reinterpret_cast<triton::ast::VariableNode*>(node.get())->evaluate();
322 return this->context.bv_val(triton::utils::toString(value).c_str(), symVar->getSize());
323 }
324
325 /* Otherwise, we keep the symbolic variables for a real conversion */
326 return this->context.bv_const(symVar->getName().c_str(), symVar->getSize());
327 }
328
329 case ZX_NODE:
330 return to_expr(this->context, Z3_mk_zero_ext(this->context, children[0].get_numeral_uint(), children[1]));
331
332 default:
333 throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): Invalid kind of node.");
334 }
335 }
336
337 }; /* ast namespace */
338}; /* triton namespace */
TRITON_EXPORT std::vector< SharedAbstractNode > & getChildren(void)
Returns the children of the node.
Definition ast.cpp:182
Reference node.
Definition ast.hpp:789
String node.
Definition ast.hpp:852
std::unordered_map< std::string, triton::engines::symbolic::SharedSymbolicVariable > variables
The set of symbolic variables contained in the expression.
TRITON_EXPORT ~TritonToZ3()
Destructor.
TRITON_EXPORT TritonToZ3(bool eval=true)
Constructor.
std::unordered_map< std::string, triton::ast::SharedAbstractNode > symbols
The map of symbols. E.g: (let (symbols expr1) expr2)
z3::context context
The z3's context.
TRITON_EXPORT z3::expr convert(const triton::ast::SharedAbstractNode &node)
Converts to Z3's AST.
Variable node.
Definition ast.hpp:878
The exception class used by all AST lifting (e.g z3 <-> triton).
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
std::vector< SharedAbstractNode > childrenExtraction(const SharedAbstractNode &node, bool unroll, bool revert)
Returns node and all its children of an AST sorted topologically. If unroll is true,...
Definition ast.cpp:3700
constexpr triton::uint32 byte
byte size in bit
Definition cpuSize.hpp:60
std::shared_ptr< triton::engines::symbolic::SymbolicVariable > SharedSymbolicVariable
Shared Symbolic variable.
Definition ast.hpp:43
math::wide_integer::uint512_t uint512
unsigned 512-bits
std::uint32_t uint32
unisgned 32-bits
std::string toString(const T &obj)
Converts an object to a string.
Definition coreUtils.hpp:38
The Triton namespace.