kdrag.contrib.pcode.asmspec

Functions

`assemble_and_check`(filename[, langid, as_bin])
`assemble_and_check_str`(asm_str)
`assemble_and_gen_vcs`(filename[, langid, as_bin])
`execute_insn`(tracestate, ctx[, verbose])
`execute_spec_stmts`(stmts, tracestate, ctx[, ...])
`pretty_trace`(ctx, trace)	Pretty print a trace.
`run_all_paths`(ctx, spec[, mem, verbose])	Initialize queue with all stated entry points, and then symbolically execute all paths, collecting verification conditions (VCs) along the way.
`substitute`(e, ctx, memstate, ghost_env)	Subsititute both ghost state and context (ram / registers).
`substitute_ghost`(e, ghost_env)	Substitute ghost variables in an expression.

Classes

`Always`(expr)
`AsmSpec`(addrmap, list[SpecStmt]] =)	A specification of an assembly program.
`Assert`(label, addr, expr)
`Assign`(label, addr, name, expr)
`Assume`(label, addr, expr)
`BoolStmt`(label, addr, expr)
`Cut`(label, addr, expr)
`Entry`(label, addr, expr)
`Exit`(label, addr, expr)
`Results`(successes, failures)
`TraceState`(start, trace, state, ghost_env, ...)
`VerificationCondition`(start, trace, ...)	The result of symbolic execution over a path.

class kdrag.contrib.pcode.asmspec.Always(expr: z3.z3.BoolRef)

Bases: object

Parameters:: expr (BoolRef)

expr: BoolRef

class kdrag.contrib.pcode.asmspec.AsmSpec(addrmap: ~collections.defaultdict[int, list[SpecStmt]] = <factory>)

Bases: object

A specification of an assembly program. https://www.philipzucker.com/assembly_verify/ Registers are named by their corresponding names in pypcode. You can examine them by

`python import pypcode print(pypcode.Context("x86:LE:64:default").registers) `

Parameters:: addrmap (defaultdict[int, list[SpecStmt]])

add_assert(label: str, addr: int, expr: BoolRef)

Parameters:

label (str)
addr (int)
expr (BoolRef)

add_assign(label: str, addr: int, name: str, expr: ExprRef)

Parameters:

label (str)
addr (int)
name (str)
expr (ExprRef)

add_assume(label: str, addr: int, expr: BoolRef)

Parameters:

label (str)
addr (int)
expr (BoolRef)

add_cut(label: str, addr: int, expr: BoolRef)

Parameters:

label (str)
addr (int)
expr (BoolRef)

add_entry(label: str, addr: int, expr: BoolRef)

Parameters:

label (str)
addr (int)
expr (BoolRef)

add_exit(label: str, addr: int, expr: BoolRef)

Parameters:

label (str)
addr (int)
expr (BoolRef)

addrmap: defaultdict[int, list[SpecStmt]]

classmethod of_file(filename: str, ctx: BinaryContext)

Parameters:

filename (str)
ctx (BinaryContext)

class kdrag.contrib.pcode.asmspec.Assert(label: str, addr: int, expr: BoolRef)

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.Assign(label: str, addr: int, name: str, expr: z3.z3.ExprRef)

Bases: object

Parameters:

label (str)
addr (int)
name (str)
expr (ExprRef)

addr: int

expr: ExprRef

label: str

name: str

class kdrag.contrib.pcode.asmspec.Assume(label: str, addr: int, expr: BoolRef)

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.BoolStmt(label: str, addr: int, expr: z3.z3.BoolRef)

Bases: object

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.Cut(label: str, addr: int, expr: BoolRef)

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.Entry(label: str, addr: int, expr: BoolRef)

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.Exit(label: str, addr: int, expr: BoolRef)

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (BoolRef)

addr: int

expr: BoolRef

label: str

class kdrag.contrib.pcode.asmspec.Results(successes: list[str] = <factory>, failures: list[str] = <factory>)

Bases: object

Parameters:

successes (list[str])
failures (list[str])

failures: list[str]

successes: list[str]

class kdrag.contrib.pcode.asmspec.TraceState(start: SpecStmt, trace: Trace, state: kdrag.contrib.pcode.SimState, ghost_env: dict[str, z3.z3.ExprRef] = <factory>)

Bases: object

Parameters:

start (SpecStmt)
trace (Trace)
state (SimState)
ghost_env (dict[str, ExprRef])

