From d4ca816d7082d2286dae3d0eb88d6e15578602df Mon Sep 17 00:00:00 2001 From: Jonathan Salwan Date: Wed, 2 Feb 2022 15:21:47 +0100 Subject: [PATCH] Add a new class: LLVMToTriton (#1078) We also renamed some files: * src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp -> src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp * src/libtriton/ast/z3/tritonToZ3Ast.cpp -> src/libtriton/ast/z3/tritonToZ3.cpp * src/libtriton/ast/z3/z3ToTritonAst.cpp -> src/libtriton/ast/z3/z3ToTriton.cpp * src/libtriton/includes/triton/tritonToBitwuzlaAst.hpp -> src/libtriton/includes/triton/tritonToBitwuzla.hpp * src/libtriton/includes/triton/tritonToZ3Ast.hpp -> src/libtriton/includes/triton/tritonToZ3.hpp * src/libtriton/includes/triton/z3ToTritonAst.hpp -> src/libtriton/includes/triton/z3ToTriton.hpp As well as classes: * TritonToZ3Ast -> TritonToZ3 * Z3ToTritonAst -> Z3ToTriton * TritonToBitwuzlaAst -> TritonToBitwuzla --- README.md | 1 + src/examples/cpp/ctest_api.cpp | 114 ++++++++- src/libtriton/CMakeLists.txt | 14 +- ...ToBitwuzlaAst.cpp => tritonToBitwuzla.cpp} | 22 +- src/libtriton/ast/llvm/llvmToTriton.cpp | 221 ++++++++++++++++++ src/libtriton/ast/llvm/tritonToLLVM.cpp | 13 +- .../z3/{tritonToZ3Ast.cpp => tritonToZ3.cpp} | 36 +-- .../z3/{z3ToTritonAst.cpp => z3ToTriton.cpp} | 95 ++++---- .../bindings/python/objects/pyAstContext.cpp | 12 +- .../solver/bitwuzla/bitwuzlaSolver.cpp | 6 +- src/libtriton/engines/solver/z3/z3Solver.cpp | 14 +- .../includes/triton/liftingEngine.hpp | 1 + .../includes/triton/liftingToLLVM.hpp | 1 + .../includes/triton/liftingToPython.hpp | 1 + .../includes/triton/liftingToSMT.hpp | 1 + .../includes/triton/llvmToTriton.hpp | 68 ++++++ ...ToBitwuzlaAst.hpp => tritonToBitwuzla.hpp} | 14 +- .../includes/triton/tritonToLLVM.hpp | 6 +- .../{tritonToZ3Ast.hpp => tritonToZ3.hpp} | 14 +- .../{z3ToTritonAst.hpp => z3ToTriton.hpp} | 6 +- 20 files changed, 530 insertions(+), 130 deletions(-) rename src/libtriton/ast/bitwuzla/{tritonToBitwuzlaAst.cpp => tritonToBitwuzla.cpp} (92%) create mode 100644 src/libtriton/ast/llvm/llvmToTriton.cpp rename src/libtriton/ast/z3/{tritonToZ3Ast.cpp => tritonToZ3.cpp} (87%) rename src/libtriton/ast/z3/{z3ToTritonAst.cpp => z3ToTriton.cpp} (70%) create mode 100644 src/libtriton/includes/triton/llvmToTriton.hpp rename src/libtriton/includes/triton/{tritonToBitwuzlaAst.hpp => tritonToBitwuzla.hpp} (87%) rename src/libtriton/includes/triton/{tritonToZ3Ast.hpp => tritonToZ3.hpp} (87%) rename src/libtriton/includes/triton/{z3ToTritonAst.hpp => z3ToTriton.hpp} (87%) diff --git a/README.md b/README.md index 91d3ed4c3..b77b7a8fd 100644 --- a/README.md +++ b/README.md @@ -97,6 +97,7 @@ Triton relies on the following dependencies: * libcapstone >= 4.0.x https://github.com/capstone-engine/capstone * libz3 (optional) >= 4.6.0 https://github.com/Z3Prover/z3 * libbitwuzla (optional) n/a https://github.com/bitwuzla/bitwuzla +* llvm (optional) >= 12 ``` diff --git a/src/examples/cpp/ctest_api.cpp b/src/examples/cpp/ctest_api.cpp index b1b7a0c7f..2090a4675 100644 --- a/src/examples/cpp/ctest_api.cpp +++ b/src/examples/cpp/ctest_api.cpp @@ -2,9 +2,13 @@ #include #include +#include +#include +#include #include #include +#include #include #include #include @@ -14,8 +18,12 @@ #include #include #include -#include -#include + +#ifdef TRITON_LLVM_INTERFACE + #include + #include +#endif + int test_1(void) { @@ -469,8 +477,7 @@ int test_9(void) { api.setArchitecture(triton::arch::ARCH_X86_64); triton::engines::symbolic::PathConstraint pco; - auto node = api.getAstContext()->equal( - api.getAstContext()->bvtrue(), api.getAstContext()->bvtrue()); + auto node = api.getAstContext()->equal(api.getAstContext()->bvtrue(), api.getAstContext()->bvtrue()); pco.addBranchConstraint(false, 0x123, 0x100, node); pco.addBranchConstraint(true, 0x123, 0x200, node); pco.addBranchConstraint(false, 0x123, 0x300, node); @@ -517,6 +524,100 @@ int test_9(void) { } +#ifdef TRITON_LLVM_INTERFACE +bool smt_proof(triton::API& ctx, const triton::ast::SharedAbstractNode& node1, const triton::ast::SharedAbstractNode& node2) { + auto actx = ctx.getAstContext(); + if (ctx.isSat(actx->distinct(node1, node2)) == false) + return true; + return false; +} + + +int test_10(void) { + triton::API ctx(triton::arch::ARCH_X86_64); + auto actx = ctx.getAstContext(); + auto varx = ctx.newSymbolicVariable(8, "x"); + + std::list nodes = { + /* bitvector */ + actx->bvadd(actx->bv(10, 8), actx->variable(varx)), + actx->bvadd(actx->variable(varx), actx->bv(11, 8)), + actx->bvand(actx->bv(12, 8), actx->variable(varx)), + actx->bvashr(actx->bv(13, 8), actx->variable(varx)), + actx->bvlshr(actx->bv(14, 8), actx->variable(varx)), + actx->bvmul(actx->bv(15, 8), actx->variable(varx)), + actx->bvnand(actx->bv(16, 8), actx->variable(varx)), + actx->bvneg(actx->bv(17, 8)), + actx->bvneg(actx->variable(varx)), + actx->bvnor(actx->bv(18, 8), actx->variable(varx)), + actx->bvnot(actx->bv(19, 8)), + actx->bvnot(actx->variable(varx)), + actx->bvor(actx->bv(20, 8), actx->variable(varx)), + actx->bvrol(actx->variable(varx), actx->bv(21, 8)), + actx->bvror(actx->variable(varx), actx->bv(22, 8)), + actx->bvsdiv(actx->variable(varx), actx->bv(23, 8)), + actx->bvshl(actx->variable(varx), actx->bv(24, 8)), + actx->bvsmod(actx->variable(varx), actx->bv(25, 8)), + actx->bvsrem(actx->variable(varx), actx->bv(26, 8)), + actx->bvsub(actx->bv(27, 8), actx->variable(varx)), + actx->bvudiv(actx->variable(varx), actx->bv(28, 8)), + actx->bvurem(actx->variable(varx), actx->bv(29, 8)), + actx->bvxnor(actx->bv(30, 8), actx->variable(varx)), + actx->bvxor(actx->bv(31, 8), actx->variable(varx)), + actx->sx(24, actx->variable(varx)), + actx->sx(8, actx->variable(varx)), + actx->zx(24, actx->variable(varx)), + actx->zx(8, actx->variable(varx)), + + /* logical */ + actx->equal(actx->bv(32, 8), actx->variable(varx)), + actx->distinct(actx->bv(33, 8), actx->variable(varx)), + actx->bvsge(actx->bv(34, 8), actx->variable(varx)), + actx->bvsgt(actx->bv(35, 8), actx->variable(varx)), + actx->bvsle(actx->bv(36, 8), actx->variable(varx)), + actx->bvslt(actx->bv(37, 8), actx->variable(varx)), + actx->bvuge(actx->bv(38, 8), actx->variable(varx)), + actx->bvugt(actx->bv(39, 8), actx->variable(varx)), + actx->bvule(actx->bv(40, 8), actx->variable(varx)), + actx->land(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))), + actx->lor(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))), + actx->lxor(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))), + + /* misc */ + actx->concat(actx->concat(actx->concat(actx->bv(50, 8), actx->variable(varx)), actx->bv(0xff, 8)), actx->variable(varx)), + actx->extract(11, 4, actx->concat(actx->bv(0xff, 8), actx->variable(varx))), + actx->ite(actx->equal(actx->bv(52, 8), actx->bv(60, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(1, 8))), + actx->ite(actx->equal(actx->bv(53, 8), actx->bv(61, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(2, 8))), + actx->ite(actx->bvsge(actx->bv(54, 8), actx->bv(62, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(3, 8))), + actx->ite(actx->bvslt(actx->bv(55, 8), actx->variable(varx)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(4, 8))), + }; + + for (const auto& node : nodes) { + /* Triton to LLVM */ + llvm::LLVMContext llvmContext; + triton::ast::TritonToLLVM ttllvm(llvmContext); + auto llvmModule = ttllvm.convert(node); + std::cerr << "IN: " << node << std::endl; + + /* LLVM to Triton */ + triton::ast::LLVMToTriton llvmtt(actx); + auto nout = llvmtt.convert(llvmModule.get()); + std::cerr << "OUT: " << nout << std::endl; + + if (smt_proof(ctx, node, nout) == false) { + std::cerr << "Node not equal" << std::endl; + std::cerr << "IN: " << node << std::endl; + std::cerr << "OUT: " << nout << std::endl; + return 1; + } + } + + std::cout << "test_10: OK" << std::endl; + return 0; +} +#endif + + int main(int ac, const char **av) { if (test_1()) return 1; @@ -545,5 +646,10 @@ int main(int ac, const char **av) { if (test_9()) return 1; + #ifdef TRITON_LLVM_INTERFACE + if (test_10()) + return 1; + #endif + return 0; } diff --git a/src/libtriton/CMakeLists.txt b/src/libtriton/CMakeLists.txt index ee776db9e..8218e8083 100644 --- a/src/libtriton/CMakeLists.txt +++ b/src/libtriton/CMakeLists.txt @@ -99,6 +99,7 @@ set(LIBTRITON_HEADER_FILES includes/triton/liftingToLLVM.hpp includes/triton/liftingToPython.hpp includes/triton/liftingToSMT.hpp + includes/triton/llvmToTriton.hpp includes/triton/memoryAccess.hpp includes/triton/modes.hpp includes/triton/modesEnums.hpp @@ -121,9 +122,9 @@ set(LIBTRITON_HEADER_FILES includes/triton/synthesisResult.hpp includes/triton/synthesizer.hpp includes/triton/taintEngine.hpp - includes/triton/tritonToBitwuzlaAst.hpp + includes/triton/tritonToBitwuzla.hpp includes/triton/tritonToLLVM.hpp - includes/triton/tritonToZ3Ast.hpp + includes/triton/tritonToZ3.hpp includes/triton/tritonTypes.hpp includes/triton/x86.spec includes/triton/x8664Cpu.hpp @@ -131,7 +132,7 @@ set(LIBTRITON_HEADER_FILES includes/triton/x86Semantics.hpp includes/triton/x86Specifications.hpp includes/triton/z3Solver.hpp - includes/triton/z3ToTritonAst.hpp + includes/triton/z3ToTriton.hpp ) # Define all resource files @@ -142,8 +143,8 @@ set(LIBTRITON_RESOURCE_FILES if(Z3_INTERFACE) set(Z3_INTERFACE_SOURCE_FILES - ast/z3/tritonToZ3Ast.cpp - ast/z3/z3ToTritonAst.cpp + ast/z3/tritonToZ3.cpp + ast/z3/z3ToTriton.cpp engines/solver/z3/z3Solver.cpp ) else() @@ -152,7 +153,7 @@ endif() if(BITWUZLA_INTERFACE) set(BITWUZLA_INTERFACE_SOURCE_FILES - ast/bitwuzla/tritonToBitwuzlaAst.cpp + ast/bitwuzla/tritonToBitwuzla.cpp engines/solver/bitwuzla/bitwuzlaSolver.cpp ) else() @@ -161,6 +162,7 @@ endif() if(LLVM_INTERFACE) set(LLVM_INTERFACE_SOURCE_FILES + ast/llvm/llvmToTriton.cpp ast/llvm/tritonToLLVM.cpp engines/lifters/liftingToLLVM.cpp ) diff --git a/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp b/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp similarity index 92% rename from src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp rename to src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp index cffc5a756..20c740ebc 100644 --- a/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp +++ b/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp @@ -11,36 +11,36 @@ #include #include #include -#include +#include namespace triton { namespace ast { - TritonToBitwuzlaAst::TritonToBitwuzlaAst(bool eval) + TritonToBitwuzla::TritonToBitwuzla(bool eval) : isEval(eval) { } - TritonToBitwuzlaAst::~TritonToBitwuzlaAst() { + TritonToBitwuzla::~TritonToBitwuzla() { this->translatedNodes.clear(); this->variables.clear(); this->symbols.clear(); } - const std::unordered_map& TritonToBitwuzlaAst::getVariables(void) const { + const std::unordered_map& TritonToBitwuzla::getVariables(void) const { return this->variables; } - const std::map& TritonToBitwuzlaAst::getBitvectorSorts(void) const { + const std::map& TritonToBitwuzla::getBitvectorSorts(void) const { return this->bvSorts; } - const BitwuzlaTerm* TritonToBitwuzlaAst::convert(const SharedAbstractNode& node, Bitwuzla* bzla) { + const BitwuzlaTerm* TritonToBitwuzla::convert(const SharedAbstractNode& node, Bitwuzla* bzla) { auto nodes = childrenExtraction(node, true /* unroll*/, true /* revert */); for (auto&& n : nodes) { translatedNodes[n] = translate(n, bzla); @@ -49,9 +49,9 @@ namespace triton { } - const BitwuzlaTerm* TritonToBitwuzlaAst::translate(const SharedAbstractNode& node, Bitwuzla* bzla) { + const BitwuzlaTerm* TritonToBitwuzla::translate(const SharedAbstractNode& node, Bitwuzla* bzla) { if (node == nullptr) - throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): node cannot be null."); + throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): node cannot be null."); std::vector children; for (auto&& n : node->getChildren()) { @@ -186,7 +186,7 @@ namespace triton { } case FORALL_NODE: - throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062)."); + throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062)."); case IFF_NODE: return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_IFF, children[0], children[1]); @@ -225,7 +225,7 @@ namespace triton { auto it = symbols.find(value); if (it == symbols.end()) - throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): [STRING_NODE] Symbols not found."); + throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): [STRING_NODE] Symbols not found."); return translatedNodes.at(it->second); } @@ -265,7 +265,7 @@ namespace triton { } default: - throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): Invalid kind of node."); + throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): Invalid kind of node."); } } diff --git a/src/libtriton/ast/llvm/llvmToTriton.cpp b/src/libtriton/ast/llvm/llvmToTriton.cpp new file mode 100644 index 000000000..7a5be15c8 --- /dev/null +++ b/src/libtriton/ast/llvm/llvmToTriton.cpp @@ -0,0 +1,221 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#include +#include + + + +namespace triton { + namespace ast { + + LLVMToTriton::LLVMToTriton(const SharedAstContext& actx) + : actx(actx) { + } + + + triton::ast::SharedAbstractNode LLVMToTriton::do_convert(llvm::Value* value) { + llvm::Instruction* instruction = llvm::dyn_cast_or_null(value); + llvm::ConstantInt* constant = llvm::dyn_cast_or_null(value); + llvm::Argument* argument = llvm::dyn_cast_or_null(value); + llvm::ICmpInst* icmp = llvm::dyn_cast_or_null(value); + + if (instruction != nullptr) { + switch (instruction->getOpcode()) { + + case llvm::Instruction::AShr: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvashr(LHS, RHS); + } + + case llvm::Instruction::Add: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvadd(LHS, RHS); + } + + case llvm::Instruction::And: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + /* LLVM does not distinct a logical AND of the bitwise AND */ + if (LHS->isLogical() && RHS->isLogical()) { + return this->actx->ite(this->actx->land(LHS, RHS), this->actx->bvtrue(), this->actx->bvfalse()); + } + return this->actx->bvand(LHS, RHS); + } + + case llvm::Instruction::ICmp: { + triton::ast::SharedAbstractNode node = nullptr; + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + if (icmp != nullptr) { + switch (icmp->getPredicate()) { + case llvm::ICmpInst::ICMP_EQ: return this->actx->equal(LHS, RHS); + case llvm::ICmpInst::ICMP_NE: return this->actx->distinct(LHS, RHS); + case llvm::ICmpInst::ICMP_UGE: return this->actx->bvuge(LHS, RHS); + case llvm::ICmpInst::ICMP_UGT: return this->actx->bvugt(LHS, RHS); + case llvm::ICmpInst::ICMP_ULE: return this->actx->bvule(LHS, RHS); + case llvm::ICmpInst::ICMP_ULT: return this->actx->bvult(LHS, RHS); + case llvm::ICmpInst::ICMP_SGE: return this->actx->bvsge(LHS, RHS); + case llvm::ICmpInst::ICMP_SGT: return this->actx->bvsgt(LHS, RHS); + case llvm::ICmpInst::ICMP_SLE: return this->actx->bvsle(LHS, RHS); + case llvm::ICmpInst::ICMP_SLT: return this->actx->bvslt(LHS, RHS); + default: + break; + } + return node; + } + throw triton::exceptions::AstLifting("LLVMToTriton::do_convert(): ICmpInst not supported"); + } + + case llvm::Instruction::LShr: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvlshr(LHS, RHS); + } + + case llvm::Instruction::Mul: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvmul(LHS, RHS); + } + + case llvm::Instruction::Or: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + /* LLVM does not distinct a logical OR of the bitwise OR */ + if (LHS->isLogical() && RHS->isLogical()) { + return this->actx->ite(this->actx->lor(LHS, RHS), this->actx->bvtrue(), this->actx->bvfalse()); + } + return this->actx->bvor(LHS, RHS); + } + + case llvm::Instruction::Ret: + return this->do_convert(instruction->getOperand(0)); + + case llvm::Instruction::SDiv: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvsdiv(LHS, RHS); + } + + case llvm::Instruction::SExt: { + /* Final size */ + auto size = instruction->getType()->getIntegerBitWidth(); + auto node = this->do_convert(instruction->getOperand(0)); + /* Size of the child */ + auto csze = instruction->getOperand(0)->getType()->getIntegerBitWidth(); + return this->actx->sx(size - csze, node); + } + + case llvm::Instruction::SRem: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvsrem(LHS, RHS); + } + + case llvm::Instruction::Select: { + auto nif = this->do_convert(instruction->getOperand(0)); + auto nthen = this->do_convert(instruction->getOperand(1)); + auto nelse = this->do_convert(instruction->getOperand(2)); + + /* + * In some cases, LLVM simplifies the icmp by a constant + * which is lifted to a bvtrue on our side. In this case, + * we have to translate it to a logical node. + */ + if (nif->isLogical() == false) { + nif = this->actx->equal(nif, this->actx->bvtrue()); + } + + return this->actx->ite(nif, nthen, nelse); + } + + case llvm::Instruction::Shl: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvshl(LHS, RHS); + } + + case llvm::Instruction::Sub: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvsub(LHS, RHS); + } + + case llvm::Instruction::Trunc: { + auto size = instruction->getType()->getIntegerBitWidth(); + auto node = this->do_convert(instruction->getOperand(0)); + return this->actx->extract(size - 1, 0, node); + } + + case llvm::Instruction::UDiv: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvudiv(LHS, RHS); + } + + case llvm::Instruction::URem: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + return this->actx->bvurem(LHS, RHS); + } + + case llvm::Instruction::Xor: { + auto LHS = this->do_convert(instruction->getOperand(0)); + auto RHS = this->do_convert(instruction->getOperand(1)); + /* LLVM does not distinct a logical XOR of the bitwise XOR */ + if (LHS->isLogical() && RHS->isLogical()) { + return this->actx->ite(this->actx->lxor(LHS, RHS), this->actx->bvtrue(), this->actx->bvfalse()); + } + return this->actx->bvxor(LHS, RHS); + } + + case llvm::Instruction::ZExt: { + /* Final size */ + auto size = instruction->getType()->getIntegerBitWidth(); + auto node = this->do_convert(instruction->getOperand(0)); + /* Size of the child */ + auto csze = instruction->getOperand(0)->getType()->getIntegerBitWidth(); + return this->actx->zx(size - csze, node); + } + + default: + throw triton::exceptions::AstLifting("LLVMToTriton::do_convert(): LLVM instruction not supported"); + } + } + else if (constant != nullptr) { + return this->actx->bv(constant->getLimitedValue(), constant->getBitWidth()); + } + else if (argument != nullptr) { + return this->actx->getVariableNode(argument->getName().data()); + } + + throw triton::exceptions::AstLifting("LLVMToTriton::do_convert(): LLVM instruction not supported"); + } + + + SharedAbstractNode LLVMToTriton::convert(llvm::Module* llvmModule, const std::string& fname) { + /* Check if the given llvm::module contains the __triton function */ + llvm::Function* function = llvmModule->getFunction(fname); + if (function == nullptr) { + throw triton::exceptions::AstLifting("LLVMToTriton::convert(): llvm::Module doesn't contain the fiven function name"); + } + + /* Get the entry block of the function */ + llvm::BasicBlock& entryBlock = function->getEntryBlock(); + + /* Get the return of the function */ + llvm::Instruction* returnInstruction = entryBlock.getTerminator(); + + /* Let's convert everything */ + return this->do_convert(returnInstruction); + } + + }; /* ast namespace */ +}; /* triton namespace */ diff --git a/src/libtriton/ast/llvm/tritonToLLVM.cpp b/src/libtriton/ast/llvm/tritonToLLVM.cpp index ab5c8637f..b89010928 100644 --- a/src/libtriton/ast/llvm/tritonToLLVM.cpp +++ b/src/libtriton/ast/llvm/tritonToLLVM.cpp @@ -31,7 +31,7 @@ namespace triton { } - void TritonToLLVM::createFunction(const triton::ast::SharedAbstractNode& node) { + void TritonToLLVM::createFunction(const triton::ast::SharedAbstractNode& node, const std::string& fname) { // Collect used symbolic variables. auto vars = triton::ast::search(node, triton::ast::VARIABLE_NODE); @@ -61,17 +61,14 @@ namespace triton { auto retSize = node->getBitvectorSize(); auto* retType = llvm::IntegerType::get(this->llvmContext, retSize); auto* funcType = llvm::FunctionType::get(retType, argsType, false /* isVarArg */); - auto* llvmFunc = llvm::Function::Create(funcType, llvm::Function::ExternalLinkage, "__triton", this->llvmModule.get()); + auto* llvmFunc = llvm::Function::Create(funcType, llvm::Function::ExternalLinkage, fname, this->llvmModule.get()); /* Rename parameters */ llvm::Function::arg_iterator params = llvmFunc->arg_begin(); for (const auto& node : vars) { auto var = reinterpret_cast(node.get())->getSymbolicVariable(); auto* param = params++; - if (var->getAlias().empty()) - param->setName(var->getName()); - else - param->setName(var->getAlias()); + param->setName(var->getName()); this->llvmVars[node] = param; } @@ -81,11 +78,11 @@ namespace triton { } - std::shared_ptr TritonToLLVM::convert(const triton::ast::SharedAbstractNode& node) { + std::shared_ptr TritonToLLVM::convert(const triton::ast::SharedAbstractNode& node, const std::string& fname) { std::unordered_map results; /* Create the LLVM function */ - this->createFunction(node); + this->createFunction(node, fname); /* Lift Triton AST to LLVM IR */ auto nodes = triton::ast::childrenExtraction(node, true /* unroll*/, true /* revert */); diff --git a/src/libtriton/ast/z3/tritonToZ3Ast.cpp b/src/libtriton/ast/z3/tritonToZ3.cpp similarity index 87% rename from src/libtriton/ast/z3/tritonToZ3Ast.cpp rename to src/libtriton/ast/z3/tritonToZ3.cpp index e544dff7e..38e6f3def 100644 --- a/src/libtriton/ast/z3/tritonToZ3Ast.cpp +++ b/src/libtriton/ast/z3/tritonToZ3.cpp @@ -11,29 +11,29 @@ #include #include #include -#include +#include namespace triton { namespace ast { - TritonToZ3Ast::TritonToZ3Ast(bool eval) + TritonToZ3::TritonToZ3(bool eval) : context() { this->isEval = eval; } - TritonToZ3Ast::~TritonToZ3Ast() { + TritonToZ3::~TritonToZ3() { /* See #828: Release ownership before calling container destructor */ this->symbols.clear(); this->variables.clear(); } - triton::__uint TritonToZ3Ast::getUintValue(const z3::expr& expr) { + triton::__uint TritonToZ3::getUintValue(const z3::expr& expr) { if (!expr.is_int()) - throw triton::exceptions::AstLifting("TritonToZ3Ast::getUintValue(): The ast is not a numerical value."); + throw triton::exceptions::AstLifting("TritonToZ3::getUintValue(): The ast is not a numerical value."); #if defined(__x86_64__) || defined(_M_X64) || defined(__aarch64__) return expr.get_numeral_uint64(); @@ -44,12 +44,12 @@ namespace triton { } - std::string TritonToZ3Ast::getStringValue(const z3::expr& expr) { + std::string TritonToZ3::getStringValue(const z3::expr& expr) { return Z3_get_numeral_string(this->context, expr); } - z3::expr TritonToZ3Ast::convert(const triton::ast::SharedAbstractNode& node) { + z3::expr TritonToZ3::convert(const triton::ast::SharedAbstractNode& node) { std::unordered_map results; auto nodes = triton::ast::childrenExtraction(node, true /* unroll*/, true /* revert */); @@ -62,9 +62,9 @@ namespace triton { } - z3::expr TritonToZ3Ast::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results) { + z3::expr TritonToZ3::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results) { if (node == nullptr) - throw triton::exceptions::AstLifting("TritonToZ3Ast::do_convert(): node cannot be null."); + throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): node cannot be null."); /* Prepare z3's children */ std::vector children; @@ -241,14 +241,14 @@ namespace triton { case LAND_NODE: { z3::expr currentValue = children[0]; if (!currentValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LandNode(): Land can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LandNode(): Land can be apply only on bool value."); } z3::expr nextValue(this->context); for (triton::uint32 idx = 1; idx < children.size(); idx++) { nextValue = children[idx]; if (!nextValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LandNode(): Land can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LandNode(): Land can be apply only on bool value."); } Z3_ast ops[] = {currentValue, nextValue}; currentValue = to_expr(this->context, Z3_mk_and(this->context, 2, ops)); @@ -267,7 +267,7 @@ namespace triton { case LNOT_NODE: { z3::expr value = children[0]; if (!value.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LnotNode(): Lnot can be apply only on bool value."); } return to_expr(this->context, Z3_mk_not(this->context, value)); } @@ -275,14 +275,14 @@ namespace triton { case LOR_NODE: { z3::expr currentValue = children[0]; if (!currentValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LnotNode(): Lnot can be apply only on bool value."); } z3::expr nextValue(this->context); for (triton::uint32 idx = 1; idx < children.size(); idx++) { nextValue = children[idx]; if (!nextValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LnotNode(): Lnot can be apply only on bool value."); } Z3_ast ops[] = {currentValue, nextValue}; currentValue = to_expr(this->context, Z3_mk_or(this->context, 2, ops)); @@ -294,14 +294,14 @@ namespace triton { case LXOR_NODE: { z3::expr currentValue = children[0]; if (!currentValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LxorNode(): Lxor can be applied only on bool value."); } z3::expr nextValue(this->context); for (triton::uint32 idx = 1; idx < children.size(); idx++) { nextValue = children[idx]; if (!nextValue.get_sort().is_bool()) { - throw triton::exceptions::AstLifting("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3::LxorNode(): Lxor can be applied only on bool value."); } currentValue = to_expr(this->context, Z3_mk_xor(this->context, currentValue, nextValue)); } @@ -316,7 +316,7 @@ namespace triton { std::string value = reinterpret_cast(node.get())->getString(); if (this->symbols.find(value) == this->symbols.end()) - throw triton::exceptions::AstLifting("TritonToZ3Ast::do_convert(): [STRING_NODE] Symbols not found."); + throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): [STRING_NODE] Symbols not found."); return results->at(this->symbols[value]); } @@ -355,7 +355,7 @@ namespace triton { } default: - throw triton::exceptions::AstLifting("TritonToZ3Ast::do_convert(): Invalid kind of node."); + throw triton::exceptions::AstLifting("TritonToZ3::do_convert(): Invalid kind of node."); } } diff --git a/src/libtriton/ast/z3/z3ToTritonAst.cpp b/src/libtriton/ast/z3/z3ToTriton.cpp similarity index 70% rename from src/libtriton/ast/z3/z3ToTritonAst.cpp rename to src/libtriton/ast/z3/z3ToTriton.cpp index 732de3cdc..bb69d4319 100644 --- a/src/libtriton/ast/z3/z3ToTritonAst.cpp +++ b/src/libtriton/ast/z3/z3ToTriton.cpp @@ -9,27 +9,27 @@ #include #include -#include +#include namespace triton { namespace ast { - Z3ToTritonAst::Z3ToTritonAst(const SharedAstContext& astCtxt) + Z3ToTriton::Z3ToTriton(const SharedAstContext& astCtxt) : astCtxt(astCtxt) { } - SharedAbstractNode Z3ToTritonAst::convert(const z3::expr& expr) { + SharedAbstractNode Z3ToTriton::convert(const z3::expr& expr) { SharedAbstractNode node = nullptr; /* Currently, only support application node (TODO) */ if (expr.is_quantifier()) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Quantifier not supported yet."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Quantifier not supported yet."); if (!expr.is_app()) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): At this moment only application are supported."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): At this moment only application are supported."); /* Get the function declaration */ z3::func_decl function = expr.decl(); @@ -39,14 +39,14 @@ namespace triton { case Z3_OP_EQ: { if (expr.num_args() != 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_EQ must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_EQ must contain two arguments."); node = this->astCtxt->equal(this->convert(expr.arg(0)), this->convert(expr.arg(1))); break; } case Z3_OP_DISTINCT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_DISTINCT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_DISTINCT must contain at least two arguments."); node = this->astCtxt->distinct(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->distinct(node, this->convert(expr.arg(i))); @@ -55,21 +55,21 @@ namespace triton { case Z3_OP_IFF: { if (expr.num_args() != 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_IFF must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_IFF must contain two arguments."); node = this->astCtxt->iff(this->convert(expr.arg(0)), this->convert(expr.arg(1))); break; } case Z3_OP_ITE: { if (expr.num_args() != 3) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ITE must contain three arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ITE must contain three arguments."); node = this->astCtxt->ite(this->convert(expr.arg(0)), this->convert(expr.arg(1)), this->convert(expr.arg(2))); break; } case Z3_OP_AND: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_AND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_AND must contain at least two arguments."); std::vector args; for (triton::uint32 i = 0; i < expr.num_args(); i++) { @@ -82,7 +82,7 @@ namespace triton { case Z3_OP_OR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_OR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_OR must contain at least two arguments."); std::vector args; for (triton::uint32 i = 0; i < expr.num_args(); i++) { @@ -95,14 +95,14 @@ namespace triton { case Z3_OP_XOR: { if (expr.num_args() != 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_XOR must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_XOR must contain two arguments."); node = this->astCtxt->lxor(this->convert(expr.arg(0)), this->convert(expr.arg(1))); break; } case Z3_OP_NOT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_NOT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_NOT must contain one argument."); node = this->astCtxt->lnot(this->convert(expr.arg(0))); break; } @@ -116,14 +116,14 @@ namespace triton { case Z3_OP_BNEG: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BNEG must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNEG must contain one argument."); node = this->astCtxt->bvneg(this->convert(expr.arg(0))); break; } case Z3_OP_BADD: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BADD must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BADD must contain at least two arguments."); node = this->astCtxt->bvadd(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvadd(node, this->convert(expr.arg(i))); @@ -132,7 +132,7 @@ namespace triton { case Z3_OP_BSUB: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BSUB must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSUB must contain at least two arguments."); node = this->astCtxt->bvsub(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsub(node, this->convert(expr.arg(i))); @@ -141,7 +141,7 @@ namespace triton { case Z3_OP_BMUL: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BMUL must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BMUL must contain at least two arguments."); node = this->astCtxt->bvmul(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvmul(node, this->convert(expr.arg(i))); @@ -151,7 +151,7 @@ namespace triton { case Z3_OP_BSDIV_I: case Z3_OP_BSDIV: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BSDIV must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSDIV must contain at least two arguments."); node = this->astCtxt->bvsdiv(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsdiv(node, this->convert(expr.arg(i))); @@ -161,7 +161,7 @@ namespace triton { case Z3_OP_BUDIV_I: case Z3_OP_BUDIV: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BUDIV must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BUDIV must contain at least two arguments."); node = this->astCtxt->bvudiv(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvudiv(node, this->convert(expr.arg(i))); @@ -171,7 +171,7 @@ namespace triton { case Z3_OP_BSREM_I: case Z3_OP_BSREM: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BSREM must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSREM must contain at least two arguments."); node = this->astCtxt->bvsrem(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsrem(node, this->convert(expr.arg(i))); @@ -181,7 +181,7 @@ namespace triton { case Z3_OP_BUREM_I: case Z3_OP_BUREM: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BUREM must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BUREM must contain at least two arguments."); node = this->astCtxt->bvurem(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvurem(node, this->convert(expr.arg(i))); @@ -191,7 +191,7 @@ namespace triton { case Z3_OP_BSMOD_I: case Z3_OP_BSMOD: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BSMOD must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSMOD must contain at least two arguments."); node = this->astCtxt->bvsmod(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsmod(node, this->convert(expr.arg(i))); @@ -200,7 +200,7 @@ namespace triton { case Z3_OP_ULEQ: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ULEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ULEQ must contain at least two arguments."); node = this->astCtxt->bvule(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvule(node, this->convert(expr.arg(i))); @@ -209,7 +209,7 @@ namespace triton { case Z3_OP_SLEQ: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SLEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SLEQ must contain at least two arguments."); node = this->astCtxt->bvsle(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsle(node, this->convert(expr.arg(i))); @@ -218,7 +218,7 @@ namespace triton { case Z3_OP_UGEQ: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_UGEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_UGEQ must contain at least two arguments."); node = this->astCtxt->bvuge(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvuge(node, this->convert(expr.arg(i))); @@ -227,7 +227,7 @@ namespace triton { case Z3_OP_SGEQ: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SGEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SGEQ must contain at least two arguments."); node = this->astCtxt->bvsge(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsge(node, this->convert(expr.arg(i))); @@ -236,7 +236,7 @@ namespace triton { case Z3_OP_ULT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ULT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ULT must contain at least two arguments."); node = this->astCtxt->bvult(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvult(node, this->convert(expr.arg(i))); @@ -245,7 +245,7 @@ namespace triton { case Z3_OP_SLT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SLT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SLT must contain at least two arguments."); node = this->astCtxt->bvslt(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvslt(node, this->convert(expr.arg(i))); @@ -254,7 +254,7 @@ namespace triton { case Z3_OP_UGT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_UGT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_UGT must contain at least two arguments."); node = this->astCtxt->bvugt(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvugt(node, this->convert(expr.arg(i))); @@ -263,7 +263,7 @@ namespace triton { case Z3_OP_SGT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SGT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SGT must contain at least two arguments."); node = this->astCtxt->bvsgt(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvsgt(node, this->convert(expr.arg(i))); @@ -272,7 +272,7 @@ namespace triton { case Z3_OP_BAND: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BAND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BAND must contain at least two arguments."); node = this->astCtxt->bvand(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvand(node, this->convert(expr.arg(i))); @@ -281,7 +281,7 @@ namespace triton { case Z3_OP_BOR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BOR must contain at least two arguments."); node = this->astCtxt->bvor(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvor(node, this->convert(expr.arg(i))); @@ -290,14 +290,14 @@ namespace triton { case Z3_OP_BNOT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BNOT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNOT must contain one argument."); node = this->astCtxt->bvnot(this->convert(expr.arg(0))); break; } case Z3_OP_BXOR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BXOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BXOR must contain at least two arguments."); node = this->astCtxt->bvxor(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvxor(node, this->convert(expr.arg(i))); @@ -306,7 +306,7 @@ namespace triton { case Z3_OP_BNAND: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BNAND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNAND must contain at least two arguments."); node = this->astCtxt->bvnand(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvnand(node, this->convert(expr.arg(i))); @@ -315,7 +315,7 @@ namespace triton { case Z3_OP_BNOR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BNOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BNOR must contain at least two arguments."); node = this->astCtxt->bvnor(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvnor(node, this->convert(expr.arg(i))); @@ -324,7 +324,7 @@ namespace triton { case Z3_OP_BXNOR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BXNOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BXNOR must contain at least two arguments."); node = this->astCtxt->bvxnor(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvxnor(node, this->convert(expr.arg(i))); @@ -333,7 +333,7 @@ namespace triton { case Z3_OP_CONCAT: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_CONCAT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_CONCAT must contain at least two arguments."); std::vector args; for (triton::uint32 i = 0; i < expr.num_args(); i++) { @@ -346,28 +346,28 @@ namespace triton { case Z3_OP_SIGN_EXT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_SIGN_EXT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_SIGN_EXT must contain one argument."); node = this->astCtxt->sx(expr.hi(), this->convert(expr.arg(0))); break; } case Z3_OP_ZERO_EXT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ZERO_EXT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ZERO_EXT must contain one argument."); node = this->astCtxt->zx(expr.hi(), this->convert(expr.arg(0))); break; } case Z3_OP_EXTRACT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_EXTRACT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_EXTRACT must contain one argument."); node = this->astCtxt->extract(expr.hi(), expr.lo(), this->convert(expr.arg(0))); break; } case Z3_OP_BSHL: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BSHL must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BSHL must contain at least two arguments."); node = this->astCtxt->bvshl(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvshl(node, this->convert(expr.arg(i))); @@ -376,7 +376,7 @@ namespace triton { case Z3_OP_BLSHR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BLSHR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BLSHR must contain at least two arguments."); node = this->astCtxt->bvlshr(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvlshr(node, this->convert(expr.arg(i))); @@ -385,7 +385,7 @@ namespace triton { case Z3_OP_BASHR: { if (expr.num_args() < 2) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_BASHR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_BASHR must contain at least two arguments."); node = this->astCtxt->bvashr(this->convert(expr.arg(0)), this->convert(expr.arg(1))); for (triton::uint32 i = 2; i < expr.num_args(); i++) node = this->astCtxt->bvashr(node, this->convert(expr.arg(i))); @@ -394,14 +394,14 @@ namespace triton { case Z3_OP_ROTATE_LEFT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ROTATE_LEFT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ROTATE_LEFT must contain one argument."); node = this->astCtxt->bvrol(this->convert(expr.arg(0)), expr.hi()); break; } case Z3_OP_ROTATE_RIGHT: { if (expr.num_args() != 1) - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ROTATE_RIGHT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): Z3_OP_ROTATE_RIGHT must contain one argument."); node = this->astCtxt->bvror(this->convert(expr.arg(0)), expr.hi()); break; } @@ -430,12 +430,11 @@ namespace triton { } default: - throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): '" + function.name().str() + "' AST node not supported yet"); + throw triton::exceptions::AstLifting("Z3ToTriton::visit(): '" + function.name().str() + "' AST node not supported yet"); } return node; } - }; /* ast namespace */ }; /* triton namespace */ diff --git a/src/libtriton/bindings/python/objects/pyAstContext.cpp b/src/libtriton/bindings/python/objects/pyAstContext.cpp index 1b0b422c8..4f18231a4 100644 --- a/src/libtriton/bindings/python/objects/pyAstContext.cpp +++ b/src/libtriton/bindings/python/objects/pyAstContext.cpp @@ -13,8 +13,8 @@ #include #include #ifdef TRITON_Z3_INTERFACE - #include - #include + #include + #include #endif #include @@ -1581,7 +1581,7 @@ namespace triton { #ifdef TRITON_Z3_INTERFACE static PyObject* AstContext_tritonToZ3(PyObject* self, PyObject* node) { - triton::ast::TritonToZ3Ast tritonToZ3Ast{false}; + triton::ast::TritonToZ3 tritonToZ3{false}; if (node == nullptr || (!PyAstNode_Check(node))) return PyErr_Format(PyExc_TypeError, "tritonToZ3(): Expects a AstNode as argument."); @@ -1601,7 +1601,7 @@ namespace triton { // Convert the node to a Z3++ expression and translate it into // python's z3 main context - z3::expr expr = tritonToZ3Ast.convert(PyAstNode_AsAstNode(node)); + z3::expr expr = tritonToZ3.convert(PyAstNode_AsAstNode(node)); Z3_ast ast = Z3_translate(expr.ctx(), expr, z3Ctx); // Check that everything went fine @@ -1632,8 +1632,8 @@ namespace triton { static PyObject* AstContext_z3ToTriton(PyObject* self, PyObject* expr) { - triton::ast::Z3ToTritonAst z3ToTritonAst{PyAstContext_AsAstContext(self)}; - z3::context z3Ctx; + triton::ast::Z3ToTriton z3ToTritonAst{PyAstContext_AsAstContext(self)}; + z3::context z3Ctx; if (std::strcmp(Py_TYPE(expr)->tp_name, "ExprRef") && std::strcmp(Py_TYPE(expr)->tp_name, "BitVecRef")) return PyErr_Format(PyExc_TypeError, "z3ToTriton(): expected an ExprRef as argument"); diff --git a/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp b/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp index 6ff3f2baa..99d06d6f9 100644 --- a/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp +++ b/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp @@ -15,7 +15,7 @@ #include #include #include -#include +#include #include @@ -106,7 +106,7 @@ namespace triton { } // Convert Triton' AST to solver terms. - auto bzlaAst = triton::ast::TritonToBitwuzlaAst(); + auto bzlaAst = triton::ast::TritonToBitwuzla(); bitwuzla_assert(bzla, bzlaAst.convert(node, bzla)); // Set solving params. @@ -223,7 +223,7 @@ namespace triton { } // Evaluate concrete AST in solver. - auto bzlaAst = triton::ast::TritonToBitwuzlaAst(true); + auto bzlaAst = triton::ast::TritonToBitwuzla(true); auto bv_value = bitwuzla_get_bv_value(bzla, bitwuzla_get_value(bzla, bzlaAst.convert(node, bzla))); auto res = this->fromBvalueToUint512(bv_value); diff --git a/src/libtriton/engines/solver/z3/z3Solver.cpp b/src/libtriton/engines/solver/z3/z3Solver.cpp index c64b767af..d64b54aff 100644 --- a/src/libtriton/engines/solver/z3/z3Solver.cpp +++ b/src/libtriton/engines/solver/z3/z3Solver.cpp @@ -12,10 +12,10 @@ #include #include #include -#include +#include #include #include -#include +#include @@ -42,7 +42,7 @@ namespace triton { std::vector> Z3Solver::getModels(const triton::ast::SharedAbstractNode& node, triton::uint32 limit, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const { std::vector> ret; triton::ast::SharedAbstractNode onode = node; - triton::ast::TritonToZ3Ast z3Ast{false}; + triton::ast::TritonToZ3 z3Ast{false}; try { if (onode == nullptr) @@ -166,7 +166,7 @@ namespace triton { bool Z3Solver::isSat(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const { - triton::ast::TritonToZ3Ast z3Ast{false}; + triton::ast::TritonToZ3 z3Ast{false}; if (node == nullptr) throw triton::exceptions::SolverEngine("Z3Solver::isSat(): node cannot be null."); @@ -242,8 +242,8 @@ namespace triton { throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null."); try { - triton::ast::TritonToZ3Ast z3Ast{false}; - triton::ast::Z3ToTritonAst tritonAst{node->getContext()}; + triton::ast::TritonToZ3 z3Ast{false}; + triton::ast::Z3ToTriton tritonAst{node->getContext()}; /* From Triton to Z3 */ z3::expr expr = z3Ast.convert(node); @@ -264,7 +264,7 @@ namespace triton { throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null."); try { - triton::ast::TritonToZ3Ast z3ast{true}; + triton::ast::TritonToZ3 z3ast{true}; /* From Triton to Z3 */ z3::expr expr = z3ast.convert(node); diff --git a/src/libtriton/includes/triton/liftingEngine.hpp b/src/libtriton/includes/triton/liftingEngine.hpp index 9b78bd56e..ecebe4ad9 100644 --- a/src/libtriton/includes/triton/liftingEngine.hpp +++ b/src/libtriton/includes/triton/liftingEngine.hpp @@ -10,6 +10,7 @@ #include #include +#include #include #include #include diff --git a/src/libtriton/includes/triton/liftingToLLVM.hpp b/src/libtriton/includes/triton/liftingToLLVM.hpp index 202df8cf1..35162c95c 100644 --- a/src/libtriton/includes/triton/liftingToLLVM.hpp +++ b/src/libtriton/includes/triton/liftingToLLVM.hpp @@ -13,6 +13,7 @@ #include #include +#include #include #include diff --git a/src/libtriton/includes/triton/liftingToPython.hpp b/src/libtriton/includes/triton/liftingToPython.hpp index c0d25158f..2d490eea2 100644 --- a/src/libtriton/includes/triton/liftingToPython.hpp +++ b/src/libtriton/includes/triton/liftingToPython.hpp @@ -11,6 +11,7 @@ #include #include +#include #include #include diff --git a/src/libtriton/includes/triton/liftingToSMT.hpp b/src/libtriton/includes/triton/liftingToSMT.hpp index aa67cbb77..694c1183d 100644 --- a/src/libtriton/includes/triton/liftingToSMT.hpp +++ b/src/libtriton/includes/triton/liftingToSMT.hpp @@ -11,6 +11,7 @@ #include #include +#include #include #include diff --git a/src/libtriton/includes/triton/llvmToTriton.hpp b/src/libtriton/includes/triton/llvmToTriton.hpp new file mode 100644 index 000000000..e17193ba0 --- /dev/null +++ b/src/libtriton/includes/triton/llvmToTriton.hpp @@ -0,0 +1,68 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ +// + +#ifndef TRITON_LLVMTOTRITON_HPP +#define TRITON_LLVMTOTRITON_HPP + +#include +#include +#include + +#include +#include +#include +#include + +#include +#include +#include + + + +//! The Triton namespace +namespace triton { +/*! + * \addtogroup triton + * @{ + */ + + //! The AST namespace + namespace ast { + /*! + * \ingroup triton + * \addtogroup ast + * @{ + */ + + //! \class LLVMToTriton + /*! \brief Converts a LLVM IR to a Triton AST. */ + class LLVMToTriton { + private: + //! The Triton AST context + triton::ast::SharedAstContext actx; + + //! Map of triton symbolic variables + std::map symvars; + + //! Converts nodes + triton::ast::SharedAbstractNode do_convert(llvm::Value* llvmnode); + + public: + //! Constructor. + TRITON_EXPORT LLVMToTriton(const triton::ast::SharedAstContext& ctxt); + + //! Converts to Triton's AST + TRITON_EXPORT triton::ast::SharedAbstractNode convert(llvm::Module* llvmModule, const std::string& fname="__triton"); + }; + + /*! @} End of ast namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* TRITON_LLVMTOTRITON_HPP */ diff --git a/src/libtriton/includes/triton/tritonToBitwuzlaAst.hpp b/src/libtriton/includes/triton/tritonToBitwuzla.hpp similarity index 87% rename from src/libtriton/includes/triton/tritonToBitwuzlaAst.hpp rename to src/libtriton/includes/triton/tritonToBitwuzla.hpp index 61f55d48f..580ea999d 100644 --- a/src/libtriton/includes/triton/tritonToBitwuzlaAst.hpp +++ b/src/libtriton/includes/triton/tritonToBitwuzla.hpp @@ -5,8 +5,8 @@ ** This program is under the terms of the Apache License 2.0. */ -#ifndef TRITON_TRITONTOBITWUZLAAST_H -#define TRITON_TRITONTOBITWUZLAAST_H +#ifndef TRITON_TRITONTOBITWUZLA_H +#define TRITON_TRITONTOBITWUZLA_H #include #include @@ -34,15 +34,15 @@ namespace triton { * @{ */ - //! \class TritonToBitwuzlaAst + //! \class TritonToBitwuzla /*! \brief Converts a Triton's AST to Bitwuzla's AST. */ - class TritonToBitwuzlaAst { + class TritonToBitwuzla { public: //! Constructor. - TRITON_EXPORT TritonToBitwuzlaAst(bool eval=false); + TRITON_EXPORT TritonToBitwuzla(bool eval=false); //! Destructor. - TRITON_EXPORT ~TritonToBitwuzlaAst(); + TRITON_EXPORT ~TritonToBitwuzla(); //! Converts to Bitwuzla's AST TRITON_EXPORT const BitwuzlaTerm* convert(const SharedAbstractNode& node, Bitwuzla* bzla); @@ -78,4 +78,4 @@ namespace triton { /*! @} End of triton namespace */ }; -#endif /* TRITON_TRITONTOBITWUZLAAST_H */ +#endif /* TRITON_TRITONTOBITWUZLA_H */ diff --git a/src/libtriton/includes/triton/tritonToLLVM.hpp b/src/libtriton/includes/triton/tritonToLLVM.hpp index 09f2c7e81..6bda40df1 100644 --- a/src/libtriton/includes/triton/tritonToLLVM.hpp +++ b/src/libtriton/includes/triton/tritonToLLVM.hpp @@ -11,9 +11,11 @@ #include #include #include +#include #include #include +#include #include #include @@ -53,7 +55,7 @@ namespace triton { std::map llvmVars; //! Create a LLVM function - void createFunction(const triton::ast::SharedAbstractNode& node); + void createFunction(const triton::ast::SharedAbstractNode& node, const std::string& fname); //! Converts Triton AST to LLVM IR llvm::Value* do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results); @@ -63,7 +65,7 @@ namespace triton { TRITON_EXPORT TritonToLLVM(llvm::LLVMContext& llvmContext); //! Lifts a symbolic expression and all its references to LLVM format. - TRITON_EXPORT std::shared_ptr convert(const triton::ast::SharedAbstractNode& node); + TRITON_EXPORT std::shared_ptr convert(const triton::ast::SharedAbstractNode& node, const std::string& fname="__triton"); }; /*! @} End of ast namespace */ diff --git a/src/libtriton/includes/triton/tritonToZ3Ast.hpp b/src/libtriton/includes/triton/tritonToZ3.hpp similarity index 87% rename from src/libtriton/includes/triton/tritonToZ3Ast.hpp rename to src/libtriton/includes/triton/tritonToZ3.hpp index 9b3923ef2..c4cda3444 100644 --- a/src/libtriton/includes/triton/tritonToZ3Ast.hpp +++ b/src/libtriton/includes/triton/tritonToZ3.hpp @@ -5,8 +5,8 @@ ** This program is under the terms of the Apache License 2.0. */ -#ifndef TRITON_TRITONTOZ3AST_H -#define TRITON_TRITONTOZ3AST_H +#ifndef TRITON_TRITONTOZ3_H +#define TRITON_TRITONTOZ3_H #include #include @@ -32,9 +32,9 @@ namespace triton { * @{ */ - //! \class TritonToZ3Ast + //! \class TritonToZ3 /*! \brief Converts a Triton's AST to Z3's AST. */ - class TritonToZ3Ast { + class TritonToZ3 { private: //! This flag define if the conversion is used to evaluated a node or not. bool isEval; @@ -60,10 +60,10 @@ namespace triton { std::unordered_map variables; //! Constructor. - TRITON_EXPORT TritonToZ3Ast(bool eval=true); + TRITON_EXPORT TritonToZ3(bool eval=true); //! Destructor. - TRITON_EXPORT ~TritonToZ3Ast(); + TRITON_EXPORT ~TritonToZ3(); //! Converts to Z3's AST TRITON_EXPORT z3::expr convert(const triton::ast::SharedAbstractNode& node); @@ -74,4 +74,4 @@ namespace triton { /*! @} End of triton namespace */ }; -#endif /* TRITON_TRITONTOZ3AST_H */ +#endif /* TRITON_TRITONTOZ3_H */ diff --git a/src/libtriton/includes/triton/z3ToTritonAst.hpp b/src/libtriton/includes/triton/z3ToTriton.hpp similarity index 87% rename from src/libtriton/includes/triton/z3ToTritonAst.hpp rename to src/libtriton/includes/triton/z3ToTriton.hpp index 876afb127..c2de04037 100644 --- a/src/libtriton/includes/triton/z3ToTritonAst.hpp +++ b/src/libtriton/includes/triton/z3ToTriton.hpp @@ -31,16 +31,16 @@ namespace triton { * @{ */ - //! \class Z3ToTritonAst + //! \class Z3ToTriton /*! \brief Converts a Z3's AST to a Triton's AST. */ - class Z3ToTritonAst { + class Z3ToTriton { private: //! The Triton's AST context triton::ast::SharedAstContext astCtxt; public: //! Constructor. - TRITON_EXPORT Z3ToTritonAst(const triton::ast::SharedAstContext& ctxt); + TRITON_EXPORT Z3ToTriton(const triton::ast::SharedAstContext& ctxt); //! Converts to Triton's AST TRITON_EXPORT triton::ast::SharedAbstractNode convert(const z3::expr& expr);