libTriton version 1.0 build 1588
Loading...
Searching...
No Matches
tritonToBitwuzla.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>
16
17
18
19namespace triton {
20 namespace ast {
21
23 : isEval(eval) {
24 }
25
26
28 this->translatedNodes.clear();
29 this->variables.clear();
30 this->symbols.clear();
31 }
32
33
34 const std::unordered_map<const BitwuzlaTerm*, triton::engines::symbolic::SharedSymbolicVariable>& TritonToBitwuzla::getVariables(void) const {
35 return this->variables;
36 }
37
38
39 const std::map<size_t, const BitwuzlaSort*>& TritonToBitwuzla::getBitvectorSorts(void) const {
40 return this->bvSorts;
41 }
42
43
44 const BitwuzlaTerm* TritonToBitwuzla::convert(const SharedAbstractNode& node, Bitwuzla* bzla) {
45 auto nodes = childrenExtraction(node, true /* unroll*/, true /* revert */);
46
47 for (auto&& n : nodes) {
48 this->translatedNodes[n] = translate(n, bzla);
49 }
50
51 return this->translatedNodes.at(node);
52 }
53
54
55 const BitwuzlaTerm* TritonToBitwuzla::translate(const SharedAbstractNode& node, Bitwuzla* bzla) {
56 if (node == nullptr)
57 throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): node cannot be null.");
58
59 std::vector<const BitwuzlaTerm*> children;
60 for (auto&& n : node->getChildren()) {
61 children.emplace_back(this->translatedNodes.at(n));
62 }
63
64 switch (node->getType()) {
65
66 case ARRAY_NODE: {
67 auto size = triton::ast::getInteger<triton::uint32>(node->getChildren()[0]);
68 auto isort = bitwuzla_mk_bv_sort(bzla, size); // index sort
69 auto vsort = bitwuzla_mk_bv_sort(bzla, 8); // value sort
70 auto asort = bitwuzla_mk_array_sort(bzla, isort, vsort); // array sort
71 auto value = bitwuzla_mk_bv_value_uint64(bzla, vsort, 0); // const value
72 return bitwuzla_mk_const_array(bzla, asort, value);
73 }
74
75 case BSWAP_NODE: {
76 auto bvsize = node->getBitvectorSize();
77 auto* bvsort = bitwuzla_mk_bv_sort(bzla, bvsize);
78 auto* retval = bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_AND, children[0], bitwuzla_mk_bv_value_uint64(bzla, bvsort, 0xff));
79 for (triton::uint32 index = 8 ; index != bvsize ; index += triton::bitsize::byte) {
80 retval = bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SHL, retval, bitwuzla_mk_bv_value_uint64(bzla, bvsort, 8));
81 retval = bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_OR, retval,
82 bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_AND,
83 bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SHR, children[0], bitwuzla_mk_bv_value_uint64(bzla, bvsort, index)),
84 bitwuzla_mk_bv_value_uint64(bzla, bvsort, 0xff)
85 )
86 );
87 }
88 return retval;
89 }
90
91 case BVADD_NODE:
92 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_ADD, children[0], children[1]);
93
94 case BVAND_NODE:
95 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_AND, children[0], children[1]);
96
97 case BVASHR_NODE:
98 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_ASHR, children[0], children[1]);
99
100 case BVLSHR_NODE:
101 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SHR, children[0], children[1]);
102
103 case BVMUL_NODE:
104 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_MUL, children[0], children[1]);
105
106 case BVNAND_NODE:
107 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_NAND, children[0], children[1]);
108
109 case BVNEG_NODE:
110 return bitwuzla_mk_term1(bzla, BITWUZLA_KIND_BV_NEG, children[0]);
111
112 case BVNOR_NODE:
113 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_NOR, children[0], children[1]);
114
115 case BVNOT_NODE:
116 return bitwuzla_mk_term1(bzla, BITWUZLA_KIND_BV_NOT, children[0]);
117
118 case BVOR_NODE:
119 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_OR, children[0], children[1]);
120
121 case BVROL_NODE: {
122 auto childNodes = node->getChildren();
123 auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
124 return bitwuzla_mk_term1_indexed1(bzla, BITWUZLA_KIND_BV_ROLI, children[0], idx);
125 }
126
127 case BVROR_NODE: {
128 auto childNodes = node->getChildren();
129 auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
130 return bitwuzla_mk_term1_indexed1(bzla, BITWUZLA_KIND_BV_RORI, children[0], idx);
131 }
132
133 case BVSDIV_NODE:
134 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SDIV, children[0], children[1]);
135
136 case BVSGE_NODE:
137 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SGE, children[0], children[1]);
138
139 case BVSGT_NODE:
140 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SGT, children[0], children[1]);
141
142 case BVSHL_NODE:
143 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SHL, children[0], children[1]);
144
145 case BVSLE_NODE:
146 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SLE, children[0], children[1]);
147
148 case BVSLT_NODE:
149 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SLT, children[0], children[1]);
150
151 case BVSMOD_NODE:
152 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SMOD, children[0], children[1]);
153
154 case BVSREM_NODE:
155 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SREM, children[0], children[1]);
156
157 case BVSUB_NODE:
158 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_SUB, children[0], children[1]);
159
160 case BVUDIV_NODE:
161 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_UDIV, children[0], children[1]);
162
163 case BVUGE_NODE:
164 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_UGE, children[0], children[1]);
165
166 case BVUGT_NODE:
167 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_UGT, children[0], children[1]);
168
169 case BVULE_NODE:
170 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_ULE, children[0], children[1]);
171
172 case BVULT_NODE:
173 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_ULT, children[0], children[1]);
174
175 case BVUREM_NODE:
176 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_UREM, children[0], children[1]);
177
178 case BVXNOR_NODE:
179 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_XNOR, children[0], children[1]);
180
181 case BVXOR_NODE:
182 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_BV_XOR, children[0], children[1]);
183
184 case BV_NODE: {
185 auto childNodes = node->getChildren();
186 auto bv_size = triton::ast::getInteger<triton::usize>(childNodes[1]);
187 auto sort = this->bvSorts.find(bv_size);
188 if (sort == this->bvSorts.end()) {
189 sort = this->bvSorts.insert({bv_size, bitwuzla_mk_bv_sort(bzla, bv_size)}).first;
190 }
191
192 // Handle bitvector value as integer if it small enough.
193 if (bv_size <= sizeof(uint64_t) * 8) {
194 auto bv_value = triton::ast::getInteger<triton::uint64>(childNodes[0]);
195 return bitwuzla_mk_bv_value_uint64(bzla, sort->second, bv_value);
196 }
197
198 auto bv_value = triton::ast::getInteger<std::string>(childNodes[0]);
199 return bitwuzla_mk_bv_value(bzla, sort->second, bv_value.c_str(), BITWUZLA_BV_BASE_DEC);
200 }
201
202 case CONCAT_NODE:
203 return bitwuzla_mk_term(bzla, BITWUZLA_KIND_BV_CONCAT, children.size(), children.data());
204
205 case DISTINCT_NODE:
206 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_DISTINCT, children[0], children[1]);
207
208 case EQUAL_NODE:
209 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_EQUAL, children[0], children[1]);
210
211 case EXTRACT_NODE: {
212 auto childNodes = node->getChildren();
213 auto high = triton::ast::getInteger<triton::usize>(childNodes[0]);
214 auto low = triton::ast::getInteger<triton::usize>(childNodes[1]);
215 return bitwuzla_mk_term1_indexed2(bzla, BITWUZLA_KIND_BV_EXTRACT, children[2], high, low);
216 }
217
218 case FORALL_NODE:
219 throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062).");
220
221 case IFF_NODE:
222 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_IFF, children[0], children[1]);
223
224 case INTEGER_NODE:
225 return nullptr;
226
227 case ITE_NODE:
228 return bitwuzla_mk_term3(bzla, BITWUZLA_KIND_ITE, children[0], children[1], children[2]);
229
230 case LAND_NODE:
231 return bitwuzla_mk_term(bzla, BITWUZLA_KIND_AND, children.size(), children.data());
232
233 case LET_NODE: {
234 auto childNodes = node->getChildren();
235 symbols[reinterpret_cast<triton::ast::StringNode*>(childNodes[0].get())->getString()] = childNodes[1];
236 return children[2];
237 }
238
239 case LNOT_NODE:
240 return bitwuzla_mk_term1(bzla, BITWUZLA_KIND_NOT, children[0]);
241
242 case LOR_NODE:
243 return bitwuzla_mk_term(bzla, BITWUZLA_KIND_OR, children.size(), children.data());
244
245 case LXOR_NODE:
246 return bitwuzla_mk_term(bzla, BITWUZLA_KIND_XOR, children.size(), children.data());
247
248 case REFERENCE_NODE: {
249 auto ref = reinterpret_cast<ReferenceNode*>(node.get())->getSymbolicExpression()->getAst();
250 return this->translatedNodes.at(ref);
251 }
252
253 case SELECT_NODE:
254 return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_ARRAY_SELECT, children[0], children[1]);
255
256 case STORE_NODE:
257 return bitwuzla_mk_term3(bzla, BITWUZLA_KIND_ARRAY_STORE, children[0], children[1], children[2]);
258
259 case STRING_NODE: {
260 std::string value = reinterpret_cast<triton::ast::StringNode*>(node.get())->getString();
261
262 auto it = symbols.find(value);
263 if (it == symbols.end())
264 throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): [STRING_NODE] Symbols not found.");
265
266 return this->translatedNodes.at(it->second);
267 }
268
269 case SX_NODE: {
270 auto childNodes = node->getChildren();
271 auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
272 return bitwuzla_mk_term1_indexed1(bzla, BITWUZLA_KIND_BV_SIGN_EXTEND, children[1], ext);
273 }
274
275 case VARIABLE_NODE: {
276 const auto& symVar = reinterpret_cast<VariableNode*>(node.get())->getSymbolicVariable();
277 auto size = symVar->getSize();
278 auto sort = this->bvSorts.find(size);
279 if (sort == this->bvSorts.end()) {
280 sort = this->bvSorts.insert({size, bitwuzla_mk_bv_sort(bzla, size)}).first;
281 }
282
283 // If the conversion is used to evaluate a node, we concretize symbolic variables.
284 if (this->isEval) {
285 triton::uint512 value = reinterpret_cast<triton::ast::VariableNode*>(node.get())->evaluate();
286 if (size <= sizeof(uint64_t) * 8) {
287 return bitwuzla_mk_bv_value_uint64(bzla, sort->second, static_cast<uint64_t>(value));
288 }
289 return bitwuzla_mk_bv_value(bzla, sort->second, triton::utils::toString(value).c_str(), BITWUZLA_BV_BASE_DEC);
290 }
291
292 auto n = bitwuzla_mk_const(bzla, sort->second, symVar->getName().c_str());
293 variables[n] = symVar;
294 return n;
295 }
296
297 case ZX_NODE: {
298 auto childNodes = node->getChildren();
299 auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
300 return bitwuzla_mk_term1_indexed1(bzla, BITWUZLA_KIND_BV_ZERO_EXTEND,children[1], ext);
301 }
302
303 default:
304 throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): Invalid kind of node.");
305 }
306 }
307
308 }; /* ast namespace */
309}; /* triton namespace */
String node.
Definition: ast.hpp:852
TRITON_EXPORT const BitwuzlaTerm * convert(const SharedAbstractNode &node, Bitwuzla *bzla)
Converts to Bitwuzla's AST.
TRITON_EXPORT ~TritonToBitwuzla()
Destructor.
TRITON_EXPORT const std::map< size_t, const BitwuzlaSort * > & getBitvectorSorts(void) const
Returns bitvector sorts.
TRITON_EXPORT const std::unordered_map< const BitwuzlaTerm *, triton::engines::symbolic::SharedSymbolicVariable > & getVariables(void) const
Returns symbolic variables and its assosiated Bitwuzla terms to process the solver model.
TRITON_EXPORT TritonToBitwuzla(bool eval=false)
Constructor.
Variable node.
Definition: ast.hpp:878
The exception class used by all AST lifting (e.g z3 <-> triton).
Definition: exceptions.hpp:413
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:3689
@ REFERENCE_NODE
Definition: astEnums.hpp:79
constexpr triton::uint32 byte
byte size in bit
Definition: cpuSize.hpp:60
std::uint32_t uint32
unisgned 32-bits
Definition: tritonTypes.hpp:39
std::string toString(const T &obj)
Converts an object to a string.
Definition: coreUtils.hpp:38
The Triton namespace.