about summary refs log tree commit diff stats
diff options
context:
space:
mode:
authorTim Blazytko <tim.blazytko@rub.de>2016-02-02 10:08:18 +0100
committerTim Blazytko <tim.blazytko@rub.de>2016-02-02 10:08:18 +0100
commita1026122c0007dff2990131a3c9d20fe43ff8907 (patch)
tree3e3e8da71dfc3efaac50d82e0b81751eadae7f0b
parent05d3c612466ee24eef1e2c72cc420ecdb5b92a1e (diff)
downloadmiasm-a1026122c0007dff2990131a3c9d20fe43ff8907.tar.gz
miasm-a1026122c0007dff2990131a3c9d20fe43ff8907.zip
z3 translator: fixed translation for bsr and bsf
-rw-r--r--miasm2/ir/translators/z3_ir.py9
1 files changed, 5 insertions, 4 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index 85997db9..a1b90ae8 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -191,15 +191,16 @@ class TranslatorZ3(Translator):
         elif expr.op == "bsf":
             size = expr.size
             src = res
-            res = z3.If((src & 1) != 0, 1, src)
+            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 & (size - 1)) != 0, 1, src)
-            for i in xrange(size - 2):
-                res = z3.If((src & (1 << i)) != 0, i, 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)