diff options
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 97a0397a..beaba618 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -205,6 +205,36 @@ class TranslatorZ3(Translator): res = res - (arg * (self._idivC(res, arg))) elif expr.op == "umod": res = z3.URem(res, arg) + elif expr.op == "==": + res = z3.If( + args[0] == args[1], + z3.BitVecVal(1, 1), + z3.BitVecVal(0, 1) + ) + elif expr.op == "<u": + res = z3.If( + z3.ULT(args[0], args[1]), + z3.BitVecVal(1, 1), + z3.BitVecVal(0, 1) + ) + elif expr.op == "<s": + res = z3.If( + z3.SLT(args[0], args[1]), + z3.BitVecVal(1, 1), + z3.BitVecVal(0, 1) + ) + elif expr.op == "<=u": + res = z3.If( + z3.ULE(args[0], args[1]), + z3.BitVecVal(1, 1), + z3.BitVecVal(0, 1) + ) + elif expr.op == "<=s": + res = z3.If( + z3.SLE(args[0], args[1]), + z3.BitVecVal(1, 1), + z3.BitVecVal(0, 1) + ) else: raise NotImplementedError("Unsupported OP yet: %s" % expr.op) elif expr.op == 'parity': |