From 68bacc75b53a77296980a58d5051b696ffe1c219 Mon Sep 17 00:00:00 2001 From: Ajax Date: Fri, 9 Feb 2018 15:30:26 +0100 Subject: Deprecate expr_cmps/expr_cmpu for a more verbose / understandable API --- test/expression/simplifications.py | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index e4c3f2e9..53283bef 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -3,7 +3,6 @@ # from pdb import pm from miasm2.expression.expression import * -from miasm2.expression.expression_helper import expr_cmpu, expr_cmps from miasm2.expression.simplifications import expr_simp, ExpressionSimplifier from miasm2.expression.simplifications_cond import ExprOp_inf_signed, ExprOp_inf_unsigned, ExprOp_equal @@ -268,37 +267,37 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), a[:16]), ((a << ExprInt(16, 32))[24:32], a[8:16]), - (expr_cmpu(ExprInt(0, 32), ExprInt(0, 32)), + (expr_is_unsigned_greater(ExprInt(0, 32), ExprInt(0, 32)), ExprInt(0, 1)), - (expr_cmpu(ExprInt(10, 32), ExprInt(0, 32)), + (expr_is_unsigned_greater(ExprInt(10, 32), ExprInt(0, 32)), ExprInt(1, 1)), - (expr_cmpu(ExprInt(10, 32), ExprInt(5, 32)), + (expr_is_unsigned_greater(ExprInt(10, 32), ExprInt(5, 32)), ExprInt(1, 1)), - (expr_cmpu(ExprInt(5, 32), ExprInt(10, 32)), + (expr_is_unsigned_greater(ExprInt(5, 32), ExprInt(10, 32)), ExprInt(0, 1)), - (expr_cmpu(ExprInt(-1, 32), ExprInt(0, 32)), + (expr_is_unsigned_greater(ExprInt(-1, 32), ExprInt(0, 32)), ExprInt(1, 1)), - (expr_cmpu(ExprInt(-1, 32), ExprInt(-1, 32)), + (expr_is_unsigned_greater(ExprInt(-1, 32), ExprInt(-1, 32)), ExprInt(0, 1)), - (expr_cmpu(ExprInt(0, 32), ExprInt(-1, 32)), + (expr_is_unsigned_greater(ExprInt(0, 32), ExprInt(-1, 32)), ExprInt(0, 1)), - (expr_cmps(ExprInt(0, 32), ExprInt(0, 32)), + (expr_is_signed_greater(ExprInt(0, 32), ExprInt(0, 32)), ExprInt(0, 1)), - (expr_cmps(ExprInt(10, 32), ExprInt(0, 32)), + (expr_is_signed_greater(ExprInt(10, 32), ExprInt(0, 32)), ExprInt(1, 1)), - (expr_cmps(ExprInt(10, 32), ExprInt(5, 32)), + (expr_is_signed_greater(ExprInt(10, 32), ExprInt(5, 32)), ExprInt(1, 1)), - (expr_cmps(ExprInt(5, 32), ExprInt(10, 32)), + (expr_is_signed_greater(ExprInt(5, 32), ExprInt(10, 32)), ExprInt(0, 1)), - (expr_cmps(ExprInt(-1, 32), ExprInt(0, 32)), + (expr_is_signed_greater(ExprInt(-1, 32), ExprInt(0, 32)), ExprInt(0, 1)), - (expr_cmps(ExprInt(-1, 32), ExprInt(-1, 32)), + (expr_is_signed_greater(ExprInt(-1, 32), ExprInt(-1, 32)), ExprInt(0, 1)), - (expr_cmps(ExprInt(0, 32), ExprInt(-1, 32)), + (expr_is_signed_greater(ExprInt(0, 32), ExprInt(-1, 32)), ExprInt(1, 1)), - (expr_cmps(ExprInt(-5, 32), ExprInt(-10, 32)), + (expr_is_signed_greater(ExprInt(-5, 32), ExprInt(-10, 32)), ExprInt(1, 1)), - (expr_cmps(ExprInt(-10, 32), ExprInt(-5, 32)), + (expr_is_signed_greater(ExprInt(-10, 32), ExprInt(-5, 32)), ExprInt(0, 1)), (ExprOp("idiv", ExprInt(0x0123, 16), ExprInt(0xfffb, 16))[:8], -- cgit 1.4.1 From f9905707570a030a40d844f68ccfea4d8a3ecc23 Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 14:22:46 +0100 Subject: Add a check against z3 in simplifications regression tests --- test/expression/simplifications.py | 84 ++++++++++++++++++++++++++++++++------ test/test_all.py | 3 ++ 2 files changed, 75 insertions(+), 12 deletions(-) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 53283bef..949aa6ff 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -2,10 +2,73 @@ # Expression simplification regression tests # # from pdb import pm +from argparse import ArgumentParser + from miasm2.expression.expression import * from miasm2.expression.simplifications import expr_simp, ExpressionSimplifier from miasm2.expression.simplifications_cond import ExprOp_inf_signed, ExprOp_inf_unsigned, ExprOp_equal +parser = ArgumentParser("Expression simplification regression tests") +parser.add_argument("--z3", action="store_true", help="Enable check against z3") +parser.add_argument("--z3-timeout", type=int, help="z3 timeout (in seconds)", + default=20) +args = parser.parse_args() + +# Additionnal imports and definitions +if args.z3: + import z3 + from miasm2.ir.translators import Translator + trans = Translator.to_language("z3") + + def check(expr_in, expr_out): + """Check that expr_in is always equals to expr_out""" + print "Ensure %s = %s" % (expr_in, expr_out) + solver = z3.Solver() + solver.set("timeout", args.z3_timeout * 1000) + try: + solver.add(trans.from_expr(expr_in) != trans.from_expr(expr_out)) + except NotImplementedError as error: + print "Unable to translate in z3", error + return + + result = solver.check() + if result == z3.unknown: + print "-> Timeout!" + return + + if result != z3.unsat: + print "ERROR: a counter-example has been founded:" + model = solver.model() + print model + + print "Reinjecting in the simplifier:" + to_rep = {} + expressions = expr_in.get_r().union(expr_out.get_r()) + for expr in expressions: + value = model.eval(trans.from_expr(expr)) + if hasattr(value, "as_long"): + new_val = ExprInt(value.as_long(), expr.size) + else: + raise RuntimeError("Unable to reinject %r" % value) + + to_rep[expr] = new_val + + new_expr_in = expr_in.replace_expr(to_rep) + new_expr_out = expr_out.replace_expr(to_rep) + + print "Check %s = %s" % (new_expr_in, new_expr_out) + simp_in = expr_simp(new_expr_in) + simp_out = expr_simp(new_expr_out) + print "[%s] %s = %s" % (simp_in == simp_out, simp_in, simp_out) + + # Either the simplification does not stand, either the test is wrong + raise RuntimeError("Bad simplification") + +else: + # Dummy 'check' method to avoid checking the '--z3' argument each time + check = lambda expr_in, expr_out: None + + # Define example objects a = ExprId('a', 32) b = ExprId('b', 32) @@ -316,16 +379,15 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ] -for e, e_check in to_test[:]: - # +for e_input, e_check in to_test: print "#" * 80 - # print str(e), str(e_check) - e_new = expr_simp(e) - print "original: ", str(e), "new: ", str(e_new) + e_new = expr_simp(e_input) + print "original: ", str(e_input), "new: ", str(e_new) rez = e_new == e_check if not rez: raise ValueError( - 'bug in expr_simp simp(%s) is %s and should be %s' % (e, e_new, e_check)) + 'bug in expr_simp simp(%s) is %s and should be %s' % (e_input, e_new, e_check)) + check(e_input, e_check) # Test conds @@ -355,17 +417,15 @@ expr_simp_cond = ExpressionSimplifier() expr_simp.enable_passes(ExpressionSimplifier.PASS_COND) -for e, e_check in to_test[:]: - # +for e_input, e_check in to_test: print "#" * 80 e_check = expr_simp(e_check) - # print str(e), str(e_check) - e_new = expr_simp(e) - print "original: ", str(e), "new: ", str(e_new) + e_new = expr_simp(e_input) + print "original: ", str(e_input), "new: ", str(e_new) rez = e_new == e_check if not rez: raise ValueError( - 'bug in expr_simp simp(%s) is %s and should be %s' % (e, e_new, e_check)) + 'bug in expr_simp simp(%s) is %s and should be %s' % (e_input, e_new, e_check)) diff --git a/test/test_all.py b/test/test_all.py index 04aca62e..6aa2a97e 100755 --- a/test/test_all.py +++ b/test/test_all.py @@ -249,6 +249,9 @@ for script in ["modint.py", "expr_cmp.py", ]: testset += RegressionTest([script], base_dir="expression") +testset += RegressionTest(["simplifications.py", "--z3"], + base_dir="expression", + tags=[TAGS["z3"]]) ## ObjC/CHandler testset += RegressionTest(["test_chandler.py"], base_dir="expr_type", -- cgit 1.4.1 From 775ad64ad56f390e3c2b063794cdbfa1da58febc Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 14:23:46 +0100 Subject: Check that expr_is_* are really computing the expected operation --- test/expression/simplifications.py | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 949aa6ff..77c7b78e 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -427,6 +427,36 @@ for e_input, e_check in to_test: raise ValueError( 'bug in expr_simp simp(%s) is %s and should be %s' % (e_input, e_new, e_check)) +if args.z3: + # This check is done on 32 bits, but the size is not use by Miasm formulas, so + # it should be OK for any size > 0 + 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) + + # (Assumptions, function(arg1, arg2) -> True/False (= i1/i0) to check) + tests = [ + (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), + ] + + for assumption, func in tests: + solver = z3.Solver() + solver.add(assumption) + solver.add(trans.from_expr(func(x1, x2)) != i1_z3) + assert solver.check() == z3.unsat x = ExprId('x', 32) -- cgit 1.4.1 From 0056026fa2f07b49d54236148ad5c528b18b381f Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 14:39:53 +0100 Subject: Use 3 arguments to highlight the recent #677 patch --- test/expression/simplifications.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 77c7b78e..8799191b 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -196,9 +196,9 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), (ExprOp('*', a, b, c, ExprInt(0x12, 32))[0:17], ExprOp( '*', a[0:17], b[0:17], c[0:17], ExprInt(0x12, 17))), - (ExprOp('*', a, ExprInt(0x0, 32)), + (ExprOp('*', a, b, ExprInt(0x0, 32)), ExprInt(0x0, 32)), - (ExprOp('&', a, ExprInt(0x0, 32)), + (ExprOp('&', a, b, ExprInt(0x0, 32)), ExprInt(0x0, 32)), (ExprOp('*', a, ExprInt(0xffffffff, 32)), -a), -- cgit 1.4.1 From c887ab5c5da2c12ccb84be93da238a9c9be3e229 Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 14:46:18 +0100 Subject: A >> X >> Y => A >> (X+Y) ONLY IF X + Y does not overflow --- miasm2/expression/simplifications_common.py | 9 +++++++-- test/expression/simplifications.py | 9 +++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) (limited to 'test/expression') diff --git a/miasm2/expression/simplifications_common.py b/miasm2/expression/simplifications_common.py index 6eb5e804..6840a0ac 100644 --- a/miasm2/expression/simplifications_common.py +++ b/miasm2/expression/simplifications_common.py @@ -212,10 +212,15 @@ def simp_cst_propagation(e_s, expr): args0 = args[0].args[0] args = [args0, args1] - # A >> X >> Y => A >> (X+Y) + # A >> X >> Y => A >> (X+Y) if X + Y does not overflow + # To be sure, only consider the simplification when X.msb and Y.msb are 0 if (op_name in ['<<', '>>'] and args[0].is_op(op_name)): - args = [args[0].args[0], args[0].args[1] + args[1]] + X = args[0].args[1] + Y = args[1] + if (e_s(X.msb()) == ExprInt(0, 1) and + e_s(Y.msb()) == ExprInt(0, 1)): + args = [args[0].args[0], X + Y] # ((A & A.mask) if op_name == "&" and args[-1] == expr.mask: diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 8799191b..5a223f7c 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -77,6 +77,9 @@ 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) + m = ExprMem(a) s = a[:8] @@ -377,6 +380,12 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ((ExprMem(ExprCond(a, b, c)),ExprCond(a, ExprMem(b), ExprMem(c)))), (ExprCond(a, i0, i1) + ExprCond(a, i0, i1), ExprCond(a, i0, i2)), + (a << b << c, a << b << c), # Left unmodified + (a << b_msb_null << c_msb_null, + a << (b_msb_null + c_msb_null)), + (a >> b >> c, a >> b >> c), # Left unmodified + (a >> b_msb_null >> c_msb_null, + a >> (b_msb_null + c_msb_null)), ] for e_input, e_check in to_test: -- cgit 1.4.1 From 47246b797bff382b508c52c467c63abe320c82bd Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 16:44:46 +0100 Subject: ExpressionSimplification: Add a verbose mode --- miasm2/expression/simplifications.py | 14 ++++++++++++++ test/expression/simplifications.py | 8 +++++++- 2 files changed, 21 insertions(+), 1 deletion(-) (limited to 'test/expression') diff --git a/miasm2/expression/simplifications.py b/miasm2/expression/simplifications.py index d3483d9e..e6c5dc54 100644 --- a/miasm2/expression/simplifications.py +++ b/miasm2/expression/simplifications.py @@ -2,6 +2,8 @@ # Simplification methods library # # # +import logging + from miasm2.expression import simplifications_common from miasm2.expression import simplifications_cond from miasm2.expression.expression_helper import fast_unify @@ -10,6 +12,12 @@ import miasm2.expression.expression as m2_expr # Expression Simplifier # --------------------- +log_exprsimp = logging.getLogger("exprsimp") +console_handler = logging.StreamHandler() +console_handler.setFormatter(logging.Formatter("%(levelname)-5s: %(message)s")) +log_exprsimp.addHandler(console_handler) +log_exprsimp.setLevel(logging.WARNING) + class ExpressionSimplifier(object): @@ -67,9 +75,15 @@ class ExpressionSimplifier(object): Return an Expr instance""" cls = expression.__class__ + debug_level = log_exprsimp.level >= logging.DEBUG for simp_func in self.expr_simp_cb.get(cls, []): # Apply simplifications + before = expression expression = simp_func(self, expression) + after = expression + + if debug_level and before != after: + log_exprsimp.debug("[%s] %s => %s", simp_func, before, after) # If class changes, stop to prevent wrong simplifications if expression.__class__ is not cls: diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 5a223f7c..cb8dc4f8 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -3,17 +3,23 @@ # from pdb import pm from argparse import ArgumentParser +import logging from miasm2.expression.expression import * -from miasm2.expression.simplifications import expr_simp, ExpressionSimplifier +from miasm2.expression.simplifications import expr_simp, ExpressionSimplifier, log_exprsimp from miasm2.expression.simplifications_cond import ExprOp_inf_signed, ExprOp_inf_unsigned, ExprOp_equal parser = ArgumentParser("Expression simplification regression tests") parser.add_argument("--z3", action="store_true", help="Enable check against z3") +parser.add_argument("-v", "--verbose", action="store_true", + help="Verbose simplify") parser.add_argument("--z3-timeout", type=int, help="z3 timeout (in seconds)", default=20) args = parser.parse_args() +if args.verbose: + log_exprsimp.setLevel(logging.DEBUG) + # Additionnal imports and definitions if args.z3: import z3 -- cgit 1.4.1 From 8e5fa3a219da14ee0e2f7096c6ba3e164cce959d Mon Sep 17 00:00:00 2001 From: Ajax Date: Tue, 13 Feb 2018 16:45:39 +0100 Subject: Update rot simplification, to avoid overflow cases --- miasm2/expression/simplifications_common.py | 35 +++++++++++++++------- test/expression/simplifications.py | 45 ++++++++++++++++++++++------- 2 files changed, 59 insertions(+), 21 deletions(-) (limited to 'test/expression') diff --git a/miasm2/expression/simplifications_common.py b/miasm2/expression/simplifications_common.py index 22e328e1..ccb97cb3 100644 --- a/miasm2/expression/simplifications_common.py +++ b/miasm2/expression/simplifications_common.py @@ -196,21 +196,34 @@ def simp_cst_propagation(e_s, expr): args[1].arg == args[0].size): return args[0] - # A <<< X <<< Y => A <<< (X+Y) (ou <<< >>>) + # (A <<< X) <<< Y => A <<< (X+Y) (or <<< >>>) if X + Y does not overflow if (op_name in ['<<<', '>>>'] and args[0].is_op() and args[0].op in ['<<<', '>>>']): - op1 = op_name - op2 = args[0].op - if op1 == op2: - op_name = op1 - args1 = args[0].args[1] + args[1] - else: - op_name = op2 - args1 = args[0].args[1] - args[1] + A = args[0].args[0] + X = args[0].args[1] + Y = args[1] + if op_name != args[0].op and e_s(X - Y) == ExprInt(0, X.size): + return args[0].args[0] + elif X.is_int() and Y.is_int(): + new_X = int(X) % expr.size + new_Y = int(Y) % expr.size + if op_name == args[0].op: + rot = (new_X + new_Y) % expr.size + op = op_name + else: + rot = new_Y - new_X + op = op_name + if rot < 0: + rot = - rot + op = {">>>": "<<<", "<<<": ">>>"}[op_name] + args = [A, ExprInt(rot, expr.size)] + op_name = op - args0 = args[0].args[0] - args = [args0, args1] + else: + # Do not consider this case, too tricky (overflow on addition / + # substraction) + pass # A >> X >> Y => A >> (X+Y) if X + Y does not overflow # To be sure, only consider the simplification when X.msb and Y.msb are 0 diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index cb8dc4f8..2650d4d1 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -86,6 +86,13 @@ 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) + + m = ExprMem(a) s = a[:8] @@ -120,17 +127,35 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), (ExprOp('>>>', a, ExprInt(32, 32)), a), (ExprOp('>>>', a, ExprInt(0, 32)), a), (ExprOp('<<', a, ExprInt(0, 32)), a), + (ExprOp('<<<', a31, ExprInt(31, 31)), a31), + (ExprOp('>>>', a31, ExprInt(31, 31)), a31), + (ExprOp('>>>', a31, ExprInt(0, 31)), a31), + (ExprOp('<<', a31, ExprInt(0, 31)), a31), + + (ExprOp('<<<', a31, ExprOp('<<<', b31, c31)), + ExprOp('<<<', a31, ExprOp('<<<', b31, c31))), + (ExprOp('<<<', ExprOp('>>>', a31, b31), c31), + ExprOp('<<<', ExprOp('>>>', a31, b31), c31)), + (ExprOp('>>>', ExprOp('<<<', a31, b31), c31), + ExprOp('>>>', ExprOp('<<<', a31, b31), c31)), + (ExprOp('>>>', ExprOp('<<<', a31, b31), b31), + a31), + (ExprOp('<<<', ExprOp('>>>', a31, b31), b31), + a31), + (ExprOp('>>>', ExprOp('>>>', a31, b31), b31), + ExprOp('>>>', ExprOp('>>>', a31, b31), b31)), + (ExprOp('<<<', ExprOp('<<<', a31, b31), b31), + ExprOp('<<<', ExprOp('<<<', a31, b31), b31)), + + (ExprOp('>>>', ExprOp('<<<', a31, ExprInt(0x1234, 31)), ExprInt(0x1111, 31)), + ExprOp('>>>', a31, ExprInt(0x13, 31))), + (ExprOp('<<<', ExprOp('>>>', a31, ExprInt(0x1234, 31)), ExprInt(0x1111, 31)), + ExprOp('<<<', a31, ExprInt(0x13, 31))), + (ExprOp('>>>', ExprOp('<<<', a31, ExprInt(-1, 31)), ExprInt(0x1111, 31)), + ExprOp('>>>', a31, ExprInt(0x1c, 31))), + (ExprOp('<<<', ExprOp('>>>', a31, ExprInt(-1, 31)), ExprInt(0x1111, 31)), + ExprOp('<<<', a31, ExprInt(0x1c, 31))), - (ExprOp('<<<', a, ExprOp('<<<', b, c)), - ExprOp('<<<', a, ExprOp('<<<', b, c))), - (ExprOp('<<<', ExprOp('<<<', a, b), c), - ExprOp('<<<', a, (b+c))), - (ExprOp('<<<', ExprOp('>>>', a, b), c), - ExprOp('>>>', a, (b-c))), - (ExprOp('>>>', ExprOp('<<<', a, b), c), - ExprOp('<<<', a, (b-c))), - (ExprOp('>>>', ExprOp('<<<', a, b), b), - a), (ExprOp(">>>", ExprInt(0x1000, 16), ExprInt(0x11, 16)), ExprInt(0x800, 16)), (ExprOp("<<<", ExprInt(0x1000, 16), ExprInt(0x11, 16)), -- cgit 1.4.1 From 63a67ae9731392afdc47ff36a57eaefc49d2f727 Mon Sep 17 00:00:00 2001 From: Ajax Date: Wed, 14 Feb 2018 12:26:52 +0100 Subject: Remove int '**' int test to let z3 always translate exprs ('**' was not really used in Miasm) --- test/expression/simplifications.py | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 2650d4d1..871ff0f4 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -30,12 +30,7 @@ if args.z3: """Check that expr_in is always equals to expr_out""" print "Ensure %s = %s" % (expr_in, expr_out) solver = z3.Solver() - solver.set("timeout", args.z3_timeout * 1000) - try: - solver.add(trans.from_expr(expr_in) != trans.from_expr(expr_out)) - except NotImplementedError as error: - print "Unable to translate in z3", error - return + solver.add(trans.from_expr(expr_in) != trans.from_expr(expr_out)) result = solver.check() if result == z3.unknown: @@ -240,8 +235,6 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ExprOp('*', a, b, c, ExprInt(0x12, 32))), (ExprOp('*', -a, -b, -c, ExprInt(0x12, 32)), - ExprOp('*', a, b, c, ExprInt(0x12, 32))), - (ExprOp('**', ExprInt(2, 32), ExprInt(8, 32)), ExprInt(0x100, 32)), - (ExprInt(2, 32)**ExprInt(8, 32), ExprInt(256, 32)), (a | ExprInt(0xffffffff, 32), ExprInt(0xffffffff, 32)), (ExprCond(a, ExprInt(1, 32), ExprInt(2, 32)) * ExprInt(4, 32), -- cgit 1.4.1 From 0f55f0779555c38cd907143527d4ddbf26c18157 Mon Sep 17 00:00:00 2001 From: Ajax Date: Wed, 14 Feb 2018 12:27:35 +0100 Subject: Lower the size of too long test to let z3 run in a human time --- test/expression/simplifications.py | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'test/expression') diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 871ff0f4..0c516a8e 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -13,8 +13,6 @@ parser = ArgumentParser("Expression simplification regression tests") parser.add_argument("--z3", action="store_true", help="Enable check against z3") parser.add_argument("-v", "--verbose", action="store_true", help="Verbose simplify") -parser.add_argument("--z3-timeout", type=int, help="z3 timeout (in seconds)", - default=20) args = parser.parse_args() if args.verbose: @@ -33,9 +31,6 @@ if args.z3: solver.add(trans.from_expr(expr_in) != trans.from_expr(expr_out)) result = solver.check() - if result == z3.unknown: - print "-> Timeout!" - return if result != z3.unsat: print "ERROR: a counter-example has been founded:" @@ -87,6 +82,12 @@ 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) s = a[:8] @@ -241,8 +242,8 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ExprCond(a, ExprInt(4, 32), ExprInt(8, 32))), (ExprCond(a, b, c) + ExprCond(a, d, e), ExprCond(a, b + d, c + e)), - (ExprCond(a, b, c) * ExprCond(a, d, e), - ExprCond(a, b * d, c * e)), + (ExprCond(a8, b8, c8) * ExprCond(a8, d8, e8), + ExprCond(a8, b8 * d8, c8 * e8)), (ExprCond(a, ExprInt(8, 32), ExprInt(4, 32)) >> ExprInt(1, 32), ExprCond(a, ExprInt(4, 32), ExprInt(2, 32))), @@ -401,7 +402,7 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ExprInt(0x0321, 16))), (ExprCompose(ExprCond(a, i1, i0), ExprCond(a, i1, i2)), ExprCond(a, ExprInt(0x100000001, 64), ExprInt(0x200000000, 64))), - ((ExprMem(ExprCond(a, b, c)),ExprCond(a, ExprMem(b), ExprMem(c)))), + ((ExprMem(ExprCond(a, b, c), 4),ExprCond(a, ExprMem(b, 4), ExprMem(c, 4)))), (ExprCond(a, i0, i1) + ExprCond(a, i0, i1), ExprCond(a, i0, i2)), (a << b << c, a << b << c), # Left unmodified -- cgit 1.4.1