logic.py

#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#

# mypy: ignore-errors

import syntax
from syntax import word64T, word32T, word8T, boolT, builtinTs, Expr, Node
from syntax import true_term, false_term, mk_num
from syntax import foldr1

from syntax import (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
                    mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word64, mk_word32, mk_word8,
                    mk_word32_maybe, mk_memacc, mk_memupd, mk_arr_index, mk_arroffs,
                    mk_if, mk_meta_typ, mk_pvalid)

from syntax import structs
from target_objects import trace, printout
from typing import List


def is_int(n):
    return hasattr(n, '__int__')


def mk_eq_with_cast(a, c):
    return mk_eq(a, syntax.arch.mk_cast(c, a.typ))


def mk_rodata(m):
    assert m.typ == builtinTs['Mem']
    return Expr('Op', boolT, name='ROData', vals=[m])


def split_scalar_globals(vs):
    for i in range(len(vs)):
        if vs[i].typ.kind != 'Word' and vs[i].typ != boolT:
            break
    else:
        i = len(vs)
    scalars = vs[:i]
    global_vars = vs[i:]

    for v in global_vars:
        if v.typ not in [builtinTs['Mem'], builtinTs['Dom'],
                         builtinTs['HTD'], builtinTs['PMS'],
                         syntax.arch.ghost_assertion_type]:
            assert not "scalar_global split expected", vs

    memT = builtinTs['Mem']
    mems = [v for v in global_vars if v.typ == memT]
    others = [v for v in global_vars if v.typ != memT]
    return (scalars, mems, others)


def mk_vars(tups):
    return [mk_var(nm, typ) for (nm, typ) in tups]


def split_scalar_pairs(var_pairs):
    return split_scalar_globals(mk_vars(var_pairs))


def azip(xs, ys):
    assert len(xs) == len(ys), (xs, ys)
    return list(zip(xs, ys))


def mk_mem_eqs(a_imem, c_imem, a_omem, c_omem, tags):
    [a_imem] = a_imem
    a_tag, c_tag = tags
    (c_in, c_out) = (c_tag + '_IN', c_tag + '_OUT')
    (a_in, a_out) = (a_tag + '_IN', a_tag + '_OUT')
    if c_imem:
        [c_imem] = c_imem
        ieqs = [((a_imem, a_in), (c_imem, c_in)),
                ((mk_rodata(c_imem), c_in), (true_term, c_in))]
    else:
        ieqs = [((mk_rodata(a_imem), a_in), (true_term, c_in))]
    if c_omem:
        [a_m] = a_omem
        [c_omem] = c_omem
        oeqs = [((a_m, a_out), (c_omem, c_out)),
                ((mk_rodata(c_omem), c_out), (true_term, c_out))]
    else:
        oeqs = [((a_m, a_out), (a_imem, a_in)) for a_m in a_omem]

    return (ieqs, oeqs)


def mk_var_list(vs, typ):
    return [syntax.mk_var(v, typ) for v in vs]


def mk_offs_sequence(init, offs, n, do_reverse=False):
    r = list(range(n))
    if do_reverse:
        r.reverse()

    def mk_offs(n):
        return Expr('Num', init.typ, val=offs * n)
    return [mk_plus(init, mk_offs(m)) for m in r]


def mk_stack_sequence(sp, offs, stack, typ, n, do_reverse=False):
    return [(mk_memacc(stack, addr, typ), addr)
            for addr in mk_offs_sequence(sp, offs, n, do_reverse)]


def mk_aligned(w, n):
    assert w.typ.kind == 'Word'
    mask = Expr('Num', w.typ, val=((1 << n) - 1))
    return mk_eq(mk_bwand(w, mask), mk_num(0, w.typ))


def mk_eqs(var_c_args, var_c_rets, c_imem, c_omem, min_stack_size):
    arg_regs = mk_var_list(
        syntax.arch.argument_registers, syntax.arch.word_type)
    ar0 = arg_regs[0]

    sp = mk_var(syntax.arch.sp_register, syntax.arch.word_type)
    st = mk_var('stack', builtinTs['Mem'])
    ra_input = mk_var('ret_addr_input', syntax.arch.word_type)
    sregs = mk_stack_sequence(sp, syntax.arch.ptr_size,
                              st, syntax.arch.word_type, len(var_c_args) + 1)
    ret = mk_var('ret', syntax.arch.word_type)

    preconds = [
        mk_aligned(sp, syntax.arch.stack_alignment_bits),
        mk_eq(ret, mk_var(syntax.arch.ra_register, syntax.arch.word_type)),
        mk_aligned(ret, syntax.arch.ret_addr_alignment_bits),
        mk_eq(ra_input, ar0),
        mk_less_eq(min_stack_size, sp)
    ]

    post_eqs = [
        (x, x) for x in mk_var_list(
            syntax.arch.callee_saved_registers,
            syntax.arch.word_type)
    ]

    arg_seq = [(r, None) for r in arg_regs] + sregs

    if len(var_c_rets) > len(syntax.arch.return_registers):
        # Our return value exceeds the capacity of the return
        # registers. In this case, the caller will pass us a
        # memory address where we can save our return value
        # as an implicit first argument (passed in the first
        # argument register).
        arg_seq.pop(0)
        preconds += [
            mk_aligned(ar0, syntax.arch.ptr_alignment_bits),
            mk_less_eq(sp, ar0)
        ]
        save_seq = mk_stack_sequence(
            ra_input, syntax.arch.ptr_size, st,
            syntax.arch.word_type, len(var_c_rets)
        )
        save_addrs = [addr for (_, addr) in save_seq]
        post_eqs += [(ra_input, ra_input)]
        out_eqs = list(zip(var_c_rets, [x for (x, _) in save_seq]))
        out_eqs = [(c, syntax.arch.mk_cast(a, c.typ)) for (c, a) in out_eqs]
        init_save_seq = mk_stack_sequence(
            ar0, syntax.arch.ptr_size, st,
            syntax.arch.word_type, len(var_c_rets)
        )
        (_, last_arg_addr) = arg_seq[len(var_c_args) - 1]
        preconds += [mk_less_eq(sp, addr)
                     for (_, addr) in init_save_seq[-1:]]
        if last_arg_addr:
            preconds += [mk_less(last_arg_addr, addr)
                         for (_, addr) in init_save_seq[:1]]
    else:
        out_eqs = list(
            zip(var_c_rets, arg_regs[:len(syntax.arch.argument_registers)]))
        save_addrs = []

    arg_seq_addrs = [addr for ((_, addr), _) in zip(arg_seq, var_c_args)
                     if addr != None]
    swrap = mk_stack_wrapper(sp, st, arg_seq_addrs)
    swrap2 = mk_stack_wrapper(sp, st, save_addrs)

    post_eqs += [(swrap, swrap2)]

    mem = mk_var('mem', builtinTs['Mem'])
    (mem_ieqs, mem_oeqs) = mk_mem_eqs([mem], c_imem, [mem], c_omem,
                                      ['ASM', 'C'])

    addr = None
    arg_eqs = [syntax.arch.cast_pair(((a_x, 'ASM_IN'), (c_x, 'C_IN')))
               for (c_x, (a_x, addr)) in zip(var_c_args, arg_seq)]

    if addr:
        preconds += [mk_less_eq(sp, addr)]

    ret_eqs = [syntax.arch.cast_pair(((a_x, 'ASM_OUT'), (c_x, 'C_OUT')))
               for (c_x, a_x) in out_eqs]

    preconds = [((a_x, 'ASM_IN'), (true_term, 'ASM_IN')) for a_x in preconds]
    asm_invs = [((vin, 'ASM_IN'), (vout, 'ASM_OUT'))
                for (vin, vout) in post_eqs]

    return (arg_eqs + mem_ieqs + preconds, ret_eqs + mem_oeqs + asm_invs)


