def inject_info(self, info):
     new_symbols = symbols()
     for expr, value in self.items():
         expr = expr_simp(expr.replace_expr(info))
         value = expr_simp(value.replace_expr(info))
         new_symbols[expr] = value
     return new_symbols

    def codepath_walk(addr, symbols, conds, depth):
        if depth >= cond_limit:
            return None

        for _ in range(uncond_limit):
            sb = symbexec(ir, symbols)
            pc = sb.emul_ir_blocs(ir, addr)
            if is_goal(sb.symbols) == True:
                return conds

            if isinstance(pc, ExprCond):
                cond_true  = {pc.cond: ExprInt_from(pc.cond, 1)}
                cond_false = {pc.cond: ExprInt_from(pc.cond, 0)}
                addr_true  = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_true), {}))
                addr_false = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_false), {}))
                conds_true = list(conds) + cond_true.items()
                conds_false = list(conds) + cond_false.items()
                rslt = codepath_walk(
                    addr_true, sb.symbols.copy(), conds_true, depth + 1)
                if rslt != None:
                    return rslt
                rslt = codepath_walk(
                    addr_false, sb.symbols.copy(), conds_false, depth + 1)
                if rslt != None:
                    return rslt
                break
            else:
                break
        return None

 def inject_info(self, info):
     s = symbols()
     for k, v in self.items():
         k = expr_simp(k.replace_expr(info))
         v = expr_simp(v.replace_expr(info))
         s[k] = v
     return s

 def del_mem_above_stack(self, sp):
     sp_val = self.symbols[sp]
     for mem_ad, (mem, _) in self.symbols.symbols_mem.items():
         # print mem_ad, sp_val
         diff = self.eval_expr(mem_ad - sp_val, {})
         diff = expr_simp(diff)
         if not isinstance(diff, ExprInt):
             continue
         m = expr_simp(diff.msb())
         if m.arg == 1:
             del(self.symbols[mem])

def check_expr_below_stack(ir_arch_a, expr):
    """
    Return False if expr pointer is below original stack pointer
    @ir_arch_a: ira instance
    @expr: Expression instance
    """
    ptr = expr.ptr
    diff = expr_simp(ptr - ir_arch_a.sp)
    if not diff.is_int():
        return True
    if int(diff) == 0 or int(expr_simp(diff.msb())) == 0:
        return False
    return True

def retrieve_stack_accesses(ir_arch_a, ssa):
    """
    Walk the ssa graph and find stack based variables.
    Return a dictionnary linking stack base address to its size/name
    @ir_arch_a: ira instance
    @ssa: SSADiGraph instance
    """
    stack_vars = set()
    for block in ssa.graph.blocks.itervalues():
        for assignblk in block:
            for dst, src in assignblk.iteritems():
                stack_vars.update(get_stack_accesses(ir_arch_a, dst))
                stack_vars.update(get_stack_accesses(ir_arch_a, src))
    stack_vars = filter(lambda expr: check_expr_below_stack(ir_arch_a, expr), stack_vars)

    base_to_var = {}
    for var in stack_vars:
        base_to_var.setdefault(var.ptr, set()).add(var)


    base_to_interval = {}
    for addr, vars in base_to_var.iteritems():
        var_interval = interval()
        for var in vars:
            offset = expr_simp(addr - ir_arch_a.sp)
            if not offset.is_int():
                # skip non linear stack offset
                continue

            start = int(offset)
            stop = int(expr_simp(offset + ExprInt(var.size / 8, offset.size)))
            mem = interval([(start, stop-1)])
            var_interval += mem
        base_to_interval[addr] = var_interval
    if not base_to_interval:
        return {}
    # Check if not intervals overlap
    _, tmp = base_to_interval.popitem()
    while base_to_interval:
        addr, mem = base_to_interval.popitem()
        assert (tmp & mem).empty
        tmp += mem

    base_to_info = {}
    for addr, vars in base_to_var.iteritems():
        name = "var_%d" % (len(base_to_info))
        size = max([var.size for var in vars])
        base_to_info[addr] = size, name
    return base_to_info

 def resolve_args_with_symbols(self, symbols=None):
     if symbols is None:
         symbols = {}
     args_out = []
     for a in self.args:
         e = a
         # try to resolve symbols using symbols (0 for default value)
         ids = m2_expr.get_expr_ids(e)
         fixed_ids = {}
         for x in ids:
             if isinstance(x.name, asmbloc.asm_label):
                 name = x.name.name
                 # special symbol $
                 if name == "$":
                     fixed_ids[x] = self.get_asm_offset(x)
                     continue
                 if not name in symbols:
                     raise ValueError("unresolved symbol! %r" % x)
             else:
                 name = x.name
             if not name in symbols:
                 continue
             if symbols[name].offset is None:
                 raise ValueError('The offset of label "%s" cannot be ' "determined" % name)
             else:
                 size = x.size
                 if size is None:
                     default_size = self.get_symbol_size(x, symbols)
                     size = default_size
                 value = m2_expr.ExprInt(symbols[name].offset, size)
             fixed_ids[x] = value
         e = e.replace_expr(fixed_ids)
         e = expr_simp(e)
         args_out.append(e)
     return args_out

