libTriton  version 0.6 build 1372
SMT Solver Interface

[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: AstContext). 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)
(bvlshr
(_ bv27030 16)
((_ zero_extend 8)
(bvand
(bvxor
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
auto raxSymId = api.getSymbolicRegisterId(TRITON_X86_REG_RAX);
// Get the full AST of RAX
auto raxFullAst = api.unrollAstFromId(raxSymId);
// Modify the AST of RAX to build the constraint
auto constraint = triton::ast::equal(raxFullAst, triton::ast::bv(0, raxFullAst->getBitvectorSize()));
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;
}