kdrag.contrib.pcode

Module Attributes

`MemSorts`	Memory is modelled as an array of 64-bit addresses to 8-bit values
`MemStateSort`	class StateExpr(NamedTuple): ctx: BinaryContext expr: smt.ExprRef

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`()
`varnode_eq`(self, other)

Classes

`BinaryContext`([filename, langid])	Almost all operations one wants to do on assembly are dependent on the binary and where it was loaded.
`CachedArray`(data, cache, owner, bits[, ...])	CachedArray keeps some writes unapplied to the array.
`MemState`(ram, register, unique, bits, read, ...)	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.simplify(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")
select64le(register(state0), &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

simplify(expr: ExprRef) → ExprRef

Call simplify and unfold if unfolding makes expression smaller.

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

substitute(memstate: MemState, expr: StateExpr) → BoolRef

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

Parameters:

memstate (MemState)
expr (StateExpr)

Return type:

BoolRef

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.select_concat(ram, x, 2)))
Concat(ram[1 + x], ram[x])

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

class kdrag.contrib.pcode.CachedArray(data: ArrayRef, cache: dict[Varnode, BitVecRef], owner: dict[int, Varnode], bits: int, register: int = False, le: bool = True)

Bases: NamedTuple

CachedArray keeps some writes unapplied to the array.

The invariant is that anything in the cache owns that data. You may replace something in the cache

>>> r1 = _TestVarnode("register", 0, 2)
>>> e1 = _TestVarnode("register", 0, 1)
>>> mem = CachedArray(smt.Array("mem", BV[64], BV[8]), {}, {}, 64, register=True)
>>> mem1 = mem.store(r1, smt.BitVecVal(2, 16))
>>> mem2 = mem1.store(e1, smt.BitVecVal(1,8))
>>> mem2.read(e1)
1
>>> mem2.read(r1)
select16le(Store(store16le(mem, &Roff0_size2, 2),
                &Roff0_size1,
                1),
        &Roff0_size2)
>>> mem2.store(r1, smt.BitVecVal(3,16)).read(r1)
3

Parameters:

data (ArrayRef)
cache (dict[Varnode, BitVecRef])
owner (dict[int, Varnode])
bits (int)
register (int)
le (bool)

bits: int: Alias for field number 3

cache: dict[Varnode, BitVecRef]: Alias for field number 1

count(value, /): Return number of occurrences of value.

data: ArrayRef: Alias for field number 0

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

le: bool: Alias for field number 5

owner: dict[int, Varnode]: Alias for field number 2

read(vnode: Varnode) → BitVecRef

Parameters:: vnode (Varnode)
Return type:: BitVecRef

register: int: Alias for field number 4

store(vnode: Varnode, value: BitVecRef) → CachedArray

Parameters:

vnode (Varnode)
value (BitVecRef)

Return type:

CachedArray

to_expr()

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(ram: ArrayRef, register: CachedArray, unique: CachedArray, bits: int, read: ArrayRef, write: list[tuple[BitVecRef, int]])

Bases: NamedTuple

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:

ram (ArrayRef)
register (CachedArray)
unique (CachedArray)
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: Alias for field number 3

count(value, /): Return number of occurrences of value.

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

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

ram: ArrayRef: Alias for field number 0

read: ArrayRef: Alias for field number 4

register: CachedArray: Alias for field number 1

setvalue(vnode: Varnode, value: BitVecRef)

Parameters:

vnode (Varnode)
value (BitVecRef)

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

Parameters:

offset (BitVecRef | int)
value (BitVecRef)

to_expr() → DatatypeRef

Return type:: DatatypeRef

unique: CachedArray: Alias for field number 2

write: list[tuple[BitVecRef, int]]: Alias for field number 5

kdrag.contrib.pcode.MemStateSort = {8: MemState, 16: MemState!1, 32: MemState!2, 64: MemState!3}

class StateExpr(NamedTuple): ctx: BinaryContext expr: smt.ExprRef

def to_lambda(self) -> smt.QuantifierRef:: mem = smt.Const(“mem”, MemStateSort[self.ctx.bits]) memstate = MemState.Const(“mem”, bits=self.ctx.bits) return smt.Lambda([mem], self(memstate))
def __call__(self, memstate: MemState) -> smt.ExprRef:: return self.ctx.substitute(memstate, self.expr)

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

kdrag.contrib.pcode.varnode_eq(self: Varnode, other) → bool

Parameters:: self (Varnode)
Return type:: bool

Modules

asmspec