diff options
| author | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:33:29 +0100 |
|---|---|---|
| committer | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:33:29 +0100 |
| commit | 964e02f46b383cab5ed056ee7120d185dac2dcf4 (patch) | |
| tree | 0c5ade8953cc140f523fffb190a6ada43877872b | |
| parent | 1762857e070241533412e63cf1d417e678700a70 (diff) | |
| download | miasm-964e02f46b383cab5ed056ee7120d185dac2dcf4.tar.gz miasm-964e02f46b383cab5ed056ee7120d185dac2dcf4.zip | |
z3 translator: added translation for bsf and bsr
| -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) |