def emul_symb(ir_arch, ircfg, mdis, states_todo, states_done):
    while states_todo:
        addr, symbols, conds = states_todo.pop()
        print '*' * 40, "addr", addr, '*' * 40
        if (addr, symbols, conds) in states_done:
            print 'Known state, skipping', addr
            continue
        states_done.add((addr, symbols, conds))
        symbexec = SymbolicExecutionEngine(ir_arch)
        symbexec.symbols = symbols.copy()
        if ir_arch.pc in symbexec.symbols:
            del symbexec.symbols[ir_arch.pc]
        irblock = get_block(ir_arch, ircfg, mdis, addr)

        print 'Run block:'
        print irblock
        addr = symbexec.eval_updt_irblock(irblock)
        print 'Final state:'
        symbexec.dump(mems=False)

        assert addr is not None
        if isinstance(addr, ExprCond):
            # Create 2 states, each including complementary conditions
            cond_group_a = {addr.cond: ExprInt(0, addr.cond.size)}
            cond_group_b = {addr.cond: ExprInt(1, addr.cond.size)}
            addr_a = expr_simp(symbexec.eval_expr(addr.replace_expr(cond_group_a), {}))
            addr_b = expr_simp(symbexec.eval_expr(addr.replace_expr(cond_group_b), {}))
            if not (addr_a.is_int() or addr_a.is_loc() and
                    addr_b.is_int() or addr_b.is_loc()):
                print str(addr_a), str(addr_b)
                raise ValueError("Unsupported condition")
            if isinstance(addr_a, ExprInt):
                addr_a = int(addr_a.arg)
            if isinstance(addr_b, ExprInt):
                addr_b = int(addr_b.arg)
            states_todo.add((addr_a, symbexec.symbols.copy(), tuple(list(conds) + cond_group_a.items())))
            states_todo.add((addr_b, symbexec.symbols.copy(), tuple(list(conds) + cond_group_b.items())))
        elif addr == ret_addr:
            print 'Return address reached'
            continue
        elif addr.is_int():
            addr = int(addr.arg)
            states_todo.add((addr, symbexec.symbols.copy(), tuple(conds)))
        elif addr.is_loc():
            states_todo.add((addr, symbexec.symbols.copy(), tuple(conds)))
        else:
            raise ValueError("Unsupported destination")

def is_stack_access(ir_arch_a, expr):
    if not expr.is_mem():
        return False
    ptr = expr.ptr
    diff = expr_simp(ptr - ir_arch_a.sp)
    if not diff.is_int():
        return False
    return expr

 def _follow_simp_expr(exprs):
     """Simplify expression so avoid tracking useless elements,
     as: XOR EAX, EAX
     """
     follow = set()
     for expr in exprs:
         follow.add(expr_simp(expr))
     return follow, set()

def fix_expr_val(e, symbols):
    def expr_calc(e):
        if isinstance(e, m2_expr.ExprId):
            s = symbols.s[e.name]
            e = m2_expr.ExprInt_from(e, s.offset)
        return e
    e = e.visit(expr_calc)
    e = expr_simp(e)
    return e

