diff options
| -rw-r--r-- | miasm2/arch/x86/sem.py | 20 | ||||
| -rw-r--r-- | miasm2/ir/translators/C.py | 1 | ||||
| -rw-r--r-- | miasm2/ir/translators/__init__.py | 1 | ||||
| -rw-r--r-- | miasm2/ir/translators/smt2.py | 9 | ||||
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 2 |
5 files changed, 9 insertions, 24 deletions
diff --git a/miasm2/arch/x86/sem.py b/miasm2/arch/x86/sem.py index cd456f7b..cc227819 100644 --- a/miasm2/arch/x86/sem.py +++ b/miasm2/arch/x86/sem.py @@ -597,22 +597,6 @@ def shrd(ir, instr, a, b, c): return _shift_tpl(">>>", ir, instr, a, b, c, "<<<") -def sal(ir, instr, a, b): - e = [] - shifter = get_shift(a, b) - c = m2_expr.ExprOp('a<<', a, shifter) - new_cf = (a >> (m2_expr.ExprInt_from(a, a.size) - shifter))[:1] - e.append(m2_expr.ExprAff(cf, m2_expr.ExprCond(shifter, - new_cf, - cf) - ) - ) - e += update_flag_znp(c) - e.append(m2_expr.ExprAff(of, c.msb() ^ new_cf)) - e.append(m2_expr.ExprAff(a, c)) - return e, [] - - def shl(ir, instr, a, b): return _shift_tpl("<<", ir, instr, a, b, left=True) @@ -3623,7 +3607,7 @@ def ps_rl_ll(ir, instr, a, b, op, size): e_do = [] slices = [] for i in xrange(0, a.size, size): - slices.append((m2_expr.ExprOp(op,a[i:i + size], count[:size]), + slices.append((m2_expr.ExprOp(op, a[i:i + size], count[:size]), i, i + size)) e.append(m2_expr.ExprAff(a[0:a.size], m2_expr.ExprCompose(slices))) e_do.append(m2_expr.ExprAff(ir.IRDst, lbl_next)) @@ -3995,7 +3979,7 @@ mnemo_func = {'mov': mov, 'rcr': rcr, 'sar': sar, 'shr': shr, - 'sal': sal, + 'sal': shl, 'shl': shl, 'shld': shld, 'cmc': cmc, diff --git a/miasm2/ir/translators/C.py b/miasm2/ir/translators/C.py index a7ba1a20..2c44d9e1 100644 --- a/miasm2/ir/translators/C.py +++ b/miasm2/ir/translators/C.py @@ -13,7 +13,6 @@ class TranslatorC(Translator): dct_shift = {'a>>': "right_arith", '>>': "right_logic", '<<': "left_logic", - 'a<<': "left_logic", } dct_rot = {'<<<': 'rot_left', '>>>': 'rot_right', diff --git a/miasm2/ir/translators/__init__.py b/miasm2/ir/translators/__init__.py index 22e00d98..d3678ffc 100644 --- a/miasm2/ir/translators/__init__.py +++ b/miasm2/ir/translators/__init__.py @@ -3,6 +3,7 @@ from miasm2.ir.translators.translator import Translator import miasm2.ir.translators.C import miasm2.ir.translators.python import miasm2.ir.translators.miasm +import miasm2.ir.translators.smt2 try: import miasm2.ir.translators.z3_ir except ImportError: diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py index e832d3b8..5bffd7f2 100644 --- a/miasm2/ir/translators/smt2.py +++ b/miasm2/ir/translators/smt2.py @@ -220,8 +220,6 @@ class TranslatorSMT2(Translator): res = bvshl(res, arg) elif expr.op == ">>": res = bvlshr(res, arg) - elif expr.op == "a<<": - res = bvshl(res, arg) elif expr.op == "a>>": res = bvashr(res, arg) elif expr.op == "<<<": @@ -286,13 +284,14 @@ class TranslatorSMT2(Translator): dst = self.from_expr(expr.dst) return smt2_assert(smt2_eq(src, dst)) - def to_smt2(self, exprs, logic="QF_ABV"): + def to_smt2(self, exprs, logic="QF_ABV", model=False): """ Converts a valid SMT2 file for a given list of SMT2 expressions. :param exprs: list of SMT2 expressions :param logic: SMT2 logic + :param model: model generation flag :return: String of the SMT2 file """ ret = "" @@ -315,6 +314,10 @@ class TranslatorSMT2(Translator): # define action ret += "(check-sat)\n" + # enable model generation + if model: + ret += "(get-model)\n" + return ret diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index a1b90ae8..79099520 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -165,8 +165,6 @@ class TranslatorZ3(Translator): res = z3.LShR(res, arg) elif expr.op == "a>>": res = res >> arg - elif expr.op == "a<<": - res = res << arg elif expr.op == "<<<": res = z3.RotateLeft(res, arg) elif expr.op == ">>>": |