simplifications Namespace Reference

Functions
def	check (expr_in, expr_out)

Variables
	parser = ArgumentParser("Expression simplification regression tests")
	action
	help
	args = parser.parse_args()
	trans = Translator.to_language("z3")
	check = lambda expr_in, expr_out: None
	a = ExprId('a', 32)
	b = ExprId('b', 32)
	c = ExprId('c', 32)
	d = ExprId('d', 32)
	e = ExprId('e', 32)
	f = ExprId('f', size=64)
	b_msb_null = b[:31].zeroExtend(32)
	c_msb_null = c[:31].zeroExtend(32)
	a31 = ExprId('a31', 31)
	b31 = ExprId('b31', 31)
	c31 = ExprId('c31', 31)
	b31_msb_null = ExprId('b31', 31)[:30].zeroExtend(31)
	c31_msb_null = ExprId('c31', 31)[:30].zeroExtend(31)
	a8 = ExprId('a8', 8)
	b8 = ExprId('b8', 8)
	c8 = ExprId('c8', 8)
	d8 = ExprId('d8', 8)
	e8 = ExprId('e8', 8)
	m = ExprMem(a, 32)
	s = a[:8]
	i0 = ExprInt(0, 32)
	i1 = ExprInt(1, 32)
	i2 = ExprInt(2, 32)
	i3 = ExprInt(3, 32)
	im1 = ExprInt(-1, 32)
	im2 = ExprInt(-2, 32)
	bi0 = ExprInt(0, 1)
	bi1 = ExprInt(1, 1)
	icustom = ExprInt(0x12345678, 32)
	cc = ExprCond(a, b, c)
	o = ExprCompose(a[8:16], a[:8])
	o2 = ExprCompose(a[8:16], a[:8])
list	l = [a[:8], b[:8], c[:8], m[:8], s, i1[:8], i2[:8], o[:8]]
list	l2 = l[::-1]
	x = ExprMem(a + b + ExprInt(0x42, 32), 32)
list	to_test
	e_new = expr_simp_explicit(e_input)
	rez = e_check
	e_check = expr_simp(e_check)
	x1 = ExprId("x1", 32)
	x2 = ExprId("x2", 32)
	i1_tmp = ExprInt(1, 1)
	x1_z3 = trans.from_expr(x1)
	x2_z3 = trans.from_expr(x2)
	i1_z3 = trans.from_expr(i1_tmp)
list	tests
	solver = z3.Solver()
	y = ExprId('y', 32)
	z = ExprId('z', 32)
	jra = ExprId('jra', 32)
	jrb = ExprId('jrb', 32)
	jrint1 = ExprId('jrint1', 32)
	e1 = ExprMem((a & ExprInt(0xFFFFFFFC, 32)) + ExprInt(0x10, 32), 32)
	e2 = ExprMem((a & ExprInt(0xFFFFFFFC, 32)) + b, 32)
tuple	e3 = (a ^ b ^ ((a ^ b) & (b ^ (b - a))) ^ (b - a)).canonize()
list	match_tests
list	get_tests

Function Documentation

check()

def simplifications.check	(		expr_in,
			expr_out
	)

Check that expr_in is always equals to expr_out

Variable Documentation

a

simplifications.a = ExprId('a', 32)

a31

simplifications.a31 = ExprId('a31', 31)

a8

simplifications.a8 = ExprId('a8', 8)

action

simplifications.action

args

simplifications.args = parser.parse_args()

b

simplifications.b = ExprId('b', 32)

b31

simplifications.b31 = ExprId('b31', 31)

b31_msb_null

simplifications.b31_msb_null = ExprId('b31', 31)[:30].zeroExtend(31)

b8

simplifications.b8 = ExprId('b8', 8)

b_msb_null

simplifications.b_msb_null = b[:31].zeroExtend(32)

bi0

simplifications.bi0 = ExprInt(0, 1)

bi1

simplifications.bi1 = ExprInt(1, 1)

c

simplifications.c = ExprId('c', 32)

c31

simplifications.c31 = ExprId('c31', 31)

c31_msb_null

simplifications.c31_msb_null = ExprId('c31', 31)[:30].zeroExtend(31)

c8

simplifications.c8 = ExprId('c8', 8)

c_msb_null

simplifications.c_msb_null = c[:31].zeroExtend(32)

cc

simplifications.cc = ExprCond(a, b, c)

check

simplifications.check = lambda expr_in, expr_out: None

d

simplifications.d = ExprId('d', 32)

d8

simplifications.d8 = ExprId('d8', 8)

e

simplifications.e = ExprId('e', 32)

e1

simplifications.e1 = ExprMem((a & ExprInt(0xFFFFFFFC, 32)) + ExprInt(0x10, 32), 32)

e2

simplifications.e2 = ExprMem((a & ExprInt(0xFFFFFFFC, 32)) + b, 32)

e3

tuple simplifications.e3 = (a ^ b ^ ((a ^ b) & (b ^ (b - a))) ^ (b - a)).canonize()

e8

simplifications.e8 = ExprId('e8', 8)

e_check

simplifications.e_check = expr_simp(e_check)

e_new

simplifications.e_new = expr_simp_explicit(e_input)

f

simplifications.f = ExprId('f', size=64)

get_tests

