Merge branch 'master' into meilers_allow_heapdep_func_calls

Author: marcoeilers

src/main/scala/viper/silver/cfg/silver/SilverCfg.scala

@@ -82,6 +82,80 @@ class SilverCfg(val blocks: Seq[SilverBlock], val edges: Seq[SilverEdge], val en
                     entry: SilverBlock = entry,
                     exit: Option[SilverBlock] = exit): SilverCfg =
     SilverCfg(blocks, edges, entry, exit)
+
+
+  /**
+    * Recursively finds the next join point to a branch point.
+    *
+    * @param queueInit     Used to initialize the BFS queue with blocks that are yet to be visited.
+    * @param visitedInit   Used to initialize list of visited nodes.
+    * @param loopHeadsSeen All the loop heads that were visited so far.
+    * @param getNext       function which returns the successor nodes.
+    * @return (jp, m) where jp is the next join point,
+    *         and m maps all branch points which have been already found
+    *         to their join points.
+    */
+  private def findJoinPoint(queueInit: Iterable[SilverBlock],
+                            visitedInit: Iterable[SilverBlock],
+                            // We never enqueue loopHeads which we already have seen.
+                            // This would lead to non-termination.
+                            loopHeadsSeen: Iterable[SilverBlock],
+                            getNext: SilverBlock => Iterable[SilverBlock])
+  : (Option[SilverBlock], mutable.Map[SilverBlock, SilverBlock]) = {
+
+    var queue = mutable.Queue.from(queueInit)
+    var visited: mutable.Set[SilverBlock] = mutable.Set.from(visitedInit)
+    val map = mutable.Map[SilverBlock, SilverBlock]()
+    var loopHeads: mutable.Set[SilverBlock] = mutable.Set.from(loopHeadsSeen)
+
+    // BFS traversal of CFG.
+    while (queue.nonEmpty) {
+      val curr = queue.dequeue()
+      val visitNext =
+        if (!visited.contains(curr)) {
+          visited += curr
+          if (curr.isInstanceOf[SilverLoopHeadBlock]) {
+            // If current block is loop head, add it to set of seen loopheads.
+            loopHeads += curr
+          }
+          getNext(curr) match {
+            case out@Seq() => out
+            case out@Seq(_) => out
+            case out@Seq(_, _) =>
+              // New branch point found, start findJoinPoint procedure
+              // recursively to find the corresponding join point.
+              val (joinPoint, innerMap) =
+                findJoinPoint(out.filter(!loopHeads.contains(_)), Seq(curr), loopHeads, getNext)
+              // Add the join points found to the map of all join points.
+              map ++= innerMap
+              joinPoint foreach {
+                jp => map += curr -> jp
+              }
+              // Continue BFS traversal from join point.
+              joinPoint
+            case _ => sys.error("At most two outgoing edges expected.")
+          }
+        } else {
+          return (Some(curr), map)
+        }
+
+
+      // Avoid re-visiting already seen loop heads.
+      queue = queue.enqueueAll(visitNext.iterator.filter(!loopHeads.contains(_)))
+    }
+    (None, map)
+  }
+
+  /**
+    * Computes a mapping from all branch points to their corresponding join points.
+    *
+    * @return Mapping from all branch points to join points.
+    */
+  lazy val joinPoints: collection.Map[SilverBlock, SilverBlock] = {
+    val (jp, map) = findJoinPoint(Seq(entry), Seq.empty, Seq.empty, successors)
+    assert(jp.isEmpty)
+    map
+  }
 }
 
 object SilverCfg {