/* BSD 2-Clause License - see OPAL/LICENSE for details. */
package org.opalj
package br
package cfg

import scala.reflect.ClassTag

import java.util.Arrays
import scala.collection.AbstractIterator
import scala.collection.Set as SomeSet

import org.opalj.collection.immutable.IntTrieSet
import org.opalj.collection.immutable.IntTrieSet1
import org.opalj.collection.mutable.FixedSizedHashIDMap
import org.opalj.collection.mutable.IntArrayStack
import org.opalj.graphs.DefaultMutableNode
import org.opalj.graphs.DominatorTree
import org.opalj.graphs.Node
import org.opalj.graphs.PostDominatorTree
import org.opalj.log.GlobalLogContext
import org.opalj.log.LogContext
import org.opalj.log.OPALLogger.info
import org.opalj.util.elidedAssert

/**
 * Represents the control flow graph of a method.
 *
 * To compute a `CFG` use the [[CFGFactory]].
 *
 * ==Thread-Safety==
 * This class is thread-safe; all data is effectively immutable '''after construction''' time.
 *
 * @param   code The code for which the CFG was build.
 * @param   normalReturnNode The unique exit node of the control flow graph if the
 *          method returns normally. If the method always throws an exception, this
 *          node will not have any predecessors.
 * @param   abnormalReturnNode The unique exit node of the control flow graph if the
 *          method returns abnormally (throws an exception). If the method is guaranteed
 *          to never throw an exception, this node will not have any predecessors.
 * @param   catchNodes List of all catch nodes. (Usually, we have one [[CatchNode]] per
 *          [[org.opalj.br.ExceptionHandler]], but if an exception handler does not catch
 *          anything, no [[CatchNode]] is created.)
 * @param   basicBlocks An implicit map between a program counter and its associated
 *          [[BasicBlock]]; it may be a sparse array!
 *
 * @author Erich Wittenbeck
 * @author Michael Eichberg
 */