def arm_guess_jump_table(
    mnemo, attrib, pool_bin, cur_bloc, offsets_to_dis, symbol_pool):
    ira = get_ira(mnemo, attrib)

    jra = ExprId('jra')
    jrb = ExprId('jrb')

    sp = AsmSymbolPool()
    ir_arch = ira(sp)
    ir_arch.add_bloc(cur_bloc)

    ir_blocks = ir_arch.blocks.values()
    for irblock in ir_blocks:
        # print 'X'*40
        # print irblock
        pc_val = None
        # lr_val = None
        for exprs in irblock.irs:
            for e in exprs:
                if e.dst == ir_arch.pc:
                    pc_val = e.src
                # if e.dst == mnemo.regs.LR:
                #    lr_val = e.src
        if pc_val is None:
            continue
        if not isinstance(pc_val, ExprMem):
            continue
        assert(pc_val.size == 32)
        print pc_val
        ad = pc_val.arg
        ad = expr_simp(ad)
        print ad
        res = match_expr(ad, jra + jrb, set([jra, jrb]))
        if res is False:
            raise NotImplementedError('not fully functional')
        print res
        if not isinstance(res[jrb], ExprInt):
            raise NotImplementedError('not fully functional')
        base_ad = int(res[jrb])
        print base_ad
        addrs = set()
        i = -1
        max_table_entry = 10000
        max_diff_addr = 0x100000  # heuristic
        while i < max_table_entry:
            i += 1
            try:
                ad = upck32(pool_bin.getbytes(base_ad + 4 * i, 4))
            except:
                break
            if abs(ad - base_ad) > max_diff_addr:
                break
            addrs.add(ad)
        print [hex(x) for x in addrs]

