# pylint:disable=line-too-long,import-outside-toplevel,import-error,multiple-statements,too-many-boolean-expressions
# ruff: noqa: SIM102
from __future__ import annotations
from typing import Any, TYPE_CHECKING
from collections import defaultdict, OrderedDict
from enum import Enum
import logging

import networkx

import claripy
from angr.ailment.block import Block
from angr.ailment.statement import Statement, ConditionalJump, Jump, Label, Return
from angr.ailment.expression import Const, UnaryOp, MultiStatementExpression, BinaryOp

from angr.utils.graph import GraphUtils
from angr.utils.ail import is_phi_assignment, is_head_controlled_loop_block
from angr.knowledge_plugins.cfg import IndirectJump, IndirectJumpType
from angr.utils.constants import SWITCH_MISSING_DEFAULT_NODE_ADDR
from angr.utils.graph import dominates, to_acyclic_graph, dfs_back_edges
from angr.analyses.decompiler.sequence_walker import SequenceWalker
from angr.analyses.decompiler.utils import (
    remove_last_statement,
    remove_last_statements,
    extract_jump_targets,
    switch_extract_cmp_bounds,
    switch_extract_cmp_bounds_from_condition,
    is_empty_or_label_only_node,
    has_nonlabel_nonphi_statements,
    first_nonlabel_nonphi_statement,
    switch_extract_bitwiseand_jumptable_info,
    switch_extract_switch_expr_from_jump_target,
)
from angr.analyses.decompiler.counters.call_counter import AILCallCounter
from angr.analyses.decompiler.node_replacer import NodeReplacer
from .structurer_nodes import (
    ConditionNode,
    SequenceNode,
    LoopNode,
    ConditionalBreakNode,
    BreakNode,
    ContinueNode,
    BaseNode,
    MultiNode,
    SwitchCaseNode,
    IncompleteSwitchCaseNode,
    EmptyBlockNotice,
    IncompleteSwitchCaseHeadStatement,
)
from .structurer_base import StructurerBase

if TYPE_CHECKING:
    from angr.knowledge_plugins.functions import Function

l = logging.getLogger(__name__)
_DEBUG = False


class GraphChangedNotification(Exception):
    """
    A notification for graph that is currently worked on being changed. Once this notification is caught, the graph
    schema matching process for the current region restarts.
    """


class MultiStmtExprMode(str, Enum):
    """
    Mode of multi-statement expression creation during structuring.
    """

    NEVER = "Never"
    ALWAYS = "Always"
    MAX_ONE_CALL = "Only when less than one call"


class GraphEdgeFilter:
    """
    Filters away edges in a graph that are marked as deleted (outgoing-edges) during cyclic refinement.
    """

    def __init__(self, graph: networkx.DiGraph):
        self.graph = graph

    def __call__(self, src, dst) -> bool:
        d = self.graph[src][dst]
        return not d.get("cyclic_refinement_outgoing", False)


def _f(graph: networkx.DiGraph):
    return networkx.subgraph_view(graph, filter_edge=GraphEdgeFilter(graph))


