/**
 * Provides classes for working with basic blocks, and predicates for computing
 * liveness information for local variables.
 */

import javascript

/**
 * Holds if `nd` starts a new basic block.
 */
private predicate startsBB(ControlFlowNode nd) {
  (not exists(nd.getAPredecessor()) and exists(nd.getASuccessor())) or
  nd.isJoin() or
  nd.getAPredecessor().isBranch()
}

/**
 * Holds if the first node of basic block `succ` is a control flow
 * successor of the last node of basic block `bb`.
 */
private predicate succBB(BasicBlock bb, BasicBlock succ) {
  succ = bb.getLastNode().getASuccessor()
}

/**
 * Holds if the first node of basic block `bb` is a control flow
 * successor of the last node of basic block `pre`.
 */
private predicate predBB(BasicBlock bb, BasicBlock pre) {
  succBB(pre, bb)
}

/** Holds if `bb` is an entry basic block. */
private predicate entryBB(BasicBlock bb) {
  bb.getFirstNode() instanceof ControlFlowEntryNode
}

/** Holds if `bb` is an exit basic block. */
private predicate exitBB(BasicBlock bb) {
  bb.getLastNode() instanceof ControlFlowExitNode
}

private cached module Internal {
  /**
   * Holds if `succ` is a control flow successor of `nd` within the same basic block.
   */
  private predicate intraBBSucc(ControlFlowNode nd, ControlFlowNode succ) {
    succ = nd.getASuccessor() and
    not succ instanceof BasicBlock
  }

  /**
   * Holds if `nd` is the `i`th node in basic block `bb`.
   *
   * In other words, `i` is the shortest distance from a node `bb`
   * that starts a basic block to `nd` along the `intraBBSucc` relation.
   */
  cached predicate bbIndex(BasicBlock bb, ControlFlowNode nd, int i) =
    shortestDistances(startsBB/1, intraBBSucc/2)(bb, nd, i)

  cached int bbLength(BasicBlock bb) {
    result = strictcount(ControlFlowNode nd | bbIndex(bb, nd, _))
  }

  cached predicate useAt(BasicBlock bb, int i, Variable v, VarUse u) {
    v = u.getVariable() and bbIndex(bb, u, i)
  }

  cached predicate defAt(BasicBlock bb, int i, Variable v, VarDef d) {
    exists (VarRef lhs |
      lhs = d.getTarget().(BindingPattern).getABindingVarRef() and
      v = lhs.getVariable() |
      lhs = d.getTarget() and
      bbIndex(bb, d, i)
      or
      exists (PropertyPattern pp |
        lhs = pp.getValuePattern() and
        bbIndex(bb, pp, i)
      )
      or
      exists (ObjectPattern op |
        lhs = op.getRest() and
        bbIndex(bb, lhs, i)
      )
      or
      exists (ArrayPattern ap |
        lhs = ap.getAnElement() and
        bbIndex(bb, lhs, i)
      )
    )
  }

  cached predicate reachableBB(BasicBlock bb) {
    entryBB(bb) or
    exists (BasicBlock predBB | succBB(predBB, bb) | reachableBB(predBB))
  }
}
private import Internal

/** Holds if `dom` is an immediate dominator of `bb`. */
private cached predicate bbIDominates(BasicBlock dom, BasicBlock bb) =
  idominance(entryBB/1, succBB/2)(_, dom, bb)

/** Holds if `dom` is an immediate post-dominator of `bb`. */
private cached predicate bbIPostDominates(BasicBlock dom, BasicBlock bb) =
  idominance(exitBB/1, predBB/2)(_, dom, bb)

/**
 * A basic block, that is, a maximal straight-line sequence of control flow nodes
 * without branches or joins.
 *
 * At the database level, a basic block is represented by its first control flow node.
 */
class BasicBlock extends @cfg_node, Locatable {
  BasicBlock() {
    startsBB(this)
  }

  /** Gets a basic block succeeding this one. */
  BasicBlock getASuccessor() {
    succBB(this, result)
  }

  /** Gets a basic block preceding this one. */
  BasicBlock getAPredecessor() {
    result.getASuccessor() = this
  }

