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)
`executeZeroExtend`(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, read, write)	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:

memstate (MemState)
pc (PC)

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:

memstate (MemState)
pc (PC)

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:

memstate (MemState)
regname (str)

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:

model (ModelRef)
memstate (MemState)

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:

memstate (MemState)
expr (ExprRef)

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)

unfold(expr: ExprRef) → ExprRef

Fully unpacked, the expressions are not readable. But definitions are opaque to z3 until unfolded. This unfolds helper definitions used during constraint production.

>>> x = smt.BitVec("x", 64)
>>> ctx = BinaryContext()
>>> ctx.unfold(x)
x
>>> import kdrag.theories.bitvec as bv
>>> ram = smt.Array("ram", BV[64], BV[8])
>>> smt.simplify(ctx.unfold(bv.select64_le[16](ram, x)))
Concat(ram[1 + x], ram[x])

Parameters:: expr (ExprRef)
Return type:: ExprRef

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, read: ArrayRef, write: list[tuple[BitVecRef, 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.Const(“mymem”) #(smt.Array(“mymem”, BV[64], BV[8]), bits=64)

Parameters:

mem (DatatypeRef)
bits (int)
read (ArrayRef)
write (list[tuple[BitVecRef, 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

read: ArrayRef

setvalue(vnode: Varnode, value: BitVecRef)

Parameters:

vnode (Varnode)
value (BitVecRef)

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

Parameters:

offset (BitVecRef | int)
value (BitVecRef)

write: list[tuple[BitVecRef, int]]

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:

op (PcodeOp)
memstate (MemState)

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:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executePopcount(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executeSignExtend(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executeStore(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executeSubpiece(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executeUnary(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

Return type:

MemState

kdrag.contrib.pcode.executeZeroExtend(op: PcodeOp, memstate: MemState) → MemState

Parameters:

op (PcodeOp)
memstate (MemState)

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