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