def fix_expr_val(expr, symbols):
    """Resolve an expression @expr using @symbols"""
    def expr_calc(e):
        if isinstance(e, m2_expr.ExprId):
            s = symbols._name2label[e.name]
            e = m2_expr.ExprInt_from(e, s.offset)
        return e
    result = expr.visit(expr_calc)
    result = expr_simp(result)
    if not isinstance(result, m2_expr.ExprInt):
        raise RuntimeError('Cannot resolve symbol %s' % expr)
    return result

 def field_addr(self, base, Clike, is_ptr=False):
     key = (base, Clike, is_ptr)
     ret = self.cache_field_addr.get(key, None)
     if ret is None:
         base_expr = self.trad(base)
         if is_ptr:
             access_expr = self.trad(Clike)
         else:
             access_expr = self.trad("&(%s)" % Clike)
         offset = int(expr_simp(access_expr - base_expr))
         ret = offset
         self.cache_field_addr[key] = ret
     return ret

 def propag_expr_cst(self, expr):
     """Propagate constant expressions in @expr
     @expr: Expression to update"""
     elements = expr.get_r(mem_read=True)
     to_propag = {}
     for element in elements:
         # Only ExprId can be safely propagated
         if not element.is_id():
             continue
         value = self.eval_expr(element)
         if self.is_expr_cst(self.ir_arch, value):
             to_propag[element] = value
     return expr_simp(expr.replace_expr(to_propag))

    def elements(self):
        value = self.cbReg.value
        if value in self.stk_args:
            line = self.ircfg.blocks[self.loc_key][self.line_nb].instr
            arg_num = self.stk_args[value]
            stk_high = m2_expr.ExprInt(idc.GetSpd(line.offset), ir_arch.sp.size)
            stk_off = m2_expr.ExprInt(self.ira.sp.size/8 * arg_num, ir_arch.sp.size)
            element =  m2_expr.ExprMem(mn.regs.regs_init[ir_arch.sp] + stk_high + stk_off, self.ira.sp.size)
            element = expr_simp(element)
            # Force stack unaliasing
            self.stk_unalias_force = True
        elif value:
            element = self.ira.arch.regs.all_regs_ids_byname.get(value, None)

        else:
            raise ValueError("Unknown element '%s'!" % value)
        return set([element])

    def resolve_args_with_symbols(self, symbols=None):
        if symbols is None:
            symbols = LocationDB()
        args_out = []
        for expr in self.args:
            # try to resolve symbols using symbols (0 for default value)
            loc_keys = m2_expr.get_expr_locs(expr)
            fixed_expr = {}
            for exprloc in loc_keys:
                loc_key = exprloc.loc_key
                names = symbols.get_location_names(loc_key)
                # special symbols
                if '$' in names:
                    fixed_expr[exprloc] = self.get_asm_offset(exprloc)
                    continue
                if '_' in names:
                    fixed_expr[exprloc] = self.get_asm_next_offset(exprloc)
                    continue
                arg_int = symbols.get_location_offset(loc_key)
                if arg_int is not None:
                    fixed_expr[exprloc] = m2_expr.ExprInt(arg_int, exprloc.size)
                    continue
                if not names:
                    raise ValueError('Unresolved symbol: %r' % exprloc)

                offset = symbols.get_location_offset(loc_key)
                if offset is None:
                    raise ValueError(
                        'The offset of loc_key "%s" cannot be determined' % names
                    )
                else:
                    # Fix symbol with its offset
                    size = exprloc.size
                    if size is None:
                        default_size = self.get_symbol_size(exprloc, symbols)
                        size = default_size
                    value = m2_expr.ExprInt(offset, size)
                fixed_expr[exprloc] = value

            expr = expr.replace_expr(fixed_expr)
            expr = expr_simp(expr)
            args_out.append(expr)
        return args_out

    def eval_updt_irblock(self, irb, step=False):
        """
        Symbolic execution of the @irb on the current state
        @irb: irblock instance
        @step: display intermediate steps
        """

        offset2cmt = {}
        for index, assignblk in enumerate(irb):
            if set(assignblk) == set([self.ir_arch.IRDst, self.ir_arch.pc]):
                # Don't display on jxx
                continue
            instr = assignblk.instr
            tmp_r = assignblk.get_r()
            tmp_w = assignblk.get_w()

            todo = set()

            # Replace PC with value to match IR args
            pc_fixed = {self.ir_arch.pc: m2_expr.ExprInt(instr.offset + instr.l, self.ir_arch.pc.size)}
            inputs = tmp_r
            inputs.update(arg for arg in tmp_w if arg.is_mem())
            for arg in inputs:
                arg = expr_simp(arg.replace_expr(pc_fixed))
                if arg in tmp_w and not arg.is_mem():
                    continue
                todo.add(arg)

            for expr in todo:
                if expr.is_int():
                    continue
                for c_str, c_type in self.chandler.expr_to_c_and_types(expr, self.symbols):
                    expr = self.cst_propag_link.get((irb.loc_key, index), {}).get(expr, expr)
                    offset2cmt.setdefault(instr.offset, set()).add(
                        "\n%s: %s\n%s" % (expr, c_str, c_type))

            self.eval_updt_assignblk(assignblk)
        for offset, value in offset2cmt.iteritems():
            idc.MakeComm(offset, '\n'.join(value))
            print "%x\n" % offset, '\n'.join(value)

        return self.eval_expr(self.ir_arch.IRDst)

    def func_write(self, symb_exec, dest, data):
        """Memory read wrapper for symbolic execution
        @symb_exec: symbexec instance
        @dest: ExprMem instance
        @data: Expr instance"""

        # Get the content to write
        data = expr_simp(data)
        if not isinstance(data, m2_expr.ExprInt):
            raise NotImplementedError("A simplification is missing: %s" % data)
        to_write = data.arg.arg

        # Format information
        addr = dest.arg.arg.arg
        size = data.size / 8
        content = hex(to_write).replace("0x", "").replace("L", "")
        content = "0" * (size * 2 - len(content)) + content
        content = content.decode("hex")[::-1]

        # Write in VmMngr context
        self.cpu.set_mem(addr, content)

 def resolve_args_with_symbols(self, symbols=None):
     if symbols is None:
         symbols = {}
     args_out = []
     for a in self.args:
         e = a
         # try to resolve symbols using symbols (0 for default value)
         ids = m2_expr.get_expr_ids(e)
         fixed_ids = {}
         for x in ids:
             if isinstance(x.name, asmbloc.asm_label):
                 name = x.name.name
                 if not name in symbols:
                     raise ValueError('unresolved symbol! %r' % x)
             else:
                 name = x.name
             # special symbol
             if name == '$':
                 fixed_ids[x] = self.get_asm_offset(x)
                 continue
             if not name in symbols:
                 continue
             if symbols[name].offset is None:
                 default_size = self.get_symbol_size(x, symbols)
                 # default value
                 value = m2_expr.ExprInt_fromsize(default_size, 0)
             else:
                 size = x.size
                 if size is None:
                     default_size = self.get_symbol_size(x, symbols)
                     size = default_size
                 value = m2_expr.ExprInt_fromsize(size, symbols[name].offset)
             fixed_ids[x] = value
         e = e.replace_expr(fixed_ids)
         e = expr_simp(e)
         args_out.append(e)
     return args_out