class PhoenixStructurer(StructurerBase):
    """
    Structure a region using a structuring algorithm that is similar to the one in Phoenix decompiler (described in the
    "phoenix decompiler" paper). Note that this implementation has quite a few improvements over the original described
    version and *should not* be used to evaluate the performance of the original algorithm described in that paper.
    """

    NAME = "phoenix"

    def __init__(
        self,
        region,
        parent_map=None,
        condition_processor=None,
        func: Function | None = None,
        case_entry_to_switch_head: dict[int, int] | None = None,
        parent_region=None,
        improve_algorithm=False,
        use_multistmtexprs: MultiStmtExprMode = MultiStmtExprMode.MAX_ONE_CALL,
        multistmtexpr_stmt_threshold: int = 5,
        **kwargs,
    ):
        super().__init__(
            region,
            parent_map=parent_map,
            condition_processor=condition_processor,
            func=func,
            case_entry_to_switch_head=case_entry_to_switch_head,
            parent_region=parent_region,
            **kwargs,
        )

        # whitelist certain edges. removing these edges will destroy critical schemas, which will impact future
        # structuring cycles.
        # the set is populated during the analysis. _last_resort_refinement() will ensure not to remove any edges
        # who fall into these sets.
        self.whitelist_edges: set[tuple[int, int]] = set()
        # also whitelist certain nodes that are definitely header for switch-case constructs. they should not be merged
        # into another node before we successfully structure the entire switch-case.
        self.switch_case_known_heads: set[Block | BaseNode] = set()

        # whitelist certain nodes that should be treated as a tail node for do-whiles. these nodes should not be
        # absorbed into other SequenceNodes
        self.dowhile_known_tail_nodes: set = set()

        # in reimplementing the core phoenix algorithm from the phoenix decompiler paper, two types of changes were
        # made to the algorithm:
        # 1. Mandatory fixes to correct flaws we found in the algorithm
        # 2. Optional fixes to improve the results of already correct choices
        #
        # the improve_algorithm flag controls whether the optional fixes are applied. these are disabled by default
        # to be as close to the original algorithm as possible. for best results, enable this flag.
        self._improve_algorithm = improve_algorithm
        self._edge_virtualization_hints = []

        # for each region, we only convert a switch-case head into an IncompleteSwitchCaseNode once. this is to avoid
        # loops of creating and unpacking IncompleteSwitchCaseNode (when the entire switch-case construct is not yet
        # ready to be structured, e.g., default node has a successor A and all case nodes have a successor B).
        # TestDecompiler.test_decompiling_abnormal_switch_case_within_a_loop_with_redundant_jump captures this case.
        self._matched_incomplete_switch_case_addrs: set[int] = set()

        # node_order keeps a dictionary of nodes and their order in a quasi-topological sort of the region full graph
        # (graph_with_successors). _generate_node_order() initializes this dictionary. we then update this dictionary
        # when new nodes are created. we do not populate this dictionary when working on acyclic graphs because it's
        # not used for acyclic graphs.
        self._node_order: dict[Any, int] | None = None

        self._use_multistmtexprs = use_multistmtexprs
        self._multistmtexpr_stmt_threshold = multistmtexpr_stmt_threshold
        self._analyze()

    @staticmethod
    def _assert_graph_ok(g, msg: str) -> None:
        if _DEBUG:
            if g is None:
                return
            assert (
                len(list(networkx.connected_components(networkx.Graph(g)))) <= 1
            ), f"{msg}: More than one connected component. Please report this."
            assert (
                len([nn for nn in g if g.in_degree[nn] == 0]) <= 1
            ), f"{msg}: More than one graph entrance. Please report this."

    def _analyze(self):
        # iterate until there is only one node in the region

        self._assert_graph_ok(self._region.graph, "Incorrect region graph")

        has_cycle = self._has_cycle()

        # special handling for single-node loops
        if len(self._region.graph.nodes) == 1 and has_cycle:
            self._analyze_cyclic()

        # backup the region prior to conducting a cyclic refinement because we may not be able to structure a cycle out
        # of the refined graph. in that case, we restore the original region and return.
        pre_refinement_region = None

        while len(self._region.graph.nodes) > 1:
            progressed = self._analyze_acyclic()
            if progressed and self._region.head not in self._region.graph:
                # update the head
                self._region.head = next(
                    iter(node for node in self._region.graph.nodes if node.addr == self._region.head.addr)
                )

            if has_cycle:
                progressed |= self._analyze_cyclic()
                if progressed:
                    pre_refinement_region = None
                    if self._region.head not in self._region.graph:
                        # update the loop head
                        self._region.head = next(
                            iter(node for node in self._region.graph.nodes if node.addr == self._region.head.addr)
                        )
                elif pre_refinement_region is None:
                    pre_refinement_region = self._region.copy()
                    refined = self._refine_cyclic()
                    if refined:
                        if self._region.head not in self._region.graph:
                            # update the loop head
                            self._region.head = next(
                                iter(node for node in self._region.graph.nodes if node.addr == self._region.head.addr)
                            )
                        has_cycle = self._has_cycle()
                        continue
                has_cycle = self._has_cycle()

            if not progressed:
                if self._region.cyclic_ancestor and not self._region.cyclic:
                    # we prefer directly returning this subgraph in case it can be further restructured within a loop
                    # region
                    l.debug("No progress is made on this acyclic graph with a cyclic ancestor. Give up.")
                    break

                l.debug("No progress is made. Enter last resort refinement.")
                removed_edge = self._last_resort_refinement(
                    self._region.head,
                    self._region.graph,
                    (
                        self._region.graph_with_successors
                        if self._region.graph_with_successors is not None
                        else networkx.DiGraph(self._region.graph)
                    ),
                )
                self._assert_graph_ok(self._region.graph, "Last resort refinement went wrong")
                if not removed_edge:
                    # cannot make any progress in this region. return the subgraph directly
                    break

        if len(self._region.graph.nodes) == 1:
            # successfully structured
            self.result = next(iter(self._region.graph.nodes))
        else:
            if pre_refinement_region is not None:
                # we could not make a loop after the last cycle refinement. restore the graph
                l.debug("Could not structure the cyclic graph. Restoring the region to the pre-refinement state.")
                self._region = pre_refinement_region

            self.result = None  # the actual result is in self._region.graph and self._region.graph_with_successors

    def _analyze_cyclic(self) -> bool:
        any_matches = False

        if self._node_order is None:
            self._generate_node_order()
        acyclic_graph = to_acyclic_graph(_f(self._region.graph), node_order=self._node_order)
        for node in list(GraphUtils.dfs_postorder_nodes_deterministic(acyclic_graph, self._region.head)):
            if node not in self._region.graph:
                continue
            matched = self._match_cyclic_schemas(
                node,
                self._region.head,
                self._region.graph,
                (
                    self._region.graph_with_successors
                    if self._region.graph_with_successors is not None
                    else networkx.DiGraph(self._region.graph)
                ),
            )
            l.debug("... matching cyclic schemas: %s at %r", matched, node)
            any_matches |= matched
            if matched:
                self._assert_graph_ok(self._region.graph, "Removed incorrect edges")
        return any_matches

    def _match_cyclic_schemas(self, node, head, graph, full_graph) -> bool:
        matched, loop_node, successor_node = self._match_cyclic_while(node, head, graph, full_graph)
        if matched:
            assert loop_node is not None and successor_node is not None
            # traverse this node and rewrite all conditional jumps that go outside the loop to breaks
            self._rewrite_conditional_jumps_to_breaks(loop_node.sequence_node, [successor_node.addr])
            # traverse this node and rewrite all jumps that go to the beginning of the loop to continue
            self._rewrite_jumps_to_continues(loop_node.sequence_node)
            return True

        matched, loop_node, successor_node = self._match_cyclic_dowhile(node, head, graph, full_graph)
        if matched:
            assert loop_node is not None and successor_node is not None
            # traverse this node and rewrite all conditional jumps that go outside the loop to breaks
            self._rewrite_conditional_jumps_to_breaks(loop_node.sequence_node, [successor_node.addr])
            # traverse this node and rewrite all jumps that go to the beginning of the loop to continue
            self._rewrite_jumps_to_continues(loop_node.sequence_node, loop_node=loop_node)
            return True

        if self._improve_algorithm:
            matched, loop_node, successor_node = self._match_cyclic_while_with_single_successor(
                node, head, graph, full_graph
            )
            if matched:
                assert loop_node is not None and successor_node is not None
                # traverse this node and rewrite all conditional jumps that go outside the loop to breaks
                self._rewrite_conditional_jumps_to_breaks(loop_node.sequence_node, [successor_node.addr])
                # traverse this node and rewrite all jumps that go to the beginning of the loop to continue
                self._rewrite_jumps_to_continues(loop_node.sequence_node)
                return True

        matched, loop_node, successor_node = self._match_cyclic_natural_loop(node, head, graph, full_graph)
        if matched:
            assert loop_node is not None
            if successor_node is not None:
                # traverse this node and rewrite all conditional jumps that go outside the loop to breaks
                self._rewrite_conditional_jumps_to_breaks(loop_node.sequence_node, [successor_node.addr])
            elif self._region.successors is not None and len(self._region.successors) == 1:
                # traverse this node and rewrite all conditional jumps that go outside the loop to breaks
                self._rewrite_conditional_jumps_to_breaks(
                    loop_node.sequence_node, [succ.addr for succ in self._region.successors]
                )
            # traverse this node and rewrite all jumps that go to the beginning of the loop to continue
            self._rewrite_jumps_to_continues(loop_node.sequence_node)
        return matched

    def _match_cyclic_while(
        self, node, head, graph_raw, full_graph_raw
    ) -> tuple[bool, LoopNode | None, BaseNode | None]:
        full_graph = _f(full_graph_raw)

        succs = list(full_graph_raw.successors(node))
        if len(succs) == 2:
            left, right = succs

            if full_graph_raw.has_edge(right, node) and not full_graph_raw.has_edge(left, node):
                left, right = right, left
            if left is node:
                # self loop
                # possible candidate
                head_block_idx, _, head_block = self._find_node_going_to_dst(node, left)
                if head_block is None:
                    # it happens. for example:
                    # ## Block 4058c8
                    # 00 | 0x4058c8 | if ((rcx<8> == 0x0<64>)) { Goto 0x4058ca<64> } else { Goto None }
                    # 01 | 0x4058c8 | rcx<8> = (rcx<8> - 0x1<64>)
                    # 02 | 0x4058c8 | cc_dep1<8> = Conv(8->64, Load(addr=rsi<8>, size=1, endness=Iend_LE))
                    # 03 | 0x4058c8 | cc_dep2<8> = Conv(8->64, Load(addr=rdi<8>, size=1, endness=Iend_LE))
                    # 04 | 0x4058c8 | rdi<8> = (rdi<8> + d<8>)
                    # 05 | 0x4058c8 | rsi<8> = (rsi<8> + d<8>)
                    # 06 | 0x4058c8 | if ((Conv(64->8, cc_dep1<8>) == Conv(64->8, cc_dep2<8>))) { Goto 0x4058c8<64> }
                    #   else { Goto None }
                    # 07 | 0x4058c8 | Goto(0x4058ca<64>)
                    head_block_idx, _, head_block = self._find_node_going_to_dst(node, right)

                if (
                    isinstance(head_block, MultiNode)
                    and head_block.nodes
                    and isinstance(head_block.nodes[0], Block)
                    and head_block.nodes[0].statements
                    and is_head_controlled_loop_block(head_block.nodes[0])
                ) or (
                    isinstance(head_block, Block)
                    and head_block.statements
                    and is_head_controlled_loop_block(head_block)
                ):
                    # it's a while loop if the conditional jump (or the head block) is at the beginning of node
                    loop_type = "while" if head_block_idx == 0 else "do-while"
                    # otherwise it's a do-while loop
                    if self.cond_proc.have_opposite_edge_conditions(full_graph_raw, head_block, left, right):
                        # c = !c
                        edge_cond_left = self.cond_proc.recover_edge_condition(full_graph_raw, head_block, left)
                        if head_block_idx == 0:
                            self._remove_first_statement_if_jump(head_block)
                        else:
                            remove_last_statement(head_block)
                        seq_node = SequenceNode(node.addr, nodes=[node]) if not isinstance(node, SequenceNode) else node
                        loop_node = LoopNode(loop_type, edge_cond_left, seq_node, addr=seq_node.addr)
                        self.replace_nodes(graph_raw, node, loop_node, self_loop=False, drop_refinement_marks=True)
                        self.replace_nodes(
                            full_graph_raw,
                            node,
                            loop_node,
                            self_loop=False,
                            update_node_order=True,
                            drop_refinement_marks=True,
                        )

                        # ensure the loop has only one successor: the right node
                        self._remove_edges_except(graph_raw, loop_node, right)
                        self._remove_edges_except(full_graph_raw, loop_node, right)

                        return True, loop_node, right
            elif (
                full_graph_raw.has_edge(left, node)
                and left is not head
                and full_graph_raw.in_degree[left] == 1
                and full_graph.out_degree[left] == 1
                and not full_graph_raw.has_edge(right, node)
            ):
                # possible candidate
                _, _, head_block = self._find_node_going_to_dst(node, left, condjump_only=True)
                if head_block is not None:
                    if self.cond_proc.have_opposite_edge_conditions(full_graph_raw, head_block, left, right):
                        # c = !c
                        if PhoenixStructurer._is_single_statement_block(node):
                            # the single-statement-block check is to ensure we don't execute any code before the
                            # conditional jump. this way the entire node can be dropped.
                            edge_cond_left = self.cond_proc.recover_edge_condition(full_graph_raw, head_block, left)
                            new_node = SequenceNode(node.addr, nodes=[left])
                            loop_node = LoopNode("while", edge_cond_left, new_node, addr=node.addr)

                            # on the original graph
                            self.replace_nodes(
                                graph_raw, node, loop_node, old_node_1=left, self_loop=False, drop_refinement_marks=True
                            )
                            # on the graph with successors
                            self.replace_nodes(
                                full_graph_raw,
                                node,
                                loop_node,
                                old_node_1=left,
                                self_loop=False,
                                update_node_order=True,
                            )

                            # ensure the loop has only one successor: the right node
                            self._remove_edges_except(graph_raw, loop_node, right)
                            self._remove_edges_except(full_graph_raw, loop_node, right)

                            return True, loop_node, right
                        # we generate a while-true loop instead
                        edge_cond_right = self.cond_proc.recover_edge_condition(full_graph_raw, head_block, right)
                        last_stmt = self._remove_last_statement_if_jump(head_block)
                        assert last_stmt is not None
                        cond_jump = Jump(
                            None,
                            Const(None, None, right.addr, self.project.arch.bits),
                            None,
                            ins_addr=last_stmt.tags["ins_addr"],
                        )
                        jump_node = Block(last_stmt.tags["ins_addr"], None, statements=[cond_jump])
                        cond_jump_node = ConditionNode(last_stmt.tags["ins_addr"], None, edge_cond_right, jump_node)
                        new_node = SequenceNode(node.addr, nodes=[node, cond_jump_node, left])
                        loop_node = LoopNode("while", claripy.true(), new_node, addr=node.addr)

                        # on the original graph
                        self.replace_nodes(
                            graph_raw, node, loop_node, old_node_1=left, self_loop=False, drop_refinement_marks=True
                        )
                        # on the graph with successors
                        self.replace_nodes(
                            full_graph_raw,
                            node,
                            loop_node,
                            old_node_1=left,
                            self_loop=False,
                            update_node_order=True,
                            drop_refinement_marks=True,
                        )

                        # ensure the loop has only one successor: the right node
                        self._remove_edges_except(graph_raw, loop_node, right)
                        self._remove_edges_except(full_graph_raw, loop_node, right)

                        return True, loop_node, right

                if self._improve_algorithm and full_graph.out_degree[node] == 1:
                    # while (true) { ...; if (...) break; }
                    _, _, head_block = self._find_node_going_to_dst(node, left, condjump_only=True)
                    if head_block is not None:
                        if self.cond_proc.have_opposite_edge_conditions(full_graph, head_block, left, right):
                            # c = !c
                            edge_cond_right = self.cond_proc.recover_edge_condition(full_graph, head_block, right)
                            self._remove_last_statement_if_jump(head_block)
                            cond_break = ConditionalBreakNode(node.addr, edge_cond_right, right.addr)
                            new_node = SequenceNode(node.addr, nodes=[node, cond_break, left])
                            loop_node = LoopNode("while", claripy.true(), new_node, addr=node.addr)

                            # on the original graph
                            self.replace_nodes(
                                graph_raw, node, loop_node, old_node_1=left, self_loop=False, drop_refinement_marks=True
                            )
                            # on the graph with successors
                            self.replace_nodes(
                                full_graph_raw,
                                node,
                                loop_node,
                                old_node_1=left,
                                self_loop=False,
                                update_node_order=True,
                                drop_refinement_marks=True,
                            )

                            # ensure the loop has only one successor: the right node
                            self._remove_edges_except(graph_raw, loop_node, right)
                            self._remove_edges_except(full_graph_raw, loop_node, right)

                            return True, loop_node, right

        return False, None, None

    def _match_cyclic_while_with_single_successor(
        self, node, head, graph_raw, full_graph_raw
    ) -> tuple[bool, LoopNode | None, BaseNode | None]:
        if self._region.successors:
            return False, None, None
        if node is not head:
            return False, None, None

        full_graph = full_graph_raw
        graph = graph_raw

        if not (node is head or graph.in_degree[node] == 2):
            return False, None, None

        loop_cond = None
        successor_node = None
        succ_node_is_true_node = None
        if (
            isinstance(node, SequenceNode)
            and node.nodes
            and isinstance(node.nodes[-1], ConditionNode)
            # must ensure the nodes before the condition node are empty. otherwise the condition may use variables that
            # are updated in these nodes leading up to the condition node.
            and all(not self.has_nonlabel_nonphi_statements(nn) for nn in node.nodes[:-1])
            and node.nodes[-1].true_node is not None
            and node.nodes[-1].false_node is not None
        ):
            # try both true node and false node; pick the first node with only Returns as last statements as the
            # successor.
            if self._cyclic_while_with_single_successor_must_return(node.nodes[-1].true_node):
                succ_node_is_true_node = True
                successor_node = node.nodes[-1].true_node
                loop_cond = claripy.Not(node.nodes[-1].condition)
            elif self._cyclic_while_with_single_successor_must_return(node.nodes[-1].false_node):
                succ_node_is_true_node = False
                successor_node = node.nodes[-1].false_node
                loop_cond = node.nodes[-1].condition
            else:
                loop_cond = None

        if loop_cond is None:
            return False, None, None

        node_copy = node.copy()
        # replace the last node with the intended successor node
        node_copy.nodes[-1] = (
            node_copy.nodes[-1].false_node if succ_node_is_true_node else node_copy.nodes[-1].true_node
        )
        # check if there is a cycle that starts with node and ends with node
        next_node = node
        seq_node = SequenceNode(node.addr, nodes=[node_copy])
        seen_nodes = set()
        while True:
            succs = list(full_graph.successors(next_node))
            if len(succs) != 1:
                return False, None, None
            next_node = succs[0]

            if next_node is node:
                break
            if next_node is not node and next_node in seen_nodes:
                return False, None, None

            seen_nodes.add(next_node)
            seq_node.nodes.append(next_node)

        loop_node = LoopNode("while", loop_cond, seq_node, addr=node.addr)

        # on the original graph
        for node_ in seq_node.nodes:
            if node_ is not node_copy:
                graph_raw.remove_node(node_)
        self.replace_nodes(graph_raw, node, loop_node, self_loop=False, drop_refinement_marks=True)
        graph_raw.add_edge(loop_node, successor_node)

        # on the graph with successors
        for node_ in seq_node.nodes:
            if node_ is not node_copy:
                full_graph_raw.remove_node(node_)
        self.replace_nodes(
            full_graph_raw, node, loop_node, self_loop=False, update_node_order=True, drop_refinement_marks=True
        )
        full_graph_raw.add_edge(loop_node, successor_node)

        if self._node_order is not None:
            self._node_order[loop_node] = self._node_order[node]
            self._node_order[successor_node] = self._node_order[loop_node]

        return True, loop_node, successor_node

    def _cyclic_while_with_single_successor_must_return(self, successor_node: SequenceNode) -> bool:
        try:
            last_stmts = self.cond_proc.get_last_statements(successor_node)
        except EmptyBlockNotice:
            return False
        if not last_stmts:
            return False
        return all(isinstance(stmt, Return) for stmt in last_stmts)

    def _match_cyclic_dowhile(
        self, node, head, graph_raw, full_graph_raw
    ) -> tuple[bool, LoopNode | None, BaseNode | None]:
        full_graph = _f(full_graph_raw)

        preds_raw = list(full_graph_raw.predecessors(node))
        succs_raw = list(full_graph_raw.successors(node))
        succs = list(full_graph.successors(node))

        if ((node is head and len(preds_raw) >= 1) or len(preds_raw) >= 2) and len(succs) == 1:
            succ = succs[0]
            succ_preds = list(full_graph.predecessors(succ))
            succ_succs = list(full_graph.successors(succ))
            if head is not succ and len(succ_succs) == 2 and node in succ_succs and len(succ_preds) == 1:
                succ_succs.remove(node)
                out_node = succ_succs[0]

                if (len(succs_raw) == 1 or (len(succs_raw) == 2 and out_node in succs_raw)) and full_graph.has_edge(
                    succ, node
                ):
                    # possible candidate
                    _, _, succ_block = self._find_node_going_to_dst(succ, out_node, condjump_only=True)
                    if succ_block is not None:
                        if self.cond_proc.have_opposite_edge_conditions(full_graph, succ_block, node, out_node):
                            # c = !c
                            edge_cond_succhead = self.cond_proc.recover_edge_condition(full_graph, succ_block, node)
                            self._remove_last_statement_if_jump(succ)
                            drop_succ = False

                            # absorb the entire succ block if possible
                            if (
                                self._improve_algorithm
                                and self._is_sequential_statement_block(succ)
                                and self._should_use_multistmtexprs(succ)
                            ):
                                stmts = self._build_multistatementexpr_statements(succ)
                                assert stmts is not None
                                if (
                                    stmts
                                    and sum(1 for stmt in stmts if not isinstance(stmt, Label))
                                    <= self._multistmtexpr_stmt_threshold
                                ):
                                    edge_cond_succhead = MultiStatementExpression(
                                        None,
                                        stmts,
                                        self.cond_proc.convert_claripy_bool_ast(edge_cond_succhead),
                                        ins_addr=succ.addr,
                                    )
                                drop_succ = True

                            new_node = SequenceNode(node.addr, nodes=[node] if drop_succ else [node, succ])
                            loop_node = LoopNode("do-while", edge_cond_succhead, new_node, addr=node.addr)

                            # on the original graph
                            self.replace_nodes(
                                graph_raw, node, loop_node, old_node_1=succ, self_loop=False, drop_refinement_marks=True
                            )
                            # on the graph with successors
                            self.replace_nodes(
                                full_graph_raw,
                                node,
                                loop_node,
                                old_node_1=succ,
                                self_loop=False,
                                update_node_order=True,
                                drop_refinement_marks=True,
                            )

                            return True, loop_node, out_node
