3 files changed, 14 insertions, 12 deletions
diff --git a/miasm2/ir/translators/C.py b/miasm2/ir/translators/C.py
index 0e285669..099f1420 100644
--- a/miasm2/ir/translators/C.py
+++ b/miasm2/ir/translators/C.py
@@ -43,8 +43,8 @@ class TranslatorC(Translator):
             if expr.op == 'parity':
                 return "parity(%s&0x%x)" % (self.from_expr(expr.args[0]),
                                             size2mask(expr.args[0].size))
-            elif expr.op in ['bsr', 'bsf']:
-                return "x86_%s(0x%x, %s)" % (expr.op,
+            elif expr.op in ['cntleadzeros', 'cnttrailzeros']:
+                return "%s(0x%x, %s)" % (expr.op,
                                              expr.args[0].size,
                                              self.from_expr(expr.args[0]))
             elif expr.op in ['clz']:
diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py
index 26ff9127..18bcb9bd 100644
--- a/miasm2/ir/translators/smt2.py
+++ b/miasm2/ir/translators/smt2.py
@@ -233,7 +233,7 @@ class TranslatorSMT2(Translator):
                 res = bvxor(res, bv_extract(i, i, arg))
         elif expr.op == '-':
             res = bvneg(res)
-        elif expr.op == "bsf":
+        elif expr.op == "cnttrailzeros":
             src = res
             size = expr.size
             size_smt2 = bit_vec_val(size, size)
@@ -254,7 +254,7 @@ class TranslatorSMT2(Translator):
                 cond = smt2_distinct(op, zero_smt2)
                 # ite(cond, i, res)
                 res = smt2_ite(cond, i_smt2, res)
-        elif expr.op == "bsr":
+        elif expr.op == "cntleadzeros":
             src = res
             size = expr.size
             one_smt2 = bit_vec_val(1, size)
@@ -271,7 +271,8 @@ class TranslatorSMT2(Translator):
                 # op != 0
                 cond = smt2_distinct(op, zero_smt2)
                 # ite(cond, index, res)
-                res = smt2_ite(cond, index_smt2, res)
+                value_smt2 = bit_vec_val(size - (index + 1), size)
+                res = smt2_ite(cond, value_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 74bdd79c..536daff1 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -207,19 +207,20 @@ class TranslatorZ3(Translator):
                 res = res ^ z3.Extract(i, i, arg)
         elif expr.op == '-':
             res = -res
-        elif expr.op == "bsf":
+        elif expr.op == "cnttrailzeros":
             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 == 0, size, src)
+            for i in xrange(size - 1, -1, -1):
                 res = z3.If((src & (1 << i)) != 0, i, res)
-        elif expr.op == "bsr":
+        elif expr.op == "cntleadzeros":
             size = expr.size
             src = res
-            res = z3.If((src & 1) != 0, 0, src)
-            for i in xrange(size - 1, 0, -1):
+            res = z3.If(src == 0, size, src)
+            for i in xrange(size, 0, -1):
                 index = - i % size
-                res = z3.If((src & (1 << index)) != 0, index, res)
+                out = size - (index + 1)
+                res = z3.If((src & (1 << index)) != 0, out, res)
         else:
             raise NotImplementedError("Unsupported OP yet: %s" % expr.op)