kdrag.contrib.ir

SSA is Functional Programming by Andrew Appel https://www.cs.princeton.edu/~appel/papers/ssafun.pdf

Functional programming and SSA can be put into close correspondence. It is to some degree a matter of pretty printing.

The recipe is to define one function per block that takes in all the currently live variables as arguments. These are also called “block arguments” and are a structural alternative to phi nodes.

SSA variables are then just references given to previous expressions. A maximal let bound form can be written. https://en.wikipedia.org/wiki/A-normal_form

Jumps are calls to the other function blocks

Functions

pp_sort(s)

Classes

`Block`(sig, insns)
`Function`(entry, blocks)
`Spec`(pre, z3.z3.BoolRef] =, post, ...)

class kdrag.contrib.ir.Block(sig: list[z3.z3.SortRef], insns: list[z3.z3.ExprRef])

Bases: object

Parameters:

sig (list[SortRef])
insns (list[ExprRef])

insns: list[ExprRef]

classmethod of_expr(e: ExprRef) → Block

>>> x,y = smt.BitVecs("x y", 64)
>>> x,y = smt.Var(1, smt.BitVecSort(64)), smt.Var(0, smt.BitVecSort(64))
>>> z = smt.BitVec("z", 64)
>>> Block.of_expr(smt.If(True, (x + y)*42, x - y + z))
^(bv64,bv64):
%0 = bvadd %var1, %var0
%1 = bvmul %0, 42
%2 = bvsub %var1, %var0
%3 = bvadd %2, z
%4 = if True, %1, %3

Parameters:: e (ExprRef)
Return type:: Block

sig: list[SortRef]

succ_calls() → list[ExprRef]

Return type:: list[ExprRef]

vname(e: ExprRef) → str

Parameters:: e (ExprRef)
Return type:: str

class kdrag.contrib.ir.Function(entry: Label, blocks: dict[Label, kdrag.contrib.ir.Block])

Bases: object

Parameters:

entry (Label)
blocks (dict[Label, Block])

blocks: dict[Label, Block]

calls_of() → dict[str, list[tuple[Label, ExprRef]]]

Returns a mapping from labels to a list of calls to that label

Return type:: dict[str, list[tuple[Label, ExprRef]]]

entry: Label

phis(): Return the analog a mapping from labels to phi nodes in that block

type kdrag.contrib.ir.Label = str

class kdrag.contrib.ir.Spec(pre: dict[str, z3.z3.BoolRef]=<factory>, post: dict[str, z3.z3.BoolRef]=<factory>, cut: dict[str, z3.z3.BoolRef]=<factory>)

Bases: object

Parameters:

pre (dict[str, BoolRef])
post (dict[str, BoolRef])
cut (dict[str, BoolRef])

cut: dict[str, BoolRef]

post: dict[str, BoolRef]

pre: dict[str, BoolRef]

kdrag.contrib.ir.pp_sort(s: SortRef) → str

Parameters:: s (SortRef)
Return type:: str

Modules

`mlir`
`qbe`