about summary refs log tree commit diff stats
path: root/miasm2/ir/translators/z3_ir.py
diff options
context:
space:
mode:
Diffstat (limited to 'miasm2/ir/translators/z3_ir.py')
-rw-r--r--miasm2/ir/translators/z3_ir.py13
1 files changed, 13 insertions, 0 deletions
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)