Merge pull request JonathanSalwan#1088 from JackBoosY/dev/jack/fix-bu…

.build_number

@@ -1 +1 @@
-1517
+1521

CMakeLists.txt

@@ -29,6 +29,8 @@ 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)
+option(BUILD_EXAMPLES       "Build the examples"                       ON)
+option(ENABLE_TEST          "Build test program"                       ON)
 
 # Define cmake dependent options
 cmake_dependent_option(PYTHON_BINDINGS      "Enable Python bindings"                        ON BUILD_SHARED_LIBS OFF)

src/CMakeLists.txt

@@ -1,12 +1,16 @@
 add_subdirectory(libtriton)
 
-if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-    # Disable exemples for windows as linkage doesn't work. Exported function should
-    # be marked as exported on windows.
-    add_subdirectory(examples)
-else()
-    enable_testing()
-    add_test(DummyTest echo "Windows is awesome")
+if (BUILD_EXAMPLES)
+    if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+        # Disable exemples for windows as linkage doesn't work. Exported function should
+        # be marked as exported on windows.
+        add_subdirectory(examples)
+    else()
+        enable_testing()
+        add_test(DummyTest echo "Windows is awesome")
+    endif()
 endif()
 
-add_subdirectory(testers)
+if (ENABLE_TEST)
+    add_subdirectory(testers)
+endif()

src/examples/python/proving_equivalence.py

@@ -0,0 +1,58 @@
+#!/usr/bin/env python
+## -*- coding: utf-8 -*-
+##
+## $ python ./proving equivalence.py
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+## True
+##
+
+import sys
+from triton import *
+
+
+def prove(ctx, n):
+    ast = ctx.getAstContext()
+    if ctx.isSat(ast.lnot(n)) == True:
+        return False
+    return True
+
+if __name__ == '__main__':
+    ctx = TritonContext(ARCH.X86_64)
+    ast = ctx.getAstContext()
+
+    ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)
+
+    x = ast.variable(ctx.newSymbolicVariable(8, 'x'))
+    y = ast.variable(ctx.newSymbolicVariable(8, 'y'))
+
+    # MBA coming from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/
+    # To detect their equivalence you can synthesize them (see synthesizing_obfuscated_expressions.py)
+    # Then you can confirm the synthesized output with this example
+    print(prove(ctx, x ^ y          == (~(~(x) & ~(y)) & ~(~(~(x)) & ~(~(y))))))
+    print(prove(ctx, x + y          == ((~(~(x)) & ~(~(y))) + (~(~(x)) | ~(~(y))))))
+    print(prove(ctx, x + y          == ((~(~(y)) | ~(~(x))) + ~(~(x)) - (~(~(x)) & ~(~(~(y)))))))
+    print(prove(ctx, x + y          == ((~(~(x)) | ~(~(y))) + (~(~(~(x))) | ~(~(y))) - (~(~(~(x)))))))
+    print(prove(ctx, x + y          == ((~(~(x)) | ~(~(y))) + ~(~(y)) - (~(~(~(x))) & ~(~(y))))))
+    print(prove(ctx, x + y          == (~(~(y)) + (~(~(x)) & ~(~(~(y)))) + (~(~(x)) & ~(~(y))))))
+    print(prove(ctx, x - y          == (~(~(x) + y))))
+    print(prove(ctx, ~((x | y) - x) == (~(((~(~(x)) | y) - (~(~(x))))))))
+    print(prove(ctx, x - y          == (~((~(x) & ~(x)) + y) & ~((~(x) & ~(x)) + y))))
+    print(prove(ctx, x & y          == ((~(~(x)) | y) - (~(~(~(x))) & y) - (~(~(x)) & ~y))))
+    print(prove(ctx, x & y          == ((~(~(~(x))) | y) - (~(~(~(x)))))))
+    print(prove(ctx, x | y          == ((~(~(x)) & ~(y)) + y)))
+    print(prove(ctx, x | y          == (((~(~(x)) & ~(y)) & y) + ((~(~(x)) & ~(y)) | y))))
+    print(prove(ctx, x + y          == ((~(~(x)) & ~(~(y))) + (~(~(x)) | ~(~(y))))))
+
+    sys.exit(0)

src/examples/python/synthesizing_obfuscated_expressions.py

@@ -3,7 +3,7 @@
 ##
 ## Example of synthesizing obfuscated expressions.
 ##
-## $ time python3 ./synthesizing_obfuscated_expressions.py
+## $ python3 ./synthesizing_obfuscated_expressions.py
 ## In: (((((SymVar_0 | SymVar_1) + SymVar_1) & 0xff) - ((~(SymVar_0) & 0xff) & SymVar_1)) & 0xff)
 ## Out: ((SymVar_0 + SymVar_1) & 0xff)
 ##