class Pairing:
    def __init__(self, tags, funs, eqs, notes=None):
        [l_tag, r_tag] = tags
        self.tags = tags
        assert set(funs) == set(tags)
        self.funs = funs
        self.eqs = eqs

        self.l_f = funs[l_tag]
        self.r_f = funs[r_tag]
        self.name = 'Pairing (%s (%s) <= %s (%s))' % (self.l_f,
                                                      l_tag, self.r_f, r_tag)

        self.notes = {}
        if notes != None:
            self.notes.update(notes)

    def __str__(self):
        return self.name

    def __hash__(self):
        return hash(self.name)

    def __eq__(self, other):
        return self.name == other.name and self.eqs == other.eqs

    def __ne__(self, other):
        return not other or not self == other


def inst_eqs_pattern(pattern, params):
    (pat_params, inp_eqs, out_eqs) = pattern
    substs = [((x.name, x.typ), y)
              for (pat_vs, vs) in azip(pat_params, params)
              for (x, y) in azip(pat_vs, vs)]
    substs = dict(substs)
    def subst(x): return var_subst(x, substs)
    return ([(subst(x), subst(y)) for (x, y) in inp_eqs],
            [(subst(x), subst(y)) for (x, y) in out_eqs])


def inst_eqs_pattern_tuples(pattern, params):
    return inst_eqs_pattern(pattern, list(map(mk_vars, params)))


def inst_eqs_pattern_exprs(pattern, params):
    (inp_eqs, out_eqs) = inst_eqs_pattern(pattern, params)
    return (foldr1(mk_and, [mk_eq(a, c) for (a, c) in inp_eqs]),
            foldr1(mk_and, [mk_eq(a, c) for (a, c) in out_eqs]))


def var_match(var_exp, conc_exp, assigns):
    if var_exp.typ != conc_exp.typ:
        return False
    if var_exp.kind == 'Var':
        key = (var_exp.name, var_exp.typ)
        if key in assigns:
            return conc_exp == assigns[key]
        else:
            assigns[key] = conc_exp
            return True
    elif var_exp.kind == 'Op':
        if conc_exp.kind != 'Op' or var_exp.name != conc_exp.name:
            return False
        return all([var_match(a, b, assigns)
                    for (a, b) in azip(var_exp.vals, conc_exp.vals)])
    else:
        return False


def var_subst(var_exp, assigns, must_subst=True):

    # hack for void func(void)
    must_subst = False

    def substor(var_exp):
        if var_exp.kind == 'Var':
            k = (var_exp.name, var_exp.typ)
            if must_subst or k in assigns:
                return assigns[k]
            else:
                return None
        else:
            return None
    return syntax.do_subst(var_exp, substor)


def recursive_term_subst(eqs, expr):
    if expr in eqs:
        return eqs[expr]
    if expr.kind == 'Op':
        vals = [recursive_term_subst(eqs, x) for x in expr.vals]
        return syntax.adjust_op_vals(expr, vals)
    return expr


def mk_accum_rewrites(typ):
    x = mk_var('x', typ)
    y = mk_var('y', typ)
    z = mk_var('z', typ)
    i = mk_var('i', typ)
    return [(x, i, mk_plus(x, y), mk_plus(x, mk_times(i, y)),
             y),
            (x, i, mk_plus(y, x), mk_plus(x, mk_times(i, y)),
             y),
            (x, i, mk_minus(x, y), mk_minus(x, mk_times(i, y)),
             mk_uminus(y)),
            (x, i, mk_plus(mk_plus(x, y), z),
             mk_plus(x, mk_times(i, mk_plus(y, z))),
             mk_plus(y, z)),
            (x, i, mk_plus(mk_plus(y, x), z),
             mk_plus(x, mk_times(i, mk_plus(y, z))),
             mk_plus(y, z)),
            (x, i, mk_plus(y, mk_plus(x, z)),
             mk_plus(x, mk_times(i, mk_plus(y, z))),
             mk_plus(y, z)),
            (x, i, mk_plus(y, mk_plus(z, x)),
             mk_plus(x, mk_times(i, mk_plus(y, z))),
             mk_plus(y, z)),
            (x, i, mk_minus(mk_minus(x, y), z),
             mk_minus(x, mk_times(i, mk_plus(y, z))),
             mk_plus(y, z)),
            ]


def mk_all_accum_rewrites():
    return [rew for typ in [word8T, word32T, syntax.word16T,
                            syntax.word64T]
            for rew in mk_accum_rewrites(typ)]


accum_rewrites = mk_all_accum_rewrites()


def default_val(typ):
    if typ.kind == 'Word':
        return Expr('Num', typ, val=0)
    elif typ == boolT:
        return false_term
    else:
        assert not 'default value for type %s created', typ


trace_accumulators = []


def accumulator_closed_form(expr, xxx_todo_changeme2, add_mask=None):
    (nm, typ) = xxx_todo_changeme2
    expr = toplevel_split_out_cast(expr)
    n = get_bwand_mask(expr)
    if n and not add_mask:
        return accumulator_closed_form(expr.vals[0], (nm, typ),
                                       add_mask=n)

    for (x, i, pattern, rewrite, offset) in accum_rewrites:
        var = mk_var(nm, typ)
        ass = {(x.name, x.typ): var}
        m = var_match(pattern, expr, ass)
        if m:
            x2_def = default_val(typ)
            i2_def = default_val(word32T)

            def do_rewrite(x2=x2_def, i2=i2_def):
                ass[(x.name, x.typ)] = x2
                ass[(i.name, i.typ)] = i2
                vs = var_subst(rewrite, ass)
                if add_mask:
                    vs = mk_bwand_mask(vs, add_mask)
                return vs
            offs = var_subst(offset, ass)
            return (do_rewrite, offs)
    if trace_accumulators:
        trace('no accumulator %s' % ((expr, nm, typ), ))
    return (None, None)


def split_out_cast(expr, target_typ, bits):
    """given a word-type expression expr (of any word length),
    compute a simplified expression expr' of the target type, which will
    have the property that expr' && mask bits = cast expr,
    where && is bitwise-and (BWAnd), mask n is the bitpattern set at the
    bottom n bits, e.g. (1 << n) - 1, and cast is WordCast."""
    if expr.is_op(['WordCast', 'WordCastSigned']):
        [x] = expr.vals
        if x.typ.num >= bits and expr.typ.num >= bits:
            return split_out_cast(x, target_typ, bits)
        else:
            return syntax.arch.mk_cast(expr, target_typ)
    elif expr.is_op('BWAnd'):
        [x, y] = expr.vals
        if y.kind == 'Num':
            val = y.val
        else:
            val = 0
        full_mask = (1 << bits) - 1
        if val & full_mask == full_mask:
            return split_out_cast(x, target_typ, bits)
        else:
            return syntax.arch.mk_cast(expr, target_typ)
    elif expr.is_op(['Plus', 'Minus']):
        # rounding issues will appear if this arithmetic is done
        # at a smaller number of bits than we'll eventually report
        if expr.typ.num >= bits:
            vals = [split_out_cast(x, target_typ, bits)
                    for x in expr.vals]
            if expr.is_op('Plus'):
                return mk_plus(vals[0], vals[1])
            else:
                return mk_minus(vals[0], vals[1])
        else:
            return syntax.arch.mk_cast(expr, target_typ)
    else:
        return syntax.arch.mk_cast(expr, target_typ)


def toplevel_split_out_cast(expr):
    bits = None
    if expr.is_op(['WordCast', 'WordCastSigned']):
        bits = min([expr.typ.num, expr.vals[0].typ.num])
    elif expr.is_op('BWAnd'):
        bits = get_bwand_mask(expr)

    if bits:
        expr = split_out_cast(expr, expr.typ, bits)
        return mk_bwand_mask(expr, bits)
    else:
        return expr


