Symbexec: Use simplifier with high level in symbexec

6 files changed, 32 insertions, 17 deletions

diff --git a/miasm2/analysis/depgraph.py b/miasm2/analysis/depgraph.py
index a5f3f0fd..46a83d2d 100644
--- a/miasm2/analysis/depgraph.py
+++ b/miasm2/analysis/depgraph.py
@@ -3,7 +3,7 @@
 from miasm2.expression.expression import ExprInt, ExprLoc, ExprAff
 from miasm2.core.graph import DiGraph
 from miasm2.core.locationdb import LocationDB
-from miasm2.expression.simplifications import expr_simp
+from miasm2.expression.simplifications import expr_simp_explicit
 from miasm2.ir.symbexec import SymbolicExecutionEngine
 from miasm2.ir.ir import IRBlock, AssignBlock
 from miasm2.ir.translators import Translator
@@ -456,7 +456,7 @@ class DependencyGraph(object):
         @implicit: (optional) Track IRDst for each block in the resulting path
 
         Following arguments define filters used to generate dependencies
-        @apply_simp: (optional) Apply expr_simp
+        @apply_simp: (optional) Apply expr_simp_explicit
         @follow_mem: (optional) Track memory syntactically
         @follow_call: (optional) Track through "call"
         """
@@ -480,7 +480,7 @@ class DependencyGraph(object):
         """
         follow = set()
         for expr in exprs:
-            follow.add(expr_simp(expr))
+            follow.add(expr_simp_explicit(expr))
         return follow, set()
 
     @staticmethod
diff --git a/miasm2/arch/arm/jit.py b/miasm2/arch/arm/jit.py
index 267bcea6..716a8826 100644
--- a/miasm2/arch/arm/jit.py
+++ b/miasm2/arch/arm/jit.py
@@ -8,6 +8,7 @@ from miasm2.jitter.codegen import CGen
 from miasm2.expression.expression import ExprId, ExprAff, ExprCond
 from miasm2.ir.ir import IRBlock, AssignBlock
 from miasm2.ir.translators.C import TranslatorC
+from miasm2.expression.simplifications import expr_simp_high_to_explicit
 
 log = logging.getLogger('jit_arm')
 hnd = logging.StreamHandler()
@@ -45,6 +46,15 @@ class arm_CGen(CGen):
             irblock_head = self.assignblk_to_irbloc(instr, assignblk_head)
             irblocks = [irblock_head] + assignblks_extra
 
+
+            # Simplify high level operators
+            out = []
+            for irblock in irblocks:
+                new_irblock = irblock.simplify(expr_simp_high_to_explicit)[1]
+                out.append(new_irblock)
+            irblocks = out
+
+
             for irblock in irblocks:
                 assert irblock.dst is not None
             irblocks_list.append(irblocks)
diff --git a/miasm2/ir/symbexec.py b/miasm2/ir/symbexec.py
index 9ab455da..1a077de5 100644
--- a/miasm2/ir/symbexec.py
+++ b/miasm2/ir/symbexec.py
@@ -4,7 +4,7 @@ from collections import MutableMapping
 
 from miasm2.expression.expression import ExprOp, ExprId, ExprLoc, ExprInt, \
     ExprMem, ExprCompose, ExprSlice, ExprCond
-from miasm2.expression.simplifications import expr_simp
+from miasm2.expression.simplifications import expr_simp_explicit
 from miasm2.ir.ir import AssignBlock
 
 log = logging.getLogger("symbexec")
@@ -138,7 +138,7 @@ class MemArray(MutableMapping):
 
     """
 
-    def __init__(self, base, expr_simp=expr_simp):
+    def __init__(self, base, expr_simp=expr_simp_explicit):
         self._base = base
         self.expr_simp = expr_simp
         self._mask = int(base.mask)
@@ -461,7 +461,7 @@ class MemSparse(object):
 
     """
 