@@ -31,7 +31,7 @@
 ## In: ((((((~(((((((((((z & 0xff) << 0x8) & 0xffffffff) | ((z >> 0x8) & 0xff)) << 0x8) & 0xffffffff) | ((z ...
 ## Out: (((bswap(z, 32) ^ 0x23746fbe) + 0xfffffffd) & 0xffffffff)
 ##
-## python3 ./synthesizing_obfuscated_expressions.py  0.12s user 0.01s system 99% cpu 0.125 total
+## [...]
 ##
 
 import sys
@@ -84,20 +84,34 @@ def main():
 
     # Some obfuscated expressions
     obf_exprs = [
-        (x | y) + y - (~x & y),                             # x + y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
-        (x | y) - y + (~x & y),                             # x ^ y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
-        (x & ~y) | (~x & y),                                # x ^ y                                      (from ?)
-        (x ^ y) + y - (~x & y),                             # x | y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
-        -(x | y) + y + x,                                   # x & y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
-        ((z << 8) >> 16) << 8,                              # z & 0xffff00                               (from https://blog.regehr.org/archives/1636)
-        (((x ^ y) + 2 * (x & y)) * 39 + 23) * 151 + 111,    # x + y                                      (from Ninon Eyrolle's thesis)
-        x_xor_92_obfuscated(x),                             # x ^ 92                                     (from imassage)
-        bswap32_xor_const(z),                               # ((bswap(z, 32) ^ 0x23746fbe) + 0xfffffffd) (from UnityPlayer.dll)
+        (x | y) + y - (~x & y),                                             # x + y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
+        (x | y) - y + (~x & y),                                             # x ^ y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
+        (x & ~y) | (~x & y),                                                # x ^ y                                      (from ?)
+        (x ^ y) + y - (~x & y),                                             # x | y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
+        -(x | y) + y + x,                                                   # x & y                                      (from http://archive.bar/pdfs/bar2020-preprint9.pdf)
+        ((z << 8) >> 16) << 8,                                              # z & 0xffff00                               (from https://blog.regehr.org/archives/1636)
+        (((x ^ y) + 2 * (x & y)) * 39 + 23) * 151 + 111,                    # x + y                                      (from Ninon Eyrolle's thesis)
+        x_xor_92_obfuscated(x),                                             # x ^ 92                                     (from iMassage)
+        bswap32_xor_const(z),                                               # ((bswap(z, 32) ^ 0x23746fbe) + 0xfffffffd) (from UnityPlayer.dll)
+        (~(~(x) & ~(y)) & ~(~(~(x)) & ~(~(y)))),                            # x ^ y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) & ~(~(y))) + (~(~(x)) | ~(~(y)))),                        # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(y)) | ~(~(x))) + ~(~(x)) - (~(~(x)) & ~(~(~(y))))),           # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) | ~(~(y))) + (~(~(~(x))) | ~(~(y))) - (~(~(~(x))))),      # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) | ~(~(y))) + ~(~(y)) - (~(~(~(x))) & ~(~(y)))),           # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        (~(~(y)) + (~(~(x)) & ~(~(~(y)))) + (~(~(x)) & ~(~(y)))),           # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        (~(~(x) + y)),                                                      # x - y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        (~(((~(~(x)) | y) - (~(~(x)))))),                                   # ~((x | y) - x)                             (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        (~((~(x) & ~(x)) + y) & ~((~(x) & ~(x)) + y)),                      # x - y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) | y) - (~(~(~(x))) & y) - (~(~(x)) & ~y)),                # x & y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(~(x))) | y) - (~(~(~(x))))),                                  # x & y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) & ~(y)) + y),                                             # x | y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        (((~(~(x)) & ~(y)) & y) + ((~(~(x)) & ~(y)) | y)),                  # x | y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
+        ((~(~(x)) & ~(~(y))) + (~(~(x)) | ~(~(y)))),                        # x + y                                      (from VMProtect https://whereisr0da.github.io/blog/posts/2021-02-16-vmp-3/)
     ]
 
     for expr in obf_exprs:
         (print('In: %s' %(expr)) if len(str(expr)) < 100 else print('In: %s ...' %(str(expr)[0:100])))
-        expr = ctx.synthesize(expr, constant=True, subexpr=True, opaque=False)
+        expr = ctx.synthesize(expr, constant=True, subexpr=True)
         print('Out: %s' %(expr))
         print()
 

src/libtriton/CMakeLists.txt

@@ -275,7 +275,7 @@ if(MSVC AND MSVC_STATIC)
 endif()
 
 if(WIN32 AND BUILD_SHARED_LIBS)
-    target_compile_definitions(triton PUBLIC TRITON_BUILDING_DLL)
+    target_compile_definitions(triton PRIVATE BUILDING_DLL)
 endif()
 
 # Install tritonTargets.cmake
