GPUVerify: add block predicator

1 files changed, 84 insertions, 0 deletions

diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs
new file mode 100644
index 00000000..3442a64d
--- /dev/null
+++ b/Source/GPUVerify/GraphAlgorithms.cs
@@ -0,0 +1,84 @@
+using Graphing;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace GPUVerify {
+
+public static class GraphAlgorithms {
+
+  public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
+    Contract.Assert(g.Reducible);
+
+    int n = g.Nodes.Count;
+    var nodeToNumber = new Dictionary<Node, int>(n);
+    var numberToNode = new Node[n];
+    var allNodes = new List<int>();
+    int counter = 0;
+    foreach (Node node in g.Nodes) {
+      numberToNode[counter] = node;
+      nodeToNumber[node] = counter;
+      allNodes.Add(counter);
+      counter++;
+    }
+
+    var loops = new List<int>[n];
+    foreach (var h in g.Headers) {
+      var loopNodes = new HashSet<Node>();
+      foreach (var b in g.BackEdgeNodes(h))
+        loopNodes.UnionWith(g.NaturalLoops(h, b));
+      loops[nodeToNumber[h]] =
+        new List<int>(loopNodes.Select(node => nodeToNumber[node]));
+    }
+
+    var successors = new List<int>[n];
+    int[] incomingEdges = new int[n];
+
+    foreach (var e in g.Edges) {
+      Contract.Assert(e.Item1 != null);
+      Contract.Assert(e.Item2 != null);
+      int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
+      if (loops[target] == null || !loops[target].Contains(source)) {
+        if (successors[source] == null)
+          successors[source] = new List<int>();
+        successors[source].Add(target);
+        incomingEdges[target]++;
+      }
+    }
+
+    var sortedNodes = new List<Tuple<Node, bool>>();
+
+    var regionStack = new Stack<Tuple<Node, List<int>>>();
+    regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
+
+    while (regionStack.Count != 0) {
+      int rootIndex = -1;
+      foreach (var i in regionStack.Peek().Item2) {
+        if (incomingEdges[i] == 0) {
+          rootIndex = i;
+          break;
+        }
+      }
+      if (rootIndex == -1) {
+        var region = regionStack.Pop();
+        if (regionStack.Count != 0)
+          sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+        continue;
+      }
+      incomingEdges[rootIndex] = -1;
+      sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+      if (successors[rootIndex] != null)
+        foreach (int s in successors[rootIndex])
+          incomingEdges[s]--;
+      if (loops[rootIndex] != null)
+        regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
+                                                    loops[rootIndex]));
+    }
+
+    return sortedNodes;
+  }
+
+}
+
+}