kdrag.contrib.pcode

Module Attributes

MemSorts

Memory is modelled as an array of 64-bit addresses to 8-bit values

Functions

executeBinary(op, memstate)

executeCBranch(op, memstate)

executeLoad(op, memstate)

executePopcount(op, memstate)

executeSignExtend(op, memstate)

executeStore(op, memstate)

executeSubpiece(op, memstate)

executeUnary(op, memstate)

pc_of_addr(addr)

pretty_insn(insn)

pretty_op(op)

test_pcode()

Classes

BinaryContext([filename, langid])

Almost all operations one wants to do on assembly are dependent on the binary and where it was loaded.

MemState(mem, bits)

MemState is a wrapper that offers getvalue and setvalue methods

SimState(memstate, pc, path_cond)

class kdrag.contrib.pcode.BinaryContext(filename=None, langid='x86:LE:64:default')

Bases: object

Almost all operations one wants to do on assembly are dependent on the binary and where it was loaded. BinaryContext is a class that holds the binary and provides methods to disassemble and translate instructions. It is the analog of an angr Project in some respects.

Run python3 -m pypcode –list to see available langid. - RISCV:LE:64:default

disassemble(addr)
execute1(memstate: MemState, pc: PC) → tuple[MemState, PC]

Execute a single PCode instruction at addr, returning the new memstate and pc.

Parameters:
Return type:

tuple[MemState, PC]

execute1_schema(pc: PC) → Proof

For a given concrete PC and binary, we can generate an axiomatic description of how execution of a single instruction at that PC will change the memory state and program counter.

Parameters:

pc (PC)

Return type:

Proof

executeBranch(op: PcodeOp, pc: PC) → PC
Parameters:

  • op (PcodeOp)

  • pc (PC)

Return type:

PC

executeCurrentOp(op, memstate: MemState, pc: PC) → tuple[MemState, PC]
Parameters:
Return type:

tuple[MemState, PC]

executeInsn(memstate, addr)
fallthruOp(pc: PC)
Parameters:

pc (PC)

get_reg(memstate: MemState, regname: str) → BitVecRef

Get the value of a register from the memstate.

>>> ctx = BinaryContext()
>>> memstate = MemState.Const("test_mem")
>>> memstate = ctx.set_reg(memstate, "RAX", smt.BitVec("RAX", 64))
>>> ctx.get_reg(memstate, "RAX")
RAX
Parameters:
Return type:

BitVecRef

get_regs(memstate: MemState) → dict[str, BitVecRef]

Get the state of the registers from the memstate.

Parameters:

memstate (MemState)

Return type:

dict[str, BitVecRef]

init_mem() → MemState

Initialize the memory state with empty memory.

>>> ctx = BinaryContext()
>>> memstate = ctx.init_mem()
>>> ctx.get_reg(memstate, "RAX")
RAX!...
Return type:

MemState

load(main_binary, **kwargs)

Load a binary file and initialize the context.

model_registers(model: ModelRef, memstate: MemState) → dict[str, BitVecRef]

Get values of all registers in model.

Parameters:
Return type:

dict[str, BitVecRef]

set_reg(memstate: MemState, regname: str, value: BitVecRef) → MemState

Set the value of a register in the memstate.

Parameters:

  • memstate (MemState)

  • regname (str)

  • value (BitVecRef)

Return type:

MemState

substitute(memstate: MemState, expr: ExprRef) → ExprRef

Substitute the values in memstate into the expression expr. expr uses the short register names and ram

Parameters:
Return type:

ExprRef

sym_execute(memstate: MemState, addr: int, path_cond: list[BoolRef] | None = None, max_insns=1, breakpoints=[], verbose=False) → list[SimState]

Symbolically execute a real instruction at addr, returning a list of SimState objects. A single instruction may contain multiple Pcode instructions or even pcode loops. Hence a symbolic execution may be required for even a single instruction.

Parameters:

  • memstate (MemState)

  • addr (int)

  • path_cond (list[BoolRef] | None)

Return type:

list[SimState]

translate(addr)
kdrag.contrib.pcode.MemSorts = {8: Array(BitVec(8), BitVec(8)), 16: Array(BitVec(16), BitVec(8)), 32: Array(BitVec(32), BitVec(8)), 64: Array(BitVec(64), BitVec(8))}

Memory is modelled as an array of 64-bit addresses to 8-bit values

class kdrag.contrib.pcode.MemState(mem: DatatypeRef, bits: int)

Bases: object

MemState is a wrapper that offers getvalue and setvalue methods

#>>> mem.getvalue(_TestVarnode(“ram”, 0, 8)) #>>> mem.setvalue(_TestVarnode(“ram”, 0, 8), 1) >>> mem = MemState(smt.Array(“mymem”, BV[64], BV[8]), bits=64)

Parameters:

  • mem (DatatypeRef)

  • bits (int)

classmethod Const(name: str, bits: int = 64) → MemState
Parameters:

  • name (str)

  • bits (int)

Return type:

MemState

bits: int
getvalue(vnode: Varnode) → BitVecRef | int
Parameters:

vnode (Varnode)

Return type:

BitVecRef | int

getvalue_ram(offset: BitVecRef | int, size: int) → BitVecRef
Parameters:

  • offset (BitVecRef | int)

  • size (int)

Return type:

BitVecRef

mem: DatatypeRef
setvalue(vnode: Varnode, value: BitVecRef)
Parameters:

  • vnode (Varnode)

  • value (BitVecRef)

setvalue_ram(offset: BitVecRef | int, value: BitVecRef)
Parameters:

  • offset (BitVecRef | int)

  • value (BitVecRef)

class kdrag.contrib.pcode.SimState(memstate: kdrag.contrib.pcode.MemState, pc: PC, path_cond: list[z3.z3.BoolRef])

Bases: object

Parameters:

  • memstate (MemState)

  • pc (PC)

  • path_cond (list[BoolRef])

memstate: MemState
path_cond: list[BoolRef]
pc: PC
kdrag.contrib.pcode.executeBinary(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executeCBranch(op, memstate: MemState) → BoolRef | bool
Parameters:

memstate (MemState)

Return type:

BoolRef | bool

kdrag.contrib.pcode.executeLoad(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executePopcount(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executeSignExtend(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executeStore(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executeSubpiece(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.executeUnary(op: PcodeOp, memstate: MemState) → MemState
Parameters:
Return type:

MemState

kdrag.contrib.pcode.pc_of_addr(addr: int) → PC
Parameters:

addr (int)

Return type:

PC

kdrag.contrib.pcode.pretty_insn(insn: Instruction) → str
Parameters:

insn (Instruction)

Return type:

str

kdrag.contrib.pcode.pretty_op(op: PcodeOp) → str
Parameters:

op (PcodeOp)

Return type:

str

kdrag.contrib.pcode.test_pcode()

Modules

asmspec