libTriton  version 0.4 build 1355
SMT Solver Interface

Table of Contents

[internal] All information about the SMT solver interface.

Description


The solver engine is the interface between an SMT solver and Triton itself. All requests are sent to the SMT solver as Triton AST (See: AST Representations). The AST representation as string looks like a manually crafted SMT2-LIB script.

Example:

; Declaration of the theory
(set-logic QF_AUFBV)
; Utility function
(define-fun parity ((x!1 (_ BitVec 8))) (_ BitVec 1)
; x ^= x >> 4;
; v &= 0xf;
; return (0x6996 >> v) & 1;
((_ extract 0 0)
(_ bv27030 16)
((_ zero_extend 8)
x!1
(bvlshr x!1 (_ bv4 8)))
(_ bv15 8)))))
)
; Declaration of the free variables
(declare-fun SymVar_0 () (_ BitVec 8))
; Formula
(assert (= (ite ...)))

C++ example


Let assume that the \(rax\)'s symbolic expression contains a symbolic variable \(x_0 \in X\) which has been instantiated previously. At this program point, we want that \(rax = 0\). We first get the symbolic expression id corresponding to the \(rax\) register, then, its AST. When the AST has been got, we are able to build our constraint such that \( AST_{constraint} = assert(AST_{rax} == 0) \).

The solver interface triton::API::getModel() gets as parameter a triton::ast::AbstractNode which corresponds to the \( AST_{constraint} \) and returns a list of triton::engines::solver::SolverModel. Each model for a symbolic variable \(x \in X\) is represented by a triton::engines::solver::SolverModel. For example, if there are two symbolic variables in your constraint, the triton::API::getModel() function will return a list of two items.

// Get the symbolic id of RAX
// Get the full AST of RAX
auto raxFullAst = api.getFullAstFromId(raxSymId);
// Modify the AST of RAX to build the constraint
auto constraint = triton::ast::assert_(triton::ast::equal(raxFullAst, triton::ast::bv(0, raxFullAst->getBitvectorSize())));
// Ask a model
auto model = api.getModel(constraint);
// Display all symbolic variable value contained in the model
std::cout << "Model:" << std::endl;
for (auto it = model.begin(); it != model.end(); it++) {
std::cout << " - Variable: " << it->getName() << std::endl;
std::cout << " - Value : " << std::hex << it->getValue() << std::endl;
}