libTriton  version 0.9 build 1499
SolverModel

[python api] All information about the SolverModel Python object.

Description


This object is used to represent a model for an SMT solver.

>>> from __future__ import print_function
>>> from triton import TritonContext, ARCH, Instruction, REG
>>> ctxt = TritonContext()
>>> ctxt.setArchitecture(ARCH.X86_64)
>>> inst = Instruction()
>>> inst.setOpcode(b"\x48\x35\x44\x33\x22\x11") # xor rax, 0x11223344
>>> symvar = ctxt.symbolizeRegister(ctxt.registers.rax)
>>> print(symvar)
SymVar_0:64
>>> ctxt.processing(inst)
True
>>> print(inst)
0x0: xor rax, 0x11223344
>>> ast = ctxt.getAstContext()
>>> raxAst = ast.unroll(ctxt.getSymbolicRegister(ctxt.registers.rax).getAst())
>>> print(raxAst)
(bvxor SymVar_0 (_ bv287454020 64))
>>> astCtxt = ctxt.getAstContext()
>>> constraint = astCtxt.equal(raxAst, astCtxt.bv(0, raxAst.getBitvectorSize()))
>>> print(constraint)
(= (bvxor SymVar_0 (_ bv287454020 64)) (_ bv0 64))
>>> model = ctxt.getModel(constraint)
>>> print(model) #doctest: +ELLIPSIS
{0: SymVar_0:64 = 0x11223344}
>>> symvarModel = model[symvar.getId()] # Model from the symvar's id
>>> print(symvarModel)
SymVar_0:64 = 0x11223344
>>> hex(symvarModel.getValue())
'0x11223344'

Python API - Methods of the SolverModel class


  • integer getId(void)
    Returns the id of the model. This id is the same as the variable id.
  • integer getValue(void)
    Returns the value of the model.
  • SymbolicVariable getVariable(void)
    Returns the symbolic variable.