two_powers = {}


def get_bwand_mask(expr):
    """recognise (x && mask) opers, where mask = ((1 << n) - 1)
    for some n"""
    if not expr.is_op('BWAnd'):
        return
    [x, y] = expr.vals
    if not y.kind == 'Num':
        return
    val = y.val & ((1 << (y.typ.num)) - 1)
    if not two_powers:
        for i in range(129):
            two_powers[1 << i] = i
    return two_powers.get(val + 1)


def mk_bwand_mask(expr, n):
    return mk_bwand(expr, mk_num(((1 << n) - 1), expr.typ))


def end_addr(p, typ):
    if typ[0] == 'Array':
        (_, typ, n) = typ
        sz = mk_times(syntax.arch.mk_word(typ.size()), n)
    else:
        assert typ[0] == 'Type', typ
        (_, typ) = typ
        sz = syntax.arch.mk_word(typ.size())
    return mk_plus(p, mk_minus(sz, syntax.arch.mk_word(1)))


def pvalid_assertion1(xxx_todo_changeme3, xxx_todo_changeme4):
    """first pointer validity assertion: incompatibility.
    pvalid1 & pvalid2 --> non-overlapping OR somehow-contained.
    typ/typ2 is ('Type', syntax.Type) or ('Array', Type, Expr) for
    dynamically sized arrays.
    """
    (typ, k, p, pv) = xxx_todo_changeme3
    (typ2, k2, p2, pv2) = xxx_todo_changeme4
    offs1 = mk_minus(p, p2)
    cond1 = get_styp_condition(offs1, typ, typ2)
    offs2 = mk_minus(p2, p)
    cond2 = get_styp_condition(offs2, typ2, typ)

    out1 = mk_less(end_addr(p, typ), p2)
    out2 = mk_less(end_addr(p2, typ2), p)
    return mk_implies(mk_and(pv, pv2), foldr1(mk_or,
                                              [cond1, cond2, out1, out2]))


def pvalid_assertion2(xxx_todo_changeme5, xxx_todo_changeme6):
    """second pointer validity assertion: implication.
    pvalid1 & strictly-contained --> pvalid2
    """
    (typ, k, p, pv) = xxx_todo_changeme5
    (typ2, k2, p2, pv2) = xxx_todo_changeme6
    if typ[0] == 'Array' and typ2[0] == 'Array':
        # this is such a vague notion it's not worth it
        return true_term
    offs1 = mk_minus(p, p2)
    cond1 = get_styp_condition(offs1, typ, typ2)
    imp1 = mk_implies(mk_and(cond1, pv2), pv)
    offs2 = mk_minus(p2, p)
    cond2 = get_styp_condition(offs2, typ2, typ)
    imp2 = mk_implies(mk_and(cond2, pv), pv2)
    return mk_and(imp1, imp2)


def sym_distinct_assertion(xxx_todo_changeme7, xxx_todo_changeme8):
    (typ, p, pv) = xxx_todo_changeme7
    (start, end) = xxx_todo_changeme8
    out1 = mk_less(mk_plus(p, syntax.arch.mk_word(
        typ.size() - 1)), syntax.arch.mk_word(start))
    out2 = mk_less(syntax.arch.mk_word(end), p)
    return mk_implies(pv, mk_or(out1, out2))


def norm_array_type(t):
    if t[0] == 'Type' and t[1].kind == 'Array':
        (_, atyp) = t
        return ('Array', atyp.el_typ_symb, syntax.arch.mk_word(atyp.num), 'Strong')
    elif t[0] == 'Array' and len(t) == 3:
        (_, typ, l) = t
        # these derive from PArrayValid assertions. we know the array is
        # at least this long, but it might be longer.
        return ('Array', typ, l, 'Weak')
    else:
        return t


stored_styp_conditions = {}


def get_styp_condition(offs, inner_typ, outer_typ):
    r = get_styp_condition_inner1(inner_typ, outer_typ)
    if not r:
        return false_term
    else:
        return r(offs)


def get_styp_condition_inner1(inner_typ, outer_typ):
    inner_typ = norm_array_type(inner_typ)
    outer_typ = norm_array_type(outer_typ)
    k = (inner_typ, outer_typ)
    if k in stored_styp_conditions:
        return stored_styp_conditions[k]
    r = get_styp_condition_inner2(inner_typ, outer_typ)
    stored_styp_conditions[k] = r
    return r


def array_typ_size(xxx_todo_changeme9):
    (kind, el_typ, num, _) = xxx_todo_changeme9
    el_size = syntax.arch.mk_word(el_typ.size())
    return mk_times(num, el_size)


def get_styp_condition_inner2(inner_typ, outer_typ):
    if inner_typ[0] == 'Array' and outer_typ[0] == 'Array':
        (_, ityp, inum, _) = inner_typ
        (_, otyp, onum, outer_bound) = outer_typ
        # array fits in another array if the starting element is
        # a sub-element, and if the size of the left array plus
        # the offset fits in the right array
        cond = get_styp_condition_inner1(('Type', ityp), outer_typ)
        isize = array_typ_size(inner_typ)
        osize = array_typ_size(outer_typ)
        if outer_bound == 'Strong' and cond:
            return lambda offs: mk_and(cond(offs),
                                       mk_less_eq(mk_plus(isize, offs), osize))
        else:
            return cond
    elif inner_typ == outer_typ:
        return lambda offs: mk_eq(offs, syntax.arch.mk_word(0))
    elif outer_typ[0] == 'Type' and outer_typ[1].kind == 'Struct':
        conds = [(get_styp_condition_inner1(inner_typ,
                                            ('Type', sf_typ)), syntax.arch.mk_word(offs2))
                 for (_, offs2, sf_typ)
                 in structs[outer_typ[1].name].fields.values()]
        conds = [cond for cond in conds if cond[0]]
        if conds:
            return lambda offs: foldr1(mk_or,
                                       [c(mk_minus(offs, offs2))
                                        for (c, offs2) in conds])
        else:
            return None
    elif outer_typ[0] == 'Array':
        (_, el_typ, n, bound) = outer_typ
        cond = get_styp_condition_inner1(inner_typ, ('Type', el_typ))
        el_size = syntax.arch.mk_word(el_typ.size())
        size = mk_times(n, el_size)
        if bound == 'Strong' and cond:
            return lambda offs: mk_and(mk_less(offs, size),
                                       cond(mk_modulus(offs, el_size)))
        elif cond:
            return lambda offs: cond(mk_modulus(offs, el_size))
        else:
            return None
    else:
        return None


def all_vars_have_prop(expr, prop):
    class Failed (Exception):
        pass

    def visit(expr):
        if expr.kind != 'Var':
            return
        v2 = (expr.name, expr.typ)
        if not prop(v2):
            raise Failed()
    try:
        expr.visit(visit)
        return True
    except Failed:
        return False


def all_vars_in_set(expr, var_set):
    # type: (syntax.Expr, tuple[str, ...]) -> bool
    return all_vars_have_prop(expr, lambda v: v in var_set)


def var_not_in_expr(var, expr):
    v2 = (var.name, var.typ)
    return all_vars_have_prop(expr, lambda v: v != v2)


def mk_array_size_ineq(typ, num, p):
    align = typ.align()
    size = mk_times(syntax.arch.mk_word(typ.size()), num)
    size_lim = ((2 ** syntax.arch.word_size) -
                syntax.arch.ptr_size) / typ.size()
    return mk_less_eq(num, syntax.arch.mk_word(size_lim))


