28 this->translatedNodes.clear();
29 this->variables.clear();
30 this->symbols.clear();
35 return this->variables;
47 for (
auto&& n : nodes) {
48 this->translatedNodes[n] = translate(n, bzla);
51 return this->translatedNodes.at(node);
55 BitwuzlaTerm TritonToBitwuzla::translate(
const SharedAbstractNode& node, Bitwuzla* bzla) {
59 std::vector<BitwuzlaTerm> children;
60 for (
auto&& n : node->getChildren()) {
61 children.emplace_back(this->translatedNodes.at(n));
64 switch (node->getType()) {
67 auto size = triton::ast::getInteger<triton::uint32>(node->getChildren()[0]);
68 auto isort = bitwuzla_mk_bv_sort(size);
69 auto vsort = bitwuzla_mk_bv_sort(8);
70 auto asort = bitwuzla_mk_array_sort(isort, vsort);
71 auto value = bitwuzla_mk_bv_value_uint64(vsort, 0);
72 return bitwuzla_mk_const_array(asort, value);
76 auto bvsize = node->getBitvectorSize();
77 auto bvsort = bitwuzla_mk_bv_sort(bvsize);
78 auto retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND, children[0], bitwuzla_mk_bv_value_uint64(bvsort, 0xff));
80 retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHL, retval, bitwuzla_mk_bv_value_uint64(bvsort, 8));
81 retval = bitwuzla_mk_term2(BITWUZLA_KIND_BV_OR, retval,
82 bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND,
83 bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHR, children[0], bitwuzla_mk_bv_value_uint64(bvsort, index)),
84 bitwuzla_mk_bv_value_uint64(bvsort, 0xff)
92 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ADD, children[0], children[1]);
95 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_AND, children[0], children[1]);
98 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ASHR, children[0], children[1]);
101 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHR, children[0], children[1]);
104 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_MUL, children[0], children[1]);
107 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_NAND, children[0], children[1]);
110 return bitwuzla_mk_term1(BITWUZLA_KIND_BV_NEG, children[0]);
113 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_NOR, children[0], children[1]);
116 return bitwuzla_mk_term1(BITWUZLA_KIND_BV_NOT, children[0]);
119 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_OR, children[0], children[1]);
122 auto childNodes = node->getChildren();
123 auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
124 return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_ROLI, children[0], idx);
128 auto childNodes = node->getChildren();
129 auto idx = triton::ast::getInteger<triton::usize>(childNodes[1]);
130 return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_RORI, children[0], idx);
134 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SDIV, children[0], children[1]);
137 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SGE, children[0], children[1]);
140 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SGT, children[0], children[1]);
143 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SHL, children[0], children[1]);
146 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SLE, children[0], children[1]);
149 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SLT, children[0], children[1]);
152 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SMOD, children[0], children[1]);
155 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SREM, children[0], children[1]);
158 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_SUB, children[0], children[1]);
161 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UDIV, children[0], children[1]);
164 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UGE, children[0], children[1]);
167 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UGT, children[0], children[1]);
170 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ULE, children[0], children[1]);
173 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_ULT, children[0], children[1]);
176 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_UREM, children[0], children[1]);
179 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_XNOR, children[0], children[1]);
182 return bitwuzla_mk_term2(BITWUZLA_KIND_BV_XOR, children[0], children[1]);
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(bv_size)}).first;
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(sort->second, bv_value);
198 auto bv_value = triton::ast::getInteger<std::string>(childNodes[0]);
199 return bitwuzla_mk_bv_value(sort->second, bv_value.c_str(), 10);
203 return bitwuzla_mk_term(BITWUZLA_KIND_BV_CONCAT, children.size(), children.data());
206 return bitwuzla_mk_term2(BITWUZLA_KIND_DISTINCT, children[0], children[1]);
209 return bitwuzla_mk_term2(BITWUZLA_KIND_EQUAL, children[0], children[1]);
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(BITWUZLA_KIND_BV_EXTRACT, children[2], high, low);
222 return bitwuzla_mk_term2(BITWUZLA_KIND_IFF, children[0], children[1]);
225 return (BitwuzlaTerm) 0;
228 return bitwuzla_mk_term3(BITWUZLA_KIND_ITE, children[0], children[1], children[2]);
231 return bitwuzla_mk_term(BITWUZLA_KIND_AND, children.size(), children.data());
234 auto childNodes = node->getChildren();
240 return bitwuzla_mk_term1(BITWUZLA_KIND_NOT, children[0]);
243 return bitwuzla_mk_term(BITWUZLA_KIND_OR, children.size(), children.data());
246 return bitwuzla_mk_term(BITWUZLA_KIND_XOR, children.size(), children.data());
249 auto ref =
reinterpret_cast<ReferenceNode*
>(node.get())->getSymbolicExpression()->getAst();
250 return this->translatedNodes.at(ref);
254 return bitwuzla_mk_term2(BITWUZLA_KIND_ARRAY_SELECT, children[0], children[1]);
257 return bitwuzla_mk_term3(BITWUZLA_KIND_ARRAY_STORE, children[0], children[1], children[2]);
262 auto it = symbols.find(value);
263 if (it == symbols.end())
266 return this->translatedNodes.at(it->second);
270 auto childNodes = node->getChildren();
271 auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
272 return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_SIGN_EXTEND, children[1], ext);
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(size)}).first;
286 if (size <=
sizeof(uint64_t) * 8) {
287 return bitwuzla_mk_bv_value_uint64(sort->second,
static_cast<uint64_t
>(value));
292 auto n = (BitwuzlaTerm) 0;
294 for (
auto it = variables.begin(); it != variables.end(); ++it) {
295 if (it->second == symVar) {
302 n = bitwuzla_mk_const(sort->second, symVar->getName().c_str());
303 variables[n] = symVar;
310 auto childNodes = node->getChildren();
311 auto ext = triton::ast::getInteger<triton::usize>(childNodes[0]);
312 return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_ZERO_EXTEND,children[1], ext);
TRITON_EXPORT BitwuzlaTerm convert(const SharedAbstractNode &node, Bitwuzla *bzla)
Converts to Bitwuzla's AST.
TRITON_EXPORT const std::map< size_t, BitwuzlaSort > & getBitvectorSorts(void) const
Returns bitvector sorts.
TRITON_EXPORT ~TritonToBitwuzla()
Destructor.
TRITON_EXPORT const std::unordered_map< 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.
The exception class used by all AST lifting (e.g z3 <-> triton).
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
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,...
constexpr triton::uint32 byte
byte size in bit
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.