Skip to content

Commit

Permalink
Add a new class: LLVMToTriton (#1078)
Browse files Browse the repository at this point in the history 
We also renamed some files:

* src/libtriton/ast/bitwuzla/tritonToBitwuzlaAst.cpp    -> src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp
* src/libtriton/ast/z3/tritonToZ3Ast.cpp                -> src/libtriton/ast/z3/tritonToZ3.cpp
* src/libtriton/ast/z3/z3ToTritonAst.cpp                -> src/libtriton/ast/z3/z3ToTriton.cpp
* src/libtriton/includes/triton/tritonToBitwuzlaAst.hpp -> src/libtriton/includes/triton/tritonToBitwuzla.hpp
* src/libtriton/includes/triton/tritonToZ3Ast.hpp       -> src/libtriton/includes/triton/tritonToZ3.hpp
* src/libtriton/includes/triton/z3ToTritonAst.hpp       -> src/libtriton/includes/triton/z3ToTriton.hpp

As well as classes:

* TritonToZ3Ast         -> TritonToZ3
* Z3ToTritonAst         -> Z3ToTriton
* TritonToBitwuzlaAst   -> TritonToBitwuzla
  • Loading branch information
@JonathanSalwan
JonathanSalwan committed Feb 2, 2022
1 parent aa1dbb5 commit 9a6f208
Show file tree
Hide file tree
Showing 20 changed files with 526 additions and 126 deletions.
1 change: 1 addition & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ Triton relies on the following dependencies:
* libcapstone >= 4.0.x https://github.com/capstone-engine/capstone
* libz3 (optional) >= 4.6.0 https://github.com/Z3Prover/z3
* libbitwuzla (optional) n/a https://github.com/bitwuzla/bitwuzla
* llvm (optional) >= 12
```


Expand Down
114 changes: 110 additions & 4 deletions src/examples/cpp/ctest_api.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,13 @@

#include <iostream>
#include <sstream>
#include <list>

#include <triton/aarch64Cpu.hpp>
#include <triton/aarch64Specifications.hpp>
#include <triton/api.hpp>
#include <triton/bitsVector.hpp>
#include <triton/config.hpp>
#include <triton/exceptions.hpp>
#include <triton/immediate.hpp>
#include <triton/instruction.hpp>
Expand All @@ -14,8 +18,12 @@
#include <triton/x8664Cpu.hpp>
#include <triton/x86Cpu.hpp>
#include <triton/x86Specifications.hpp>
#include <triton/aarch64Cpu.hpp>
#include <triton/aarch64Specifications.hpp>

#ifdef TRITON_LLVM_INTERFACE
#include <triton/tritonToLLVM.hpp>
#include <triton/llvmToTriton.hpp>
#endif



int test_1(void) {
Expand Down Expand Up @@ -469,8 +477,7 @@ int test_9(void) {
api.setArchitecture(triton::arch::ARCH_X86_64);

triton::engines::symbolic::PathConstraint pco;
auto node = api.getAstContext()->equal(
api.getAstContext()->bvtrue(), api.getAstContext()->bvtrue());
auto node = api.getAstContext()->equal(api.getAstContext()->bvtrue(), api.getAstContext()->bvtrue());
pco.addBranchConstraint(false, 0x123, 0x100, node);
pco.addBranchConstraint(true, 0x123, 0x200, node);
pco.addBranchConstraint(false, 0x123, 0x300, node);
Expand Down Expand Up @@ -517,6 +524,100 @@ int test_9(void) {
}


#ifdef TRITON_LLVM_INTERFACE
bool smt_proof(triton::API& ctx, const triton::ast::SharedAbstractNode& node1, const triton::ast::SharedAbstractNode& node2) {
auto actx = ctx.getAstContext();
if (ctx.isSat(actx->distinct(node1, node2)) == false)
return true;
return false;
}


int test_10(void) {
triton::API ctx(triton::arch::ARCH_X86_64);
auto actx = ctx.getAstContext();
auto varx = ctx.newSymbolicVariable(8, "x");

std::list<triton::ast::SharedAbstractNode> nodes = {
/* bitvector */
actx->bvadd(actx->bv(10, 8), actx->variable(varx)),
actx->bvadd(actx->variable(varx), actx->bv(11, 8)),
actx->bvand(actx->bv(12, 8), actx->variable(varx)),
actx->bvashr(actx->bv(13, 8), actx->variable(varx)),
actx->bvlshr(actx->bv(14, 8), actx->variable(varx)),
actx->bvmul(actx->bv(15, 8), actx->variable(varx)),
actx->bvnand(actx->bv(16, 8), actx->variable(varx)),
actx->bvneg(actx->bv(17, 8)),
actx->bvneg(actx->variable(varx)),
actx->bvnor(actx->bv(18, 8), actx->variable(varx)),
actx->bvnot(actx->bv(19, 8)),
actx->bvnot(actx->variable(varx)),
actx->bvor(actx->bv(20, 8), actx->variable(varx)),
actx->bvrol(actx->variable(varx), actx->bv(21, 8)),
actx->bvror(actx->variable(varx), actx->bv(22, 8)),
actx->bvsdiv(actx->variable(varx), actx->bv(23, 8)),
actx->bvshl(actx->variable(varx), actx->bv(24, 8)),
actx->bvsmod(actx->variable(varx), actx->bv(25, 8)),
actx->bvsrem(actx->variable(varx), actx->bv(26, 8)),
actx->bvsub(actx->bv(27, 8), actx->variable(varx)),
actx->bvudiv(actx->variable(varx), actx->bv(28, 8)),
actx->bvurem(actx->variable(varx), actx->bv(29, 8)),
actx->bvxnor(actx->bv(30, 8), actx->variable(varx)),
actx->bvxor(actx->bv(31, 8), actx->variable(varx)),
actx->sx(24, actx->variable(varx)),
actx->sx(8, actx->variable(varx)),
actx->zx(24, actx->variable(varx)),
actx->zx(8, actx->variable(varx)),

/* logical */
actx->equal(actx->bv(32, 8), actx->variable(varx)),
actx->distinct(actx->bv(33, 8), actx->variable(varx)),
actx->bvsge(actx->bv(34, 8), actx->variable(varx)),
actx->bvsgt(actx->bv(35, 8), actx->variable(varx)),
actx->bvsle(actx->bv(36, 8), actx->variable(varx)),
actx->bvslt(actx->bv(37, 8), actx->variable(varx)),
actx->bvuge(actx->bv(38, 8), actx->variable(varx)),
actx->bvugt(actx->bv(39, 8), actx->variable(varx)),
actx->bvule(actx->bv(40, 8), actx->variable(varx)),
actx->land(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))),
actx->lor(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))),
actx->lxor(actx->equal(actx->bv(10, 8), actx->variable(varx)), actx->bvsge(actx->bv(10, 8), actx->variable(varx))),

/* misc */
actx->concat(actx->concat(actx->concat(actx->bv(50, 8), actx->variable(varx)), actx->bv(0xff, 8)), actx->variable(varx)),
actx->extract(11, 4, actx->concat(actx->bv(0xff, 8), actx->variable(varx))),
actx->ite(actx->equal(actx->bv(52, 8), actx->bv(60, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(1, 8))),
actx->ite(actx->equal(actx->bv(53, 8), actx->bv(61, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(2, 8))),
actx->ite(actx->bvsge(actx->bv(54, 8), actx->bv(62, 8)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(3, 8))),
actx->ite(actx->bvslt(actx->bv(55, 8), actx->variable(varx)), actx->variable(varx), actx->bvadd(actx->variable(varx), actx->bv(4, 8))),
};

for (const auto& node : nodes) {
/* Triton to LLVM */
llvm::LLVMContext llvmContext;
triton::ast::TritonToLLVM ttllvm(llvmContext);
auto llvmModule = ttllvm.convert(node);
std::cerr << "IN: " << node << std::endl;

/* LLVM to Triton */
triton::ast::LLVMToTriton llvmtt(actx);
auto nout = llvmtt.convert(llvmModule.get());
std::cerr << "OUT: " << nout << std::endl;

if (smt_proof(ctx, node, nout) == false) {
std::cerr << "Node not equal" << std::endl;
std::cerr << "IN: " << node << std::endl;
std::cerr << "OUT: " << nout << std::endl;
return 1;
}
}

std::cout << "test_10: OK" << std::endl;
return 0;
}
#endif


int main(int ac, const char **av) {
if (test_1())
return 1;
Expand Down Expand Up @@ -545,5 +646,10 @@ int main(int ac, const char **av) {
if (test_9())
return 1;

#ifdef TRITON_LLVM_INTERFACE
if (test_10())
return 1;
#endif

return 0;
}
14 changes: 8 additions & 6 deletions src/libtriton/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ set(LIBTRITON_HEADER_FILES
includes/triton/liftingToLLVM.hpp
includes/triton/liftingToPython.hpp
includes/triton/liftingToSMT.hpp
includes/triton/llvmToTriton.hpp
includes/triton/memoryAccess.hpp
includes/triton/modes.hpp
includes/triton/modesEnums.hpp
Expand All @@ -121,17 +122,17 @@ set(LIBTRITON_HEADER_FILES
includes/triton/synthesisResult.hpp
includes/triton/synthesizer.hpp
includes/triton/taintEngine.hpp
includes/triton/tritonToBitwuzlaAst.hpp
includes/triton/tritonToBitwuzla.hpp
includes/triton/tritonToLLVM.hpp
includes/triton/tritonToZ3Ast.hpp
includes/triton/tritonToZ3.hpp
includes/triton/tritonTypes.hpp
includes/triton/x86.spec
includes/triton/x8664Cpu.hpp
includes/triton/x86Cpu.hpp
includes/triton/x86Semantics.hpp
includes/triton/x86Specifications.hpp
includes/triton/z3Solver.hpp
includes/triton/z3ToTritonAst.hpp
includes/triton/z3ToTriton.hpp
)

# Define all resource files
Expand All @@ -142,8 +143,8 @@ set(LIBTRITON_RESOURCE_FILES

if(Z3_INTERFACE)
set(Z3_INTERFACE_SOURCE_FILES
ast/z3/tritonToZ3Ast.cpp
ast/z3/z3ToTritonAst.cpp
ast/z3/tritonToZ3.cpp
ast/z3/z3ToTriton.cpp
engines/solver/z3/z3Solver.cpp
)
else()
Expand All @@ -152,7 +153,7 @@ endif()

if(BITWUZLA_INTERFACE)
set(BITWUZLA_INTERFACE_SOURCE_FILES
ast/bitwuzla/tritonToBitwuzlaAst.cpp
ast/bitwuzla/tritonToBitwuzla.cpp
engines/solver/bitwuzla/bitwuzlaSolver.cpp
)
else()
Expand All @@ -161,6 +162,7 @@ endif()

if(LLVM_INTERFACE)
set(LLVM_INTERFACE_SOURCE_FILES
ast/llvm/llvmToTriton.cpp
ast/llvm/tritonToLLVM.cpp
engines/lifters/liftingToLLVM.cpp
)
Expand Down
22 changes: 11 additions & 11 deletions ...iton/ast/bitwuzla/tritonToBitwuzlaAst.cpp → ...btriton/ast/bitwuzla/tritonToBitwuzla.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,36 +11,36 @@
#include <triton/exceptions.hpp>
#include <triton/symbolicExpression.hpp>
#include <triton/symbolicVariable.hpp>
#include <triton/tritonToBitwuzlaAst.hpp>
#include <triton/tritonToBitwuzla.hpp>



namespace triton {
namespace ast {

TritonToBitwuzlaAst::TritonToBitwuzlaAst(bool eval)
TritonToBitwuzla::TritonToBitwuzla(bool eval)
: isEval(eval) {
}


TritonToBitwuzlaAst::~TritonToBitwuzlaAst() {
TritonToBitwuzla::~TritonToBitwuzla() {
this->translatedNodes.clear();
this->variables.clear();
this->symbols.clear();
}


const std::unordered_map<const BitwuzlaTerm*, triton::engines::symbolic::SharedSymbolicVariable>& TritonToBitwuzlaAst::getVariables(void) const {
const std::unordered_map<const BitwuzlaTerm*, triton::engines::symbolic::SharedSymbolicVariable>& TritonToBitwuzla::getVariables(void) const {
return this->variables;
}


const std::map<size_t, const BitwuzlaSort*>& TritonToBitwuzlaAst::getBitvectorSorts(void) const {
const std::map<size_t, const BitwuzlaSort*>& TritonToBitwuzla::getBitvectorSorts(void) const {
return this->bvSorts;
}


const BitwuzlaTerm* TritonToBitwuzlaAst::convert(const SharedAbstractNode& node, Bitwuzla* bzla) {
const BitwuzlaTerm* TritonToBitwuzla::convert(const SharedAbstractNode& node, Bitwuzla* bzla) {
auto nodes = childrenExtraction(node, true /* unroll*/, true /* revert */);
for (auto&& n : nodes) {
translatedNodes[n] = translate(n, bzla);
Expand All @@ -49,9 +49,9 @@ namespace triton {
}


const BitwuzlaTerm* TritonToBitwuzlaAst::translate(const SharedAbstractNode& node, Bitwuzla* bzla) {
const BitwuzlaTerm* TritonToBitwuzla::translate(const SharedAbstractNode& node, Bitwuzla* bzla) {
if (node == nullptr)
throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): node cannot be null.");
throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): node cannot be null.");

std::vector<const BitwuzlaTerm*> children;
for (auto&& n : node->getChildren()) {
Expand Down Expand Up @@ -186,7 +186,7 @@ namespace triton {
}

case FORALL_NODE:
throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062).");
throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): FORALL node can't be converted due to a Bitwuzla issue (see #1062).");

case IFF_NODE:
return bitwuzla_mk_term2(bzla, BITWUZLA_KIND_IFF, children[0], children[1]);
Expand Down Expand Up @@ -225,7 +225,7 @@ namespace triton {

auto it = symbols.find(value);
if (it == symbols.end())
throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): [STRING_NODE] Symbols not found.");
throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): [STRING_NODE] Symbols not found.");

return translatedNodes.at(it->second);
}
Expand Down Expand Up @@ -265,7 +265,7 @@ namespace triton {
}

default:
throw triton::exceptions::AstLifting("TritonToBitwuzlaAst::translate(): Invalid kind of node.");
throw triton::exceptions::AstLifting("TritonToBitwuzla::translate(): Invalid kind of node.");
}
}

Expand Down
Loading

0 comments on commit 9a6f208

Please sign in to comment.