  /** Gets a node in this block. */
  ControlFlowNode getANode() { result = getNode(_) }

  /** Gets the node at the given position in this block. */
  ControlFlowNode getNode(int pos) {
    bbIndex(this, result, pos)
  }

  /** Gets the first node in this block. */
  ControlFlowNode getFirstNode() { result = this }

  /** Gets the last node in this block. */
  ControlFlowNode getLastNode() { result = getNode(length()-1) }

  /** Gets the length of this block. */
  int length() { result = bbLength(this) }

  /** Holds if this basic block uses variable `v` in its `i`th node `u`. */
  predicate useAt(int i, Variable v, VarUse u) {
    useAt(this, i, v, u)
  }

  /** Holds if this basic block defines variable `v` in its `i`th node `u`. */
  predicate defAt(int i, Variable v, VarDef d) {
    defAt(this, i, v, d)
  }

  /**
   * Holds if `v` is live at entry to this basic block and `u` is a use of `v`
   * witnessing the liveness.
   *
   * In other words, `u` is a use of `v` that is reachable from the
   * entry node of this basic block without going through a redefinition
   * of `v`. The use `u` may either be in this basic block, or in another
   * basic block reachable from this one.
   */
  predicate isLiveAtEntry(Variable v, VarUse u) {
    // restrict `u` to be reachable from this basic block
    u = getASuccessor*().getANode() and
    (// shortcut: if `v` is never defined, then it must be live
     isDefinedInSameContainer(v) implies
     // otherwise, do full liveness computation
     isLiveAtEntryImpl(v, u))
  }

  /**
   * Holds if `v` is live at entry to this basic block and `u` is a use of `v`
   * witnessing the liveness, where `v` is defined at least once in the enclosing
   * function or script.
   */
  private predicate isLiveAtEntryImpl(Variable v, VarUse u) {
    isLocallyLiveAtEntry(v, u)
    or
    isDefinedInSameContainer(v) and
    not this.defAt(_, v, _) and
    getASuccessor().isLiveAtEntryImpl(v, u)
  }

  /**
   * Holds if `v` is defined at least once in the function or script to which
   * this basic block belongs.
   */
  private predicate isDefinedInSameContainer(Variable v) {
    exists (VarDef def | def.getAVariable() = v and def.getContainer() = getContainer())
  }

  /**
   * Holds if `v` is a variable that is live at entry to this basic block.
   *
   * Note that this is equivalent to `bb.isLiveAtEntry(v, _)`, but may
   * be more efficient on large databases.
   */
  predicate isLiveAtEntry(Variable v) {
    isLocallyLiveAtEntry(v, _) or
    (not this.defAt(_, v, _) and getASuccessor().isLiveAtEntry(v))
  }

  /**
   * Holds if local variable `v` is live at entry to this basic block and
   * `u` is a use of `v` witnessing the liveness.
   */
  predicate localIsLiveAtEntry(LocalVariable v, VarUse u) {
    isLocallyLiveAtEntry(v, u) or
    (not this.defAt(_, v, _) and getASuccessor().localIsLiveAtEntry(v, u))
  }

  /**
   * Holds if local variable `v` is live at entry to this basic block.
   */
  predicate localIsLiveAtEntry(LocalVariable v) {
    isLocallyLiveAtEntry(v, _) or
    (not this.defAt(_, v, _) and getASuccessor().localIsLiveAtEntry(v))
  }

  /**
   * Holds if `d` is a definition of `v` that is reachable from the beginning of
   * this basic block without going through a redefinition of `v`.
   */
  predicate localMayBeOverwritten(LocalVariable v, VarDef d) {
    isLocallyOverwritten(v, d) or
    (not defAt(_, v, _) and getASuccessor().localMayBeOverwritten(v, d))
  }

  /**
   * Gets the next index after `i` in this basic block at which `v` is
   * defined or used, provided that `d` is a definition of `v` at index `i`.
   * If there are no further uses or definitions of `v` after `i`, the
   * result is the length of this basic block.
   */
  private int nextDefOrUseAfter(PurelyLocalVariable v, int i, VarDef d) {
    defAt(i, v, d) and
    result = min(int j | (defAt(j, v, _) or useAt(j, v, _) or j = length()) and j > i)
  }

