SolverModel

Table of Contents

• Description
• Python API - Methods of the SolverModel class

[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)
0
>>> 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.