diff options
| author | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:34:37 +0100 |
|---|---|---|
| committer | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:34:37 +0100 |
| commit | 6b0665ec2f0386fbd28e169cf098bc99242c6241 (patch) | |
| tree | 490b091595d64d1cc5149bda8f5bf436f6fe6311 | |
| parent | 964e02f46b383cab5ed056ee7120d185dac2dcf4 (diff) | |
| download | miasm-6b0665ec2f0386fbd28e169cf098bc99242c6241.tar.gz miasm-6b0665ec2f0386fbd28e169cf098bc99242c6241.zip | |
smt2 translator: added translation for bsf and bsr
| -rw-r--r-- | miasm2/ir/translators/smt2.py | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py index f5fbf427..9de1e00e 100644 --- a/miasm2/ir/translators/smt2.py +++ b/miasm2/ir/translators/smt2.py @@ -247,6 +247,69 @@ class TranslatorSMT2(Translator): res = bvxor(res, bv_extract(i, i, arg)) elif expr.op == '-': res = bvneg(res) + elif expr.op == "bsf": + size = expr.size + src = res + one_smt2 = bit_vec_val(1, size) + zero_smt2 = bit_vec_val(0, size) + if self.is_little_endian(): + # (src & 1) != 0 + cond = smt2_distinct(bvand(src, one_smt2), zero_smt2) + # ite((src & 1) != 0, 1, src) + res = smt2_ite(cond, one_smt2, src) + for i in xrange(size - 2, -1, -1): + # smt2 expression of i + i_smt2 = bit_vec_val(i, size) + # src & (1 << i) + op = bvand(src, bvshl(one_smt2, i_smt2)) + # op != 0 + cond = smt2_distinct(op, zero_smt2) + # ite(cond, i, res) + res = smt2_ite(cond, i_smt2, res) + else: + # (src & (size - 1)) != 0 + cond = smt2_distinct(bvand(src, bit_vec_val(size - 1, size)), zero_smt2) + res = smt2_ite(cond, one_smt2, src) + for i in xrange(size - 2): + # smt2 expression of i + i_smt2 = bit_vec_val(i, size) + # src & (1 << i) + op = bvand(src, bvshl(one_smt2, i_smt2)) + # op != 0 + cond = smt2_distinct(op, zero_smt2) + # ite(cond, i, res) + res = smt2_ite(cond, i_smt2, res) + elif expr.op == "bsr": + size = expr.size + src = res + one_smt2 = bit_vec_val(1, size) + zero_smt2 = bit_vec_val(0, size) + if self.is_little_endian(): + # (src & (size - 1)) != 0 + cond = smt2_distinct(bvand(src, bit_vec_val(size - 1, size)), zero_smt2) + res = smt2_ite(cond, one_smt2, src) + for i in xrange(size - 2): + # smt2 expression of i + i_smt2 = bit_vec_val(i, size) + # src & (1 << i) + op = bvand(src, bvshl(one_smt2, i_smt2)) + # op != 0 + cond = smt2_distinct(op, zero_smt2) + # ite(cond, i, res) + res = smt2_ite(cond, i_smt2, res) + else: + # (src & 1) != 0 + cond = smt2_distinct(bvand(src, one_smt2), zero_smt2) + # ite((src & 1) != 0, 1, src) + res = smt2_ite(cond, one_smt2, src) + for i in xrange(size - 2, -1, -1): + i_smt2 = bit_vec_val(i, size) + # src & (1 << i) + op = bvand(src, bvshl(one_smt2, i_smt2)) + # op != 0 + cond = smt2_distinct(op, zero_smt2) + # ite(cond, i, res) + res = smt2_ite(cond, i_smt2, res) else: raise NotImplementedError("Unsupported OP yet: %s" % expr.op) |