// In the following, we demonstrate how to get the 
//    - Dominator Tree(DT), 
//    - Post-Dominator Tree and 
//    - Control-Dependence Graph 
// for a given method.
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.11/resource_managed/test/controlflow.jar"))

// Select a method // HERE, WE DELIBERATELY CHOOSE A METHOD WHICH CONTAINS AN INFINITE LOOP (NOT AN UNBOUNDED ONE...); i.e., 
val cf = p.classFile(ObjectType("controlflow/InfiniteLoops")).get
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(bbcfg.toDot,"BBCFG-"+methodName,".bbcfg.gv")
  
  val cfg = r.domain.cfgAsGraph
  writeAndOpen(org.opalj.graphs.toDot(List(cfg)),"CFG-"+methodName,".cfg.gv")

  // Domintator Tree
  val dt = r.domain.dominatorTree
  writeAndOpen(dt.toDot(m.body.get.instructions(_) != null),"DT-"+methodName,".dt.gv")

  // (Forward) Dominance Frontiers
  val df = org.opalj.graphs.DominanceFrontiers.apply(dt,r.domain.wasExecuted)
  writeAndOpen(df.toDot(i => i >= m.body.get.codeSize || m.body.get.instructions(i) != null),"DF-"+methodName,".df.gv")

  // Post Dominator Tree
  val pdt = r.domain.postDominatorTree
  writeAndOpen(pdt.toDot(i => i >= m.body.get.codeSize || m.body.get.instructions(i) != null),"PDT-"+methodName,".pdt.gv")
  
  r.domain.infiniteLoopHeaders.foreach(println)
  
  val cdg = r.domain.controlDependencies // Uses backward dominance frontiers
  for (pc <- r.domain.allExecuted){
    var ps : List[Int] = Nil
    cdg.xIsControlDependentOn(pc)(p => ps ::= p)
    println(s"$pc is control dependent on ${ps.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)
  }
}