"""ISL condition recovery by CFG DATAFLOW, replacing `isl.conditions`'s linear walk.

`isl.conditions` walks the flat stream and resets its tracker at every
control-flow boundary, so a block entered only by a branch reports an unknown.
This module instead builds the CFG and runs a worklist fixpoint, joining each
block's state over its ACTUAL predecessors (a value survives the join only if
every predecessor agrees).

Measured over all 28 stages, against the linear walk:

    instructions reached by the CFG         85.0%
    condition sites with an unknown LHS     402 (5.32%)   linear walk: 756 (10.00%)
    of those, still never reached           389
    sites where both resolve but DISAGREE   161   <- the linear walk was wrong

Two things the entry-point search had to get right, both of which read as zero
results first:

  * The phase bases reach only ~36% of the code.  Most routines are COROUTINES
    the engine starts from its trigger queue, so they have no static predecessor
    and must be seeded from every `start_coroutine` target.
  * That target is staged in TWO steps -- `special[0] = imm` then
    `local[0] = special[0]`.  Matching only the direct-immediate form found ZERO
    entries in a file with 216 of them.

The 389 that remain unreached are the honest limit: nothing in the bytecode
starts them, so they are entered by data (the trigger queue at `phase+272`),
not by code.
"""
import struct, collections
import isl

REL = isl.REL

def _val(op, kind, operand, lo, sp, loc):
    if kind == 1:
        if op == 1:
            return '%.6g' % struct.unpack('>d', struct.pack('>II', operand, lo))[0]
        return str(operand)
    if kind == 2: return sp.get(operand)
    if kind == 3: return loc.get(operand)
    return 'global[%d]' % operand

def _pack(sp, loc, stack):
    return (tuple(sorted(sp.items())), tuple(sorted(loc.items())), tuple(stack))

def _join(a, bst):
    if a is None: return bst
    if bst is None: return a
    if a == bst: return a
    def m(x, y):
        dx, dy = dict(x), dict(y)
        return tuple(sorted((k, v) for k, v in dx.items() if dy.get(k) == v))
    st = a[2] if a[2] == bst[2] else ()
    return (m(a[0], bst[0]), m(a[1], bst[1]), st)

def edges(b, spawn=False):
    """off -> successors.  `spawn` includes the coroutine a start_coroutine creates."""
    offs = isl.linear_offsets(b)
    nxt = {offs[i]: offs[i+1] for i in range(len(offs)-1)}
    bases = isl.phase_bases(b)
    E = collections.defaultdict(list)
    loc, sp = {}, {}
    for off in offs:
        w = struct.unpack_from('>I', b, off)[0]
        op, ln = w & 0xFF, (w >> 8) & 0xFF
        sk, dk = (w >> 24) & 0xFF, (w >> 16) & 0xFF
        words = [struct.unpack_from('>I', b, off+i)[0]
                 for i in range(4, max(ln,4), 4) if off+i+4 <= len(b)]
        ph = sum(1 for x in bases if x <= off)
        base = bases[ph-1] if ph else bases[0]
        fall = nxt.get(off)
        if op == 0 and len(words) >= 2:
            v = words[1] if sk == 1 else sp.get(words[1]) if sk == 2 else None
            d = sp if dk == 2 else loc
            if v is None: d.pop(words[0], None)
            else: d[words[0]] = v
        elif op == 19 and words:
            if words[0] == 11: fall = None            # end_coroutine: thread dies
            if spawn and words[0] == 1 and 0 in loc:
                t = base + loc[0]
                if t in nxt or t in offs: E[off].append(t)
            loc = {}
        elif op == 12 and words:
            E[off].append(base + words[0]); fall = None
        elif op in isl.REL and words:
            E[off].append(base + words[0])
        if fall: E[off].append(fall)
    return E, nxt


def must_reach_exit(b):
    """Nodes from which an `END_PHASE` is UNAVOIDABLE.

    Least fixpoint: n qualifies when it has successors and ALL of them qualify.
    Deliberately conservative -- a loop never enters the set, which is the honest
    answer: a poll loop reaches its exit only if the polled predicate eventually
    becomes true, and that is a LIVENESS property, not a graph one.
    """
    import collections as _c
    E, _nxt = edges(b, spawn=True)
    ends = {o for o, bid, _x in isl.call_sites(b) if bid in (6, 62)}
    rev = _c.defaultdict(list)
    for a, ss in E.items():
        for s in ss: rev[s].append(a)
    A = set(ends)
    work = _c.deque(ends)
    while work:
        n = work.popleft()
        for pnode in rev.get(n, ()):
            if pnode in A: continue
            ss = E.get(pnode, ())
            if ss and all(x in A for x in ss):
                A.add(pnode); work.append(pnode)
    return A