def mk_align_valid_ineq(typ, p):
    if typ[0] == 'Type':
        (_, typ) = typ
        align = typ.align()
        size = syntax.arch.mk_word(typ.size())
        size_req = []
    else:
        assert typ[0] == 'Array', typ
        (kind, typ, num) = typ
        align = typ.align()
        size = mk_times(syntax.arch.mk_word(typ.size()), num)
        size_req = [mk_array_size_ineq(typ, num, p)]
    assert align in [1, 4, 8]
    w0 = syntax.arch.mk_word(0)
    if align > 1:
        align_req = [mk_eq(mk_bwand(p, syntax.arch.mk_word(align - 1)), w0)]
    else:
        align_req = []
    return foldr1(mk_and, align_req + size_req + [mk_not(mk_eq(p, w0)),
                                                  mk_implies(mk_less(w0, size),
                                                             mk_less_eq(p, mk_uminus(size)))])

# generic operations on function/problem graphs


def dict_list(xys, keys=None):
    """dict_list ([(1, 2), (1, 3), (2, 4)]) = {1: [2, 3], 2: [4]}"""
    d = {}
    for (x, y) in xys:
        d.setdefault(x, [])
        d[x].append(y)
    if keys:
        for x in keys:
            d.setdefault(x, [])
    return d


def compute_preds(nodes):
    preds = dict_list([(c, n) for n in nodes
                       for c in nodes[n].get_conts()],
                      keys=nodes)
    for n in ['Ret', 'Err']:
        preds.setdefault(n, [])
    preds = dict([(n, sorted(set(ps)))
                  for (n, ps) in preds.items()])
    return preds


def simplify_node_elementary(node):
    if node.kind == 'Cond' and node.cond == true_term:
        return Node('Basic', node.left, [])
    elif node.kind == 'Cond' and node.cond == false_term:
        return Node('Basic', node.right, [])
    elif node.kind == 'Cond' and node.left == node.right:
        return Node('Basic', node.left, [])
    else:
        return node


def compute_var_flows(nodes, outputs, preds, override_lvals_rvals={}):
    # compute a graph of reverse var flows to pass to tarjan's algorithm
    graph = {}
    entries = ['Ret']
    for (n, node) in nodes.items():
        if node.kind == 'Basic':
            for (lv, rv) in node.upds:
                graph[(n, 'Post', lv)] = [(n, 'Pre', v)
                                          for v in syntax.get_expr_var_set(rv)]
        elif node.is_noop():
            pass
        else:
            if n in override_lvals_rvals:
                (lvals, rvals) = override_lvals_rvals[n]
            else:
                rvals = syntax.get_node_rvals(node)
                rvals = set(rvals.items())
                lvals = set(node.get_lvals())
            if node.kind != 'Basic':
                lvals = list(lvals) + ['PC']
                entries.append((n, 'Post', 'PC'))
            for lv in lvals:
                graph[(n, 'Post', lv)] = [(n, 'Pre', rv)
                                          for rv in rvals]
    graph['Ret'] = [(n, 'Post', v)
                    for n in preds['Ret'] for v in outputs(n)]
    vs = set([v for k in graph for (_, _, v) in graph[k]])
    for v in vs:
        for n in nodes:
            graph.setdefault((n, 'Post', v), [(n, 'Pre', v)])
            graph[(n, 'Pre', v)] = [(n2, 'Post', v)
                                    for n2 in preds[n]]

    comps = tarjan(graph, entries)
    return (graph, comps)


def mk_not_red(v):
    if v.is_op('Not'):
        [v] = v.vals
        return v
    else:
        return syntax.mk_not(v)


def cont_with_conds(nodes, n, conds):
    while True:
        if n not in nodes or nodes[n].kind != 'Cond':
            return n
        cond = nodes[n].cond
        if cond in conds:
            n = nodes[n].left
        elif mk_not_red(cond) in conds:
            n = nodes[n].right
        else:
            return n


def contextual_conds(nodes, preds):
    """computes a collection of conditions that can be assumed true
    at any point in the node graph."""
    pre_conds = {}
    arc_conds = {}
    visit = [n for n in nodes if not (preds[n])]
    while visit:
        n = visit.pop()
        if n not in nodes:
            continue
        in_arc_conds = [arc_conds.get((pre, n), set())
                        for pre in preds[n]]
        if not in_arc_conds:
            conds = set()
        else:
            conds = set.intersection(* in_arc_conds)
        if pre_conds.get(n) == conds:
            continue
        pre_conds[n] = conds
        if n not in nodes:
            continue
        if nodes[n].kind == 'Cond' and nodes[n].left == nodes[n].right:
            c_conds = [conds, conds]
        elif nodes[n].kind == 'Cond':
            c_conds = [nodes[n].cond, mk_not_red(nodes[n].cond)]
            c_conds = [set.union(set([c]), conds)
                       for c in c_conds]
        else:
            upds = set(nodes[n].get_lvals())
            c_conds = [set([c for c in conds if
                            not set.intersection(upds,
                                                 syntax.get_expr_var_set(c))])]
        for (cont, conds) in zip(nodes[n].get_conts(), c_conds):
            arc_conds[(n, cont)] = conds
            visit.append(cont)
    return (arc_conds, pre_conds)


def contextual_cond_simps(nodes, preds):
    """a common pattern in architectures with conditional operations is
    a sequence of instructions with the same condition.
    we can usually then reduce to a single contional block.
      b   e    =>    b-e
     / \ / \   =>   /   \
    a-c-d-f-g  =>  a-c-f-g
    this is sometimes important if b calculates a register that e uses
    since variable dependency analysis will see this register escape via
    the impossible path a-c-d-e
    """
    (arc_conds, pre_conds) = contextual_conds(nodes, preds)
    nodes = dict(nodes)
    for n in nodes:
        if nodes[n].kind == 'Cond':
            continue
        cont = nodes[n].cont
        conds = arc_conds[(n, cont)]
        cont2 = cont_with_conds(nodes, cont, conds)
        if cont2 != cont:
            nodes[n] = syntax.copy_rename(nodes[n],
                                          ({}, {cont: cont2}))
    return nodes


def minimal_loop_node_set(p):
    """discover a minimal set of loop addresses, excluding some operations
    using conditional instructions which are syntactically within the
    loop but semantically must always be followed by an immediate loop
    exit.

    amounts to rerunning loop detection after contextual_cond_simps."""

    loop_ns = set(p.loop_data)
    really_in_loop = {}
    nodes = contextual_cond_simps(p.nodes, p.preds)

    def is_really_in_loop(n):
        if n in really_in_loop:
            return really_in_loop[n]
        ns = []
        r = None
        while r == None:
            ns.append(n)
            if n not in loop_ns:
                r = False
            elif n in p.splittable_points(n):
                r = True
            else:
                conts = [n2 for n2 in nodes[n].get_conts()
                         if n2 != 'Err']
                if len(conts) > 1:
                    r = True
                else:
                    [n] = conts
        for n in ns:
            really_in_loop[n] = r
        return r
    return set([n for n in loop_ns if is_really_in_loop(n)])