  /**
   * Holds if `d` defines variable `v` at the `i`th node of this basic block, and
   * the definition is live, that is, the variable may be read after this
   * definition and before a re-definition.
   */
  predicate localLiveDefAt(PurelyLocalVariable v, int i, VarDef d) {
    exists (int j | j = nextDefOrUseAfter(v, i, d) |
      useAt(j, v, _) or
      j = length() and getASuccessor().localIsLiveAtEntry(v)
    )
  }

  /**
   * Holds if `u` is a use of `v` in this basic block, and there are
   * no definitions of `v` before it.
   */
  private predicate isLocallyLiveAtEntry(Variable v, VarUse u) {
    exists (int n | useAt(n, v, u) |
      not exists (int m | m < n | defAt(m, v, _))
    )
  }

  /**
   * Holds if `d` is a definition of `v` in this basic block, and there are
   * no other definitions of `v` before it.
   */
  private predicate isLocallyOverwritten(Variable v, VarDef d) {
    exists (int n | defAt(n, v, d) |
      not exists (int m | m < n | defAt(m, v, _))
    )
  }

  /**
   * Gets the function or script to which this basic block belongs.
   */
  StmtContainer getContainer() {
    result = getFirstNode().getContainer()
  }

  /**
   * Gets the basic block that immediately dominates this basic block.
   */
  ReachableBasicBlock getImmediateDominator() {
    bbIDominates(result, this)
  }
}

/**
 * An unreachable basic block, that is, a basic block
 * whose first node is unreachable.
 */
class UnreachableBlock extends BasicBlock {
  UnreachableBlock() { getFirstNode().isUnreachable() }
}

/**
 * An entry basic block, that is, a basic block
 * whose first node is the entry node of a statement container.
 */
class EntryBasicBlock extends BasicBlock {
  EntryBasicBlock() { entryBB(this) }
}

/**
 * A basic block that is reachable from an entry basic block.
 */
class ReachableBasicBlock extends BasicBlock {
  ReachableBasicBlock() {
    reachableBB(this)
  }

  /**
   * Holds if this basic block strictly dominates `bb`.
   */
  cached
  predicate strictlyDominates(ReachableBasicBlock bb) {
    bbIDominates+(this, bb)
  }

  /**
   * Holds if this basic block dominates `bb`.
   *
   * This predicate is reflexive: each reachable basic block dominates itself.
   */
  predicate dominates(ReachableBasicBlock bb) {
    bb = this or
    strictlyDominates(bb)
  }

  /**
   * Holds if this basic block strictly post-dominates `bb`.
   */
  cached
  predicate strictlyPostDominates(ReachableBasicBlock bb) {
    bbIPostDominates+(this, bb)
  }

  /**
   * Holds if this basic block post-dominates `bb`.
   *
   * This predicate is reflexive: each reachable basic block post-dominates itself.
   */
  predicate postDominates(ReachableBasicBlock bb) {
    bb = this or
    strictlyPostDominates(bb)
  }

}

/**
 * A reachable basic block with more than one predecessor.
 */
class ReachableJoinBlock extends ReachableBasicBlock {
  ReachableJoinBlock() { getFirstNode().isJoin() }

  /**
   * Holds if this basic block belongs to the dominance frontier of `b`, that is
   * `b` dominates a predecessor of this block, but not this block itself.
   *
   * Algorithm from Cooper et al., "A Simple, Fast Dominance Algorithm" (Figure 5),
   * who in turn attribute it to Ferrante et al., "The program dependence graph and
   * its use in optimization".
   */
  predicate inDominanceFrontierOf(ReachableBasicBlock b) {
    b = getAPredecessor() and not b = getImmediateDominator()
    or
    exists (ReachableBasicBlock prev | inDominanceFrontierOf(prev) |
      b = prev.getImmediateDominator() and
      not b = getImmediateDominator()
    )
  }
}