def dominating_conditions(b):
    """For each END_PHASE / FORCE_END_PHASE site, the conditions that DOMINATE it.

    A condition dominates an exit when EVERY path from an entry to that exit
    passes through it -- so it is a NECESSARY condition for the phase to end.
    That is what the port needs.

    ⚠️ The obvious query, "one branch reaches END_PHASE and the other does not",
    is WRONG for this language and was tried first.  The dominant shape here is a
    POLL LOOP, where the loop-back branch also reaches the exit -- one iteration
    later -- so neither successor discriminates.  It found exactly ONE guard in
    each of Stage 02's phases 1 and 3 (a `read_freg(0) < 1200` timeout) while
    missing every objective test.  Dominance has no such blind spot.
    """
    import collections as _c
    E, nxt = edges(b, spawn=True)
    offs = isl.linear_offsets(b)
    entries = {e for e in set(isl.phase_bases(b)) | set(coroutine_entries(b))
               | set(stream_entries(b)) if e in nxt}
    preds = _c.defaultdict(list)
    for a, ss in E.items():
        for s in ss: preds[s].append(a)
    R, q = set(entries), _c.deque(entries)
    while q:
        n = q.popleft()
        for s in E.get(n, ()):
            if s not in R: R.add(s); q.append(s)
    order = [o for o in offs if o in R]
    idx = {o: i for i, o in enumerate(order)}
    N = len(order); FULL = (1 << N) - 1
    DOM = [(1 << i) if o in entries else FULL for i, o in enumerate(order)]
    for _ in range(50):
        changed = False
        for i, o in enumerate(order):
            if o in entries: continue
            ps = [idx[p] for p in preds.get(o, ()) if p in idx]
            if not ps: new = 1 << i
            else:
                acc = DOM[ps[0]]
                for p in ps[1:]: acc &= DOM[p]
                new = acc | (1 << i)
            if new != DOM[i]: DOM[i] = new; changed = True
        if not changed: break
    conds = {c['off']: c for c in conditions(b, isl.symbols(b, 1), isl.symbols(b, 2))}
    A = must_reach_exit(b)
    for c in conds.values():
        c['sufficient'] = c['target'] in A
    bases = isl.phase_bases(b)
    out = []
    for e, bid, _x in [(o, bid, x) for o, bid, x in isl.call_sites(b) if bid in (6, 62)]:
        ph = sum(1 for x in bases if x <= e)
        if e not in idx:
            out.append({'end': e, 'phase': ph, 'builtin': bid, 'conds': None}); continue
        m = DOM[idx[e]]
        dc = [conds[order[i]] for i in range(N) if (m >> i) & 1 and order[i] in conds]
        out.append({'end': e, 'phase': ph, 'builtin': bid,
                    'conds': sorted(dc, key=lambda c: c['off'])})
    return out, len(R), len(offs)


def stream_entries(b):
    """The pair of entry points each mission-level `0x1883` record carries.

    Layout, per phase:  `0x1883, base_delta, size, 0, entry_a, entry_b`
    with both entries PHASE-RELATIVE.  Measured over all 28 stages: 82 of 88
    land on a valid instruction (93.2 %) against a 38.6 % chance rate for a
    random 4-aligned offset.

    These are why some routines have no static predecessor at all: nothing in
    the bytecode names them.  In Stage 02 the SECOND entry of phases 1 and 3 is
    exactly the `FORCE_END_PHASE` site that the CFG could not otherwise reach.
    """
    code = struct.unpack_from('>I', b, 0x08)[0]
    end = struct.unpack_from('>I', b, 0x0C)[0]
    out = []
    for o in range(0x24, 0x400, 4):
        if o + 24 > len(b): break
        if struct.unpack_from('>I', b, o)[0] == 0x1883:
            base = code + struct.unpack_from('>I', b, o + 4)[0]
            for k in (16, 20):
                t = base + struct.unpack_from('>I', b, o + k)[0]
                if 0 <= t < end: out.append(t)
    return out


def coroutine_entries(b):
    """Every `start_coroutine` target, found by a linear pre-pass."""
    offs = isl.linear_offsets(b)
    bases = isl.phase_bases(b)
    out, loc, sp = [], {}, {}
    for off in offs:
        w = struct.unpack_from('>I', b, off)[0]
        op, ln = w & 0xFF, (w >> 8) & 0xFF
        sk, dk = (w >> 24) & 0xFF, (w >> 16) & 0xFF
        words = [struct.unpack_from('>I', b, off + i)[0]
                 for i in range(4, max(ln, 4), 4) if off + i + 4 <= len(b)]
        if op == 0 and len(words) >= 2:
            # staging is TWO-step: `special[0] = imm` then `local[0] = special[0]`.
            # Matching only the direct-immediate form found ZERO entries in a file
            # with 216 start_coroutine sites.
            v = words[1] if sk == 1 else sp.get(words[1]) if sk == 2 else None
            if v is None: (sp if dk == 2 else loc).pop(words[0], None)
            else: (sp if dk == 2 else loc)[words[0]] = v
        elif op == 19 and words:
            if words[0] == 1 and 0 in loc:
                ph = sum(1 for x in bases if x <= off)
                out.append(bases[ph - 1] + loc[0])
            loc = {}
    return out