def possible_graph_divs(p, min_cost=20, max_cost=20, ratio=0.85,
                        trace=None):
    es = [e[0] for e in p.entries]
    divs = []
    direct_costs = {}
    future_costs = {'Ret': set(), 'Err': set()}
    prev_costs = {}
    int_costs = {}
    fracs = {}
    for n in p.nodes:
        node = p.nodes[n]
        if node.kind == 'Call':
            cost = set([(n, 20)])
        elif p.loop_id(n):
            cost = set([(p.loop_id(n), 50)])
        else:
            cost = set([(n, len(node.get_mem_accesses()))])
            cost.discard((n, 0))
        direct_costs[n] = cost
    for n in p.tarjan_order:
        prev_costs[n] = set.union(* ([direct_costs[n]]
                                     + [prev_costs.get(c, set()) for c in p.preds[n]]))
    for n in reversed(p.tarjan_order):
        cont_costs = [future_costs.get(c, set())
                      for c in p.nodes[n].get_conts()]
        cost = set.union(* ([direct_costs[n]] + cont_costs))
        p_ct = sum([c for (_, c) in prev_costs[n]])
        future_costs[n] = cost
        if p.nodes[n].kind != 'Cond' or p_ct > max_cost:
            continue
        ct = sum([c for (_, c) in set.union(cost, prev_costs[n])])
        if ct < min_cost:
            continue
        [c1, c2] = [sum([c for (_, c)
                         in set.union(cs, prev_costs[n])])
                    for cs in cont_costs]
        fracs[n] = ((c1 * c1) + (c2 * c2)) / (ct * ct * 1.0)
        if fracs[n] < ratio:
            divs.append(n)
    divs.reverse()
    if trace != None:
        trace[0] = (direct_costs, future_costs, prev_costs,
                    int_costs, fracs)
    return divs


def compute_var_deps(nodes, outputs, preds, override_lvals_rvals={},
                     trace=None):
    # outs = list of (outname, retvars)
    var_deps = {}
    visit = set()
    visit.update(preds['Ret'])
    visit.update(preds['Err'])

    nodes = contextual_cond_simps(nodes, preds)

    while visit:
        n = visit.pop()

        node = simplify_node_elementary(nodes[n])
        if n in override_lvals_rvals:
            (lvals, rvals) = override_lvals_rvals[n]
            lvals = set(lvals)
            rvals = set(rvals)
        elif node.is_noop():
            lvals = set([])
            rvals = set([])
        else:
            rvals = syntax.get_node_rvals(node)
            rvals = set(rvals.items())
            lvals = set(node.get_lvals())
        cont_vs = set()

        for c in node.get_conts():
            if c == 'Ret':
                cont_vs.update(outputs(n))
            elif c == 'Err':
                pass
            else:
                cont_vs.update(var_deps.get(c, []))
        vs = set.union(rvals, cont_vs - lvals)

        if n in var_deps and vs <= var_deps[n]:
            continue
        if trace and n in trace:
            diff = vs - var_deps.get(n, set())
            printout('add %s at %d' % (diff, n))
            printout('  %s, %s, %s, %s' %
                     (len(vs), len(cont_vs), len(lvals), len(rvals)))
        var_deps[n] = vs
        visit.update(preds[n])

    return var_deps


def compute_loop_var_analysis(p, var_deps, n, override_nodes=None):
    if override_nodes == None:
        nodes = p.nodes
    else:
        nodes = override_nodes

    upd_vs = set([v for n2 in p.loop_body(n)
                  if not nodes[n2].is_noop()
                  for v in nodes[n2].get_lvals()])
    const_vs = set([v for n2 in p.loop_body(n)
                    for v in var_deps[n2] if v not in upd_vs])

    vca = compute_var_cycle_analysis(p, nodes, n,
                                     const_vs, set(var_deps[n]))
    vca = [(syntax.mk_var(nm, typ), data)
           for ((nm, typ), data) in list(vca.items())]
    return vca


cvca_trace = []
cvca_diag = [False]
no_accum_expressions = set()


def compute_var_cycle_analysis(p, nodes, n, const_vars, vs, diag=None):

    if diag == None:
        diag = cvca_diag[0]

    cache = {}
    del cvca_trace[:]
    impossible_nodes = {}
    loop = p.loop_body(n)

    def warm_cache_before(n2, v):
        cvca_trace.append((n2, v))
        cvca_trace.append('(')
        arc = []
        for i in range(100000):
            opts = [n3 for n3 in p.preds[n2] if n3 in loop
                    if v not in nodes[n3].get_lvals()
                    if n3 != n
                    if (n3, v) not in cache]
            if not opts:
                break
            n2 = opts[0]
            arc.append(n2)
        if not (len(arc) < 100000):
            trace('warmup overrun in compute_var_cycle_analysis')
            trace('chasing %s in %s' % (v, set(arc)))
            assert False, (v, arc[-500:])
        for n2 in reversed(arc):
            var_eval_before(n2, v)
        cvca_trace.append(')')

    def var_eval_before(n2, v, do_cmp=True):
        if (n2, v) in cache and do_cmp:
            return cache[(n2, v)]
        if n2 == n and do_cmp:
            var_exp = mk_var(v[0], v[1])
            vs = set([v for v in [v] if v not in const_vars])
            return (vs, var_exp)
        warm_cache_before(n2, v)
        ps = [n3 for n3 in p.preds[n2] if n3 in loop
              if not node_impossible(n3)]
        if not ps:
            return None
        vs = [var_eval_after(n3, v) for n3 in ps]
        if not all([v3 == vs[0] for v3 in vs]):
            if diag:
                trace('vs disagree for %s @ %d: %s' % (v, n2, vs))
            r = None
        else:
            r = vs[0]
        if do_cmp:
            cache[(n2, v)] = r
        return r

    def var_eval_after(n2, v):
        node = nodes[n2]
        if node.kind == 'Call' and v in node.rets:
            if diag:
                trace('fetched %s from call at %d' % (v, n2))
            return None
        elif node.kind == 'Basic':
            for (lv, val) in node.upds:
                if lv == v:
                    return expr_eval_before(n2, val)
            return var_eval_before(n2, v)
        else:
            return var_eval_before(n2, v)

    def expr_eval_before(n2, expr):
        if expr.kind == 'Op':
            if expr.vals == []:
                return (set(), expr)
            vals = [expr_eval_before(n2, v)
                    for v in expr.vals]
            if None in vals:
                return None
            s = set.union(* [s for (s, v) in vals])
            if len(s) > 1:
                if diag:
                    trace('too many vars for %s @ %d: %s' % (expr, n2, s))
                return None
            return (s, Expr('Op', expr.typ,
                            name=expr.name,
                            vals=[v for (s, v) in vals]))
        elif expr.kind == 'Num':
            return (set(), expr)
        elif expr.kind == 'Var':
            return var_eval_before(n2,
                                   (expr.name, expr.typ))
        else:
            if diag:
                trace('Unwalkable expr %s' % expr)
            return None

    def node_impossible(n2):
        if n2 in impossible_nodes:
            return impossible_nodes[n2]
        if n2 == n or n2 in p.get_loop_splittables(n):
            imposs = False
        else:
            pres = [n3 for n3 in p.preds[n2]
                    if n3 in loop if not node_impossible(n3)]
            if n2 in impossible_nodes:
                imposs = impossible_nodes[n2]
            else:
                imposs = not bool(pres)
        impossible_nodes[n2] = imposs
        node = nodes[n2]
        if imposs or node.kind != 'Cond':
            return imposs
        if 1 >= len([n3 for n3 in node.get_conts()
                     if n3 in loop]):
            return imposs
        c = expr_eval_before(n2, node.cond)
        if c != None:
            c = try_eval_expr(c[1])
        if c != None:
            trace('determined loop inner cond at %d equals %s'
                  % (n2, c == syntax.true_term))
        if c == syntax.true_term:
            impossible_nodes[node.right] = True
        elif c == syntax.false_term:
            impossible_nodes[node.left] = True
        return imposs

    vca = {}
    for v in vs:
        rv = var_eval_before(n, v, do_cmp=False)
        if rv == None:
            vca[v] = 'LoopVariable'
            continue
        (s, expr) = rv
        if expr == mk_var(v[0], v[1]):
            vca[v] = 'LoopConst'
            continue
        if all_vars_in_set(expr, const_vars):
            # a repeatedly evaluated const expression, is const
            vca[v] = 'LoopConst'
            continue
        if var_not_in_expr(mk_var(v[0], v[1]), expr):
            # leaf calculations do not have data flow to
            # themselves. the search algorithm doesn't
            # have to worry about these.
            vca[v] = 'LoopLeaf'
            continue
        (form, offs) = accumulator_closed_form(expr, v)
        if form != None and all_vars_in_set(form(), const_vars):
            vca[v] = ('LoopLinearSeries', form, offs)
        else:
            if diag:
                trace('No accumulator %s => %s'
                      % (v, expr))
            no_accum_expressions.add((v, expr))
            vca[v] = 'LoopVariable'
    return vca


