diff --git a/claripy/operations.py b/claripy/operations.py index b97cc44..5a3d108 100644 --- a/claripy/operations.py +++ b/claripy/operations.py @@ -333,6 +333,14 @@ def boolean_reverse_simplifier(body): if body.length == 8: return body + if body.op == 'Extract': + high,low = body.args[:2] + if high % 8 == 7 and low % 8 == 0: + if body.args[2].op == 'Reverse': + bits = body.args[2].args[0].size() + if bits % 8 == 0: + return body.make_like(body.op,[bits - 1 - low,bits - 1 - high,body.args[2].args[0]]) + if body.op == 'Concat': if all(a.op == 'Extract' for a in body.args): first_ast = body.args[0].args[2] @@ -351,9 +359,9 @@ def boolean_reverse_simplifier(body): return body.make_like(body.op, body.args[::-1]) if body.op == 'Concat': - if all(a.op == 'Reverse' for a in body.args): + if all(a.op == 'Reverse' or (a.op == 'BVV' and a.args[0] == 0) for a in body.args): if all(a.length % 8 == 0 for a in body.args): - return body.make_like(body.op,reversed([a.args[0] for a in body.args])) + return body.make_like(body.op,reversed([a.args[0] if a.op == 'Reverse' else a for a in body.args])) def boolean_and_simplifier(*args): if len(args) == 1: @@ -543,6 +551,11 @@ def bitwise_xor_simplifier(a, b): result = bitwise_xor_simplifier_minmax(a,b) if result is not None: return result + if a.op == 'Concat' and b.op == 'Concat': + if len(a.args) == len(b.args): + if all(x.size() == y.size() for x,y in zip(a.args,b.args)): + return ast.all_operations.Concat(*[x ^ y for x,y in zip(a.args,b.args)]) + def _flattening_filter(args): # since a ^ a == 0, we can safely remove those from args # this procedure is done carefully in order to keep the ordering of arguments @@ -578,6 +591,11 @@ def bitwise_and_simplifier(a, b): elif a is b: return a + if a.op == 'Concat' and b.op == 'Concat': + if len(a.args) == len(b.args): + if all(x.size() == y.size() for x,y in zip(a.args,b.args)): + return ast.all_operations.Concat(*[x & y for x,y in zip(a.args,b.args)]) + def _flattening_filter(args): # a & a == a return tuple(OrderedSet(args)) @@ -641,6 +659,14 @@ def extract_simplifier(high, low, val): if (val.op == 'SignExt' or val.op == 'ZeroExt') and low == 0 and high + 1 == val.args[1].size(): return val.args[1] + # (SignExt(n,v)>>s)[b-1:0] => v>>s if v has b bits + # XXX: do rshift semantics guarantee that shift distance is in range? + if val.op == '__rshift__': + if val.args[0].op == 'SignExt': + bits = val.args[0].args[1].size() + if low == 0 and high == bits - 1 and val.args[0].args[0] + bits < 2**(bits - 1): + return val.args[0].args[1].make_like(val.op,[val.args[0].args[1],val.args[1][bits-1:0]]) + if val.op == 'ZeroExt': extending_bits = val.args[0] if extending_bits == 0: -- 2.18.0