def conditions(b, s1=None, s2=None):
    offs = isl.linear_offsets(b)
    nxt = {offs[i]: offs[i + 1] for i in range(len(offs) - 1)}
    bases = isl.phase_bases(b)
    EMPTY = ((), (), ())
    IN = {}
    work = collections.deque()
    # Entry points.  The phase bases alone reach only ~36% of the code: most
    # routines are COROUTINES the engine starts from its trigger queue, so they
    # have no static predecessor.  Seed every `start_coroutine` target as well --
    # a linear pre-pass finds them because the target is staged into local[0]
    # immediately before the call, which no control-flow boundary intervenes in.
    entries = list(bases) + coroutine_entries(b) + stream_entries(b)
    for e in entries:
        if e in nxt or e == offs[-1]:
            IN[e] = EMPTY; work.append(e)
    conds = {}
    pend_at = {}
    seen_entry = set(bases)
    rounds = 0
    while work:
        rounds += 1
        if rounds > 400000: break
        off = work.popleft()
        state = IN[off]
        sp, loc, stack = dict(state[0]), dict(state[1]), list(state[2])
        w = struct.unpack_from('>I', b, off)[0]
        op, ln = w & 0xFF, (w >> 8) & 0xFF
        sk, dk = (w >> 24) & 0xFF, (w >> 16) & 0xFF
        words = [struct.unpack_from('>I', b, off + i)[0]
                 for i in range(4, max(ln, 4), 4) if off + i + 4 <= len(b)]
        succ, fall = [], nxt.get(off)
        if op in (0, 1) and len(words) >= 2:
            v = _val(op, sk, words[1], words[2] if len(words) > 2 else 0, sp, loc)
            d = sp if dk == 2 else loc
            if v is None: d.pop(words[0], None)
            else: d[words[0]] = v
        elif op == 19 and words:
            bid = words[0]
            nm = isl.BUILTIN.get(bid, 'builtin%d' % bid)
            args = []
            tags = {sl - 4 for sl, ids in isl.UNIT_SLOTS.items() if bid in ids and sl in loc}
            for sl in sorted(loc):
                v = loc[sl]
                if sl in tags and v == '1': continue
                if v.isdigit():
                    i = int(v)
                    if s2 and bid in isl.UNIT_SLOTS.get(sl, ()) and i in s2: v = s2[i][1]
                    elif s1 and bid in isl.SYM1_SLOTS.get(sl, ()) and i in s1: v = s1[i][1]
                args.append(v)
            sp[0] = '%s(%s)' % (nm, ', '.join(args))
            loc = {}
            if bid == 1:                       # start_coroutine: a FRESH thread
                t = state[1] and dict(state[1]).get(0)
                if t and t.isdigit():
                    e = bases[max(0, sum(1 for x in bases if x <= off) - 1)] + int(t)
                    if e in nxt or e in IN:
                        if e not in seen_entry:
                            seen_entry.add(e); IN[e] = EMPTY; work.append(e)
            if bid == 11:                      # end_coroutine: thread destroyed
                fall = None
        elif op in (21, 22):
            stack.append(sp.get(1))
        elif op in (23, 24):
            if stack: sp[1] = stack.pop()
            else: sp.pop(1, None)
        elif op == 12 and words:
            ph = sum(1 for x in bases if x <= off)
            succ.append(bases[ph - 1] + words[0]); fall = None
        elif op in (10, 11):
            pend_at[off] = (_val(op, dk, words[0], 0, sp, loc),
                            _val(op, sk, words[1], words[2] if len(words) > 2 else 0, sp, loc))
        elif op in REL and words:
            ph = sum(1 for x in bases if x <= off)
            succ.append(bases[ph - 1] + words[0])
        out = _pack(sp, loc, stack)
        for s in ([fall] if fall else []) + succ:
            if s is None or s not in nxt and s not in IN and s != offs[-1]: continue
            j = _join(IN.get(s), out)
            if IN.get(s) != j:
                IN[s] = j; work.append(s)
    # read conditions off the fixpoint
    out = []
    prev = None
    for off in offs:
        w = struct.unpack_from('>I', b, off)[0]; op = w & 0xFF
        if op in (10, 11): prev = off
        elif op in REL and prev is not None:
            lhs, rhs = pend_at.get(prev, (None, None))
            ph = sum(1 for x in bases if x <= off)
            words = [struct.unpack_from('>I', b, off + 4)[0]]
            out.append({'off': prev, 'phase': ph, 'lhs': lhs, 'rel': REL[op],
                        'rhs': rhs, 'target': bases[ph - 1] + words[0]})
            prev = None
    return out