Functions
def	equiv (z3_expr1, z3_expr2)

def	check_interp (interp, constraints, bits=32, valbits=8)

Variables
	loc_db = LocationDB()

	translator1 = TranslatorZ3(endianness="<", loc_db=loc_db)

	translator2 = TranslatorZ3(endianness=">", loc_db=loc_db)

	mem = Z3Mem(endianness='<')

	eax = z3.BitVec('EAX', 32)

	ax = z3.BitVec('AX', 16)

	e = ExprId('x', 32)

	ez3 = translator1.from_expr(e)

	z3_e = z3.BitVec('x', 32)

	four = ExprInt(4, 32)

	five = ExprInt(5, 32)

tuple	e2 = (e + five + four) * five

	z3_four = z3.BitVecVal(4, 32)

	z3_five = z3.BitVecVal(5, 32)

tuple	z3_e2 = (z3_e + z3_five + z3_four) * z3_five

	emem = ExprMem(ExprInt(0xdeadbeef, 32), size=32)

	emem2 = ExprMem(ExprInt(0xfee1dead, 32), size=32)

tuple	e3 = (emem + e) * ExprInt(2, 32) * emem2

	z3_emem = mem.get(z3.BitVecVal(0xdeadbeef, 32), 32)

	z3_emem2 = mem.get(z3.BitVecVal(0xfee1dead, 32), 32)

tuple	z3_e3 = (z3_emem + z3_e) * z3.BitVecVal(2, 32) * z3_emem2

	e4 = emem * five

	z3_e4 = z3_emem * z3_five

	solver = z3.Solver()

	model = solver.model()

	memb = Z3Mem(endianness=">")

	e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five

	z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five

	seven = ExprInt(7, 32)

	one0seven = ExprInt(0x107, 32)

	e6 = ExprOp('parity', miasm_int)

	z3_e6 = z3.BitVecVal(res, 1)

	label_histoire = loc_db.add_location("label_histoire", 0xdeadbeef)

	e7 = ExprLoc(label_histoire, 32)

	z3_e7 = z3.BitVecVal(0xdeadbeef, 32)

	lbl_e8 = loc_db.add_location("label_jambe")

	e8 = ExprLoc(lbl_e8, 32)

	cnttrailzeros1 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32)))

	cnttrailzeros2 = z3.BitVecVal(3, 32)

	cntleadzeros1 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32)))

	cntleadzeros2 = z3.BitVecVal(0xf, 32)

	cnttrailzeros3 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32))

	cntleadzeros3 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32)))

Function Documentation

◆ check_interp()

def z3_ir.check_interp	(	interp,
		constraints,
		bits = `32`,
		valbits = `8`
	)

Checks that a list of @constraints (addr, value) (as python ints)
match a z3 FuncInterp (@interp).

Here is the call graph for this function:

◆ equiv()

def z3_ir.equiv	(	z3_expr1,
		z3_expr2
	)

Here is the caller graph for this function:

Variable Documentation

◆ ax

z3_ir.ax = z3.BitVec('AX', 16)

◆ cntleadzeros1

z3_ir.cntleadzeros1 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32)))

◆ cntleadzeros2

z3_ir.cntleadzeros2 = z3.BitVecVal(0xf, 32)

◆ cntleadzeros3

z3_ir.cntleadzeros3 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32)))

◆ cnttrailzeros1

z3_ir.cnttrailzeros1 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32)))

◆ cnttrailzeros2

z3_ir.cnttrailzeros2 = z3.BitVecVal(3, 32)

◆ cnttrailzeros3

z3_ir.cnttrailzeros3 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32))

◆ e

z3_ir.e = ExprId('x', 32)

◆ e2

tuple z3_ir.e2 = (e + five + four) * five

◆ e3

tuple z3_ir.e3 = (emem + e) * ExprInt(2, 32) * emem2

◆ e4

z3_ir.e4 = emem * five

◆ e5

z3_ir.e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five

◆ e6

z3_ir.e6 = ExprOp('parity', miasm_int)

◆ e7

z3_ir.e7 = ExprLoc(label_histoire, 32)

◆ e8

z3_ir.e8 = ExprLoc(lbl_e8, 32)

◆ eax

z3_ir.eax = z3.BitVec('EAX', 32)

◆ emem

z3_ir.emem = ExprMem(ExprInt(0xdeadbeef, 32), size=32)

◆ emem2

z3_ir.emem2 = ExprMem(ExprInt(0xfee1dead, 32), size=32)

◆ ez3

z3_ir.ez3 = translator1.from_expr(e)

◆ five

z3_ir.five = ExprInt(5, 32)

◆ four

z3_ir.four = ExprInt(4, 32)

◆ label_histoire

z3_ir.label_histoire = loc_db.add_location("label_histoire", 0xdeadbeef)

◆ lbl_e8

z3_ir.lbl_e8 = loc_db.add_location("label_jambe")

◆ loc_db

z3_ir.loc_db = LocationDB()

◆ mem

z3_ir.mem = Z3Mem(endianness='<')

◆ memb

z3_ir.memb = Z3Mem(endianness=">")

◆ model

z3_ir.model = solver.model()

◆ one0seven

z3_ir.one0seven = ExprInt(0x107, 32)

◆ seven

z3_ir.seven = ExprInt(7, 32)

◆ solver

z3_ir.solver = z3.Solver()

◆ translator1

z3_ir.translator1 = TranslatorZ3(endianness="<", loc_db=loc_db)

◆ translator2

z3_ir.translator2 = TranslatorZ3(endianness=">", loc_db=loc_db)

◆ z3_e

z3_ir.z3_e = z3.BitVec('x', 32)

◆ z3_e2

tuple z3_ir.z3_e2 = (z3_e + z3_five + z3_four) * z3_five

◆ z3_e3

tuple z3_ir.z3_e3 = (z3_emem + z3_e) * z3.BitVecVal(2, 32) * z3_emem2

◆ z3_e4

z3_ir.z3_e4 = z3_emem * z3_five

◆ z3_e5

z3_ir.z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five

◆ z3_e6

z3_ir.z3_e6 = z3.BitVecVal(res, 1)

◆ z3_e7

z3_ir.z3_e7 = z3.BitVecVal(0xdeadbeef, 32)

◆ z3_emem

z3_ir.z3_emem = mem.get(z3.BitVecVal(0xdeadbeef, 32), 32)

◆ z3_emem2

z3_ir.z3_emem2 = mem.get(z3.BitVecVal(0xfee1dead, 32), 32)

◆ z3_five

z3_ir.z3_five = z3.BitVecVal(5, 32)

◆ z3_four

z3_ir.z3_four = z3.BitVecVal(4, 32)

Functions

Variables