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 <vector>
9 
10 #include <triton/cpuSize.hpp>
11 #include <triton/exceptions.hpp>
12 #include <triton/symbolicExpression.hpp>
13 #include <triton/symbolicVariable.hpp>
14 #include <triton/tritonToZ3Ast.hpp>
15 
16 
17 
18 namespace triton {
19   namespace ast {
20 
TritonToZ3Ast(bool eval)21     TritonToZ3Ast::TritonToZ3Ast(bool eval)
22       : context() {
23       this->isEval = eval;
24     }
25 
26 
~TritonToZ3Ast()27     TritonToZ3Ast::~TritonToZ3Ast() {
28       /* See #828: Release ownership before calling container destructor */
29       this->symbols.clear();
30       this->variables.clear();
31     }
32 
33 
getUintValue(const z3::expr & expr)34     triton::__uint TritonToZ3Ast::getUintValue(const z3::expr& expr) {
35       if (!expr.is_int())
36         throw triton::exceptions::Exception("TritonToZ3Ast::getUintValue(): The ast is not a numerical value.");
37 
38       #if defined(__x86_64__) || defined(_M_X64) || defined(__aarch64__)
39       return expr.get_numeral_uint64();
40       #endif
41       #if defined(__i386) || defined(_M_IX86)
42       return expr.get_numeral_uint();
43       #endif
44     }
45 
46 
getStringValue(const z3::expr & expr)47     std::string TritonToZ3Ast::getStringValue(const z3::expr& expr) {
48       return Z3_get_numeral_string(this->context, expr);
49     }
50 
51 
convert(const triton::ast::SharedAbstractNode & node)52     z3::expr TritonToZ3Ast::convert(const triton::ast::SharedAbstractNode& node) {
53       std::unordered_map<triton::ast::SharedAbstractNode, z3::expr> results;
54 
55       auto nodes = triton::ast::childrenExtraction(node, true /* unroll*/, true /* revert */);
56 
57       for (auto&& n : nodes) {
58         results.insert(std::make_pair(n, this->do_convert(n, &results)));
59       }
60 
61       return results.at(node);
62     }
63 
64 
do_convert(const triton::ast::SharedAbstractNode & node,std::unordered_map<triton::ast::SharedAbstractNode,z3::expr> * results)65     z3::expr TritonToZ3Ast::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map<triton::ast::SharedAbstractNode, z3::expr>* results) {
66       if (node == nullptr)
67         throw triton::exceptions::AstTranslations("TritonToZ3Ast::do_convert(): node cannot be null.");
68 
69       /* Prepare z3's children */
70       std::vector<z3::expr> children;
71       for (auto&& n : node->getChildren()) {
72         children.emplace_back(results->at(n));
73       }
74 
75       switch (node->getType()) {
76         case BVADD_NODE:
77           return to_expr(this->context, Z3_mk_bvadd(this->context, children[0], children[1]));
78 
79         case BVAND_NODE:
80           return to_expr(this->context, Z3_mk_bvand(this->context, children[0], children[1]));
81 
82         case BVASHR_NODE:
83           return to_expr(this->context, Z3_mk_bvashr(this->context, children[0], children[1]));
84 
85         case BVLSHR_NODE:
86           return to_expr(this->context, Z3_mk_bvlshr(this->context, children[0], children[1]));
87 
88         case BVMUL_NODE:
89           return to_expr(this->context, Z3_mk_bvmul(this->context, children[0], children[1]));
90 
91         case BVNAND_NODE:
92           return to_expr(this->context, Z3_mk_bvnand(this->context, children[0], children[1]));
93 
94         case BVNEG_NODE:
95           return to_expr(this->context, Z3_mk_bvneg(this->context, children[0]));
96 
97         case BVNOR_NODE:
98           return to_expr(this->context, Z3_mk_bvnor(this->context, children[0], children[1]));
99 
100         case BVNOT_NODE:
101           return to_expr(this->context, Z3_mk_bvnot(this->context, children[0]));
102 
103         case BVOR_NODE:
104           return to_expr(this->context, Z3_mk_bvor(this->context, children[0], children[1]));
105 
106         case BVROL_NODE: {
107           triton::uint32 rot = reinterpret_cast<triton::ast::IntegerNode*>(node->getChildren()[1].get())->getInteger().convert_to<triton::uint32>();
108           return to_expr(this->context, Z3_mk_rotate_left(this->context, rot, children[0]));
109         }
110 
111         case BVROR_NODE: {
112           triton::uint32 rot = reinterpret_cast<triton::ast::IntegerNode*>(node->getChildren()[1].get())->getInteger().convert_to<triton::uint32>();
113           return to_expr(this->context, Z3_mk_rotate_right(this->context, rot, children[0]));
114         }
115 
116         case BVSDIV_NODE:
117           return to_expr(this->context, Z3_mk_bvsdiv(this->context, children[0], children[1]));
118 
119         case BVSGE_NODE:
120           return to_expr(this->context, Z3_mk_bvsge(this->context, children[0], children[1]));
121 
122         case BVSGT_NODE:
123           return to_expr(this->context, Z3_mk_bvsgt(this->context, children[0], children[1]));
124 
125         case BVSHL_NODE:
126           return to_expr(this->context, Z3_mk_bvshl(this->context, children[0], children[1]));
127 
128         case BVSLE_NODE:
129           return to_expr(this->context, Z3_mk_bvsle(this->context, children[0], children[1]));
130 
131         case BVSLT_NODE:
132           return to_expr(this->context, Z3_mk_bvslt(this->context, children[0], children[1]));
133 
134         case BVSMOD_NODE:
135           return to_expr(this->context, Z3_mk_bvsmod(this->context, children[0], children[1]));
136 
137         case BVSREM_NODE:
138           return to_expr(this->context, Z3_mk_bvsrem(this->context, children[0], children[1]));
139 
140         case BVSUB_NODE:
141           return to_expr(this->context, Z3_mk_bvsub(this->context, children[0], children[1]));
142 
143         case BVUDIV_NODE:
144           return to_expr(this->context, Z3_mk_bvudiv(this->context, children[0], children[1]));
145 
146         case BVUGE_NODE:
147           return to_expr(this->context, Z3_mk_bvuge(this->context, children[0], children[1]));
148 
149         case BVUGT_NODE:
150           return to_expr(this->context, Z3_mk_bvugt(this->context, children[0], children[1]));
151 
152         case BVULE_NODE:
153           return to_expr(this->context, Z3_mk_bvule(this->context, children[0], children[1]));
154 
155         case BVULT_NODE:
156           return to_expr(this->context, Z3_mk_bvult(this->context, children[0], children[1]));
157 
158         case BVUREM_NODE:
159           return to_expr(this->context, Z3_mk_bvurem(this->context, children[0], children[1]));
160 
161         case BVXNOR_NODE:
162           return to_expr(this->context, Z3_mk_bvxnor(this->context, children[0], children[1]));
163 
164         case BVXOR_NODE:
165           return to_expr(this->context, Z3_mk_bvxor(this->context, children[0], children[1]));
166 
167         case BV_NODE: {
168           z3::expr value        = children[0];
169           z3::expr size         = children[1];
170           triton::uint32 bvsize = static_cast<triton::uint32>(this->getUintValue(size));
171           return this->context.bv_val(this->getStringValue(value).c_str(), bvsize);
172         }
173 
174         case CONCAT_NODE: {
175           z3::expr currentValue = children[0];
176           z3::expr nextValue(this->context);
177 
178           // Child[0] is the LSB
179           for (triton::uint32 idx = 1; idx < children.size(); idx++) {
180             nextValue = children[idx];
181             currentValue = to_expr(this->context, Z3_mk_concat(this->context, currentValue, nextValue));
182           }
183           return currentValue;
184         }
185 
186         case DISTINCT_NODE: {
187           z3::expr op1 = children[0];
188           z3::expr op2 = children[1];
189           Z3_ast ops[] = {op1, op2};
190 
191           return to_expr(this->context, Z3_mk_distinct(this->context, 2, ops));
192         }
193 
194         case EQUAL_NODE:
195           return to_expr(this->context, Z3_mk_eq(this->context, children[0], children[1]));
196 
197         case EXTRACT_NODE: {
198           z3::expr high     = children[0];
199           z3::expr low      = children[1];
200           z3::expr value    = children[2];
201           triton::uint32 hv = static_cast<triton::uint32>(this->getUintValue(high));
202           triton::uint32 lv = static_cast<triton::uint32>(this->getUintValue(low));
203 
204           return to_expr(this->context, Z3_mk_extract(this->context, hv, lv, value));
205         }
206 
207         case FORALL_NODE: {
208           triton::usize size = node->getChildren().size() - 1;
209           Z3_app* vars = new Z3_app[size];
210 
211           for (triton::uint32 i = 0; i != size; i++) {
212             vars[i] = children[i];
213           }
214 
215           z3::expr e = to_expr(this->context, Z3_mk_forall_const(this->context, 0, size, vars, 0, 0, children[size]));
216           delete[] vars;
217 
218           return e;
219         }
220 
221         case IFF_NODE: {
222           z3::expr op1 = children[0];
223           z3::expr op2 = children[1];
224 
225           return to_expr(this->context, Z3_mk_iff(this->context, op1, op2));
226         }
227 
228         case INTEGER_NODE: {
229           std::string value(reinterpret_cast<triton::ast::IntegerNode*>(node.get())->getInteger().convert_to<std::string>());
230           return this->context.int_val(value.c_str());
231         }
232 
233         case ITE_NODE: {
234           z3::expr op1 = children[0]; // condition
235           z3::expr op2 = children[1]; // if true
236           z3::expr op3 = children[2]; // if false
237 
238           return to_expr(this->context, Z3_mk_ite(this->context, op1, op2, op3));
239         }
240 
241         case LAND_NODE: {
242           z3::expr currentValue = children[0];
243           if (!currentValue.get_sort().is_bool()) {
244             throw triton::exceptions::AstTranslations("TritonToZ3Ast::LandNode(): Land can be apply only on bool value.");
245           }
246           z3::expr nextValue(this->context);
247 
248           for (triton::uint32 idx = 1; idx < children.size(); idx++) {
249             nextValue = children[idx];
250             if (!nextValue.get_sort().is_bool()) {
251               throw triton::exceptions::AstTranslations("TritonToZ3Ast::LandNode(): Land can be apply only on bool value.");
252             }
253             Z3_ast ops[] = {currentValue, nextValue};
254             currentValue = to_expr(this->context, Z3_mk_and(this->context, 2, ops));
255           }
256 
257           return currentValue;
258         }
259 
260         case LET_NODE: {
261           std::string symbol    = reinterpret_cast<triton::ast::StringNode*>(node->getChildren()[0].get())->getString();
262           this->symbols[symbol] = node->getChildren()[1];
263 
264           return children[2];
265         }
266 
267         case LNOT_NODE: {
268           z3::expr value = children[0];
269           if (!value.get_sort().is_bool()) {
270             throw triton::exceptions::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value.");
271           }
272           return to_expr(this->context, Z3_mk_not(this->context, value));
273         }
274 
275         case LOR_NODE: {
276           z3::expr currentValue = children[0];
277           if (!currentValue.get_sort().is_bool()) {
278             throw triton::exceptions::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value.");
279           }
280           z3::expr nextValue(this->context);
281 
282           for (triton::uint32 idx = 1; idx < children.size(); idx++) {
283             nextValue = children[idx];
284             if (!nextValue.get_sort().is_bool()) {
285               throw triton::exceptions::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value.");
286             }
287             Z3_ast ops[] = {currentValue, nextValue};
288             currentValue = to_expr(this->context, Z3_mk_or(this->context, 2, ops));
289           }
290 
291           return currentValue;
292         }
293 
294         case LXOR_NODE: {
295           z3::expr currentValue = children[0];
296           if (!currentValue.get_sort().is_bool()) {
297             throw triton::exceptions::AstTranslations("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value.");
298           }
299           z3::expr nextValue(this->context);
300 
301           for (triton::uint32 idx = 1; idx < children.size(); idx++) {
302             nextValue = children[idx];
303             if (!nextValue.get_sort().is_bool()) {
304               throw triton::exceptions::AstTranslations("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value.");
305             }
306             currentValue = to_expr(this->context, Z3_mk_xor(this->context, currentValue, nextValue));
307           }
308 
309           return currentValue;
310         }
311 
312         case REFERENCE_NODE:
313           return results->at(reinterpret_cast<triton::ast::ReferenceNode*>(node.get())->getSymbolicExpression()->getAst());
314 
315         case STRING_NODE: {
316           std::string value = reinterpret_cast<triton::ast::StringNode*>(node.get())->getString();
317 
318           if (this->symbols.find(value) == this->symbols.end())
319             throw triton::exceptions::AstTranslations("TritonToZ3Ast::do_convert(): [STRING_NODE] Symbols not found.");
320 
321           return results->at(this->symbols[value]);
322         }
323 
324         case SX_NODE: {
325           z3::expr ext        = children[0];
326           z3::expr value      = children[1];
327           triton::uint32 extv = static_cast<triton::uint32>(this->getUintValue(ext));
328 
329           return to_expr(this->context, Z3_mk_sign_ext(this->context, extv, value));
330         }
331 
332         case VARIABLE_NODE: {
333           const triton::engines::symbolic::SharedSymbolicVariable& symVar = reinterpret_cast<triton::ast::VariableNode*>(node.get())->getSymbolicVariable();
334 
335           /* Record variable */
336           this->variables[symVar->getName()] = symVar;
337 
338           /* If the conversion is used to evaluate a node, we concretize symbolic variables */
339           if (this->isEval) {
340             triton::uint512 value = reinterpret_cast<triton::ast::VariableNode*>(node.get())->evaluate();
341             std::string strValue(value.convert_to<std::string>());
342             return this->context.bv_val(strValue.c_str(), symVar->getSize());
343           }
344 
345           /* Otherwise, we keep the symbolic variables for a real conversion */
346           return this->context.bv_const(symVar->getName().c_str(), symVar->getSize());
347         }
348 
349         case ZX_NODE: {
350           z3::expr ext        = children[0];
351           z3::expr value      = children[1];
352           triton::uint32 extv = static_cast<triton::uint32>(this->getUintValue(ext));
353 
354           return to_expr(this->context, Z3_mk_zero_ext(this->context, extv, value));
355         }
356 
357         default:
358           throw triton::exceptions::AstTranslations("TritonToZ3Ast::do_convert(): Invalid kind of node.");
359       }
360     }
361 
362   }; /* ast namespace */
363 }; /* triton namespace */
364