package tip.analysis

import tip.graph.ControlFlowGraph
import tip.ast._
import tip.graph.NodeOps._
import tip.ast.AstOps._
import tip.lattices._
import tip.solvers._
import tip.graph._

/**
 * Base class for the live variables analysis
 */
abstract class LiveVarsAnalysis(cfg: ControlFlowGraph[AstNode]) extends FlowSensitiveAnalysis(cfg) {

  val allVars = cfg.nodes.map {
    _.appearingIds
  }.flatten

  /**
   * The lattice for the liveness analysis
   */
  val lattice = new MapLattice(cfg.nodes, new PowersetLattice(allVars))

  def transfer(n: GNode[AstNode], s: lattice.l.Element, o: lattice.Element): lattice.l.Element = {
    val succStates = n.succ.map { x => o(x) }
    val joinState = succStates.foldLeft(lattice.l.bottom) { (lub, succ) => lattice.l.lub(lub, succ) }

    n match {
      case exit: FunExit[AstNode] => lattice.l.bottom
      case r: GRealNode[AstNode] =>
        r.data match {
          case cond: ABinaryOp => lattice.l.lub(joinState, cond.appearingIds) //This must be a guard, indeed
          case ass: AAssignStmt => ass.left match {
            case id: AIdentifier => lattice.l.lub((joinState - id), ass.right.appearingIds)
            case un: AUnaryOp => lattice.l.lub(joinState, ass.right.appearingIds)
          }
          case varr: AVarStmt => joinState -- varr.appearingIds
          case _ => joinState
        }
      case _ => joinState
    }

  }
}

/**
 * A live variables analysis which uses the simple fixpoint solver
 */
class LiveVarsAnalysisSimpleSolver(cfg: ControlFlowGraph[AstNode])
  extends LiveVarsAnalysis(cfg) with SimpleFixpointSolver with MapLatticeTransfer[GNode[AstNode]]

/**
 * A live variables analysis which uses the worklist solver
 */
class LiveVarsAnalysisWorklistSolver(cfg: ControlFlowGraph[AstNode])
  extends LiveVarsAnalysis(cfg) with WorklistFixpointSolver[GNode[AstNode]] with BackwardDependencies