-    def __init__(self, addrsize, expr_simp=expr_simp):
+    def __init__(self, addrsize, expr_simp=expr_simp_explicit):
         """
         @addrsize: size (in bits) of the addresses manipulated by the MemSparse
         @expr_simp: an ExpressionSimplifier instance
@@ -604,7 +604,7 @@ class MemSparse(object):
 class SymbolMngr(object):
     """Symbolic store manager (IDs and MEMs)"""
 
-    def __init__(self, init=None, addrsize=None, expr_simp=expr_simp):
+    def __init__(self, init=None, addrsize=None, expr_simp=expr_simp_explicit):
         assert addrsize is not None
         if init is None:
             init = {}
@@ -807,7 +807,7 @@ class SymbolicExecutionEngine(object):
     def __init__(self, ir_arch, state=None,
                  func_read=None,
                  func_write=None,
-                 sb_expr_simp=expr_simp):
+                 sb_expr_simp=expr_simp_explicit):
 
         self.expr_to_visitor = {
             ExprInt: self.eval_exprint,
@@ -823,7 +823,7 @@ class SymbolicExecutionEngine(object):
         if state is None:
             state = {}
 
-        self.symbols = SymbolMngr(addrsize=ir_arch.addrsize, expr_simp=expr_simp)
+        self.symbols = SymbolMngr(addrsize=ir_arch.addrsize, expr_simp=sb_expr_simp)
 
         for dst, src in state.iteritems():
             self.symbols.write(dst, src)
@@ -1270,9 +1270,9 @@ class symbexec(SymbolicExecutionEngine):
     def __init__(self, ir_arch, known_symbols,
                  func_read=None,
                  func_write=None,
-                 sb_expr_simp=expr_simp):
+                 sb_expr_simp=expr_simp_explicit):
         warnings.warn("Deprecated API: use SymbolicExecutionEngine")
         super(symbexec, self).__init__(ir_arch, known_symbols,
                                        func_read,
                                        func_write,
-                                       sb_expr_simp=expr_simp)
+                                       sb_expr_simp=sb_expr_simp)
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index 887c68d0..1b0578b7 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -229,6 +229,12 @@ class TranslatorZ3(Translator):
                 index = - i % size
                 out = size - (index + 1)
                 res = z3.If((src & (1 << index)) != 0, out, res)
+        elif expr.op.startswith("zeroExt"):
+            arg, = expr.args
+            res = z3.ZeroExt(expr.size - arg.size, self.from_expr(arg))
+        elif expr.op.startswith("signExt"):
+            arg, = expr.args
+            res = z3.SignExt(expr.size - arg.size, self.from_expr(arg))
         else:
             raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
 
diff --git a/miasm2/jitter/codegen.py b/miasm2/jitter/codegen.py
index fec10f41..69e83de5 100644
--- a/miasm2/jitter/codegen.py
+++ b/miasm2/jitter/codegen.py
@@ -8,7 +8,7 @@ from miasm2.ir.ir import IRBlock, AssignBlock
 
 from miasm2.ir.translators.C import TranslatorC, int_size_to_bn
 from miasm2.core.asmblock import AsmBlockBad
-from miasm2.expression.simplifications_high_level import expr_simp
+from miasm2.expression.simplifications import expr_simp_high_to_explicit
 
 TRANSLATOR_NO_SYMBOL = TranslatorC(loc_db=None)
 
@@ -170,7 +170,7 @@ class CGen(object):
             # Simplify high level operators
             out = []
             for irblock in irblocks:
-                new_irblock = irblock.simplify(expr_simp)[1]
+                new_irblock = irblock.simplify(expr_simp_high_to_explicit)[1]
                 out.append(new_irblock)
             irblocks = out
 
diff --git a/miasm2/jitter/jitcore_python.py b/miasm2/jitter/jitcore_python.py
index 61bd98d0..b97727cd 100644
--- a/miasm2/jitter/jitcore_python.py
+++ b/miasm2/jitter/jitcore_python.py
@@ -1,7 +1,7 @@
 import miasm2.jitter.jitcore as jitcore
 import miasm2.expression.expression as m2_expr
 import miasm2.jitter.csts as csts
-from miasm2.expression.simplifications import ExpressionSimplifier
+from miasm2.expression.simplifications import ExpressionSimplifier, expr_simp_explicit
 from miasm2.jitter.emulatedsymbexec import EmulatedSymbExec
 
 ################################################################################
@@ -20,12 +20,11 @@ class JitCore_Python(jitcore.JitCore):
         self.ircfg = self.ir_arch.new_ircfg()
 
         # CPU & VM (None for now) will be set later
-        expr_simp = ExpressionSimplifier()
-        expr_simp.enable_passes(ExpressionSimplifier.PASS_COMMONS)
+
         self.symbexec = self.SymbExecClass(
             None, None,
             self.ir_arch, {},
-            sb_expr_simp=expr_simp
+            sb_expr_simp=expr_simp_explicit
         )
         self.symbexec.enable_emulated_simplifications()