diff options
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 1e02ea9a..a2cf9271 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -197,6 +197,28 @@ class TranslatorZ3(Translator): res = res ^ z3.Extract(i, i, arg) elif expr.op == '-': res = -res + elif expr.op == "bsf": + size = expr.size + src = res + if self.is_little_endian(): + res = z3.If((src & 1) != 0, 1, src) + for i in xrange(size - 2, -1, -1): + res = z3.If((src & (1 << i)) != 0, i, res) + else: + res = z3.If((src & (size - 1)) != 0, 1, src) + for i in xrange(size - 2): + res = z3.If((src & (1 << i)) != 0, i, res) + elif expr.op == "bsr": + size = expr.size + src = res + if self.is_little_endian(): + res = z3.If((src & (size - 1)) != 0, 1, src) + for i in xrange(size - 2): + res = z3.If((src & (1 << i)) != 0, i, res) + else: + res = z3.If((src & 1) != 0, 1, src) + for i in xrange(size - 2, -1, -1): + res = z3.If((src & (1 << i)) != 0, i, res) else: raise NotImplementedError("Unsupported OP yet: %s" % expr.op) |