ghost_env: dict[str, ExprRef]

start: SpecStmt

state: SimState

trace: Trace

class kdrag.contrib.pcode.asmspec.VerificationCondition(start: SpecStmt, trace: list[int], path_cond: list[BoolRef], memstate: MemState, ghost_env: dict[str, ExprRef], assertion: SpecStmt)

Bases: NamedTuple

The result of symbolic execution over a path. There is a reason the execution started (entry point), the necessary conditions on the initial state to follow this path (path_cond), the memory state at the end of the path (memstate), the ghost environment at the end of the path (ghost_env), and the assertion that must hold at the end of the path (assertion).

Parameters:

start (SpecStmt)
trace (list[int])
path_cond (list[BoolRef])
memstate (MemState)
ghost_env (dict[str, ExprRef])
assertion (SpecStmt)

assertion: SpecStmt: Alias for field number 5

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

countermodel(ctx: BinaryContext, m: ModelRef) → dict

Interpret a countermodel on the relevant constants

Parameters:

ctx (BinaryContext)
m (ModelRef)

Return type:

dict

ghost_env: dict[str, ExprRef]: Alias for field number 4

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

Return first index of value.

Raises ValueError if the value is not present.

memstate: MemState: Alias for field number 3

path_cond: list[BoolRef]: Alias for field number 2

start: SpecStmt: Alias for field number 0

trace: list[int]: Alias for field number 1

vc(ctx: BinaryContext) → BoolRef

Return the verification condition as an expression.

Parameters:: ctx (BinaryContext)
Return type:: BoolRef

verify(ctx: BinaryContext, **kwargs) → Proof

Verify the verification condition using the given context.

Parameters:: ctx (BinaryContext)
Return type:: Proof

kdrag.contrib.pcode.asmspec.assemble_and_check(filename: str, langid='x86:LE:64:default', as_bin='as') → Results

Parameters:: filename (str)
Return type:: Results

kdrag.contrib.pcode.asmspec.assemble_and_check_str(asm_str: str) → Results

Parameters:: asm_str (str)
Return type:: Results

kdrag.contrib.pcode.asmspec.assemble_and_gen_vcs(filename: str, langid='x86:LE:64:default', as_bin='as') → tuple[BinaryContext, list[VerificationCondition]]

Parameters:: filename (str)
Return type:: tuple[BinaryContext, list[VerificationCondition]]

kdrag.contrib.pcode.asmspec.execute_insn(tracestate: TraceState, ctx: BinaryContext, verbose=True) → list[TraceState]

Parameters:

tracestate (TraceState)
ctx (BinaryContext)

Return type:

list[TraceState]

kdrag.contrib.pcode.asmspec.execute_spec_stmts(stmts: list[SpecStmt], tracestate: TraceState, ctx: BinaryContext, verbose=True) → tuple[TraceState | None, list[VerificationCondition]]

Parameters:

stmts (list[SpecStmt])
tracestate (TraceState)
ctx (BinaryContext)

Return type:

tuple[TraceState | None, list[VerificationCondition]]

kdrag.contrib.pcode.asmspec.pretty_trace(ctx: BinaryContext, trace: Trace) → str

Pretty print a trace.

Parameters:

ctx (BinaryContext)
trace (Trace)

Return type:

str

kdrag.contrib.pcode.asmspec.run_all_paths(ctx: BinaryContext, spec: AsmSpec, mem=None, verbose=True) → list[VerificationCondition]

Initialize queue with all stated entry points, and then symbolically execute all paths, collecting verification conditions (VCs) along the way. This interleaves executions of actual assembly instructions with spec statements.

Parameters:

ctx (BinaryContext)
spec (AsmSpec)

Return type:

list[VerificationCondition]

kdrag.contrib.pcode.asmspec.substitute(e: ExprRef, ctx: BinaryContext, memstate: MemState, ghost_env: dict[str, ExprRef]) → ExprRef

Subsititute both ghost state and context (ram / registers). Usually you want this

Parameters:

e (ExprRef)
ctx (BinaryContext)
memstate (MemState)
ghost_env (dict[str, ExprRef])

Return type:

ExprRef

kdrag.contrib.pcode.asmspec.substitute_ghost(e: ExprRef, ghost_env: dict[str, ExprRef]) → ExprRef

Substitute ghost variables in an expression.

Parameters:

e (ExprRef)
ghost_env (dict[str, ExprRef])

Return type:

ExprRef