case class CFG[I <: AnyRef, C <: CodeSequence[I]](
    code:                    C,
    normalReturnNode:        ExitNode,
    abnormalReturnNode:      ExitNode,
    catchNodes:              Seq[CatchNode],
    private val basicBlocks: Array[BasicBlock]
) { cfg =>

    if (CFG.Validate) {
        val allBBs = basicBlocks.filter(_ != null)
        val allBBsSet = allBBs.toSet
        // 1. Check that each basic block has a lower start pc than the end pc
        //    i.e., startPC <= endPC.
        check(
            allBBs.forall(bb => bb.startPC <= bb.endPC),
            allBBs.filter(bb => bb.startPC > bb.endPC).mkString
        )

        // 2. Check that each pc belonging to a basic block (bb) actually points to the respective bb
        //    i.e., pc in basicBlock : bb => basicBlock(pc) == bb.
        check(
            allBBsSet.forall { bb =>
                (bb.startPC to bb.endPC).forall { pc => (basicBlocks(pc) eq null) || (basicBlocks(pc) eq bb) }
            },
            basicBlocks.zipWithIndex.filter(_._1 != null).map(bb =>
                s"${bb._2}:${bb._1}#${System.identityHashCode(bb._1).toHexString}"
            ).mkString("basic blocks mapping broken:\n\t", ",\n\t", "\n")
        )

        // 3. Check that the CFG is self-consistent; i.e., that no node references a node
        //    that does not occur in the BB.
        check(
            allBBsSet.forall { bb =>
                bb.successors.forall { successorBB =>
                    (successorBB.isBasicBlock && {
                        val succBB = successorBB.asBasicBlock
                        (basicBlocks(succBB.startPC) eq succBB) && (basicBlocks(succBB.endPC) eq succBB)
                    }) ||
                    (successorBB.isCatchNode && catchNodes.contains(successorBB.asCatchNode)) ||
                    successorBB.isExitNode
                }
            },
            allBBs.map(bb =>
                bb.toString + " => " + bb.successors.mkString(", ")
            ).mkString("unexpected successors:\n\t", "\n\t", "")
        )
        check(
            allBBsSet.forall { bb =>
                bb.predecessors.forall { predecessorBB =>
                    (
                        predecessorBB.isBasicBlock && {
                            val predBB = predecessorBB.asBasicBlock
                            (basicBlocks(predBB.startPC) eq predBB) && (basicBlocks(predBB.endPC) eq predBB)
                        }
                    ) ||
                    (predecessorBB.isCatchNode && catchNodes.contains(predecessorBB.asCatchNode))
                }
            },
            basicBlocks.zipWithIndex.filter(_._1 != null).map(_.swap).map(bb =>
                s"${bb._1}:${bb._2.toString} predecessors: ${bb._2.predecessors.mkString(", ")}"
            ).mkString("unexpected predecessors:\n\t", "\n\t", s"\ncode:$code")
        )

        // 4.  Check that all catch nodes referred to by the basic blocks are listed in the
        //     sequence of catch nodes
        check(
            allBBs.filter(bb => bb.successors.exists { _.isCatchNode }).flatMap(bb =>
                bb.successors.collect { case cn: CatchNode => cn }
            ).forall(catchBB => catchNodes.contains(catchBB)),
            catchNodes.mkString("the set of catch nodes {", ", ", "} is incomplete:\n") +
                allBBs.collect {
                    case bb if bb.successors.exists(succBB => succBB.isCatchNode && !catchNodes.contains(succBB)) =>
                        s"$bb => ${bb.successors.collect { case cn: CatchNode => cn }.mkString(", ")}"
                }.mkString("\n")
        )

        // 5.   Check that predecessors and successors are consistent.
        check(
            allBBsSet.forall(bb => bb.successors.forall { succBB => succBB.predecessors.contains(bb) }),
            "successors and predecessors are inconsistent; e.g., " +
                allBBsSet.find(bb => !bb.successors.forall { succBB => succBB.predecessors.contains(bb) }).map(bb =>
                    bb.successors.find(succBB => !succBB.predecessors.contains(bb)).map(succBB =>
                        s"$succBB is a successor of $bb, but does not list it as a predecessor"
                    ).get
                ).get
        )
        check(
            allBBsSet.forall(bb => bb.predecessors.forall { predBB => predBB.successors.contains(bb) }),
            "predecessors and successors are inconsistent; e.g., " +
                allBBsSet.find(bb => !bb.predecessors.forall { predBB => predBB.successors.contains(bb) }).map(bb =>
                    bb.predecessors.find(predBB => !predBB.successors.contains(bb)).map(predBB =>
                        s"$predBB is a predecessor of $bb, but does not list it as a successor"
                    ).get
                ).get
        )
    }

    /**
     * Computes the maximum fixed point solution for forward data-flow analyses.
     *
     * @param seed The initial facts associated with the first instruction (pc = 0).
     *
     * @param t The transfer function which implements the analysis:
     *        `(Facts, I, PC, CFG.SuccessorId) => Facts`.
     *        The parameters are: 1. the current set of facts, 2. the current instruction,
     *        3. the program counter of the current instruction and 4. the id of the successor.
     *
     * @param join The operation (typically a set intersection or set union) that is
     *        executed to join the results of the predecessors of a specific instruction.
     *        '''It is required that join returns the left (first) set as is if the set of facts
     *        didn't change.'''
     *        I.e., even if the left and right sets contain the same values and are
     *       `equal` (`==`) it is necessary to return the left set.
     */
    final def performForwardDataFlowAnalysis[Facts >: Null <: AnyRef: ClassTag](
        seed: Facts,
        t:    (Facts, I, PC, CFG.SuccessorId) => Facts,
        join: (Facts, Facts) => Facts
    ): (Array[Facts], /*normal return*/ Facts, /*abnormal return*/ Facts) = {

        implicit val logContext: LogContext = GlobalLogContext

        val instructions = code.instructions
        val codeSize = instructions.length

        val entryFacts = new Array[Facts](codeSize) // the facts before instruction evaluation
        entryFacts(0) = seed
        var normalReturnFacts: Facts = null
        var abnormalReturnFacts: Facts = null

        val workList = new IntArrayStack(Math.min(codeSize, 10))
        workList.push(0)

        while (workList.nonEmpty) {
            val pc = workList.pop()
            val instruction = instructions(pc)
            val facts = entryFacts(pc)

            foreachLogicalSuccessor(pc) {
                case CFG.NormalReturnId =>
                    val newFactsNoException = t(facts, instruction, pc, CFG.NormalReturnId)
                    normalReturnFacts =
                        if (normalReturnFacts == null) {
                            newFactsNoException
                        } else {
                            join(normalReturnFacts, newFactsNoException)
                        }

                case CFG.AbnormalReturnId =>
                    val newFactsException = t(facts, instruction, pc, CFG.AbnormalReturnId)
                    abnormalReturnFacts =
                        if (abnormalReturnFacts == null) {
                            newFactsException
                        } else {
                            join(abnormalReturnFacts, newFactsException)
                        }

                case succId =>
                    val newFacts = t(facts, instruction, pc, succId)
                    val effectiveSuccPC = if (succId < 0) -succId else succId
                    val succPCFacts = entryFacts(effectiveSuccPC)
                    if (succPCFacts == null) {
                        if (CFG.TraceDFSolver) {
                            info("progress - df solver", s"[initial] $pc -> $succId: $newFacts")
                        }
                        entryFacts(effectiveSuccPC) = newFacts
                        workList += effectiveSuccPC
                    } else {
                        val newSuccPCFacts = join(succPCFacts, newFacts)
                        if (newSuccPCFacts ne succPCFacts) {
                            if (CFG.TraceDFSolver) {
                                info("progress - df solver", s"[update] $pc -> $succId: $succPCFacts -> $newSuccPCFacts")
                            }
                            entryFacts(effectiveSuccPC) = newSuccPCFacts
                            workList += effectiveSuccPC
                        } else {
                            if (CFG.TraceDFSolver) {
                                info(
                                    "progress - df solver",
                                    s"[no update] $pc -> $succId: $succPCFacts -> $newSuccPCFacts"
                                )
                            }
                        }
                    }
            }
        }

        (entryFacts, normalReturnFacts, abnormalReturnFacts)
    }

    /**
     * Computes the maximum fixed point solution for backward data-flow analyses.
     *
     * @param seed The initial facts associated with instructions which lead to (ab)normal
     *        returns.
     *
     * @param t The transfer function which implements the analysis:
     *        `(Facts, I, PC, CFG.PredecessorId) => Facts`.
     *        The parameters are: 1. the current set of facts, 2. the current instruction,
     *        3. the program counter of the current instruction and 4. the id of the predecessor.
     *
     * @param join The operation (typically a set intersection or set union) that is
     *        executed to join the results of the successors of a specific instruction.
     *        '''It is required that join returns the left (first) set as is if the set of facts
     *        didn't change.'''
     *        I.e., even if the left and right sets contain the same values and are
     *       `equal` (`==`) it is necessary to return the left set.
     *
     * @note   No facts will be derived for stmts that are not reachable from an
     *         exit node; e.g., due to an infinite loop.
     *         That is, the returned array may contain `null` values and in an
     *         extreme case will only contain null values!
     */
    final def performBackwardDataFlowAnalysis[Facts >: Null <: AnyRef: ClassTag](
        seed: Facts,
        t:    (Facts, I, PC, CFG.PredecessorId) => Facts,
        join: (Facts, Facts) => Facts
    ): (Array[Facts], /*init*/ Facts) = {

        implicit val logContext: LogContext = GlobalLogContext

        val instructions = code.instructions
        val codeSize = instructions.length

        val exitFacts = new Array[Facts](codeSize) // stores the facts after instruction evaluation
        val workList = new IntArrayStack(Math.min(codeSize, 10))
        normalReturnNode.predecessors.foreach { predBB =>
            val returnPC = predBB.asBasicBlock.endPC
            exitFacts(returnPC) = seed
            workList.push(returnPC)
        }
        abnormalReturnNode.predecessors.foreach { predBB =>
            val stmtPC = predBB.asBasicBlock.endPC
            exitFacts(stmtPC) = seed
            workList.push(stmtPC)
        }

        var initFacts: Facts = null

        def handleTransition(pc: PC, predId: Int): Unit = {
            val instruction = instructions(pc)
            val facts = exitFacts(pc)
            val newFacts = t(facts, instruction, pc, predId)

            if (predId >= 0) {
                val predPCFacts = exitFacts(predId)
                if (predPCFacts == null) {
                    if (CFG.TraceDFSolver) {
                        info("progress - df solver", s"[initial] $pc -> $predId: $newFacts")
                    }
                    exitFacts(predId) = newFacts
                    workList += predId
                } else {
                    val newPredPCFacts = join(predPCFacts, newFacts)
                    if (newPredPCFacts ne predPCFacts) {
                        if (CFG.TraceDFSolver) {
                            info(
                                "progress - df solver",
                                s"[update] $pc -> $predId: $predPCFacts -> $newPredPCFacts"
                            )
                        }
                        exitFacts(predId) = newPredPCFacts
                        workList += predId
                    } else {
                        if (CFG.TraceDFSolver) {
                            info(
                                "progress - df solver",
                                s"[no update] $pc -> $predId: $predPCFacts -> $newPredPCFacts"
                            )
                        }
                    }
                }
            } else {
                if (initFacts == null) {
                    if (CFG.TraceDFSolver) {
                        info("progress - df solver", s"[initial] $pc -> -1: $newFacts")
                    }
                    initFacts = newFacts
                } else {
                    val newInitFacts = join(initFacts, newFacts)
                    if (newInitFacts ne initFacts) {
                        if (CFG.TraceDFSolver) {
                            info(
                                "progress - df solver",
                                s"[update] $pc -> -1: $initFacts -> $newInitFacts"
                            )
                        }
                        initFacts = newFacts
                    } else {
                        if (CFG.TraceDFSolver) {
                            info(
                                "progress - df solver",
                                s"[no update] $pc -> -1: $initFacts -> $newFacts"
                            )
                        }
                    }
                }
            }
        }

        while (workList.nonEmpty) {
            val pc = workList.pop()
            foreachPredecessor(pc) { predPC => handleTransition(pc, predPC) }
            if (pc == 0) handleTransition(pc, -1)
        }

        (exitFacts, initFacts)
    }

    /**
     * The basic block associated with the very first instruction.
     */
    final def startBlock: BasicBlock = basicBlocks(0)

    /**
     * Returns the basic block to which the instruction with the given `pc` belongs.
     *
     * @param pc A valid pc.
     * @return The basic block associated with the given `pc`. If the `pc` is not valid,
     *         `null` is returned or an index out of bounds exception is thrown.
     */
    final def bb(pc: Int): BasicBlock = basicBlocks(pc)

    /**
     * Returns the set of all reachable [[CFGNode]]s of the control flow graph.
     */
    lazy val reachableBBs: SomeSet[CFGNode] = basicBlocks(0).reachable(reflexive = true)

    /**
     * Iterates over the set of all [[BasicBlock]]s. (I.e., the exit and catch nodes are
     * not returned.) Always returns the basic block containing the first instruction first.
     */
    def allBBs: Iterator[BasicBlock] = {
        new AbstractIterator[BasicBlock] {

            private var currentBBPC = 0

            def hasNext: Boolean = currentBBPC < basicBlocks.length

            def next(): BasicBlock = {
                val basicBlocks = cfg.basicBlocks
                val current = basicBlocks(currentBBPC)
                currentBBPC = current.endPC + 1
                // jump to the end and check if the instruction directly following this bb
                // actually belongs to a basic block
                val maxPC = basicBlocks.length
                while (currentBBPC < maxPC && (basicBlocks(currentBBPC) eq null)) {
                    currentBBPC += 1
                }
                current
            }
        }
    }

    def allNodes: Iterator[CFGNode] = {
        allBBs ++ catchNodes.iterator ++ Iterator(normalReturnNode, abnormalReturnNode)
    }

    /**
     * Returns all direct runtime successors of the instruction with the given pc.
     *
     * If the returned set is empty, then the instruction is either a return instruction or an
     * instruction that always causes an exception to be thrown that is not handled by
     * a handler of the respective method.
     *
     * @note   If possible, the function `foreachSuccessor` should be used as it does not have
     *         to create comparatively expensive intermediate data structures.
     *
     * @param pc A valid pc of an instruction of the code block from which this cfg was derived.
     */
    def successors(pc: Int): IntTrieSet = {
        val bb = this.bb(pc)
        if (bb.endPC > pc) {
            // it must be - w.r.t. the code array - the next instruction
            IntTrieSet1(code.pcOfNextInstruction(pc))
        } else {
            // the set of successor can be (at the same time) a RegularBB or an ExitNode
            var successorPCs = IntTrieSet.empty
            bb.successors foreach {
                case succ: BasicBlock => successorPCs += succ.startPC
                case cb: CatchNode    => successorPCs += cb.handlerPC
                case _                =>
            }
            successorPCs
        }
    }

    /**
     * Iterates over the direct successors of the instruction with the given pc and calls the given
     * function `f` for each successor. `f` is guaranteed to be called only once for each successor
     * instruction. (E.g., relevant in case of a switch where multiple cases are handled in the
     * same way.)
     */
    def foreachSuccessor(pc: Int)(f: PC => Unit): Unit = {
        val bb = this.bb(pc)
        if (bb.endPC > pc) {
            // it must be - w.r.t. the code array - the next instruction
            f(code.pcOfNextInstruction(pc))
        } else {
            // the set of successors can be (at the same time) a RegularBB or an ExitNode
            var visited = IntTrieSet.empty
            bb.successors foreach { succ =>
                val nextPC =
                    if (succ.isBasicBlock) succ.asBasicBlock.startPC
                    else if (succ.isCatchNode) succ.asCatchNode.handlerPC
                    else -1
                if (nextPC != -1 && !visited.contains(nextPC)) {
                    visited += nextPC
                    f(nextPC)
                }
                // else if (bb.isExitNode)... is not relevant
            }
        }
    }

    /**
     * Iterates over the direct successors of the instruction with the given pc and calls the given
     * function `f` for each successor. `f` is guaranteed to be called only once for each successor
     * instruction. (E.g., relevant in case of a switch where multiple cases are handled in the
     * same way.)
     * The value passed to f will either be:
     *  - the pc of an instruction.
     *  - the value `CFG.AbnormalReturnId` (`Int.MinValue`) in case the evaluation of the
     *    instruction with the given pc throws an exception that leads to an abnormal return.
     *  - the value `CFG.NormalReturnId` (`Int.MaxValue`) in case the evaluation of the
     *    (return) instruction with the given `pc` leads to a normal return.
     *  - `-(successorPC)` if the evaluation leads to an exception that is caught and where the
     *    first instruction of the handler has the given `successorPC`.
     */
    def foreachLogicalSuccessor(pc: Int)(f: Int => Unit): Unit = {
        val bb = this.bb(pc)
        if (bb.endPC > pc) {
            // it must be - w.r.t. the code array - the next instruction
            f(code.pcOfNextInstruction(pc))
        } else {
            // The set of successors can be (at the same time) a RegularBB, a CatchBB or an ExitNode
            var visited = IntTrieSet.empty
            bb.successors foreach {
                case succ: BasicBlock =>
                    val nextPC = succ.startPC
                    if (!visited.contains(nextPC)) {
                        visited += nextPC
                        f(nextPC)
                    }
                case cn: CatchNode =>
                    val nextPC = cn.handlerPC
                    if (!visited.contains(nextPC)) {
                        visited += nextPC
                        f(-nextPC)
                    }
                case en: ExitNode =>
                    f(if (en.normalReturn) CFG.NormalReturnId else CFG.AbnormalReturnId)
            }
        }
    }

    def predecessors(pc: Int): IntTrieSet = {
        if (pc == 0)
            return IntTrieSet.empty;

        val bb = this.bb(pc)
        if (bb.startPC == pc) {
            var predecessorPCs = IntTrieSet.empty
            bb.predecessors foreach {
                case pred: BasicBlock =>
                    predecessorPCs += pred.endPC
                case cn: CatchNode =>
                    cn.predecessors.foreach { pred => predecessorPCs += pred.asBasicBlock.endPC }
            }
            predecessorPCs
        } else {
            IntTrieSet1(code.pcOfPreviousInstruction(pc))
        }
    }

    def foreachPredecessor(pc: Int)(f: Int => Unit): Unit = {
        if (pc == 0)
            return;

        val bb = this.bb(pc)
        if (bb.startPC == pc) {
            var visited = IntTrieSet.empty
            bb.predecessors foreach { pred =>
                if (pred.isBasicBlock) {
                    f(pred.asBasicBlock.endPC)
                } else if (pred.isCatchNode) {
                    pred.asCatchNode.predecessors foreach { predBB =>
                        val nextPC = predBB.asBasicBlock.endPC
                        if (!visited.contains(nextPC)) {
                            visited += nextPC
                            f(nextPC)
                        }
                    }
                }
            }
        } else {
            f(code.pcOfPreviousInstruction(pc))
        }
    }

    /**
     * @return Returns the dominator tree of this CFG.
     *
     * @see [[DominatorTree.apply]]
     */
    lazy val dominatorTree: DominatorTree = {
        DominatorTree(
            0,
            basicBlocks.head.predecessors.nonEmpty,
            foreachSuccessor,
            foreachPredecessor,
            basicBlocks.last.endPC
        )
    }

    /**
     * @return Returns the post dominator tree of this CFG.
     *
     * @see [[PostDominatorTree.apply]]
     */
    lazy val postDominatorTree: PostDominatorTree = {
        val exitNodes = (normalReturnNode.predecessors ++ abnormalReturnNode.predecessors).map(_.endPC)

        PostDominatorTree(
            if (exitNodes.size == 1) exitNodes.headOption else None,
            exitNodes.contains,
            IntTrieSet.empty,
            exitNodes.foreach,
            foreachSuccessor,
            foreachPredecessor,
            basicBlocks.last.endPC
        )
    }

    /**
     * Creates a new CFG where the boundaries of the basic blocks are updated given the `pcToIndex`
     * mapping. The assumption is made that the indexes are continuous.
     * If the first index (i.e., `pcToIndex(0)` is not 0, then a new basic block for the indexes
     * in {0,pcToIndex(0)} is created if necessary.
     *
     * @param  lastIndex The index of the last instruction of the underlying (non-empty) code array.
     *         I.e., if the instruction array contains one instruction then the `lastIndex` has
     *         to be `0`.
     * @param  singletonBBsExpander Function called for each basic block which encompasses a single
     *         instruction to expand the BB to encompass more instructions. This supports the
     *         case where an instruction was transformed in a way that resulted in multiple
     *         instructions/statements, but which all belong to the same basic block.
     *         ''This situation cannot be handled using pcToIndex.''
     *         This information is used to ensure that if a basic block, which currently just
     *         encompasses a single instruction, will encompass the new and the old instruction
     *         afterward.
     *         The returned value will be used as the `endIndex.`
     *         `endIndex = singletonBBsExpander(pcToIndex(pc of singleton bb))`
     *         Hence, the function is given the mapped index has to return that value if the index
     *         does not belong to the expanded instruction.
     */
    def mapPCsToIndexes[NewI <: AnyRef, NewC <: CodeSequence[NewI]](
        newCode:              NewC,
        pcToIndex:            Array[Int /*PC*/ ],
        singletonBBsExpander: Int /*PC*/ => Int,
        lastIndex:            Int
    ): CFG[NewI, NewC] = {

        /*
        // [USED FOR DEBUGGING PURPOSES] *********************************************************
        println(
            basicBlocks.
                filter(_ != null).
                toSet.
                map((bb: BasicBlock) => bb.toString + " => " + bb.successors.mkString(", ")).
                mkString("Successors:\n", "\n", "\n")
        )
        println(
            basicBlocks.
                filter(_ != null).
                toSet.
                map((bb: BasicBlock) => bb.predecessors.mkString(", ") + " => " + bb.toString).
                mkString("Predecessors:\n", "\n", "\n")
        )
        println(catchNodes.mkString("CatchNodes:", ",", "\n"))
        println(pcToIndex.zipWithIndex.map(_.swap).mkString("Mapping:", ",", "\n"))
        //
        // ********************************************************* [USED FOR DEBUGGING PURPOSES]
         */

        val bbsLength = basicBlocks.length
        // Note, catch node ids have values in the range [-3-number of catch nodes,-3].
        // Furthermore, we may have "dead" exception handlers and therefore the number
        // of catch nodes does not necessarily reflect the smallest catch node id.
        val leastCatchNodeId = if (catchNodes.isEmpty) 0 else catchNodes.iterator.map(_.nodeId).min
        val bbMapping = FixedSizedHashIDMap[CFGNode, CFGNode](
            minValue = Math.min(-2 /*the exit nodes*/, leastCatchNodeId),
            maxValue = code.instructions.length
        )

        val newBasicBlocks = new Array[BasicBlock](lastIndex + 1)
        val newBasicBlocksArray = newBasicBlocks.asInstanceOf[Array[Object]]
        val requiresNewStartBlock = pcToIndex(0) > 0

        var lastNewBB: BasicBlock = null
        if (requiresNewStartBlock) {
            val endIndex = pcToIndex(0) - 1
            // we have added instructions at the beginning which belong to a new start bb
            lastNewBB = new BasicBlock(startPC = 0, _endPC = endIndex)
            Arrays.fill(newBasicBlocksArray, 0, endIndex + 1, lastNewBB)
        }
        var startPC = 0
        while {
            val oldBB = basicBlocks(startPC)
            val startIndex = pcToIndex(startPC)
            val endIndex = {
                val initialCandidate = pcToIndex(oldBB.endPC)
                val endIndexCandidate =
                    if (initialCandidate == -1) { // There may be dead instructions
                        pcToIndex(
                            ((oldBB.endPC - 1) to oldBB.startPC by -1).find(pcToIndex(_) > -0).getOrElse(0)
                        )
                    } else initialCandidate
                if (startIndex == endIndexCandidate) {
                    singletonBBsExpander(startIndex)
                } else {
                    endIndexCandidate
                }
            }
            lastNewBB = new BasicBlock(startIndex, endIndex)
            bbMapping.put(oldBB, lastNewBB)
            Arrays.fill(newBasicBlocksArray, startIndex, endIndex + 1, lastNewBB)
            // let's advance startPC to the next instruction which is live (which has a BB)
            startPC = oldBB.endPC + 1
            var tempBB: BasicBlock = null
            while (startPC < bbsLength && {
                       tempBB = basicBlocks(startPC)
                       (tempBB eq null) || pcToIndex(tempBB.startPC) < 0
                   }
            ) {
                elidedAssert(tempBB ne oldBB)
                // This (index < 0) handles the case where the initial CFG was created using
                // a simple algorithm that actually resulted in a CFG with detached basic blocks;
                // we now kill these basic blocks by jumping over them!
                // NOTE: This is indicative of dead code in the bytecode in the first place!
                if (tempBB ne null) {
                    startPC = tempBB.endPC
                }
                startPC += 1
            }

            startPC < bbsLength
        } do ()

        if (requiresNewStartBlock) {
            val firstBB = newBasicBlocks(0)
            val secondBB = newBasicBlocks(pcToIndex(0))
            firstBB.addSuccessor(secondBB)
            secondBB.addPredecessor(firstBB)
        }

        // add the catch nodes
        val codeSize = code.instructions.length
        catchNodes foreach { cn =>
            val newCN = cn.copy(
                startPC = pcToIndex(cn.startPC),
                endPC = if (cn.endPC == codeSize) lastIndex + 1 else pcToIndex(cn.endPC),
                handlerPC = pcToIndex(cn.handlerPC)
            )
            bbMapping.put(cn, newCN)
        }

        val newNormalReturnNode = new ExitNode(normalReturn = true)
        bbMapping.put(normalReturnNode, newNormalReturnNode)
        val newAbnormalReturnNode = new ExitNode(normalReturn = false)
        bbMapping.put(abnormalReturnNode, newAbnormalReturnNode)

        // rewire the graph
        bbMapping iterate { (oldBB, newBB) =>
            oldBB.successors foreach { oldSuccBB =>
                val newSuccBB = bbMapping(oldSuccBB)
                elidedAssert(newSuccBB ne null, s"no mapping for $oldSuccBB")
                newBB.addSuccessor(newSuccBB)
                // Instead of iterating over the predecessors, we just iterate over
                // the successors; this way, we only include the nodes that are
                // live; nodes that; e.g., are attached to the exit node but for
                // which there is no path to reach them at all are dropped!
                newSuccBB.addPredecessor(newBB)
            }
        }

        val newCatchNodes = catchNodes.map(bbMapping(_).asInstanceOf[CatchNode])
        elidedAssert(newCatchNodes.forall { _ ne null })

        // let's see if we can merge the first two basic blocks
        if (requiresNewStartBlock && basicBlocks(0).predecessors.isEmpty) {
            val firstBB = newBasicBlocks(0)
            val secondBB = firstBB.successors.head.asBasicBlock
            val newFirstBB = secondBB.copy(startPC = 0, predecessors = Set.empty)
            newFirstBB.successors.foreach(succBB => succBB.updatePredecessor(secondBB, newFirstBB))
            Arrays.fill(newBasicBlocksArray, 0, secondBB._endPC + 1 /* (exclusive)*/, newFirstBB)
        }

        CFG[NewI, NewC](newCode, newNormalReturnNode, newAbnormalReturnNode, newCatchNodes, newBasicBlocks)
    }

    // ---------------------------------------------------------------------------------------------
    //
    // Visualization & Debugging
    //
    // ---------------------------------------------------------------------------------------------

    override def toString: String = {
        //        code:                    Code,
        //        normalReturnNode:        ExitNode,
        //        abnormalReturnNode:      ExitNode,
        //        catchNodes:              Seq[CatchNode],
        //        private val basicBlocks: Array[BasicBlock]

        val cfgNodes: Set[CFGNode] =
            basicBlocks.filter(_ ne null).toSet[CFGNode] ++
                catchNodes +
                normalReturnNode +
                abnormalReturnNode

        val bbIds: Map[CFGNode, Int] = cfgNodes.zipWithIndex.toMap

        bbIds.map { bbId =>
            val (bb, id) = bbId
            if (bb.isExitNode) {
                s"BB_${id.toHexString}: $bb"
            } else {
                bb.successors.map(succBB =>
                    "BB_" + bbIds(succBB).toHexString
                ).mkString(s"BB_${id.toHexString}: $bb -> {", ",", "}")
            }
        }.toList.sorted.mkString("CFG(\n\t", "\n\t", "\n)")
    }

    def toDot: String = {
        val rootNodes = Set(startBlock) ++ catchNodes
        org.opalj.graphs.toDot(rootNodes)
    }

    /**
     * @return The pair:
     *         `('''Node for the start BB''', '''all Nodes (incl. the node for the start BB)''')`
     */
    def toDot(
        f:                      BasicBlock => String,
        includeAbnormalReturns: Boolean = true
    ): (Node, Iterable[Node]) = {
        // 1. create a node foreach cfg node
        val bbsIterator = allBBs
        val startBB = bbsIterator.next()
        val startNodeVisualProperties = Map("fillcolor" -> "green", "style" -> "filled", "shape" -> "box")
        val startBBNode = new DefaultMutableNode(f(startBB), theVisualProperties = startNodeVisualProperties)
        var cfgNodeToGNodes: Map[CFGNode, DefaultMutableNode[String]] = Map(startBB -> startBBNode)
        cfgNodeToGNodes ++= bbsIterator.map(bb => (bb, new DefaultMutableNode(f(bb))))
        cfgNodeToGNodes ++= catchNodes.map(cn => (cn, new DefaultMutableNode(cn.toString)))
        cfgNodeToGNodes += (
            abnormalReturnNode -> {
                if (includeAbnormalReturns)
                    new DefaultMutableNode("abnormal return", theVisualProperties = abnormalReturnNode.visualProperties)
                else
                    null
            }
        )
        cfgNodeToGNodes += (
            normalReturnNode ->
                new DefaultMutableNode("return", theVisualProperties = normalReturnNode.visualProperties)
        )

        // 2. reconnect nodes
        cfgNodeToGNodes foreach { cfgNodeToGNode =>
            val (cfgNode, gNode) = cfgNodeToGNode
            if (gNode != null)
                cfgNode.successors foreach { cfgNode =>
                    val targetGNode = cfgNodeToGNodes(cfgNode)
                    if (targetGNode != null) gNode.addChild(targetGNode)
                }
        }

        val nodes = cfgNodeToGNodes.values
        (startBBNode, nodes)
    }
}

