Merge pull request #318 from mrphrazer/translator_bsf_bsr

z3/smt2 translation for  bsf and bsr

3 files changed, 70 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)
 
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index b6645d2b..a1b90ae8 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -188,6 +188,19 @@ class TranslatorZ3(Translator):
                 res = res ^ z3.Extract(i, i, arg)
         elif expr.op == '-':
             res = -res
+        elif expr.op == "bsf":
+            size = expr.size
+            src = res
+            res = z3.If((src & (1 << (size - 1))) != 0, size - 1, src)
+            for i in xrange(size - 2, -1, -1):
+                res = z3.If((src & (1 << i)) != 0, i, res)
+        elif expr.op == "bsr":
+            size = expr.size
+            src = res
+            res = z3.If((src & 1) != 0, 0, src)
+            for i in xrange(size - 1, 0, -1):
+                index = - i % size
+                res = z3.If((src & (1 << index)) != 0, index, res)
         else:
             raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
 
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index a4fa7410..e080c7f5 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -149,5 +149,23 @@ e8 = ExprId(asm_label("label_jambe"), 32)
 ez3 = Translator.to_language('z3').from_expr(e8)
 assert not equiv(ez3, z3_e7)
 
+# --------------------------------------------------------------------------
+# bsr, bsf
+
+# bsf(0x1138) == 3
+bsf1 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x1138, 32)))
+bsf2 = z3.BitVecVal(3, 32)
+assert(equiv(bsf1, bsf2))
+
+# bsr(0x11300) == 0x10
+bsr1 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x11300, 32)))
+bsr2 = z3.BitVecVal(0x10, 32)
+assert(equiv(bsr1, bsr2))
+
+# bsf(0x80000) == bsr(0x80000)
+bsf3 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x80000, 32)))
+bsr3 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x80000, 32)))
+assert(equiv(bsf3, bsr3))
+
 print "TranslatorZ3 tests are OK."