list simplifications.get_tests

Initial value:

=  [
    (ExprAssign(ExprMem(a, 32), ExprMem(b, 32)).get_r(True), set([a, b, ExprMem(b, 32)])),
    (ExprAssign(ExprMem(a, 32), ExprMem(b, 32)).get_w(), set([ExprMem(a, 32)])),
    (ExprAssign(ExprMem(ExprMem(a, 32), 32), ExprMem(b, 32))
     .get_r(True), set([a, b, ExprMem(b, 32), ExprMem(a, 32)])),
]

help

simplifications.help

i0

simplifications.i0 = ExprInt(0, 32)

i1

simplifications.i1 = ExprInt(1, 32)

i1_tmp

simplifications.i1_tmp = ExprInt(1, 1)

i1_z3

simplifications.i1_z3 = trans.from_expr(i1_tmp)

i2

simplifications.i2 = ExprInt(2, 32)

i3

simplifications.i3 = ExprInt(3, 32)

icustom

simplifications.icustom = ExprInt(0x12345678, 32)

im1

simplifications.im1 = ExprInt(-1, 32)

im2

simplifications.im2 = ExprInt(-2, 32)

jra

simplifications.jra = ExprId('jra', 32)

jrb

simplifications.jrb = ExprId('jrb', 32)

jrint1

simplifications.jrint1 = ExprId('jrint1', 32)

l

list simplifications.l = [a[:8], b[:8], c[:8], m[:8], s, i1[:8], i2[:8], o[:8]]

l2

list simplifications.l2 = l[::-1]

m

simplifications.m = ExprMem(a, 32)

match_tests

list simplifications.match_tests

Initial value:

=  [
    (match_expr(ExprInt(12, 32), a, [a]), {a: ExprInt(12, 32)}),
    (match_expr(x, a, [a]), {a: x}),
    (match_expr(x + y, a, [a]), {a: x + y}),
    (match_expr(x + y, a + y, [a]), {a: x}),
    (match_expr(x + y, x + a, [a]), {a: y}),
    (match_expr(x + y, a + b, [a, b]), {a: x, b: y}),
    (match_expr(x + ExprInt(12, 32), a + b, [a, b]), {a: x, b: ExprInt(12, 32)}),
    (match_expr(ExprMem(x, 32), a, [a]), {a: ExprMem(x, 32)}),
    (match_expr(ExprMem(x, 32), ExprMem(a, 32), [a]), {a: x}),
    (match_expr(x[0:8], a, [a]), {a: x[0:8]}),
    (match_expr(x[0:8], a[0:8], [a]), {a: x}),
    (match_expr(ExprCond(x, y, z), a, [a]), {a: ExprCond(x, y, z)}),
    (match_expr(ExprCond(x, y, z),
               ExprCond(a, b, c), [a, b, c]),
     {a: x, b: y, c: z}),
    (match_expr(ExprCompose(x[:8], y[:8]), a, [a]),
     {a: ExprCompose(x[:8], y[:8])}),
    (match_expr(ExprCompose(x[:8], y[:8]),
               ExprCompose(a[:8], b[:8]), [a, b]),
     {a: x, b: y}),
    (match_expr(e1, e2, [b]), {b: ExprInt(0x10, 32)}),
    (match_expr(e3,
               (((jra ^ jrb) & (jrb ^ jrint1))
                ^ jra ^ jrb ^ jrint1).canonize(),
               [jra, jrb, jrint1]),
     {jra: a, jrb: b, jrint1: b - a}),
]

o

simplifications.o = ExprCompose(a[8:16], a[:8])

o2

simplifications.o2 = ExprCompose(a[8:16], a[:8])

parser

simplifications.parser = ArgumentParser("Expression simplification regression tests")

rez

simplifications.rez = e_check

s

simplifications.s = a[:8]

solver

simplifications.solver = z3.Solver()

tests

list simplifications.tests

Initial value:

=  [
        (x1_z3 == x2_z3, expr_is_equal),
        (x1_z3 != x2_z3, expr_is_not_equal),
        (z3.UGT(x1_z3, x2_z3), expr_is_unsigned_greater),
        (z3.UGE(x1_z3, x2_z3), expr_is_unsigned_greater_or_equal),
        (z3.ULT(x1_z3, x2_z3), expr_is_unsigned_lower),
        (z3.ULE(x1_z3, x2_z3), expr_is_unsigned_lower_or_equal),
        (x1_z3 > x2_z3, expr_is_signed_greater),
        (x1_z3 >= x2_z3, expr_is_signed_greater_or_equal),
        (x1_z3 < x2_z3, expr_is_signed_lower),
        (x1_z3 <= x2_z3, expr_is_signed_lower_or_equal),
    ]

to_test

list simplifications.to_test

trans

simplifications.trans = Translator.to_language("z3")

x

simplifications.x = ExprMem(a + b + ExprInt(0x42, 32), 32)

x1

simplifications.x1 = ExprId("x1", 32)

x1_z3

simplifications.x1_z3 = trans.from_expr(x1)

x2

simplifications.x2 = ExprId("x2", 32)

x2_z3

simplifications.x2_z3 = trans.from_expr(x2)

y

simplifications.y = ExprId('y', 32)

z

simplifications.z = ExprId('z', 32)