object CFG {

    final val NormalReturnId = Int.MaxValue
    final val AbnormalReturnId = Int.MinValue

    /**
     * Identifies the successor of an instruction.
     * The id is either:
     *  - `CFG.NormalReturnId` (`== Int.MaxValue`) if the successor is the unique exit
     *           node representing normal returns.
     *  - `CFG.AbnormalReturnId` (`== Int.MinValue`) if the successor is the unique exit
     *           node representing abnormal returns (i.e., an uncaught exception will be thrown
     *           by the instruction).
     *  - [-65535,-1] to identify the catch handler that handles the exception thrown
     *           by the current instruction. The pc of the first instruction of the catch handler
     *           is (`- successorId`).
     *  - the (valid) pc of the next instruction (the normal case.)
     */
    final type SuccessorId = Int

    /**
     * Identifies the predecessor of an instruction.
     *  - -1 if the current instruction is the first instruction (`pc`/`index` = `0`)
     *  - a regular pc.
     */
    final type PredecessorId = Int

    final val ValidateKey = "org.opalj.br.cfg.CFG.Validate"

    private var validate: Boolean = {
        val initialValidate = BaseConfig.getBoolean(ValidateKey)
        updateValidate(initialValidate)
        initialValidate
    }

    // We think of it as a runtime constant (which can be changed for testing purposes).
    def Validate: Boolean = validate

    def updateValidate(newValidate: Boolean): Unit = {
        implicit val logContext: GlobalLogContext.type = GlobalLogContext
        validate =
            if (newValidate) {
                info("OPAL", s"$ValidateKey: validation on")
                true
            } else {
                info("OPAL", s"$ValidateKey: validation off")
                false
            }
    }

    final val TraceDFSolverKey = "org.opalj.br.cfg.CFG.DF.Solver.Trace"

    final val TraceDFSolver: Boolean = {
        val traceDFSolver = BaseConfig.getBoolean(TraceDFSolverKey)
        info("OPAL", s"$TraceDFSolverKey: $traceDFSolver")(using GlobalLogContext)
        traceDFSolver
    }
}