@@ -291,6 +291,7 @@ install(
     EXPORT tritonTargets
     PUBLIC_HEADER DESTINATION include/triton
     INCLUDES DESTINATION include
+    RUNTIME DESTINATION bin
     ARCHIVE DESTINATION lib
     LIBRARY DESTINATION lib
 )

src/libtriton/Config.cmake.in

@@ -8,6 +8,7 @@ set(TRITON_BUILD_SHARED_LIBS    @BUILD_SHARED_LIBS@)
 set(TRITON_INCLUDE_DIRS         "@CMAKE_INSTALL_PREFIX@/include")
 set(TRITON_INSTALL_PREFIX       @CMAKE_INSTALL_PREFIX@)
 set(TRITON_LIBRARY              "@CMAKE_INSTALL_PREFIX@/lib/@CMAKE_SHARED_LIBRARY_PREFIX@triton@CMAKE_SHARED_LIBRARY_SUFFIX@")
+set(TRITON_LIBRARIES            "${TRITON_LIBRARY};@PYTHON_LIBRARIES@;@Z3_LIBRARIES@;@LLVM_LIBRARIES@;@BITWUZLA_LIBRARIES@;@CAPSTONE_LIBRARIES@")
 set(TRITON_LLVM_INTERFACE       @LLVM_INTERFACE@)
 set(TRITON_MSVC_STATIC          @MSVC_STATIC@)
 set(TRITON_PYTHON_BINDINGS      @PYTHON_BINDINGS@)
