// In the following, we demonstrate how to get the 
//    - Dominator Tree(DT), 
//    - Post-Dominator Tree and 
//    - Control-Dependence Graph based on the Post-Dominator Tree
// for a given method.
//
// ======== NOTE: IN CASE OF METHODS WITH MULTIPLE EXIT POINTS  ======= 
// ========       (in particular due to exceptiions) AND/OR     =======
// ========       INFINITE LOOPS THE CONTROL-DEPENDENCE GRAPH   =======
// ========       WILL CONTAIN SPURIOUS RESULTS.                =======
// ======== SEE:  A New Foundation for Control Dependence and Slicing for Modern Program Structures
// ========       ACM Transactions on Programming Languages and Systems, Vol. 29, No. 5, Article 27, Publication date: August 2007.

import org.opalj.graphs.dotToSVG
import org.opalj.io.writeAndOpen
import org.opalj.br._ ; 
import org.opalj.br.analyses._; 
import org.opalj.ai._;

implicit val p = Project(new java.io.File("OPAL/bi/target/scala-2.12/resource_managed/test/controlflow.jar"))

// Select a method // HERE, WE DELIBERATELY CHOSE METHODS WHICH CONTAIN INFINITE LOOPS (NOT UNBOUNDED ONES...)...
val cf = p.classFile(ObjectType("controlflow/InfiniteLoops")).get
// val methodNames = cf.methods.map(_.name).filterNot(_ =="<init>")
// val methodName = "multipleInfiniteLoops"
val methodNames = List(
//  "trivialInfiniteLoop",
//  "trivialNestedInfiniteLoops",
//  "regularLoopInInfiniteLoop",
//  "nestedInfiniteLoops",
//  "complexPathToInfiniteLoop",
//  "infiniteLoopWithComplexPath",
//  "complexPathToInfiniteLoopWithComplexPath",
  "multipleInfiniteLoops"
)
val aiResults = for {methodName <- methodNames} yield {
  println("processing: "+methodName)
  
  val m = cf.findMethod(methodName).head

  // Perform an intra-procedural, very lightweight abstract interpretation of the method
  // using a domain which records the CFG (RecordCFG); the most lightweight domain is
  // the `PrimitiveTACAIDomain`.
  val r = BaseAI(m,new domain.l1.DefaultDomainWithCFG(p,m))

  val bbcfg = r.domain.bbCFG
  writeAndOpen(dotToSVG(bbcfg.toDot),"BBCFG-"+methodName,".bbcfg.svg")
  
  val cfg = r.domain.cfgAsGraph
  writeAndOpen(dotToSVG(org.opalj.graphs.toDot(List(cfg))),"CFG-"+methodName,".cfg.svg")

  val allExecuted = r.domain.allExecuted
  println(allExecuted.mkString("executed: {", ", ","}"))
  println(r.domain.infiniteLoopHeaders.mkString("infinite loop headers: {", ", ","}"))
  
  // Domintator Tree
  val dt = r.domain.dominatorTree
  writeAndOpen(dt.toDot(allExecuted),"DT-"+methodName,".dt.gv")
  // (Forward) Dominance Frontiers
  val df = org.opalj.graphs.DominanceFrontiers.apply(dt,allExecuted)
  writeAndOpen(dotToSVG(df.toDot(i => i >= m.body.get.codeSize || allExecuted(i))),"DF-"+methodName,".df.svg")

  // Post Dominator Tree
  val pdt = r.domain.postDominatorTree
  writeAndOpen(dotToSVG(pdt.toDot(i => i >= m.body.get.codeSize || allExecuted(i))),"PDT-"+methodName,".pdt.svg")
  // Post Dominance Frontiers/Control Dependencies
  val cdg = r.domain.pdtBasedControlDependencies // Uses backward dominance frontiers
  // val pdf = org.opalj.graphs.DominanceFrontiers.apply(pdt,r.domain.wasExecuted)
  writeAndOpen(dotToSVG(cdg.toDot(i => i >= m.body.get.codeSize || allExecuted(i))),"PDF-"+methodName,".pdf.svg")  
    
  for (pc <- allExecuted){
    print("\n"+pc)
    var ps : List[Int] = Nil
    cdg.xIsControlDependentOn(pc)(p => ps ::= p)
    println(s"\tis control dependent on ${ps.mkString("{",", ","}")}")
    println(s"\tbelongs to the dominance frontier of ${df.df(pc).mkString("{",", ","}")} ==>(transitively) ${df.transitiveDF(pc).mkString("{",", ","}")}")
  }
  
  r
}

// Check if some method contains an infinite loop
p.allClassFiles.foreach{cf => 
  cf.methods.filter(_.body.isDefined).foreach{m =>
    val r = BaseAI(m,new domain.l1.DefaultDomainWithCFG(p,m)); 
    val infiniteLoops = r.domain.infiniteLoopHeaders
    print(if(infiniteLoops.nonEmpty) Console.RED else Console.GREEN)
    println(m.toJava("infinite loops="+infiniteLoops.mkString(", "))+Console.RESET)
  }
}