diff options
Diffstat (limited to 'miasm2/ir/translators/z3_ir.py')
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 97a0397a..1cc8c29d 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -144,7 +144,7 @@ class TranslatorZ3(Translator): return z3.BitVec(str(loc_key), expr.size) def from_ExprMem(self, expr): - addr = self.from_expr(expr.arg) + addr = self.from_expr(expr.ptr) return self._mem.get(addr, expr.size) def from_ExprSlice(self, expr): @@ -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': |