@@ -18,3 +19,30 @@ message(STATUS "Found Triton: ${CMAKE_CURRENT_LIST_DIR}/tritonConfig.cmake (foun
 
 include(CMakeFindDependencyMacro)
 find_dependency(Boost)
+
+# Triton include
+include_directories("@CMAKE_INSTALL_PREFIX@/include")
+
+# Capstone include
+include_directories("@CAPSTONE_INCLUDE_DIRS@")
+
+# Python include directories
+if (TRITON_PYTHON_BINDINGS)
+    include_directories("@PYTHON_INCLUDE_DIRS@")
+endif()
+
+# LLVM include and lib directories
+if (TRITON_LLVM_INTERFACE)
+    link_directories(BEFORE "@LLVM_LIBRARY_DIRS@")
+    include_directories("@LLVM_INCLUDE_DIRS@")
+endif()
+
+# Z3 include directories
+if (TRITON_Z3_INTERFACE)
+    include_directories("@Z3_INCLUDE_DIRS@")
+endif()
+
+# Bitwuzla include directories
+if (TRITON_BITWUZLA_INTERFACE)
+    include_directories("@BITWUZLA_INCLUDE_DIRS@")
+endif()

src/libtriton/api/api.cpp

@@ -881,13 +881,15 @@ namespace triton {
   }
 
 
-  triton::ast::SharedAbstractNode API::simplify(const triton::ast::SharedAbstractNode& node, bool usingSolver) const {
-    this->checkSymbolic();
-
+  triton::ast::SharedAbstractNode API::simplify(const triton::ast::SharedAbstractNode& node, bool usingSolver, bool usingLLVM) const {
     if (usingSolver) {
       return this->simplifyAstViaSolver(node);
     }
+    else if (usingLLVM) {
+      return this->simplifyAstViaLLVM(node);
+    }
     else {
+      this->checkSymbolic();
       return this->symbolic->simplify(node);
     }
   }
@@ -1133,7 +1135,7 @@ namespace triton {
     #endif
     #ifdef TRITON_BITWUZLA_INTERFACE
     if (this->getSolver() == triton::engines::solver::SOLVER_BITWUZLA) {
-        return reinterpret_cast<const triton::engines::solver::BitwuzlaSolver*>(this->getSolverInstance())->evaluate(node);
+      return reinterpret_cast<const triton::engines::solver::BitwuzlaSolver*>(this->getSolverInstance())->evaluate(node);
     }
     #endif
     throw triton::exceptions::API("API::evaluateAstViaZ3(): Solver instance must be a SOLVER_Z3 or SOLVER_BITWUZLA.");
@@ -1373,17 +1375,17 @@ namespace triton {
 
   /* Lifters engine API ================================================================================= */
 
-  std::ostream& API::liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node) {
+  std::ostream& API::liftToLLVM(std::ostream& stream, const triton::ast::SharedAbstractNode& node, const char* fname, bool optimize) {
     this->checkLifting();
     #ifdef TRITON_LLVM_INTERFACE
-    return this->lifting->liftToLLVM(stream, node);
+    return this->lifting->liftToLLVM(stream, node, fname, optimize);
     #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::liftToLLVM(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, const char* fname, bool optimize) {
+    return this->liftToLLVM(stream, expr->getAst(), fname, optimize);
   }
 
 
@@ -1398,4 +1400,13 @@ namespace triton {
     return this->lifting->liftToSMT(stream, expr, assert_);
   }
 
+
+  triton::ast::SharedAbstractNode API::simplifyAstViaLLVM(const triton::ast::SharedAbstractNode& node) const {
+    this->checkLifting();
+    #ifdef TRITON_LLVM_INTERFACE
+    return this->lifting->simplifyAstViaLLVM(node);
+    #endif
+    throw triton::exceptions::API("API::simplifyAstViaLLVM(): Triton not built with LLVM");
+  }
+
 }; /* triton namespace */

src/libtriton/arch/instruction.cpp

@@ -35,12 +35,14 @@ namespace triton {
     }
 
 
-    Instruction::Instruction(const triton::uint8* opcode, triton::uint32 opSize) : Instruction::Instruction() {
+    Instruction::Instruction(const triton::uint8* opcode, triton::uint32 opSize)
+      : Instruction::Instruction() {
       this->setOpcode(opcode, opSize);
     }
 
 
-    Instruction::Instruction(triton::uint64 addr, const triton::uint8* opcode, triton::uint32 opSize) : Instruction::Instruction(opcode, opSize) {
+    Instruction::Instruction(triton::uint64 addr, const triton::uint8* opcode, triton::uint32 opSize)
+      : Instruction::Instruction(opcode, opSize) {
       this->setAddress(addr);
     }
 
@@ -132,7 +134,7 @@ namespace triton {
 
 
     void Instruction::setOpcode(const triton::uint8* opcode, triton::uint32 size) {
-      if (size >= sizeof(this->opcode))
+      if (size > sizeof(this->opcode))
        throw triton::exceptions::Instruction("Instruction::setOpcode(): Invalid size (too big).");
       std::memcpy(this->opcode, opcode, size);
       this->size = size;
@@ -340,11 +342,10 @@ namespace triton {
     }
 
 
-    const triton::engines::symbolic::SharedSymbolicExpression& Instruction::addSymbolicExpression(const triton::engines::symbolic::SharedSymbolicExpression& expr) {
+    void Instruction::addSymbolicExpression(const triton::engines::symbolic::SharedSymbolicExpression& expr) {
       if (expr == nullptr)
         throw triton::exceptions::Instruction("Instruction::addSymbolicExpression(): Cannot add a null expression.");
       this->symbolicExpressions.push_back(expr);
-      return this->symbolicExpressions.back();
     }
 
 

src/libtriton/ast/ast.cpp

@@ -183,13 +183,13 @@ namespace triton {
       auto it = parents.find(p);
 
       if (it == parents.end()) {
-        auto A = p->shared_from_this();
+        SharedAbstractNode A = p->shared_from_this();
         this->parents.insert(std::make_pair(p, std::make_pair(1, WeakAbstractNode(A))));
       }
       else {
         if (it->second.second.expired()) {
           parents.erase(it);
-          auto A = p->shared_from_this();
+          SharedAbstractNode A = p->shared_from_this();
           this->parents.insert(std::make_pair(p, std::make_pair(1, WeakAbstractNode(A))));
         }
         // Ptr already in, add it for the counter
@@ -213,8 +213,9 @@ namespace triton {
 
 
     void AbstractNode::setParent(std::unordered_set<AbstractNode*>& p) {
-      for (auto ptr : p)
+      for (AbstractNode* ptr : p) {
         this->setParent(ptr);
+      }
     }
 
 
@@ -3290,7 +3291,7 @@ namespace triton {
 
         /* If unroll is true, we unroll all references */
         if (unroll && ast->getType() == REFERENCE_NODE) {
-          const auto& ref = reinterpret_cast<ReferenceNode*>(ast.get())->getSymbolicExpression()->getAst();
+          const SharedAbstractNode& ref = reinterpret_cast<ReferenceNode*>(ast.get())->getSymbolicExpression()->getAst();
           if (visited.find(ref.get()) == visited.end()) {
             worklist.push({ref, false});
           }
@@ -3323,7 +3324,7 @@ namespace triton {
 
       worklist.push(node.get());
       while (!worklist.empty()) {
-        auto current = worklist.top();
+        AbstractNode* current = worklist.top();
         worklist.pop();
 
         // This means that node is already visited and we will not need to visited it second time
@@ -3339,7 +3340,7 @@ namespace triton {
           worklist.push(reinterpret_cast<triton::ast::ReferenceNode*>(current)->getSymbolicExpression()->getAst().get());
         }
         else {
-          for (const auto& child : current->getChildren()) {
+          for (const SharedAbstractNode& child : current->getChildren()) {
             worklist.push(child.get());
           }
         }