summaryrefslogtreecommitdiff
path: root/Source/Graph/Graph.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Graph/Graph.cs')
-rw-r--r--Source/Graph/Graph.cs2894
1 files changed, 1447 insertions, 1447 deletions
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 8e5479e3..7f636200 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -1,1447 +1,1447 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Linq;
-using System.Collections.Generic;
-using System.Text; // for StringBuilder
-using System.Diagnostics.Contracts;
-namespace Microsoft.Boogie.GraphUtil {
-
- internal static class Util {
- private static string/*!*/ ListToString<T>(IEnumerable<T> xs) {
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("[");
- bool first = true;
- foreach (T/*!*/ x in xs) {
- Contract.Assert(x != null);
- if (!first)
- sb.Append(", ");
- sb.Append(x.ToString());
- first = false;
- }
- sb.Append("]");
- return sb.ToString();
- }
- public static string/*!*/ MapToString<Node>(Dictionary<Node, List<Node>> d) {
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("{");
- bool first = true;
- foreach (KeyValuePair<Node, List<Node>> de in d) {
- if (!first)
- sb.Append(", ");
- Contract.Assert(!object.Equals(de.Key,default(Node)));
- sb.Append(de.Key.ToString());
- sb.Append("~>");
- sb.Append(ListToString(de.Value));
- first = false;
- }
- sb.Append("}");
- return sb.ToString();
- }
- }
-
- // own struct to represent possibly undefined values, because Mono does
- // not like arrays with element type T! or T?
- public struct Maybe<T> {
- private T Value;
- public bool IsSet; // initialised with false by the default ctor
- public T Val {
- get {
- Contract.Assume(IsSet);
- return Value;
- }
- set {
- Value = value;
- IsSet = true;
- }
- }
- public void UnSet() {
- IsSet = false;
- }
- }
-
- public class DomRelation<Node> {
- // doms maps (unique) node numbers to the node numbers of the immediate dominator
- // to use it on Nodes, one needs the two way mapping between nodes and their numbers.
- private int[] doms; // 0 is unused: means undefined
- // here are the two mappings
- private Maybe<Node>[] postOrderNumberToNode;
- private Dictionary<Node, int> nodeToPostOrderNumber;
- private int sourceNum; // (number for) root of the graph
- private Node source; // root of the graph
- private Graph<Node> graph;
- private Dictionary<Node, List<Node>> immediateDominatorMap;
-
- [NotDelayed]
- internal DomRelation(Graph<Node> g, Node source) {
- this.graph = g;
- // slot 0 not used: nodes are numbered from 1 to n so zero
- // can represent undefined.
- this.source = source;
- //:base();
- this.NewComputeDominators();
- }
- public Dictionary<Node, List<Node>> ImmediateDominatorMap {
- get {
- Contract.Assume(this.immediateDominatorMap != null);
- return this.immediateDominatorMap;
- }
- }
- public bool DominatedBy(Node dominee, Node dominator, List<Node> path = null) {
- Contract.Assume(this.nodeToPostOrderNumber != null);
- Contract.Assume(this.doms != null);
- int domineeNum = this.nodeToPostOrderNumber[dominee];
- int dominatorNum = this.nodeToPostOrderNumber[dominator];
- if (domineeNum == dominatorNum)
- return true;
- int currentNodeNum = this.doms[domineeNum];
- while (true) {
- if (currentNodeNum == dominatorNum)
- return true;
- if (currentNodeNum == this.sourceNum)
- return false;
- if (path != null)
- path.Add(postOrderNumberToNode[currentNodeNum].Val);
- currentNodeNum = this.doms[currentNodeNum];
- }
- }
- private Dictionary<Node, List<Node>> domMap = null;
- [Pure]
- public override string ToString() {
- Contract.Assume(this.doms != null);
- int[] localDoms = this.doms;
- Contract.Assume(this.postOrderNumberToNode != null);
- if (domMap == null) {
- domMap = new Dictionary<Node, List<Node>>();
- for (int i = 1; i < localDoms.Length; i++) { // 0 slot is not used
- int domineeNum = i;
- int currentNodeNum = domineeNum;
- List<Node> dominators = new List<Node>();
- while (currentNodeNum != this.sourceNum) {
- dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val);
- currentNodeNum = this.doms[currentNodeNum];
- }
- dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val);
- domMap.Add(this.postOrderNumberToNode[i].Val, dominators);
- }
- }
- StringBuilder sb = new StringBuilder();
- sb.Append("{");
- bool first = true;
- foreach (KeyValuePair<Node, List<Node>> de in domMap) {
- if (!first)
- sb.Append(", ");
- Contract.Assert(!object.Equals(de.Key, default(Node)));
- sb.Append(de.Key.ToString());
- sb.Append("~>");
- sb.Append(ListToString(de.Value));
- first = false;
- }
- sb.Append("}");
- return sb.ToString();
- }
- private void PrintIntArray(int[] xs) {
- Console.Write("[");
- for (int i = 0; i < xs.Length; i++) {
- if (0 < i)
- Console.Write(", ");
- Console.Write(xs[i]);
- }
- Console.WriteLine("]");
- }
- public void PrintList<T>(IEnumerable<T> xs) {
- Console.Write("[");
- int i = 0;
- foreach (T/*!*/ x in xs) {
- Contract.Assert(x != null);
- if (0 < i)
- Console.Write(", ");
- Console.Write(x.ToString());
- i++;
- }
- Console.WriteLine("]");
- }
- public string/*!*/ ListToString<T>(IEnumerable<T> xs) {
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("[");
- bool first = true;
- foreach (T/*!*/ x in xs) {
- Contract.Assert(x != null);
- if (!first)
- sb.Append(", ");
- sb.Append(x.ToString());
- first = false;
- }
- sb.Append("]");
- return sb.ToString();
- }
-
- // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001.
- // http://citeseer.ist.psu.edu/cooper01simple.html
- private void NewComputeDominators() {
- int n = this.graph.Nodes.Count;
- this.postOrderNumberToNode = new Maybe<Node>[n + 1];
- this.nodeToPostOrderNumber = new Dictionary<Node, int>();
- //HashSet<Node> visited = new HashSet<Node>();
- //int currentNumber = 1;
- Contract.Assume(this.source != null);
- //this.PostOrderVisit(this.source, visited, ref currentNumber);
- this.PostOrderVisitIterative(this.source);
- this.sourceNum = this.nodeToPostOrderNumber[source];
- // for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); }
- this.doms = new int[n + 1]; // 0 is unused: means undefined
- Node start_node = this.source;
- this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node];
- bool changed = true;
- // PrintIntArray(doms);
- while (changed) {
- changed = false;
- // for all nodes, b, in reverse postorder (except start_node)
- for (int nodeNum = n - 1; 1 <= nodeNum; nodeNum--) {
- Node b = this.postOrderNumberToNode[nodeNum].Val;
- IEnumerable<Node> predecessors = this.graph.Predecessors(b);
- // find a predecessor (i.e., a higher number) for which
- // the doms array has been set
- int new_idom = 0;
- int first_processed_predecessor = 0;
- #region new_idom <- number of first (processed) predecessor of b (pick one)
- foreach (Node p in predecessors) {
- if (this.doms[this.nodeToPostOrderNumber[p]] != 0) {
- int x = this.nodeToPostOrderNumber[p];
- new_idom = x;
- first_processed_predecessor = x;
- break;
- }
- }
- #endregion
- #region for all other predecessors, p, of b
- foreach (Node p in predecessors) {
- if (this.nodeToPostOrderNumber[p] == first_processed_predecessor) {
- continue;
- }
- if (this.doms[this.nodeToPostOrderNumber[p]] != 0)
- new_idom = intersect(this.nodeToPostOrderNumber[p], new_idom, this.doms);
- }
- #endregion
- if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom) {
- this.doms[this.nodeToPostOrderNumber[b]] = new_idom;
- changed = true;
- }
- }
- }
- #region Populate the Immediate Dominator Map
- int sourceNum = this.nodeToPostOrderNumber[this.source];
- immediateDominatorMap = new Dictionary<Node, List<Node>>();
- for (int i = 1; i <= n; i++) {
- Node node = this.postOrderNumberToNode[i].Val;
- Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val;
- if (i == sourceNum && this.doms[i] == sourceNum) {
- continue;
- }
- if (immediateDominatorMap.ContainsKey(idomNode)) {
- immediateDominatorMap[idomNode].Add(node);
- } else {
- List<Node> l = new List<Node>();
- l.Add(node);
- immediateDominatorMap.Add(idomNode, l);
- }
- }
- #endregion
- }
- private int intersect(int b1, int b2, int[] doms) {
- int finger1 = b1;
- int finger2 = b2;
- while (finger1 != finger2) {
- while (finger1 < finger2) {
- finger1 = doms[finger1];
- }
- while (finger2 < finger1) {
- finger2 = doms[finger2];
- }
- }
- return finger1;
- }
- private void PostOrderVisit(Node/*!*/ n, HashSet<Node> visited, ref int currentNumber) {
- Contract.Requires(n != null);
- if (visited.Contains(n))
- return;
- visited.Add(n);
- foreach (Node/*!*/ child in this.graph.Successors(n)) {
- Contract.Assert(child != null);
- PostOrderVisit(child, visited, ref currentNumber);
- }
- Contract.Assume(this.postOrderNumberToNode != null);
- Contract.Assume(this.nodeToPostOrderNumber != null);
- this.postOrderNumberToNode[currentNumber].Val = n;
- this.nodeToPostOrderNumber[n] = currentNumber;
- currentNumber++;
- return;
- }
- // Iterative version: mimics the above recursive procedure
- private void PostOrderVisitIterative(Node n)
- {
- Contract.Requires(n != null);
- var visited = new HashSet<Node>();
- var grey = new HashSet<Node>();
- var stack = new Stack<Node>();
-
- int currentNumber = 1;
-
- stack.Push(n);
- visited.Add(n);
-
- while (stack.Count != 0)
- {
- var curr = stack.Pop();
-
- if (grey.Contains(curr))
- {
- Contract.Assume(this.postOrderNumberToNode != null);
- Contract.Assume(this.nodeToPostOrderNumber != null);
- this.postOrderNumberToNode[currentNumber].Val = curr;
- this.nodeToPostOrderNumber[curr] = currentNumber;
- currentNumber++;
- }
- else
- {
- grey.Add(curr);
- stack.Push(curr);
- foreach (Node/*!*/ child in this.graph.Successors(curr))
- {
- Contract.Assert(child != null);
- if (!visited.Contains(child))
- {
- visited.Add(child);
- stack.Push(child);
- }
- }
- }
-
- }
-
-
- }
-
- public Node LeastCommonAncestor(Node n1, Node n2)
- {
- int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2];
- int lca = intersect(num1, num2, this.doms);
- return postOrderNumberToNode[lca].Val;
- }
- }
-
- public class Graph<Node> {
- private HashSet<Tuple<Node/*!*/, Node/*!*/>> es;
- private HashSet<Node> ns;
- private Node source;
- private bool reducible;
- private HashSet<Node> headers;
- private Dictionary<Node, HashSet<Node>> backEdgeNodes;
- private Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;
- private HashSet<Node> splitCandidates;
-
- private DomRelation<Node> dominatorMap = null;
- private Dictionary<Node, HashSet<Node>> predCache = new Dictionary<Node, HashSet<Node>>();
- private Dictionary<Node, HashSet<Node>> succCache = new Dictionary<Node, HashSet<Node>>();
- private bool predComputed;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null));
- Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));
- }
-
- private class PreHeader {
- Node/*!*/ myHeader;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(myHeader != null);
- }
-
- internal PreHeader(Node/*!*/ h) {
- Contract.Requires(h != null);
- myHeader = h;
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return "#" + myHeader.ToString();
- }
- }
-
- public Graph(HashSet<Tuple<Node/*!*/, Node/*!*/>> edges) {
-
- Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null));
- es = edges;
-
- // original A#
- //ns = Set<Node>{ x : <x,y> in es } + Set<Node>{ y : <x,y> in es };
-
- // closest Spec#
- //ns = new Set<Node>{ Tuple<Node,Node> p in edges; p.Item1 } + new Set<Node>{ Tuple<Node,Node> p in edges; p.Item2 };
-
- //
- HashSet<Node> temp = new HashSet<Node>();
- foreach (Tuple<Node/*!*/, Node/*!*/> p in edges) {
- Contract.Assert(p.Item1 != null);
- temp.Add(p.Item1);
- Contract.Assert(p.Item2 != null);
- temp.Add(p.Item2);
- }
- ns = temp;
- }
- public Graph() {
- es = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
- ns = new HashSet<Node>();
- }
-
- // BUGBUG: Set<T>.ToString() should return a non-null string
- [Pure]
- public override string/*!*/ ToString() {
- return "" + es.ToString();
- }
-
- public void AddSource(Node/*!*/ x) {
- Contract.Requires(x != null);
- // BUGBUG: This generates bad code in the compiler
- //ns += new Set<Node>{x};
- ns.Add(x);
- source = x;
- }
-
- public void AddEdge(Node/*!*/ source, Node/*!*/ dest) {
- Contract.Requires(source != null);
- Contract.Requires(dest != null);
- //es += Set<Edge>{<source,dest>};
- //ns += Set<Node>{source, dest};
- es.Add(new Tuple<Node/*!*/, Node/*!*/>(source, dest));
- ns.Add(source);
- ns.Add(dest);
- predComputed = false;
- }
-
- public HashSet<Node> Nodes {
- get {
- return ns;
- }
- }
- public IEnumerable<Tuple<Node/*!*/, Node/*!*/>> Edges {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Tuple<Node, Node>>>())
- && Contract.ForAll(Contract.Result<IEnumerable<Tuple<Node, Node>>>(), n =>
- n.Item1 != null && n.Item2 != null));
- return es;
- }
- }
-
- public bool Edge(Node/*!*/ x, Node/*!*/ y) {
- Contract.Requires(x != null);
- Contract.Requires(y != null);
- // original A#
- // return <x,y> in es;
- return es.Contains(new Tuple<Node/*!*/, Node/*!*/>(x, y));
- }
-
- private void ComputePredSuccCaches() {
- if (predComputed)
- return;
- predComputed = true;
- predCache = new Dictionary<Node, HashSet<Node>>();
- succCache = new Dictionary<Node, HashSet<Node>>();
-
- foreach (Node n in Nodes) {
- predCache[n] = new HashSet<Node>();
- succCache[n] = new HashSet<Node>();
- }
-
- foreach (Tuple<Node/*!*/, Node/*!*/> p in Edges) {
- Contract.Assert(p.Item1 != null);
- Contract.Assert(p.Item2 != null);
- HashSet<Node> tmp;
-
- tmp = predCache[p.Item2];
- tmp.Add(p.Item1);
- predCache[p.Item2] = tmp;
-
- tmp = succCache[p.Item1];
- tmp.Add(p.Item2);
- succCache[p.Item1] = tmp;
- }
- }
-
- public IEnumerable<Node> Predecessors(Node n) {
- // original A#
- //Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
-
- ComputePredSuccCaches();
- return predCache[n];
- }
-
- public IEnumerable<Node> Successors(Node n) {
- ComputePredSuccCaches();
- return succCache[n];
- }
-
- public List<Node> SuccessorsAsList(Node n) {
- ComputePredSuccCaches();
- List<Node> ret = new List<Node>();
- foreach (Node s in succCache[n])
- ret.Add(s);
- return ret;
- }
-
- public DomRelation<Node> /*Map<Node,Set<Node>>*/ DominatorMap {
- get {
- Contract.Assert(source != null);
- if (this.dominatorMap == null) {
- this.dominatorMap = new DomRelation<Node>(this, this.source);
- }
- return this.dominatorMap;
- }
- }
-
- public Dictionary<Node, List<Node>> ImmediateDominatorMap {
- get {
- Contract.Assert(source != null);
- if (this.dominatorMap == null) {
- this.dominatorMap = new DomRelation<Node>(this, this.source);
- }
- return this.dominatorMap.ImmediateDominatorMap;
- }
- }
- public List<Node> ImmediatelyDominatedBy(Node/*!*/ n) {
- Contract.Requires(n != null);
- List<Node> dominees;
- this.ImmediateDominatorMap.TryGetValue(n, out dominees);
- return dominees == null ? new List<Node>() : dominees;
- }
-
- public IEnumerable<Node/*?*/> TopologicalSort(bool reversed = false) {
- bool acyclic;
- List<Node> sortedList;
- this.TarjanTopSort(out acyclic, out sortedList, reversed);
- return acyclic ? sortedList : new List<Node>();
- }
- // From Tarjan 1972
- public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes, bool reversed = false) {
- int n = this.Nodes.Count;
- if (n == 0) {
- acyclic = true;
- sortedNodes = new List<Node>();
- return;
- }
- int[] incomingEdges = new int[n];
- // need an arbitrary numbering for the nodes to use as indices into
- // the arrays used within this algorithm
- Dictionary<Node, int> nodeToNumber = new Dictionary<Node, int>(n);
- Maybe<Node>[] numberToNode = new Maybe<Node>[n];
- int counter = 0;
- foreach (Node node in this.Nodes) {
- numberToNode[counter].Val = node;
- nodeToNumber[node] = counter;
- counter++;
- }
- foreach (Tuple<Node/*!*/, Node/*!*/> e in this.Edges) {
- Contract.Assert(e.Item1 != null);
- Contract.Assert(e.Item2 != null);
- Node/*!*/ target = e.Item2;
- incomingEdges[nodeToNumber[target]]++;
- }
- List<Node> sorted = new List<Node>();
- int sortedIndex = 0;
- while (sortedIndex < n) {
- // find a root (i.e., its index)
- int rootIndex = -1;
- if (reversed) {
- for (int i = n-1; i >= 0; i--) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
- }
- }
- } else {
- for (int i = 0; i < n; i++) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
- }
- }
- }
- if (rootIndex == -1) {
- acyclic = false;
- sortedNodes = new List<Node>();
- return;
- }
- // mark root so it won't be used again
- incomingEdges[rootIndex] = -1;
- Node root = numberToNode[rootIndex].Val;
- sorted.Add(root);
- ++sortedIndex;
- foreach (Node s in this.Successors(root)) {
- incomingEdges[nodeToNumber[s]]--;
- }
- }
- acyclic = true;
- sortedNodes = sorted;
- return;
- }
- private IEnumerable<Node> OldTopologicalSort() {
- Tuple<bool, List<Node>> result = this.TopSort();
- return result.Item1 ? result.Item2 : (IEnumerable<Node>)new List<Node>();
- }
- // From AsmL distribution example
- private Tuple<bool, List<Node>> TopSort()
- {
- List<Node> S = new List<Node>();
- HashSet<Node> V = this.Nodes;
- HashSet<Node> X = new HashSet<Node>();
- foreach (Node/*!*/ n in V) {
- Contract.Assert(n != null);
- X.Add(n);
- }
- bool change = true;
- while (change)
- // invariant: X = V - S
- {
- change = false;
- if (X.Count > 0) {
- foreach (Node/*!*/ n in X) {
- Contract.Assert(n != null);
- // see if n has any incoming edges from any other node in X
- bool inDegreeZero = true;
- foreach (Node/*!*/ u in X) {
- Contract.Assert(u != null);
- if (this.Edge(u, n)) {
- inDegreeZero = false;
- break; // no point looking further
- }
- }
- if (inDegreeZero) {
- S.Add(n);
- X.Remove(n);
- change = true;
- break; // might as well go back and start looking through X from the beginning
- }
- }
- // Then we made it all the way through X without finding a source node
- if (!change) {
- return new Tuple<bool, List<Node>>(false, new List<Node>());
- }
- }
- }
- return new Tuple<bool, List<Node>>(true, S);
- }
-
- public static bool Acyclic(Graph<Node> g, Node source) {
- bool acyclic;
- List<Node> sortedList;
- g.TarjanTopSort(out acyclic, out sortedList);
- return acyclic;
- }
-
- // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.]
- static HashSet<Node> NaturalLoop(Graph<Node> g, Tuple<Node/*!*/, Node/*!*/> backEdge)
- {
- Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null);
- Node/*!*/ n = backEdge.Item1;
- Node/*!*/ d = backEdge.Item2;
- Stack<Node> stack = new Stack<Node>();
- HashSet<Node> loop = new HashSet<Node>();
- loop.Add(d);
- if (!n.Equals(d)) // then n is not in loop
- {
- loop.Add(n);
- stack.Push(n); // push n onto stack
- }
- while (stack.Count > 0) // not empty
- {
- Node m = stack.Peek();
- stack.Pop(); // pop stack
- foreach (Node/*!*/ p in g.Predecessors(m)) {
- Contract.Assert(p != null);
- if (!(loop.Contains(p))) {
- loop.Add(p);
- stack.Push(p); // push p onto stack
- }
- }
- }
- return loop;
- }
-
- internal struct ReducibleResult {
- internal bool reducible;
- internal HashSet<Node> headers;
- internal Dictionary<Node, HashSet<Node>> backEdgeNodes;
- internal Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;
- internal HashSet<Node> splitCandidates;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null));
- }
-
- internal ReducibleResult(bool b, HashSet<Node> headers, Dictionary<Node, HashSet<Node>> backEdgeNodes, Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops, HashSet<Node> splitCandidates)
- {
- Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null));
- this.reducible = b;
- this.headers = headers;
- this.backEdgeNodes = backEdgeNodes;
- this.naturalLoops = naturalLoops;
- this.splitCandidates = splitCandidates;
- }
-
- }
-
- // [Dragon, p. 606]
- static ReducibleResult ComputeReducible(Graph<Node> g, Node source) {
- // first, compute the dom relation
- DomRelation<Node> /*Map<Node,Set<Node>>*/ D = g.DominatorMap;
- return ComputeReducible(g, source, D);
- }
-
- static HashSet<Node> FindCycle(Graph<Node> g, Node source) {
- Stack<Tuple<Node, List<Node>>> stack = new Stack<Tuple<Node, List<Node>>>();
- HashSet<Node> stackAsSet = new HashSet<Node>();
- HashSet<Node> visited = new HashSet<Node>();
- stack.Push(new Tuple<Node, List<Node>>(source, g.SuccessorsAsList(source)));
- stackAsSet.Add(source);
- while (stack.Count > 0) {
- Tuple<Node, List<Node>> tuple = stack.Peek();
- List<Node> children = tuple.Item2;
- if (children.Count == 0) {
- stack.Pop();
- stackAsSet.Remove(tuple.Item1);
- continue;
- }
- Node n = children[0];
- children.RemoveAt(0);
- if (stackAsSet.Contains(n)) {
- HashSet<Node> ret = new HashSet<Node>();
- ret.Add(n);
- while (true) {
- Node x = stack.Pop().Item1;
- if (x.Equals(n))
- return ret;
- }
- }
- if (visited.Contains(n))
- continue;
- stack.Push(new Tuple<Node, List<Node>>(n, g.SuccessorsAsList(n)));
- visited.Add(n);
- stackAsSet.Add(n);
- System.Diagnostics.Debug.Assert(stack.Count == stackAsSet.Count);
- }
- return new HashSet<Node>();
- }
-
- // [Dragon, p. 606]
- static ReducibleResult ComputeReducible(Graph<Node> g,
- Node source,
- DomRelation<Node>/*!*/ DomRelation) {
- Contract.Requires(DomRelation != null);
-
- //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible");
- IEnumerable<Tuple<Node/*!*/, Node/*!*/>> edges = g.Edges;
- Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null));
- HashSet<Tuple<Node/*!*/, Node/*!*/>> backEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
- HashSet<Tuple<Node/*!*/, Node/*!*/>> nonBackEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
- foreach (Tuple<Node/*!*/, Node/*!*/> e in edges) {
- Contract.Assert(e.Item1 != null);
- Contract.Assert(e.Item2 != null);
- Node x = e.Item1;
- Node y = e.Item2; // so there is an edge from x to y
- if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x
- backEdges.Add(e);
- } else {
- nonBackEdges.Add(e);
- }
- }
- Graph<Node> withoutBackEdges = new Graph<Node>(nonBackEdges);
- if (!Acyclic(withoutBackEdges, source)) {
- return new ReducibleResult(false,
- new HashSet<Node>(),
- new Dictionary<Node, HashSet<Node>>(),
- new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>(),
- FindCycle(withoutBackEdges, source));
- } else {
- // original A#:
- //Set<Node> headers = Set{ d : <n,d> in backEdges };
- HashSet<Node> headers = new HashSet<Node>();
- foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {
-
- Contract.Assert(e.Item1 != null);
- Contract.Assert(e.Item2 != null);
- headers.Add(e.Item2);
- }
- // original A#:
- //Map<Node,Set<Node>> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set<Node>{ b : <b,x> in backEdges, x == h } };
- Dictionary<Node, HashSet<Node>> backEdgeNodes = new Dictionary<Node, HashSet<Node>>();
- foreach (Node/*!*/ h in headers) {
- Contract.Assert(h != null);
- HashSet<Node> bs = new HashSet<Node>();
- foreach (Tuple<Node, Node> backedge in backEdges) {
- Contract.Assert(backedge.Item1 != null);
- Contract.Assert(backedge.Item2 != null);
- if (backedge.Item2.Equals(h)) {
- bs.Add(backedge.Item1);
- }
- }
- backEdgeNodes.Add(h, bs);
- }
-
- // original A#:
- //Map<Tuple<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };
- Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops = new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>();
- foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {
- Contract.Assert(e.Item1 != null && e.Item2 != null);
- naturalLoops.Add(e, NaturalLoop(g, e));
- }
-
- //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible");
- return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops, new HashSet<Node>());
- }
- }
-
- public bool Reducible {
- get {
- return reducible;
- }
- }
- public IEnumerable<Node> Headers {
- get {
- return headers;
- }
- }
- public IEnumerable<Node> BackEdgeNodes(Node/*!*/ h) {
- Contract.Requires(h != null);
- // original A#:
- //return h in backEdgeNodes ? backEdgeNodes[h] : null;
- return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new List<Node>());
- }
- public IEnumerable<Node> NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) {
- Contract.Requires(header != null);
- Contract.Requires(backEdgeNode != null);
- Tuple<Node/*!*/, Node/*!*/> e = new Tuple<Node/*!*/, Node/*!*/>(backEdgeNode, header);
- return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new List<Node>();
- }
- public HashSet<Node> SplitCandidates {
- get {
- return splitCandidates;
- }
- }
- public void ComputeLoops() {
- ReducibleResult r = ComputeReducible(this, this.source);
- this.reducible = r.reducible;
- this.headers = r.headers;
- this.backEdgeNodes = r.backEdgeNodes;
- this.naturalLoops = r.naturalLoops;
- this.splitCandidates = r.splitCandidates;
- return;
- }
-
- public IEnumerable<Node> SortHeadersByDominance()
- {
- Graph<Node> dag = new Graph<Node>();
- foreach (Node b in headers)
- {
- dag.AddSource(b);
- foreach (Node c in headers)
- {
- if (b.Equals(c)) continue;
- if (DominatorMap.DominatedBy(b, c))
- {
- System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b));
- dag.AddEdge(b, c);
- }
- }
- }
- return dag.TopologicalSort();
- }
-
- public string ToDot(Func<Node, string> NodeLabel = null, Func<Node, string> NodeStyle = null) {
- NodeLabel = NodeLabel ?? (n => n.ToString());
- NodeStyle = NodeStyle ?? (n => "[shape=box]");
- var s = new StringBuilder();
- s.AppendLine("digraph G {");
- foreach (var n in Nodes)
- s.AppendLine(" \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";");
- foreach (var e in Edges)
- s.AppendLine(" \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";");
- s.AppendLine("}");
- return s.ToString();
- }
-
- public ICollection<Node> ComputeReachable() {
- ICollection<Node> result = new HashSet<Node>();
- Stack<Node> stack = new Stack<Node>();
- stack.Push(source);
- while(!(stack.Count() == 0)) {
- Node n = stack.Pop();
- result.Add(n);
- foreach(var m in Successors(n)) {
- if(!result.Contains(m)) {
- stack.Push(m);
- }
- }
- }
- return result;
- }
-
- } // end: class Graph
-
- public static class GraphAlgorithms
- {
-
-
- public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
- {
- var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
- Node source;
- if (exits.Count == 0)
- exits.Add(dummySource);
- var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
- if (exits.Count == 1)
- {
- dual.AddSource(exits[0]);
- source = exits[0];
- }
- else
- {
- dual.AddSource(dummySource);
- source = dummySource;
- foreach (var exit in exits)
- dual.AddEdge(dummySource, exit);
- }
-
- #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node
- foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item)))
- {
- dual.AddEdge(source, n);
- }
- #endregion
-
- return dual;
- }
-
- 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];
- var predecessors = new List<int>[n];
- int[] incomingEdges = new int[n];
-
- for (int i = 0; i < n; i++)
- predecessors[i] = new List<int>();
-
- 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]++;
- }
- predecessors[target].Add(source);
- }
-
- var sortedNodes = new List<Tuple<Node, bool>>();
- var sortedNodesInternal = new List<int>();
-
- var regionStack = new Stack<Tuple<Node, List<int>>>();
- regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
-
- while (regionStack.Count != 0)
- {
- var rootIndexes = new List<int>();
- foreach (var i in regionStack.Peek().Item2)
- {
- if (incomingEdges[i] == 0)
- rootIndexes.Add(i);
- }
- if (rootIndexes.Count() == 0)
- {
- var region = regionStack.Pop();
- if (regionStack.Count != 0) {
- sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
- sortedNodesInternal.Add(nodeToNumber[region.Item1]);
- }
- continue;
- }
- int rootIndex = rootIndexes[0];
- int maxPredIndex = -1;
- foreach (var i in rootIndexes) {
- foreach (var p in predecessors[i]) {
- int predIndex =
- sortedNodesInternal.FindLastIndex(x => x == p);
- if (predIndex > maxPredIndex) {
- rootIndex = i;
- maxPredIndex = predIndex;
- }
- }
- }
- incomingEdges[rootIndex] = -1;
- sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
- sortedNodesInternal.Add(rootIndex);
- 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;
- }
-
- // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
- // "The Program Dependence Graph and Its Use in Optimization"
- public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new()
- {
- Graph<Node> dual = g.Dual(new Node());
- DomRelation<Node> pdom = dual.DominatorMap;
-
- var result = new Dictionary<Node, HashSet<Node>>();
-
- var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
- foreach (var edge in S)
- {
- var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
- var deps = new List<Node>();
- if (L == edge.Item1)
- {
- pdom.DominatedBy(edge.Item2, edge.Item1, deps);
- deps.Add(edge.Item2);
- deps.Add(edge.Item1);
- }
- else
- {
- pdom.DominatedBy(edge.Item2, L, deps);
- deps.Add(edge.Item2);
- }
- if (result.ContainsKey(edge.Item1))
- {
- result[edge.Item1].UnionWith(deps);
- }
- else
- {
- result[edge.Item1] = new HashSet<Node>(deps);
- }
- }
-
- return result;
- }
-
- public static void TransitiveClosure<Node>(this Dictionary<Node, HashSet<Node>> graph) where Node : class {
- bool changed;
- do {
- changed = false;
- foreach (var entry in graph) {
- var newSuccessors = new HashSet<Node>(entry.Value);
- foreach (var successor in entry.Value) {
- if (graph.ContainsKey(successor))
- newSuccessors.UnionWith(graph[successor]);
- }
- if (newSuccessors.Count != entry.Value.Count) {
- entry.Value.UnionWith(newSuccessors);
- changed = true;
- }
- }
- } while (changed);
- }
-
- }
-
- public delegate System.Collections.IEnumerable/*<Node!>*//*!*/ Adjacency<T>(T/*!*/ node);
-
-
- // An SCC is a set of nodes
- public sealed class SCC<Node> : ICollection<Node>
- {
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(nodesMap != null);
- }
-
- private IDictionary<Node, object>/*!*/ nodesMap = new Dictionary<Node, object>();
- private ICollection<Node>/*!*/ nodes
- {
- get
- {
- return cce.NonNull(nodesMap.Keys);
- }
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
- {
- Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
-
- return ((System.Collections.IEnumerable)nodes).GetEnumerator();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- IEnumerator<Node>/*!*/ IEnumerable<Node>.GetEnumerator()
- {
- Contract.Ensures(Contract.Result<IEnumerator<Node>>() != null);
-
- return ((IEnumerable<Node>)nodes).GetEnumerator();
- }
-
- public int Count
- {
- get
- {
- return nodes.Count;
- }
- }
- public bool IsReadOnly
- {
- get
- {
- return nodesMap.IsReadOnly;
- }
- }
- public void Add(Node item)
- {
- nodesMap.Add(item, null);
- }
- public void Clear()
- {
- nodesMap.Clear();
- }
- [Pure]
- public bool Contains(Node item)
- {
- return nodesMap.ContainsKey(item);
- }
- public void CopyTo(Node[] array, int arrayIndex)
- {
- //Contract.Requires(array != null);
- nodes.CopyTo(array, arrayIndex);
- }
- public bool Remove(Node item)
- {
- return nodesMap.Remove(item);
- }
- }
-
- public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class
- {
- private readonly IDictionary<Node/*!*/, object>/*!*/ graph;
- [ContractInvariantMethod]
- void graphInvariantMethod()
- {
- Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null));
- Contract.Invariant(preds != null);
- Contract.Invariant(succs != null);
- }
- private readonly Adjacency<Node>/*!*/ preds;
- private readonly Adjacency<Node>/*!*/ succs;
-
- private bool computed = false;
- public bool Computed
- {
- get
- {
- return computed;
- }
- }
-
- [NotDelayed]
- public StronglyConnectedComponents(System.Collections.IEnumerable/*<Node!>*/ graph, Adjacency<Node> preds, Adjacency<Node> succs)
- : base()
- {
- Contract.Requires(succs != null);
- Contract.Requires(preds != null);
- Contract.Requires(graph != null);
- Contract.Ensures(!Computed);
- IDictionary<Node/*!*/, object>/*!*/ dict = new Dictionary<Node/*!*/, object>();
- foreach (Node/*!*/ n in graph)
- {
- Contract.Assert(n != null);
- dict.Add(n, null);
- }
-
- this.graph = dict;
- this.preds = preds;
- this.succs = succs;
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
- {
- Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
-
- return ((System.Collections.IEnumerable)sccs).GetEnumerator();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- IEnumerator<SCC<Node>/*!*/>/*!*/ IEnumerable<SCC<Node>/*!*/>.GetEnumerator()
- {
- Contract.Ensures(Contract.Result<IEnumerator<SCC<Node>>>() != null);
-
- Contract.Assume(Computed);
- Contract.Assert(cce.NonNullElements((IEnumerable<SCC<Node>/*!*/>)sccs));//REVIEW
- return ((IEnumerable<SCC<Node>/*!*/>)sccs).GetEnumerator();
- }
-
- private readonly IList<SCC<Node>/*!*/>/*!*/ sccs = new List<SCC<Node>/*!*/>();
- [ContractInvariantMethod]
- void sccsInvariant()
- {
- Contract.Invariant(cce.NonNullElements(sccs));
- }
-
-
- public void Compute()
- {
- Contract.Requires(!Computed);
- Contract.Ensures(Computed);
- // Compute post times on graph with edges reversed
- this.dfsNext = this.preds;
- foreach (Node/*!*/ n in cce.NonNull(graph.Keys))
- {
- Contract.Assert(n != null);
- if (!seen.ContainsKey(n))
- {
- OrderNodes(n);
- }
- }
-
- // Clear seen
- seen.Clear();
-
- // Compute SCCs
- this.dfsNext = this.succs;
- while (postOrder.Count > 0)
- {
- Node/*!*/ n = postOrder.Pop();
- Contract.Assert(n != null);
-
- if (!seen.ContainsKey(n))
- {
- SCC<Node>/*!*/ curr = new SCC<Node>();
- FindSCCs(n, curr);
- sccs.Add(curr);
- }
- }
-
- // Clear seen
- seen.Clear();
-
- this.computed = true;
- }
-
- private Adjacency<Node>/*?*/ dfsNext = null;
-
- private readonly IDictionary<Node/*!*/, object>/*!*/ seen = new Dictionary<Node/*!*/, object>();
- private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(seen != null);
- Contract.Invariant(cce.NonNullElements(postOrder));
- }
-
-
- // DFS to order nodes by post times
- private void OrderNodes(Node node)
- {
- Contract.Requires(node != null);
- seen.Add(node, null);
-
- Contract.Assert(dfsNext != null);
- System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
- Contract.Assert(nexts != null);
- foreach (Node/*!*/ n in nexts)
- {
- Contract.Assert(n != null);
- if (graph.ContainsKey(n) && !seen.ContainsKey(n))
- {
- OrderNodes(n);
- }
- }
-
- postOrder.Push(node);
- }
-
- // DFS to compute SCCs
- private void FindSCCs(Node node, SCC<Node> currSCC)
- {
- Contract.Requires(currSCC != null);
- Contract.Requires(node != null);
- //modifies currSCC.*;
- seen.Add(node, null);
- currSCC.Add(node);
-
- Contract.Assert(dfsNext != null);
- System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
- Contract.Assert(nexts != null);
- foreach (Node/*!*/ n in nexts)
- {
- Contract.Assert(n != null);
- if (graph.ContainsKey(n) && !seen.ContainsKey(n))
- {
- FindSCCs(n, currSCC);
- }
- }
- }
-
- [Pure]
- public override string ToString()
- {
- Contract.Ensures(Contract.Result<string>() != null);
- string outStr = "";
- int i = 0;
-
- foreach (ICollection<Node> component in this)
- {
- string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++);
- Contract.Assert(tmp != null);
- outStr += tmp;
-
- bool firstInRow = true;
-
- foreach (Node b in component)
- {
- string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b);
- Contract.Assert(tmpComponent != null);
- outStr += tmpComponent;
- firstInRow = false;
- }
- }
- return outStr;
- }
-
- }
-
- public class GraphProgram {
- static void TestGraph<T>(T/*!*/ source, params Tuple<T/*!*/, T/*!*/>[] edges) {
- Contract.Requires(source != null);
- Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null));
- HashSet<Tuple<T/*!*/, T/*!*/>> es = new HashSet<Tuple<T/*!*/, T/*!*/>>();
- foreach (Tuple<T/*!*/, T/*!*/> e in edges) {
- Contract.Assert(e.Item1 != null && e.Item2 != null);
- es.Add(e);
- }
- Graph<T> g = new Graph<T>(es);
- g.AddSource(source);
- Console.WriteLine("G = " + g);
- g.ComputeLoops();
- Console.WriteLine("G's Dominator Map = " + g.DominatorMap);
- Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap));
- Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no"));
- }
-
- static void Main(string[] args)
- //requires forall{string s in args; s != null};
- {
- Console.WriteLine("Spec# says hello!");
- // This generates bad IL -- need to fix a bug in the compiler
- //Graph<int> g = new Graph<int>(new Set<Tuple<int,int>>{ new Tuple<int,int>(1,2), new Tuple<int,int>(1,3), new Tuple<int,int>(2,3) });
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Tuple<char, char>('a', 'b'),
- new Tuple<char, char>('a', 'c'),
- new Tuple<char, char>('b', 'c')
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Tuple<char, char>('a', 'b'),
- new Tuple<char, char>('a', 'c'),
- new Tuple<char, char>('b', 'd'),
- new Tuple<char, char>('c', 'e'),
- new Tuple<char, char>('c', 'f'),
- new Tuple<char, char>('d', 'e'),
- new Tuple<char, char>('e', 'd'),
- new Tuple<char, char>('e', 'f'),
- new Tuple<char, char>('f', 'e')
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Tuple<char, char>('a', 'b'),
- new Tuple<char, char>('a', 'c'),
- new Tuple<char, char>('b', 'c'),
- new Tuple<char, char>('c', 'b')
- );
-
- Console.WriteLine("");
- TestGraph<int>(1,
- new Tuple<int, int>(1, 2),
- new Tuple<int, int>(1, 3),
- new Tuple<int, int>(2, 3)
- );
-
- Console.WriteLine("");
- TestGraph<int>(1,
- new Tuple<int, int>(1, 2),
- new Tuple<int, int>(1, 3),
- new Tuple<int, int>(2, 3),
- new Tuple<int, int>(3, 2)
- );
-
- Console.WriteLine("");
- TestGraph<int>(2,
- new Tuple<int, int>(2, 3),
- new Tuple<int, int>(2, 4),
- new Tuple<int, int>(3, 2)
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Tuple<char, char>('a', 'b'),
- new Tuple<char, char>('a', 'c'),
- new Tuple<char, char>('b', 'c'),
- new Tuple<char, char>('b', 'b')
- );
-
-
- }
- }
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.Text; // for StringBuilder
+using System.Diagnostics.Contracts;
+namespace Microsoft.Boogie.GraphUtil {
+
+ internal static class Util {
+ private static string/*!*/ ListToString<T>(IEnumerable<T> xs) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("[");
+ bool first = true;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (!first)
+ sb.Append(", ");
+ sb.Append(x.ToString());
+ first = false;
+ }
+ sb.Append("]");
+ return sb.ToString();
+ }
+ public static string/*!*/ MapToString<Node>(Dictionary<Node, List<Node>> d) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("{");
+ bool first = true;
+ foreach (KeyValuePair<Node, List<Node>> de in d) {
+ if (!first)
+ sb.Append(", ");
+ Contract.Assert(!object.Equals(de.Key,default(Node)));
+ sb.Append(de.Key.ToString());
+ sb.Append("~>");
+ sb.Append(ListToString(de.Value));
+ first = false;
+ }
+ sb.Append("}");
+ return sb.ToString();
+ }
+ }
+
+ // own struct to represent possibly undefined values, because Mono does
+ // not like arrays with element type T! or T?
+ public struct Maybe<T> {
+ private T Value;
+ public bool IsSet; // initialised with false by the default ctor
+ public T Val {
+ get {
+ Contract.Assume(IsSet);
+ return Value;
+ }
+ set {
+ Value = value;
+ IsSet = true;
+ }
+ }
+ public void UnSet() {
+ IsSet = false;
+ }
+ }
+
+ public class DomRelation<Node> {
+ // doms maps (unique) node numbers to the node numbers of the immediate dominator
+ // to use it on Nodes, one needs the two way mapping between nodes and their numbers.
+ private int[] doms; // 0 is unused: means undefined
+ // here are the two mappings
+ private Maybe<Node>[] postOrderNumberToNode;
+ private Dictionary<Node, int> nodeToPostOrderNumber;
+ private int sourceNum; // (number for) root of the graph
+ private Node source; // root of the graph
+ private Graph<Node> graph;
+ private Dictionary<Node, List<Node>> immediateDominatorMap;
+
+ [NotDelayed]
+ internal DomRelation(Graph<Node> g, Node source) {
+ this.graph = g;
+ // slot 0 not used: nodes are numbered from 1 to n so zero
+ // can represent undefined.
+ this.source = source;
+ //:base();
+ this.NewComputeDominators();
+ }
+ public Dictionary<Node, List<Node>> ImmediateDominatorMap {
+ get {
+ Contract.Assume(this.immediateDominatorMap != null);
+ return this.immediateDominatorMap;
+ }
+ }
+ public bool DominatedBy(Node dominee, Node dominator, List<Node> path = null) {
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ Contract.Assume(this.doms != null);
+ int domineeNum = this.nodeToPostOrderNumber[dominee];
+ int dominatorNum = this.nodeToPostOrderNumber[dominator];
+ if (domineeNum == dominatorNum)
+ return true;
+ int currentNodeNum = this.doms[domineeNum];
+ while (true) {
+ if (currentNodeNum == dominatorNum)
+ return true;
+ if (currentNodeNum == this.sourceNum)
+ return false;
+ if (path != null)
+ path.Add(postOrderNumberToNode[currentNodeNum].Val);
+ currentNodeNum = this.doms[currentNodeNum];
+ }
+ }
+ private Dictionary<Node, List<Node>> domMap = null;
+ [Pure]
+ public override string ToString() {
+ Contract.Assume(this.doms != null);
+ int[] localDoms = this.doms;
+ Contract.Assume(this.postOrderNumberToNode != null);
+ if (domMap == null) {
+ domMap = new Dictionary<Node, List<Node>>();
+ for (int i = 1; i < localDoms.Length; i++) { // 0 slot is not used
+ int domineeNum = i;
+ int currentNodeNum = domineeNum;
+ List<Node> dominators = new List<Node>();
+ while (currentNodeNum != this.sourceNum) {
+ dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val);
+ currentNodeNum = this.doms[currentNodeNum];
+ }
+ dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val);
+ domMap.Add(this.postOrderNumberToNode[i].Val, dominators);
+ }
+ }
+ StringBuilder sb = new StringBuilder();
+ sb.Append("{");
+ bool first = true;
+ foreach (KeyValuePair<Node, List<Node>> de in domMap) {
+ if (!first)
+ sb.Append(", ");
+ Contract.Assert(!object.Equals(de.Key, default(Node)));
+ sb.Append(de.Key.ToString());
+ sb.Append("~>");
+ sb.Append(ListToString(de.Value));
+ first = false;
+ }
+ sb.Append("}");
+ return sb.ToString();
+ }
+ private void PrintIntArray(int[] xs) {
+ Console.Write("[");
+ for (int i = 0; i < xs.Length; i++) {
+ if (0 < i)
+ Console.Write(", ");
+ Console.Write(xs[i]);
+ }
+ Console.WriteLine("]");
+ }
+ public void PrintList<T>(IEnumerable<T> xs) {
+ Console.Write("[");
+ int i = 0;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (0 < i)
+ Console.Write(", ");
+ Console.Write(x.ToString());
+ i++;
+ }
+ Console.WriteLine("]");
+ }
+ public string/*!*/ ListToString<T>(IEnumerable<T> xs) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("[");
+ bool first = true;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (!first)
+ sb.Append(", ");
+ sb.Append(x.ToString());
+ first = false;
+ }
+ sb.Append("]");
+ return sb.ToString();
+ }
+
+ // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001.
+ // http://citeseer.ist.psu.edu/cooper01simple.html
+ private void NewComputeDominators() {
+ int n = this.graph.Nodes.Count;
+ this.postOrderNumberToNode = new Maybe<Node>[n + 1];
+ this.nodeToPostOrderNumber = new Dictionary<Node, int>();
+ //HashSet<Node> visited = new HashSet<Node>();
+ //int currentNumber = 1;
+ Contract.Assume(this.source != null);
+ //this.PostOrderVisit(this.source, visited, ref currentNumber);
+ this.PostOrderVisitIterative(this.source);
+ this.sourceNum = this.nodeToPostOrderNumber[source];
+ // for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); }
+ this.doms = new int[n + 1]; // 0 is unused: means undefined
+ Node start_node = this.source;
+ this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node];
+ bool changed = true;
+ // PrintIntArray(doms);
+ while (changed) {
+ changed = false;
+ // for all nodes, b, in reverse postorder (except start_node)
+ for (int nodeNum = n - 1; 1 <= nodeNum; nodeNum--) {
+ Node b = this.postOrderNumberToNode[nodeNum].Val;
+ IEnumerable<Node> predecessors = this.graph.Predecessors(b);
+ // find a predecessor (i.e., a higher number) for which
+ // the doms array has been set
+ int new_idom = 0;
+ int first_processed_predecessor = 0;
+ #region new_idom <- number of first (processed) predecessor of b (pick one)
+ foreach (Node p in predecessors) {
+ if (this.doms[this.nodeToPostOrderNumber[p]] != 0) {
+ int x = this.nodeToPostOrderNumber[p];
+ new_idom = x;
+ first_processed_predecessor = x;
+ break;
+ }
+ }
+ #endregion
+ #region for all other predecessors, p, of b
+ foreach (Node p in predecessors) {
+ if (this.nodeToPostOrderNumber[p] == first_processed_predecessor) {
+ continue;
+ }
+ if (this.doms[this.nodeToPostOrderNumber[p]] != 0)
+ new_idom = intersect(this.nodeToPostOrderNumber[p], new_idom, this.doms);
+ }
+ #endregion
+ if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom) {
+ this.doms[this.nodeToPostOrderNumber[b]] = new_idom;
+ changed = true;
+ }
+ }
+ }
+ #region Populate the Immediate Dominator Map
+ int sourceNum = this.nodeToPostOrderNumber[this.source];
+ immediateDominatorMap = new Dictionary<Node, List<Node>>();
+ for (int i = 1; i <= n; i++) {
+ Node node = this.postOrderNumberToNode[i].Val;
+ Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val;
+ if (i == sourceNum && this.doms[i] == sourceNum) {
+ continue;
+ }
+ if (immediateDominatorMap.ContainsKey(idomNode)) {
+ immediateDominatorMap[idomNode].Add(node);
+ } else {
+ List<Node> l = new List<Node>();
+ l.Add(node);
+ immediateDominatorMap.Add(idomNode, l);
+ }
+ }
+ #endregion
+ }
+ private int intersect(int b1, int b2, int[] doms) {
+ int finger1 = b1;
+ int finger2 = b2;
+ while (finger1 != finger2) {
+ while (finger1 < finger2) {
+ finger1 = doms[finger1];
+ }
+ while (finger2 < finger1) {
+ finger2 = doms[finger2];
+ }
+ }
+ return finger1;
+ }
+ private void PostOrderVisit(Node/*!*/ n, HashSet<Node> visited, ref int currentNumber) {
+ Contract.Requires(n != null);
+ if (visited.Contains(n))
+ return;
+ visited.Add(n);
+ foreach (Node/*!*/ child in this.graph.Successors(n)) {
+ Contract.Assert(child != null);
+ PostOrderVisit(child, visited, ref currentNumber);
+ }
+ Contract.Assume(this.postOrderNumberToNode != null);
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ this.postOrderNumberToNode[currentNumber].Val = n;
+ this.nodeToPostOrderNumber[n] = currentNumber;
+ currentNumber++;
+ return;
+ }
+ // Iterative version: mimics the above recursive procedure
+ private void PostOrderVisitIterative(Node n)
+ {
+ Contract.Requires(n != null);
+ var visited = new HashSet<Node>();
+ var grey = new HashSet<Node>();
+ var stack = new Stack<Node>();
+
+ int currentNumber = 1;
+
+ stack.Push(n);
+ visited.Add(n);
+
+ while (stack.Count != 0)
+ {
+ var curr = stack.Pop();
+
+ if (grey.Contains(curr))
+ {
+ Contract.Assume(this.postOrderNumberToNode != null);
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ this.postOrderNumberToNode[currentNumber].Val = curr;
+ this.nodeToPostOrderNumber[curr] = currentNumber;
+ currentNumber++;
+ }
+ else
+ {
+ grey.Add(curr);
+ stack.Push(curr);
+ foreach (Node/*!*/ child in this.graph.Successors(curr))
+ {
+ Contract.Assert(child != null);
+ if (!visited.Contains(child))
+ {
+ visited.Add(child);
+ stack.Push(child);
+ }
+ }
+ }
+
+ }
+
+
+ }
+
+ public Node LeastCommonAncestor(Node n1, Node n2)
+ {
+ int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2];
+ int lca = intersect(num1, num2, this.doms);
+ return postOrderNumberToNode[lca].Val;
+ }
+ }
+
+ public class Graph<Node> {
+ private HashSet<Tuple<Node/*!*/, Node/*!*/>> es;
+ private HashSet<Node> ns;
+ private Node source;
+ private bool reducible;
+ private HashSet<Node> headers;
+ private Dictionary<Node, HashSet<Node>> backEdgeNodes;
+ private Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;
+ private HashSet<Node> splitCandidates;
+
+ private DomRelation<Node> dominatorMap = null;
+ private Dictionary<Node, HashSet<Node>> predCache = new Dictionary<Node, HashSet<Node>>();
+ private Dictionary<Node, HashSet<Node>> succCache = new Dictionary<Node, HashSet<Node>>();
+ private bool predComputed;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null));
+ Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));
+ }
+
+ private class PreHeader {
+ Node/*!*/ myHeader;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(myHeader != null);
+ }
+
+ internal PreHeader(Node/*!*/ h) {
+ Contract.Requires(h != null);
+ myHeader = h;
+ }
+
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "#" + myHeader.ToString();
+ }
+ }
+
+ public Graph(HashSet<Tuple<Node/*!*/, Node/*!*/>> edges) {
+
+ Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null));
+ es = edges;
+
+ // original A#
+ //ns = Set<Node>{ x : <x,y> in es } + Set<Node>{ y : <x,y> in es };
+
+ // closest Spec#
+ //ns = new Set<Node>{ Tuple<Node,Node> p in edges; p.Item1 } + new Set<Node>{ Tuple<Node,Node> p in edges; p.Item2 };
+
+ //
+ HashSet<Node> temp = new HashSet<Node>();
+ foreach (Tuple<Node/*!*/, Node/*!*/> p in edges) {
+ Contract.Assert(p.Item1 != null);
+ temp.Add(p.Item1);
+ Contract.Assert(p.Item2 != null);
+ temp.Add(p.Item2);
+ }
+ ns = temp;
+ }
+ public Graph() {
+ es = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
+ ns = new HashSet<Node>();
+ }
+
+ // BUGBUG: Set<T>.ToString() should return a non-null string
+ [Pure]
+ public override string/*!*/ ToString() {
+ return "" + es.ToString();
+ }
+
+ public void AddSource(Node/*!*/ x) {
+ Contract.Requires(x != null);
+ // BUGBUG: This generates bad code in the compiler
+ //ns += new Set<Node>{x};
+ ns.Add(x);
+ source = x;
+ }
+
+ public void AddEdge(Node/*!*/ source, Node/*!*/ dest) {
+ Contract.Requires(source != null);
+ Contract.Requires(dest != null);
+ //es += Set<Edge>{<source,dest>};
+ //ns += Set<Node>{source, dest};
+ es.Add(new Tuple<Node/*!*/, Node/*!*/>(source, dest));
+ ns.Add(source);
+ ns.Add(dest);
+ predComputed = false;
+ }
+
+ public HashSet<Node> Nodes {
+ get {
+ return ns;
+ }
+ }
+ public IEnumerable<Tuple<Node/*!*/, Node/*!*/>> Edges {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Tuple<Node, Node>>>())
+ && Contract.ForAll(Contract.Result<IEnumerable<Tuple<Node, Node>>>(), n =>
+ n.Item1 != null && n.Item2 != null));
+ return es;
+ }
+ }
+
+ public bool Edge(Node/*!*/ x, Node/*!*/ y) {
+ Contract.Requires(x != null);
+ Contract.Requires(y != null);
+ // original A#
+ // return <x,y> in es;
+ return es.Contains(new Tuple<Node/*!*/, Node/*!*/>(x, y));
+ }
+
+ private void ComputePredSuccCaches() {
+ if (predComputed)
+ return;
+ predComputed = true;
+ predCache = new Dictionary<Node, HashSet<Node>>();
+ succCache = new Dictionary<Node, HashSet<Node>>();
+
+ foreach (Node n in Nodes) {
+ predCache[n] = new HashSet<Node>();
+ succCache[n] = new HashSet<Node>();
+ }
+
+ foreach (Tuple<Node/*!*/, Node/*!*/> p in Edges) {
+ Contract.Assert(p.Item1 != null);
+ Contract.Assert(p.Item2 != null);
+ HashSet<Node> tmp;
+
+ tmp = predCache[p.Item2];
+ tmp.Add(p.Item1);
+ predCache[p.Item2] = tmp;
+
+ tmp = succCache[p.Item1];
+ tmp.Add(p.Item2);
+ succCache[p.Item1] = tmp;
+ }
+ }
+
+ public IEnumerable<Node> Predecessors(Node n) {
+ // original A#
+ //Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
+
+ ComputePredSuccCaches();
+ return predCache[n];
+ }
+
+ public IEnumerable<Node> Successors(Node n) {
+ ComputePredSuccCaches();
+ return succCache[n];
+ }
+
+ public List<Node> SuccessorsAsList(Node n) {
+ ComputePredSuccCaches();
+ List<Node> ret = new List<Node>();
+ foreach (Node s in succCache[n])
+ ret.Add(s);
+ return ret;
+ }
+
+ public DomRelation<Node> /*Map<Node,Set<Node>>*/ DominatorMap {
+ get {
+ Contract.Assert(source != null);
+ if (this.dominatorMap == null) {
+ this.dominatorMap = new DomRelation<Node>(this, this.source);
+ }
+ return this.dominatorMap;
+ }
+ }
+
+ public Dictionary<Node, List<Node>> ImmediateDominatorMap {
+ get {
+ Contract.Assert(source != null);
+ if (this.dominatorMap == null) {
+ this.dominatorMap = new DomRelation<Node>(this, this.source);
+ }
+ return this.dominatorMap.ImmediateDominatorMap;
+ }
+ }
+ public List<Node> ImmediatelyDominatedBy(Node/*!*/ n) {
+ Contract.Requires(n != null);
+ List<Node> dominees;
+ this.ImmediateDominatorMap.TryGetValue(n, out dominees);
+ return dominees == null ? new List<Node>() : dominees;
+ }
+
+ public IEnumerable<Node/*?*/> TopologicalSort(bool reversed = false) {
+ bool acyclic;
+ List<Node> sortedList;
+ this.TarjanTopSort(out acyclic, out sortedList, reversed);
+ return acyclic ? sortedList : new List<Node>();
+ }
+ // From Tarjan 1972
+ public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes, bool reversed = false) {
+ int n = this.Nodes.Count;
+ if (n == 0) {
+ acyclic = true;
+ sortedNodes = new List<Node>();
+ return;
+ }
+ int[] incomingEdges = new int[n];
+ // need an arbitrary numbering for the nodes to use as indices into
+ // the arrays used within this algorithm
+ Dictionary<Node, int> nodeToNumber = new Dictionary<Node, int>(n);
+ Maybe<Node>[] numberToNode = new Maybe<Node>[n];
+ int counter = 0;
+ foreach (Node node in this.Nodes) {
+ numberToNode[counter].Val = node;
+ nodeToNumber[node] = counter;
+ counter++;
+ }
+ foreach (Tuple<Node/*!*/, Node/*!*/> e in this.Edges) {
+ Contract.Assert(e.Item1 != null);
+ Contract.Assert(e.Item2 != null);
+ Node/*!*/ target = e.Item2;
+ incomingEdges[nodeToNumber[target]]++;
+ }
+ List<Node> sorted = new List<Node>();
+ int sortedIndex = 0;
+ while (sortedIndex < n) {
+ // find a root (i.e., its index)
+ int rootIndex = -1;
+ if (reversed) {
+ for (int i = n-1; i >= 0; i--) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
+ }
+ } else {
+ for (int i = 0; i < n; i++) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
+ }
+ }
+ if (rootIndex == -1) {
+ acyclic = false;
+ sortedNodes = new List<Node>();
+ return;
+ }
+ // mark root so it won't be used again
+ incomingEdges[rootIndex] = -1;
+ Node root = numberToNode[rootIndex].Val;
+ sorted.Add(root);
+ ++sortedIndex;
+ foreach (Node s in this.Successors(root)) {
+ incomingEdges[nodeToNumber[s]]--;
+ }
+ }
+ acyclic = true;
+ sortedNodes = sorted;
+ return;
+ }
+ private IEnumerable<Node> OldTopologicalSort() {
+ Tuple<bool, List<Node>> result = this.TopSort();
+ return result.Item1 ? result.Item2 : (IEnumerable<Node>)new List<Node>();
+ }
+ // From AsmL distribution example
+ private Tuple<bool, List<Node>> TopSort()
+ {
+ List<Node> S = new List<Node>();
+ HashSet<Node> V = this.Nodes;
+ HashSet<Node> X = new HashSet<Node>();
+ foreach (Node/*!*/ n in V) {
+ Contract.Assert(n != null);
+ X.Add(n);
+ }
+ bool change = true;
+ while (change)
+ // invariant: X = V - S
+ {
+ change = false;
+ if (X.Count > 0) {
+ foreach (Node/*!*/ n in X) {
+ Contract.Assert(n != null);
+ // see if n has any incoming edges from any other node in X
+ bool inDegreeZero = true;
+ foreach (Node/*!*/ u in X) {
+ Contract.Assert(u != null);
+ if (this.Edge(u, n)) {
+ inDegreeZero = false;
+ break; // no point looking further
+ }
+ }
+ if (inDegreeZero) {
+ S.Add(n);
+ X.Remove(n);
+ change = true;
+ break; // might as well go back and start looking through X from the beginning
+ }
+ }
+ // Then we made it all the way through X without finding a source node
+ if (!change) {
+ return new Tuple<bool, List<Node>>(false, new List<Node>());
+ }
+ }
+ }
+ return new Tuple<bool, List<Node>>(true, S);
+ }
+
+ public static bool Acyclic(Graph<Node> g, Node source) {
+ bool acyclic;
+ List<Node> sortedList;
+ g.TarjanTopSort(out acyclic, out sortedList);
+ return acyclic;
+ }
+
+ // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.]
+ static HashSet<Node> NaturalLoop(Graph<Node> g, Tuple<Node/*!*/, Node/*!*/> backEdge)
+ {
+ Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null);
+ Node/*!*/ n = backEdge.Item1;
+ Node/*!*/ d = backEdge.Item2;
+ Stack<Node> stack = new Stack<Node>();
+ HashSet<Node> loop = new HashSet<Node>();
+ loop.Add(d);
+ if (!n.Equals(d)) // then n is not in loop
+ {
+ loop.Add(n);
+ stack.Push(n); // push n onto stack
+ }
+ while (stack.Count > 0) // not empty
+ {
+ Node m = stack.Peek();
+ stack.Pop(); // pop stack
+ foreach (Node/*!*/ p in g.Predecessors(m)) {
+ Contract.Assert(p != null);
+ if (!(loop.Contains(p))) {
+ loop.Add(p);
+ stack.Push(p); // push p onto stack
+ }
+ }
+ }
+ return loop;
+ }
+
+ internal struct ReducibleResult {
+ internal bool reducible;
+ internal HashSet<Node> headers;
+ internal Dictionary<Node, HashSet<Node>> backEdgeNodes;
+ internal Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops;
+ internal HashSet<Node> splitCandidates;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null));
+ }
+
+ internal ReducibleResult(bool b, HashSet<Node> headers, Dictionary<Node, HashSet<Node>> backEdgeNodes, Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops, HashSet<Node> splitCandidates)
+ {
+ Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null));
+ this.reducible = b;
+ this.headers = headers;
+ this.backEdgeNodes = backEdgeNodes;
+ this.naturalLoops = naturalLoops;
+ this.splitCandidates = splitCandidates;
+ }
+
+ }
+
+ // [Dragon, p. 606]
+ static ReducibleResult ComputeReducible(Graph<Node> g, Node source) {
+ // first, compute the dom relation
+ DomRelation<Node> /*Map<Node,Set<Node>>*/ D = g.DominatorMap;
+ return ComputeReducible(g, source, D);
+ }
+
+ static HashSet<Node> FindCycle(Graph<Node> g, Node source) {
+ Stack<Tuple<Node, List<Node>>> stack = new Stack<Tuple<Node, List<Node>>>();
+ HashSet<Node> stackAsSet = new HashSet<Node>();
+ HashSet<Node> visited = new HashSet<Node>();
+ stack.Push(new Tuple<Node, List<Node>>(source, g.SuccessorsAsList(source)));
+ stackAsSet.Add(source);
+ while (stack.Count > 0) {
+ Tuple<Node, List<Node>> tuple = stack.Peek();
+ List<Node> children = tuple.Item2;
+ if (children.Count == 0) {
+ stack.Pop();
+ stackAsSet.Remove(tuple.Item1);
+ continue;
+ }
+ Node n = children[0];
+ children.RemoveAt(0);
+ if (stackAsSet.Contains(n)) {
+ HashSet<Node> ret = new HashSet<Node>();
+ ret.Add(n);
+ while (true) {
+ Node x = stack.Pop().Item1;
+ if (x.Equals(n))
+ return ret;
+ }
+ }
+ if (visited.Contains(n))
+ continue;
+ stack.Push(new Tuple<Node, List<Node>>(n, g.SuccessorsAsList(n)));
+ visited.Add(n);
+ stackAsSet.Add(n);
+ System.Diagnostics.Debug.Assert(stack.Count == stackAsSet.Count);
+ }
+ return new HashSet<Node>();
+ }
+
+ // [Dragon, p. 606]
+ static ReducibleResult ComputeReducible(Graph<Node> g,
+ Node source,
+ DomRelation<Node>/*!*/ DomRelation) {
+ Contract.Requires(DomRelation != null);
+
+ //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible");
+ IEnumerable<Tuple<Node/*!*/, Node/*!*/>> edges = g.Edges;
+ Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null));
+ HashSet<Tuple<Node/*!*/, Node/*!*/>> backEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
+ HashSet<Tuple<Node/*!*/, Node/*!*/>> nonBackEdges = new HashSet<Tuple<Node/*!*/, Node/*!*/>>();
+ foreach (Tuple<Node/*!*/, Node/*!*/> e in edges) {
+ Contract.Assert(e.Item1 != null);
+ Contract.Assert(e.Item2 != null);
+ Node x = e.Item1;
+ Node y = e.Item2; // so there is an edge from x to y
+ if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x
+ backEdges.Add(e);
+ } else {
+ nonBackEdges.Add(e);
+ }
+ }
+ Graph<Node> withoutBackEdges = new Graph<Node>(nonBackEdges);
+ if (!Acyclic(withoutBackEdges, source)) {
+ return new ReducibleResult(false,
+ new HashSet<Node>(),
+ new Dictionary<Node, HashSet<Node>>(),
+ new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>(),
+ FindCycle(withoutBackEdges, source));
+ } else {
+ // original A#:
+ //Set<Node> headers = Set{ d : <n,d> in backEdges };
+ HashSet<Node> headers = new HashSet<Node>();
+ foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {
+
+ Contract.Assert(e.Item1 != null);
+ Contract.Assert(e.Item2 != null);
+ headers.Add(e.Item2);
+ }
+ // original A#:
+ //Map<Node,Set<Node>> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set<Node>{ b : <b,x> in backEdges, x == h } };
+ Dictionary<Node, HashSet<Node>> backEdgeNodes = new Dictionary<Node, HashSet<Node>>();
+ foreach (Node/*!*/ h in headers) {
+ Contract.Assert(h != null);
+ HashSet<Node> bs = new HashSet<Node>();
+ foreach (Tuple<Node, Node> backedge in backEdges) {
+ Contract.Assert(backedge.Item1 != null);
+ Contract.Assert(backedge.Item2 != null);
+ if (backedge.Item2.Equals(h)) {
+ bs.Add(backedge.Item1);
+ }
+ }
+ backEdgeNodes.Add(h, bs);
+ }
+
+ // original A#:
+ //Map<Tuple<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };
+ Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>> naturalLoops = new Dictionary<Tuple<Node/*!*/, Node/*!*/>, HashSet<Node>>();
+ foreach (Tuple<Node/*!*/, Node/*!*/> e in backEdges) {
+ Contract.Assert(e.Item1 != null && e.Item2 != null);
+ naturalLoops.Add(e, NaturalLoop(g, e));
+ }
+
+ //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible");
+ return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops, new HashSet<Node>());
+ }
+ }
+
+ public bool Reducible {
+ get {
+ return reducible;
+ }
+ }
+ public IEnumerable<Node> Headers {
+ get {
+ return headers;
+ }
+ }
+ public IEnumerable<Node> BackEdgeNodes(Node/*!*/ h) {
+ Contract.Requires(h != null);
+ // original A#:
+ //return h in backEdgeNodes ? backEdgeNodes[h] : null;
+ return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new List<Node>());
+ }
+ public IEnumerable<Node> NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) {
+ Contract.Requires(header != null);
+ Contract.Requires(backEdgeNode != null);
+ Tuple<Node/*!*/, Node/*!*/> e = new Tuple<Node/*!*/, Node/*!*/>(backEdgeNode, header);
+ return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new List<Node>();
+ }
+ public HashSet<Node> SplitCandidates {
+ get {
+ return splitCandidates;
+ }
+ }
+ public void ComputeLoops() {
+ ReducibleResult r = ComputeReducible(this, this.source);
+ this.reducible = r.reducible;
+ this.headers = r.headers;
+ this.backEdgeNodes = r.backEdgeNodes;
+ this.naturalLoops = r.naturalLoops;
+ this.splitCandidates = r.splitCandidates;
+ return;
+ }
+
+ public IEnumerable<Node> SortHeadersByDominance()
+ {
+ Graph<Node> dag = new Graph<Node>();
+ foreach (Node b in headers)
+ {
+ dag.AddSource(b);
+ foreach (Node c in headers)
+ {
+ if (b.Equals(c)) continue;
+ if (DominatorMap.DominatedBy(b, c))
+ {
+ System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b));
+ dag.AddEdge(b, c);
+ }
+ }
+ }
+ return dag.TopologicalSort();
+ }
+
+ public string ToDot(Func<Node, string> NodeLabel = null, Func<Node, string> NodeStyle = null) {
+ NodeLabel = NodeLabel ?? (n => n.ToString());
+ NodeStyle = NodeStyle ?? (n => "[shape=box]");
+ var s = new StringBuilder();
+ s.AppendLine("digraph G {");
+ foreach (var n in Nodes)
+ s.AppendLine(" \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";");
+ foreach (var e in Edges)
+ s.AppendLine(" \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";");
+ s.AppendLine("}");
+ return s.ToString();
+ }
+
+ public ICollection<Node> ComputeReachable() {
+ ICollection<Node> result = new HashSet<Node>();
+ Stack<Node> stack = new Stack<Node>();
+ stack.Push(source);
+ while(!(stack.Count() == 0)) {
+ Node n = stack.Pop();
+ result.Add(n);
+ foreach(var m in Successors(n)) {
+ if(!result.Contains(m)) {
+ stack.Push(m);
+ }
+ }
+ }
+ return result;
+ }
+
+ } // end: class Graph
+
+ public static class GraphAlgorithms
+ {
+
+
+ public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
+ {
+ var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
+ Node source;
+ if (exits.Count == 0)
+ exits.Add(dummySource);
+ var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
+ if (exits.Count == 1)
+ {
+ dual.AddSource(exits[0]);
+ source = exits[0];
+ }
+ else
+ {
+ dual.AddSource(dummySource);
+ source = dummySource;
+ foreach (var exit in exits)
+ dual.AddEdge(dummySource, exit);
+ }
+
+ #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node
+ foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item)))
+ {
+ dual.AddEdge(source, n);
+ }
+ #endregion
+
+ return dual;
+ }
+
+ 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];
+ var predecessors = new List<int>[n];
+ int[] incomingEdges = new int[n];
+
+ for (int i = 0; i < n; i++)
+ predecessors[i] = new List<int>();
+
+ 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]++;
+ }
+ predecessors[target].Add(source);
+ }
+
+ var sortedNodes = new List<Tuple<Node, bool>>();
+ var sortedNodesInternal = new List<int>();
+
+ var regionStack = new Stack<Tuple<Node, List<int>>>();
+ regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
+
+ while (regionStack.Count != 0)
+ {
+ var rootIndexes = new List<int>();
+ foreach (var i in regionStack.Peek().Item2)
+ {
+ if (incomingEdges[i] == 0)
+ rootIndexes.Add(i);
+ }
+ if (rootIndexes.Count() == 0)
+ {
+ var region = regionStack.Pop();
+ if (regionStack.Count != 0) {
+ sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+ sortedNodesInternal.Add(nodeToNumber[region.Item1]);
+ }
+ continue;
+ }
+ int rootIndex = rootIndexes[0];
+ int maxPredIndex = -1;
+ foreach (var i in rootIndexes) {
+ foreach (var p in predecessors[i]) {
+ int predIndex =
+ sortedNodesInternal.FindLastIndex(x => x == p);
+ if (predIndex > maxPredIndex) {
+ rootIndex = i;
+ maxPredIndex = predIndex;
+ }
+ }
+ }
+ incomingEdges[rootIndex] = -1;
+ sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+ sortedNodesInternal.Add(rootIndex);
+ 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;
+ }
+
+ // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
+ // "The Program Dependence Graph and Its Use in Optimization"
+ public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new()
+ {
+ Graph<Node> dual = g.Dual(new Node());
+ DomRelation<Node> pdom = dual.DominatorMap;
+
+ var result = new Dictionary<Node, HashSet<Node>>();
+
+ var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
+ foreach (var edge in S)
+ {
+ var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
+ var deps = new List<Node>();
+ if (L == edge.Item1)
+ {
+ pdom.DominatedBy(edge.Item2, edge.Item1, deps);
+ deps.Add(edge.Item2);
+ deps.Add(edge.Item1);
+ }
+ else
+ {
+ pdom.DominatedBy(edge.Item2, L, deps);
+ deps.Add(edge.Item2);
+ }
+ if (result.ContainsKey(edge.Item1))
+ {
+ result[edge.Item1].UnionWith(deps);
+ }
+ else
+ {
+ result[edge.Item1] = new HashSet<Node>(deps);
+ }
+ }
+
+ return result;
+ }
+
+ public static void TransitiveClosure<Node>(this Dictionary<Node, HashSet<Node>> graph) where Node : class {
+ bool changed;
+ do {
+ changed = false;
+ foreach (var entry in graph) {
+ var newSuccessors = new HashSet<Node>(entry.Value);
+ foreach (var successor in entry.Value) {
+ if (graph.ContainsKey(successor))
+ newSuccessors.UnionWith(graph[successor]);
+ }
+ if (newSuccessors.Count != entry.Value.Count) {
+ entry.Value.UnionWith(newSuccessors);
+ changed = true;
+ }
+ }
+ } while (changed);
+ }
+
+ }
+
+ public delegate System.Collections.IEnumerable/*<Node!>*//*!*/ Adjacency<T>(T/*!*/ node);
+
+
+ // An SCC is a set of nodes
+ public sealed class SCC<Node> : ICollection<Node>
+ {
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(nodesMap != null);
+ }
+
+ private IDictionary<Node, object>/*!*/ nodesMap = new Dictionary<Node, object>();
+ private ICollection<Node>/*!*/ nodes
+ {
+ get
+ {
+ return cce.NonNull(nodesMap.Keys);
+ }
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
+
+ return ((System.Collections.IEnumerable)nodes).GetEnumerator();
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator<Node>/*!*/ IEnumerable<Node>.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<IEnumerator<Node>>() != null);
+
+ return ((IEnumerable<Node>)nodes).GetEnumerator();
+ }
+
+ public int Count
+ {
+ get
+ {
+ return nodes.Count;
+ }
+ }
+ public bool IsReadOnly
+ {
+ get
+ {
+ return nodesMap.IsReadOnly;
+ }
+ }
+ public void Add(Node item)
+ {
+ nodesMap.Add(item, null);
+ }
+ public void Clear()
+ {
+ nodesMap.Clear();
+ }
+ [Pure]
+ public bool Contains(Node item)
+ {
+ return nodesMap.ContainsKey(item);
+ }
+ public void CopyTo(Node[] array, int arrayIndex)
+ {
+ //Contract.Requires(array != null);
+ nodes.CopyTo(array, arrayIndex);
+ }
+ public bool Remove(Node item)
+ {
+ return nodesMap.Remove(item);
+ }
+ }
+
+ public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class
+ {
+ private readonly IDictionary<Node/*!*/, object>/*!*/ graph;
+ [ContractInvariantMethod]
+ void graphInvariantMethod()
+ {
+ Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null));
+ Contract.Invariant(preds != null);
+ Contract.Invariant(succs != null);
+ }
+ private readonly Adjacency<Node>/*!*/ preds;
+ private readonly Adjacency<Node>/*!*/ succs;
+
+ private bool computed = false;
+ public bool Computed
+ {
+ get
+ {
+ return computed;
+ }
+ }
+
+ [NotDelayed]
+ public StronglyConnectedComponents(System.Collections.IEnumerable/*<Node!>*/ graph, Adjacency<Node> preds, Adjacency<Node> succs)
+ : base()
+ {
+ Contract.Requires(succs != null);
+ Contract.Requires(preds != null);
+ Contract.Requires(graph != null);
+ Contract.Ensures(!Computed);
+ IDictionary<Node/*!*/, object>/*!*/ dict = new Dictionary<Node/*!*/, object>();
+ foreach (Node/*!*/ n in graph)
+ {
+ Contract.Assert(n != null);
+ dict.Add(n, null);
+ }
+
+ this.graph = dict;
+ this.preds = preds;
+ this.succs = succs;
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
+
+ return ((System.Collections.IEnumerable)sccs).GetEnumerator();
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator<SCC<Node>/*!*/>/*!*/ IEnumerable<SCC<Node>/*!*/>.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<IEnumerator<SCC<Node>>>() != null);
+
+ Contract.Assume(Computed);
+ Contract.Assert(cce.NonNullElements((IEnumerable<SCC<Node>/*!*/>)sccs));//REVIEW
+ return ((IEnumerable<SCC<Node>/*!*/>)sccs).GetEnumerator();
+ }
+
+ private readonly IList<SCC<Node>/*!*/>/*!*/ sccs = new List<SCC<Node>/*!*/>();
+ [ContractInvariantMethod]
+ void sccsInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(sccs));
+ }
+
+
+ public void Compute()
+ {
+ Contract.Requires(!Computed);
+ Contract.Ensures(Computed);
+ // Compute post times on graph with edges reversed
+ this.dfsNext = this.preds;
+ foreach (Node/*!*/ n in cce.NonNull(graph.Keys))
+ {
+ Contract.Assert(n != null);
+ if (!seen.ContainsKey(n))
+ {
+ OrderNodes(n);
+ }
+ }
+
+ // Clear seen
+ seen.Clear();
+
+ // Compute SCCs
+ this.dfsNext = this.succs;
+ while (postOrder.Count > 0)
+ {
+ Node/*!*/ n = postOrder.Pop();
+ Contract.Assert(n != null);
+
+ if (!seen.ContainsKey(n))
+ {
+ SCC<Node>/*!*/ curr = new SCC<Node>();
+ FindSCCs(n, curr);
+ sccs.Add(curr);
+ }
+ }
+
+ // Clear seen
+ seen.Clear();
+
+ this.computed = true;
+ }
+
+ private Adjacency<Node>/*?*/ dfsNext = null;
+
+ private readonly IDictionary<Node/*!*/, object>/*!*/ seen = new Dictionary<Node/*!*/, object>();
+ private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(seen != null);
+ Contract.Invariant(cce.NonNullElements(postOrder));
+ }
+
+
+ // DFS to order nodes by post times
+ private void OrderNodes(Node node)
+ {
+ Contract.Requires(node != null);
+ seen.Add(node, null);
+
+ Contract.Assert(dfsNext != null);
+ System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
+ Contract.Assert(nexts != null);
+ foreach (Node/*!*/ n in nexts)
+ {
+ Contract.Assert(n != null);
+ if (graph.ContainsKey(n) && !seen.ContainsKey(n))
+ {
+ OrderNodes(n);
+ }
+ }
+
+ postOrder.Push(node);
+ }
+
+ // DFS to compute SCCs
+ private void FindSCCs(Node node, SCC<Node> currSCC)
+ {
+ Contract.Requires(currSCC != null);
+ Contract.Requires(node != null);
+ //modifies currSCC.*;
+ seen.Add(node, null);
+ currSCC.Add(node);
+
+ Contract.Assert(dfsNext != null);
+ System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
+ Contract.Assert(nexts != null);
+ foreach (Node/*!*/ n in nexts)
+ {
+ Contract.Assert(n != null);
+ if (graph.ContainsKey(n) && !seen.ContainsKey(n))
+ {
+ FindSCCs(n, currSCC);
+ }
+ }
+ }
+
+ [Pure]
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ string outStr = "";
+ int i = 0;
+
+ foreach (ICollection<Node> component in this)
+ {
+ string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++);
+ Contract.Assert(tmp != null);
+ outStr += tmp;
+
+ bool firstInRow = true;
+
+ foreach (Node b in component)
+ {
+ string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b);
+ Contract.Assert(tmpComponent != null);
+ outStr += tmpComponent;
+ firstInRow = false;
+ }
+ }
+ return outStr;
+ }
+
+ }
+
+ public class GraphProgram {
+ static void TestGraph<T>(T/*!*/ source, params Tuple<T/*!*/, T/*!*/>[] edges) {
+ Contract.Requires(source != null);
+ Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null));
+ HashSet<Tuple<T/*!*/, T/*!*/>> es = new HashSet<Tuple<T/*!*/, T/*!*/>>();
+ foreach (Tuple<T/*!*/, T/*!*/> e in edges) {
+ Contract.Assert(e.Item1 != null && e.Item2 != null);
+ es.Add(e);
+ }
+ Graph<T> g = new Graph<T>(es);
+ g.AddSource(source);
+ Console.WriteLine("G = " + g);
+ g.ComputeLoops();
+ Console.WriteLine("G's Dominator Map = " + g.DominatorMap);
+ Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap));
+ Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no"));
+ }
+
+ static void Main(string[] args)
+ //requires forall{string s in args; s != null};
+ {
+ Console.WriteLine("Spec# says hello!");
+ // This generates bad IL -- need to fix a bug in the compiler
+ //Graph<int> g = new Graph<int>(new Set<Tuple<int,int>>{ new Tuple<int,int>(1,2), new Tuple<int,int>(1,3), new Tuple<int,int>(2,3) });
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Tuple<char, char>('a', 'b'),
+ new Tuple<char, char>('a', 'c'),
+ new Tuple<char, char>('b', 'c')
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Tuple<char, char>('a', 'b'),
+ new Tuple<char, char>('a', 'c'),
+ new Tuple<char, char>('b', 'd'),
+ new Tuple<char, char>('c', 'e'),
+ new Tuple<char, char>('c', 'f'),
+ new Tuple<char, char>('d', 'e'),
+ new Tuple<char, char>('e', 'd'),
+ new Tuple<char, char>('e', 'f'),
+ new Tuple<char, char>('f', 'e')
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Tuple<char, char>('a', 'b'),
+ new Tuple<char, char>('a', 'c'),
+ new Tuple<char, char>('b', 'c'),
+ new Tuple<char, char>('c', 'b')
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(1,
+ new Tuple<int, int>(1, 2),
+ new Tuple<int, int>(1, 3),
+ new Tuple<int, int>(2, 3)
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(1,
+ new Tuple<int, int>(1, 2),
+ new Tuple<int, int>(1, 3),
+ new Tuple<int, int>(2, 3),
+ new Tuple<int, int>(3, 2)
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(2,
+ new Tuple<int, int>(2, 3),
+ new Tuple<int, int>(2, 4),
+ new Tuple<int, int>(3, 2)
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Tuple<char, char>('a', 'b'),
+ new Tuple<char, char>('a', 'c'),
+ new Tuple<char, char>('b', 'c'),
+ new Tuple<char, char>('b', 'b')
+ );
+
+
+ }
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 01:31:46 +0000