eval_expr_solver = [None]


def try_eval_expr(expr):
    """attempt to reduce an expression to a single result, vaguely like
    what constant propagation would do. it might work!"""
    import search
    if not eval_expr_solver[0]:
        import solver
        eval_expr_solver[0] = solver.Solver()
    try:
        return search.eval_model_expr({}, eval_expr_solver[0], expr)
    except KeyboardInterrupt as e:
        raise e
    except Exception as e:
        return None


expr_linear_sum = set(['Plus', 'Minus'])
expr_linear_cast = set(['WordCast', 'WordCastSigned'])

expr_linear_all = set.union(expr_linear_sum, expr_linear_cast,
                            ['Times', 'ShiftLeft'])


def possibly_linear(expr):
    if expr.kind in set(['Var', 'Num', 'Symbol', 'Type', 'Token']):
        return True
    elif expr.is_op(expr_linear_all):
        return all([possibly_linear(x) for x in expr.vals])
    else:
        return False


def lv_expr(expr, env):
    if expr in env:
        return env[expr]
    elif expr.kind in set(['Num', 'Symbol', 'Type', 'Token']):
        return (expr, 'LoopConst', None, set())
    elif expr.kind == 'Var':
        return (None, None, None, None)
    elif expr.kind != 'Op':
        assert expr in env, expr

    lvs = [lv_expr(v, env) for v in expr.vals]
    rs = [lv[1] for lv in lvs]
    def mk_offs(vals): return syntax.adjust_op_vals(expr, vals)
    if None in rs:
        return (None, None, None, None)
    if set(rs) == set(['LoopConst']):
        return (expr, 'LoopConst', None, set())
    offs_set = set.union(* ([lv[3] for lv in lvs] + [set()]))
    arg_offs = []
    for (expr2, k, offs, _) in lvs:
        if k == 'LoopConst' and expr2.typ.kind == 'Word':
            arg_offs.append(syntax.mk_num(0, expr2.typ))
        else:
            arg_offs.append(offs)
    if expr.is_op(expr_linear_sum):
        if set(rs) == set(['LoopConst', 'LoopLinearSeries']):
            return (expr, 'LoopLinearSeries', mk_offs(arg_offs),
                    offs_set)
    elif expr.is_op('Times'):
        if set(rs) == set(['LoopLinearSeries', 'LoopConst']):
            # the new offset is the product of the linear offset
            # and the constant value
            [linear_offs] = [offs for (_, k, offs, _) in lvs
                             if k == 'LoopLinearSeries']
            [const_value] = [v for (v, k, _, _) in lvs
                             if k == 'LoopConst']
            return (expr, 'LoopLinearSeries',
                    mk_offs([linear_offs, const_value]), offs_set)
    if expr.is_op('ShiftLeft'):
        if rs == ['LoopLinearSeries', 'LoopConst']:
            return (expr, 'LoopLinearSeries',
                    mk_offs([arg_offs[0], lvs[1][0]]), offs_set)
    if expr.is_op(expr_linear_cast):
        if rs == ['LoopLinearSeries']:
            return (expr, 'LoopLinearSeries', mk_offs(arg_offs),
                    offs_set)
    return (None, None, None, None)

# FIXME: this should probably be unified with compute_var_cycle_analysis,
# but doing so is complicated


def linear_series_exprs(p, loop, va):
    def lv_init(v, data):
        if data[0] == 'LoopLinearSeries':
            return (v, 'LoopLinearSeries', data[2], set([data[2]]))
        elif data == 'LoopConst':
            return (v, 'LoopConst', None, set())
        else:
            return (None, None, None, None)
    cache = {loop: dict([(v, lv_init(v, data)) for (v, data) in va])}
    post_cache = {}
    loop_body = p.loop_body(loop)
    frontier = [n2 for n2 in p.nodes[loop].get_conts()
                if n2 in loop_body]

    def lv_merge(xxx_todo_changeme, xxx_todo_changeme1):
        (v1, lv1, offs1, oset1) = xxx_todo_changeme
        (v2, lv2, offs2, oset2) = xxx_todo_changeme1
        if v1 != v2:
            return (None, None, None, None)
        assert lv1 == lv2 and offs1 == offs2
        return (v1, lv1, offs1, oset1)

    def compute_post(n):
        if n in post_cache:
            return post_cache[n]
        pre_env = cache[n]
        env = dict(cache[n])
        if p.nodes[n].kind == 'Basic':
            for ((v, typ), rexpr) in p.nodes[n].upds:
                env[mk_var(v, typ)] = lv_expr(rexpr, pre_env)
        elif p.nodes[n].kind == 'Call':
            for (v, typ) in p.nodes[n].get_lvals():
                env[mk_var(v, typ)] = (None, None, None, None)
        post_cache[n] = env
        return env
    while frontier:
        n = frontier.pop()
        if [n2 for n2 in p.preds[n] if n2 in loop_body
                if n2 not in cache]:
            continue
        if n in cache:
            continue
        envs = [compute_post(n2) for n2 in p.preds[n]
                if n2 in loop_body]
        all_vs = set.union(* [set(env) for env in envs])
        cache[n] = dict([(v, foldr1(lv_merge,
                                    [env.get(v, (None, None, None, None))
                                     for env in envs]))
                         for v in all_vs])
        frontier.extend([n2 for n2 in p.nodes[n].get_conts()
                         if n2 in loop_body])
    return cache


def get_loop_linear_offs(p, loop_head):
    import search
    va = search.get_loop_var_analysis_at(p, loop_head)
    exprs = linear_series_exprs(p, loop_head, va)

    def offs_fn(n, expr):
        assert p.loop_id(n) == loop_head
        env = exprs[n]
        rv = lv_expr(expr, env)
        if rv[1] == None:
            return None
        elif rv[1] == 'LoopConst':
            return mk_num(0, expr.typ)
        elif rv[1] == 'LoopLinearSeries':
            return rv[2]
        else:
            assert not 'lv_expr kind understood', rv
    return offs_fn


def interesting_node_exprs(p, n, tags=None, use_pairings=True):
    if tags == None:
        tags = p.pairing.tags
    node = p.nodes[n]
    memaccs = node.get_mem_accesses()
    vs = [(kind, ptr) for (kind, ptr, v, m) in memaccs]
    vs += [('MemUpdateArg', v) for (kind, ptr, v, m) in memaccs
           if kind == 'MemUpdate']
    if node.kind == 'Call' and use_pairings:
        tag = p.node_tags[n][0]
        from target_objects import functions, pairings
        import solver
        fun = functions[node.fname]
        arg_input_map = dict(azip(fun.inputs, node.args))
        pairs = [pair for pair in pairings.get(node.fname, [])
                 if pair.tags == tags]
        if not pairs:
            return vs
        [pair] = pairs
        in_eq_vs = [(('Call', pair.name, i),
                     var_subst(v, arg_input_map))
                    for (i, ((lhs, l_s), (rhs, r_s)))
                    in enumerate(pair.eqs[0])
                    if l_s.endswith('_IN') and r_s.endswith('_IN')
                    if l_s != r_s
                    if solver.typ_representable(lhs.typ)
                    for (v, site) in [(lhs, l_s), (rhs, r_s)]
                    if site == '%s_IN' % tag]
        vs.extend(in_eq_vs)
    return vs


