kdrag.contrib.pcode.asmspec

Functions

`assemble_and_check`(filename[, langid, as_bin])
`assemble_and_check_str`(asm_str)
`assemble_and_gen_vcs`(filename[, langid, ...])
`execute_insn`(tracestate, ctx[, verbose])	Execute one actual instruction from the current trace state.
`execute_spec_and_insn`(tracestate0, spec, ctx)	Execute spec statements and then one instruction.
`execute_spec_stmts`(stmts, tracestate, ctx[, ...])	Execute a list of spec statements on a given trace state.
`init_trace_states`(ctx, mem, spec[, verbose])	Initialize all trace states from the entry points in the spec.
`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.
`update_write`(state, ghost_env)

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)
`Debug`(ctx[, spec, verbose])
`Entry`(label, addr, expr)
`Exit`(label, addr, expr)
`OutOfGas`()
`Results`(successes, failures)
`TraceState`(start, trace, state, trace_id, ...)
`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.Debug(ctx: BinaryContext, spec: AsmSpec | None = None, verbose=True)

Bases: object

Parameters:

ctx (BinaryContext)
spec (AsmSpec | None)

add_assert(name, assertion)

add_assign(name, var_name, expr)

add_cut(name, invariant)

add_entry(name, precond=True)

add_exit(name, postcond=True)

addr()

breakpoint(addr)

eval(expr: ExprRef) → ExprRef

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

ghost(name)

insn()

label(label: str | int) → int

Parameters:: label (str | int)
Return type:: int

model()

pop()

pop_lemma() → ProofState

Return type:: ProofState

pop_run(): Run until the current trace state is completely done.

pop_verify(**kwargs)

ram(addr, size=None): Get the expression held at at ram location addr

reg(name)

run()

run_vc()

spec_file(filename: str)

Parameters:: filename (str)

start(mem=None)

step(n=1)

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.OutOfGas

Bases: object

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: StartStmt, trace: Trace, state: kdrag.contrib.pcode.SimState, trace_id: list[int], ghost_env: dict[str, z3.z3.ExprRef])

Bases: object

Parameters:

start (StartStmt)
trace (Trace)
state (SimState)
trace_id (list[int])
ghost_env (dict[str, ExprRef])

ghost_env: dict[str, ExprRef]

start: StartStmt

state: SimState

trace: Trace

trace_id: list[int]

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

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 (StartStmt)
trace (list[int])
path_cond (list[BoolRef])
memstate (MemState)
ghost_env (dict[str, ExprRef])
assertion (EndStmt)

assertion: EndStmt: 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: StartStmt: 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', max_insns=None) → 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]

Execute one actual instruction from the current trace state.

Parameters:

tracestate (TraceState)
ctx (BinaryContext)

Return type:

list[TraceState]

kdrag.contrib.pcode.asmspec.execute_spec_and_insn(tracestate0: TraceState, spec: AsmSpec, ctx: BinaryContext, verbose=True) → tuple[list[TraceState], list[VerificationCondition]]

Execute spec statements and then one instruction.

Parameters:

tracestate0 (TraceState)
spec (AsmSpec)
ctx (BinaryContext)

Return type:

tuple[list[TraceState], list[VerificationCondition]]

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

Execute a list of spec statements on a given trace state.

Parameters:

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

Return type:

tuple[TraceState | None, list[VerificationCondition]]

kdrag.contrib.pcode.asmspec.init_trace_states(ctx: BinaryContext, mem: MemState, spec: AsmSpec, verbose=True) → tuple[list[TraceState], list[VerificationCondition]]

Initialize all trace states from the entry points in the spec. This will run the spec statements after the entry statement and also the first actual instruction.

Parameters:

ctx (BinaryContext)
mem (MemState)
spec (AsmSpec)

Return type:

tuple[list[TraceState], 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, max_insns=None) → 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

kdrag.contrib.pcode.asmspec.update_write(state, ghost_env)