From aa1dbb526e0a7f186fd63decb4b442be53757919 Mon Sep 17 00:00:00 2001 From: Jonathan Salwan Date: Sun, 30 Jan 2022 20:10:09 +0100 Subject: [PATCH] Lifting to LLVM IR --- .build_number | 2 +- .github/workflows/codecov.yml | 2 +- .github/workflows/llvm.yml | 57 ++++ CMakeLists.txt | 11 +- CMakeModules/FindLLVM.cmake | 20 ++ src/examples/cpp/CMakeLists.txt | 12 +- .../synthesizing_obfuscated_expressions.py | 15 +- src/libtriton/CMakeLists.txt | 20 +- src/libtriton/Config.cmake.in | 3 +- src/libtriton/api/api.cpp | 51 ++- src/libtriton/ast/astContext.cpp | 8 +- .../ast/bitwuzla/tritonToBitwuzlaAst.cpp | 8 +- src/libtriton/ast/llvm/tritonToLLVM.cpp | 303 ++++++++++++++++++ .../astPythonRepresentation.cpp | 10 +- .../ast/representations/astRepresentation.cpp | 5 +- src/libtriton/ast/z3/tritonToZ3Ast.cpp | 22 +- src/libtriton/ast/z3/z3ToTritonAst.cpp | 88 ++--- .../namespaces/initVersionNamespace.cpp | 24 +- .../python/objects/pyTritonContext.cpp | 141 +++++--- .../engines/lifters/liftingToLLVM.cpp | 52 +++ .../engines/lifters/liftingToPython.cpp | 93 ++++++ .../engines/lifters/liftingToSMT.cpp | 101 ++++++ .../solver/bitwuzla/bitwuzlaSolver.cpp | 2 +- src/libtriton/engines/solver/z3/z3Solver.cpp | 8 +- .../engines/symbolic/symbolicEngine.cpp | 68 ---- src/libtriton/includes/triton/api.hpp | 34 +- src/libtriton/includes/triton/astContext.hpp | 6 +- src/libtriton/includes/triton/astEnums.hpp | 6 +- .../includes/triton/astRepresentation.hpp | 8 +- src/libtriton/includes/triton/config.hpp.in | 1 + src/libtriton/includes/triton/exceptions.hpp | 22 +- .../includes/triton/liftingEngine.hpp | 74 +++++ .../includes/triton/liftingToLLVM.hpp | 68 ++++ .../includes/triton/liftingToPython.hpp | 70 ++++ .../includes/triton/liftingToSMT.hpp | 67 ++++ src/libtriton/includes/triton/oracleEntry.hpp | 8 +- .../includes/triton/symbolicEngine.hpp | 4 +- .../includes/triton/synthesisResult.hpp | 6 +- src/libtriton/includes/triton/synthesizer.hpp | 6 +- .../includes/triton/tritonToLLVM.hpp | 74 +++++ .../unittests/test_ast_representation.py | 219 +++++++++---- 41 files changed, 1480 insertions(+), 319 deletions(-) create mode 100644 .github/workflows/llvm.yml create mode 100644 CMakeModules/FindLLVM.cmake create mode 100644 src/libtriton/ast/llvm/tritonToLLVM.cpp create mode 100644 src/libtriton/engines/lifters/liftingToLLVM.cpp create mode 100644 src/libtriton/engines/lifters/liftingToPython.cpp create mode 100644 src/libtriton/engines/lifters/liftingToSMT.cpp create mode 100644 src/libtriton/includes/triton/liftingEngine.hpp create mode 100644 src/libtriton/includes/triton/liftingToLLVM.hpp create mode 100644 src/libtriton/includes/triton/liftingToPython.hpp create mode 100644 src/libtriton/includes/triton/liftingToSMT.hpp create mode 100644 src/libtriton/includes/triton/tritonToLLVM.hpp diff --git a/.build_number b/.build_number index 00b89bd1f..f34028d59 100644 --- a/.build_number +++ b/.build_number @@ -1 +1 @@ -1514 +1515 diff --git a/.github/workflows/codecov.yml b/.github/workflows/codecov.yml index 56a379bb6..03a1489df 100644 --- a/.github/workflows/codecov.yml +++ b/.github/workflows/codecov.yml @@ -59,7 +59,7 @@ jobs: run: | mkdir ./build cd ./build - cmake -DGCOV=ON -DZ3_INTERFACE=on -DBITWUZLA_INTERFACE=on .. + cmake -DGCOV=ON -DZ3_INTERFACE=on -DBITWUZLA_INTERFACE=on -DLLVM_INTERFACE=ON -DLLVM_INCLUDE_DIRS=$(llvm-config-12 --includedir) -DLLVM_LIBRARIES=$(llvm-config-12 --libfiles) .. sudo make -j3 install - name: Unittests run: | diff --git a/.github/workflows/llvm.yml b/.github/workflows/llvm.yml new file mode 100644 index 000000000..24dde5d26 --- /dev/null +++ b/.github/workflows/llvm.yml @@ -0,0 +1,57 @@ +name: Tests on Linux with LLVM + +on: [push, pull_request, workflow_dispatch] + +jobs: + build: + runs-on: ubuntu-latest + strategy: + matrix: + python-version: [3.9] + steps: + - name: Checkout + uses: actions/checkout@v2 + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v2 + with: + python-version: ${{ matrix.python-version }} + - name: Upgrade pip version + run: | + python -m pip install -U pip + - name: Install dependencies + run: | + sudo apt-get install python-setuptools libboost-dev + - name: Install Z3 + run: | + sudo apt-get install libz3-dev + python -m pip install z3-solver + - name: Install Capstone + run: | + wget https://github.com/aquynh/capstone/archive/4.0.2.tar.gz + tar -xf ./4.0.2.tar.gz + cd ./capstone-4.0.2 + bash ./make.sh + sudo make install + cd ../ + - name: Install Unicorn + run: | + git clone https://github.com/unicorn-engine/unicorn + cd ./unicorn + git checkout ec4c6365c3c91703b3725540100023f6a03db742 # 1.0.2-rc2 + UNICORN_ARCHS="x86 arm aarch64" ./make.sh # we use unicorn to only test some semantics + sudo make install + cd bindings/python + python ./setup.py install --user + cd ../../../ + - name: Install LIEF + run: | + python -m pip install lief + - name: Compile Triton + run: | + mkdir ./build + cd ./build + cmake -DLLVM_INTERFACE=ON -DLLVM_INCLUDE_DIRS=$(llvm-config-12 --includedir) -DLLVM_LIBRARIES=$(llvm-config-12 --libfiles) .. + sudo make -j3 install + - name: Unittests + run: | + make -C build check diff --git a/CMakeLists.txt b/CMakeLists.txt index 30691b086..0f836c8ba 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -25,8 +25,9 @@ include(CMakeDependentOption) option(ASAN "Enable the ASAN linking" OFF) option(BITWUZLA_INTERFACE "Use Bitwuzla as SMT solver" OFF) option(BUILD_SHARED_LIBS "Build a shared library" ON) -option(MSVC_STATIC "Use statically-linked runtime library" OFF) option(GCOV "Enable code coverage" OFF) +option(LLVM_INTERFACE "Use LLVM for lifting" OFF) +option(MSVC_STATIC "Use statically-linked runtime library" OFF) option(Z3_INTERFACE "Use Z3 as SMT solver" ON) # Define cmake dependent options @@ -109,6 +110,14 @@ if(BITWUZLA_INTERFACE) set(TRITON_BITWUZLA_INTERFACE ON) endif() +# Find LLVM +if(LLVM_INTERFACE) + message(STATUS "Compiling with LLVM") + find_package(LLVM REQUIRED) + include_directories(${LLVM_INCLUDE_DIRS}) + set(TRITON_LLVM_INTERFACE ON) +endif() + # Find Capstone message(STATUS "Compiling with Capstone") find_package(CAPSTONE REQUIRED) diff --git a/CMakeModules/FindLLVM.cmake b/CMakeModules/FindLLVM.cmake new file mode 100644 index 000000000..4f879e450 --- /dev/null +++ b/CMakeModules/FindLLVM.cmake @@ -0,0 +1,20 @@ +# - Try to find LLVM +# Once done, this will define +# +# LLVM_INCLUDE_DIRS - the LLVM include directories +# LLVM_LIBRARIES - link these to use LLVM + +if(NOT LLVM_INCLUDE_DIRS) + set(LLVM_INCLUDE_DIRS "$ENV{LLVM_INCLUDE_DIRS}") +endif() + +if(NOT LLVM_LIBRARIES) + set(LLVM_LIBRARIES "$ENV{LLVM_LIBRARIES}") +endif() + +if(NOT LLVM_INCLUDE_DIRS AND NOT LLVM_LIBRARIES) + message(FATAL_ERROR "LLVM not found") +else() + message(STATUS "LLVM includes directory defined: ${LLVM_INCLUDE_DIRS}") + message(STATUS "LLVM libraries defined: ${LLVM_LIBRARIES}") +endif() diff --git a/src/examples/cpp/CMakeLists.txt b/src/examples/cpp/CMakeLists.txt index d6ed58d30..19ad41914 100644 --- a/src/examples/cpp/CMakeLists.txt +++ b/src/examples/cpp/CMakeLists.txt @@ -7,37 +7,37 @@ if (NOT BUILD_SHARED_LIBS) endif() add_executable(taint_reg taint_reg.cpp) -set_property(TARGET taint_reg PROPERTY CXX_STANDARD 11) +set_property(TARGET taint_reg PROPERTY CXX_STANDARD 14) target_link_libraries(taint_reg triton) add_test(TaintRegister taint_reg) add_dependencies(check taint_reg) add_executable(info_reg info_reg.cpp) -set_property(TARGET info_reg PROPERTY CXX_STANDARD 11) +set_property(TARGET info_reg PROPERTY CXX_STANDARD 14) target_link_libraries(info_reg triton) add_test(InfoRegister info_reg) add_dependencies(check info_reg) add_executable(ir ir.cpp) -set_property(TARGET ir PROPERTY CXX_STANDARD 11) +set_property(TARGET ir PROPERTY CXX_STANDARD 14) target_link_libraries(ir triton) add_test(IR ir) add_dependencies(check ir) add_executable(simplification simplification.cpp) -set_property(TARGET simplification PROPERTY CXX_STANDARD 11) +set_property(TARGET simplification PROPERTY CXX_STANDARD 14) target_link_libraries(simplification triton) add_test(Simplification simplification) add_dependencies(check simplification) add_executable(constraint constraint.cpp) -set_property(TARGET constraint PROPERTY CXX_STANDARD 11) +set_property(TARGET constraint PROPERTY CXX_STANDARD 14) target_link_libraries(constraint triton) add_test(Constraint constraint) add_dependencies(check constraint) add_executable(ctest_api ctest_api.cpp) -set_property(TARGET ctest_api PROPERTY CXX_STANDARD 11) +set_property(TARGET ctest_api PROPERTY CXX_STANDARD 14) target_link_libraries(ctest_api triton) add_test(TestAPI ctest_api) add_dependencies(check ctest_api) diff --git a/src/examples/python/synthesizing_obfuscated_expressions.py b/src/examples/python/synthesizing_obfuscated_expressions.py index 906cf97e2..7dae53f0a 100755 --- a/src/examples/python/synthesizing_obfuscated_expressions.py +++ b/src/examples/python/synthesizing_obfuscated_expressions.py @@ -31,8 +31,6 @@ ## python3 ./synthesizing_obfuscated_expressions.py 0.12s user 0.01s system 99% cpu 0.125 total ## -from __future__ import print_function - import sys import ctypes @@ -56,18 +54,15 @@ def x_xor_92_obfuscated(x): def main(): - ctx = TritonContext(ARCH.X86_64) - - try: - ctx.setSolver(SOLVER.Z3) - except: - # NOTE The FORALL node is not supported currently in Bitwuzla. Remove - # this check once it is supported. + if VERSION.Z3_INTERFACE is False: + # NOTE: The FORALL node is not supported currently in Bitwuzla. print("This script requires Z3 as the solver engine. Compile Triton with Z3 support and re-run.") - # Return 0 so the test don't fail. sys.exit(0) + ctx = TritonContext(ARCH.X86_64) + ctx.setSolver(SOLVER.Z3) + ast = ctx.getAstContext() ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON) diff --git a/src/libtriton/CMakeLists.txt b/src/libtriton/CMakeLists.txt index 856671442..ee776db9e 100644 --- a/src/libtriton/CMakeLists.txt +++ b/src/libtriton/CMakeLists.txt @@ -42,6 +42,8 @@ set(LIBTRITON_SOURCE_FILES ast/representations/astRepresentation.cpp ast/representations/astSmtRepresentation.cpp callbacks/callbacks.cpp + engines/lifters/liftingToPython.cpp + engines/lifters/liftingToSMT.cpp engines/solver/solverEngine.cpp engines/solver/solverModel.cpp engines/symbolic/pathConstraint.cpp @@ -93,6 +95,10 @@ set(LIBTRITON_HEADER_FILES includes/triton/immediate.hpp includes/triton/instruction.hpp includes/triton/irBuilder.hpp + includes/triton/liftingEngine.hpp + includes/triton/liftingToLLVM.hpp + includes/triton/liftingToPython.hpp + includes/triton/liftingToSMT.hpp includes/triton/memoryAccess.hpp includes/triton/modes.hpp includes/triton/modesEnums.hpp @@ -116,6 +122,7 @@ set(LIBTRITON_HEADER_FILES includes/triton/synthesizer.hpp includes/triton/taintEngine.hpp includes/triton/tritonToBitwuzlaAst.hpp + includes/triton/tritonToLLVM.hpp includes/triton/tritonToZ3Ast.hpp includes/triton/tritonTypes.hpp includes/triton/x86.spec @@ -152,6 +159,15 @@ else() set(BITWUZLA_INTERFACE_SOURCE_FILES) endif() +if(LLVM_INTERFACE) + set(LLVM_INTERFACE_SOURCE_FILES + ast/llvm/tritonToLLVM.cpp + engines/lifters/liftingToLLVM.cpp + ) +else() + set(LLVM_INTERFACE_SOURCE_FILES) +endif() + if(PYTHON_BINDINGS) set(LIBTRITON_PYTHON_SOURCE_FILES bindings/python/init.cpp @@ -221,6 +237,7 @@ add_library(triton ${LIBTRITON_RESOURCE_FILES} ${Z3_INTERFACE_SOURCE_FILES} ${BITWUZLA_INTERFACE_SOURCE_FILES} + ${LLVM_INTERFACE_SOURCE_FILES} ${LIBTRITON_PYTHON_SOURCE_FILES} ${LIBTRITON_PYTHON_HEADER_FILES} ) @@ -240,6 +257,7 @@ target_link_libraries(triton PUBLIC ${PYTHON_LIBRARIES} ${Boost_LIBRARIES} ${Z3_LIBRARIES} + ${LLVM_LIBRARIES} ${BITWUZLA_LIBRARIES} ${CAPSTONE_LIBRARIES} ${LIBTRITON_OTHER_LIBS} @@ -247,7 +265,7 @@ target_link_libraries(triton PUBLIC # Workaround to allow building 'namespace linux' (defined by -std=gnu++11) if(NOT MSVC AND (CMAKE_CXX_COMPILER_ID MATCHES "Clang" OR CMAKE_CXX_COMPILER_ID STREQUAL "GNU")) - target_compile_options(triton PRIVATE -std=c++11) + target_compile_options(triton PRIVATE -std=c++14) endif() # Enable static msvc runtime. diff --git a/src/libtriton/Config.cmake.in b/src/libtriton/Config.cmake.in index e496cc525..47134889d 100644 --- a/src/libtriton/Config.cmake.in +++ b/src/libtriton/Config.cmake.in @@ -3,8 +3,9 @@ include("${CMAKE_CURRENT_LIST_DIR}/tritonTargets.cmake") set(TRITON_VERSION @VERSION_MAJOR@.@VERSION_MINOR@) -set(TRITON_Z3_INTERFACE @Z3_INTERFACE@) set(TRITON_BITWUZLA_INTERFACE @BITWUZLA_INTERFACE@) +set(TRITON_LLVM_INTERFACE @LLVM_INTERFACE@) +set(TRITON_Z3_INTERFACE @Z3_INTERFACE@) set(TRITON_INCLUDE_DIRS "@CMAKE_INSTALL_PREFIX@/@CMAKE_INSTALL_INCLUDEDIR@") set(TRITON_LIBRARY "@CMAKE_INSTALL_PREFIX@/@CMAKE_INSTALL_LIBDIR@/@CMAKE_SHARED_LIBRARY_PREFIX@triton@CMAKE_SHARED_LIBRARY_SUFFIX@") diff --git a/src/libtriton/api/api.cpp b/src/libtriton/api/api.cpp index 7798042e6..3337f3826 100644 --- a/src/libtriton/api/api.cpp +++ b/src/libtriton/api/api.cpp @@ -284,6 +284,12 @@ namespace triton { } + inline void API::checkLifting(void) const { + if (!this->lifting) + throw triton::exceptions::API("API::checkLifting(): Lifting engine is undefined, you should define an architecture first."); + } + + /* Architecture API ============================================================================== */ @@ -555,6 +561,10 @@ namespace triton { if (this->taint == nullptr) throw triton::exceptions::API("API::initEngines(): Not enough memory."); + this->lifting = new(std::nothrow) triton::engines::lifters::LiftingEngine(this->astCtxt, this->symbolic); + if (this->lifting == nullptr) + throw triton::exceptions::API("API::initEngines(): Not enough memory."); + this->irBuilder = new(std::nothrow) triton::arch::IrBuilder(&this->arch, this->modes, this->astCtxt, this->symbolic, this->taint); if (this->irBuilder == nullptr) throw triton::exceptions::API("API::initEngines(): Not enough memory."); @@ -567,12 +577,14 @@ namespace triton { void API::removeEngines(void) { if (this->isArchitectureValid()) { delete this->irBuilder; + delete this->lifting; delete this->solver; delete this->symbolic; delete this->taint; this->astCtxt = nullptr; this->irBuilder = nullptr; + this->lifting = nullptr; this->solver = nullptr; this->symbolic = nullptr; this->taint = nullptr; @@ -621,12 +633,12 @@ namespace triton { /* AST representation API ========================================================================= */ - triton::uint32 API::getAstRepresentationMode(void) const { + triton::ast::representations::mode_e API::getAstRepresentationMode(void) const { return this->astCtxt->getRepresentationMode(); } - void API::setAstRepresentationMode(triton::uint32 mode) { + void API::setAstRepresentationMode(triton::ast::representations::mode_e mode) { this->astCtxt->setRepresentationMode(mode); } @@ -1043,12 +1055,6 @@ namespace triton { } - std::ostream& API::printSlicedExpressions(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_) { - this->checkSymbolic(); - return this->symbolic->printSlicedExpressions(stream, expr, assert_); - } - - std::vector API::getTaintedSymbolicExpressions(void) const { this->checkSymbolic(); return this->symbolic->getTaintedSymbolicExpressions(); @@ -1363,4 +1369,33 @@ namespace triton { return synth.synthesize(node, constant, subexpr, opaque); } + + + /* Lifters engine API ================================================================================= */ + + std::ostream& API::liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node) { + this->checkLifting(); + #ifdef TRITON_LLVM_INTERFACE + return this->lifting->liftToLLVM(stream, node); + #endif + throw triton::exceptions::API("API::liftToLLVM(): Triton not built with LLVM"); + } + + + std::ostream& API::liftToLLVM(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr) { + return this->liftToLLVM(stream, expr->getAst()); + } + + + std::ostream& API::liftToPython(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr) { + this->checkLifting(); + return this->lifting->liftToPython(stream, expr); + } + + + std::ostream& API::liftToSMT(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_) { + this->checkLifting(); + return this->lifting->liftToSMT(stream, expr, assert_); + } + }; /* triton namespace */ diff --git a/src/libtriton/ast/astContext.cpp b/src/libtriton/ast/astContext.cpp index 338360aea..f6ae74b53 100644 --- a/src/libtriton/ast/astContext.cpp +++ b/src/libtriton/ast/astContext.cpp @@ -376,7 +376,7 @@ namespace triton { * in order to make index rotation symbolic. Note that this mode increases the * complexity of solving. * - * bvrol(rot, expr) = ((expr << (rot % size)) | (expr >> (size - (rot % size)))) + * bvrol(expr, rot) = ((expr << (rot % size)) | (expr >> (size - (rot % size)))) **/ if (this->modes->isModeEnabled(triton::modes::SYMBOLIZE_INDEX_ROTATION)) { auto size = expr->getBitvectorSize(); @@ -426,7 +426,7 @@ namespace triton { * in order to make index rotation symbolic. Note that this mode increases the * complexity of solving. * - * bvror(rot, expr) = ((value >> (rot % size)) | (value << (size - (rot % size)))) + * bvror(expr, rot) = ((expr >> (rot % size)) | (expr << (size - (rot % size)))) **/ if (this->modes->isModeEnabled(triton::modes::SYMBOLIZE_INDEX_ROTATION)) { auto size = expr->getBitvectorSize(); @@ -1054,12 +1054,12 @@ namespace triton { } - void AstContext::setRepresentationMode(triton::uint32 mode) { + void AstContext::setRepresentationMode(triton::ast::representations::mode_e mode) { this->astRepresentation.setMode(mode); } - triton::uint32 AstContext::getRepresentationMode(void) const { + triton::ast::representations::mode_e AstContext::getRepresentationMode(void) const { return this->astRepresentation.getMode(); } diff --git a/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp b/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp index 350cb96d5..cffc5a756 100644 --- a/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp +++ b/src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp @@ -51,7 +51,7 @@ namespace triton { const BitwuzlaTerm* TritonToBitwuzlaAst::translate(const SharedAbstractNode& node, Bitwuzla* bzla) { if (node == nullptr) - throw triton::exceptions::AstTranslations("TritonToBitwuzlaAst::translate(): node cannot be null."); + throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::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::AstTranslations("TritonToBitwuzlaAst::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062)."); + throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::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::AstTranslations("TritonToBitwuzlaAst::translate(): [STRING_NODE] Symbols not found."); + throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): [STRING_NODE] Symbols not found."); return translatedNodes.at(it->second); } @@ -265,7 +265,7 @@ namespace triton { } default: - throw triton::exceptions::AstTranslations("TritonToBitwuzlaAst::translate(): Invalid kind of node."); + throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): Invalid kind of node."); } } diff --git a/src/libtriton/ast/llvm/tritonToLLVM.cpp b/src/libtriton/ast/llvm/tritonToLLVM.cpp new file mode 100644 index 000000000..ab5c8637f --- /dev/null +++ b/src/libtriton/ast/llvm/tritonToLLVM.cpp @@ -0,0 +1,303 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#include +#include +#include +#include + +#include +#include +#include +#include +#include +#include + + + +namespace triton { + namespace ast { + + TritonToLLVM::TritonToLLVM(llvm::LLVMContext& llvmContext) + : llvmContext(llvmContext), llvmIR(this->llvmContext) { + this->llvmModule = std::make_shared("tritonModule", this->llvmContext); + if (llvmModule == nullptr) { + triton::exceptions::LiftingEngine("TritonToLLVM::TritonToLLVM: Failed to allocate the LLVM Module"); + } + } + + + void TritonToLLVM::createFunction(const triton::ast::SharedAbstractNode& node) { + // Collect used symbolic variables. + auto vars = triton::ast::search(node, triton::ast::VARIABLE_NODE); + + // Each symbolic variable is a function argument + std::vector argsType; + argsType.resize(vars.size()); + for (triton::usize index = 0 ; index < vars.size() ; index++) { + switch (vars[index]->getBitvectorSize()) { + case 8: + argsType[index] = llvm::Type::getInt8Ty(this->llvmContext); + break; + case 16: + argsType[index] = llvm::Type::getInt16Ty(this->llvmContext); + break; + case 32: + argsType[index] = llvm::Type::getInt32Ty(this->llvmContext); + break; + case 64: + argsType[index] = llvm::Type::getInt64Ty(this->llvmContext); + break; + default: + throw triton::exceptions::AstLifting("TritonToLLVM::do_convert(): Symbolic variables must be aligned on 8, 16, 32 or 64 bit."); + } + } + + /* Declare LLVM function */ + 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()); + + /* 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()); + this->llvmVars[node] = param; + } + + // A Triton expression is represented as one basic block + auto* llvmBasicBlock = llvm::BasicBlock::Create(this->llvmContext, "entry", llvmFunc); + this->llvmIR.SetInsertPoint(llvmBasicBlock); + } + + + std::shared_ptr TritonToLLVM::convert(const triton::ast::SharedAbstractNode& node) { + std::unordered_map results; + + /* Create the LLVM function */ + this->createFunction(node); + + /* Lift Triton AST to LLVM IR */ + auto nodes = triton::ast::childrenExtraction(node, true /* unroll*/, true /* revert */); + for (const auto& node : nodes) { + if (node->getBitvectorSize()) { + results.insert(std::make_pair(node, this->do_convert(node, &results))); + } + } + + /* Create the return instruction */ + this->llvmIR.CreateRet(results.at(node)); + + return this->llvmModule; + } + + + llvm::Value* TritonToLLVM::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results) { + if (node == nullptr) + throw triton::exceptions::AstLifting("TritonToLLVM::do_convert(): node cannot be null."); + + /* Prepare llvm's children */ + std::vector children; + for (auto&& n : node->getChildren()) { + /* Ignore children like INTEGER_NODE */ + if (n->getBitvectorSize() == 0) { + children.emplace_back(nullptr); + } + else { + children.emplace_back(results->at(n)); + } + } + + switch (node->getType()) { + case triton::ast::BVADD_NODE: + return this->llvmIR.CreateAdd(children[0], children[1]); + + case triton::ast::BVAND_NODE: + return this->llvmIR.CreateAnd(children[0], children[1]); + + case triton::ast::BVASHR_NODE: + return this->llvmIR.CreateAShr(children[0], children[1]); + + case triton::ast::BVLSHR_NODE: + return this->llvmIR.CreateLShr(children[0], children[1]); + + case triton::ast::BVMUL_NODE: + return this->llvmIR.CreateMul(children[0], children[1]); + + case triton::ast::BVNAND_NODE: + return this->llvmIR.CreateNot(this->llvmIR.CreateAnd(children[0], children[1])); + + case triton::ast::BVNEG_NODE: + return this->llvmIR.CreateNeg(children[0]); + + case triton::ast::BVNOR_NODE: + return this->llvmIR.CreateNot(this->llvmIR.CreateOr(children[0], children[1])); + + case triton::ast::BVNOT_NODE: + return this->llvmIR.CreateNot(children[0]); + + case triton::ast::BVOR_NODE: + return this->llvmIR.CreateOr(children[0], children[1]); + + // bvrol(expr, rot) = ((expr << (rot % size)) | (expr >> (size - (rot % size)))) + case triton::ast::BVROL_NODE: { + auto rot = reinterpret_cast(node->getChildren()[1].get())->getInteger().convert_to(); + auto size = node->getBitvectorSize(); + return this->llvmIR.CreateOr(this->llvmIR.CreateShl(children[0], rot % size), this->llvmIR.CreateLShr(children[0], (size - (rot % size)))); + } + + // bvror(expr, rot) = ((expr >> (rot % size)) | (expr << (size - (rot % size)))) + case triton::ast::BVROR_NODE: { + auto rot = reinterpret_cast(node->getChildren()[1].get())->getInteger().convert_to(); + auto size = node->getBitvectorSize(); + return this->llvmIR.CreateOr(this->llvmIR.CreateLShr(children[0], rot % size), this->llvmIR.CreateShl(children[0], (size - (rot % size)))); + } + + case triton::ast::BVSDIV_NODE: + return this->llvmIR.CreateSDiv(children[0], children[1]); + + case triton::ast::BVSGE_NODE: + return this->llvmIR.CreateICmpSGE(children[0], children[1]); + + case triton::ast::BVSGT_NODE: + return this->llvmIR.CreateICmpSGT(children[0], children[1]); + + case triton::ast::BVSHL_NODE: + return this->llvmIR.CreateShl(children[0], children[1]); + + case triton::ast::BVSLE_NODE: + return this->llvmIR.CreateICmpSLE(children[0], children[1]); + + case triton::ast::BVSLT_NODE: + return this->llvmIR.CreateICmpSLT(children[0], children[1]); + + case triton::ast::BVSMOD_NODE: { + auto* LHS = children[0]; + auto* RHS = children[1]; + return this->llvmIR.CreateSRem(this->llvmIR.CreateAdd(this->llvmIR.CreateSRem(LHS, RHS), RHS), RHS); + } + + case triton::ast::BVSREM_NODE: + return this->llvmIR.CreateSRem(children[0], children[1]); + + case triton::ast::BVSUB_NODE: + return this->llvmIR.CreateSub(children[0], children[1]); + + case triton::ast::BVUDIV_NODE: + return this->llvmIR.CreateUDiv(children[0], children[1]); + + case triton::ast::BVUGE_NODE: + return this->llvmIR.CreateICmpUGE(children[0], children[1]); + + case triton::ast::BVUGT_NODE: + return this->llvmIR.CreateICmpUGT(children[0], children[1]); + + case triton::ast::BVULE_NODE: + return this->llvmIR.CreateICmpULE(children[0], children[1]); + + case triton::ast::BVULT_NODE: + return this->llvmIR.CreateICmpULT(children[0], children[1]); + + case triton::ast::BVUREM_NODE: + return this->llvmIR.CreateURem(children[0], children[1]); + + case triton::ast::BVXNOR_NODE: + return this->llvmIR.CreateNot(this->llvmIR.CreateXor(children[0], children[1])); + + case triton::ast::BVXOR_NODE: + return this->llvmIR.CreateXor(children[0], children[1]); + + case triton::ast::BV_NODE: + return llvm::ConstantInt::get(this->llvmContext, llvm::APInt(node->getBitvectorSize(), node->evaluate().convert_to(), false)); + + case triton::ast::CONCAT_NODE: { + auto dstSize = node->getBitvectorSize(); + auto finalNode = this->llvmIR.CreateZExt(children[0], llvm::IntegerType::get(this->llvmContext, dstSize)); + + for (triton::usize index = 1; index < children.size(); index++) { + finalNode = this->llvmIR.CreateShl(finalNode, node->getChildren()[index]->getBitvectorSize()); + auto* n = this->llvmIR.CreateZExt(children[index], llvm::IntegerType::get(this->llvmContext, dstSize)); + finalNode = this->llvmIR.CreateOr(finalNode, n); + } + + return finalNode; + } + + case triton::ast::DISTINCT_NODE: + return this->llvmIR.CreateICmpNE(children[0], children[1]); + + case triton::ast::EQUAL_NODE: + return this->llvmIR.CreateICmpEQ(children[0], children[1]); + + case triton::ast::EXTRACT_NODE: { + auto low = reinterpret_cast(node->getChildren()[1].get())->getInteger().convert_to(); + auto dstSize = node->getChildren()[2]->getBitvectorSize(); + auto* value = children[2]; + + if (low == 0) { + return this->llvmIR.CreateTrunc(value, llvm::IntegerType::get(this->llvmContext, node->getBitvectorSize())); + } + + return this->llvmIR.CreateTrunc(this->llvmIR.CreateLShr(value, low), llvm::IntegerType::get(this->llvmContext, node->getBitvectorSize())); + } + + case triton::ast::ITE_NODE: + return this->llvmIR.CreateSelect(children[0], children[1], children[2]); + + case triton::ast::LAND_NODE: { + auto* truenode = llvm::ConstantInt::get(this->llvmContext, llvm::APInt(1, 1)); + return this->llvmIR.CreateICmpEQ(this->llvmIR.CreateAnd(children), truenode); + } + + case triton::ast::LNOT_NODE: { + auto* truenode = llvm::ConstantInt::get(this->llvmContext, llvm::APInt(1, 1)); + return this->llvmIR.CreateICmpEQ(this->llvmIR.CreateNot(children[0]), truenode); + } + + case triton::ast::LOR_NODE: { + auto* truenode = llvm::ConstantInt::get(this->llvmContext, llvm::APInt(1, 1)); + return this->llvmIR.CreateICmpEQ(this->llvmIR.CreateOr(children), truenode); + } + + case triton::ast::LXOR_NODE: { + auto* child0 = children[0]; + auto* child1 = children[1]; + auto* current = this->llvmIR.CreateXor(child0, child1); + + for (triton::usize index = 2; index < children.size(); index++) { + current = this->llvmIR.CreateXor(current, children[index]); + } + + auto* truenode = llvm::ConstantInt::get(this->llvmContext, llvm::APInt(1, 1)); + return this->llvmIR.CreateICmpEQ(current, truenode); + } + + case triton::ast::REFERENCE_NODE: + return results->at(reinterpret_cast(node.get())->getSymbolicExpression()->getAst()); + + case triton::ast::SX_NODE: + return this->llvmIR.CreateSExt(children[1], llvm::IntegerType::get(this->llvmContext, node->getBitvectorSize())); + + case triton::ast::VARIABLE_NODE: + return this->llvmVars.at(node); + + case triton::ast::ZX_NODE: + return this->llvmIR.CreateZExt(children[1], llvm::IntegerType::get(this->llvmContext, node->getBitvectorSize())); + + default: + throw triton::exceptions::AstLifting("TritonToLLVM::do_convert(): Invalid kind of node."); + } + } + + }; /* ast namespace */ +}; /* triton namespace */ diff --git a/src/libtriton/ast/representations/astPythonRepresentation.cpp b/src/libtriton/ast/representations/astPythonRepresentation.cpp index 2878c4d5d..bf1b8f28c 100644 --- a/src/libtriton/ast/representations/astPythonRepresentation.cpp +++ b/src/libtriton/ast/representations/astPythonRepresentation.cpp @@ -83,7 +83,7 @@ namespace triton { /* assert representation */ std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::AssertNode* node) { - stream << "assert_(" << node->getChildren()[0] << ")"; + stream << "assert (" << node->getChildren()[0] << ")"; return stream; } @@ -160,14 +160,14 @@ namespace triton { /* bvrol representation */ std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::BvrolNode* node) { - stream << "rol(" << node->getChildren()[0] << ", " << node->getChildren()[1] << ")"; + stream << "rol(" << node->getChildren()[0] << ", " << node->getChildren()[1] << ", " << node->getBitvectorSize() << ")"; return stream; } /* bvror representation */ std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::BvrorNode* node) { - stream << "ror(" << node->getChildren()[0] << ", " << node->getChildren()[1] << ")"; + stream << "ror(" << node->getChildren()[0] << ", " << node->getChildren()[1] << ", " << node->getBitvectorSize() << ")"; return stream; } @@ -330,9 +330,9 @@ namespace triton { std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::DeclareNode* node) { const triton::engines::symbolic::SharedSymbolicVariable& var = reinterpret_cast(node->getChildren()[0].get())->getSymbolicVariable(); if (var->getAlias().empty()) - stream << var->getName() << " = " << "0xdeadbeef"; + stream << var->getName() << " = " << "int(input())"; else - stream << var->getAlias() << " = " << "0xdeadbeef"; + stream << var->getAlias() << " = " << "int(input())"; return stream; } diff --git a/src/libtriton/ast/representations/astRepresentation.cpp b/src/libtriton/ast/representations/astRepresentation.cpp index 84258f933..998b9c2f8 100644 --- a/src/libtriton/ast/representations/astRepresentation.cpp +++ b/src/libtriton/ast/representations/astRepresentation.cpp @@ -45,12 +45,12 @@ namespace triton { } - triton::uint32 AstRepresentation::getMode(void) const { + triton::ast::representations::mode_e AstRepresentation::getMode(void) const { return this->mode; } - void AstRepresentation::setMode(triton::uint32 mode) { + void AstRepresentation::setMode(triton::ast::representations::mode_e mode) { if (mode >= triton::ast::representations::LAST_REPRESENTATION) throw triton::exceptions::AstRepresentation("AstRepresentation::setMode(): Invalid representation mode."); this->mode = mode; @@ -64,4 +64,3 @@ namespace triton { }; }; }; - diff --git a/src/libtriton/ast/z3/tritonToZ3Ast.cpp b/src/libtriton/ast/z3/tritonToZ3Ast.cpp index 4b76fd79a..e544dff7e 100644 --- a/src/libtriton/ast/z3/tritonToZ3Ast.cpp +++ b/src/libtriton/ast/z3/tritonToZ3Ast.cpp @@ -33,7 +33,7 @@ namespace triton { triton::__uint TritonToZ3Ast::getUintValue(const z3::expr& expr) { if (!expr.is_int()) - throw triton::exceptions::Exception("TritonToZ3Ast::getUintValue(): The ast is not a numerical value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::getUintValue(): The ast is not a numerical value."); #if defined(__x86_64__) || defined(_M_X64) || defined(__aarch64__) return expr.get_numeral_uint64(); @@ -64,7 +64,7 @@ namespace triton { z3::expr TritonToZ3Ast::do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results) { if (node == nullptr) - throw triton::exceptions::AstTranslations("TritonToZ3Ast::do_convert(): node cannot be null."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LandNode(): Land can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LandNode(): Land can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LnotNode(): Lnot can be apply only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::LxorNode(): Lxor can be applied only on bool value."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::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::AstTranslations("TritonToZ3Ast::do_convert(): [STRING_NODE] Symbols not found."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::do_convert(): [STRING_NODE] Symbols not found."); return results->at(this->symbols[value]); } @@ -355,7 +355,7 @@ namespace triton { } default: - throw triton::exceptions::AstTranslations("TritonToZ3Ast::do_convert(): Invalid kind of node."); + throw triton::exceptions::AstLifting("TritonToZ3Ast::do_convert(): Invalid kind of node."); } } diff --git a/src/libtriton/ast/z3/z3ToTritonAst.cpp b/src/libtriton/ast/z3/z3ToTritonAst.cpp index db516ac82..732de3cdc 100644 --- a/src/libtriton/ast/z3/z3ToTritonAst.cpp +++ b/src/libtriton/ast/z3/z3ToTritonAst.cpp @@ -26,10 +26,10 @@ namespace triton { /* Currently, only support application node (TODO) */ if (expr.is_quantifier()) - throw triton::exceptions::AstTranslations("Z3ToTritonAst::visit(): Quantifier not supported yet."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Quantifier not supported yet."); if (!expr.is_app()) - throw triton::exceptions::AstTranslations("Z3ToTritonAst::visit(): At this moment only application are supported."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_EQ must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_DISTINCT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_IFF must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ITE must contain three arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_AND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_OR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_XOR must contain two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_NOT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BNEG must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BADD must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BSUB must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BMUL must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BSDIV must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BUDIV must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BSREM must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BUREM must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BSMOD must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ULEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_SLEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_UGEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_SGEQ must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ULT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_SLT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_UGT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_SGT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BAND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BNOT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BXOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BNAND must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BNOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BXNOR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_CONCAT must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_SIGN_EXT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ZERO_EXT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_EXTRACT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BSHL must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BLSHR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_BASHR must contain at least two arguments."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ROTATE_LEFT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::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::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ROTATE_RIGHT must contain one argument."); + throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): Z3_OP_ROTATE_RIGHT must contain one argument."); node = this->astCtxt->bvror(this->convert(expr.arg(0)), expr.hi()); break; } @@ -430,7 +430,7 @@ namespace triton { } default: - throw triton::exceptions::AstTranslations("Z3ToTritonAst::visit(): '" + function.name().str() + "' AST node not supported yet"); + throw triton::exceptions::AstLifting("Z3ToTritonAst::visit(): '" + function.name().str() + "' AST node not supported yet"); } return node; diff --git a/src/libtriton/bindings/python/namespaces/initVersionNamespace.cpp b/src/libtriton/bindings/python/namespaces/initVersionNamespace.cpp index ebefe89e5..d145de687 100644 --- a/src/libtriton/bindings/python/namespaces/initVersionNamespace.cpp +++ b/src/libtriton/bindings/python/namespaces/initVersionNamespace.cpp @@ -5,6 +5,7 @@ ** This program is under the terms of the Apache License 2.0. */ +#include #include #include #include @@ -25,9 +26,12 @@ The VERSION namespace contains all version numbers. \section VERSION_py_api Python API - Items of the VERSION namespace
+- **VERSION.BUILD** - **VERSION.MAJOR** - **VERSION.MINOR** -- **VERSION.BUILD** +- **VERSION.BITWUZLA_INTERFACE** +- **VERSION.LLVM_INTERFACE** +- **VERSION.Z3_INTERFACE** */ @@ -41,6 +45,24 @@ namespace triton { xPyDict_SetItemString(versionDict, "MAJOR", PyLong_FromUint32(triton::MAJOR)); xPyDict_SetItemString(versionDict, "MINOR", PyLong_FromUint32(triton::MINOR)); xPyDict_SetItemString(versionDict, "BUILD", PyLong_FromUint32(triton::BUILD)); + + #ifdef TRITON_Z3_INTERFACE + xPyDict_SetItemString(versionDict, "Z3_INTERFACE", Py_True); + #else + xPyDict_SetItemString(versionDict, "Z3_INTERFACE", Py_False); + #endif + + #ifdef TRITON_BITWUZLA_INTERFACE + xPyDict_SetItemString(versionDict, "BITWUZLA_INTERFACE", Py_True); + #else + xPyDict_SetItemString(versionDict, "BITWUZLA_INTERFACE", Py_False); + #endif + + #ifdef TRITON_LLVM_INTERFACE + xPyDict_SetItemString(versionDict, "LLVM_INTERFACE", Py_True); + #else + xPyDict_SetItemString(versionDict, "LLVM_INTERFACE", Py_False); + #endif } }; /* python namespace */ diff --git a/src/libtriton/bindings/python/objects/pyTritonContext.cpp b/src/libtriton/bindings/python/objects/pyTritonContext.cpp index 6f285dbeb..5dfa40350 100644 --- a/src/libtriton/bindings/python/objects/pyTritonContext.cpp +++ b/src/libtriton/bindings/python/objects/pyTritonContext.cpp @@ -286,6 +286,18 @@ Returns true if the taint engine is enabled. - bool isThumb(void)
Returns true if execution mode is Thumb (only valid for ARM32). +- string liftToLLVM(\ref py_AstNode_page node)
+Lifts an AST node and all its references to LLVM IR. + +- string liftToLLVM(\ref py_SymbolicExpression_page expr)
+Lifts a symbolic expression and all its references to LLVM IR. + +- string liftToPython(\ref py_SymbolicExpression_page expr)
+Lifts a symbolic expression and all its references to Python format. + +- string liftToSMT(\ref py_SymbolicExpression_page expr, bool assert_=False)
+Lifts a symbolic expression and all its references to SMT format. If `assert_` is true, then (assert ). + - \ref py_SymbolicExpression_page newSymbolicExpression(\ref py_AstNode_page node, string comment)
Returns a new symbolic expression. Note that if there are simplification passes recorded, simplifications will be applied. @@ -295,9 +307,6 @@ Returns a new symbolic variable. - void popPathConstraint(void)
Pops the last constraints added to the path predicate. -- void printSlicedExpressions(\ref py_SymbolicExpression_page expr, bool assert_=False)
-Prints symbolic expression with used references and symbolic variables in AST representation mode. If `assert_` is true, then (assert ). - - bool processing(\ref py_Instruction_page inst)
Processes an instruction and updates engines according to the instruction semantics. Returns true if the instruction is supported. You must define an architecture before. @@ -314,7 +323,7 @@ Resets everything. Initializes an architecture. This function must be called before any call to the rest of the API. - void setAstRepresentationMode(\ref py_AST_REPRESENTATION_page mode)
-Sets the AST representation mode. +Sets the AST representation. - void setConcreteMemoryAreaValue(integer baseAddr, [integer,])
Sets the concrete value of a memory area. Note that setting a concrete value will probably imply a desynchronization with @@ -2221,6 +2230,89 @@ namespace triton { } } + + static PyObject* TritonContext_liftToLLVM(PyObject* self, PyObject* arg) { + if (!PySymbolicExpression_Check(arg) && !PyAstNode_Check(arg)) + return PyErr_Format(PyExc_TypeError, "TritonContext::liftToLLVM(): Expects a SymbolicExpression or a AstNode as first argument."); + + try { + std::ostringstream stream; + if (PySymbolicExpression_Check(arg)) { + PyTritonContext_AsTritonContext(self)->liftToLLVM(stream, PySymbolicExpression_AsSymbolicExpression(arg)); + } + else { + PyTritonContext_AsTritonContext(self)->liftToLLVM(stream, PyAstNode_AsAstNode(arg)); + } + return xPyString_FromString(stream.str().c_str()); + } + catch (const triton::exceptions::PyCallbacks&) { + return nullptr; + } + catch (const triton::exceptions::Exception& e) { + return PyErr_Format(PyExc_TypeError, "%s", e.what()); + } + + Py_INCREF(Py_None); + return Py_None; + } + + + static PyObject* TritonContext_liftToPython(PyObject* self, PyObject* expr) { + if (!PySymbolicExpression_Check(expr)) + return PyErr_Format(PyExc_TypeError, "TritonContext::liftToPython(): Expects a SymbolicExpression as first argument."); + + try { + std::ostringstream stream; + PyTritonContext_AsTritonContext(self)->liftToPython(stream, PySymbolicExpression_AsSymbolicExpression(expr)); + return xPyString_FromString(stream.str().c_str()); + } + catch (const triton::exceptions::PyCallbacks&) { + return nullptr; + } + catch (const triton::exceptions::Exception& e) { + return PyErr_Format(PyExc_TypeError, "%s", e.what()); + } + + Py_INCREF(Py_None); + return Py_None; + } + + + static PyObject* TritonContext_liftToSMT(PyObject* self, PyObject* args) { + PyObject* expr = nullptr; + PyObject* assertFlag = nullptr; + + /* Extract arguments */ + if (PyArg_ParseTuple(args, "|OO", &expr, &assertFlag) == false) { + return PyErr_Format(PyExc_TypeError, "TritonContext::liftToSMT(): Invalid number of arguments"); + } + + if (expr == nullptr || !PySymbolicExpression_Check(expr)) + return PyErr_Format(PyExc_TypeError, "TritonContext::liftToSMT(): Expects a SymbolicExpression as first argument."); + + if (assertFlag != nullptr && !PyBool_Check(assertFlag)) + return PyErr_Format(PyExc_TypeError, "TritonContext::liftToSMT(): Expects a boolean as second argument."); + + if (assertFlag == nullptr) + assertFlag = PyLong_FromUint32(false); + + try { + std::ostringstream stream; + PyTritonContext_AsTritonContext(self)->liftToSMT(stream, PySymbolicExpression_AsSymbolicExpression(expr), PyLong_AsBool(assertFlag)); + return xPyString_FromString(stream.str().c_str()); + } + catch (const triton::exceptions::PyCallbacks&) { + return nullptr; + } + catch (const triton::exceptions::Exception& e) { + return PyErr_Format(PyExc_TypeError, "%s", e.what()); + } + + Py_INCREF(Py_None); + return Py_None; + } + + static PyObject* TritonContext_newSymbolicExpression(PyObject* self, PyObject* args) { PyObject* node = nullptr; PyObject* comment = nullptr; @@ -2298,41 +2390,6 @@ namespace triton { } - static PyObject* TritonContext_printSlicedExpressions(PyObject* self, PyObject* args) { - PyObject* expr = nullptr; - PyObject* assertFlag = nullptr; - - /* Extract arguments */ - if (PyArg_ParseTuple(args, "|OO", &expr, &assertFlag) == false) { - return PyErr_Format(PyExc_TypeError, "TritonContext::printSlicedExpressions(): Invalid number of arguments"); - } - - if (expr == nullptr || !PySymbolicExpression_Check(expr)) - return PyErr_Format(PyExc_TypeError, "TritonContext::printSlicedExpressions(): Expects a SymbolicExpression as first argument."); - - if (assertFlag != nullptr && !PyBool_Check(assertFlag)) - return PyErr_Format(PyExc_TypeError, "TritonContext::printSlicedExpressions(): Expects a boolean as second argument."); - - if (assertFlag == nullptr) - assertFlag = PyLong_FromUint32(false); - - try { - std::ostringstream stream; - PyTritonContext_AsTritonContext(self)->printSlicedExpressions(stream, PySymbolicExpression_AsSymbolicExpression(expr), PyLong_AsBool(assertFlag)); - return xPyString_FromString(stream.str().c_str()); - } - catch (const triton::exceptions::PyCallbacks&) { - return nullptr; - } - catch (const triton::exceptions::Exception& e) { - return PyErr_Format(PyExc_TypeError, "%s", e.what()); - } - - Py_INCREF(Py_None); - return Py_None; - } - - static PyObject* TritonContext_processing(PyObject* self, PyObject* inst) { if (!PyInstruction_Check(inst)) return PyErr_Format(PyExc_TypeError, "TritonContext::processing(): Expects an Instruction as argument."); @@ -2476,7 +2533,7 @@ namespace triton { return PyErr_Format(PyExc_TypeError, "TritonContext::setAstRepresentationMode(): Expects an AST_REPRESENTATION as argument."); try { - PyTritonContext_AsTritonContext(self)->setAstRepresentationMode(PyLong_AsUint32(arg)); + PyTritonContext_AsTritonContext(self)->setAstRepresentationMode(static_cast(PyLong_AsUint32(arg))); } catch (const triton::exceptions::PyCallbacks&) { return nullptr; @@ -3348,10 +3405,12 @@ namespace triton { {"isSymbolicExpressionExists", (PyCFunction)TritonContext_isSymbolicExpressionExists, METH_O, ""}, {"isTaintEngineEnabled", (PyCFunction)TritonContext_isTaintEngineEnabled, METH_NOARGS, ""}, {"isThumb", (PyCFunction)TritonContext_isThumb, METH_NOARGS, ""}, + {"liftToLLVM", (PyCFunction)TritonContext_liftToLLVM, METH_O, ""}, + {"liftToPython", (PyCFunction)TritonContext_liftToPython, METH_O, ""}, + {"liftToSMT", (PyCFunction)TritonContext_liftToSMT, METH_VARARGS, ""}, {"newSymbolicExpression", (PyCFunction)TritonContext_newSymbolicExpression, METH_VARARGS, ""}, {"newSymbolicVariable", (PyCFunction)TritonContext_newSymbolicVariable, METH_VARARGS, ""}, {"popPathConstraint", (PyCFunction)TritonContext_popPathConstraint, METH_NOARGS, ""}, - {"printSlicedExpressions", (PyCFunction)TritonContext_printSlicedExpressions, METH_VARARGS, ""}, {"processing", (PyCFunction)TritonContext_processing, METH_O, ""}, {"pushPathConstraint", (PyCFunction)TritonContext_pushPathConstraint, METH_O, ""}, {"removeCallback", (PyCFunction)TritonContext_removeCallback, METH_VARARGS, ""}, diff --git a/src/libtriton/engines/lifters/liftingToLLVM.cpp b/src/libtriton/engines/lifters/liftingToLLVM.cpp new file mode 100644 index 000000000..998af444f --- /dev/null +++ b/src/libtriton/engines/lifters/liftingToLLVM.cpp @@ -0,0 +1,52 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#include +#include +#include + +#include +#include + + + +namespace triton { + namespace engines { + namespace lifters { + + LiftingToLLVM::LiftingToLLVM() { + } + + + std::ostream& LiftingToLLVM::liftToLLVM(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr) { + this->liftToLLVM(stream, expr->getAst()); + return stream; + } + + + std::ostream& LiftingToLLVM::liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node) { + /* The LLVM context */ + llvm::LLVMContext context; + + /* The lifter Triton -> LLVM */ + triton::ast::TritonToLLVM lifter(context); + + /* Lift AST to LLVM IR */ + auto llvmModule = lifter.convert(node); + + /* Print the LLVM module into the stream */ + std::string dump; + llvm::raw_string_ostream llvmStream(dump); + llvmModule->print(llvmStream, nullptr); + stream << dump; + + return stream; + } + + }; /* lifters namespace */ + }; /* engines namespace */ +}; /* triton namespace */ diff --git a/src/libtriton/engines/lifters/liftingToPython.cpp b/src/libtriton/engines/lifters/liftingToPython.cpp new file mode 100644 index 000000000..00850d0fd --- /dev/null +++ b/src/libtriton/engines/lifters/liftingToPython.cpp @@ -0,0 +1,93 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#include +#include +#include + +#include +#include +#include + + + +namespace triton { + namespace engines { + namespace lifters { + + LiftingToPython::LiftingToPython(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic) + : astCtxt(astCtxt), symbolic(symbolic) { + } + + + void LiftingToPython::requiredFunctions(std::ostream& stream) { + stream << "def sx(bits, value):" << std::endl; + stream << " sign_bit = 1 << (bits - 1)" << std::endl; + stream << " return (value & (sign_bit - 1)) - (value & sign_bit)" << std::endl; + + stream << std::endl; + stream << "def rol(value, rot, bits):" << std::endl; + stream << " return ((value << rot) | (value >> (bits - rot))) & ((0b1 << bits) - 1)" << std::endl; + + stream << std::endl; + stream << "def ror(value, rot, bits):" << std::endl; + stream << " return ((value >> rot) | (value << (bits - rot))) & ((0b1 << bits) - 1)" << std::endl; + + stream << std::endl; + stream << "def forall(variables, expr):" << std::endl; + stream << " return True" << std::endl; + + stream << std::endl; + } + + + std::ostream& LiftingToPython::liftToPython(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr) { + /* Save the AST representation mode */ + triton::ast::representations::mode_e mode = this->astCtxt->getRepresentationMode(); + this->astCtxt->setRepresentationMode(triton::ast::representations::PYTHON_REPRESENTATION); + + /* Collect SSA form */ + auto ssa = this->symbolic->sliceExpressions(expr); + std::vector symExprs; + for (const auto& se : ssa) { + symExprs.push_back(se.first); + } + + /* Collect used symbolic variables */ + std::map symVars; + for (const auto& n : triton::ast::search(expr->getAst(), triton::ast::VARIABLE_NODE)) { + auto var = reinterpret_cast(n.get())->getSymbolicVariable(); + symVars[var->getId()] = var; + } + + /* Print required functions */ + this->requiredFunctions(stream); + + /* Print symbolic variables */ + for (const auto& var : symVars) { + auto n = this->astCtxt->declare(this->astCtxt->variable(var.second)); + this->astCtxt->print(stream, n.get()); + stream << std::endl; + } + + /* Sort SSA */ + std::sort(symExprs.begin(), symExprs.end()); + + /* Print symbolic expressions */ + for (const auto& id : symExprs) { + stream << ssa[id]->getFormattedExpression() << std::endl; + } + + /* Restore the AST representation mode */ + this->astCtxt->setRepresentationMode(mode); + + return stream; + } + + }; /* lifters namespace */ + }; /* engines namespace */ +}; /* triton namespace */ diff --git a/src/libtriton/engines/lifters/liftingToSMT.cpp b/src/libtriton/engines/lifters/liftingToSMT.cpp new file mode 100644 index 000000000..5f3e1dee8 --- /dev/null +++ b/src/libtriton/engines/lifters/liftingToSMT.cpp @@ -0,0 +1,101 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#include +#include +#include + +#include +#include +#include + + + +namespace triton { + namespace engines { + namespace lifters { + + LiftingToSMT::LiftingToSMT(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic) + : astCtxt(astCtxt), symbolic(symbolic) { + } + + + std::ostream& LiftingToSMT::liftToSMT(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_) { + /* Save the AST representation mode */ + triton::ast::representations::mode_e mode = this->astCtxt->getRepresentationMode(); + this->astCtxt->setRepresentationMode(triton::ast::representations::SMT_REPRESENTATION); + + /* Collect SSA form */ + auto ssa = this->symbolic->sliceExpressions(expr); + std::vector symExprs; + for (const auto& se : ssa) { + symExprs.push_back(se.first); + } + + /* Collect used symbolic variables */ + std::map symVars; + for (const auto& n : triton::ast::search(expr->getAst(), triton::ast::VARIABLE_NODE)) { + auto var = reinterpret_cast(n.get())->getSymbolicVariable(); + symVars[var->getId()] = var; + } + + /* Print symbolic variables */ + for (const auto& var : symVars) { + auto n = this->astCtxt->declare(this->astCtxt->variable(var.second)); + this->astCtxt->print(stream, n.get()); + stream << std::endl; + } + + /* Sort SSA */ + std::sort(symExprs.begin(), symExprs.end()); + if (assert_) { + /* The last node will be handled later to separate conjuncts */ + symExprs.pop_back(); + } + + /* Print symbolic expressions */ + for (const auto& id : symExprs) { + stream << ssa[id]->getFormattedExpression() << std::endl; + } + + if (assert_) { + /* Print conjuncts in separate asserts */ + std::vector exprs; + std::vector wl{expr->getAst()}; + + while (!wl.empty()) { + auto n = wl.back(); + wl.pop_back(); + + if (n->getType() != ast::LAND_NODE) { + exprs.push_back(n); + continue; + } + + for (const auto& child : n->getChildren()) { + wl.push_back(child); + } + } + + for (auto it = exprs.crbegin(); it != exprs.crend(); ++it) { + this->astCtxt->print(stream, this->astCtxt->assert_(*it).get()); + stream << std::endl; + } + + stream << "(check-sat)" << std::endl; + stream << "(get-model)" << std::endl; + } + + /* Restore the AST representation mode */ + this->astCtxt->setRepresentationMode(mode); + + return stream; + } + + }; /* lifters namespace */ + }; /* engines namespace */ +}; /* triton namespace */ diff --git a/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp b/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp index 3eba56c63..6ff3f2baa 100644 --- a/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp +++ b/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp @@ -210,7 +210,7 @@ namespace triton { triton::uint512 BitwuzlaSolver::evaluate(const triton::ast::SharedAbstractNode& node) const { if (node == nullptr) { - throw triton::exceptions::AstTranslations("BitwuzlaSolver::evaluate(): node cannot be null."); + throw triton::exceptions::AstLifting("BitwuzlaSolver::evaluate(): node cannot be null."); } auto bzla = bitwuzla_new(); diff --git a/src/libtriton/engines/solver/z3/z3Solver.cpp b/src/libtriton/engines/solver/z3/z3Solver.cpp index ef360cce9..c64b767af 100644 --- a/src/libtriton/engines/solver/z3/z3Solver.cpp +++ b/src/libtriton/engines/solver/z3/z3Solver.cpp @@ -239,7 +239,7 @@ namespace triton { triton::ast::SharedAbstractNode Z3Solver::simplify(const triton::ast::SharedAbstractNode& node) const { if (node == nullptr) - throw triton::exceptions::AstTranslations("Z3Solver::simplify(): node cannot be null."); + throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null."); try { triton::ast::TritonToZ3Ast z3Ast{false}; @@ -254,14 +254,14 @@ namespace triton { return snode; } catch (const z3::exception& e) { - throw triton::exceptions::AstTranslations(std::string("Z3Solver::evaluate(): ") + e.msg()); + throw triton::exceptions::AstLifting(std::string("Z3Solver::evaluate(): ") + e.msg()); } } triton::uint512 Z3Solver::evaluate(const triton::ast::SharedAbstractNode& node) const { if (node == nullptr) - throw triton::exceptions::AstTranslations("Z3Solver::simplify(): node cannot be null."); + throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null."); try { triton::ast::TritonToZ3Ast z3ast{true}; @@ -281,7 +281,7 @@ namespace triton { return res; } catch (const z3::exception& e) { - throw triton::exceptions::AstTranslations(std::string("Z3Solver::evaluate(): ") + e.msg()); + throw triton::exceptions::AstLifting(std::string("Z3Solver::evaluate(): ") + e.msg()); } } diff --git a/src/libtriton/engines/symbolic/symbolicEngine.cpp b/src/libtriton/engines/symbolic/symbolicEngine.cpp index 66f6765df..9be044194 100644 --- a/src/libtriton/engines/symbolic/symbolicEngine.cpp +++ b/src/libtriton/engines/symbolic/symbolicEngine.cpp @@ -479,74 +479,6 @@ namespace triton { } - /* Prints symbolic expression with used references and symbolic variables */ - std::ostream& SymbolicEngine::printSlicedExpressions(std::ostream& stream, const SharedSymbolicExpression& expr, bool assert_) { - /* Collect SSA form */ - auto ssa = this->sliceExpressions(expr); - std::vector symExprs; - for (const auto& se : ssa) { - symExprs.push_back(se.first); - } - - /* Collect used symbolic variables */ - std::map symVars; - for (const auto& n : ast::search(expr->getAst(), ast::VARIABLE_NODE)) { - auto var = reinterpret_cast(n.get())->getSymbolicVariable(); - symVars[var->getId()] = var; - } - - /* Print symbolic variables */ - for (const auto& var : symVars) { - auto n = this->astCtxt->declare(this->astCtxt->variable(var.second)); - this->astCtxt->print(stream, n.get()); - stream << std::endl; - } - - /* Sort SSA */ - std::sort(symExprs.begin(), symExprs.end()); - if (assert_) { - symExprs.pop_back(); - } - - /* Print symbolic expressions */ - for (const auto& id : symExprs) { - stream << ssa[id]->getFormattedExpression() << std::endl; - } - - if (assert_) { - /* Print conjuncts in separate asserts */ - std::vector exprs; - std::vector wl{expr->getAst()}; - - while (!wl.empty()) { - auto n = wl.back(); - wl.pop_back(); - - if (n->getType() != ast::LAND_NODE) { - exprs.push_back(n); - continue; - } - - for (const auto& child : n->getChildren()) { - wl.push_back(child); - } - } - - for (auto it = exprs.crbegin(); it != exprs.crend(); ++it) { - this->astCtxt->print(stream, this->astCtxt->assert_(*it).get()); - stream << std::endl; - } - - if (this->astCtxt->getRepresentationMode() == ast::representations::SMT_REPRESENTATION) { - stream << "(check-sat)" << std::endl; - stream << "(get-model)" << std::endl; - } - } - - return stream; - } - - /* Returns a list which contains all tainted expressions */ std::vector SymbolicEngine::getTaintedSymbolicExpressions(void) const { std::vector taintedExprs; diff --git a/src/libtriton/includes/triton/api.hpp b/src/libtriton/includes/triton/api.hpp index 28588ba78..f1fa8067c 100644 --- a/src/libtriton/includes/triton/api.hpp +++ b/src/libtriton/includes/triton/api.hpp @@ -17,6 +17,7 @@ #include #include #include +#include #include #include #include @@ -57,6 +58,9 @@ namespace triton { //! Raises an exception if the taint engine is not initialized. inline void checkTaint(void) const; + //! Raises an exception if the lifting engine is not initialized. + inline void checkLifting(void) const; + protected: //! The Callbacks interface. @@ -68,6 +72,9 @@ namespace triton { //! The modes. triton::modes::SharedModes modes; + //! The lifting engine. + triton::engines::lifters::LiftingEngine* lifting = nullptr; + //! The taint engine. triton::engines::taint::TaintEngine* taint = nullptr; @@ -273,11 +280,11 @@ namespace triton { /* AST Representation API ======================================================================== */ - //! [**AST representation api**] - Returns the AST representation mode as triton::ast::representations::mode_e. - TRITON_EXPORT triton::uint32 getAstRepresentationMode(void) const; + //! [**AST representation api**] - Returns the AST representation as triton::ast::representation_e. + TRITON_EXPORT triton::ast::representations::mode_e getAstRepresentationMode(void) const; - //! [**AST representation api**] - Sets the AST representation mode. - TRITON_EXPORT void setAstRepresentationMode(triton::uint32 mode); + //! [**AST representation api**] - Sets the AST representation. + TRITON_EXPORT void setAstRepresentationMode(triton::ast::representations::mode_e mode); @@ -487,9 +494,6 @@ namespace triton { //! [**symbolic api**] - Slices all expressions from a given one. TRITON_EXPORT std::unordered_map sliceExpressions(const triton::engines::symbolic::SharedSymbolicExpression& expr); - //! [**symbolic api**] - Prints symbolic expression with used references and symbolic variables in AST representation mode. If `assert_` is true, then (assert ). - TRITON_EXPORT std::ostream& printSlicedExpressions(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_=false); - //! [**symbolic api**] - Returns the list of the tainted symbolic expressions. TRITON_EXPORT std::vector getTaintedSymbolicExpressions(void) const; @@ -663,6 +667,22 @@ namespace triton { //! [**synthesizer api**] - Synthesizes a given node. If `constant` is true, performa a constant synthesis. If `opaque` is true, perform opaque constant synthesis. If `subexpr` is true, analyze children AST. TRITON_EXPORT triton::engines::synthesis::SynthesisResult synthesize(const triton::ast::SharedAbstractNode& node, bool constant=true, bool subexpr=true, bool opaque=false); + + + + /* Lifters engine API ================================================================================= */ + + //! [**lifting api**] - Lifts an AST and all its references to LLVM format. + TRITON_EXPORT std::ostream& liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node); + + //! [**lifting api**] - Lifts a symbolic expression and all its references to LLVM format. + TRITON_EXPORT std::ostream& liftToLLVM(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr); + + //! [**lifting api**] - Lifts a symbolic expression and all its references to Python format. + TRITON_EXPORT std::ostream& liftToPython(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr); + + //! [**lifting api**] - Lifts a symbolic expression and all its references to SMT format. If `assert_` is true, then (assert ). + TRITON_EXPORT std::ostream& liftToSMT(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_); }; /*! @} End of triton namespace */ diff --git a/src/libtriton/includes/triton/astContext.hpp b/src/libtriton/includes/triton/astContext.hpp index 1de3001d0..38c909115 100644 --- a/src/libtriton/includes/triton/astContext.hpp +++ b/src/libtriton/includes/triton/astContext.hpp @@ -327,12 +327,12 @@ namespace triton { TRITON_EXPORT const triton::uint512& getVariableValue(const std::string& name) const; //! Sets the representation mode for this astContext - TRITON_EXPORT void setRepresentationMode(triton::uint32 mode); + TRITON_EXPORT void setRepresentationMode(triton::ast::representations::mode_e mode); //! Gets the representations mode of this astContext - TRITON_EXPORT triton::uint32 getRepresentationMode(void) const; + TRITON_EXPORT triton::ast::representations::mode_e getRepresentationMode(void) const; - //! Prints the given node with this context representation + //! Prints the node according to the current representation mode. TRITON_EXPORT std::ostream& print(std::ostream& stream, AbstractNode* node); }; diff --git a/src/libtriton/includes/triton/astEnums.hpp b/src/libtriton/includes/triton/astEnums.hpp index 5e5122952..c1bd3ce17 100644 --- a/src/libtriton/includes/triton/astEnums.hpp +++ b/src/libtriton/includes/triton/astEnums.hpp @@ -92,9 +92,9 @@ namespace triton { //! All types of representation mode. enum mode_e { - SMT_REPRESENTATION, /*!< SMT representation */ - PYTHON_REPRESENTATION, /*!< Python representation */ - LAST_REPRESENTATION /*!< Must be the last item */ + SMT_REPRESENTATION = 0, /*!< SMT representation */ + PYTHON_REPRESENTATION = 1, /*!< Python representation */ + LAST_REPRESENTATION = 2, /*!< Must be the last item */ }; /*! @} End of representations namespace */ diff --git a/src/libtriton/includes/triton/astRepresentation.hpp b/src/libtriton/includes/triton/astRepresentation.hpp index 7465f932a..15a2ac01a 100644 --- a/src/libtriton/includes/triton/astRepresentation.hpp +++ b/src/libtriton/includes/triton/astRepresentation.hpp @@ -47,7 +47,7 @@ namespace triton { class AstRepresentation { protected: //! The representation mode. - triton::uint32 mode; + triton::ast::representations::mode_e mode; //! AstRepresentation interface. std::unique_ptr representations[triton::ast::representations::LAST_REPRESENTATION]; @@ -63,12 +63,12 @@ namespace triton { TRITON_EXPORT AstRepresentation& operator=(const AstRepresentation& other); //! Returns the representation mode. - TRITON_EXPORT triton::uint32 getMode(void) const; + TRITON_EXPORT triton::ast::representations::mode_e getMode(void) const; //! Sets the representation mode. - TRITON_EXPORT void setMode(triton::uint32 mode); + TRITON_EXPORT void setMode(triton::ast::representations::mode_e mode); - //! Displays the node according to the representation mode. + //! Prints the node according to the current representation mode. TRITON_EXPORT std::ostream& print(std::ostream& stream, AbstractNode* node); }; diff --git a/src/libtriton/includes/triton/config.hpp.in b/src/libtriton/includes/triton/config.hpp.in index f8eb4deb0..bb3ec8251 100644 --- a/src/libtriton/includes/triton/config.hpp.in +++ b/src/libtriton/includes/triton/config.hpp.in @@ -10,5 +10,6 @@ #cmakedefine TRITON_Z3_INTERFACE #cmakedefine TRITON_BITWUZLA_INTERFACE +#cmakedefine TRITON_LLVM_INTERFACE #endif // TRITON_CONFIG_HPP diff --git a/src/libtriton/includes/triton/exceptions.hpp b/src/libtriton/includes/triton/exceptions.hpp index 9c764f92f..84e60e9d8 100644 --- a/src/libtriton/includes/triton/exceptions.hpp +++ b/src/libtriton/includes/triton/exceptions.hpp @@ -168,6 +168,18 @@ namespace triton { }; + /*! \class LiftingEngine + * \brief The exception class used by the lifting engine. */ + class LiftingEngine : public triton::exceptions::Engines { + public: + //! Constructor. + TRITON_EXPORT LiftingEngine(const char* message) : triton::exceptions::Engines(message) {}; + + //! Constructor. + TRITON_EXPORT LiftingEngine(const std::string& message) : triton::exceptions::Engines(message) {}; + }; + + /*! \class SolverEngine * \brief The exception class used by the solver engine. */ class SolverEngine : public triton::exceptions::Engines { @@ -384,15 +396,15 @@ namespace triton { }; - /*! \class AstTranslations - * \brief The exception class used by all AST translations (`z3 <-> triton`). */ - class AstTranslations : public triton::exceptions::Ast { + /*! \class AstLifting + * \brief The exception class used by all AST lifting (e.g `z3 <-> triton`). */ + class AstLifting : public triton::exceptions::Ast { public: //! Constructor. - TRITON_EXPORT AstTranslations(const char* message) : triton::exceptions::Ast(message) {}; + TRITON_EXPORT AstLifting(const char* message) : triton::exceptions::Ast(message) {}; //! Constructor. - TRITON_EXPORT AstTranslations(const std::string& message) : triton::exceptions::Ast(message) {}; + TRITON_EXPORT AstLifting(const std::string& message) : triton::exceptions::Ast(message) {}; }; diff --git a/src/libtriton/includes/triton/liftingEngine.hpp b/src/libtriton/includes/triton/liftingEngine.hpp new file mode 100644 index 000000000..9b78bd56e --- /dev/null +++ b/src/libtriton/includes/triton/liftingEngine.hpp @@ -0,0 +1,74 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#ifndef TRITON_LIFTINGENGINE_HPP +#define TRITON_LIFTINGENGINE_HPP + +#include +#include +#include +#include +#include +#include + +#ifdef TRITON_LLVM_INTERFACE + #include +#endif + + + +//! The Triton namespace +namespace triton { +/*! + * \addtogroup triton + * @{ + */ + + //! The Engines namespace + namespace engines { + /*! + * \ingroup triton + * \addtogroup engines + * @{ + */ + + //! The Lifters namespace + namespace lifters { + /*! + * \ingroup engines + * \addtogroup lifters + * @{ + */ + + //! \class LiftingEngine + /*! \brief The lifting engine class. */ + class LiftingEngine + : public LiftingToSMT, + #ifdef TRITON_LLVM_INTERFACE + public LiftingToLLVM, + #endif + public LiftingToPython { + + public: + //! Constructor. + TRITON_EXPORT LiftingEngine(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic) + : LiftingToSMT(astCtxt, symbolic), + #ifdef TRITON_LLVM_INTERFACE + LiftingToLLVM(), + #endif + LiftingToPython(astCtxt, symbolic) { + }; + }; + + /*! @} End of lifters namespace */ + }; + /*! @} End of engines namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* TRITON_LIFTINGENGINE_HPP */ diff --git a/src/libtriton/includes/triton/liftingToLLVM.hpp b/src/libtriton/includes/triton/liftingToLLVM.hpp new file mode 100644 index 000000000..202df8cf1 --- /dev/null +++ b/src/libtriton/includes/triton/liftingToLLVM.hpp @@ -0,0 +1,68 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#ifndef TRITON_LIFTINGTOLLVM_HPP +#define TRITON_LIFTINGTOLLVM_HPP + +#include +#include +#include + +#include +#include + +#include +#include +#include + + + +//! The Triton namespace +namespace triton { +/*! + * \addtogroup triton + * @{ + */ + + //! The Engines namespace + namespace engines { + /*! + * \ingroup triton + * \addtogroup engines + * @{ + */ + + //! The Lifters namespace + namespace lifters { + /*! + * \ingroup engines + * \addtogroup lifters + * @{ + */ + + //! \class LiftingToLLVM + /*! \brief The lifting to LLVM class. */ + class LiftingToLLVM { + public: + //! Constructor. + TRITON_EXPORT LiftingToLLVM(); + + //! Lifts a symbolic expression and all its references to LLVM format. + TRITON_EXPORT std::ostream& liftToLLVM(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr); + + //! Lifts a abstract node and all its references to LLVM format. + TRITON_EXPORT std::ostream& liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node); + }; + + /*! @} End of lifters namespace */ + }; + /*! @} End of engines namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* TRITON_LIFTINGTOLLVM_HPP */ diff --git a/src/libtriton/includes/triton/liftingToPython.hpp b/src/libtriton/includes/triton/liftingToPython.hpp new file mode 100644 index 000000000..c0d25158f --- /dev/null +++ b/src/libtriton/includes/triton/liftingToPython.hpp @@ -0,0 +1,70 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#ifndef TRITON_LIFTINGTOPYTHON_HPP +#define TRITON_LIFTINGTOPYTHON_HPP + +#include + +#include +#include +#include + + + +//! The Triton namespace +namespace triton { +/*! + * \addtogroup triton + * @{ + */ + + //! The Engines namespace + namespace engines { + /*! + * \ingroup triton + * \addtogroup engines + * @{ + */ + + //! The Lifters namespace + namespace lifters { + /*! + * \ingroup engines + * \addtogroup lifters + * @{ + */ + + //! \class LiftingToPython + /*! \brief The lifting to Python class. */ + class LiftingToPython { + private: + //! Reference to the context managing ast nodes. + triton::ast::SharedAstContext astCtxt; + + //! Instance to the symbolic engine. + triton::engines::symbolic::SymbolicEngine* symbolic; + + //! Define required functions like ror, rol, sx and forall + void requiredFunctions(std::ostream& stream); + + public: + //! Constructor. + TRITON_EXPORT LiftingToPython(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic); + + //! Lifts a symbolic expression and all its references to Python format. + TRITON_EXPORT std::ostream& liftToPython(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr); + }; + + /*! @} End of lifters namespace */ + }; + /*! @} End of engines namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* TRITON_LIFTINGTOPYTHON_HPP */ diff --git a/src/libtriton/includes/triton/liftingToSMT.hpp b/src/libtriton/includes/triton/liftingToSMT.hpp new file mode 100644 index 000000000..aa67cbb77 --- /dev/null +++ b/src/libtriton/includes/triton/liftingToSMT.hpp @@ -0,0 +1,67 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#ifndef TRITON_LIFTINGTOSMT_HPP +#define TRITON_LIFTINGTOSMT_HPP + +#include + +#include +#include +#include + + + +//! The Triton namespace +namespace triton { +/*! + * \addtogroup triton + * @{ + */ + + //! The Engines namespace + namespace engines { + /*! + * \ingroup triton + * \addtogroup engines + * @{ + */ + + //! The Lifters namespace + namespace lifters { + /*! + * \ingroup engines + * \addtogroup lifters + * @{ + */ + + //! \class LiftingToSMT + /*! \brief The lifting to SMT class. */ + class LiftingToSMT { + private: + //! Reference to the context managing ast nodes. + triton::ast::SharedAstContext astCtxt; + + //! Instance to the symbolic engine. + triton::engines::symbolic::SymbolicEngine* symbolic; + + public: + //! Constructor. + TRITON_EXPORT LiftingToSMT(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic); + + //! Lifts a symbolic expression and all its references to SMT format. If `assert_` is true, then (assert ). + TRITON_EXPORT std::ostream& liftToSMT(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_); + }; + + /*! @} End of lifters namespace */ + }; + /*! @} End of engines namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* LIFTINGTOSMT_HPP */ diff --git a/src/libtriton/includes/triton/oracleEntry.hpp b/src/libtriton/includes/triton/oracleEntry.hpp index 5d87fb5cf..42399605e 100644 --- a/src/libtriton/includes/triton/oracleEntry.hpp +++ b/src/libtriton/includes/triton/oracleEntry.hpp @@ -5,8 +5,8 @@ ** This program is under the terms of the Apache License 2.0. */ -#ifndef ORACLEENTRY_HPP -#define ORACLEENTRY_HPP +#ifndef TRITON_ORACLEENTRY_HPP +#define TRITON_ORACLEENTRY_HPP #include #include @@ -54,7 +54,7 @@ namespace triton { //! Constructor TRITON_EXPORT ConstantEntry(triton::uint8 position, const triton::ast::SharedAbstractNode& op) - : position(position), op(op) { + : op(op), position(position) { }; }; @@ -161,4 +161,4 @@ namespace triton { /*! @} End of triton namespace */ }; -#endif /* ORACLEENTRY_HPP */ +#endif /* TRITON_ORACLEENTRY_HPP */ diff --git a/src/libtriton/includes/triton/symbolicEngine.hpp b/src/libtriton/includes/triton/symbolicEngine.hpp index 2ca759021..dbe2227a4 100644 --- a/src/libtriton/includes/triton/symbolicEngine.hpp +++ b/src/libtriton/includes/triton/symbolicEngine.hpp @@ -17,6 +17,7 @@ #include #include #include +#include #include #include #include @@ -260,9 +261,6 @@ namespace triton { //! Slices all expressions from a given one. TRITON_EXPORT std::unordered_map sliceExpressions(const SharedSymbolicExpression& expr); - //! Prints symbolic expression with used references and symbolic variables in AST representation mode. If `assert_` is true, then (assert ). - TRITON_EXPORT std::ostream& printSlicedExpressions(std::ostream& stream, const SharedSymbolicExpression& expr, bool assert_=false); - //! Returns the vector of the tainted symbolic expressions. TRITON_EXPORT std::vector getTaintedSymbolicExpressions(void) const; diff --git a/src/libtriton/includes/triton/synthesisResult.hpp b/src/libtriton/includes/triton/synthesisResult.hpp index c805df742..4a748d524 100644 --- a/src/libtriton/includes/triton/synthesisResult.hpp +++ b/src/libtriton/includes/triton/synthesisResult.hpp @@ -5,8 +5,8 @@ ** This program is under the terms of the Apache License 2.0. */ -#ifndef SYNTHESISRESULT_HPP -#define SYNTHESISRESULT_HPP +#ifndef TRITON_SYNTHESISRESULT_HPP +#define TRITON_SYNTHESISRESULT_HPP #include #include @@ -95,4 +95,4 @@ namespace triton { /*! @} End of triton namespace */ }; -#endif /* SYNTHESISRESULT_HPP */ +#endif /* TRITON_SYNTHESISRESULT_HPP */ diff --git a/src/libtriton/includes/triton/synthesizer.hpp b/src/libtriton/includes/triton/synthesizer.hpp index 7b558cf59..56dfce5d7 100644 --- a/src/libtriton/includes/triton/synthesizer.hpp +++ b/src/libtriton/includes/triton/synthesizer.hpp @@ -5,8 +5,8 @@ ** This program is under the terms of the Apache License 2.0. */ -#ifndef SYNTHESIZER_HPP -#define SYNTHESIZER_HPP +#ifndef TRITON_SYNTHESIZER_HPP +#define TRITON_SYNTHESIZER_HPP #include #include @@ -117,4 +117,4 @@ namespace triton { /*! @} End of triton namespace */ }; -#endif /* SYNTHESIZER_HPP */ +#endif /* TRITON_SYNTHESIZER_HPP */ diff --git a/src/libtriton/includes/triton/tritonToLLVM.hpp b/src/libtriton/includes/triton/tritonToLLVM.hpp new file mode 100644 index 000000000..09f2c7e81 --- /dev/null +++ b/src/libtriton/includes/triton/tritonToLLVM.hpp @@ -0,0 +1,74 @@ +//! \file +/* +** Copyright (C) - Triton +** +** This program is under the terms of the Apache License 2.0. +*/ + +#ifndef TRITON_TRITONTOLLVM_HPP +#define TRITON_TRITONTOLLVM_HPP + +#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 TritonToLLVM + /*! \brief Converts a Triton's AST to LVM IR. */ + class TritonToLLVM { + private: + //! The LLVM context + llvm::LLVMContext& llvmContext; + + //! The LLVM module + std::shared_ptr llvmModule; + + //! The LLVM IR builder + llvm::IRBuilder<> llvmIR; + + //! Map Triton variables to LLVM ones + std::map llvmVars; + + //! Create a LLVM function + void createFunction(const triton::ast::SharedAbstractNode& node); + + //! Converts Triton AST to LLVM IR + llvm::Value* do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map* results); + + public: + //! Constructor. + 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); + }; + + /*! @} End of ast namespace */ + }; +/*! @} End of triton namespace */ +}; + +#endif /* TRITON_TRITONTOLLVM_HPP */ diff --git a/src/testers/unittests/test_ast_representation.py b/src/testers/unittests/test_ast_representation.py index 816666569..e12dcf384 100644 --- a/src/testers/unittests/test_ast_representation.py +++ b/src/testers/unittests/test_ast_representation.py @@ -4,7 +4,31 @@ import unittest -from triton import TritonContext, ARCH, AST_REPRESENTATION +from triton import TritonContext, ARCH, AST_REPRESENTATION, VERSION + + +smtlifting = """(declare-fun SymVar_0 () (_ BitVec 8)) +(declare-fun SymVar_1 () (_ BitVec 8)) +(define-fun ref!0 () (_ BitVec 8) (bvadd SymVar_0 SymVar_1)) ; ref test +""" + +pythonlifting = """def sx(bits, value): + sign_bit = 1 << (bits - 1) + return (value & (sign_bit - 1)) - (value & sign_bit) + +def rol(value, rot, bits): + return ((value << rot) | (value >> (bits - rot))) & ((0b1 << bits) - 1) + +def ror(value, rot, bits): + return ((value >> rot) | (value << (bits - rot))) & ((0b1 << bits) - 1) + +def forall(variables, expr): + return True + +SymVar_0 = int(input()) +SymVar_1 = int(input()) +ref_0 = ((SymVar_0 + SymVar_1) & 0xff) # ref test +""" class TestAstRepresentation(unittest.TestCase): @@ -13,88 +37,145 @@ class TestAstRepresentation(unittest.TestCase): def setUp(self): """Define the arch.""" - self.Triton = TritonContext() - self.Triton.setArchitecture(ARCH.X86_64) - self.astCtxt = self.Triton.getAstContext() + self.ctx = TritonContext(ARCH.X86_64) + self.ast = self.ctx.getAstContext() - self.v1 = self.astCtxt.variable(self.Triton.newSymbolicVariable(8)) - self.v2 = self.astCtxt.variable(self.Triton.newSymbolicVariable(8)) - self.ref = self.Triton.newSymbolicExpression(self.v1 + self.v2, "ref test") + self.v1 = self.ast.variable(self.ctx.newSymbolicVariable(8)) + self.v2 = self.ast.variable(self.ctx.newSymbolicVariable(8)) + self.ref = self.ctx.newSymbolicExpression(self.v1 + self.v2, "ref test") # Default - self.assertEqual(self.Triton.getAstRepresentationMode(), AST_REPRESENTATION.SMT) + self.assertEqual(self.ctx.getAstRepresentationMode(), AST_REPRESENTATION.SMT) self.node = [ - # Overloaded operators # SMT # Python - ((self.v1 & self.v2), "(bvand SymVar_0 SymVar_1)", "(SymVar_0 & SymVar_1)"), - ((self.v1 + self.v2), "(bvadd SymVar_0 SymVar_1)", "((SymVar_0 + SymVar_1) & 0xFF)"), - ((self.v1 - self.v2), "(bvsub SymVar_0 SymVar_1)", "((SymVar_0 - SymVar_1) & 0xFF)"), - ((self.v1 ^ self.v2), "(bvxor SymVar_0 SymVar_1)", "(SymVar_0 ^ SymVar_1)"), - ((self.v1 | self.v2), "(bvor SymVar_0 SymVar_1)", "(SymVar_0 | SymVar_1)"), - ((self.v1 * self.v2), "(bvmul SymVar_0 SymVar_1)", "((SymVar_0 * SymVar_1) & 0xFF)"), - ((self.v1 / self.v2), "(bvudiv SymVar_0 SymVar_1)", "(SymVar_0 / SymVar_1)"), - ((self.v1 % self.v2), "(bvurem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), - ((self.v1 << self.v2), "(bvshl SymVar_0 SymVar_1)", "((SymVar_0 << SymVar_1) & 0xFF)"), - ((self.v1 >> self.v2), "(bvlshr SymVar_0 SymVar_1)", "(SymVar_0 >> SymVar_1)"), - ((~self.v1), "(bvnot SymVar_0)", "(~(SymVar_0) & 0xFF)"), - ((-self.v1), "(bvneg SymVar_0)", "(-(symvar_0) & 0xff)"), - ((self.v1 == self.v2), "(= SymVar_0 SymVar_1)", "(SymVar_0 == SymVar_1)"), - ((self.v1 != self.v2), "(not (= SymVar_0 SymVar_1))", "not (SymVar_0 == SymVar_1)"), - ((self.v1 <= self.v2), "(bvule SymVar_0 SymVar_1)", "(SymVar_0 <= SymVar_1)"), - ((self.v1 >= self.v2), "(bvuge SymVar_0 SymVar_1)", "(SymVar_0 >= SymVar_1)"), - ((self.v1 < self.v2), "(bvult SymVar_0 SymVar_1)", "(SymVar_0 < SymVar_1)"), - ((self.v1 > self.v2), "(bvugt SymVar_0 SymVar_1)", "(SymVar_0 > SymVar_1)"), + # Overloaded operators # SMT # Python + ((self.v1 & self.v2), "(bvand SymVar_0 SymVar_1)", "(SymVar_0 & SymVar_1)"), + ((self.v1 + self.v2), "(bvadd SymVar_0 SymVar_1)", "((SymVar_0 + SymVar_1) & 0xFF)"), + ((self.v1 - self.v2), "(bvsub SymVar_0 SymVar_1)", "((SymVar_0 - SymVar_1) & 0xFF)"), + ((self.v1 ^ self.v2), "(bvxor SymVar_0 SymVar_1)", "(SymVar_0 ^ SymVar_1)"), + ((self.v1 | self.v2), "(bvor SymVar_0 SymVar_1)", "(SymVar_0 | SymVar_1)"), + ((self.v1 * self.v2), "(bvmul SymVar_0 SymVar_1)", "((SymVar_0 * SymVar_1) & 0xFF)"), + ((self.v1 / self.v2), "(bvudiv SymVar_0 SymVar_1)", "(SymVar_0 / SymVar_1)"), + ((self.v1 % self.v2), "(bvurem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), + ((self.v1 << self.v2), "(bvshl SymVar_0 SymVar_1)", "((SymVar_0 << SymVar_1) & 0xFF)"), + ((self.v1 >> self.v2), "(bvlshr SymVar_0 SymVar_1)", "(SymVar_0 >> SymVar_1)"), + ((~self.v1), "(bvnot SymVar_0)", "(~(SymVar_0) & 0xFF)"), + ((-self.v1), "(bvneg SymVar_0)", "(-(symvar_0) & 0xff)"), + ((self.v1 == self.v2), "(= SymVar_0 SymVar_1)", "(SymVar_0 == SymVar_1)"), + ((self.v1 != self.v2), "(not (= SymVar_0 SymVar_1))", "not (SymVar_0 == SymVar_1)"), + ((self.v1 <= self.v2), "(bvule SymVar_0 SymVar_1)", "(SymVar_0 <= SymVar_1)"), + ((self.v1 >= self.v2), "(bvuge SymVar_0 SymVar_1)", "(SymVar_0 >= SymVar_1)"), + ((self.v1 < self.v2), "(bvult SymVar_0 SymVar_1)", "(SymVar_0 < SymVar_1)"), + ((self.v1 > self.v2), "(bvugt SymVar_0 SymVar_1)", "(SymVar_0 > SymVar_1)"), # AST api # SMT # Python - (self.astCtxt.assert_(self.v1 == 0), "(assert (= SymVar_0 (_ bv0 8)))", "assert_((SymVar_0 == 0x0))"), - (self.astCtxt.bv(2, 8), "(_ bv2 8)", "0x2"), - (self.astCtxt.bvashr(self.v1, self.v2), "(bvashr SymVar_0 SymVar_1)", "(SymVar_0 >> SymVar_1)"), - (self.astCtxt.bvfalse(), "(_ bv0 1)", "0x0"), - (self.astCtxt.bvnand(self.v1, self.v2), "(bvnand SymVar_0 SymVar_1)", "(~(SymVar_0 & SymVar_1) & 0xFF)"), - (self.astCtxt.bvnor(self.v1, self.v2), "(bvnor SymVar_0 SymVar_1)", "(~(SymVar_0 | SymVar_1) & 0xFF)"), - (self.astCtxt.bvrol(self.v1, self.astCtxt.bv(3, 8)), "((_ rotate_left 3) SymVar_0)", "rol(SymVar_0, 0x3)"), - (self.astCtxt.bvror(self.v2, self.astCtxt.bv(2, 8)), "((_ rotate_right 2) SymVar_1)", "ror(SymVar_1, 0x2)"), - (self.astCtxt.bvsdiv(self.v1, self.v2), "(bvsdiv SymVar_0 SymVar_1)", "(SymVar_0 / SymVar_1)"), - (self.astCtxt.bvsge(self.v1, self.v2), "(bvsge SymVar_0 SymVar_1)", "(SymVar_0 >= SymVar_1)"), - (self.astCtxt.bvsgt(self.v1, self.v2), "(bvsgt SymVar_0 SymVar_1)", "(SymVar_0 > SymVar_1)"), - (self.astCtxt.bvsle(self.v1, self.v2), "(bvsle SymVar_0 SymVar_1)", "(SymVar_0 <= SymVar_1)"), - (self.astCtxt.bvslt(self.v1, self.v2), "(bvslt SymVar_0 SymVar_1)", "(SymVar_0 < SymVar_1)"), - (self.astCtxt.bvsmod(self.v1, self.v2), "(bvsmod SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), - (self.astCtxt.bvsrem(self.v1, self.v2), "(bvsrem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), - (self.astCtxt.bvtrue(), "(_ bv1 1)", "0x1"), - (self.astCtxt.bvurem(self.v1, self.v2), "(bvurem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), - (self.astCtxt.bvxnor(self.v1, self.v2), "(bvxnor SymVar_0 SymVar_1)", "(~(SymVar_0 ^ SymVar_1) & 0xFF)"), - (self.astCtxt.compound([self.v1, self.v2]), "SymVar_0\nSymVar_1", "SymVar_0\nSymVar_1"), - (self.astCtxt.concat([self.v1, self.v2]), "(concat SymVar_0 SymVar_1)", "((SymVar_0) << 8 | SymVar_1)"), - (self.astCtxt.declare(self.v1), "(declare-fun SymVar_0 () (_ BitVec 8))", "SymVar_0 = 0xdeadbeef"), - (self.astCtxt.distinct(self.v1, self.v2), "(distinct SymVar_0 SymVar_1)", "(SymVar_0 != SymVar_1)"), - (self.astCtxt.equal(self.v1, self.v2), "(= SymVar_0 SymVar_1)", "(SymVar_0 == SymVar_1)"), - (self.astCtxt.extract(4, 2, self.v1), "((_ extract 4 2) SymVar_0)", "((SymVar_0 >> 2) & 0x7)"), - (self.astCtxt.extract(6, 0, self.v1), "((_ extract 6 0) SymVar_0)", "(SymVar_0 & 0x7F)"), - (self.astCtxt.extract(7, 0, self.v1), "SymVar_0", "SymVar_0"), - (self.astCtxt.iff(self.v1 == 1, self.v2 == 2), "(iff (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2)) or (not (SymVar_0 == 0x1) and not (SymVar_1 == 0x2))"), - (self.astCtxt.ite(self.v1 == 1, self.v1, self.v2), "(ite (= SymVar_0 (_ bv1 8)) SymVar_0 SymVar_1)", "(SymVar_0 if (SymVar_0 == 0x1) else SymVar_1)"), - (self.astCtxt.land([self.v1 == 1, self.v2 == 2]), "(and (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2))"), - (self.astCtxt.let("alias", self.v1, self.v2), "(let ((alias SymVar_0)) SymVar_1)", "SymVar_1"), - (self.astCtxt.lnot(self.v1 == 0), "(not (= SymVar_0 (_ bv0 8)))", "not (SymVar_0 == 0x0)"), - (self.astCtxt.lor([self.v1 >= 0, self.v2 <= 10]), "(or (bvuge SymVar_0 (_ bv0 8)) (bvule SymVar_1 (_ bv10 8)))", "((SymVar_0 >= 0x0) or (SymVar_1 <= 0xA))"), - (self.astCtxt.lxor([self.v1 >= 0, self.v2 <= 10]), "(xor (bvuge SymVar_0 (_ bv0 8)) (bvule SymVar_1 (_ bv10 8)))", "(bool((SymVar_0 >= 0x0)) != bool((SymVar_1 <= 0xA)))"), - (self.astCtxt.reference(self.ref), "ref!0", "ref_0"), - (self.astCtxt.string("test"), "test", "test"), - (self.astCtxt.sx(8, self.v1), "((_ sign_extend 8) SymVar_0)", "sx(0x8, SymVar_0)"), - (self.astCtxt.zx(8, self.v1), "((_ zero_extend 8) SymVar_0)", "SymVar_0"), - (self.astCtxt.forall([self.v1], 1 == self.v1), "(forall ((SymVar_0 (_ BitVec 8))) (= SymVar_0 (_ bv1 8)))", "forall([symvar_0], (symvar_0 == 0x1))"), + (self.ast.assert_(self.v1 == 0), "(assert (= SymVar_0 (_ bv0 8)))", "assert ((SymVar_0 == 0x0))"), + (self.ast.bv(2, 8), "(_ bv2 8)", "0x2"), + (self.ast.bvashr(self.v1, self.v2), "(bvashr SymVar_0 SymVar_1)", "(SymVar_0 >> SymVar_1)"), + (self.ast.bvfalse(), "(_ bv0 1)", "0x0"), + (self.ast.bvnand(self.v1, self.v2), "(bvnand SymVar_0 SymVar_1)", "(~(SymVar_0 & SymVar_1) & 0xFF)"), + (self.ast.bvnor(self.v1, self.v2), "(bvnor SymVar_0 SymVar_1)", "(~(SymVar_0 | SymVar_1) & 0xFF)"), + (self.ast.bvrol(self.v1, self.ast.bv(3, 8)), "((_ rotate_left 3) SymVar_0)", "rol(SymVar_0, 0x3, 8)"), + (self.ast.bvror(self.v2, self.ast.bv(2, 8)), "((_ rotate_right 2) SymVar_1)", "ror(SymVar_1, 0x2, 8)"), + (self.ast.bvsdiv(self.v1, self.v2), "(bvsdiv SymVar_0 SymVar_1)", "(SymVar_0 / SymVar_1)"), + (self.ast.bvsge(self.v1, self.v2), "(bvsge SymVar_0 SymVar_1)", "(SymVar_0 >= SymVar_1)"), + (self.ast.bvsgt(self.v1, self.v2), "(bvsgt SymVar_0 SymVar_1)", "(SymVar_0 > SymVar_1)"), + (self.ast.bvsle(self.v1, self.v2), "(bvsle SymVar_0 SymVar_1)", "(SymVar_0 <= SymVar_1)"), + (self.ast.bvslt(self.v1, self.v2), "(bvslt SymVar_0 SymVar_1)", "(SymVar_0 < SymVar_1)"), + (self.ast.bvsmod(self.v1, self.v2), "(bvsmod SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), + (self.ast.bvsrem(self.v1, self.v2), "(bvsrem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), + (self.ast.bvtrue(), "(_ bv1 1)", "0x1"), + (self.ast.bvurem(self.v1, self.v2), "(bvurem SymVar_0 SymVar_1)", "(SymVar_0 % SymVar_1)"), + (self.ast.bvxnor(self.v1, self.v2), "(bvxnor SymVar_0 SymVar_1)", "(~(SymVar_0 ^ SymVar_1) & 0xFF)"), + (self.ast.compound([self.v1, self.v2]), "SymVar_0\nSymVar_1", "SymVar_0\nSymVar_1"), + (self.ast.concat([self.v1, self.v2]), "(concat SymVar_0 SymVar_1)", "((SymVar_0) << 8 | SymVar_1)"), + (self.ast.declare(self.v1), "(declare-fun SymVar_0 () (_ BitVec 8))", "SymVar_0 = int(input())"), + (self.ast.distinct(self.v1, self.v2), "(distinct SymVar_0 SymVar_1)", "(SymVar_0 != SymVar_1)"), + (self.ast.equal(self.v1, self.v2), "(= SymVar_0 SymVar_1)", "(SymVar_0 == SymVar_1)"), + (self.ast.extract(4, 2, self.v1), "((_ extract 4 2) SymVar_0)", "((SymVar_0 >> 2) & 0x7)"), + (self.ast.extract(6, 0, self.v1), "((_ extract 6 0) SymVar_0)", "(SymVar_0 & 0x7F)"), + (self.ast.extract(7, 0, self.v1), "SymVar_0", "SymVar_0"), + (self.ast.iff(self.v1 == 1, self.v2 == 2), "(iff (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2)) or (not (SymVar_0 == 0x1) and not (SymVar_1 == 0x2))"), + (self.ast.ite(self.v1 == 1, self.v1, self.v2), "(ite (= SymVar_0 (_ bv1 8)) SymVar_0 SymVar_1)", "(SymVar_0 if (SymVar_0 == 0x1) else SymVar_1)"), + (self.ast.land([self.v1 == 1, self.v2 == 2]), "(and (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2))"), + (self.ast.let("alias", self.v1, self.v2), "(let ((alias SymVar_0)) SymVar_1)", "SymVar_1"), + (self.ast.lnot(self.v1 == 0), "(not (= SymVar_0 (_ bv0 8)))", "not (SymVar_0 == 0x0)"), + (self.ast.lor([self.v1 >= 0, self.v2 <= 10]), "(or (bvuge SymVar_0 (_ bv0 8)) (bvule SymVar_1 (_ bv10 8)))", "((SymVar_0 >= 0x0) or (SymVar_1 <= 0xA))"), + (self.ast.lxor([self.v1 >= 0, self.v2 <= 10]), "(xor (bvuge SymVar_0 (_ bv0 8)) (bvule SymVar_1 (_ bv10 8)))", "(bool((SymVar_0 >= 0x0)) != bool((SymVar_1 <= 0xA)))"), + (self.ast.reference(self.ref), "ref!0", "ref_0"), + (self.ast.string("test"), "test", "test"), + (self.ast.sx(8, self.v1), "((_ sign_extend 8) SymVar_0)", "sx(0x8, SymVar_0)"), + (self.ast.zx(8, self.v1), "((_ zero_extend 8) SymVar_0)", "SymVar_0"), + (self.ast.forall([self.v1], 1 == self.v1), "(forall ((SymVar_0 (_ BitVec 8))) (= SymVar_0 (_ bv1 8)))", "forall([symvar_0], (symvar_0 == 0x1))"), ] def test_smt_representation(self): - self.Triton.setAstRepresentationMode(AST_REPRESENTATION.SMT) - self.assertEqual(self.Triton.getAstRepresentationMode(), AST_REPRESENTATION.SMT) + self.ctx.setAstRepresentationMode(AST_REPRESENTATION.SMT) + self.assertEqual(self.ctx.getAstRepresentationMode(), AST_REPRESENTATION.SMT) for n in self.node: self.assertEqual(str(n[0]), n[1]) def test_python_representation(self): - self.Triton.setAstRepresentationMode(AST_REPRESENTATION.PYTHON) - self.assertEqual(self.Triton.getAstRepresentationMode(), AST_REPRESENTATION.PYTHON) + self.ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON) + self.assertEqual(self.ctx.getAstRepresentationMode(), AST_REPRESENTATION.PYTHON) for n in self.node: # Note: lower() in order to handle boost-1.55 (from travis) and boost-1.71 (from an up-to-date machine) self.assertEqual(str(n[0]).lower(), n[2].lower()) + + def test_lifting(self): + self.assertEqual(self.ctx.liftToSMT(self.ref), smtlifting) + self.assertEqual(self.ctx.liftToPython(self.ref), pythonlifting) + + if VERSION.LLVM_INTERFACE is True: + nodes = [ + (self.v1 & self.v2), + (self.v1 + self.v2), + (self.v1 - self.v2), + (self.v1 ^ self.v2), + (self.v1 | self.v2), + (self.v1 * self.v2), + (self.v1 / self.v2), + (self.v1 % self.v2), + (self.v1 << self.v2), + (self.v1 >> self.v2), + (~self.v1), + (-self.v1), + (self.v1 == self.v2), + (self.v1 != self.v2), + (self.v1 <= self.v2), + (self.v1 >= self.v2), + (self.v1 < self.v2), + (self.v1 > self.v2), + self.ast.bv(2, 8), + self.ast.bvashr(self.v1, self.v2), + self.ast.bvnand(self.v1, self.v2), + self.ast.bvnor(self.v1, self.v2), + self.ast.bvrol(self.v1, self.ast.bv(3, 8)), + self.ast.bvror(self.v2, self.ast.bv(2, 8)), + self.ast.bvsdiv(self.v1, self.v2), + self.ast.bvsge(self.v1, self.v2), + self.ast.bvsgt(self.v1, self.v2), + self.ast.bvsle(self.v1, self.v2), + self.ast.bvslt(self.v1, self.v2), + self.ast.bvsmod(self.v1, self.v2), + self.ast.bvsrem(self.v1, self.v2), + self.ast.bvurem(self.v1, self.v2), + self.ast.bvxnor(self.v1, self.v2), + self.ast.concat([self.v1, self.v2]), + self.ast.distinct(self.v1, self.v2), + self.ast.equal(self.v1, self.v2), + self.ast.extract(4, 2, self.v1), + self.ast.extract(6, 0, self.v1), + self.ast.extract(7, 0, self.v1), + self.ast.ite(self.v1 == 1, self.v1, self.v2), + self.ast.land([self.v1 == 1, self.v2 == 2]), + self.ast.lnot(self.v1 == 0), + self.ast.lor([self.v1 >= 0, self.v2 <= 10]), + self.ast.lxor([self.v1 >= 0, self.v2 <= 10]), + self.ast.reference(self.ref), + self.ast.sx(8, self.v1), + self.ast.zx(8, self.v1), + ] + + for n in nodes: + self.assertNotEqual(len(self.ctx.liftToLLVM(n)), 0)