def interesting_linear_series_exprs(p, loop, va, tags=None,
                                    use_pairings=True):
    if tags == None:
        tags = p.pairing.tags
    expr_env = linear_series_exprs(p, loop, va)
    res_env = {}
    for (n, env) in expr_env.items():
        vs = interesting_node_exprs(p, n)

        vs = [(kind, v, lv_expr(v, env)) for (kind, v) in vs]
        vs = [(kind, v, offs, offs_set)
              for (kind, v, (_, lv, offs, offs_set)) in vs
              if lv == 'LoopLinearSeries']
        if vs:
            res_env[n] = vs
    return res_env


def mk_var_renames(xs, ys):
    renames = {}
    for (x, y) in azip(xs, ys):
        assert x.kind == 'Var' and y.kind == 'Var'
        assert x.name not in renames
        renames[x.name] = y.name
    return renames


def first_aligned_address(nodes, radix):
    ks = [k for k in nodes
          if k % radix == 0]
    if ks:
        return min(ks)
    else:
        return None


def entry_aligned_address(fun, radix):
    n = fun.entry
    while n % radix != 0:
        ns = fun.nodes[n].get_conts()
        assert len(ns) == 1, (fun.name, n)
        [n] = ns
    return n


def aligned_address_sanity(functions, symbols, radix):
    for (f, func) in functions.items():
        if f not in symbols:
            # happens for static or invented functions sometimes
            continue
        if func.entry:
            addr = first_aligned_address(func.nodes, radix)
            if addr == None:
                printout('Warning: %s: no aligned instructions' % f)
                continue
            addr2 = symbols[f][0]
            if addr != addr2:
                printout('target mismatch on func %s' % f)
                printout('  (starts at 0x%x not 0x%x)' % (addr, addr2))
                return False
            addr3 = entry_aligned_address(func, radix)
            if addr3 != addr2:
                printout('entry mismatch on func %s' % f)
                printout('  (enters at 0x%x not 0x%x)' % (addr3, addr2))
                return False
    return True

# variant of tarjan's strongly connected component algorithm


def tarjan(graph, entries):
    """tarjan (graph, entries)
    variant of tarjan's strongly connected component algorithm
    e.g. tarjan ({1: [2, 3], 3: [4, 5]}, [1])
    entries should not be reachable"""
    data = {}
    comps = []
    for v in entries:
        assert v not in data
        tarjan1(graph, v, data, [], set([]), comps)
    return comps


def tarjan1(graph, v, data, stack, stack_set, comps):
    vs = []
    while True:
        # skip through nodes with single successors
        data[v] = [len(data), len(data)]
        stack.append(v)
        stack_set.add(v)
        cs = graph[v]
        if len(cs) != 1 or cs[0] in data:
            break
        vs.append((v, cs[0]))
        [v] = cs

    for c in graph[v]:
        if c not in data:
            tarjan1(graph, c, data, stack, stack_set, comps)
            data[v][1] = min(data[v][1], data[c][1])
        elif c in stack_set:
            data[v][1] = min(data[v][1], data[c][0])

    vs.reverse()
    for (v2, c) in vs:
        data[v2][1] = min(data[v2][1], data[c][1])

    for (v2, _) in [(v, 0)] + vs:
        if data[v2][1] == data[v2][0]:
            comp = []
            while True:
                x = stack.pop()
                stack_set.remove(x)
                if x == v2:
                    break
                comp.append(x)
            comps.append((v2, comp))


def divides_loop(graph, split_set):
    graph2 = dict(graph)
    for n in split_set:
        graph2[n] = []
    assert 'ENTRY_POINT' not in graph2
    graph2['ENTRY_POINT'] = list(graph)
    comps = tarjan(graph2, ['ENTRY_POINT'])
    return not ([(h, t) for (h, t) in comps if t])


def strongly_connected_split_points1(graph):
    """find the nodes of a strongly connected
    component which, when removed, disconnect the component.
    complex loops lack such a split point."""

    # find one simple cycle in the graph
    walk = []
    walk_set = set()
    n = min(graph)
    while n not in walk_set:
        walk.append(n)
        walk_set.add(n)
        n = graph[n][0]
    i = walk.index(n)
    cycle = walk[i:]

    def subgraph_test(subgraph):
        graph2 = dict([(n, [n2 for n2 in graph[n] if n2 in subgraph])
                       for n in subgraph])
        graph2['HEAD'] = list(subgraph)
        comps = tarjan(graph2, ['HEAD'])
        return bool([h for (h, t) in comps if t])

    cycle_set = set(cycle)
    cycle = [('Node', set([n]), False,
              [n2 for n2 in graph[n] if n2 != graph[n][0]])
             for n in cycle]
    i = 0
    while i < len(cycle):
        (kind, ns, test, unvisited) = cycle[i]
        if not unvisited:
            i += 1
            continue
        n = unvisited.pop()
        arc_set = set()
        while n not in cycle_set:
            if n in arc_set:
                # found two totally disjoint loops, so there
                # are no splitting points
                return set()
            arc_set.add(n)
            n = graph[n][0]
        if n in ns:
            if kind == 'Node':
                # only this node can be a splittable now.
                if subgraph_test(set(graph) - set([n])):
                    return set()
                else:
                    return set([n])
            else:
                cycle[i] = (kind, ns, True, unvisited)
                ns.update(arc_set)
                continue
        j = (i + 1) % len(cycle)
        new_ns = set()
        new_unvisited = set()
        new_test = False
        while n not in cycle[j][1]:
            new_ns.update(cycle[j][1])
            new_unvisited.update(cycle[j][3])
            new_test = cycle[j][2] or new_test
            j = (j + 1) % len(cycle)
        new_ns.update(arc_set)
        new_unvisited.update([n3 for n2 in arc_set for n3 in graph[n2]])
        new_v = ('Group', new_ns, new_test, list(new_unvisited - new_ns))
        if j > i:
            cycle[i + 1:j] = [new_v]
        else:
            cycle = [cycle[i], new_v] + cycle[j:i]
            i = 0
        cycle_set.update(new_ns)
    for (kind, ns, test, unvisited) in cycle:
        if test and subgraph_test(ns):
            return set()
    return set([n for (kind, ns, _, _) in cycle
                if kind == 'Node' for n in ns])


def strongly_connected_split_points(graph):
    res = strongly_connected_split_points1(graph)
    res2 = set()
    for n in graph:
        graph2 = dict(graph)
        graph2[n] = []
        graph2['ENTRY'] = list(graph)
        comps = tarjan(graph2, ['ENTRY'])
        if not [comp for comp in comps if comp[1]]:
            res2.add(n)
    assert res == res2, (graph, res, res2)
    return res


def get_one_loop_splittable(p, loop_set):
    """discover a component of a strongly connected
    component which, when removed, disconnects the component.
    complex loops lack such a split point."""
    candidates = set(loop_set)
    graph = dict([(x, [y for y in p.nodes[x].get_conts()
                       if y in loop_set]) for x in loop_set])
    while candidates:
        loop2 = find_loop_avoiding(graph, loop_set, candidates)
        candidates = set.intersection(loop2, candidates)
        if not candidates:
            return None
        n = candidates.pop()
        graph2 = dict([(x, [y for y in graph[x] if y != n])
                       for x in graph])
        comps = tarjan(graph2, [n])
        comps = [(h, t) for (h, t) in comps if t]
        if not comps:
            return n
        for (h, t) in comps:
            s = set([h] + t)
            candidates = set.intersection(s, candidates)
    return None


