libTriton version 1.0 build 1590
Loading...
Searching...
No Matches
z3ToTriton.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 <list>
9
10#include <triton/astContext.hpp>
11#include <triton/exceptions.hpp>
12#include <triton/z3ToTriton.hpp>
13
14
15
16namespace triton {
17 namespace ast {
18
19 Z3ToTriton::Z3ToTriton(const SharedAstContext& astCtxt)
20 : astCtxt(astCtxt) {
21 }
22
23
24 SharedAbstractNode Z3ToTriton::convert(const z3::expr& expr) {
25 SharedAbstractNode node = nullptr;
26
27 /* Currently, only support application node (TODO) */
28 if (expr.is_quantifier())
29 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Quantifier not supported yet.");
30
31 if (!expr.is_app())
32 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): At this moment only application are supported.");
33
34 /* Get the function declaration */
35 z3::func_decl function = expr.decl();
36
37 /* All z3's AST nodes supported */
38 switch (function.decl_kind()) {
39
40 /* Const array */
41 case Z3_OP_CONST_ARRAY: {
42 node = this->astCtxt->array(function.range().array_domain().bv_size());
43 break;
44 }
45
46 case Z3_OP_EQ: {
47 if (expr.num_args() != 2)
48 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_EQ must contain two arguments.");
49 node = this->astCtxt->equal(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
50 break;
51 }
52
53 case Z3_OP_DISTINCT: {
54 if (expr.num_args() < 2)
55 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_DISTINCT must contain at least two arguments.");
56 node = this->astCtxt->distinct(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
57 for (triton::uint32 i = 2; i < expr.num_args(); i++)
58 node = this->astCtxt->distinct(node, this->convert(expr.arg(i)));
59 break;
60 }
61
62 case Z3_OP_IFF: {
63 if (expr.num_args() != 2)
64 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_IFF must contain two arguments.");
65 node = this->astCtxt->iff(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
66 break;
67 }
68
69 case Z3_OP_ITE: {
70 if (expr.num_args() != 3)
71 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ITE must contain three arguments.");
72 node = this->astCtxt->ite(this->convert(expr.arg(0)), this->convert(expr.arg(1)), this->convert(expr.arg(2)));
73 break;
74 }
75
76 case Z3_OP_AND: {
77 if (expr.num_args() < 2)
78 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_AND must contain at least two arguments.");
79
80 std::vector<SharedAbstractNode> args;
81 for (triton::uint32 i = 0; i < expr.num_args(); i++) {
82 args.push_back(this->convert(expr.arg(i)));
83 }
84
85 node = this->astCtxt->land(args);
86 break;
87 }
88
89 case Z3_OP_OR: {
90 if (expr.num_args() < 2)
91 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_OR must contain at least two arguments.");
92
93 std::vector<SharedAbstractNode> args;
94 for (triton::uint32 i = 0; i < expr.num_args(); i++) {
95 args.push_back(this->convert(expr.arg(i)));
96 }
97
98 node = this->astCtxt->lor(args);
99 break;
100 }
101
102 case Z3_OP_XOR: {
103 if (expr.num_args() != 2)
104 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_XOR must contain two arguments.");
105 node = this->astCtxt->lxor(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
106 break;
107 }
108
109 case Z3_OP_NOT: {
110 if (expr.num_args() != 1)
111 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_NOT must contain one argument.");
112 node = this->astCtxt->lnot(this->convert(expr.arg(0)));
113 break;
114 }
115
116 case Z3_OP_BNUM: {
117 std::string stringValue = Z3_get_numeral_string(expr.ctx(), expr);
118 triton::uint512 intValue{stringValue.c_str()};
119 node = this->astCtxt->bv(intValue, expr.get_sort().bv_size());
120 break;
121 }
122
123 case Z3_OP_BNEG: {
124 if (expr.num_args() != 1)
125 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNEG must contain one argument.");
126 node = this->astCtxt->bvneg(this->convert(expr.arg(0)));
127 break;
128 }
129
130 case Z3_OP_BADD: {
131 if (expr.num_args() < 2)
132 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BADD must contain at least two arguments.");
133 node = this->astCtxt->bvadd(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
134 for (triton::uint32 i = 2; i < expr.num_args(); i++)
135 node = this->astCtxt->bvadd(node, this->convert(expr.arg(i)));
136 break;
137 }
138
139 case Z3_OP_BSUB: {
140 if (expr.num_args() < 2)
141 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSUB must contain at least two arguments.");
142 node = this->astCtxt->bvsub(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
143 for (triton::uint32 i = 2; i < expr.num_args(); i++)
144 node = this->astCtxt->bvsub(node, this->convert(expr.arg(i)));
145 break;
146 }
147
148 case Z3_OP_BMUL: {
149 if (expr.num_args() < 2)
150 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BMUL must contain at least two arguments.");
151 node = this->astCtxt->bvmul(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
152 for (triton::uint32 i = 2; i < expr.num_args(); i++)
153 node = this->astCtxt->bvmul(node, this->convert(expr.arg(i)));
154 break;
155 }
156
157 case Z3_OP_BSDIV_I:
158 case Z3_OP_BSDIV: {
159 if (expr.num_args() < 2)
160 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSDIV must contain at least two arguments.");
161 node = this->astCtxt->bvsdiv(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
162 for (triton::uint32 i = 2; i < expr.num_args(); i++)
163 node = this->astCtxt->bvsdiv(node, this->convert(expr.arg(i)));
164 break;
165 }
166
167 case Z3_OP_BUDIV_I:
168 case Z3_OP_BUDIV: {
169 if (expr.num_args() < 2)
170 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BUDIV must contain at least two arguments.");
171 node = this->astCtxt->bvudiv(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
172 for (triton::uint32 i = 2; i < expr.num_args(); i++)
173 node = this->astCtxt->bvudiv(node, this->convert(expr.arg(i)));
174 break;
175 }
176
177 case Z3_OP_BSREM_I:
178 case Z3_OP_BSREM: {
179 if (expr.num_args() < 2)
180 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSREM must contain at least two arguments.");
181 node = this->astCtxt->bvsrem(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
182 for (triton::uint32 i = 2; i < expr.num_args(); i++)
183 node = this->astCtxt->bvsrem(node, this->convert(expr.arg(i)));
184 break;
185 }
186
187 case Z3_OP_BUREM_I:
188 case Z3_OP_BUREM: {
189 if (expr.num_args() < 2)
190 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BUREM must contain at least two arguments.");
191 node = this->astCtxt->bvurem(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
192 for (triton::uint32 i = 2; i < expr.num_args(); i++)
193 node = this->astCtxt->bvurem(node, this->convert(expr.arg(i)));
194 break;
195 }
196
197 case Z3_OP_BSMOD_I:
198 case Z3_OP_BSMOD: {
199 if (expr.num_args() < 2)
200 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSMOD must contain at least two arguments.");
201 node = this->astCtxt->bvsmod(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
202 for (triton::uint32 i = 2; i < expr.num_args(); i++)
203 node = this->astCtxt->bvsmod(node, this->convert(expr.arg(i)));
204 break;
205 }
206
207 case Z3_OP_ULEQ: {
208 if (expr.num_args() < 2)
209 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ULEQ must contain at least two arguments.");
210 node = this->astCtxt->bvule(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
211 for (triton::uint32 i = 2; i < expr.num_args(); i++)
212 node = this->astCtxt->bvule(node, this->convert(expr.arg(i)));
213 break;
214 }
215
216 case Z3_OP_SLEQ: {
217 if (expr.num_args() < 2)
218 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SLEQ must contain at least two arguments.");
219 node = this->astCtxt->bvsle(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
220 for (triton::uint32 i = 2; i < expr.num_args(); i++)
221 node = this->astCtxt->bvsle(node, this->convert(expr.arg(i)));
222 break;
223 }
224
225 case Z3_OP_UGEQ: {
226 if (expr.num_args() < 2)
227 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_UGEQ must contain at least two arguments.");
228 node = this->astCtxt->bvuge(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
229 for (triton::uint32 i = 2; i < expr.num_args(); i++)
230 node = this->astCtxt->bvuge(node, this->convert(expr.arg(i)));
231 break;
232 }
233
234 case Z3_OP_SGEQ: {
235 if (expr.num_args() < 2)
236 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SGEQ must contain at least two arguments.");
237 node = this->astCtxt->bvsge(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
238 for (triton::uint32 i = 2; i < expr.num_args(); i++)
239 node = this->astCtxt->bvsge(node, this->convert(expr.arg(i)));
240 break;
241 }
242
243 case Z3_OP_ULT: {
244 if (expr.num_args() < 2)
245 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ULT must contain at least two arguments.");
246 node = this->astCtxt->bvult(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
247 for (triton::uint32 i = 2; i < expr.num_args(); i++)
248 node = this->astCtxt->bvult(node, this->convert(expr.arg(i)));
249 break;
250 }
251
252 case Z3_OP_SLT: {
253 if (expr.num_args() < 2)
254 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SLT must contain at least two arguments.");
255 node = this->astCtxt->bvslt(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
256 for (triton::uint32 i = 2; i < expr.num_args(); i++)
257 node = this->astCtxt->bvslt(node, this->convert(expr.arg(i)));
258 break;
259 }
260
261 case Z3_OP_UGT: {
262 if (expr.num_args() < 2)
263 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_UGT must contain at least two arguments.");
264 node = this->astCtxt->bvugt(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
265 for (triton::uint32 i = 2; i < expr.num_args(); i++)
266 node = this->astCtxt->bvugt(node, this->convert(expr.arg(i)));
267 break;
268 }
269
270 case Z3_OP_SGT: {
271 if (expr.num_args() < 2)
272 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SGT must contain at least two arguments.");
273 node = this->astCtxt->bvsgt(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
274 for (triton::uint32 i = 2; i < expr.num_args(); i++)
275 node = this->astCtxt->bvsgt(node, this->convert(expr.arg(i)));
276 break;
277 }
278
279 case Z3_OP_BAND: {
280 if (expr.num_args() < 2)
281 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BAND must contain at least two arguments.");
282 node = this->astCtxt->bvand(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
283 for (triton::uint32 i = 2; i < expr.num_args(); i++)
284 node = this->astCtxt->bvand(node, this->convert(expr.arg(i)));
285 break;
286 }
287
288 case Z3_OP_BOR: {
289 if (expr.num_args() < 2)
290 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BOR must contain at least two arguments.");
291 node = this->astCtxt->bvor(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
292 for (triton::uint32 i = 2; i < expr.num_args(); i++)
293 node = this->astCtxt->bvor(node, this->convert(expr.arg(i)));
294 break;
295 }
296
297 case Z3_OP_BNOT: {
298 if (expr.num_args() != 1)
299 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNOT must contain one argument.");
300 node = this->astCtxt->bvnot(this->convert(expr.arg(0)));
301 break;
302 }
303
304 case Z3_OP_BXOR: {
305 if (expr.num_args() < 2)
306 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BXOR must contain at least two arguments.");
307 node = this->astCtxt->bvxor(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
308 for (triton::uint32 i = 2; i < expr.num_args(); i++)
309 node = this->astCtxt->bvxor(node, this->convert(expr.arg(i)));
310 break;
311 }
312
313 case Z3_OP_BNAND: {
314 if (expr.num_args() < 2)
315 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNAND must contain at least two arguments.");
316 node = this->astCtxt->bvnand(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
317 for (triton::uint32 i = 2; i < expr.num_args(); i++)
318 node = this->astCtxt->bvnand(node, this->convert(expr.arg(i)));
319 break;
320 }
321
322 case Z3_OP_BNOR: {
323 if (expr.num_args() < 2)
324 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNOR must contain at least two arguments.");
325 node = this->astCtxt->bvnor(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
326 for (triton::uint32 i = 2; i < expr.num_args(); i++)
327 node = this->astCtxt->bvnor(node, this->convert(expr.arg(i)));
328 break;
329 }
330
331 case Z3_OP_BXNOR: {
332 if (expr.num_args() < 2)
333 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BXNOR must contain at least two arguments.");
334 node = this->astCtxt->bvxnor(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
335 for (triton::uint32 i = 2; i < expr.num_args(); i++)
336 node = this->astCtxt->bvxnor(node, this->convert(expr.arg(i)));
337 break;
338 }
339
340 case Z3_OP_CONCAT: {
341 if (expr.num_args() < 2)
342 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_CONCAT must contain at least two arguments.");
343
344 std::vector<SharedAbstractNode> args;
345 for (triton::uint32 i = 0; i < expr.num_args(); i++) {
346 args.push_back(this->convert(expr.arg(i)));
347 }
348
349 node = this->astCtxt->concat(args);
350 break;
351 }
352
353 case Z3_OP_SIGN_EXT: {
354 if (expr.num_args() != 1)
355 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SIGN_EXT must contain one argument.");
356 node = this->astCtxt->sx(expr.hi(), this->convert(expr.arg(0)));
357 break;
358 }
359
360 case Z3_OP_ZERO_EXT: {
361 if (expr.num_args() != 1)
362 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ZERO_EXT must contain one argument.");
363 node = this->astCtxt->zx(expr.hi(), this->convert(expr.arg(0)));
364 break;
365 }
366
367 case Z3_OP_EXTRACT: {
368 if (expr.num_args() != 1)
369 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_EXTRACT must contain one argument.");
370 node = this->astCtxt->extract(expr.hi(), expr.lo(), this->convert(expr.arg(0)));
371 break;
372 }
373
374 case Z3_OP_BSHL: {
375 if (expr.num_args() < 2)
376 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSHL must contain at least two arguments.");
377 node = this->astCtxt->bvshl(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
378 for (triton::uint32 i = 2; i < expr.num_args(); i++)
379 node = this->astCtxt->bvshl(node, this->convert(expr.arg(i)));
380 break;
381 }
382
383 case Z3_OP_BLSHR: {
384 if (expr.num_args() < 2)
385 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BLSHR must contain at least two arguments.");
386 node = this->astCtxt->bvlshr(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
387 for (triton::uint32 i = 2; i < expr.num_args(); i++)
388 node = this->astCtxt->bvlshr(node, this->convert(expr.arg(i)));
389 break;
390 }
391
392 case Z3_OP_BASHR: {
393 if (expr.num_args() < 2)
394 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BASHR must contain at least two arguments.");
395 node = this->astCtxt->bvashr(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
396 for (triton::uint32 i = 2; i < expr.num_args(); i++)
397 node = this->astCtxt->bvashr(node, this->convert(expr.arg(i)));
398 break;
399 }
400
401 case Z3_OP_ROTATE_LEFT: {
402 if (expr.num_args() != 1)
403 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ROTATE_LEFT must contain one argument.");
404 node = this->astCtxt->bvrol(this->convert(expr.arg(0)), expr.hi());
405 break;
406 }
407
408 case Z3_OP_ROTATE_RIGHT: {
409 if (expr.num_args() != 1)
410 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ROTATE_RIGHT must contain one argument.");
411 node = this->astCtxt->bvror(this->convert(expr.arg(0)), expr.hi());
412 break;
413 }
414
415 case Z3_OP_SELECT: {
416 if (expr.num_args() != 2)
417 throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SELECT must contain two argument.");
418 node = this->astCtxt->select(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
419 break;
420 }
421
422 case Z3_OP_STORE: {
423 if (expr.num_args() != 3)
424 throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_STORE must contain three argument.");
425 node = this->astCtxt->store(this->convert(expr.arg(0)), this->convert(expr.arg(1)), this->convert(expr.arg(2)));
426 break;
427 }
428
429 /* Always TRUE */
430 case Z3_OP_TRUE: {
431 node = this->astCtxt->equal(this->astCtxt->bvtrue(), this->astCtxt->bvtrue());
432 break;
433 }
434
435 /* Always FALSE */
436 case Z3_OP_FALSE: {
437 node = this->astCtxt->equal(this->astCtxt->bvtrue(), this->astCtxt->bvfalse());
438 break;
439 }
440
441 /* Variable or string */
442 case Z3_OP_UNINTERPRETED: {
443 std::string name = function.name().str();
444
445 node = this->astCtxt->getVariableNode(name);
446 if (node == nullptr) {
447 node = this->astCtxt->string(name);
448 }
449
450 break;
451 }
452
453 default:
454 throw triton::exceptions::AstLifting("Z3ToTriton::visit(): '" + function.name().str() + "' AST node not supported yet");
455 }
456
457 return node;
458 }
459
460 }; /* ast namespace */
461}; /* triton namespace */
triton::ast::Z3ToTriton::Z3ToTriton
TRITON_EXPORT Z3ToTriton(const triton::ast::SharedAstContext &ctxt)
Constructor.
Definition z3ToTriton.cpp:19
triton::ast::Z3ToTriton::convert
TRITON_EXPORT triton::ast::SharedAbstractNode convert(const z3::expr &expr)
Converts to Triton's AST.
Definition z3ToTriton.cpp:24
triton::exceptions::AstLifting
The exception class used by all AST lifting (e.g z3 <-> triton).
Definition exceptions.hpp:413
triton::ast::SharedAbstractNode
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
triton::ast::SharedAstContext
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition ast.hpp:65
triton::uint512
math::wide_integer::uint512_t uint512
unsigned 512-bits
Definition tritonTypes.hpp:69
triton::uint32
std::uint32_t uint32
unisgned 32-bits
Definition tritonTypes.hpp:39
triton
The Triton namespace.
Definition architecture.cpp:22
Generated by doxygen 1.9.8