Merge pull request #318 from mrphrazer/translator_bsf_bsr

z3/smt2 translation for  bsf and bsr

1 files changed, 39 insertions, 0 deletions

diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py
index 96f8dab3..e832d3b8 100644
--- a/miasm2/ir/translators/smt2.py
+++ b/miasm2/ir/translators/smt2.py
@@ -237,6 +237,45 @@ class TranslatorSMT2(Translator):
                 res = bvxor(res, bv_extract(i, i, arg))
         elif expr.op == '-':
             res = bvneg(res)
+        elif expr.op == "bsf":
+            src = res
+            size = expr.size
+            size_smt2 = bit_vec_val(size, size)
+            one_smt2 = bit_vec_val(1, size)
+            zero_smt2 = bit_vec_val(0, size)
+            # src & (1 << (size - 1))
+            op = bvand(src, bvshl(one_smt2, bvsub(size_smt2, one_smt2)))
+            # op != 0
+            cond = smt2_distinct(op, zero_smt2)
+            # ite(cond, size - 1, src)
+            res = smt2_ite(cond, bvsub(size_smt2, 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)
+        elif expr.op == "bsr":
+            src = res
+            size = expr.size
+            one_smt2 = bit_vec_val(1, size)
+            zero_smt2 = bit_vec_val(0, size)
+            # (src & 1) != 0
+            cond = smt2_distinct(bvand(src, one_smt2), zero_smt2)
+            # ite(cond, 0, src)
+            res= smt2_ite(cond, zero_smt2, src)
+            for i in xrange(size - 1, 0, -1):
+                index = - i % size
+                index_smt2 = bit_vec_val(index, size)
+                # src & (1 << index)
+                op = bvand(src, bvshl(one_smt2, index_smt2))
+                # op != 0
+                cond = smt2_distinct(op, zero_smt2)
+                # ite(cond, index, res)
+                res = smt2_ite(cond, index_smt2, res)
         else:
             raise NotImplementedError("Unsupported OP yet: %s" % expr.op)