def find_loop_avoiding(graph, loop, avoid):
    n = (list(loop - avoid) + list(loop))[0]
    arc = [n]
    visited = set([n])
    while True:
        cs = set(graph[n])
        acs = cs - avoid
        vcs = set.intersection(cs, visited)
        if vcs:
            n = vcs.pop()
            break
        elif acs:
            n = acs.pop()
        else:
            n = cs.pop()
        visited.add(n)
        arc.append(n)
    [i] = [i for (i, n2) in enumerate(arc) if n2 == n]
    return set(arc[i:])

# non-equality relations in proof hypotheses are recorded as a pretend
# equality and reverted to their 'real' meaning here.


def mk_stack_wrapper(stack_ptr, stack, excepts):
    return syntax.mk_rel_wrapper('StackWrapper',
                                 [stack_ptr, stack] + excepts)


def mk_mem_acc_wrapper(addr, v):
    return syntax.mk_rel_wrapper('MemAccWrapper', [addr, v])


def mk_mem_wrapper(m):
    return syntax.mk_rel_wrapper('MemWrapper', [m])


def list_from_tm(t):
    xs = []
    while t.is_op('Plus'):
        [x, t] = t.vals
        assert x.kind == 'Num' and x.typ == syntax.arch.word_type
        xs.append(x.val)
    if t.kind == 'Num':
        xs.append(t.val)
    return xs


def tm_with_word_list(xs):
    if xs:
        return foldr1(mk_plus, list(map(syntax.arch.mk_word, xs)))
    else:
        return mk_uminus(syntax.arch.mk_word(0))


def mk_eq_selective_wrapper(v, xxx_todo_changeme10):
    # this is a huge hack, but we need to put these lists somewhere
    (xs, ys) = xxx_todo_changeme10
    xs = tm_with_word_list(xs)
    ys = tm_with_word_list(ys)
    return syntax.mk_rel_wrapper('EqSelectiveWrapper', [v, xs, ys])


def apply_rel_wrapper(lhs, rhs):
    assert lhs.typ == syntax.builtinTs['RelWrapper']
    assert rhs.typ == syntax.builtinTs['RelWrapper']
    assert lhs.kind == 'Op'
    assert rhs.kind == 'Op'
    ops = set([lhs.name, rhs.name])
    if ops == set(['StackWrapper']):
        [sp1, st1] = lhs.vals[:2]
        [sp2, st2] = rhs.vals[:2]
        excepts = list(set(lhs.vals[2:] + rhs.vals[2:]))
        for p in excepts:
            st1 = syntax.mk_memupd(st1, p, syntax.arch.mk_word(0))
            st2 = syntax.mk_memupd(st2, p, syntax.arch.mk_word(0))

        return syntax.Expr('Op', boolT, name='StackEquals',
                           vals=[sp1, st1, sp2, st2])
    elif ops == set(['MemAccWrapper', 'MemWrapper']):
        [acc] = [v for v in [lhs, rhs] if v.is_op('MemAccWrapper')]
        [addr, val] = acc.vals
        assert addr.typ == syntax.arch.wordT
        [m] = [v for v in [lhs, rhs] if v.is_op('MemWrapper')]
        [m] = m.vals
        assert m.typ == builtinTs['Mem']
        expr = mk_eq(mk_memacc(m, addr, val.typ), val)
        return expr
    elif ops == set(['EqSelectiveWrapper']):
        [lhs_v, _, _] = lhs.vals
        [rhs_v, _, _] = rhs.vals
        if lhs_v.typ == syntax.builtinTs['RelWrapper']:
            return apply_rel_wrapper(lhs_v, rhs_v)
        else:
            return mk_eq(lhs, rhs)
    else:
        assert not 'rel wrapper opname understood'


def inst_eq_at_visit(exp, vis):
    if not exp.is_op('EqSelectiveWrapper'):
        return True
    [_, xs, ys] = exp.vals
    xs = list_from_tm(xs)
    ys = list_from_tm(ys)
    if vis.kind == 'Number':
        return vis.n in xs
    elif vis.kind == 'Offset':
        return vis.n in ys
    else:
        assert not 'visit kind useable', vis


def strengthen_hyp(expr, sign=1):
    if not expr.kind == 'Op':
        return expr
    if expr.name in ['And', 'Or']:
        vals = [strengthen_hyp(v, sign) for v in expr.vals]
        return syntax.adjust_op_vals(expr, vals)
    elif expr.name == 'Implies':
        [l, r] = expr.vals
        l = strengthen_hyp(l, - sign)
        r = strengthen_hyp(r, sign)
        return syntax.mk_implies(l, r)
    elif expr.name == 'Not':
        [x] = expr.vals
        x = strengthen_hyp(x, - sign)
        return syntax.mk_not(x)
    elif expr.name == 'StackEquals':
        if sign == 1:
            return syntax.Expr('Op', boolT,
                               name='ImpliesStackEquals', vals=expr.vals)
        else:
            return syntax.Expr('Op', boolT,
                               name='StackEqualsImplies', vals=expr.vals)
    elif expr.name == 'ROData':
        if sign == 1:
            return syntax.Expr('Op', boolT,
                               name='ImpliesROData', vals=expr.vals)
        else:
            return expr
    elif expr.name == 'Equals' and expr.vals[0].typ == boolT:
        vals = expr.vals
        if vals[1] in [syntax.true_term, syntax.false_term]:
            vals = [vals[1], vals[0]]
        if vals[0] == syntax.true_term:
            return strengthen_hyp(vals[1], sign)
        elif vals[0] == syntax.false_term:
            return strengthen_hyp(syntax.mk_not(vals[1]), sign)
        else:
            return expr
    else:
        return expr


def weaken_assert(expr):
    return strengthen_hyp(expr, -1)


pred_logic_ops = set(['Not', 'And', 'Or', 'Implies'])


def norm_neg(expr):
    if not expr.is_op('Not'):
        return expr
    [nexpr] = expr.vals
    if not nexpr.is_op(pred_logic_ops):
        return expr
    if nexpr.is_op('Not'):
        [expr] = nexpr.vals
        return norm_neg(expr)
    [x, y] = nexpr.vals
    if nexpr.is_op('And'):
        return mk_or(norm_mk_not(x), norm_mk_not(y))
    elif nexpr.is_op('Or'):
        return mk_and(norm_mk_not(x), norm_mk_not(y))
    elif nexpr.is_op('Implies'):
        return mk_and(x, mk_not(y))


def norm_mk_not(expr):
    return norm_neg(mk_not(expr))


def split_conjuncts(expr):
    # type: (Expr) -> List[Expr]
    expr = norm_neg(expr)
    if expr.is_op('And'):
        [x, y] = expr.vals
        return split_conjuncts(x) + split_conjuncts(y)
    else:
        return [expr]


def split_disjuncts(expr):
    expr = norm_neg(expr)
    if expr.is_op('Or'):
        [x, y] = expr.vals
        return split_disjuncts(x) + split_disjuncts(y)
    else:
        return [expr]


def binary_search_least(test, minimum, maximum):
    """find least n, minimum <= n <= maximum, for which test (n)."""
    assert maximum >= minimum
    if test(minimum):
        return minimum
    if maximum == minimum or not test(maximum):
        return None
    while maximum > minimum + 1:
        cur = (minimum + maximum) / 2
        if test(cur):
            maximum = cur
        else:
            minimum = cur + 1
    assert minimum + 1 == maximum
    return maximum


def binary_search_greatest(test, minimum, maximum):
    """find greatest n, minimum <= n <= maximum, for which test (n)."""
    assert maximum >= minimum
    if test(maximum):
        return maximum
    if maximum == minimum or not test(minimum):
        return None
    while maximum > minimum + 1:
        cur = (minimum + maximum) / 2
        if test(cur):
            minimum = cur
        else:
            maximum = cur - 1
    assert minimum + 1 == maximum
    return minimum