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_ghost`(e, ghost_env)	Substitute ghost variables in an expression.
`substitute_state`(e, ctx, memstate, ghost_env)	Substitute both ghost state and context state (ram / registers).
`update_write_and_num_insn`(state, ghost_env)

Classes

`Always`(expr)
`AsmProof`(spec, pfs)
`AsmProofState`(spec)
`AsmSpec`(ctx, 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, ...)
`VCProofState`(vc, ctx[, _parent])
`VerificationCondition`(start, trace, ...)	The result of symbolic execution over a path.

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

Bases: object

Parameters:: expr (StateProp)

expr: StateProp

class kdrag.contrib.pcode.asmspec.AsmProof(spec: kdrag.contrib.pcode.asmspec.AsmSpec, pfs: tuple[kdrag.kernel.Proof])

Bases: object

Parameters:

spec (AsmSpec)
pfs (tuple[Proof])

pfs: tuple[Proof]

spec: AsmSpec

class kdrag.contrib.pcode.asmspec.AsmProofState(spec: AsmSpec)

Bases: object

Parameters:: spec (AsmSpec)

auto(n, **kwargs)

exact(pf: Proof)

Parameters:: pf (Proof)

lemma(n) → VCProofState

Return type:: VCProofState

qed()

class kdrag.contrib.pcode.asmspec.AsmSpec(ctx: ~kdrag.contrib.pcode.BinaryContext, 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:

ctx (BinaryContext)
addrmap (defaultdict[int, list[SpecStmt]])

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

Parameters:

label (str)
addr (int)
expr (StateProp)

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

Parameters:

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

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

Parameters:

label (str)
addr (int)
expr (StateProp)

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

Parameters:

label (str)
addr (int)
expr (StateProp)

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

Parameters:

label (str)
addr (int)
expr (StateProp)

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

Parameters:

label (str)
addr (int)
expr (StateProp)

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

ctx: BinaryContext

find_label(label: str) → int

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

json()

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

Parameters:

filename (str)
ctx (BinaryContext)

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

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

label: str

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

Bases: object

Parameters:

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

addr: int

expr: StateExpr

label: str

name: str

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

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

label: str

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

Bases: object

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

label: str

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

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

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

verify(**kwargs)

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

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

label: str

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

Bases: BoolStmt

Parameters:

label (str)
addr (int)
expr (StateProp)

addr: int

expr: StateProp

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.VCProofState(vc: VerificationCondition, ctx: BinaryContext, _parent=None)

Bases: ProofState

Parameters:

vc (VerificationCondition)
ctx (BinaryContext)

__enter__() → ProofState

On entering a with block, return self. This marks that at the exit of the with block, qed will be automatically called and kd.Proof propagated back to a parent

Return type:: ProofState

__exit__(exc_type, exc_value, traceback): On exiting a with block, if no exception occurred, call qed and propagate the proof to the parent

add_lemma(lemma: Proof)

Record a lemma in the current ProofState state.

Parameters:: lemma (Proof)

admit() → Goal

admit the current goal without proof. Don’t feel bad about keeping yourself moving, but be aware that you’re not done.

>>> l = Lemma(smt.BoolVal(False)) # a false goal
>>> _ = l.admit()
Admitting lemma False
>>> l.qed()
|= False

Return type:: Goal

apply(pf: Proof | int)

apply matches the conclusion of a proven clause

>>> x,y = smt.Ints("x y")
>>> l = kd.Lemma(smt.Implies(smt.Implies(x == 7, y == 3), y == 3))
>>> l.intros()
[Implies(x == 7, y == 3)] ?|= y == 3
>>> l.apply(0)
[Implies(x == 7, y == 3)] ?|= x == 7

>>> mylemma = kd.prove(kd.QForAll([x], x > 1, x > 0))
>>> kd.Lemma(x > 0).apply(mylemma)
[] ?|= x > 1

>>> p,q = smt.Bools("p q")
>>> l = kd.Lemma(smt.Implies(smt.Not(p), q))
>>> l.intros()
[Not(p)] ?|= q
>>> l.apply(0)
[Not(q)] ?|= p

Parameters:: pf (Proof | int)

assumes(hyp: BoolRef)

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p, q))
>>> l.assumes(p)
[p] ?|= q

Parameters:: hyp (BoolRef)

assumption() → Goal

Exact match of goal in the context

Return type:: Goal

auto(**kwargs): auto discharges a goal using z3. It forwards all parameters to kd.prove

beta(at=None)

Perform beta reduction on goal or context

>>> x = smt.Int("x")
>>> l = Lemma(smt.Lambda([x], x + 1)[3] == 4)
>>> l.beta()
[] ?|= 3 + 1 == 4
>>> l = Lemma(smt.Implies(smt.Lambda([x], x + 1)[3] == 5, True))
>>> l.intros()
[Lambda(x, x + 1)[3] == 5] ?|= True
>>> l.beta(at=0)
[3 + 1 == 5] ?|= True

case(thm=None) → ProofState

To make more readable proofs, case lets you state which case you are currently in from a cases It is basically an alias for have followed by clear(-1).

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Or(p, smt.Not(p)))
>>> _ = l.cases(p)
>>> l.case(p)
[p == True] ?|= Or(p, Not(p))
>>> _ = l.auto()
>>> l.case(smt.Not(p))
[p == False] ?|= Or(p, Not(p))

Return type:: ProofState

cases(t)

cases let’s us consider an object by cases. We consider whether Bools are True or False We consider the different constructors for datatypes

>>> import kdrag.theories.nat as nat
>>> x = smt.Const("x", nat.Nat)
>>> l = Lemma(smt.BoolVal(True))
>>> l.cases(x)
[is(Z, x) == True] ?|= True
>>> l.auto() # next case
[is(S, x) == True] ?|= True

clear(n: int)

Remove a hypothesis from the context

Parameters:: n (int)

contra()

Prove the goal by contradiction.

>>> p = smt.Bool("p")
>>> l = Lemma(p)
>>> l.contra()
[Not(p)] ?|= False

copy()

ProofState methods mutates the proof state. This can make you a copy. Does not copy the pushed ProofState stack.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l1 = l.copy()
>>> l.intros()
[p] ?|= q
>>> l1
[] ?|= Implies(p, q)

emt(): Use egraph based equality modulo theories to simplify the goal. >>> x, y, z, w = smt.Ints(“x y z w”) >>> l = Lemma(smt.Implies(x + y + 1 == z, x + y + 1 == w)) >>> l.intros() [x + y + 1 == z] ?|= x + y + 1 == w >>> l.emt() [x + y + 1 == z] ?|= z == w

eq(rhs: ExprRef, **kwargs)

replace rhs in equational goal

Parameters:: rhs (ExprRef)

exact(pf: Proof)

Exact match of goal with given proof

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Implies(p, p))
>>> l.exact(kd.prove(smt.BoolVal(True)))
Traceback (most recent call last):
    ...
ValueError: Exact tactic failed. Given: True Expected: Implies(p, p)
>>> l.exact(kd.prove(smt.Implies(p, p)))
Nothing to do!

Parameters:: pf (Proof)

exists(*ts) → ProofState

Give terms ts to satisfy an exists goal ?|= exists x, p(x) becomes ?|= p(ts)

>>> x,y = smt.Ints("x y")
>>> Lemma(smt.Exists([x], x == y)).exists(y)
[] ?|= y == y

Return type:: ProofState

ext(at=None)

Apply extensionality to a goal

>>> x = smt.Int("x")
>>> l = Lemma(smt.Lambda([x], smt.IntVal(1)) == smt.K(smt.IntSort(), smt.IntVal(1)))
>>> _ = l.ext()

fix(prefix=None) → ExprRef

Open a single ForAll quantifier

>>> x = smt.Int("x")
>>> l = Lemma(smt.ForAll([x], x != x + 1))
>>> _x = l.fix()
>>> l
[x!...] ; [] ?|= x!... != x!... + 1
>>> _x.eq(x)
False
>>> Lemma(smt.ForAll([x], x != x + 1)).fix("w")
w!...

Return type:: ExprRef

fixes(prefixes=None) → list[ExprRef]

fixes opens a forall quantifier. ?|= forall x, p(x) becomes x ?|= p(x)

>>> x,y = smt.Ints("x y")
>>> l = Lemma(kd.QForAll([x,y], y >= 0, x + y >= x))
>>> _x, _y = l.fixes()
>>> l
[x!..., y!...] ?|= Implies(y!... >= 0, x!... + y!... >= x!...)
>>> _x, _y
(x!..., y!...)
>>> _x.eq(x)
False
>>> Lemma(kd.QForAll([x,y], x >= 0)).fixes("z w")
[z!..., w!...]

Return type:: list[ExprRef]

generalize(*vs: ExprRef)

Put variables forall quantified back on goal. Useful for strengthening induction hypotheses.

Parameters:: vs (ExprRef)

get_lemma(thm: BoolRef) → Proof

Parameters:: thm (BoolRef)
Return type:: Proof

have(conc: BoolRef, **kwargs) → ProofState

Prove the given formula and add it to the current context

>>> x = smt.Int("x")
>>> l = Lemma(smt.Implies(x > 0, x > -2))
>>> l.intros()
[x > 0] ?|= x > -2
>>> l.have(x > -1, by=[])
[x > 0, x > -1] ?|= x > -2
>>> l.have(x > 42)
[x > 0, x > -1] ?|= x > 42

Parameters:: conc (BoolRef)
Return type:: ProofState

induct(x: ExprRef, using: Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None = None)

Apply an induction lemma instantiated on x.

Parameters:

x (ExprRef)
using (Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None)

intros() → ExprRef | list[ExprRef] | Goal

intros opens an implication. ?|= p -> q becomes p ?|= q

>>> p,q,r = smt.Bools("p q r")
>>> l = Lemma(smt.Implies(p, q))
>>> l.intros()
[p] ?|= q
>>> l = Lemma(smt.Not(q))
>>> l.intros()
[q] ?|= False

Return type:: ExprRef | list[ExprRef] | Goal

left(n=0)

Select the left case of an Or goal. Since we’re working classically, the other cases are negated and added to the context.

>>> p,q,r = smt.Bools("p q r")
>>> l = Lemma(smt.Or(p,q))
>>> l.left()
[Not(q)] ?|= p
>>> l = Lemma(smt.Or(p,q,r))
>>> l.left(1)
[Not(p), Not(r)] ?|= q

newgoal(newgoal: BoolRef, **kwargs)

Try to show newgoal is sufficient to prove current goal

Parameters:: newgoal (BoolRef)

obtain(n) → ExprRef | list[ExprRef]

obtain opens an exists quantifier in context and returns the fresh eigenvariable. [exists x, p(x)] ?|= goal becomes p(x) ?|= goal

Return type:: ExprRef | list[ExprRef]

pop(): Pop state off the ProofState stack.

pop_goal() → Goal

Return type:: Goal

pop_lemmas()

push()

Push a copy of the current ProofState state onto a stack. This why you can try things out, and if they fail

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l.push()
[] ?|= Implies(p, q)
>>> l.intros()
[p] ?|= q
>>> l.pop()
[] ?|= Implies(p, q)

push_lemmas()

qed(**kwargs) → Proof

return the actual final Proof of the lemma that was defined at the beginning.

Return type:: Proof

qfix(prefix=None) → ExprRef

Return type:: ExprRef

qfixes(prefixes=None) → list[ExprRef]

Return type:: list[ExprRef]

repeat(f: Callable[[], Goal]) → Goal

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Implies(p, smt.Implies(p, p)))
>>> l.intros()
[p] ?|= Implies(p, p)
>>> l = Lemma(smt.Implies(p, smt.Implies(p, p)))
>>> l.repeat(lambda: l.intros())
[p, p] ?|= p

Parameters:: f (Callable[[], Goal])
Return type:: Goal

revert(n: int)

Move a hypothesis back onto the goal as an implication. >>> p,q = smt.Bools(“p q”) >>> l = Lemma(smt.Implies(p, q)) >>> l.intros() [p] ?|= q >>> l.revert(0) [] ?|= Implies(p, q)

Parameters:: n (int)

right()

Select the right case of an Or goal. Since we’re working classically, the other cases are negated and added to the context.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Or(p,q))
>>> l.right()
[Not(p)] ?|= q

rw(rule: Proof | int, at=None, rev=False, **kwargs) → ProofState

rewrite allows you to apply rewrite rule (which may either be a Proof or an index into the context) to the goal or to the context.

>>> x = kd.FreshVar("x", smt.RealSort())
>>> pf = kd.prove(smt.Implies(x >= 0, smt.Sqrt(x) ** 2 == x)).forall([x])
>>> l = Lemma(smt.Implies(x >= 0, smt.Sqrt(x + 2)**2 == x + 2))
>>> l.intros()
[x!... >= 0] ?|= ((x!... + 2)**(1/2))**2 == x!... + 2
>>> l.rw(pf,by=[])
[x!... >= 0, x!... + 2 >= 0] ?|= x!... + 2 == x!... + 2

Parameters:: rule (Proof | int)
Return type:: ProofState

search(*args, at=None, db={})

Search the lemma database for things that may match the current goal.

>>> import kdrag.theories.nat as nat
>>> n = smt.Const("n", nat.Nat)
>>> l = Lemma(smt.ForAll([n], nat.Z + n == n))
>>> ("kdrag.theories.nat.add_Z", nat.add_Z) in l.search().keys()
True
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search().keys()
False
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search(nat.add).keys()
True

show(thm: BoolRef, **kwargs) → ProofState

Documents the current goal and discharge it if by keyword is used

>>> x = smt.Int("x")
>>> l = Lemma(smt.Implies(x > 0, smt.And(x > -2, x > -1)))
>>> l.intros()
[x > 0] ?|= And(x > -2, x > -1)
>>> l.split()
[x > 0] ?|= x > -2
>>> with l.show(x > -2).sub() as sub1:
...     _ = sub1.auto()
>>> l
[x > 0] ?|= x > -1
>>> l.show(x > -1, by=[])
Nothing to do. Hooray!
>>> l.qed()
|= Implies(x > 0, And(x > -2, x > -1))

Parameters:: thm (BoolRef)
Return type:: ProofState

simp(at=None, unfold=False, path=None) → ProofState

Use built in z3 simplifier. May be useful for boolean, arithmetic, lambda, and array simplifications.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(x + y == y + x)
>>> l.simp()
[] ?|= True
>>> l = Lemma(x == 3 + y + 7)
>>> l.simp()
[] ?|= x == 10 + y
>>> l = Lemma(smt.Lambda([x], x + 1)[3] == y)
>>> l.simp()
[] ?|= 4 == y
>>> l = Lemma(1 + ((2 + smt.IntVal(4)) + 3))
>>> l.simp(path=[1,0])
[] ?|= 1 + 6 + 3

Return type:: ProofState

specialize(n, *ts)

Instantiate a universal quantifier in the context.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(smt.Implies(smt.ForAll([x],x == y), True))
>>> l.intros()
[ForAll(x, x == y)] ?|= True
>>> l.specialize(0, smt.IntVal(42))
[ForAll(x, x == y), 42 == y] ?|= True

split(at=None) → ProofState

split breaks apart an And or bi-implication == goal. The optional keyword at allows you to break apart an And or Or in the context

>>> p = smt.Bool("p")
>>> l = Lemma(smt.And(True,p))
>>> l.split()
[] ?|= True
>>> l.auto() # next goal
[] ?|= p

Return type:: ProofState

sub() → ProofState

Return type:: ProofState

sublemma() → ProofState

Create a sub ProofState for the current goal. This is useful to break up a proof into smaller lemmas. The goal is the same but the internally held kd.Proof database is cleared, making it easier for z3 On calling ‘l.qed(), the sublemma will propagate it’s kd.Proof back to it’s parent.

>>> l1 = Lemma(smt.BoolVal(True))
>>> l2 = l1.sublemma()
>>> l2
[] ?|= True
>>> l2.auto()
Nothing to do. Hooray!
>>> l1
[] ?|= True
>>> l2.qed()
|= True
>>> l1
Nothing to do. Hooray!
>>> l1.qed()
|= True

Return type:: ProofState

symm()

Swap left and right hand side of equational goal

>>> x,y = smt.Ints("x y")
>>> Lemma(x == y).symm()
[] ?|= y == x

top_goal() → Goal

Return type:: Goal

unfold(*decls: FuncDeclRef, at=None, keep=False) → ProofState

Unfold all definitions once. If declarations are given, only those are unfolded.

>>> import kdrag.theories.nat as nat
>>> l = Lemma(nat.Z + nat.Z == nat.Z)
>>> l
[] ?|= add(Z, Z) == Z
>>> l.unfold(nat.double) # does not unfold add
[] ?|= add(Z, Z) == Z
>>> l.unfold()
[] ?|= If(is(Z, Z), Z, S(add(pred(Z), Z))) == Z

Parameters:: decls (FuncDeclRef)
Return type:: ProofState

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_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.substitute_state(e: ExprRef, ctx: BinaryContext, memstate: MemState, ghost_env: dict[str, ExprRef]) → ExprRef

Substitute both ghost state and context state (ram / registers). Converts an expression in state variables to one that one that extracts those values from the given memstate and ghost_env.

Parameters:

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

Return type:

ExprRef

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