libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
astSmtRepresentation.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
12
13
14
15namespace triton {
16 namespace ast {
17 namespace representations {
18
21
22
23 /* Representation dispatcher from an abstract node */
24 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::AbstractNode* node) {
25 switch (node->getType()) {
26 case ARRAY_NODE: return this->print(stream, reinterpret_cast<triton::ast::ArrayNode*>(node)); break;
27 case ASSERT_NODE: return this->print(stream, reinterpret_cast<triton::ast::AssertNode*>(node)); break;
28 case BSWAP_NODE: return this->print(stream, reinterpret_cast<triton::ast::BswapNode*>(node)); break;
29 case BVADD_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvaddNode*>(node)); break;
30 case BVAND_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvandNode*>(node)); break;
31 case BVASHR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvashrNode*>(node)); break;
32 case BVLSHR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvlshrNode*>(node)); break;
33 case BVMUL_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvmulNode*>(node)); break;
34 case BVNAND_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvnandNode*>(node)); break;
35 case BVNEG_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvnegNode*>(node)); break;
36 case BVNOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvnorNode*>(node)); break;
37 case BVNOT_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvnotNode*>(node)); break;
38 case BVOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvorNode*>(node)); break;
39 case BVROL_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvrolNode*>(node)); break;
40 case BVROR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvrorNode*>(node)); break;
41 case BVSDIV_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsdivNode*>(node)); break;
42 case BVSGE_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsgeNode*>(node)); break;
43 case BVSGT_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsgtNode*>(node)); break;
44 case BVSHL_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvshlNode*>(node)); break;
45 case BVSLE_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsleNode*>(node)); break;
46 case BVSLT_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsltNode*>(node)); break;
47 case BVSMOD_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsmodNode*>(node)); break;
48 case BVSREM_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsremNode*>(node)); break;
49 case BVSUB_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvsubNode*>(node)); break;
50 case BVUDIV_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvudivNode*>(node)); break;
51 case BVUGE_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvugeNode*>(node)); break;
52 case BVUGT_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvugtNode*>(node)); break;
53 case BVULE_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvuleNode*>(node)); break;
54 case BVULT_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvultNode*>(node)); break;
55 case BVUREM_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvuremNode*>(node)); break;
56 case BVXNOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvxnorNode*>(node)); break;
57 case BVXOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvxorNode*>(node)); break;
58 case BV_NODE: return this->print(stream, reinterpret_cast<triton::ast::BvNode*>(node)); break;
59 case COMPOUND_NODE: return this->print(stream, reinterpret_cast<triton::ast::CompoundNode*>(node)); break;
60 case CONCAT_NODE: return this->print(stream, reinterpret_cast<triton::ast::ConcatNode*>(node)); break;
61 case DECLARE_NODE: return this->print(stream, reinterpret_cast<triton::ast::DeclareNode*>(node)); break;
62 case DISTINCT_NODE: return this->print(stream, reinterpret_cast<triton::ast::DistinctNode*>(node)); break;
63 case EQUAL_NODE: return this->print(stream, reinterpret_cast<triton::ast::EqualNode*>(node)); break;
64 case EXTRACT_NODE: return this->print(stream, reinterpret_cast<triton::ast::ExtractNode*>(node)); break;
65 case FORALL_NODE: return this->print(stream, reinterpret_cast<triton::ast::ForallNode*>(node)); break;
66 case IFF_NODE: return this->print(stream, reinterpret_cast<triton::ast::IffNode*>(node)); break;
67 case INTEGER_NODE: return this->print(stream, reinterpret_cast<triton::ast::IntegerNode*>(node)); break;
68 case ITE_NODE: return this->print(stream, reinterpret_cast<triton::ast::IteNode*>(node)); break;
69 case LAND_NODE: return this->print(stream, reinterpret_cast<triton::ast::LandNode*>(node)); break;
70 case LET_NODE: return this->print(stream, reinterpret_cast<triton::ast::LetNode*>(node)); break;
71 case LNOT_NODE: return this->print(stream, reinterpret_cast<triton::ast::LnotNode*>(node)); break;
72 case LOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::LorNode*>(node)); break;
73 case LXOR_NODE: return this->print(stream, reinterpret_cast<triton::ast::LxorNode*>(node)); break;
74 case REFERENCE_NODE: return this->print(stream, reinterpret_cast<triton::ast::ReferenceNode*>(node)); break;
75 case SELECT_NODE: return this->print(stream, reinterpret_cast<triton::ast::SelectNode*>(node)); break;
76 case STORE_NODE: return this->print(stream, reinterpret_cast<triton::ast::StoreNode*>(node)); break;
77 case STRING_NODE: return this->print(stream, reinterpret_cast<triton::ast::StringNode*>(node)); break;
78 case SX_NODE: return this->print(stream, reinterpret_cast<triton::ast::SxNode*>(node)); break;
79 case VARIABLE_NODE: return this->print(stream, reinterpret_cast<triton::ast::VariableNode*>(node)); break;
80 case ZX_NODE: return this->print(stream, reinterpret_cast<triton::ast::ZxNode*>(node)); break;
81 default:
82 throw triton::exceptions::AstRepresentation("AstSmtRepresentation::print(AbstractNode): Invalid kind node.");
83 }
84 return stream;
85 }
86
87
88 /* array representation */
89 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ArrayNode* node) {
90 stream << "Memory";
91 return stream;
92 }
93
94
95 /* assert representation */
96 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::AssertNode* node) {
97 stream << "(assert " << node->getChildren()[0] << ")";
98 return stream;
99 }
100
101
102 /* bswap representation */
103 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BswapNode* node) {
104 stream << "(bswap" << node->getBitvectorSize() << " " << node->getChildren()[0] << ")";
105 return stream;
106 }
107
108
109 /* bvadd representation */
110 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvaddNode* node) {
111 stream << "(bvadd " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
112 return stream;
113 }
114
115
116 /* bvand representation */
117 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvandNode* node) {
118 stream << "(bvand " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
119 return stream;
120 }
121
122
123 /* bvashr representation */
124 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvashrNode* node) {
125 stream << "(bvashr " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
126 return stream;
127 }
128
129
130 /* bvlshr representation */
131 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvlshrNode* node) {
132 stream << "(bvlshr " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
133 return stream;
134 }
135
136
137 /* bvmul representation */
138 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvmulNode* node) {
139 stream << "(bvmul " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
140 return stream;
141 }
142
143
144 /* bvnand representation */
145 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvnandNode* node) {
146 stream << "(bvnand " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
147 return stream;
148 }
149
150
151 /* bvneg representation */
152 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvnegNode* node) {
153 stream << "(bvneg " << node->getChildren()[0] << ")";
154 return stream;
155 }
156
157
158 /* bvnor representation */
159 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvnorNode* node) {
160 stream << "(bvnor " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
161 return stream;
162 }
163
164
165 /* bvnot representation */
166 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvnotNode* node) {
167 stream << "(bvnot " << node->getChildren()[0] << ")";
168 return stream;
169 }
170
171
172 /* bvor representation */
173 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvorNode* node) {
174 stream << "(bvor " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
175 return stream;
176 }
177
178
179 /* bvrol representation */
180 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvrolNode* node) {
181 stream << "((_ rotate_left " << node->getChildren()[1] << ") " << node->getChildren()[0] << ")";
182 return stream;
183 }
184
185
186 /* bvror representation */
187 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvrorNode* node) {
188 stream << "((_ rotate_right " << node->getChildren()[1] << ") " << node->getChildren()[0] << ")";
189 return stream;
190 }
191
192
193 /* bvsdiv representation */
194 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsdivNode* node) {
195 stream << "(bvsdiv " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
196 return stream;
197 }
198
199
200 /* bvsge representation */
201 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsgeNode* node) {
202 stream << "(bvsge " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
203 return stream;
204 }
205
206
207 /* bvsgt representation */
208 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsgtNode* node) {
209 stream << "(bvsgt " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
210 return stream;
211 }
212
213
214 /* bvshl representation */
215 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvshlNode* node) {
216 stream << "(bvshl " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
217 return stream;
218 }
219
220
221 /* bvsle representation */
222 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsleNode* node) {
223 stream << "(bvsle " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
224 return stream;
225 }
226
227
228 /* bvslt representation */
229 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsltNode* node) {
230 stream << "(bvslt " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
231 return stream;
232 }
233
234
235 /* bvsmod representation */
236 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsmodNode* node) {
237 stream << "(bvsmod " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
238 return stream;
239 }
240
241
242 /* bvsrem representation */
243 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsremNode* node) {
244 stream << "(bvsrem " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
245 return stream;
246 }
247
248
249 /* bvsub representation */
250 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvsubNode* node) {
251 stream << "(bvsub " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
252 return stream;
253 }
254
255
256 /* bvudiv representation */
257 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvudivNode* node) {
258 stream << "(bvudiv " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
259 return stream;
260 }
261
262
263 /* bvuge representation */
264 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvugeNode* node) {
265 stream << "(bvuge " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
266 return stream;
267 }
268
269
270 /* bvugt representation */
271 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvugtNode* node) {
272 stream << "(bvugt " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
273 return stream;
274 }
275
276
277 /* bvule representation */
278 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvuleNode* node) {
279 stream << "(bvule " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
280 return stream;
281 }
282
283
284 /* bvult representation */
285 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvultNode* node) {
286 stream << "(bvult " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
287 return stream;
288 }
289
290
291 /* bvurem representation */
292 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvuremNode* node) {
293 stream << "(bvurem " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
294 return stream;
295 }
296
297
298 /* bvxnor representation */
299 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvxnorNode* node) {
300 stream << "(bvxnor " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
301 return stream;
302 }
303
304
305 /* bvxor representation */
306 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvxorNode* node) {
307 stream << "(bvxor " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
308 return stream;
309 }
310
311
312 /* bv representation */
313 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::BvNode* node) {
314 stream << "(_ bv" << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
315 return stream;
316 }
317
318
319 /* compound representation */
320 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::CompoundNode* node) {
321 std::vector<triton::ast::SharedAbstractNode> children = node->getChildren();
322 triton::usize size = children.size();
323
324 for (triton::usize index = 0; index < size-1; index++)
325 stream << children[index] << std::endl;
326 stream << children[size-1];
327
328 return stream;
329 }
330
331
332 /* concat representation */
333 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ConcatNode* node) {
334 std::vector<triton::ast::SharedAbstractNode> children = node->getChildren();
335 triton::usize size = children.size();
336
337 if (size < 2)
338 throw triton::exceptions::AstRepresentation("AstSmtRepresentation::print(ConcatNode): Exprs must contain at least two expressions.");
339
340 stream << "(concat";
341 for (triton::usize index = 0; index < size; index++)
342 stream << " " << children[index];
343 stream << ")";
344
345 return stream;
346 }
347
348
349 /* declare representation */
350 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::DeclareNode* node) {
351 if (node->getChildren()[0]->getType() == VARIABLE_NODE) {
352 const triton::engines::symbolic::SharedSymbolicVariable& var = reinterpret_cast<triton::ast::VariableNode*>(node->getChildren()[0].get())->getSymbolicVariable();
353 if (var->getAlias().empty())
354 stream << "(declare-fun " << var->getName() << " () (_ BitVec " << var->getSize() << "))";
355 else
356 stream << "(declare-fun " << var->getAlias() << " () (_ BitVec " << var->getSize() << "))";
357 }
358
359 else if (node->getChildren()[0]->getType() == ARRAY_NODE) {
360 const auto& array = node->getChildren()[0];
361 const auto& size = array->getChildren()[0];
362 stream << "(define-fun " << node->getChildren()[0] << " () (Array (_ BitVec " << size << ") (_ BitVec 8)) ";
363 stream << "((as const (Array (_ BitVec " << size << ") (_ BitVec 8))) (_ bv0 8)))";
364 }
365
366 else
367 throw triton::exceptions::AstRepresentation("AstSmtRepresentation::print(DeclareNode): Invalid sort.");
368
369 return stream;
370 }
371
372
373 /* distinct representation */
374 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::DistinctNode* node) {
375 stream << "(distinct " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
376 return stream;
377 }
378
379
380 /* equal representation */
381 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::EqualNode* node) {
382 stream << "(= " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
383 return stream;
384 }
385
386
387 /* extract representation */
388 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ExtractNode* node) {
389 stream << "((_ extract " << node->getChildren()[0] << " " << node->getChildren()[1] << ") " << node->getChildren()[2] << ")";
390 return stream;
391 }
392
393
394 /* forall representation */
395 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ForallNode* node) {
396 triton::usize size = node->getChildren().size() - 1;
397
398 stream << "(forall (";
399 for (triton::uint32 i = 0; i != size; i++) {
400 const auto& var = reinterpret_cast<triton::ast::VariableNode*>(node->getChildren()[i].get())->getSymbolicVariable();
401 if (var->getAlias().empty()) stream << "(" << var->getName() << " (_ BitVec " << var->getSize() << "))";
402 else stream << "(" << var->getAlias() << " (_ BitVec " << var->getSize() << "))";
403 if (i + 1 != size) stream << " ";
404 }
405 stream << ") " << node->getChildren()[size] << ")";
406
407 return stream;
408 }
409
410
411 /* iff representation */
412 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::IffNode* node) {
413 stream << "(iff " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
414 return stream;
415 }
416
417
418 /* integer representation */
419 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::IntegerNode* node) {
420 stream << node->getInteger();
421 return stream;
422 }
423
424
425 /* ite representation */
426 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::IteNode* node) {
427 stream << "(ite " << node->getChildren()[0] << " " << node->getChildren()[1] << " " << node->getChildren()[2] << ")";
428 return stream;
429 }
430
431
432 /* land representation */
433 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::LandNode* node) {
434 triton::usize size = node->getChildren().size();
435
436 stream << "(and";
437 for (triton::usize index = 0; index < size; index++)
438 stream << " " << node->getChildren()[index];
439 stream << ")";
440
441 return stream;
442 }
443
444
445 /* let representation */
446 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::LetNode* node) {
447 stream << "(let ((" << node->getChildren()[0] << " " << node->getChildren()[1] << ")) " << node->getChildren()[2] << ")";
448 return stream;
449 }
450
451
452 /* lnot representation */
453 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::LnotNode* node) {
454 stream << "(not " << node->getChildren()[0] << ")";
455 return stream;
456 }
457
458
459 /* lor representation */
460 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::LorNode* node) {
461 triton::usize size = node->getChildren().size();
462
463 stream << "(or";
464 for (triton::usize index = 0; index < size; index++)
465 stream << " " << node->getChildren()[index];
466 stream << ")";
467
468 return stream;
469 }
470
471
472 /* lxor representation */
473 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::LxorNode* node) {
474 triton::usize size = node->getChildren().size();
475
476 stream << "(xor";
477 for (triton::usize index = 0; index < size; index++)
478 stream << " " << node->getChildren()[index];
479 stream << ")";
480
481 return stream;
482 }
483
484
485 /* reference representation */
486 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ReferenceNode* node) {
487 stream << node->getSymbolicExpression()->getFormattedId();
488 return stream;
489 }
490
491
492 /* select representation */
493 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::SelectNode* node) {
494 stream << "(select " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
495 return stream;
496 }
497
498
499 /* store representation */
500 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::StoreNode* node) {
501 stream << "(store " << node->getChildren()[0] << " " << node->getChildren()[1] << " " << node->getChildren()[2] << ")";
502 return stream;
503 }
504
505
506 /* string representation */
507 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::StringNode* node) {
508 stream << node->getString();
509 return stream;
510 }
511
512
513 /* sx representation */
514 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::SxNode* node) {
515 stream << "((_ sign_extend " << node->getChildren()[0] << ") " << node->getChildren()[1] << ")";
516 return stream;
517 }
518
519
520 /* variable representation */
521 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::VariableNode* node) {
522 if (node->getSymbolicVariable()->getAlias().empty())
523 stream << node->getSymbolicVariable()->getName();
524 else
525 stream << node->getSymbolicVariable()->getAlias();
526 return stream;
527 }
528
529
530 /* zx representation */
531 std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::ZxNode* node) {
532 stream << "((_ zero_extend " << node->getChildren()[0] << ") " << node->getChildren()[1] << ")";
533 return stream;
534 }
535
536 };
537 };
538};
Abstract node.
Definition ast.hpp:68
TRITON_EXPORT triton::uint32 getBitvectorSize(void) const
Returns the size of the node.
Definition ast.cpp:60
TRITON_EXPORT std::vector< SharedAbstractNode > & getChildren(void)
Returns the children of the node.
Definition ast.cpp:182
TRITON_EXPORT triton::ast::ast_e getType(void) const
Returns the type of the node.
Definition ast.cpp:55
(Array (_ BitVec indexSize) (_ BitVec 8)) node
Definition ast.hpp:193
(assert <expr>) node
Definition ast.hpp:231
(bswap <expr>) node
Definition ast.hpp:242
(_ bv<value> <size>) node
Definition ast.hpp:574
(bvadd <expr1> <expr2>) node
Definition ast.hpp:253
(bvand <expr1> <expr2>) node
Definition ast.hpp:264
(bvashr <expr1> <expr2>) node
Definition ast.hpp:275
(bvlshr <expr1> <expr2>) node
Definition ast.hpp:286
(bvmul <expr1> <expr2>) node
Definition ast.hpp:297
(bvnand <expr1> <expr2>) node
Definition ast.hpp:308
(bvneg <expr>) node
Definition ast.hpp:319
(bvnor <expr1> <expr2>) node
Definition ast.hpp:330
(bvnot <expr>) node
Definition ast.hpp:341
(bvor <expr1> <expr2>) node
Definition ast.hpp:352
((_ rotate_left rot) <expr>) node
Definition ast.hpp:363
((_ rotate_right rot) <expr>) node
Definition ast.hpp:375
(bvsdiv <expr1> <expr2>) node
Definition ast.hpp:387
(bvsge <expr1> <expr2>) node
Definition ast.hpp:398
(bvsgt <expr1> <expr2>) node
Definition ast.hpp:409
(bvshl <expr1> <expr2>) node
Definition ast.hpp:420
(bvsle <expr1> <expr2>) node
Definition ast.hpp:431
(bvslt <expr1> <expr2>) node
Definition ast.hpp:442
(bvsmod <expr1> <expr2>) node
Definition ast.hpp:453
(bvsrem <expr1> <expr2>) node
Definition ast.hpp:464
(bvsub <expr1> <expr2>) node
Definition ast.hpp:475
(bvudiv <expr1> <expr2>) node
Definition ast.hpp:486
(bvuge <expr1> <expr2>) node
Definition ast.hpp:497
(bvugt <expr1> <expr2>) node
Definition ast.hpp:508
(bvule <expr1> <expr2>) node
Definition ast.hpp:519
(bvult <expr1> <expr2>) node
Definition ast.hpp:530
(bvurem <expr1> <expr2>) node
Definition ast.hpp:541
(bvxnor <expr1> <expr2>) node
Definition ast.hpp:552
(bvxor <expr1> <expr2>) node
Definition ast.hpp:563
[<expr1> <expr2> <expr3> ...] node
Definition ast.hpp:585
(concat <expr1> <expr2> ...) node
Definition ast.hpp:601
(declare-fun <var_name> () (_ BitVec <var_size>)) node
Definition ast.hpp:618
(distinct <expr1> <expr2> ...) node
Definition ast.hpp:629
(= <expr1> <expr2> ...) node
Definition ast.hpp:640
((_ extract <high> <low>) <expr>) node
Definition ast.hpp:651
(forall ((x (_ BitVec <size>)), ...) body)
Definition ast.hpp:662
(iff <expr1> <expr2>)
Definition ast.hpp:679
Integer node.
Definition ast.hpp:690
(ite <ifExpr> <thenExpr> <elseExpr>)
Definition ast.hpp:705
(and <expr1> <expr2>)
Definition ast.hpp:716
(let ((<alias> <expr2>)) <expr3>)
Definition ast.hpp:733
(lnot <expr>)
Definition ast.hpp:744
(or <expr1> <expr2>)
Definition ast.hpp:755
(xor <expr1> <expr2>)
Definition ast.hpp:772
Reference node.
Definition ast.hpp:789
(select array index)
Definition ast.hpp:804
(store array index expr)
Definition ast.hpp:816
String node.
Definition ast.hpp:852
((_ sign_extend sizeExt) <expr>) node
Definition ast.hpp:867
Variable node.
Definition ast.hpp:878
((_ zero_extend sizeExt) <expr>) node
Definition ast.hpp:893
TRITON_EXPORT std::ostream & print(std::ostream &stream, triton::ast::AbstractNode *node)
Displays the node according to the representation mode.
The exception class used by all AST node representations.
std::shared_ptr< triton::engines::symbolic::SymbolicVariable > SharedSymbolicVariable
Shared Symbolic variable.
Definition ast.hpp:43
std::size_t usize
unsigned MAX_INT 32 or 64 bits according to the CPU.
std::uint32_t uint32
unisgned 32-bits
The Triton namespace.