z3_ir.py File Reference

Namespaces
	z3_ir

Functions
def	z3_ir.equiv (z3_expr1, z3_expr2)
def	z3_ir.check_interp (interp, constraints, bits=32, valbits=8)

Variables
	z3_ir.loc_db = LocationDB()
	z3_ir.translator1 = TranslatorZ3(endianness="<", loc_db=loc_db)
	z3_ir.translator2 = TranslatorZ3(endianness=">", loc_db=loc_db)
	z3_ir.mem = Z3Mem(endianness='<')
	z3_ir.eax = z3.BitVec('EAX', 32)
	z3_ir.ax = z3.BitVec('AX', 16)
	z3_ir.e = ExprId('x', 32)
	z3_ir.ez3 = translator1.from_expr(e)
	z3_ir.z3_e = z3.BitVec('x', 32)
	z3_ir.four = ExprInt(4, 32)
	z3_ir.five = ExprInt(5, 32)
tuple	z3_ir.e2 = (e + five + four) * five
	z3_ir.z3_four = z3.BitVecVal(4, 32)
	z3_ir.z3_five = z3.BitVecVal(5, 32)
tuple	z3_ir.z3_e2 = (z3_e + z3_five + z3_four) * z3_five
	z3_ir.emem = ExprMem(ExprInt(0xdeadbeef, 32), size=32)
	z3_ir.emem2 = ExprMem(ExprInt(0xfee1dead, 32), size=32)
tuple	z3_ir.e3 = (emem + e) * ExprInt(2, 32) * emem2
	z3_ir.z3_emem = mem.get(z3.BitVecVal(0xdeadbeef, 32), 32)
	z3_ir.z3_emem2 = mem.get(z3.BitVecVal(0xfee1dead, 32), 32)
tuple	z3_ir.z3_e3 = (z3_emem + z3_e) * z3.BitVecVal(2, 32) * z3_emem2
	z3_ir.e4 = emem * five
	z3_ir.z3_e4 = z3_emem * z3_five
	z3_ir.solver = z3.Solver()
	z3_ir.model = solver.model()
	z3_ir.memb = Z3Mem(endianness=">")
	z3_ir.e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five
	z3_ir.z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five
	z3_ir.seven = ExprInt(7, 32)
	z3_ir.one0seven = ExprInt(0x107, 32)
	z3_ir.e6 = ExprOp('parity', miasm_int)
	z3_ir.z3_e6 = z3.BitVecVal(res, 1)
	z3_ir.label_histoire = loc_db.add_location("label_histoire", 0xdeadbeef)
	z3_ir.e7 = ExprLoc(label_histoire, 32)
	z3_ir.z3_e7 = z3.BitVecVal(0xdeadbeef, 32)
	z3_ir.lbl_e8 = loc_db.add_location("label_jambe")
	z3_ir.e8 = ExprLoc(lbl_e8, 32)
	z3_ir.cnttrailzeros1 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32)))
	z3_ir.cnttrailzeros2 = z3.BitVecVal(3, 32)
	z3_ir.cntleadzeros1 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32)))
	z3_ir.cntleadzeros2 = z3.BitVecVal(0xf, 32)
	z3_ir.cnttrailzeros3 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32))
	z3_ir.cntleadzeros3 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32)))